max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: add DefEqM

Browse source 
The idea is to make clear that the field `posponed` is transient
state. It is only used during `isDefEq`.
The refactoring was motivated by a bug I found where the `posponed`
constraints were not being handled correctly. For example,
the `check (e : Expr)` method was returning `true`, but leaving pending
universe constraints at `postponed`.

cc @Kha
This commit is contained in:
Leonardo de Moura 2020-09-12 16:42:16 -07:00
parent 0967ad7e91
commit e181c1adee
8 changed files with 154 additions and 148 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

40
src/Lean/Meta/Basic.lean
View file

@ -90,14 +90,9 @@ structure Cache :=
(whnfDefault : PersistentExprStructMap Expr := {}) -- cache for closed terms and `TransparencyMode.default`
(whnfAll : PersistentExprStructMap Expr := {}) -- cache for closed terms and `TransparencyMode.all`
structure PostponedEntry :=
(lhs : Level)
(rhs : Level)
structure State :=
(mctx : MetavarContext := {})
(cache : Cache := {})
(postponed : PersistentArray PostponedEntry := {})
/- When `trackZeta == true`, then any let-decl free variable that is zeta expansion performed by `MetaM` is stored in `zetaFVarIds`. -/
(zetaFVarIds : NameSet := {})
@ -108,7 +103,13 @@ structure Context :=
(lctx : LocalContext := {})
(localInstances : LocalInstances := #[])
abbrev MetaM := ReaderT Context $ StateRefT State $ CoreM
abbrev MetaM := ReaderT Context $ StateRefT State $ CoreM
structure PostponedEntry :=
(lhs : Level)
(rhs : Level)
abbrev DefEqM := StateRefT (PersistentArray PostponedEntry) MetaM
instance : MonadIO MetaM :=
{ liftIO := fun α x => liftM (liftIO x : CoreM α) }
@ -143,7 +144,7 @@ pure (a, sCore, s)
instance hasEval {α} [MetaHasEval α] : MetaHasEval (MetaM α) :=
⟨fun env opts x _ => MetaHasEval.eval env opts $ x.run'⟩
protected def throwIsDefEqStuck {α} : MetaM α :=
protected def throwIsDefEqStuck {α} : DefEqM α :=
throw $ Exception.internal isDefEqStuckExceptionId
@[init] private def regTraceClasses : IO Unit := do
@ -184,10 +185,10 @@ IO.mkRef $ fun _ => throwError "inferType implementation was not set"
@[init mkInferTypeRef] def inferTypeRef : IO.Ref (Expr → MetaM Expr) := arbitrary _
def mkIsExprDefEqAuxRef : IO (IO.Ref (Expr → Expr → MetaM Bool)) :=
def mkIsExprDefEqAuxRef : IO (IO.Ref (Expr → Expr → DefEqM Bool)) :=
IO.mkRef $ fun _ _ => throwError "isDefEq implementation was not set"
@[init mkIsExprDefEqAuxRef] def isExprDefEqAuxRef : IO.Ref (Expr → Expr → MetaM Bool) := arbitrary _
@[init mkIsExprDefEqAuxRef] def isExprDefEqAuxRef : IO.Ref (Expr → Expr → DefEqM Bool) := arbitrary _
def mkSynthPendingRef : IO (IO.Ref (MVarId → MetaM Bool)) :=
IO.mkRef $ fun _ => pure false
@ -208,7 +209,7 @@ liftMetaM $ withIncRecDepth do
fn ← liftIO inferTypeRef.get;
fn e
protected def isExprDefEqAux (t s : Expr) : MetaM Bool :=
protected def isExprDefEqAux (t s : Expr) : DefEqM Bool :=
withIncRecDepth do
fn ← liftIO isExprDefEqAuxRef.get;
fn t s
@ -969,6 +970,25 @@ pure $ Lean.ppExpr env mctx lctx opts e
def ppExpr (e : Expr) : m Format :=
liftMetaM $ ppExprImp e
@[inline] protected def orelse {α} (x y : MetaM α) : MetaM α := do
env ← getEnv;
mctx ← getMCtx;
catch x (fun _ => do setEnv env; setMCtx mctx; y)
instance Meta.hasOrelse {α} : HasOrelse (MetaM α) := ⟨Meta.orelse⟩
/-- `commitWhenSome? x` executes `x` and keep modifications when it returns `some a`. -/
@[specialize] def commitWhenSome? {α} (x? : MetaM (Option α)) : MetaM (Option α) := do
env ← getEnv;
mctx ← getMCtx;
catch
(do
a? ← x?;
match a? with
| some a => pure a?
| none => do setEnv env; setMCtx mctx; pure none)
(fun ex => do setEnv env; setMCtx mctx; throw ex)
end Methods
end Meta

7
src/Lean/Meta/Check.lean
View file

@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Meta.InferType
import Lean.Meta.LevelDefEq
/-
This is not the Kernel type checker, but an auxiliary method for checking
@ -41,7 +42,7 @@ lambdaLetTelescope e $ fun xs b => do
ensureType t;
check t;
vType ← inferType v;
unlessM (Meta.isExprDefEqAux t vType) $ throwLetTypeMismatchMessage x.fvarId!;
unlessM (isDefEq t vType) $ throwLetTypeMismatchMessage x.fvarId!;
check v
};
check b
@ -90,7 +91,7 @@ fType ← whnf fType;
match fType with
| Expr.forallE _ d _ _ => do
aType ← inferType a;
unlessM (Meta.isExprDefEqAux d aType) $ throwAppTypeMismatch f a
unlessM (isDefEq d aType) $ throwAppTypeMismatch f a
| _ => throwFunctionExpected (mkApp f a)
private partial def checkAux : Expr → MetaM Unit
@ -109,7 +110,7 @@ traceCtx `Meta.check $
def isTypeCorrect (e : Expr) : MetaM Bool :=
catch
(traceCtx `Meta.check $ do checkAux e; pure true)
(do check e; pure true)
(fun ex => do
trace! `Meta.typeError ex.toMessageData;
pure false)

136
src/Lean/Meta/ExprDefEq.lean
View file

@ -23,7 +23,7 @@ namespace Meta
(fun x : A => f ?m) =?= f
```
The left-hand side of the constraint above it not eta-reduced because `?m` is a metavariable. -/
private def isDefEqEta (a b : Expr) : MetaM Bool :=
private def isDefEqEta (a b : Expr) : DefEqM Bool :=
if a.isLambda && !b.isLambda then do
bType ← inferType b;
bType ← whnfD bType;
@ -36,10 +36,10 @@ else
pure false
/-- Support for `Lean.reduceBool` and `Lean.reduceNat` -/
def isDefEqNative (s t : Expr) : MetaM LBool := do
let isDefEq (s t) : MetaM LBool := toLBoolM $ Meta.isExprDefEqAux s t;
s? ← reduceNative? s;
t? ← reduceNative? t;
def isDefEqNative (s t : Expr) : DefEqM LBool := do
let isDefEq (s t) : DefEqM LBool := toLBoolM $ Meta.isExprDefEqAux s t;
s? ← liftM $ reduceNative? s;
t? ← liftM $ reduceNative? t;
match s?, t? with
| some s, some t => isDefEq s t
| some s, none => isDefEq s t
@ -47,13 +47,13 @@ match s?, t? with
| none, none => pure LBool.undef
/-- Support for reducing Nat basic operations. -/
def isDefEqNat (s t : Expr) : MetaM LBool := do
let isDefEq (s t) : MetaM LBool := toLBoolM $ Meta.isExprDefEqAux s t;
def isDefEqNat (s t : Expr) : DefEqM LBool := do
let isDefEq (s t) : DefEqM LBool := toLBoolM $ Meta.isExprDefEqAux s t;
if s.hasFVar || s.hasMVar || t.hasFVar || t.hasMVar then
pure LBool.undef
else do
s? ← reduceNat? s;
t? ← reduceNat? t;
s? ← liftM $ reduceNat? s;
t? ← liftM $ reduceNat? t;
match s?, t? with
| some s, some t => isDefEq s t
| some s, none => isDefEq s t
@ -61,8 +61,8 @@ else do
| none, none => pure LBool.undef
/-- Support for constraints of the form `("..." =?= String.mk cs)` -/
def isDefEqStringLit (s t : Expr) : MetaM LBool := do
let isDefEq (s t) : MetaM LBool := toLBoolM $ Meta.isExprDefEqAux s t;
def isDefEqStringLit (s t : Expr) : DefEqM LBool := do
let isDefEq (s t) : DefEqM LBool := toLBoolM $ Meta.isExprDefEqAux s t;
if s.isStringLit && t.isAppOf `String.mk then
isDefEq (toCtorIfLit s) t
else if s.isAppOf `String.mk && t.isStringLit then
@ -73,7 +73,7 @@ else
/--
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. -/
def isEtaUnassignedMVar (e : Expr) : MetaM Bool :=
def isEtaUnassignedMVar (e : Expr) : DefEqM Bool :=
match e.etaExpanded? with
| some (Expr.mvar mvarId _) =>
condM (isReadOnlyOrSyntheticOpaqueExprMVar mvarId)
@ -114,7 +114,7 @@ match e.etaExpanded? with
Pre: `paramInfo.size <= args₁.size = args₂.size`
-/
private partial def isDefEqArgsFirstPass
(paramInfo : Array ParamInfo) (args₁ args₂ : Array Expr) : Nat → Array Nat → MetaM (Option (Array Nat))
(paramInfo : Array ParamInfo) (args₁ args₂ : Array Expr) : Nat → Array Nat → DefEqM (Option (Array Nat))
| i, postponed =>
if h : i < paramInfo.size then
let info := paramInfo.get ⟨i, h⟩;
@ -133,7 +133,7 @@ private partial def isDefEqArgsFirstPass
else
pure (some postponed)
private partial def isDefEqArgsAux (args₁ args₂ : Array Expr) (h : args₁.size = args₂.size) : Nat → MetaM Bool
private partial def isDefEqArgsAux (args₁ args₂ : Array Expr) (h : args₁.size = args₂.size) : Nat → DefEqM Bool
| i =>
if h₁ : i < args₁.size then
let a₁ := args₁.get ⟨i, h₁⟩;
@ -144,15 +144,15 @@ private partial def isDefEqArgsAux (args₁ args₂ : Array Expr) (h : args₁.s
else
pure true
@[specialize] private def trySynthPending (e : Expr) : MetaM Bool := do
@[specialize] private def trySynthPending (e : Expr) : DefEqM Bool := do
mvarId? ← getStuckMVar? e;
match mvarId? with
| some mvarId => Meta.synthPending mvarId
| some mvarId => liftM $ Meta.synthPending mvarId
| none => pure false
private def isDefEqArgs (f : Expr) (args₁ args₂ : Array Expr) : MetaM Bool :=
private def isDefEqArgs (f : Expr) (args₁ args₂ : Array Expr) : DefEqM Bool :=
if h : args₁.size = args₂.size then do
finfo ← getFunInfoNArgs f args₁.size;
finfo ← liftM $ getFunInfoNArgs f args₁.size;
(some postponed) ← isDefEqArgsFirstPass finfo.paramInfo args₁ args₂ 0 #[] | pure false;
(isDefEqArgsAux args₁ args₂ h finfo.paramInfo.size)
<&&>
@ -183,7 +183,7 @@ else
We can't use `withNewLocalInstances` because the `isDeq fvarType d₂`
may use local instances. -/
@[specialize] partial def isDefEqBindingDomain (fvars : Array Expr) (ds₂ : Array Expr) : Nat → MetaM Bool → MetaM Bool
@[specialize] partial def isDefEqBindingDomain (fvars : Array Expr) (ds₂ : Array Expr) : Nat → DefEqM Bool → DefEqM Bool
| i, k =>
if h : i < fvars.size then do
let fvar := fvars.get ⟨i, h⟩;
@ -203,9 +203,9 @@ else
It accumulates the new free variables in `fvars`, and declare them at `lctx`.
We use the domain types of `e₁` to create the new free variables.
We store the domain types of `e₂` at `ds₂`. -/
private partial def isDefEqBindingAux : LocalContext → Array Expr → Expr → Expr → Array Expr → MetaM Bool
private partial def isDefEqBindingAux : LocalContext → Array Expr → Expr → Expr → Array Expr → DefEqM Bool
| lctx, fvars, e₁, e₂, ds₂ =>
let process (n : Name) (d₁ d₂ b₁ b₂ : Expr) : MetaM Bool := do {
let process (n : Name) (d₁ d₂ b₁ b₂ : Expr) : DefEqM Bool := do {
let d₁ := d₁.instantiateRev fvars;
let d₂ := d₂.instantiateRev fvars;
fvarId ← mkFreshId;
@ -221,11 +221,11 @@ private partial def isDefEqBindingAux : LocalContext → Array Expr → Expr →
isDefEqBindingDomain fvars ds₂ 0 $
Meta.isExprDefEqAux (e₁.instantiateRev fvars) (e₂.instantiateRev fvars)
@[inline] private def isDefEqBinding (a b : Expr) : MetaM Bool := do
@[inline] private def isDefEqBinding (a b : Expr) : DefEqM Bool := do
lctx ← getLCtx;
isDefEqBindingAux lctx #[] a b #[]
private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool :=
private def checkTypesAndAssign (mvar : Expr) (v : Expr) : DefEqM Bool :=
traceCtx `Meta.isDefEq.assign.checkTypes $ do
-- must check whether types are definitionally equal or not, before assigning and returning true
mvarType ← inferType mvar;
@ -368,7 +368,7 @@ structure Context :=
(hasCtxLocals : Bool)
(rhs : Expr)
abbrev CheckAssignmentM := ReaderT Context $ StateRefT State $ MetaM
abbrev CheckAssignmentM := ReaderT Context $ StateRefT State $ DefEqM
def throwCheckAssignmentFailure {α} : CheckAssignmentM α :=
throw $ Exception.internal checkAssignmentExceptionId
@ -450,7 +450,7 @@ else match mctx.getExprAssignment? mvarId with
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` -/
def assignToConstFun (mvar : Expr) (numArgs : Nat) (newMVar : Expr) : MetaM Bool := do
def assignToConstFun (mvar : Expr) (numArgs : Nat) (newMVar : Expr) : DefEqM Bool := do
mvarType ← inferType mvar;
forallBoundedTelescope mvarType numArgs $ fun xs _ =>
if xs.size != numArgs then pure false
@ -495,7 +495,7 @@ partial def check : Expr → CheckAssignmentM Expr
args ← args.mapM (visit check);
pure $ mkAppN f args
@[inline] def run (x : CheckAssignmentM Expr) (mvarId : MVarId) (fvars : Array Expr) (hasCtxLocals : Bool) (v : Expr) : MetaM (Option Expr) := do
@[inline] def run (x : CheckAssignmentM Expr) (mvarId : MVarId) (fvars : Array Expr) (hasCtxLocals : Bool) (v : Expr) : DefEqM (Option Expr) := do
mvarDecl ← getMVarDecl mvarId;
let ctx := { mvarId := mvarId, mvarDecl := mvarDecl, fvars := fvars, hasCtxLocals := hasCtxLocals, rhs := v : Context };
let x : CheckAssignmentM (Option Expr) :=
@ -549,7 +549,7 @@ partial def check
end CheckAssignmentQuick
-- See checkAssignment
def checkAssignmentAux (mvarId : MVarId) (fvars : Array Expr) (hasCtxLocals : Bool) (v : Expr) : MetaM (Option Expr) := do
def checkAssignmentAux (mvarId : MVarId) (fvars : Array Expr) (hasCtxLocals : Bool) (v : Expr) : DefEqM (Option Expr) := do
CheckAssignment.run (CheckAssignment.check v) mvarId fvars hasCtxLocals v
/--
@ -561,7 +561,7 @@ CheckAssignment.run (CheckAssignment.check v) mvarId fvars hasCtxLocals 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. -/
def checkAssignment (mvarId : MVarId) (fvars : Array Expr) (v : Expr) : MetaM (Option Expr) := do
def checkAssignment (mvarId : MVarId) (fvars : Array Expr) (v : Expr) : DefEqM (Option Expr) := do
if !v.hasExprMVar && !v.hasFVar then
pure (some v)
else do
@ -575,7 +575,7 @@ else do
v ← instantiateMVars v;
checkAssignmentAux mvarId fvars hasCtxLocals v
private def processAssignmentFOApproxAux (mvar : Expr) (args : Array Expr) (v : Expr) : MetaM Bool :=
private def processAssignmentFOApproxAux (mvar : Expr) (args : Array Expr) (v : Expr) : DefEqM Bool :=
match v with
| Expr.app f a _ => Meta.isExprDefEqAux args.back a <&&> Meta.isExprDefEqAux (mkAppRange mvar 0 (args.size - 1) args) f
| _ => pure false
@ -596,7 +596,7 @@ match v with
def ITactic := Tactic Unit
-/
private partial def processAssignmentFOApprox (mvar : Expr) (args : Array Expr) : Expr → MetaM Bool
private partial def processAssignmentFOApprox (mvar : Expr) (args : Array Expr) : Expr → DefEqM Bool
| v => do
cfg ← getConfig;
if !cfg.foApprox then pure false
@ -609,7 +609,7 @@ private partial def processAssignmentFOApprox (mvar : Expr) (args : Array Expr)
| none => pure false
| some v => processAssignmentFOApprox v)
private partial def simpAssignmentArgAux : Expr → MetaM Expr
private partial def simpAssignmentArgAux : Expr → DefEqM Expr
| Expr.mdata _ e _ => simpAssignmentArgAux e
| e@(Expr.fvar fvarId _) => do
decl ← getLocalDecl fvarId;
@ -621,11 +621,11 @@ private partial def simpAssignmentArgAux : Expr → MetaM Expr
/- Auxiliary procedure for processing `?m a₁ ... aₙ =?= v`.
We apply it to each `aᵢ`. It instantiates assigned metavariables if `aᵢ` is of the form `f[?n] b₁ ... bₘ`,
and then removes metadata, and zeta-expand let-decls. -/
private def simpAssignmentArg (arg : Expr) : MetaM Expr := do
private def simpAssignmentArg (arg : Expr) : DefEqM Expr := do
arg ← if arg.getAppFn.hasExprMVar then instantiateMVars arg else pure arg;
simpAssignmentArgAux arg
private def processConstApprox (mvar : Expr) (numArgs : Nat) (v : Expr) : MetaM Bool := do
private def processConstApprox (mvar : Expr) (numArgs : Nat) (v : Expr) : DefEqM Bool := do
cfg ← getConfig;
if cfg.constApprox then do
let mvarId := mvar.mvarId!;
@ -642,10 +642,10 @@ if cfg.constApprox then do
else
pure false
private partial def processAssignmentAux (mvar : Expr) (mvarDecl : MetavarDecl) : Nat → Array Expr → Expr → MetaM Bool
private partial def processAssignmentAux (mvar : Expr) (mvarDecl : MetavarDecl) : Nat → Array Expr → Expr → DefEqM Bool
| i, args, v => do
cfg ← getConfig;
let useFOApprox (args : Array Expr) : MetaM Bool :=
let useFOApprox (args : Array Expr) : DefEqM Bool :=
processAssignmentFOApprox mvar args v <||> processConstApprox mvar args.size v;
if h : i < args.size then do
let arg := args.get ⟨i, h⟩;
@ -677,7 +677,7 @@ private partial def processAssignmentAux (mvar : Expr) (mvarDecl : MetavarDecl)
if args.any (fun arg => mvarDecl.lctx.containsFVar arg) then
/- We need to type check `v` because abstraction using `mkLambdaFVars` may have produced
a type incorrect term. See discussion at A2 -/
condM (isTypeCorrect v)
condM (liftM $ isTypeCorrect v)
(checkTypesAndAssign mvar v)
(do trace `Meta.isDefEq.assign.typeError $ fun _ => mvar ++ " := " ++ v;
useFOApprox args)
@ -686,41 +686,41 @@ private partial def processAssignmentAux (mvar : Expr) (mvarDecl : MetavarDecl)
/-- Tries to solve `?m a₁ ... aₙ =?= v` by assigning `?m`.
It assumes `?m` is unassigned. -/
private def processAssignment (mvarApp : Expr) (v : Expr) : MetaM Bool :=
private def processAssignment (mvarApp : Expr) (v : Expr) : DefEqM Bool :=
traceCtx `Meta.isDefEq.assign $ do
trace! `Meta.isDefEq.assign (mvarApp ++ " := " ++ v);
let mvar := mvarApp.getAppFn;
mvarDecl ← getMVarDecl mvar.mvarId!;
processAssignmentAux mvar mvarDecl 0 mvarApp.getAppArgs v
private def isDeltaCandidate? (t : Expr) : MetaM (Option ConstantInfo) :=
private def isDeltaCandidate? (t : Expr) : DefEqM (Option ConstantInfo) :=
match t.getAppFn with
| Expr.const c _ _ => getConst? c
| Expr.const c _ _ => liftM $ getConst? c
| _ => pure none
/-- Auxiliary method for isDefEqDelta -/
private def isListLevelDefEq (us vs : List Level) : MetaM LBool :=
private def isListLevelDefEq (us vs : List Level) : DefEqM LBool :=
toLBoolM $ isListLevelDefEqAux us vs
/-- Auxiliary method for isDefEqDelta -/
private def isDefEqLeft (fn : Name) (t s : Expr) : MetaM LBool := do
private def isDefEqLeft (fn : Name) (t s : Expr) : DefEqM LBool := do
trace! `Meta.isDefEq.delta.unfoldLeft fn;
toLBoolM $ Meta.isExprDefEqAux t s
/-- Auxiliary method for isDefEqDelta -/
private def isDefEqRight (fn : Name) (t s : Expr) : MetaM LBool := do
private def isDefEqRight (fn : Name) (t s : Expr) : DefEqM LBool := do
trace! `Meta.isDefEq.delta.unfoldRight fn;
toLBoolM $ Meta.isExprDefEqAux t s
/-- Auxiliary method for isDefEqDelta -/
private def isDefEqLeftRight (fn : Name) (t s : Expr) : MetaM LBool := do
private def isDefEqLeftRight (fn : Name) (t s : Expr) : DefEqM LBool := do
trace! `Meta.isDefEq.delta.unfoldLeftRight fn;
toLBoolM $ Meta.isExprDefEqAux t s
/-- Try to solve `f a₁ ... aₙ =?= f b₁ ... bₙ` by solving `a₁ =?= b₁, ..., aₙ =?= bₙ`.
Auxiliary method for isDefEqDelta -/
private def tryHeuristic (t s : Expr) : MetaM Bool :=
private def tryHeuristic (t s : Expr) : DefEqM Bool :=
let tFn := t.getAppFn;
let sFn := s.getAppFn;
traceCtx `Meta.isDefEq.delta $
@ -732,14 +732,14 @@ traceCtx `Meta.isDefEq.delta $
pure b
/-- Auxiliary method for isDefEqDelta -/
private abbrev unfold {α} (e : Expr) (failK : MetaM α) (successK : Expr → MetaM α) : MetaM α := do
private abbrev unfold {α} (e : Expr) (failK : DefEqM α) (successK : Expr → DefEqM α) : DefEqM α := do
e? ← unfoldDefinition? e;
match e? with
| some e => successK e
| none => failK
/-- Auxiliary method for isDefEqDelta -/
private def unfoldBothDefEq (fn : Name) (t s : Expr) : MetaM LBool :=
private def unfoldBothDefEq (fn : Name) (t s : Expr) : DefEqM LBool :=
match t, s with
| Expr.const _ ls₁ _, Expr.const _ ls₂ _ => isListLevelDefEq ls₁ ls₂
| Expr.app _ _ _, Expr.app _ _ _ =>
@ -761,7 +761,7 @@ match t.getAppFn, s.getAppFn with
- Otherwise unfold t and s if possible.
Auxiliary method for isDefEqDelta -/
private def unfoldComparingHeadsDefEq (tInfo sInfo : ConstantInfo) (t s : Expr) : MetaM LBool :=
private def unfoldComparingHeadsDefEq (tInfo sInfo : ConstantInfo) (t s : Expr) : DefEqM LBool :=
unfold t
(unfold s
(pure LBool.undef) -- `t` and `s` failed to be unfolded
@ -783,7 +783,7 @@ unfold t
Otherwise, use `unfoldComparingHeadsDefEq`.
Auxiliary method for isDefEqDelta -/
private def unfoldDefEq (tInfo sInfo : ConstantInfo) (t s : Expr) : MetaM LBool :=
private def unfoldDefEq (tInfo sInfo : ConstantInfo) (t s : Expr) : DefEqM LBool :=
if !t.hasExprMVar && !s.hasExprMVar then
/- If `t` and `s` do not contain metavariables,
we simulate strategy used in the kernel. -/
@ -804,11 +804,11 @@ else
Otherwise, use `unfoldDefEq`
Auxiliary method for isDefEqDelta -/
private def unfoldReducibeDefEq (tInfo sInfo : ConstantInfo) (t s : Expr) : MetaM LBool :=
private def unfoldReducibeDefEq (tInfo sInfo : ConstantInfo) (t s : Expr) : DefEqM LBool :=
condM shouldReduceReducibleOnly
(unfoldDefEq tInfo sInfo t s)
(do tReducible ← Meta.isReducible tInfo.name;
sReducible ← Meta.isReducible sInfo.name;
(do tReducible ← liftM $ Meta.isReducible tInfo.name;
sReducible ← liftM $ Meta.isReducible sInfo.name;
if tReducible && !sReducible then
unfold t (unfoldDefEq tInfo sInfo t s) $ fun t => isDefEqLeft tInfo.name t s
else if !tReducible && sReducible then
@ -823,7 +823,7 @@ condM shouldReduceReducibleOnly
Otherwise, use `unfoldReducibeDefEq`
Auxiliary method for isDefEqDelta -/
private def unfoldNonProjFnDefEq (tInfo sInfo : ConstantInfo) (t s : Expr) : MetaM LBool := do
private def unfoldNonProjFnDefEq (tInfo sInfo : ConstantInfo) (t s : Expr) : DefEqM LBool := do
env ← getEnv;
let tProj? := env.isProjectionFn tInfo.name;
let sProj? := env.isProjectionFn sInfo.name;
@ -855,7 +855,7 @@ else
10- If `headSymbol (unfold s) == headSymbol t`, then unfold s
11- Otherwise, unfold `t` and `s` and continue.
Remark: 9&10&11 are implemented by `unfoldComparingHeadsDefEq` -/
private def isDefEqDelta (t s : Expr) : MetaM LBool := do
private def isDefEqDelta (t s : Expr) : DefEqM LBool := do
tInfo? ← isDeltaCandidate? t.getAppFn;
sInfo? ← isDeltaCandidate? s.getAppFn;
match tInfo?, sInfo? with
@ -868,11 +868,11 @@ match tInfo?, sInfo? with
else
unfoldNonProjFnDefEq tInfo sInfo t s
private def isAssigned : Expr → MetaM Bool
private def isAssigned : Expr → DefEqM Bool
| Expr.mvar mvarId _ => isExprMVarAssigned mvarId
| _ => pure false
private def isDelayedAssignedHead (tFn : Expr) (t : Expr) : MetaM Bool :=
private def isDelayedAssignedHead (tFn : Expr) (t : Expr) : DefEqM Bool :=
match tFn with
| Expr.mvar mvarId _ => do
condM (isDelayedAssigned mvarId)
@ -881,7 +881,7 @@ match tFn with
(pure false)
| _ => pure false
private def isSynthetic : Expr → MetaM Bool
private def isSynthetic : Expr → DefEqM Bool
| Expr.mvar mvarId _ => do
mvarDecl ← getMVarDecl mvarId;
match mvarDecl.kind with
@ -890,7 +890,7 @@ private def isSynthetic : Expr → MetaM Bool
| MetavarKind.natural => pure false
| _ => pure false
private def isAssignable : Expr → MetaM Bool
private def isAssignable : Expr → DefEqM Bool
| Expr.mvar mvarId _ => do b ← isReadOnlyOrSyntheticOpaqueExprMVar mvarId; pure (!b)
| _ => pure false
@ -899,12 +899,12 @@ match t.etaExpanded? with
| some t => t == s
| none => false
private def isLetFVar (fvarId : FVarId) : MetaM Bool := do
private def isLetFVar (fvarId : FVarId) : DefEqM Bool := do
decl ← getLocalDecl fvarId;
pure decl.isLet
private def isDefEqProofIrrel (t s : Expr) : MetaM LBool := do
status ← isProofQuick t;
private def isDefEqProofIrrel (t s : Expr) : DefEqM LBool := do
status ← liftM $ isProofQuick t;
match status with
| LBool.false =>
pure LBool.undef
@ -918,7 +918,7 @@ match status with
(do sType ← inferType s; toLBoolM $ Meta.isExprDefEqAux tType sType)
(pure LBool.undef)
private partial def isDefEqQuick : Expr → Expr → MetaM LBool
private partial def isDefEqQuick : Expr → Expr → DefEqM LBool
| Expr.lit l₁ _, Expr.lit l₂ _ => pure (l₁ == l₂).toLBool
| Expr.sort u _, Expr.sort v _ => toLBoolM $ isLevelDefEqAux u v
| t@(Expr.lam _ _ _ _), s@(Expr.lam _ _ _ _) => if t == s then pure LBool.true else toLBoolM $ isDefEqBinding t s
@ -945,7 +945,7 @@ private partial def isDefEqQuick : Expr → Expr → MetaM LBool
sAssign? ← isAssignable sFn;
trace! `Meta.isDefEq
(t ++ (if tAssign? then " [assignable]" else " [nonassignable]") ++ " =?= " ++ s ++ (if sAssign? then " [assignable]" else " [nonassignable]"));
let assign (t s : Expr) : MetaM LBool := toLBoolM $ processAssignment t s;
let assign (t s : Expr) : DefEqM LBool := toLBoolM $ processAssignment t s;
cond (tAssign? && !sAssign?) (assign t s) $
cond (!tAssign? && sAssign?) (assign s t) $
cond (!tAssign? && !sAssign?)
@ -968,7 +968,7 @@ private partial def isDefEqQuick : Expr → Expr → MetaM LBool
condM (commitWhen (processAssignment t s)) (pure LBool.true) $
assign s t
@[inline] def whenUndefDo (x : MetaM LBool) (k : MetaM Bool) : MetaM Bool := do
@[inline] def whenUndefDo (x : DefEqM LBool) (k : DefEqM Bool) : DefEqM Bool := do
status ← x;
match status with
| LBool.true => pure true
@ -977,7 +977,7 @@ match status with
@[specialize] private partial def isDefEqWHNF
(t s : Expr)
(k : Expr → Expr → MetaM Bool) : MetaM Bool := do
(k : Expr → Expr → DefEqM Bool) : DefEqM Bool := do
t' ← whnfCore t;
s' ← whnfCore s;
if t == t' && s == s' then
@ -988,16 +988,16 @@ else
@[specialize] private def unstuckMVar
(e : Expr)
(successK : Expr → MetaM Bool) (failK : MetaM Bool): MetaM Bool := do
(successK : Expr → DefEqM Bool) (failK : DefEqM Bool): DefEqM Bool := do
mvarId? ← getStuckMVar? e;
match mvarId? with
| some mvarId =>
condM (Meta.synthPending mvarId)
condM (liftM $ Meta.synthPending mvarId)
(do e ← instantiateMVars e; successK e)
failK
| none => failK
private def isDefEqOnFailure (t s : Expr) : MetaM Bool :=
private def isDefEqOnFailure (t s : Expr) : DefEqM Bool :=
unstuckMVar t (fun t => Meta.isExprDefEqAux t s) $
unstuckMVar s (fun s => Meta.isExprDefEqAux t s) $
pure false
@ -1007,7 +1007,7 @@ private def consumeLet : Expr → Expr
| e@(Expr.letE _ _ _ b _) => if b.hasLooseBVars then e else consumeLet b
| e => e
partial def isExprDefEqAuxImpl : Expr → Expr → MetaM Bool
partial def isExprDefEqAuxImpl : Expr → Expr → DefEqM Bool
| t, s => do
let t := consumeLet t;
let s := consumeLet s;

82
src/Lean/Meta/LevelDefEq.lean
View file

@ -90,10 +90,10 @@ private def solveSelfMax (mvarId : MVarId) (v : Level) : MetaM Unit := do
n ← mkFreshLevelMVar;
assignLevelMVar mvarId $ mkMaxArgsDiff mvarId v n
private def postponeIsLevelDefEq (lhs : Level) (rhs : Level) : MetaM Unit :=
modify $ fun s => { s with postponed := s.postponed.push { lhs := lhs, rhs := rhs } }
private def postponeIsLevelDefEq (lhs : Level) (rhs : Level) : DefEqM Unit :=
modify fun postponed => postponed.push { lhs := lhs, rhs := rhs }
@[specialize] private def solve (isLevelDefEqAux : Level → Level → MetaM Bool) (u v : Level) : MetaM LBool := do
@[specialize] private def solve (isLevelDefEqAux : Level → Level → DefEqM Bool) (u v : Level) : DefEqM LBool := do
match u, v with
| Level.mvar mvarId _, _ =>
condM (isReadOnlyLevelMVar mvarId)
@ -101,7 +101,7 @@ match u, v with
(if !u.occurs v then do
assignLevelMVar u.mvarId! v; pure LBool.true
else if !strictOccursMax u v then do
solveSelfMax u.mvarId! v; pure LBool.true
liftM $ solveSelfMax u.mvarId! v; pure LBool.true
else
pure LBool.undef)
| Level.zero _, Level.max v₁ v₂ _ =>
@ -115,7 +115,7 @@ match u, v with
| none => pure LBool.undef
| _, _ => pure LBool.undef
partial def isLevelDefEqAux : Level → Level → MetaM Bool
partial def isLevelDefEqAux : Level → Level → DefEqM Bool
| Level.succ lhs _, Level.succ rhs _ => isLevelDefEqAux lhs rhs
| lhs, rhs =>
if lhs == rhs then
@ -144,23 +144,22 @@ partial def isLevelDefEqAux : Level → Level → MetaM Bool
else do
postponeIsLevelDefEq lhs rhs; pure true
def isListLevelDefEqAux : List Level → List Level → MetaM Bool
def isListLevelDefEqAux : List Level → List Level → DefEqM Bool
| [], [] => pure true
| u::us, v::vs => isLevelDefEqAux u v <&&> isListLevelDefEqAux us vs
| _, _ => pure false
private def getNumPostponed : MetaM Nat := do
s ← get; pure s.postponed.size
private def getNumPostponed : DefEqM Nat := do
s ← get; pure s.size
open Std (PersistentArray)
private def getResetPostponed : MetaM (PersistentArray PostponedEntry) := do
s ← get;
let ps := s.postponed;
modify $ fun s => { s with postponed := {} };
private def getResetPostponed : DefEqM (PersistentArray PostponedEntry) := do
ps ← get;
modify fun _ => {};
pure ps
private def processPostponedStep : MetaM Bool :=
private def processPostponedStep : DefEqM Bool :=
traceCtx `Meta.isLevelDefEq.postponed.step $ do
ps ← getResetPostponed;
ps.foldlM
@ -171,7 +170,7 @@ traceCtx `Meta.isLevelDefEq.postponed.step $ do
pure false)
true
private partial def processPostponedAux : Unit → MetaM Bool
private partial def processPostponedAux : Unit → DefEqM Bool
| _ => do
numPostponed ← getNumPostponed;
if numPostponed == 0 then
@ -191,59 +190,47 @@ private partial def processPostponedAux : Unit → MetaM Bool
trace! `Meta.isLevelDefEq.postponed (format "no progress solving pending is-def-eq level constraints");
pure false
private def processPostponed : MetaM Bool := do
private def processPostponed : DefEqM Bool := do
numPostponed ← getNumPostponed;
if numPostponed == 0 then pure true
else traceCtx `Meta.isLevelDefEq.postponed $ processPostponedAux ()
def restore (env : Environment) (mctx : MetavarContext) (postponed : PersistentArray PostponedEntry) : MetaM Unit := do
private def restore (env : Environment) (mctx : MetavarContext) (postponed : PersistentArray PostponedEntry) : DefEqM Unit := do
setEnv env;
modify $ fun s => { s with mctx := mctx, postponed := postponed }
setMCtx mctx;
set postponed
/--
`commitWhenSome? x` executes `x` and process all postponed universe level constraints produced by `x`.
We keep the modifications only if `processPostponed` return true and `x` returned `some a`.
`commitWhen x` executes `x` and process all postponed universe level constraints produced by `x`.
We keep the modifications only if `processPostponed` return true and `x` returned `true`.
Remark: postponed universe level constraints must be solved before returning. Otherwise,
we don't know whether `x` really succeeded. -/
@[specialize] def commitWhenSome? {α} (x? : MetaM (Option α)) : MetaM (Option α) := do
env ← getEnv;
s ← get;
let mctx := s.mctx;
let postponed := s.postponed;
modify $ fun s => { s with postponed := {} };
@[specialize] def commitWhen (x : DefEqM Bool) : DefEqM Bool := do
env ← getEnv;
mctx ← getMCtx;
postponed ← getResetPostponed;
catch
(do
a? ← x?;
match a? with
| some a =>
condM x
(condM processPostponed
(pure (some a))
(do restore env mctx postponed; pure none))
| none => do
restore env mctx postponed; pure none)
(pure true)
(do restore env mctx postponed; pure false))
(do restore env mctx postponed; pure false))
(fun ex => do restore env mctx postponed; throw ex)
@[specialize] def commitWhen (x : MetaM Bool) : MetaM Bool := do
r? ← commitWhenSome? (condM x (pure $ some ()) (pure none));
match r? with
| some _ => pure true
| none => pure false
@[init] private def regTraceClasses : IO Unit := do
registerTraceClass `Meta.isLevelDefEq;
registerTraceClass `Meta.isLevelDefEq.step;
registerTraceClass `Meta.isLevelDefEq.postponed
private def runDefEqM (x : DefEqM Bool) : MetaM Bool :=
(commitWhen x).run' {}
def isLevelDefEq (u v : Level) : m Bool := liftMetaM do
traceCtx `Meta.isLevelDefEq $ do
b ← Meta.commitWhen $ Meta.isLevelDefEqAux u v;
traceCtx `Meta.isLevelDefEq do
b ← runDefEqM $ Meta.isLevelDefEqAux u v;
trace! `Meta.isLevelDefEq (u ++ " =?= " ++ v ++ " ... " ++ if b then "success" else "failure");
pure b
def isExprDefEq (t s : Expr) : m Bool := liftMetaM do
traceCtx `Meta.isDefEq $ do
b ← Meta.commitWhen $ Meta.isExprDefEqAux t s;
b ← runDefEqM $ Meta.isExprDefEqAux t s;
trace! `Meta.isDefEq (t ++ " =?= " ++ s ++ " ... " ++ if b then "success" else "failure");
pure b
@ -253,5 +240,10 @@ isExprDefEq t s
def isDefEqNoConstantApprox (t s : Expr) : m Bool := liftMetaM do
approxDefEq $ isDefEq t s
@[init] private def regTraceClasses : IO Unit := do
registerTraceClass `Meta.isLevelDefEq;
registerTraceClass `Meta.isLevelDefEq.step;
registerTraceClass `Meta.isLevelDefEq.postponed
end Meta
end Lean

4
src/Lean/Meta/Offset.lean
View file

@ -98,8 +98,8 @@ if offset == 0 then e
else if isNatZero e then mkNatLit offset
else mkAppB (mkConst `Nat.add) e (mkNatLit offset)
def isDefEqOffset (s t : Expr) : MetaM LBool :=
let isDefEq (s t) : MetaM LBool := toLBoolM $ Meta.isExprDefEqAux s t;
def isDefEqOffset (s t : Expr) : DefEqM LBool :=
let isDefEq (s t) : DefEqM LBool := toLBoolM $ Meta.isExprDefEqAux s t;
match isOffset s with
| some (s, k₁) => match isOffset t with
| some (t, k₂) => -- s+k₁ =?= t+k₂

7
src/Lean/Meta/Tactic/Util.lean
View file

@ -41,13 +41,6 @@ mctx ← getMCtx;
opts ← getOptions;
pure $ ppGoal env mctx opts mvarId
@[inline] protected def orelse {α} (x y : MetaM α) : MetaM α := do
env ← getEnv;
s ← get;
catch x (fun _ => do restore env s.mctx s.postponed; y)
instance Meta.hasOrelse {α} : HasOrelse (MetaM α) := ⟨Meta.orelse⟩
@[init] private def regTraceClasses : IO Unit :=
registerTraceClass `Meta.Tactic

2
src/Lean/Meta/WHNF.lean
View file

@ -77,7 +77,7 @@ else if majorType.hasExprMVar && majorType.getAppArgs.anyFrom rec.nparams Expr.h
else do
(some newCtorApp) ← mkNullaryCtor majorType rec.nparams | pure none;
newType ← inferType newCtorApp;
defeq ← Meta.isExprDefEqAux majorType newType;
defeq ← isDefEq majorType newType;
pure $ if defeq then newCtorApp else none
/-- Auxiliary function for reducing recursor applications. -/

24
tests/lean/doSeqRightIssue.lean.expected.out
View file

@ -4,41 +4,41 @@ doSeqRightIssue.lean:7:0: error: don't know how to synthesize placeholder
context:
α : Type u
β : α → (sorryAx (Sort u_1))
ex : ∀ {p₁p₂ : (sorryAx (Sort u_2))} (h₁ : (sorryAx ?m.364)=(sorryAx ?m.364)), (sorryAx (?m.365 h₁))≅_ → p₁=p₂
ex : ∀ {p₁p₂ : (sorryAx (Sort u_2))} (h₁ : (sorryAx ?m.366)=(sorryAx ?m.366)), (sorryAx (?m.367 h₁))≅_ → p₁=p₂
p₁ p₂ : (sorryAx (Sort u_2))
h₁ : (sorryAx ?m.364)=(sorryAx ?m.364)
h : (sorryAx (?m.365 _))≅_
h₁ : (sorryAx ?m.366)=(sorryAx ?m.366)
h : (sorryAx (?m.367 _))≅_
_a_1 _a_2 : (sorryAx (Sort u_2))
_a_3 : (sorryAx ?m.364)=(sorryAx ?m.364)
_a_3 : (sorryAx ?m.366)=(sorryAx ?m.366)
⊢ Prop
doSeqRightIssue.lean:7:0: error: don't know how to synthesize placeholder
context:
α : Type u
β : α → (sorryAx (Sort u_1))
ex : ∀ {p₁p₂ : (sorryAx (Sort u_2))} (h₁ : (sorryAx ?m.364)=(sorryAx ?m.364)), (sorryAx (?m.365 h₁))≅_ → p₁=p₂
ex : ∀ {p₁p₂ : (sorryAx (Sort u_2))} (h₁ : (sorryAx ?m.366)=(sorryAx ?m.366)), (sorryAx (?m.367 h₁))≅_ → p₁=p₂
p₁ p₂ : (sorryAx (Sort u_2))
h₁ : (sorryAx ?m.364)=(sorryAx ?m.364)
h : (sorryAx (?m.365 _))≅_
h₁ : (sorryAx ?m.366)=(sorryAx ?m.366)
h : (sorryAx (?m.367 _))≅_
_a_1 _a_2 : (sorryAx (Sort u_2))
⊢ Prop
doSeqRightIssue.lean:7:66: error: don't know how to synthesize placeholder
@HEq ?m.365 … … …
@HEq ?m.367 … … …
context:
α : Type u
β : α → (sorryAx (Sort u_1))
p₁ p₂ : (sorryAx (Sort u_2))
h₁ : (sorryAx ?m.364)=(sorryAx ?m.364)
h₁ : (sorryAx ?m.366)=(sorryAx ?m.366)
⊢ Prop
doSeqRightIssue.lean:7:66: error: don't know how to synthesize placeholder
@HEq ?m.365 … … …
@HEq ?m.367 … … …
context:
α : Type u
β : α → (sorryAx (Sort u_1))
p₁ p₂ : (sorryAx (Sort u_2))
h₁ : (sorryAx ?m.364)=(sorryAx ?m.364)
h₁ : (sorryAx ?m.366)=(sorryAx ?m.366)
⊢ Prop
doSeqRightIssue.lean:7:48: error: don't know how to synthesize placeholder
@Eq ?m.364 … …
@Eq ?m.366 … …
context:
α : Type u
β : α → (sorryAx (Sort u_1))