Documentation

Lean.Meta.ExprDefEq

def Lean.Meta.isAbstractedUnassignedMVar :

Lean.Expr → Lean.MetaM Bool

Return true if e is of the form fun (x_1 ... x_n) => ?m y_1 ... y_k), and ?m is unassigned. Remark: n, k may be 0. This function is used to filter unification problems in isDefEqArgs/isDefEqEtaStruct where we can assign proofs. If one side is of the form described above, then we can likely assign ?m. But it it's not, we would most likely apply proof irrelevance, which is usually very expensive since it needs to unify the types as well.

Equations

One or more equations did not get rendered due to their size.
Lean.Meta.isAbstractedUnassignedMVar (Lean.Expr.lam binderName binderType b binderInfo) = Lean.Meta.isAbstractedUnassignedMVar b
Lean.Meta.isAbstractedUnassignedMVar (Lean.Expr.app a arg) = Lean.Meta.isAbstractedUnassignedMVar a
Lean.Meta.isAbstractedUnassignedMVar x = pure false

Instances For

def Lean.Meta.isDefEqNative (s : Lean.Expr) (t : Lean.Expr) :

Lean.MetaM Lean.LBool

Support for Lean.reduceBool and Lean.reduceNat

Equations

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

Instances For

def Lean.Meta.isDefEqNat (s : Lean.Expr) (t : Lean.Expr) :

Lean.MetaM Lean.LBool

Support for reducing Nat basic operations.

Equations

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

Instances For

def Lean.Meta.isDefEqStringLit (s : Lean.Expr) (t : Lean.Expr) :

Lean.MetaM Lean.LBool

Support for constraints of the form ("..." =?= String.mk cs)

Equations

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

Instances For

def Lean.Meta.isEtaUnassignedMVar (e : Lean.Expr) :

Lean.MetaM Bool

Return true if e is of the form fun (x_1 ... x_n) => ?m x_1 ... x_n), and ?m is unassigned. Remark: n may be 0.

Equations

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

Instances For

inductive Lean.Meta.DefEqArgsFirstPassResult :

failed: Lean.Meta.DefEqArgsFirstPassResult
Failed to establish that explicit arguments are def-eq. Remark: higher output parameters, and parameters that depend on them are postponed.
ok: Array Nat → Array Nat → Lean.Meta.DefEqArgsFirstPassResult
Succeeded. The array postponedImplicit contains the position of the implicit arguments for which def-eq has been postponed. postponedHO contains the higher order output parameters, and parameters that depend on them. They should be processed after the implict ones. postponedHO is used to handle applications involving functions that contain higher order output parameters. Example:
```
getElem :
  {cont : Type u_1} → {idx : Type u_2} → {elem : Type u_3} →
  {dom : cont → idx → Prop} → [self : GetElem cont idx elem dom] →
  (xs : cont) → (i : idx) → (h : dom xs i) → elem
```
The argumengs dom and h must be processed after all implicit arguments otherwise higher-order unification problems are generated. See issue #1299, when trying to solve
```
getElem ?a ?i ?h =?= getElem a i (Fin.val_lt_of_le i ...)
```
we have to solve the constraint
```
?dom a i.val =?= LT.lt i.val (Array.size a)
```
by solving after the instance has been synthesized, we reduce this constraint to a simple check.

Result type for isDefEqArgsFirstPass.

Instances For

@[specialize #[]]

def Lean.Meta.isDefEqBindingDomain (fvars : Array Lean.Expr) (ds₂ : Array Lean.Expr) (k : Lean.MetaM Bool) :

Lean.MetaM Bool

Check whether the types of the free variables at fvars are definitionally equal to the types at ds₂.

Pre: fvars.size == ds₂.size

This method also updates the set of local instances, and invokes the continuation k with the updated set.

We can't use withNewLocalInstances because the isDeq fvarType d₂ may use local instances.

Equations

Lean.Meta.isDefEqBindingDomain fvars ds₂ k = Lean.Meta.isDefEqBindingDomain.loop fvars ds₂ k 0

Instances For

partial def Lean.Meta.isDefEqBindingDomain.loop (fvars : Array Lean.Expr) (ds₂ : Array Lean.Expr) (k : Lean.MetaM Bool) (i : Nat) :

Lean.MetaM Bool

Each metavariable is declared in a particular local context. We use the notation C |- ?m : t to denote a metavariable ?m that was declared at the local context C with type t (see MetavarDecl). We also use ?m@C as a shorthand for C |- ?m : t where t is the type of ?m.

The following method process the unification constraint

   ?m@C a₁ ... aₙ =?= t

We say the unification constraint is a pattern IFF

1) `a₁ ... aₙ` are pairwise distinct free variables that are *not* let-variables.
2) `a₁ ... aₙ` are not in `C`
3) `t` only contains free variables in `C` and/or `{a₁, ..., aₙ}`
4) For every metavariable `?m'@C'` occurring in `t`, `C'` is a subprefix of `C`
5) `?m` does not occur in `t`
*not* let-variables.
2) `a₁ ... aₙ` are not in `C`
3) `t` only contains free variables in `C` and/or `{a₁, ..., aₙ}`
4) For every metavariable `?m'@C'` occurring in `t`, `C'` is a subprefix of `C`
5) `?m` does not occur in `t`
 let-variables.
2) `a₁ ... aₙ` are not in `C`
3) `t` only contains free variables in `C` and/or `{a₁, ..., aₙ}`
4) For every metavariable `?m'@C'` occurring in `t`, `C'` is a subprefix of `C`
5) `?m` does not occur in `t`

Claim: we don't have to check free variable declarations. That is, if t contains a reference to x : A := v, we don't need to check v. Reason: The reference to x is a free variable, and it must be in C (by 1 and 3). If x is in C, then any metavariable occurring in v must have been defined in a strict subprefix of C. So, condition 4 and 5 are satisfied.

If the conditions above have been satisfied, then the solution for the unification constrain is

?m := fun a₁ ... aₙ => t

Now, we consider some workarounds/approximations.

A1) Suppose t contains a reference to x : A := v and x is not in C (failed condition 3) (precise) solution: unfold x in t.

A2) Suppose some aᵢ is in C (failed condition 2) (approximated) solution (when config.quasiPatternApprox is set to true) : ignore condition and also use

    ?m := fun a₁ ... aₙ => t

Here is an example where this approximation fails: Given C containing a : nat, consider the following two constraints ?m@C a =?= a ?m@C b =?= a

If we use the approximation in the first constraint, we get ?m := fun x => x when we apply this solution to the second one we get a failure.

IMPORTANT: When applying this approximation we need to make sure the abstracted term fun a₁ ... aₙ => t is type correct. The check can only be skipped in the pattern case described above. Consider the following example. Given the local context

  (α : Type) (a : α)

we try to solve

 ?m α =?= @id α a

If we use the approximation above we obtain:

 ?m := (fun α' => @id α' a)

which is a type incorrect term. a has type α but it is expected to have type α'.

The problem occurs because the right hand side contains a free variable a that depends on the free variable α being abstracted. Note that this dependency cannot occur in patterns.

We can address this by type checking the term after abstraction. This is not a significant performance bottleneck because this case doesn't happen very often in practice (262 times when compiling stdlib on Jan 2018). The second example is trickier, but it also occurs less frequently (8 times when compiling stdlib on Jan 2018, and all occurrences were at Init/Control when we define monads and auxiliary combinators for them). We considered three options for the addressing the issue on the second example:

A3) a₁ ... aₙ are not pairwise distinct (failed condition 1). In Lean3, we would try to approximate this case using an approach similar to A2. However, this approximation complicates the code, and is never used in the Lean3 stdlib and mathlib.

A4) t contains a metavariable ?m'@C' where C' is not a subprefix of C. If ?m' is assigned, we substitute. If not, we create an auxiliary metavariable with a smaller scope. Actually, we let elimMVarDeps at MetavarContext.lean to perform this step.

A5) If some aᵢ is not a free variable, then we use first-order unification (if config.foApprox is set to true)

   ?m a_1 ... a_i a_{i+1} ... a_{i+k} =?= f b_1 ... b_k

reduces to

   ?M a_1 ... a_i =?= f
   a_{i+1}        =?= b_1
   ...
   a_{i+k}        =?= b_k

A6) If (m =?= v) is of the form

    ?m a_1 ... a_n =?= ?m b_1 ... b_k

 then we use first-order unification (if `config.foApprox` is set to true)

A7) When foApprox, we may use another approximation (constApprox) for solving constraints of the form ?m s₁ ... sₙ =?= t where s₁ ... sₙ are arbitrary terms. We solve them by assigning the constant function to ?m. ?m := fun _ ... _ => t

 In general, this approximation may produce bad solutions, and may prevent coercions from being tried.
 For example, consider the term `pure (x > 0)` with inferred type `?m Prop` and expected type `IO Bool`.
 In this situation, the
 elaborator generates the unification constraint
 ```
 ?m Prop =?= IO Bool
 ```
 It is not a higher-order pattern, nor first-order approximation is applicable. However, constant approximation
 produces the bogus solution `?m := fun _ => IO Bool`, and prevents the system from using the coercion from
 the decidable proposition `x > 0` to `Bool`.

 On the other hand, the constant approximation is desirable for elaborating the term
 ```
 let f (x : _) := pure "hello"; f ()
 ```
 with expected type `IO String`.
 In this example, the following unification contraint is generated.
 ```
 ?m () String =?= IO String
 ```
 It is not a higher-order pattern, first-order approximation reduces it to
 ```
 ?m () =?= IO
 ```
 which fails to be solved. However, constant approximation solves it by assigning
 ```
 ?m := fun _ => IO
 ```
 Note that `f`s type is `(x : ?α) -> ?m x String`. The metavariable `?m` may depend on `x`.
 If `constApprox` is set to true, we use constant approximation. Otherwise, we use a heuristic to decide
 whether we should apply it or not. The heuristic is based on observing where the constraints above come from.
 In the first example, the constraint `?m Prop =?= IO Bool` come from polymorphic method where `?m` is expected to
 be a **function** of type `Type -> Type`. In the second example, the first argument of `?m` is used to model
 a **potential** dependency on `x`. By using constant approximation here, we are just saying the type of `f`
 does **not** depend on `x`. We claim this is a reasonable approximation in practice. Moreover, it is expected
 by any functional programmer used to non-dependently type languages (e.g., Haskell).
 We distinguish the two cases above by using the field `numScopeArgs` at `MetavarDecl`. This fiels tracks
 how many metavariable arguments are representing dependencies.

def Lean.Meta.mkAuxMVar (lctx : Lean.LocalContext) (localInsts : Lean.LocalInstances) (type : Lean.Expr) (numScopeArgs : optParam Nat 0) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkAuxMVar lctx localInsts type numScopeArgs = Lean.Meta.mkFreshExprMVarAt lctx localInsts type Lean.MetavarKind.natural Lean.Name.anonymous numScopeArgs

Instances For

opaque Lean.Meta.CheckAssignment.checkAssignmentExceptionId :

Lean.InternalExceptionId

opaque Lean.Meta.CheckAssignment.outOfScopeExceptionId :

Lean.InternalExceptionId

structure Lean.Meta.CheckAssignment.State :

cache : Lean.ExprStructMap Lean.Expr

Instances For

structure Lean.Meta.CheckAssignment.Context :

mvarId : Lean.MVarId
mvarDecl : Lean.MetavarDecl
fvars : Array Lean.Expr
hasCtxLocals : Bool
rhs : Lean.Expr

Instances For

@[inline, reducible]

abbrev Lean.Meta.CheckAssignment.CheckAssignmentM (α : Type) :

Equations

Lean.Meta.CheckAssignment.CheckAssignmentM = ReaderT Lean.Meta.CheckAssignment.Context (StateRefT' IO.RealWorld Lean.Meta.CheckAssignment.State Lean.MetaM)

Instances For

def Lean.Meta.CheckAssignment.throwCheckAssignmentFailure {α : Type} :

Lean.Meta.CheckAssignment.CheckAssignmentM α

Equations

Lean.Meta.CheckAssignment.throwCheckAssignmentFailure = throw (Lean.Exception.internal Lean.Meta.CheckAssignment.checkAssignmentExceptionId)

Instances For

def Lean.Meta.CheckAssignment.throwOutOfScopeFVar {α : Type} :

Lean.Meta.CheckAssignment.CheckAssignmentM α

Equations

Lean.Meta.CheckAssignment.throwOutOfScopeFVar = throw (Lean.Exception.internal Lean.Meta.CheckAssignment.outOfScopeExceptionId)

Instances For

instance Lean.Meta.CheckAssignment.instMonadCacheExprCheckAssignmentM :

Lean.MonadCache Lean.Expr Lean.Expr Lean.Meta.CheckAssignment.CheckAssignmentM

Equations

Lean.Meta.CheckAssignment.instMonadCacheExprCheckAssignmentM = { findCached? := Lean.Meta.CheckAssignment.findCached?, cache := Lean.Meta.CheckAssignment.cache }

@[inline]

def Lean.Meta.CheckAssignment.run (x : Lean.Meta.CheckAssignment.CheckAssignmentM Lean.Expr) (mvarId : Lean.MVarId) (fvars : Array Lean.Expr) (hasCtxLocals : Bool) (v : Lean.Expr) :

Lean.MetaM (Option Lean.Expr)

Equations

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

Instances For

partial def Lean.Meta.CheckAssignment.checkFVar (fvar : Lean.Expr) :

Lean.Meta.CheckAssignment.CheckAssignmentM Lean.Expr

partial def Lean.Meta.CheckAssignment.checkMVar (mvar : Lean.Expr) :

Lean.Meta.CheckAssignment.CheckAssignmentM Lean.Expr

partial def Lean.Meta.CheckAssignment.assignToConstFun (mvar : Lean.Expr) (numArgs : Nat) (newMVar : Lean.Expr) :

Lean.MetaM Bool

Auxiliary function used to "fix" subterms of the form ?m x_1 ... x_n where x_is are free variables, and one of them is out-of-scope. See Expr.app case at check. If ctxApprox is true, then we solve this case by creating a fresh metavariable ?n with the correct scope, an assigning ?m := fun _ ... _ => ?n

partial def Lean.Meta.CheckAssignment.checkAssignmentAux (mvarId : Lean.MVarId) (fvars : Array Lean.Expr) (hasCtxLocals : Bool) (v : Lean.Expr) :

Lean.MetaM (Option Lean.Expr)

partial def Lean.Meta.CheckAssignment.checkApp (e : Lean.Expr) :

Lean.Meta.CheckAssignment.CheckAssignmentM Lean.Expr

partial def Lean.Meta.CheckAssignment.check (e : Lean.Expr) :

Lean.Meta.CheckAssignment.CheckAssignmentM Lean.Expr

def Lean.Meta.CheckAssignmentQuick.check (hasCtxLocals : Bool) (mctx : Lean.MetavarContext) (lctx : Lean.LocalContext) (mvarDecl : Lean.MetavarDecl) (mvarId : Lean.MVarId) (fvars : Array Lean.Expr) (e : Lean.Expr) :

Equations

Lean.Meta.CheckAssignmentQuick.check hasCtxLocals mctx lctx mvarDecl mvarId fvars e = Lean.Meta.CheckAssignmentQuick.check.visit hasCtxLocals mctx lctx mvarDecl mvarId fvars e

Instances For

partial def Lean.Meta.CheckAssignmentQuick.check.visit (hasCtxLocals : Bool) (mctx : Lean.MetavarContext) (lctx : Lean.LocalContext) (mvarDecl : Lean.MetavarDecl) (mvarId : Lean.MVarId) (fvars : Array Lean.Expr) (e : Lean.Expr) :

def Lean.Meta.checkAssignment (mvarId : Lean.MVarId) (fvars : Array Lean.Expr) (v : Lean.Expr) :

Lean.MetaM (Option Lean.Expr)

Auxiliary function for handling constraints of the form ?m a₁ ... aₙ =?= v. It will check whether we can perform the assignment

?m := fun fvars => v

The result is none if the assignment can't be performed. The result is some newV where newV is a possibly updated v. This method may need to unfold let-declarations.

Equations

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

Instances For

@[inline]

def Lean.Meta.whenUndefDo (x : Lean.MetaM Lean.LBool) (k : Lean.MetaM Bool) :

Lean.MetaM Bool

Equations

Lean.Meta.whenUndefDo x k = do let status ← x match status with | Lean.LBool.true => pure true | Lean.LBool.false => pure false | Lean.LBool.undef => k

Instances For

@[export lean_is_expr_def_eq]

partial def Lean.Meta.isExprDefEqAuxImpl (t : Lean.Expr) (s : Lean.Expr) :

Lean.MetaM Bool