source
def Lean.Expr.toCtorIfLit :
Expr → MetaM Expr
Equations

- (Lean.Expr.lit (Lean.Literal.natVal v)).toCtorIfLit = if (v == 0) = true then pure (Lean.mkConst `Nat.zero) else pure (Lean.mkApp (Lean.mkConst `Nat.succ) (Lean.mkRawNatLit (v - 1)))
- (Lean.Expr.lit (Lean.Literal.strVal v)).toCtorIfLit = Lean.Meta.whnf (Lean.mkApp (Lean.mkConst `String.mk) (Lean.toExpr v.toList))
- x✝.toCtorIfLit = pure x✝

Instances For

# Smart unfolding support #

source
@[extern lean_get_structural_rec_arg_pos]
opaque Lean.Meta.getStructuralRecArgPos? (declName : Name) :
CoreM (Option Nat)

Forward declaration. It is defined in the module `src/Lean/Elab/PreDefinition/Structural/Eqns.lean`. It is possible to avoid this hack if we move `Structural.EqnInfo` and `Structural.eqnInfoExt` to this module.

source
def Lean.Meta.smartUnfoldingSuffix :
String
Equations

- Lean.Meta.smartUnfoldingSuffix = "_sunfold"

Instances For

source
@[inline]
def Lean.Meta.mkSmartUnfoldingNameFor (declName : Name) :
Name
Equations

- Lean.Meta.mkSmartUnfoldingNameFor declName = declName.mkStr Lean.Meta.smartUnfoldingSuffix

Instances For

source
def Lean.Meta.hasSmartUnfoldingDecl (env : Environment) (declName : Name) :
Bool
Equations

- Lean.Meta.hasSmartUnfoldingDecl env declName = env.contains (Lean.Meta.mkSmartUnfoldingNameFor declName)

Instances For

source
opaque Lean.Meta.smartUnfolding :
Lean.Option Bool
source
def Lean.Meta.markSmartUnfoldingMatch (e : Expr) :
Expr

Add auxiliary annotation to indicate the `match`-expression `e` must be reduced when performing smart unfolding.

Equations

- Lean.Meta.markSmartUnfoldingMatch e = Lean.mkAnnotation `sunfoldMatch e

Instances For

source
def Lean.Meta.smartUnfoldingMatch? (e : Expr) :
Option Expr
Equations

- Lean.Meta.smartUnfoldingMatch? e = Lean.annotation? `sunfoldMatch e

Instances For

source
def Lean.Meta.markSmartUnfoldingMatchAlt (e : Expr) :
Expr

Add auxiliary annotation to indicate expression `e` (a `match` alternative rhs) was successfully reduced by smart unfolding.

Equations

- Lean.Meta.markSmartUnfoldingMatchAlt e = Lean.mkAnnotation `sunfoldMatchAlt e

Instances For

source
def Lean.Meta.smartUnfoldingMatchAlt? (e : Expr) :
Option Expr
Equations

- Lean.Meta.smartUnfoldingMatchAlt? e = Lean.annotation? `sunfoldMatchAlt e

Instances For

# Helper methods #

source
def Lean.Meta.isAuxDef (constName : Name) :
MetaM Bool
Equations

- Lean.Meta.isAuxDef constName = do let env ← Lean.getEnv pure (Lean.isAuxRecursor env constName || Lean.isNoConfusion env constName)

Instances For

# Helper functions for reducing recursors #

source
def Lean.Meta.mkProjFn (ctorVal : ConstructorVal) (us : List Level) (params : Array Expr) (i : Nat) (major : Expr) :
CoreM Expr

Create the `i`th projection `major`. It tries to use the auto-generated projection functions if available. Otherwise falls back to `Expr.proj`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

# Helper functions for reducing Quot.lift and Quot.ind #

# Helper function for extracting "stuck term" #

source
partial def Lean.Meta.getStuckMVar? (e : Expr) :
MetaM (Option MVarId)

Return `some (Expr.mvar mvarId)` if metavariable `mvarId` is blocking reduction.

# Weak Head Normal Form auxiliary combinators #

source
@[specialize #[]]
partial def Lean.Meta.whnfEasyCases (e : Expr) (k : Expr → MetaM Expr) :
MetaM Expr

Auxiliary combinator for handling easy WHNF cases. It takes a function for handling the "hard" cases as an argument

source
inductive Lean.Meta.ReduceMatcherResult :
Type

- reduced (val : Expr) : ReduceMatcherResult
- stuck (val : Expr) : ReduceMatcherResult
- notMatcher : ReduceMatcherResult
- partialApp : ReduceMatcherResult

Instances For

The "match" compiler uses dependent if-then-else `dite` and other auxiliary declarations to compile match-expressions such as

    match v with
    | 'a' => 1
    | 'b' => 2
    | _   => 3

because it is more efficient than using `casesOn` recursors. The method `reduceMatcher?` fails if these auxiliary definitions cannot be unfolded in the current transparency setting. This is problematic because tactics such as `simp` use `TransparencyMode.reducible`, and most users assume that expressions such as

    match 0 with
    | 0 => 1
    | 100 => 2
    | _ => 3

should reduce in any transparency mode.

Thus, if the transparency mode is `.reducible` or `.instances`, we first eagerly unfold `dite` constants used in the auxiliary match-declaration, and then use a custom `canUnfoldAtMatcher` predicate for `whnfMatcher`.

Remark: we used to include `dite` (and `ite`) as auxiliary declarations to unfold at `canUnfoldAtMatcher`, but this is problematic because the `dite`/`ite` may occur in the discriminant. See issue #5388.

This solution is not very modular because modifications at the `match` compiler require changes here. We claim this is defensible because it is reducing the auxiliary declaration defined by the `match` compiler.

Remark: if the eager unfolding is problematic, we may cache the result. We may also consider not using `dite` in the `match`-compiler and use `Decidable.casesOn`, but it will require changes in how we generate equation lemmas.

Alternative solution: tactics that use `TransparencyMode.reducible` should rely on the equations we generated for match-expressions. This solution is also not perfect because the match-expression above will not reduce during type checking when we are not using `TransparencyMode.default` or `TransparencyMode.all`.

source
def Lean.Meta.canUnfoldAtMatcher (cfg : Config) (info : ConstantInfo) :
CoreM Bool

Auxiliary predicate for `whnfMatcher`. See comment above.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Meta.reduceMatcher? (e : Expr) :
MetaM ReduceMatcherResult
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Meta.projectCore? (e : Expr) (i : Nat) :
MetaM (Option Expr)
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Meta.project? (e : Expr) (i : Nat) :
MetaM (Option Expr)
Equations

- Lean.Meta.project? e i = do let __do_lift ← Lean.Meta.whnf e Lean.Meta.projectCore? __do_lift i

Instances For

source
def Lean.Meta.reduceProj? (e : Expr) :
MetaM (Option Expr)

Reduce kernel projection `Expr.proj ..` expression.

Equations

- Lean.Meta.reduceProj? (Lean.Expr.proj typeName i c) = Lean.Meta.project? c i
- Lean.Meta.reduceProj? e = pure none

Instances For

source
partial def Lean.Meta.expandLet (e : Expr) (vs : Array Expr) (zetaHave : Bool := true) :
Expr

Zeta reduces `let`s/`have`s. If `zetaHave` is false, then `have`s are not zeta reduced.

Auxiliary function for `whnfCore` and `Simp.reduceStep`, to implement the `zeta` option. This function does not implement `zetaUnused` logic, which is instead the responsibility of `consumeUnusedLet`. The `expandLet` function works with expressions with loose bound variables, and thus determining whether a let variable is used isn't an O(1) operation.

Note: since `expandLet` and `consumeUnusedLet` are separated like this, a consequence is that in the `+zeta -zetaHave +zetaUnused` configuration, then `whnfCore` has quadratic complexity when reducing a sequence of alternating `let`s and `have`s where the `let`s are used but the `have`s are unused.

source
partial def Lean.Meta.consumeUnusedLet (e : Expr) (consumeNondep : Bool := false) :
Expr

Consumes unused `let`s/`have`s. If `consumeNondep` is false, then `have`s are not consumed.

Auxiliary function for `whnfCore`, `isDefEqQuick`, and `Simp.reduceStep`, to implement the `zetaUnused` option. In the case of `isDefEqQuick`, it is also used when `zeta` is set.

source
def Lean.Meta.whnfCore (e : Expr) :
MetaM Expr

Apply beta-reduction, zeta-reduction (i.e., unfold let local-decls), iota-reduction, expand let-expressions, expand assigned meta-variables.

Equations

- Lean.Meta.whnfCore e = Lean.Meta.whnfCore.go✝ e

Instances For

source
def Lean.Meta.smartUnfoldingReduce? (e : Expr) :
MetaM (Option Expr)

Recall that `_sunfold` auxiliary definitions contains the markers: `markSmartUnfoldingMatch` (*) and `markSmartUnfoldingMatchAlt` (**). For example, consider the following definition

    def r (i j : Nat) : Nat :=
      i +
        match j with
        | Nat.zero => 1
        | Nat.succ j =>
          i + match j with
              | Nat.zero => 2
              | Nat.succ j => r i j

produces the following `_sunfold` auxiliary definition with the markers

    def r._sunfold (i j : Nat) : Nat :=
      i +
        (*) match j with
        | Nat.zero => (**) 1
        | Nat.succ j =>
          i + (*) match j with
              | Nat.zero => (**) 2
              | Nat.succ j => (**) r i j

`match` expressions marked with `markSmartUnfoldingMatch` (*) must be reduced, otherwise the resulting term is not definitionally equal to the given expression. The recursion may be interrupted as soon as the annotation `markSmartUnfoldingAlt` (**) is reached.

For example, the term `r i j.succ.succ` reduces to the definitionally equal term `i + i * r i j`

Equations

- Lean.Meta.smartUnfoldingReduce? e = (Lean.Meta.smartUnfoldingReduce?.go✝ e).run

Instances For

source
partial def Lean.Meta.unfoldProjInst? (e : Expr) :
MetaM (Option Expr)

Auxiliary method for unfolding a class projection.

source
partial def Lean.Meta.unfoldProjInstWhenInstances? (e : Expr) :
MetaM (Option Expr)

Auxiliary method for unfolding a class projection when transparency is set to `TransparencyMode.instances`. Recall that class instance projections are not marked with `[reducible]` because we want them to be in "reducible canonical form".

source
partial def Lean.Meta.unfoldDefinition? (e : Expr) (ignoreTransparency : Bool := false) :
MetaM (Option Expr)

Unfold definition using "smart unfolding" if possible. If `ignoreTransparency = true`, then the definition is unfolded even if the transparency setting does not allow it.

source
def Lean.Meta.unfoldDefinition (e : Expr) :
MetaM Expr
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[specialize #[]]
partial def Lean.Meta.whnfHeadPred (e : Expr) (pred : Expr → MetaM Bool) :
MetaM Expr
source
def Lean.Meta.whnfUntil (e : Expr) (declName : Name) :
MetaM (Option Expr)
Equations

- Lean.Meta.whnfUntil e declName = do let e ← Lean.Meta.whnfHeadPred e fun (e : Lean.Expr) => pure !e.isAppOf declName if e.isAppOf declName = true then pure (some e) else pure none

Instances For

source
def Lean.Meta.whnfCoreUnfoldingAnnotations (e : Expr) :
MetaM Expr

Applies `whnfCore` while unfolding type annotations (`outParam`/`optParam`/etc.).

Equations

- Lean.Meta.whnfCoreUnfoldingAnnotations e = Lean.Meta.whnfHeadPred e fun (e : Lean.Expr) => pure e.isTypeAnnotation

Instances For

source
def Lean.Meta.reduceRecMatcher? (e : Expr) :
MetaM (Option Expr)

Try to reduce matcher/recursor/quot applications. We say they are all "morally" recursor applications.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
unsafe def Lean.Meta.reduceBoolNativeUnsafe (constName : Name) :
MetaM Bool
Equations

- Lean.Meta.reduceBoolNativeUnsafe constName = Lean.evalConstCheck Bool `Bool constName

Instances For

source
unsafe def Lean.Meta.reduceNatNativeUnsafe (constName : Name) :
MetaM Nat
Equations

- Lean.Meta.reduceNatNativeUnsafe constName = Lean.evalConstCheck Nat `Nat constName

Instances For

source
@[implemented_by Lean.Meta.reduceBoolNativeUnsafe]
opaque Lean.Meta.reduceBoolNative (constName : Name) :
MetaM Bool
source
@[implemented_by Lean.Meta.reduceNatNativeUnsafe]
opaque Lean.Meta.reduceNatNative (constName : Name) :
MetaM Nat
source
def Lean.Meta.reduceNative? (e : Expr) :
MetaM (Option Expr)
Equations

- One or more equations did not get rendered due to their size.
- Lean.Meta.reduceNative? e = pure none

Instances For

source
@[inline]
def Lean.Meta.withNatValue {α : Type} (a : Expr) (k : Nat → MetaM (Option α)) :
MetaM (Option α)
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Meta.reduceUnaryNatOp (f : Nat → Nat) (a : Expr) :
MetaM (Option Expr)
Equations

- Lean.Meta.reduceUnaryNatOp f a = Lean.Meta.withNatValue a fun (a : Nat) => pure (some (Lean.mkRawNatLit (f a)))

Instances For

source
def Lean.Meta.reduceBinNatOp (f : Nat → Nat → Nat) (a b : Expr) :
MetaM (Option Expr)
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Meta.reducePow (a b : Expr) :
MetaM (Option Expr)
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Meta.reduceBinNatPred (f : Nat → Nat → Bool) (a b : Expr) :
MetaM (Option Expr)
Equations

- Lean.Meta.reduceBinNatPred f a b = Lean.Meta.withNatValue a fun (a : Nat) => Lean.Meta.withNatValue b fun (b : Nat) => pure (some (Lean.toExpr (f a b)))

Instances For

source
def Lean.Meta.reduceNat? (e : Expr) :
MetaM (Option Expr)
Equations

- Lean.Meta.reduceNat? ((Lean.Expr.const fn us).app a) = if (fn == `Nat.succ) = true then Lean.Meta.reduceUnaryNatOp Nat.succ a else pure none
- Lean.Meta.reduceNat? (((Lean.Expr.const `Nat.add us).app a1).app a2) = Lean.Meta.reduceBinNatOp Nat.add a1 a2
- Lean.Meta.reduceNat? (((Lean.Expr.const `Nat.sub us).app a1).app a2) = Lean.Meta.reduceBinNatOp Nat.sub a1 a2
- Lean.Meta.reduceNat? (((Lean.Expr.const `Nat.mul us).app a1).app a2) = Lean.Meta.reduceBinNatOp Nat.mul a1 a2
- Lean.Meta.reduceNat? (((Lean.Expr.const `Nat.div us).app a1).app a2) = Lean.Meta.reduceBinNatOp Nat.div a1 a2
- Lean.Meta.reduceNat? (((Lean.Expr.const `Nat.mod us).app a1).app a2) = Lean.Meta.reduceBinNatOp Nat.mod a1 a2
- Lean.Meta.reduceNat? (((Lean.Expr.const `Nat.pow us).app a1).app a2) = Lean.Meta.reducePow a1 a2
- Lean.Meta.reduceNat? (((Lean.Expr.const `Nat.gcd us).app a1).app a2) = Lean.Meta.reduceBinNatOp Nat.gcd a1 a2
- Lean.Meta.reduceNat? (((Lean.Expr.const `Nat.beq us).app a1).app a2) = Lean.Meta.reduceBinNatPred Nat.beq a1 a2
- Lean.Meta.reduceNat? (((Lean.Expr.const `Nat.ble us).app a1).app a2) = Lean.Meta.reduceBinNatPred Nat.ble a1 a2
- Lean.Meta.reduceNat? (((Lean.Expr.const `Nat.land us).app a1).app a2) = Lean.Meta.reduceBinNatOp Nat.land a1 a2
- Lean.Meta.reduceNat? (((Lean.Expr.const `Nat.lor us).app a1).app a2) = Lean.Meta.reduceBinNatOp Nat.lor a1 a2
- Lean.Meta.reduceNat? (((Lean.Expr.const `Nat.xor us).app a1).app a2) = Lean.Meta.reduceBinNatOp Nat.xor a1 a2
- Lean.Meta.reduceNat? (((Lean.Expr.const `Nat.shiftLeft us).app a1).app a2) = Lean.Meta.reduceBinNatOp Nat.shiftLeft a1 a2
- Lean.Meta.reduceNat? (((Lean.Expr.const `Nat.shiftRight us).app a1).app a2) = Lean.Meta.reduceBinNatOp Nat.shiftRight a1 a2
- Lean.Meta.reduceNat? (((Lean.Expr.const fn us).app a1).app a2) = pure none
- Lean.Meta.reduceNat? e = pure none

Instances For

source
@[export lean_whnf]
partial def Lean.Meta.whnfImp (e : Expr) :
MetaM Expr
source
def Lean.Meta.reduceProjOf? (e : Expr) (p : Name → Bool) :
MetaM (Option Expr)

If `e` is a projection function that satisfies `p`, then reduce it

Equations

- One or more equations did not get rendered due to their size.

Instances For