From 5481999560c77e346d1ede86cf8384cbb71bfd6c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 26 Oct 2020 14:10:15 -0700 Subject: [PATCH] chore: cleanup --- src/Lean/Meta/AbstractNestedProofs.lean | 80 +- src/Lean/Meta/Check.lean | 134 +-- src/Lean/Meta/Closure.lean | 374 +++---- src/Lean/Meta/CollectMVars.lean | 38 +- src/Lean/Meta/DiscrTree.lean | 397 ++++---- src/Lean/Meta/DiscrTreeTypes.lean | 36 +- src/Lean/Meta/ExprDefEq.lean | 1218 +++++++++++------------ src/Lean/Meta/LevelDefEq.lean | 285 +++--- 8 files changed, 1280 insertions(+), 1282 deletions(-) diff --git a/src/Lean/Meta/AbstractNestedProofs.lean b/src/Lean/Meta/AbstractNestedProofs.lean index f31931bbee..a25f753e36 100644 --- a/src/Lean/Meta/AbstractNestedProofs.lean +++ b/src/Lean/Meta/AbstractNestedProofs.lean @@ -9,60 +9,60 @@ namespace Lean.Meta namespace AbstractNestedProofs def isNonTrivialProof (e : Expr) : MetaM Bool := do -if ! (← isProof e) then - pure false -else - e.withApp fun f args => - pure $ !f.isAtomic || args.any fun arg => !arg.isAtomic + if !(← isProof e) then + pure false + else + e.withApp fun f args => + pure $ !f.isAtomic || args.any fun arg => !arg.isAtomic structure Context := -(baseName : Name) + (baseName : Name) structure State := -(nextIdx : Nat := 1) + (nextIdx : Nat := 1) abbrev M := ReaderT Context $ MonadCacheT Expr Expr $ StateRefT State $ MetaM private def mkAuxLemma (e : Expr) : M Expr := do -let ctx ← read -let s ← get -let lemmaName ← mkAuxName (ctx.baseName ++ `proof) s.nextIdx -modify fun s => { s with nextIdx := s.nextIdx + 1 } -mkAuxDefinitionFor lemmaName e + let ctx ← read + let s ← get + let lemmaName ← mkAuxName (ctx.baseName ++ `proof) s.nextIdx + modify fun s => { s with nextIdx := s.nextIdx + 1 } + mkAuxDefinitionFor lemmaName e partial def visit (e : Expr) : M Expr := do -if e.isAtomic then - pure e -else - let visitBinders (xs : Array Expr) (k : M Expr) : M Expr := do - let localInstances ← getLocalInstances - let lctx ← getLCtx - for x in xs do - let xFVarId := x.fvarId! - let localDecl ← getLocalDecl xFVarId - let type ← visit localDecl.type - let localDecl := localDecl.setType type - let localDecl ← match localDecl.value? with - | some value => do let value ← visit value; pure $ localDecl.setValue value - | none => pure localDecl - lctx :=lctx.modifyLocalDecl xFVarId fun _ => localDecl - withLCtx lctx localInstances k - checkCache e fun e => - if (← isNonTrivialProof e) then - mkAuxLemma e - else match e with - | Expr.lam _ _ _ _ => lambdaLetTelescope e fun xs b => visitBinders xs do mkLambdaFVars xs (← visit b) - | Expr.letE _ _ _ _ _ => lambdaLetTelescope e fun xs b => visitBinders xs do mkLambdaFVars xs (← visit b) - | Expr.forallE _ _ _ _ => forallTelescope e fun xs b => visitBinders xs do mkForallFVars xs (← visit b) - | Expr.mdata _ b _ => do pure $ e.updateMData! (← visit b) - | Expr.proj _ _ b _ => do pure $ e.updateProj! (← visit b) - | Expr.app _ _ _ => e.withApp fun f args => do pure $ mkAppN f (← args.mapM visit) - | _ => pure e + if e.isAtomic then + pure e + else + let visitBinders (xs : Array Expr) (k : M Expr) : M Expr := do + let localInstances ← getLocalInstances + let lctx ← getLCtx + for x in xs do + let xFVarId := x.fvarId! + let localDecl ← getLocalDecl xFVarId + let type ← visit localDecl.type + let localDecl := localDecl.setType type + let localDecl ← match localDecl.value? with + | some value => do let value ← visit value; pure $ localDecl.setValue value + | none => pure localDecl + lctx :=lctx.modifyLocalDecl xFVarId fun _ => localDecl + withLCtx lctx localInstances k + checkCache e fun e => do + if (← isNonTrivialProof e) then + mkAuxLemma e + else match e with + | Expr.lam _ _ _ _ => lambdaLetTelescope e fun xs b => visitBinders xs do mkLambdaFVars xs (← visit b) + | Expr.letE _ _ _ _ _ => lambdaLetTelescope e fun xs b => visitBinders xs do mkLambdaFVars xs (← visit b) + | Expr.forallE _ _ _ _ => forallTelescope e fun xs b => visitBinders xs do mkForallFVars xs (← visit b) + | Expr.mdata _ b _ => return e.updateMData! (← visit b) + | Expr.proj _ _ b _ => return e.updateProj! (← visit b) + | Expr.app _ _ _ => e.withApp fun f args => do return mkAppN f (← args.mapM visit) + | _ => pure e end AbstractNestedProofs /-- Replace proofs nested in `e` with new lemmas. The new lemmas have names of the form `mainDeclName.proof_` -/ def abstractNestedProofs (mainDeclName : Name) (e : Expr) : MetaM Expr := -(((AbstractNestedProofs.visit e).run { baseName := mainDeclName }).run).run' { nextIdx := 1 } + AbstractNestedProofs.visit e $.run { baseName := mainDeclName } $.run $.run' { nextIdx := 1 } end Lean.Meta diff --git a/src/Lean/Meta/Check.lean b/src/Lean/Meta/Check.lean index e1a8f25e66..101c499c0e 100644 --- a/src/Lean/Meta/Check.lean +++ b/src/Lean/Meta/Check.lean @@ -14,100 +14,100 @@ whether terms produced by tactics and `isDefEq` are type correct. namespace Lean.Meta private def ensureType (e : Expr) : MetaM Unit := do -getLevel e -pure () + getLevel e + pure () def throwLetTypeMismatchMessage {α} (fvarId : FVarId) : MetaM α := do -let lctx ← getLCtx -match lctx.find? fvarId with -| some (LocalDecl.ldecl _ _ n t v _) => do - let vType ← inferType v - throwError! "invalid let declaration, term{indentExpr v}\nhas type{indentExpr vType}\nbut is expected to have type{indentExpr t}" -| _ => unreachable! + let lctx ← getLCtx + match lctx.find? fvarId with + | some (LocalDecl.ldecl _ _ n t v _) => do + let vType ← inferType v + throwError! "invalid let declaration, term{indentExpr v}\nhas type{indentExpr vType}\nbut is expected to have type{indentExpr t}" + | _ => unreachable! @[specialize] private def checkLambdaLet (check : Expr → MetaM Unit) (e : Expr) : MetaM Unit := -lambdaLetTelescope e fun xs b => do - xs.forM fun x => do - let xDecl ← getFVarLocalDecl x; - match xDecl with - | LocalDecl.cdecl _ _ _ t _ => - ensureType t - check t - | LocalDecl.ldecl _ _ _ t v _ => - ensureType t - check t - let vType ← inferType v - unless (← isDefEq t vType) do throwLetTypeMismatchMessage x.fvarId! - check v - check b + lambdaLetTelescope e fun xs b => do + xs.forM fun x => do + let xDecl ← getFVarLocalDecl x; + match xDecl with + | LocalDecl.cdecl _ _ _ t _ => + ensureType t + check t + | LocalDecl.ldecl _ _ _ t v _ => + ensureType t + check t + let vType ← inferType v + unless (← isDefEq t vType) do throwLetTypeMismatchMessage x.fvarId! + check v + check b @[specialize] private def checkForall (check : Expr → MetaM Unit) (e : Expr) : MetaM Unit := -forallTelescope e fun xs b => do - xs.forM fun x => do - let xDecl ← getFVarLocalDecl x - ensureType xDecl.type - check xDecl.type - ensureType b - check b + forallTelescope e fun xs b => do + xs.forM fun x => do + let xDecl ← getFVarLocalDecl x + ensureType xDecl.type + check xDecl.type + ensureType b + check b private def checkConstant (constName : Name) (us : List Level) : MetaM Unit := do -let cinfo ← getConstInfo constName -unless us.length == cinfo.lparams.length do - throwIncorrectNumberOfLevels constName us + let cinfo ← getConstInfo constName + unless us.length == cinfo.lparams.length do + throwIncorrectNumberOfLevels constName us private def getFunctionDomain (f : Expr) : MetaM Expr := do -let fType ← inferType f -let fType ← whnfD fType -match fType with -| Expr.forallE _ d _ _ => pure d -| _ => throwFunctionExpected f + let fType ← inferType f + let fType ← whnfD fType + match fType with + | Expr.forallE _ d _ _ => pure d + | _ => throwFunctionExpected f def throwAppTypeMismatch {α} {m} [Monad m] [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m] [MonadLiftT MetaM m] (f a : Expr) (extraMsg : MessageData := Format.nil) : m α := do -let e := mkApp f a -let aType ← inferType a -let expectedType ← liftM $ getFunctionDomain f -throwError! "application type mismatch{indentExpr e}\nargument{indentExpr a}\nhas type{indentExpr aType}\nbut is expected to have type{indentExpr expectedType}{extraMsg}" + let e := mkApp f a + let aType ← inferType a + let expectedType ← liftM $ getFunctionDomain f + throwError! "application type mismatch{indentExpr e}\nargument{indentExpr a}\nhas type{indentExpr aType}\nbut is expected to have type{indentExpr expectedType}{extraMsg}" @[specialize] private def checkApp (check : Expr → MetaM Unit) (f a : Expr) : MetaM Unit := do -check f -check a -let fType ← inferType f -let fType ← whnf fType -match fType with -| Expr.forallE _ d _ _ => - let aType ← inferType a - unless (← isDefEq d aType) do - throwAppTypeMismatch f a -| _ => throwFunctionExpected (mkApp f a) + check f + check a + let fType ← inferType f + let fType ← whnf fType + match fType with + | Expr.forallE _ d _ _ => + let aType ← inferType a + unless (← isDefEq d aType) do + throwAppTypeMismatch f a + | _ => throwFunctionExpected (mkApp f a) private partial def checkAux : Expr → MetaM Unit -| e@(Expr.forallE ..) => checkForall checkAux e -| e@(Expr.lam ..) => checkLambdaLet checkAux e -| e@(Expr.letE ..) => checkLambdaLet checkAux e -| Expr.const c lvls _ => checkConstant c lvls -| Expr.app f a _ => checkApp checkAux f a -| Expr.mdata _ e _ => checkAux e -| Expr.proj _ _ e _ => checkAux e -| _ => pure () + | e@(Expr.forallE ..) => checkForall checkAux e + | e@(Expr.lam ..) => checkLambdaLet checkAux e + | e@(Expr.letE ..) => checkLambdaLet checkAux e + | Expr.const c lvls _ => checkConstant c lvls + | Expr.app f a _ => checkApp checkAux f a + | Expr.mdata _ e _ => checkAux e + | Expr.proj _ _ e _ => checkAux e + | _ => pure () def check (e : Expr) : MetaM Unit := -traceCtx `Meta.check $ - withTransparency TransparencyMode.all $ checkAux e + traceCtx `Meta.check do + withTransparency TransparencyMode.all $ checkAux e def isTypeCorrect (e : Expr) : MetaM Bool := do -try - check e - pure true -catch ex => - trace[Meta.typeError]! ex.toMessageData - pure false + try + check e + pure true + catch ex => + trace[Meta.typeError]! ex.toMessageData + pure false builtin_initialize registerTraceClass `Meta.check diff --git a/src/Lean/Meta/Closure.lean b/src/Lean/Meta/Closure.lean index 358ab883a1..e80981a67d 100644 --- a/src/Lean/Meta/Closure.lean +++ b/src/Lean/Meta/Closure.lean @@ -98,196 +98,197 @@ namespace Lean.Meta namespace Closure structure ToProcessElement := -(fvarId : FVarId) (newFVarId : FVarId) + (fvarId : FVarId) + (newFVarId : FVarId) instance : Inhabited ToProcessElement := -⟨⟨arbitrary _, arbitrary _⟩⟩ + ⟨⟨arbitrary _, arbitrary _⟩⟩ structure Context := -(zeta : Bool) + (zeta : Bool) structure State := -(visitedLevel : LevelMap Level := {}) -(visitedExpr : ExprStructMap Expr := {}) -(levelParams : Array Name := #[]) -(nextLevelIdx : Nat := 1) -(levelArgs : Array Level := #[]) -(newLocalDecls : Array LocalDecl := #[]) -(newLocalDeclsForMVars : Array LocalDecl := #[]) -(newLetDecls : Array LocalDecl := #[]) -(nextExprIdx : Nat := 1) -(exprMVarArgs : Array Expr := #[]) -(exprFVarArgs : Array Expr := #[]) -(toProcess : Array ToProcessElement := #[]) + (visitedLevel : LevelMap Level := {}) + (visitedExpr : ExprStructMap Expr := {}) + (levelParams : Array Name := #[]) + (nextLevelIdx : Nat := 1) + (levelArgs : Array Level := #[]) + (newLocalDecls : Array LocalDecl := #[]) + (newLocalDeclsForMVars : Array LocalDecl := #[]) + (newLetDecls : Array LocalDecl := #[]) + (nextExprIdx : Nat := 1) + (exprMVarArgs : Array Expr := #[]) + (exprFVarArgs : Array Expr := #[]) + (toProcess : Array ToProcessElement := #[]) abbrev ClosureM := ReaderT Context $ StateRefT State MetaM @[inline] def visitLevel (f : Level → ClosureM Level) (u : Level) : ClosureM Level := do -if !u.hasMVar && !u.hasParam then - pure u -else - let s ← get - match s.visitedLevel.find? u with - | some v => pure v - | none => do - let v ← f u - modify fun s => { s with visitedLevel := s.visitedLevel.insert u v } - pure v + if !u.hasMVar && !u.hasParam then + pure u + else + let s ← get + match s.visitedLevel.find? u with + | some v => pure v + | none => do + let v ← f u + modify fun s => { s with visitedLevel := s.visitedLevel.insert u v } + pure v @[inline] def visitExpr (f : Expr → ClosureM Expr) (e : Expr) : ClosureM Expr := do -if !e.hasLevelParam && !e.hasFVar && !e.hasMVar then - pure e -else - let s ← get - match s.visitedExpr.find? e with - | some r => pure r - | none => - let r ← f e - modify fun s => { s with visitedExpr := s.visitedExpr.insert e r } - pure r + if !e.hasLevelParam && !e.hasFVar && !e.hasMVar then + pure e + else + let s ← get + match s.visitedExpr.find? e with + | some r => pure r + | none => + let r ← f e + modify fun s => { s with visitedExpr := s.visitedExpr.insert e r } + pure r def mkNewLevelParam (u : Level) : ClosureM Level := do -let s ← get -let p := (`u).appendIndexAfter s.nextLevelIdx -modify fun s => { s with levelParams := s.levelParams.push p, nextLevelIdx := s.nextLevelIdx + 1, levelArgs := s.levelArgs.push u } -pure $ mkLevelParam p + let s ← get + let p := (`u).appendIndexAfter s.nextLevelIdx + modify fun s => { s with levelParams := s.levelParams.push p, nextLevelIdx := s.nextLevelIdx + 1, levelArgs := s.levelArgs.push u } + pure $ mkLevelParam p partial def collectLevelAux : Level → ClosureM Level -| u@(Level.succ v _) => do return u.updateSucc! (← visitLevel collectLevelAux v) -| u@(Level.max v w _) => do return u.updateMax! (← visitLevel collectLevelAux v) (← visitLevel collectLevelAux w) -| u@(Level.imax v w _) => do return u.updateIMax! (← visitLevel collectLevelAux v) (← visitLevel collectLevelAux w) -| u@(Level.mvar mvarId _) => mkNewLevelParam u -| u@(Level.param _ _) => mkNewLevelParam u -| u@(Level.zero _) => pure u + | u@(Level.succ v _) => do return u.updateSucc! (← visitLevel collectLevelAux v) + | u@(Level.max v w _) => do return u.updateMax! (← visitLevel collectLevelAux v) (← visitLevel collectLevelAux w) + | u@(Level.imax v w _) => do return u.updateIMax! (← visitLevel collectLevelAux v) (← visitLevel collectLevelAux w) + | u@(Level.mvar mvarId _) => mkNewLevelParam u + | u@(Level.param _ _) => mkNewLevelParam u + | u@(Level.zero _) => pure u def collectLevel (u : Level) : ClosureM Level := do --- u ← instantiateLevelMVars u -visitLevel collectLevelAux u + -- u ← instantiateLevelMVars u + visitLevel collectLevelAux u def preprocess (e : Expr) : ClosureM Expr := do -let e ← instantiateMVars e -let ctx ← read --- If we are not zeta-expanding let-decls, then we use `check` to find --- which let-decls are dependent. We say a let-decl is dependent if its lambda abstraction is type incorrect. -if !ctx.zeta then - check e -pure e + let e ← instantiateMVars e + let ctx ← read + -- If we are not zeta-expanding let-decls, then we use `check` to find + -- which let-decls are dependent. We say a let-decl is dependent if its lambda abstraction is type incorrect. + if !ctx.zeta then + check e + pure e /-- Remark: This method does not guarantee unique user names. The correctness of the procedure does not rely on unique user names. Recall that the pretty printer takes care of unintended collisions. -/ def mkNextUserName : ClosureM Name := do -let s ← get -let n := (`_x).appendIndexAfter s.nextExprIdx -modify fun s => { s with nextExprIdx := s.nextExprIdx + 1 } -pure n + let s ← get + let n := (`_x).appendIndexAfter s.nextExprIdx + modify fun s => { s with nextExprIdx := s.nextExprIdx + 1 } + pure n def pushToProcess (elem : ToProcessElement) : ClosureM Unit := -modify fun s => { s with toProcess := s.toProcess.push elem } + modify fun s => { s with toProcess := s.toProcess.push elem } partial def collectExprAux (e : Expr) : ClosureM Expr := do -let collect (e : Expr) := visitExpr collectExprAux e -match e with -| Expr.proj _ _ s _ => return e.updateProj! (← collect s) -| Expr.forallE _ d b _ => return e.updateForallE! (← collect d) (← collect b) -| Expr.lam _ d b _ => return e.updateLambdaE! (← collect d) (← collect b) -| Expr.letE _ t v b _ => return e.updateLet! (← collect t) (← collect v) (← collect b) -| Expr.app f a _ => return e.updateApp! (← collect f) (← collect a) -| Expr.mdata _ b _ => return e.updateMData! (← collect b) -| Expr.sort u _ => return e.updateSort! (← collectLevel u) -| Expr.const c us _ => return e.updateConst! (← us.mapM collectLevel) -| Expr.mvar mvarId _ => - let mvarDecl ← getMVarDecl mvarId - let type ← preprocess mvarDecl.type - let type ← collect type - let newFVarId ← mkFreshFVarId - let userName ← mkNextUserName - modify fun s => { s with - newLocalDeclsForMVars := s.newLocalDeclsForMVars.push $ LocalDecl.cdecl (arbitrary _) newFVarId userName type BinderInfo.default, - exprMVarArgs := s.exprMVarArgs.push e - } - return mkFVar newFVarId -| Expr.fvar fvarId _ => - match (← read).zeta, (← getLocalDecl fvarId).value? with - | true, some value => collect (← preprocess value) - | _, _ => + let collect (e : Expr) := visitExpr collectExprAux e + match e with + | Expr.proj _ _ s _ => return e.updateProj! (← collect s) + | Expr.forallE _ d b _ => return e.updateForallE! (← collect d) (← collect b) + | Expr.lam _ d b _ => return e.updateLambdaE! (← collect d) (← collect b) + | Expr.letE _ t v b _ => return e.updateLet! (← collect t) (← collect v) (← collect b) + | Expr.app f a _ => return e.updateApp! (← collect f) (← collect a) + | Expr.mdata _ b _ => return e.updateMData! (← collect b) + | Expr.sort u _ => return e.updateSort! (← collectLevel u) + | Expr.const c us _ => return e.updateConst! (← us.mapM collectLevel) + | Expr.mvar mvarId _ => + let mvarDecl ← getMVarDecl mvarId + let type ← preprocess mvarDecl.type + let type ← collect type let newFVarId ← mkFreshFVarId - pushToProcess ⟨fvarId, newFVarId⟩ + let userName ← mkNextUserName + modify fun s => { s with + newLocalDeclsForMVars := s.newLocalDeclsForMVars.push $ LocalDecl.cdecl (arbitrary _) newFVarId userName type BinderInfo.default, + exprMVarArgs := s.exprMVarArgs.push e + } return mkFVar newFVarId -| e => pure e + | Expr.fvar fvarId _ => + match (← read).zeta, (← getLocalDecl fvarId).value? with + | true, some value => collect (← preprocess value) + | _, _ => + let newFVarId ← mkFreshFVarId + pushToProcess ⟨fvarId, newFVarId⟩ + return mkFVar newFVarId + | e => pure e def collectExpr (e : Expr) : ClosureM Expr := do -let e ← preprocess e -visitExpr collectExprAux e + let e ← preprocess e + visitExpr collectExprAux e partial def pickNextToProcessAux (lctx : LocalContext) (i : Nat) (toProcess : Array ToProcessElement) (elem : ToProcessElement) : ToProcessElement × Array ToProcessElement := -if h : i < toProcess.size then - let elem' := toProcess.get ⟨i, h⟩ - if (lctx.get! elem.fvarId).index < (lctx.get! elem'.fvarId).index then - pickNextToProcessAux lctx (i+1) (toProcess.set ⟨i, h⟩ elem) elem' + if h : i < toProcess.size then + let elem' := toProcess.get ⟨i, h⟩ + if (lctx.get! elem.fvarId).index < (lctx.get! elem'.fvarId).index then + pickNextToProcessAux lctx (i+1) (toProcess.set ⟨i, h⟩ elem) elem' + else + pickNextToProcessAux lctx (i+1) toProcess elem else - pickNextToProcessAux lctx (i+1) toProcess elem -else - (elem, toProcess) + (elem, toProcess) def pickNextToProcess? : ClosureM (Option ToProcessElement) := do -let lctx ← getLCtx -let s ← get -if s.toProcess.isEmpty then pure none -else - modifyGet fun s => - let elem := s.toProcess.back - let toProcess := s.toProcess.pop - let (elem, toProcess) := pickNextToProcessAux lctx 0 toProcess elem - (some elem, { s with toProcess := toProcess }) + let lctx ← getLCtx + let s ← get + if s.toProcess.isEmpty then + pure none + else + modifyGet fun s => + let elem := s.toProcess.back + let toProcess := s.toProcess.pop + let (elem, toProcess) := pickNextToProcessAux lctx 0 toProcess elem + (some elem, { s with toProcess := toProcess }) def pushFVarArg (e : Expr) : ClosureM Unit := -modify fun s => { s with exprFVarArgs := s.exprFVarArgs.push e } + modify fun s => { s with exprFVarArgs := s.exprFVarArgs.push e } def pushLocalDecl (newFVarId : FVarId) (userName : Name) (type : Expr) (bi := BinderInfo.default) : ClosureM Unit := do -let type ← collectExpr type -modify fun s => { s with newLocalDecls := s.newLocalDecls.push $ LocalDecl.cdecl (arbitrary _) newFVarId userName type bi } + let type ← collectExpr type + modify fun s => { s with newLocalDecls := s.newLocalDecls.push $ LocalDecl.cdecl (arbitrary _) newFVarId userName type bi } partial def process : ClosureM Unit := do -match (← pickNextToProcess?) with -| none => pure () -| some ⟨fvarId, newFVarId⟩ => - let localDecl ← getLocalDecl fvarId - match localDecl with - | LocalDecl.cdecl _ _ userName type bi => - pushLocalDecl newFVarId userName type bi - pushFVarArg (mkFVar fvarId) - process - | LocalDecl.ldecl _ _ userName type val _ => - let zetaFVarIds ← getZetaFVarIds - if !zetaFVarIds.contains fvarId then - /- Non-dependent let-decl - - Recall that if `fvarId` is in `zetaFVarIds`, then we zeta-expanded it - during type checking (see `check` at `collectExpr`). - - Our type checker may zeta-expand declarations that are not needed, but this - check is conservative, and seems to work well in practice. -/ - pushLocalDecl newFVarId userName type + match (← pickNextToProcess?) with + | none => pure () + | some ⟨fvarId, newFVarId⟩ => + let localDecl ← getLocalDecl fvarId + match localDecl with + | LocalDecl.cdecl _ _ userName type bi => + pushLocalDecl newFVarId userName type bi pushFVarArg (mkFVar fvarId) process - else - /- Dependent let-decl -/ - let type ← collectExpr type - let val ← collectExpr val - modify fun s => { s with newLetDecls := s.newLetDecls.push $ LocalDecl.ldecl (arbitrary _) newFVarId userName type val false } - /- We don't want to interleave let and lambda declarations in our closure. So, we expand any occurrences of newFVarId - at `newLocalDecls` -/ - modify fun s => { s with newLocalDecls := s.newLocalDecls.map (replaceFVarIdAtLocalDecl newFVarId val) } - process + | LocalDecl.ldecl _ _ userName type val _ => + let zetaFVarIds ← getZetaFVarIds + if !zetaFVarIds.contains fvarId then + /- Non-dependent let-decl + + Recall that if `fvarId` is in `zetaFVarIds`, then we zeta-expanded it + during type checking (see `check` at `collectExpr`). + + Our type checker may zeta-expand declarations that are not needed, but this + check is conservative, and seems to work well in practice. -/ + pushLocalDecl newFVarId userName type + pushFVarArg (mkFVar fvarId) + process + else + /- Dependent let-decl -/ + let type ← collectExpr type + let val ← collectExpr val + modify fun s => { s with newLetDecls := s.newLetDecls.push $ LocalDecl.ldecl (arbitrary _) newFVarId userName type val false } + /- We don't want to interleave let and lambda declarations in our closure. So, we expand any occurrences of newFVarId + at `newLocalDecls` -/ + modify fun s => { s with newLocalDecls := s.newLocalDecls.map (replaceFVarIdAtLocalDecl newFVarId val) } + process @[inline] def mkBinding (isLambda : Bool) (decls : Array LocalDecl) (b : Expr) : Expr := -let xs := decls.map LocalDecl.toExpr -let b := b.abstract xs -decls.size.foldRev - (fun i b => + let xs := decls.map LocalDecl.toExpr + let b := b.abstract xs + decls.size.foldRev (init := b) fun i b => let decl := decls[i] match decl with | LocalDecl.cdecl _ _ n ty bi => @@ -302,64 +303,63 @@ decls.size.foldRev let val := val.abstractRange i xs mkLet n ty val b nonDep else - b.lowerLooseBVars 1 1) - b + b.lowerLooseBVars 1 1 def mkLambda (decls : Array LocalDecl) (b : Expr) : Expr := -mkBinding true decls b + mkBinding true decls b def mkForall (decls : Array LocalDecl) (b : Expr) : Expr := -mkBinding false decls b + mkBinding false decls b structure MkValueTypeClosureResult := -(levelParams : Array Name) -(type : Expr) -(value : Expr) -(levelArgs : Array Level) -(exprArgs : Array Expr) + (levelParams : Array Name) + (type : Expr) + (value : Expr) + (levelArgs : Array Level) + (exprArgs : Array Expr) def mkValueTypeClosureAux (type : Expr) (value : Expr) : ClosureM (Expr × Expr) := do -resetZetaFVarIds -withTrackingZeta do - let type ← collectExpr type - let value ← collectExpr value - process - pure (type, value) + resetZetaFVarIds + withTrackingZeta do + let type ← collectExpr type + let value ← collectExpr value + process + pure (type, value) def mkValueTypeClosure (type : Expr) (value : Expr) (zeta : Bool) : MetaM MkValueTypeClosureResult := do -let ((type, value), s) ← ((mkValueTypeClosureAux type value).run { zeta := zeta }).run {} -let newLocalDecls := s.newLocalDecls.reverse ++ s.newLocalDeclsForMVars -let newLetDecls := s.newLetDecls.reverse -let type := mkForall newLocalDecls (mkForall newLetDecls type) -let value := mkLambda newLocalDecls (mkLambda newLetDecls value) -pure { - type := type, - value := value, - levelParams := s.levelParams, - levelArgs := s.levelArgs, - exprArgs := s.exprFVarArgs.reverse ++ s.exprMVarArgs -} + let ((type, value), s) ← ((mkValueTypeClosureAux type value).run { zeta := zeta }).run {} + let newLocalDecls := s.newLocalDecls.reverse ++ s.newLocalDeclsForMVars + let newLetDecls := s.newLetDecls.reverse + let type := mkForall newLocalDecls (mkForall newLetDecls type) + let value := mkLambda newLocalDecls (mkLambda newLetDecls value) + pure { + type := type, + value := value, + levelParams := s.levelParams, + levelArgs := s.levelArgs, + exprArgs := s.exprFVarArgs.reverse ++ s.exprMVarArgs + } end Closure variables {m : Type → Type} [MonadLiftT MetaM m] private def mkAuxDefinitionImp (name : Name) (type : Expr) (value : Expr) (zeta : Bool) (compile : Bool) : MetaM Expr := do -let result ← Closure.mkValueTypeClosure type value zeta -let env ← getEnv -let decl := Declaration.defnDecl { - name := name, - lparams := result.levelParams.toList, - type := result.type, - value := result.value, - hints := ReducibilityHints.regular (getMaxHeight env result.value + 1), - isUnsafe := env.hasUnsafe result.type || env.hasUnsafe result.value -} -trace[Meta.debug]! "{name} : {result.type} := {result.value}" -addDecl decl -if compile then - compileDecl decl -pure $ mkAppN (mkConst name result.levelArgs.toList) result.exprArgs + let result ← Closure.mkValueTypeClosure type value zeta + let env ← getEnv + let decl := Declaration.defnDecl { + name := name, + lparams := result.levelParams.toList, + type := result.type, + value := result.value, + hints := ReducibilityHints.regular (getMaxHeight env result.value + 1), + isUnsafe := env.hasUnsafe result.type || env.hasUnsafe result.value + } + trace[Meta.debug]! "{name} : {result.type} := {result.value}" + addDecl decl + if compile then + compileDecl decl + pure $ mkAppN (mkConst name result.levelArgs.toList) result.exprArgs /-- Create an auxiliary definition with the given name, type and value. @@ -368,13 +368,13 @@ pure $ mkAppN (mkConst name result.levelArgs.toList) result.exprArgs returned where `u_i`s are universe parameters and metavariables `type` and `value` depend on, and `t_j`s are free and meta variables `type` and `value` depend on. -/ def mkAuxDefinition (name : Name) (type : Expr) (value : Expr) (zeta := false) (compile := true) : m Expr := liftMetaM do -trace[Meta.debug]! "{name} : {type} := {value}" -mkAuxDefinitionImp name type value zeta compile + trace[Meta.debug]! "{name} : {type} := {value}" + mkAuxDefinitionImp name type value zeta compile /-- Similar to `mkAuxDefinition`, but infers the type of `value`. -/ def mkAuxDefinitionFor (name : Name) (value : Expr) : m Expr := liftMetaM do -let type ← inferType value -let type := type.headBeta -mkAuxDefinition name type value + let type ← inferType value + let type := type.headBeta + mkAuxDefinition name type value end Lean.Meta diff --git a/src/Lean/Meta/CollectMVars.lean b/src/Lean/Meta/CollectMVars.lean index 574054376a..28761a798c 100644 --- a/src/Lean/Meta/CollectMVars.lean +++ b/src/Lean/Meta/CollectMVars.lean @@ -18,42 +18,42 @@ namespace Lean.Meta we collect `?m` and unassigned metavariables occurring in `t`. We collect `?m` because it has not been assigned yet. -/ partial def collectMVars (e : Expr) : StateRefT CollectMVars.State MetaM Unit := do -let e ← instantiateMVars e -let s ← get -let resultSavedSize := s.result.size -let s := e.collectMVars s -set s -for mvarId in s.result[resultSavedSize:] do - match (← getDelayedAssignment? mvarId) with - | none => pure () - | some d => collectMVars d.val + let e ← instantiateMVars e + let s ← get + let resultSavedSize := s.result.size + let s := e.collectMVars s + set s + for mvarId in s.result[resultSavedSize:] do + match (← getDelayedAssignment? mvarId) with + | none => pure () + | some d => collectMVars d.val variables {m : Type → Type} [MonadLiftT MetaM m] def getMVarsImp (e : Expr) : MetaM (Array MVarId) := do -let (_, s) ← (collectMVars e).run {} -pure s.result + let (_, s) ← (collectMVars e).run {} + pure s.result /-- Return metavariables in occuring the given expression. See `collectMVars` -/ def getMVars (e : Expr) : m (Array MVarId) := -liftM $ getMVarsImp e + liftM $ getMVarsImp e def getMVarsNoDelayedImp (e : Expr) : MetaM (Array MVarId) := do -let mvarIds ← getMVars e -mvarIds.filterM fun mvarId => not <$> isDelayedAssigned mvarId + let mvarIds ← getMVars e + mvarIds.filterM fun mvarId => not <$> isDelayedAssigned mvarId /-- Similar to getMVars, but removes delayed assignments. -/ def getMVarsNoDelayed (e : Expr) : m (Array MVarId) := -liftM $ getMVarsNoDelayedImp e + liftM $ getMVarsNoDelayedImp e def collectMVarsAtDecl (d : Declaration) : StateRefT CollectMVars.State MetaM Unit := -d.forExprM collectMVars + d.forExprM collectMVars def getMVarsAtDeclImp (d : Declaration) : MetaM (Array MVarId) := do -let (_, s) ← (collectMVarsAtDecl d).run {} -pure s.result + let (_, s) ← (collectMVarsAtDecl d).run {} + pure s.result def getMVarsAtDecl (d : Declaration) : m (Array MVarId) := -liftM $ getMVarsAtDeclImp d + liftM $ getMVarsAtDeclImp d end Lean.Meta diff --git a/src/Lean/Meta/DiscrTree.lean b/src/Lean/Meta/DiscrTree.lean index b23b3e27f4..487c0c35b0 100644 --- a/src/Lean/Meta/DiscrTree.lean +++ b/src/Lean/Meta/DiscrTree.lean @@ -49,35 +49,35 @@ namespace Lean.Meta.DiscrTree -/ def Key.ctorIdx : Key → Nat -| Key.star => 0 -| Key.other => 1 -| Key.lit _ => 2 -| Key.fvar _ _ => 3 -| Key.const _ _ => 4 + | Key.star => 0 + | Key.other => 1 + | Key.lit _ => 2 + | Key.fvar _ _ => 3 + | Key.const _ _ => 4 def Key.lt : Key → Key → Bool -| Key.lit v₁, Key.lit v₂ => v₁ < v₂ -| Key.fvar n₁ a₁, Key.fvar n₂ a₂ => Name.quickLt n₁ n₂ || (n₁ == n₂ && a₁ < a₂) -| Key.const n₁ a₁, Key.const n₂ a₂ => Name.quickLt n₁ n₂ || (n₁ == n₂ && a₁ < a₂) -| k₁, k₂ => k₁.ctorIdx < k₂.ctorIdx + | Key.lit v₁, Key.lit v₂ => v₁ < v₂ + | Key.fvar n₁ a₁, Key.fvar n₂ a₂ => Name.quickLt n₁ n₂ || (n₁ == n₂ && a₁ < a₂) + | Key.const n₁ a₁, Key.const n₂ a₂ => Name.quickLt n₁ n₂ || (n₁ == n₂ && a₁ < a₂) + | k₁, k₂ => k₁.ctorIdx < k₂.ctorIdx instance : HasLess Key := ⟨fun a b => Key.lt a b⟩ instance (a b : Key) : Decidable (a < b) := inferInstanceAs (Decidable (Key.lt a b)) def Key.format : Key → Format -| Key.star => "*" -| Key.other => "◾" -| Key.lit (Literal.natVal v) => fmt v -| Key.lit (Literal.strVal v) => repr v -| Key.const k _ => fmt k -| Key.fvar k _ => fmt k + | Key.star => "*" + | Key.other => "◾" + | Key.lit (Literal.natVal v) => fmt v + | Key.lit (Literal.strVal v) => repr v + | Key.const k _ => fmt k + | Key.fvar k _ => fmt k instance : HasFormat Key := ⟨Key.format⟩ def Key.arity : Key → Nat -| Key.const _ a => a -| Key.fvar _ a => a -| _ => 0 + | Key.const _ a => a + | Key.fvar _ a => a + | _ => 0 instance {α} : Inhabited (Trie α) := ⟨Trie.node #[] #[]⟩ @@ -121,27 +121,26 @@ instance {α} : Inhabited (DiscrTree α) := ⟨{}⟩ and `ignoreArg` would return true for any term of the form `noIndexing t`. -/ private def ignoreArg (a : Expr) (i : Nat) (infos : Array ParamInfo) : MetaM Bool := -if h : i < infos.size then - let info := infos.get ⟨i, h⟩ - if info.instImplicit then - pure true - else if info.implicit then - not <$> isType a + if h : i < infos.size then + let info := infos.get ⟨i, h⟩ + if info.instImplicit then + pure true + else if info.implicit then + not <$> isType a + else + isProof a else isProof a -else - isProof a private partial def pushArgsAux (infos : Array ParamInfo) : Nat → Expr → Array Expr → MetaM (Array Expr) -| i, Expr.app f a _, todo => do - if (← ignoreArg a i infos) then - pushArgsAux infos (i-1) f (todo.push tmpStar) - else - pushArgsAux infos (i-1) f (todo.push a) -| _, _, todo => pure todo + | i, Expr.app f a _, todo => do + if (← ignoreArg a i infos) then + pushArgsAux infos (i-1) f (todo.push tmpStar) + else + pushArgsAux infos (i-1) f (todo.push a) + | _, _, todo => pure todo -private partial def whnfEta : Expr → MetaM Expr -| e => do +private partial def whnfEta (e : Expr) : MetaM Expr := do let e ← whnf e match e.etaExpandedStrict? with | some e => whnfEta e @@ -152,38 +151,37 @@ private partial def whnfEta : Expr → MetaM Expr Then, `DiscrTree` users may control which symbols should be treated as wildcards. Different `DiscrTree` users may populate this set using, for example, attributes. -/ private def shouldAddAsStar (constName : Name) : Bool := -constName == `Nat.zero || constName == `Nat.succ || constName == `Nat.add || constName == `HasAdd.add + constName == `Nat.zero || constName == `Nat.succ || constName == `Nat.add || constName == `HasAdd.add private def pushArgs (todo : Array Expr) (e : Expr) : MetaM (Key × Array Expr) := do -let e ← whnfEta e -let fn := e.getAppFn -let push (k : Key) (nargs : Nat) : MetaM (Key × Array Expr) := do - let info ← getFunInfoNArgs fn nargs - let todo ← pushArgsAux info.paramInfo (nargs-1) e todo - pure (k, todo) -match fn with -| Expr.lit v _ => pure (Key.lit v, todo) -| Expr.const c _ _ => - if shouldAddAsStar c then - pure (Key.star, todo) - else + let e ← whnfEta e + let fn := e.getAppFn + let push (k : Key) (nargs : Nat) : MetaM (Key × Array Expr) := do + let info ← getFunInfoNArgs fn nargs + let todo ← pushArgsAux info.paramInfo (nargs-1) e todo + pure (k, todo) + match fn with + | Expr.lit v _ => pure (Key.lit v, todo) + | Expr.const c _ _ => + if shouldAddAsStar c then + pure (Key.star, todo) + else + let nargs := e.getAppNumArgs + push (Key.const c nargs) nargs + | Expr.fvar fvarId _ => let nargs := e.getAppNumArgs - push (Key.const c nargs) nargs -| Expr.fvar fvarId _ => - let nargs := e.getAppNumArgs - push (Key.fvar fvarId nargs) nargs -| Expr.mvar mvarId _ => - if mvarId == tmpMVarId then - -- We use `tmp to mark implicit arguments and proofs - pure (Key.star, todo) - else if (← isReadOnlyOrSyntheticOpaqueExprMVar mvarId) then - pure (Key.other, todo) - else - pure (Key.star, todo) -| _ => pure (Key.other, todo) + push (Key.fvar fvarId nargs) nargs + | Expr.mvar mvarId _ => + if mvarId == tmpMVarId then + -- We use `tmp to mark implicit arguments and proofs + pure (Key.star, todo) + else if (← isReadOnlyOrSyntheticOpaqueExprMVar mvarId) then + pure (Key.other, todo) + else + pure (Key.star, todo) + | _ => pure (Key.other, todo) -partial def mkPathAux : Array Expr → Array Key → MetaM (Array Key) -| todo, keys => do +partial def mkPathAux (todo : Array Expr) (keys : Array Key) : MetaM (Array Key) := do if todo.isEmpty then pure keys else @@ -195,13 +193,12 @@ partial def mkPathAux : Array Expr → Array Key → MetaM (Array Key) private def initCapacity := 8 def mkPath (e : Expr) : MetaM (Array Key) := -withReducible do - let todo : Array Expr := Array.mkEmpty initCapacity - let keys : Array Key := Array.mkEmpty initCapacity - mkPathAux (todo.push e) keys + withReducible do + let todo : Array Expr := Array.mkEmpty initCapacity + let keys : Array Key := Array.mkEmpty initCapacity + mkPathAux (todo.push e) keys -private partial def createNodes {α} (keys : Array Key) (v : α) : Nat → Trie α -| i => +private partial def createNodes {α} (keys : Array Key) (v : α) (i : Nat) : Trie α := if h : i < keys.size then let k := keys.get ⟨i, h⟩ let c := createNodes keys v (i+1) @@ -210,168 +207,168 @@ private partial def createNodes {α} (keys : Array Key) (v : α) : Nat → Trie Trie.node #[v] #[] private def insertVal {α} [HasBeq α] (vs : Array α) (v : α) : Array α := -if vs.contains v then vs else vs.push v + if vs.contains v then vs else vs.push v private partial def insertAux {α} [HasBeq α] (keys : Array Key) (v : α) : Nat → Trie α → Trie α -| i, Trie.node vs cs => - if h : i < keys.size then - let k := keys.get ⟨i, h⟩ - let c := Id.run $ cs.binInsertM - (fun a b => a.1 < b.1) - (fun ⟨_, s⟩ => let c := insertAux keys v (i+1) s; (k, c)) -- merge with existing - (fun _ => let c := createNodes keys v (i+1); (k, c)) - (k, arbitrary _) - Trie.node vs c - else - Trie.node (insertVal vs v) cs + | i, Trie.node vs cs => + if h : i < keys.size then + let k := keys.get ⟨i, h⟩ + let c := Id.run $ cs.binInsertM + (fun a b => a.1 < b.1) + (fun ⟨_, s⟩ => let c := insertAux keys v (i+1) s; (k, c)) -- merge with existing + (fun _ => let c := createNodes keys v (i+1); (k, c)) + (k, arbitrary _) + Trie.node vs c + else + Trie.node (insertVal vs v) cs def insertCore {α} [HasBeq α] (d : DiscrTree α) (keys : Array Key) (v : α) : DiscrTree α := -if keys.isEmpty then panic! "invalid key sequence" -else - let k := keys[0] - match d.root.find? k with - | none => - let c := createNodes keys v 1 - { root := d.root.insert k c } - | some c => - let c := insertAux keys v 1 c - { root := d.root.insert k c } + if keys.isEmpty then panic! "invalid key sequence" + else + let k := keys[0] + match d.root.find? k with + | none => + let c := createNodes keys v 1 + { root := d.root.insert k c } + | some c => + let c := insertAux keys v 1 c + { root := d.root.insert k c } def insert {α} [HasBeq α] (d : DiscrTree α) (e : Expr) (v : α) : MetaM (DiscrTree α) := do -let keys ← mkPath e -pure $ d.insertCore keys v + let keys ← mkPath e + pure $ d.insertCore keys v partial def Trie.format {α} [HasFormat α] : Trie α → Format -| Trie.node vs cs => Format.group $ Format.paren $ - "node" ++ (if vs.isEmpty then Format.nil else " " ++ fmt vs) - ++ Format.join (cs.toList.map $ fun ⟨k, c⟩ => Format.line ++ Format.paren (fmt k ++ " => " ++ format c)) + | Trie.node vs cs => Format.group $ Format.paren $ + "node" ++ (if vs.isEmpty then Format.nil else " " ++ fmt vs) + ++ Format.join (cs.toList.map $ fun ⟨k, c⟩ => Format.line ++ Format.paren (fmt k ++ " => " ++ format c)) instance {α} [HasFormat α] : HasFormat (Trie α) := ⟨Trie.format⟩ partial def format {α} [HasFormat α] (d : DiscrTree α) : Format := -let (_, r) := d.root.foldl - (fun (p : Bool × Format) k c => - (false, p.2 ++ (if p.1 == true then Format.nil else Format.line) ++ Format.paren (fmt k ++ " => " ++ fmt c))) -- TODO: fix p.1 == true - (true, Format.nil) -Format.group r + let (_, r) := d.root.foldl + (fun (p : Bool × Format) k c => + (false, p.2 ++ (if p.1 == true then Format.nil else Format.line) ++ Format.paren (fmt k ++ " => " ++ fmt c))) -- TODO: fix p.1 == true + (true, Format.nil) + Format.group r instance {α} [HasFormat α] : HasFormat (DiscrTree α) := ⟨format⟩ private def getKeyArgs (e : Expr) (isMatch? : Bool) : MetaM (Key × Array Expr) := do -let e ← whnfEta e -match e.getAppFn with -| Expr.lit v _ => pure (Key.lit v, #[]) -| Expr.const c _ _ => - let nargs := e.getAppNumArgs - pure (Key.const c nargs, e.getAppRevArgs) -| Expr.fvar fvarId _ => - let nargs := e.getAppNumArgs - pure (Key.fvar fvarId nargs, e.getAppRevArgs) -| Expr.mvar mvarId _ => - if isMatch? then - pure (Key.other, #[]) - else do - let ctx ← read - if ctx.config.isDefEqStuckEx then - /- - When the configuration flag `isDefEqStuckEx` is set to true, - we want `isDefEq` to throw an exception whenever it tries to assign - a read-only metavariable. - This feature is useful for type class resolution where - we may want to notify the caller that the TC problem may be solveable - later after it assigns `?m`. - The method `DiscrTree.getUnify e` returns candidates `c` that may "unify" with `e`. - That is, `isDefEq c e` may return true. Now, consider `DiscrTree.getUnify d (HasAdd ?m)` - where `?m` is a read-only metavariable, and the discrimination tree contains the keys - `HadAdd Nat` and `HasAdd Int`. If `isDefEqStuckEx` is set to true, we must treat `?m` as - a regular metavariable here, otherwise we return the empty set of candidates. - This is incorrect because it is equivalent to saying that there is no solution even if - the caller assigns `?m` and try again. -/ - pure (Key.star, #[]) - else if (← isReadOnlyOrSyntheticOpaqueExprMVar mvarId) then + let e ← whnfEta e + match e.getAppFn with + | Expr.lit v _ => pure (Key.lit v, #[]) + | Expr.const c _ _ => + let nargs := e.getAppNumArgs + pure (Key.const c nargs, e.getAppRevArgs) + | Expr.fvar fvarId _ => + let nargs := e.getAppNumArgs + pure (Key.fvar fvarId nargs, e.getAppRevArgs) + | Expr.mvar mvarId _ => + if isMatch? then pure (Key.other, #[]) - else - pure (Key.star, #[]) -| _ => pure (Key.other, #[]) + else do + let ctx ← read + if ctx.config.isDefEqStuckEx then + /- + When the configuration flag `isDefEqStuckEx` is set to true, + we want `isDefEq` to throw an exception whenever it tries to assign + a read-only metavariable. + This feature is useful for type class resolution where + we may want to notify the caller that the TC problem may be solveable + later after it assigns `?m`. + The method `DiscrTree.getUnify e` returns candidates `c` that may "unify" with `e`. + That is, `isDefEq c e` may return true. Now, consider `DiscrTree.getUnify d (HasAdd ?m)` + where `?m` is a read-only metavariable, and the discrimination tree contains the keys + `HadAdd Nat` and `HasAdd Int`. If `isDefEqStuckEx` is set to true, we must treat `?m` as + a regular metavariable here, otherwise we return the empty set of candidates. + This is incorrect because it is equivalent to saying that there is no solution even if + the caller assigns `?m` and try again. -/ + pure (Key.star, #[]) + else if (← isReadOnlyOrSyntheticOpaqueExprMVar mvarId) then + pure (Key.other, #[]) + else + pure (Key.star, #[]) + | _ => pure (Key.other, #[]) private abbrev getMatchKeyArgs (e : Expr) : MetaM (Key × Array Expr) := -getKeyArgs e true + getKeyArgs e true private abbrev getUnifyKeyArgs (e : Expr) : MetaM (Key × Array Expr) := -getKeyArgs e false + getKeyArgs e false private partial def getMatchAux {α} : Array Expr → Trie α → Array α → MetaM (Array α) -| todo, Trie.node vs cs, result => - if todo.isEmpty then pure $ result ++ vs - else if cs.isEmpty then pure result - else do - let e := todo.back - let todo := todo.pop - let first := cs[0] /- Recall that `Key.star` is the minimal key -/ - let (k, args) ← getMatchKeyArgs e - /- We must always visit `Key.star` edges since they are wildcards. - Thus, `todo` is not used linearly when there is `Key.star` edge - and there is an edge for `k` and `k != Key.star`. -/ - let visitStarChild (result : Array α) : MetaM (Array α) := - if first.1 == Key.star then getMatchAux todo first.2 result else pure result - match k with - | Key.star => visitStarChild result - | _ => - match cs.binSearch (k, arbitrary _) (fun a b => a.1 < b.1) with - | none => visitStarChild result - | some c => - let result ← visitStarChild result - getMatchAux (todo ++ args) c.2 result + | todo, Trie.node vs cs, result => + if todo.isEmpty then pure $ result ++ vs + else if cs.isEmpty then pure result + else do + let e := todo.back + let todo := todo.pop + let first := cs[0] /- Recall that `Key.star` is the minimal key -/ + let (k, args) ← getMatchKeyArgs e + /- We must always visit `Key.star` edges since they are wildcards. + Thus, `todo` is not used linearly when there is `Key.star` edge + and there is an edge for `k` and `k != Key.star`. -/ + let visitStarChild (result : Array α) : MetaM (Array α) := + if first.1 == Key.star then getMatchAux todo first.2 result else pure result + match k with + | Key.star => visitStarChild result + | _ => + match cs.binSearch (k, arbitrary _) (fun a b => a.1 < b.1) with + | none => visitStarChild result + | some c => + let result ← visitStarChild result + getMatchAux (todo ++ args) c.2 result private def getStarResult {α} (d : DiscrTree α) : Array α := -let result : Array α := Array.mkEmpty initCapacity -match d.root.find? Key.star with -| none => result -| some (Trie.node vs _) => result ++ vs + let result : Array α := Array.mkEmpty initCapacity + match d.root.find? Key.star with + | none => result + | some (Trie.node vs _) => result ++ vs def getMatch {α} (d : DiscrTree α) (e : Expr) : MetaM (Array α) := -withReducible do - let result := getStarResult d - let (k, args) ← getMatchKeyArgs e - match k with - | Key.star => pure result - | _ => - match d.root.find? k with - | none => pure result - | some c => getMatchAux args c result + withReducible do + let result := getStarResult d + let (k, args) ← getMatchKeyArgs e + match k with + | Key.star => pure result + | _ => + match d.root.find? k with + | none => pure result + | some c => getMatchAux args c result private partial def getUnifyAux {α} : Nat → Array Expr → Trie α → (Array α) → MetaM (Array α) -| skip+1, todo, Trie.node vs cs, result => - if cs.isEmpty then pure result - else cs.foldlM (fun result ⟨k, c⟩ => getUnifyAux (skip + k.arity) todo c result) result -| 0, todo, Trie.node vs cs, result => do - if todo.isEmpty then pure (result ++ vs) - else if cs.isEmpty then pure result - else - let e := todo.back - let todo := todo.pop - let (k, args) ← getUnifyKeyArgs e - match k with - | Key.star => cs.foldlM (fun result ⟨k, c⟩ => getUnifyAux k.arity todo c result) result - | _ => - let first := cs[0] - let visitStarChild (result : Array α) : MetaM (Array α) := - if first.1 == Key.star then getUnifyAux 0 todo first.2 result else pure result - match cs.binSearch (k, arbitrary _) (fun a b => a.1 < b.1) with - | none => visitStarChild result - | some c => - let result ← visitStarChild result - getUnifyAux 0 (todo ++ args) c.2 result + | skip+1, todo, Trie.node vs cs, result => + if cs.isEmpty then pure result + else cs.foldlM (fun result ⟨k, c⟩ => getUnifyAux (skip + k.arity) todo c result) result + | 0, todo, Trie.node vs cs, result => do + if todo.isEmpty then pure (result ++ vs) + else if cs.isEmpty then pure result + else + let e := todo.back + let todo := todo.pop + let (k, args) ← getUnifyKeyArgs e + match k with + | Key.star => cs.foldlM (fun result ⟨k, c⟩ => getUnifyAux k.arity todo c result) result + | _ => + let first := cs[0] + let visitStarChild (result : Array α) : MetaM (Array α) := + if first.1 == Key.star then getUnifyAux 0 todo first.2 result else pure result + match cs.binSearch (k, arbitrary _) (fun a b => a.1 < b.1) with + | none => visitStarChild result + | some c => + let result ← visitStarChild result + getUnifyAux 0 (todo ++ args) c.2 result def getUnify {α} (d : DiscrTree α) (e : Expr) : MetaM (Array α) := -withReducible do - let (k, args) ← getUnifyKeyArgs e - match k with - | Key.star => d.root.foldlM (fun result k c => getUnifyAux k.arity #[] c result) #[] - | _ => - let result := getStarResult d - match d.root.find? k with - | none => pure result - | some c => getUnifyAux 0 args c result + withReducible do + let (k, args) ← getUnifyKeyArgs e + match k with + | Key.star => d.root.foldlM (fun result k c => getUnifyAux k.arity #[] c result) #[] + | _ => + let result := getStarResult d + match d.root.find? k with + | none => pure result + | some c => getUnifyAux 0 args c result end Lean.Meta.DiscrTree diff --git a/src/Lean/Meta/DiscrTreeTypes.lean b/src/Lean/Meta/DiscrTreeTypes.lean index be49d63382..1365276597 100644 --- a/src/Lean/Meta/DiscrTreeTypes.lean +++ b/src/Lean/Meta/DiscrTreeTypes.lean @@ -12,35 +12,35 @@ namespace Lean.Meta namespace DiscrTree inductive Key -| const : Name → Nat → Key -| fvar : FVarId → Nat → Key -| lit : Literal → Key -| star : Key -| other : Key + | const : Name → Nat → Key + | fvar : FVarId → Nat → Key + | lit : Literal → Key + | star : Key + | other : Key instance : Inhabited Key := ⟨Key.star⟩ protected def Key.hash : Key → USize -| Key.const n a => mixHash 5237 $ mixHash (hash n) (hash a) -| Key.fvar n a => mixHash 3541 $ mixHash (hash n) (hash a) -| Key.lit v => mixHash 1879 $ hash v -| Key.star => 7883 -| Key.other => 2411 + | Key.const n a => mixHash 5237 $ mixHash (hash n) (hash a) + | Key.fvar n a => mixHash 3541 $ mixHash (hash n) (hash a) + | Key.lit v => mixHash 1879 $ hash v + | Key.star => 7883 + | Key.other => 2411 instance : Hashable Key := ⟨Key.hash⟩ protected def Key.beq : Key → Key → Bool -| Key.const c₁ a₁, Key.const c₂ a₂ => c₁ == c₂ && a₁ == a₂ -| Key.fvar c₁ a₁, Key.fvar c₂ a₂ => c₁ == c₂ && a₁ == a₂ -| Key.lit v₁, Key.lit v₂ => v₁ == v₂ -| Key.star, Key.star => true -| Key.other, Key.other => true -| _, _ => false + | Key.const c₁ a₁, Key.const c₂ a₂ => c₁ == c₂ && a₁ == a₂ + | Key.fvar c₁ a₁, Key.fvar c₂ a₂ => c₁ == c₂ && a₁ == a₂ + | Key.lit v₁, Key.lit v₂ => v₁ == v₂ + | Key.star, Key.star => true + | Key.other, Key.other => true + | _, _ => false instance : HasBeq Key := ⟨Key.beq⟩ inductive Trie (α : Type) -| node (vs : Array α) (children : Array (Key × Trie α)) : Trie α + | node (vs : Array α) (children : Array (Key × Trie α)) : Trie α end DiscrTree @@ -48,6 +48,6 @@ open DiscrTree open Std (PersistentHashMap) structure DiscrTree (α : Type) := -(root : PersistentHashMap Key (Trie α) := {}) + (root : PersistentHashMap Key (Trie α) := {}) end Lean.Meta diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index 014be7cacf..d53248f8dd 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/src/Lean/Meta/ExprDefEq.lean @@ -23,66 +23,65 @@ namespace Lean.Meta ``` The left-hand side of the constraint above it not eta-reduced because `?m` is a metavariable. -/ private def isDefEqEta (a b : Expr) : DefEqM Bool := do -if a.isLambda && !b.isLambda then - let bType ← inferType b - let bType ← whnfD bType - match bType with - | Expr.forallE n d _ c => - let b' := mkLambda n c.binderInfo d (mkApp b (mkBVar 0)) - commitWhen $ Meta.isExprDefEqAux a b' - | _ => pure false -else - pure false + if a.isLambda && !b.isLambda then + let bType ← inferType b + let bType ← whnfD bType + match bType with + | Expr.forallE n d _ c => + let b' := mkLambda n c.binderInfo d (mkApp b (mkBVar 0)) + commitWhen $ Meta.isExprDefEqAux a b' + | _ => pure false + else + pure false /-- Support for `Lean.reduceBool` and `Lean.reduceNat` -/ def isDefEqNative (s t : Expr) : DefEqM LBool := do -let isDefEq (s t) : DefEqM LBool := toLBoolM $ Meta.isExprDefEqAux s t -let s? ← liftM $ reduceNative? s -let t? ← liftM $ reduceNative? t -match s?, t? with -| some s, some t => isDefEq s t -| some s, none => isDefEq s t -| none, some t => isDefEq s t -| none, none => pure LBool.undef - -/-- Support for reducing Nat basic operations. -/ -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 - let s? ← liftM $ reduceNat? s - let t? ← liftM $ reduceNat? t + let isDefEq (s t) : DefEqM LBool := toLBoolM $ Meta.isExprDefEqAux s t + let s? ← liftM $ reduceNative? s + let t? ← liftM $ reduceNative? t match s?, t? with | some s, some t => isDefEq s t | some s, none => isDefEq s t | none, some t => isDefEq s t | none, none => pure LBool.undef +/-- Support for reducing Nat basic operations. -/ +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 + let s? ← liftM $ reduceNat? s + let t? ← liftM $ reduceNat? t + match s?, t? with + | some s, some t => isDefEq s t + | some s, none => isDefEq s t + | none, some t => isDefEq s t + | none, none => pure LBool.undef + /-- Support for constraints of the form `("..." =?= String.mk cs)` -/ 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 - isDefEq s (toCtorIfLit t) -else - pure LBool.undef + 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 + isDefEq s (toCtorIfLit t) + else + pure LBool.undef /-- 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) : DefEqM Bool := do -match e.etaExpanded? with -| some (Expr.mvar mvarId _) => - if (← isReadOnlyOrSyntheticOpaqueExprMVar mvarId) then - pure false - else if (← isExprMVarAssigned mvarId) then - pure false - else - pure true -| _ => pure false - + match e.etaExpanded? with + | some (Expr.mvar mvarId _) => + if (← isReadOnlyOrSyntheticOpaqueExprMVar mvarId) then + pure false + else if (← isExprMVarAssigned mvarId) then + pure false + else + pure true + | _ => pure false /- First pass for `isDefEqArgs`. We unify explicit arguments, *and* easy cases @@ -115,64 +114,64 @@ match e.etaExpanded? with -/ private partial def isDefEqArgsFirstPass (paramInfo : Array ParamInfo) (args₁ args₂ : Array Expr) : DefEqM (Option (Array Nat)) := do -let rec loop (i : Nat) (postponed : Array Nat) := do - if h : i < paramInfo.size then - let info := paramInfo.get ⟨i, h⟩ - let a₁ := args₁[i] - let a₂ := args₂[i] - if info.implicit || info.instImplicit then - if (← isEtaUnassignedMVar a₁ <||> isEtaUnassignedMVar a₂) then - if (← Meta.isExprDefEqAux a₁ a₂) then - loop (i+1) postponed + let rec loop (i : Nat) (postponed : Array Nat) := do + if h : i < paramInfo.size then + let info := paramInfo.get ⟨i, h⟩ + let a₁ := args₁[i] + let a₂ := args₂[i] + if info.implicit || info.instImplicit then + if (← isEtaUnassignedMVar a₁ <||> isEtaUnassignedMVar a₂) then + if (← Meta.isExprDefEqAux a₁ a₂) then + loop (i+1) postponed + else + pure none else - pure none + loop (i+1) (postponed.push i) + else if (← Meta.isExprDefEqAux a₁ a₂) then + loop (i+1) postponed else - loop (i+1) (postponed.push i) - else if (← Meta.isExprDefEqAux a₁ a₂) then - loop (i+1) postponed + pure none else - pure none - else - pure (some postponed) -loop 0 #[] + pure (some postponed) + loop 0 #[] @[specialize] private def trySynthPending (e : Expr) : DefEqM Bool := do -let mvarId? ← getStuckMVar? e -match mvarId? with -| some mvarId => Meta.synthPending mvarId -| none => pure false + let mvarId? ← getStuckMVar? e + match mvarId? with + | some mvarId => Meta.synthPending mvarId + | none => pure false private partial def isDefEqArgs (f : Expr) (args₁ args₂ : Array Expr) : DefEqM Bool := -if h : args₁.size = args₂.size then do - let finfo ← liftM $ getFunInfoNArgs f args₁.size - let (some postponed) ← isDefEqArgsFirstPass finfo.paramInfo args₁ args₂ | pure false - let rec processOtherArgs (i : Nat) : DefEqM Bool := do - if h₁ : i < args₁.size then - let a₁ := args₁.get ⟨i, h₁⟩ - let a₂ := args₂.get ⟨i, Eq.subst h h₁⟩ - if (← Meta.isExprDefEqAux a₁ a₂) then - processOtherArgs (i+1) + if h : args₁.size = args₂.size then do + let finfo ← liftM $ getFunInfoNArgs f args₁.size + let (some postponed) ← isDefEqArgsFirstPass finfo.paramInfo args₁ args₂ | pure false + let rec processOtherArgs (i : Nat) : DefEqM Bool := do + if h₁ : i < args₁.size then + let a₁ := args₁.get ⟨i, h₁⟩ + let a₂ := args₂.get ⟨i, Eq.subst h h₁⟩ + if (← Meta.isExprDefEqAux a₁ a₂) then + processOtherArgs (i+1) + else + pure false else - pure false + pure true + if (← processOtherArgs finfo.paramInfo.size) then + postponed.allM fun i => do + /- Second pass: unify implicit arguments. + In the second pass, we make sure we are unfolding at + least non reducible definitions (default setting). -/ + let a₁ := args₁[i] + let a₂ := args₂[i] + let info := finfo.paramInfo[i] + if info.instImplicit then + trySynthPending a₁ + trySynthPending a₂ + pure () + withAtLeastTransparency TransparencyMode.default $ Meta.isExprDefEqAux a₁ a₂ else - pure true - if (← processOtherArgs finfo.paramInfo.size) then - postponed.allM fun i => do - /- Second pass: unify implicit arguments. - In the second pass, we make sure we are unfolding at - least non reducible definitions (default setting). -/ - let a₁ := args₁[i] - let a₂ := args₂[i] - let info := finfo.paramInfo[i] - if info.instImplicit then - trySynthPending a₁ - trySynthPending a₂ - pure () - withAtLeastTransparency TransparencyMode.default $ Meta.isExprDefEqAux a₁ a₂ + pure false else pure false -else - pure false /-- Check whether the types of the free variables at `fvars` are @@ -186,28 +185,27 @@ 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) (k : DefEqM Bool) : DefEqM Bool := -let rec loop (i : Nat) := do - if h : i < fvars.size then do - let fvar := fvars.get ⟨i, h⟩ - let fvarDecl ← getFVarLocalDecl fvar - let fvarType := fvarDecl.type - let d₂ := ds₂[i] - if (← Meta.isExprDefEqAux fvarType d₂) then - match (← isClass? fvarType) with - | some className => withNewLocalInstance className fvar $ loop (i+1) - | none => loop (i+1) + let rec loop (i : Nat) := do + if h : i < fvars.size then do + let fvar := fvars.get ⟨i, h⟩ + let fvarDecl ← getFVarLocalDecl fvar + let fvarType := fvarDecl.type + let d₂ := ds₂[i] + if (← Meta.isExprDefEqAux fvarType d₂) then + match (← isClass? fvarType) with + | some className => withNewLocalInstance className fvar $ loop (i+1) + | none => loop (i+1) + else + pure false else - pure false - else - k -loop 0 + k + loop 0 /- Auxiliary function for `isDefEqBinding` for handling binders `forall/fun`. 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 → DefEqM Bool -| lctx, fvars, e₁, e₂, ds₂ => +private partial def isDefEqBindingAux (lctx : LocalContext) (fvars : Array Expr) (e₁ e₂ : Expr) (ds₂ : Array Expr) : DefEqM Bool := let process (n : Name) (d₁ d₂ b₁ b₂ : Expr) : DefEqM Bool := do let d₁ := d₁.instantiateRev fvars let d₂ := d₂.instantiateRev fvars @@ -219,26 +217,26 @@ private partial def isDefEqBindingAux : LocalContext → Array Expr → Expr → | Expr.forallE n d₁ b₁ _, Expr.forallE _ d₂ b₂ _ => process n d₁ d₂ b₁ b₂ | Expr.lam n d₁ b₁ _, Expr.lam _ d₂ b₂ _ => process n d₁ d₂ b₁ b₂ | _, _ => - withReader (fun ctx => { ctx with lctx := lctx }) $ + withReader (fun ctx => { ctx with lctx := lctx }) do isDefEqBindingDomain fvars ds₂ $ Meta.isExprDefEqAux (e₁.instantiateRev fvars) (e₂.instantiateRev fvars) @[inline] private def isDefEqBinding (a b : Expr) : DefEqM Bool := do -let lctx ← getLCtx -isDefEqBindingAux lctx #[] a b #[] + let lctx ← getLCtx + isDefEqBindingAux lctx #[] a b #[] 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 - let mvarType ← inferType mvar - let vType ← inferType v - if (← withTransparency TransparencyMode.default $ Meta.isExprDefEqAux mvarType vType) then - trace[Meta.isDefEq.assign.final]! "{mvar} := {v}" - assignExprMVar mvar.mvarId! v - pure true - else - trace[Meta.isDefEq.assign.typeMismatch]! "{mvar} : {mvarType} := {v} : {vType}" - pure false + traceCtx `Meta.isDefEq.assign.checkTypes do + -- must check whether types are definitionally equal or not, before assigning and returning true + let mvarType ← inferType mvar + let vType ← inferType v + if (← withTransparency TransparencyMode.default $ Meta.isExprDefEqAux mvarType vType) then + trace[Meta.isDefEq.assign.final]! "{mvar} := {v}" + assignExprMVar mvar.mvarId! v + pure true + else + trace[Meta.isDefEq.assign.typeMismatch]! "{mvar} : {mvarType} := {v} : {vType}" + pure false /- Each metavariable is declared in a particular local context. @@ -399,7 +397,7 @@ traceCtx `Meta.isDefEq.assign.checkTypes do -/ def mkAuxMVar (lctx : LocalContext) (localInsts : LocalInstances) (type : Expr) (numScopeArgs : Nat := 0) : DefEqM Expr := do -mkFreshExprMVarAt lctx localInsts type MetavarKind.natural Name.anonymous numScopeArgs + mkFreshExprMVarAt lctx localInsts type MetavarKind.natural Name.anonymous numScopeArgs namespace CheckAssignment @@ -407,87 +405,88 @@ builtin_initialize checkAssignmentExceptionId : InternalExceptionId ← register builtin_initialize outOfScopeExceptionId : InternalExceptionId ← registerInternalExceptionId `outOfScope structure State := -(cache : ExprStructMap Expr := {}) + (cache : ExprStructMap Expr := {}) structure Context := -(mvarId : MVarId) -(mvarDecl : MetavarDecl) -(fvars : Array Expr) -(hasCtxLocals : Bool) -(rhs : Expr) + (mvarId : MVarId) + (mvarDecl : MetavarDecl) + (fvars : Array Expr) + (hasCtxLocals : Bool) + (rhs : Expr) abbrev CheckAssignmentM := ReaderT Context $ StateRefT State $ DefEqM def throwCheckAssignmentFailure {α} : CheckAssignmentM α := -throw $ Exception.internal checkAssignmentExceptionId + throw $ Exception.internal checkAssignmentExceptionId def throwOutOfScopeFVar {α} : CheckAssignmentM α := -throw $ Exception.internal outOfScopeExceptionId + throw $ Exception.internal outOfScopeExceptionId private def findCached? (e : Expr) : CheckAssignmentM (Option Expr) := do -return (← get).cache.find? e + return (← get).cache.find? e private def cache (e r : Expr) : CheckAssignmentM Unit := do -modify fun s => { s with cache := s.cache.insert e r } + modify fun s => { s with cache := s.cache.insert e r } -instance : MonadCache Expr Expr CheckAssignmentM := -{ findCached? := findCached?, cache := cache } +instance : MonadCache Expr Expr CheckAssignmentM := { + findCached? := findCached?, cache := cache +} @[inline] private def visit (f : Expr → CheckAssignmentM Expr) (e : Expr) : CheckAssignmentM Expr := -if !e.hasExprMVar && !e.hasFVar then pure e else checkCache e f + if !e.hasExprMVar && !e.hasFVar then pure e else checkCache e f private def addAssignmentInfo (msg : MessageData) : CheckAssignmentM MessageData := do -let ctx ← read -pure $ msg ++ " @ " ++ mkMVar ctx.mvarId ++ " " ++ ctx.fvars ++ " := " ++ ctx.rhs + let ctx ← read + return msg!" @ {mkMVar ctx.mvarId} {ctx.fvars} := {ctx.rhs}" @[specialize] def checkFVar (check : Expr → CheckAssignmentM Expr) (fvar : Expr) : CheckAssignmentM Expr := do -let ctxMeta ← readThe Meta.Context -let ctx ← read -if ctx.mvarDecl.lctx.containsFVar fvar then - pure fvar -else - let lctx := ctxMeta.lctx - match lctx.findFVar? fvar with - | some (LocalDecl.ldecl _ _ _ _ v _) => visit check v - | _ => - if ctx.fvars.contains fvar then pure fvar - else - traceM `Meta.isDefEq.assign.outOfScopeFVar $ addAssignmentInfo fvar - throwOutOfScopeFVar + let ctxMeta ← readThe Meta.Context + let ctx ← read + if ctx.mvarDecl.lctx.containsFVar fvar then + pure fvar + else + let lctx := ctxMeta.lctx + match lctx.findFVar? fvar with + | some (LocalDecl.ldecl _ _ _ _ v _) => visit check v + | _ => + if ctx.fvars.contains fvar then pure fvar + else + traceM `Meta.isDefEq.assign.outOfScopeFVar do addAssignmentInfo fvar + throwOutOfScopeFVar @[specialize] def checkMVar (check : Expr → CheckAssignmentM Expr) (mvar : Expr) : CheckAssignmentM Expr := do -let mvarId := mvar.mvarId! -let ctx ← read -let mctx ← getMCtx -if mvarId == ctx.mvarId then do - traceM `Meta.isDefEq.assign.occursCheck $ addAssignmentInfo "occurs check failed" - throwCheckAssignmentFailure -else match mctx.getExprAssignment? mvarId with - | some v => check v - | none => match mctx.findDecl? mvarId with - | none => liftM $ throwUnknownMVar mvarId - | some mvarDecl => - if ctx.hasCtxLocals then - throwCheckAssignmentFailure -- It is not a pattern, then we fail and fall back to FO unification - else if mvarDecl.lctx.isSubPrefixOf ctx.mvarDecl.lctx ctx.fvars then - /- The local context of `mvar` - free variables being abstracted is a subprefix of the metavariable being assigned. - We "substract" variables being abstracted because we use `elimMVarDeps` -/ - pure mvar - else if mvarDecl.depth != mctx.depth || mvarDecl.kind.isSyntheticOpaque then do - traceM `Meta.isDefEq.assign.readOnlyMVarWithBiggerLCtx $ addAssignmentInfo (mkMVar mvarId) - throwCheckAssignmentFailure - else do - let ctxMeta ← readThe Meta.Context - if ctxMeta.config.ctxApprox && ctx.mvarDecl.lctx.isSubPrefixOf mvarDecl.lctx then do - let mvarType ← check mvarDecl.type - /- Create an auxiliary metavariable with a smaller context and "checked" type. - Note that `mvarType` may be different from `mvarDecl.type`. Example: `mvarType` contains - a metavariable that we also need to reduce the context. -/ - let newMVar ← mkAuxMVar ctx.mvarDecl.lctx ctx.mvarDecl.localInstances mvarType mvarDecl.numScopeArgs - modifyThe Meta.State fun s => { s with mctx := s.mctx.assignExpr mvarId newMVar } - pure newMVar - else + let mvarId := mvar.mvarId! + let ctx ← read + let mctx ← getMCtx + if mvarId == ctx.mvarId then + traceM `Meta.isDefEq.assign.occursCheck $ addAssignmentInfo "occurs check failed" + throwCheckAssignmentFailure + else match mctx.getExprAssignment? mvarId with + | some v => check v + | none => match mctx.findDecl? mvarId with + | none => liftM $ throwUnknownMVar mvarId + | some mvarDecl => + if ctx.hasCtxLocals then + throwCheckAssignmentFailure -- It is not a pattern, then we fail and fall back to FO unification + else if mvarDecl.lctx.isSubPrefixOf ctx.mvarDecl.lctx ctx.fvars then + /- The local context of `mvar` - free variables being abstracted is a subprefix of the metavariable being assigned. + We "substract" variables being abstracted because we use `elimMVarDeps` -/ pure mvar + else if mvarDecl.depth != mctx.depth || mvarDecl.kind.isSyntheticOpaque then + traceM `Meta.isDefEq.assign.readOnlyMVarWithBiggerLCtx $ addAssignmentInfo (mkMVar mvarId) + throwCheckAssignmentFailure + else + let ctxMeta ← readThe Meta.Context + if ctxMeta.config.ctxApprox && ctx.mvarDecl.lctx.isSubPrefixOf mvarDecl.lctx then + let mvarType ← check mvarDecl.type + /- Create an auxiliary metavariable with a smaller context and "checked" type. + Note that `mvarType` may be different from `mvarDecl.type`. Example: `mvarType` contains + a metavariable that we also need to reduce the context. -/ + let newMVar ← mkAuxMVar ctx.mvarDecl.lctx ctx.mvarDecl.localInstances mvarType mvarDecl.numScopeArgs + modifyThe Meta.State fun s => { s with mctx := s.mctx.assignExpr mvarId newMVar } + pure newMVar + else + pure mvar /- Auxiliary function used to "fix" subterms of the form `?m x_1 ... x_n` where `x_i`s are free variables, @@ -496,61 +495,62 @@ else match mctx.getExprAssignment? mvarId with 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) : DefEqM Bool := do -let mvarType ← inferType mvar -forallBoundedTelescope mvarType numArgs fun xs _ => do - if xs.size != numArgs then pure false - else - let v ← mkLambdaFVars xs newMVar - checkTypesAndAssign mvar v + let mvarType ← inferType mvar + forallBoundedTelescope mvarType numArgs fun xs _ => do + if xs.size != numArgs then pure false + else + let v ← mkLambdaFVars xs newMVar + checkTypesAndAssign mvar v -partial def check : Expr → CheckAssignmentM Expr -| e@(Expr.mdata _ b _) => do return e.updateMData! (← visit check b) -| e@(Expr.proj _ _ s _) => do return e.updateProj! (← visit check s) -| e@(Expr.lam _ d b _) => do return e.updateLambdaE! (← visit check d) (← visit check b) -| e@(Expr.forallE _ d b _) => do return e.updateForallE! (← visit check d) (← visit check b) -| e@(Expr.letE _ t v b _) => do return e.updateLet! (← visit check t) (← visit check v) (← visit check b) -| e@(Expr.bvar _ _) => pure e -| e@(Expr.sort _ _) => pure e -| e@(Expr.const _ _ _) => pure e -| e@(Expr.lit _ _) => pure e -| e@(Expr.fvar _ _) => visit (checkFVar check) e -| e@(Expr.mvar _ _) => visit (checkMVar check) e -| Expr.localE _ _ _ _ => unreachable! -| e@(Expr.app _ _ _) => e.withApp fun f args => do - let ctxMeta ← readThe Meta.Context - if f.isMVar && ctxMeta.config.ctxApprox && args.all Expr.isFVar then - let f ← visit (checkMVar check) f - catchInternalId outOfScopeExceptionId - (do - let args ← args.mapM (visit check) - pure $ mkAppN f args) - (fun ex => do - if (← isDelayedAssigned f.mvarId!) then - throw ex - else - let eType ← inferType e - let mvarType ← check eType - /- Create an auxiliary metavariable with a smaller context and "checked" type, assign `?f := fun _ => ?newMVar` - Note that `mvarType` may be different from `eType`. -/ - let ctx ← read - let newMVar ← liftM $ mkAuxMVar ctx.mvarDecl.lctx ctx.mvarDecl.localInstances mvarType - if (← liftM $ assignToConstFun f args.size newMVar) then - pure newMVar +partial def check (e : Expr) : CheckAssignmentM Expr := do + match e with + | Expr.mdata _ b _ => return e.updateMData! (← visit check b) + | Expr.proj _ _ s _ => return e.updateProj! (← visit check s) + | Expr.lam _ d b _ => return e.updateLambdaE! (← visit check d) (← visit check b) + | Expr.forallE _ d b _ => return e.updateForallE! (← visit check d) (← visit check b) + | Expr.letE _ t v b _ => return e.updateLet! (← visit check t) (← visit check v) (← visit check b) + | Expr.bvar .. => return e + | Expr.sort .. => return e + | Expr.const .. => return e + | Expr.lit .. => return e + | Expr.fvar .. => visit (checkFVar check) e + | Expr.mvar .. => visit (checkMVar check) e + | Expr.localE .. => unreachable! + | Expr.app .. => e.withApp fun f args => do + let ctxMeta ← readThe Meta.Context + if f.isMVar && ctxMeta.config.ctxApprox && args.all Expr.isFVar then + let f ← visit (checkMVar check) f + catchInternalId outOfScopeExceptionId + (do + let args ← args.mapM (visit check) + pure $ mkAppN f args) + (fun ex => do + if (← isDelayedAssigned f.mvarId!) then + throw ex else - throw ex) - else - let f ← visit check f - let args ← args.mapM (visit check) - pure $ mkAppN f args + let eType ← inferType e + let mvarType ← check eType + /- Create an auxiliary metavariable with a smaller context and "checked" type, assign `?f := fun _ => ?newMVar` + Note that `mvarType` may be different from `eType`. -/ + let ctx ← read + let newMVar ← liftM $ mkAuxMVar ctx.mvarDecl.lctx ctx.mvarDecl.localInstances mvarType + if (← liftM $ assignToConstFun f args.size newMVar) then + pure newMVar + else + throw ex) + else + let f ← visit check f + let args ← args.mapM (visit check) + pure $ mkAppN f args @[inline] def run (x : CheckAssignmentM Expr) (mvarId : MVarId) (fvars : Array Expr) (hasCtxLocals : Bool) (v : Expr) : DefEqM (Option Expr) := do -let mvarDecl ← getMVarDecl mvarId -let ctx := { mvarId := mvarId, mvarDecl := mvarDecl, fvars := fvars, hasCtxLocals := hasCtxLocals, rhs := v : Context } -let x : CheckAssignmentM (Option Expr) := - catchInternalIds [outOfScopeExceptionId, checkAssignmentExceptionId] - (do let e ← x; pure $ some e) - (fun _ => pure none) -(x.run ctx).run' {} + let mvarDecl ← getMVarDecl mvarId + let ctx := { mvarId := mvarId, mvarDecl := mvarDecl, fvars := fvars, hasCtxLocals := hasCtxLocals, rhs := v : Context } + let x : CheckAssignmentM (Option Expr) := + catchInternalIds [outOfScopeExceptionId, checkAssignmentExceptionId] + (do let e ← x; pure $ some e) + (fun _ => pure none) + x.run ctx $.run' {} end CheckAssignment @@ -559,48 +559,48 @@ namespace CheckAssignmentQuick partial def check (hasCtxLocals ctxApprox : Bool) (mctx : MetavarContext) (lctx : LocalContext) (mvarDecl : MetavarDecl) (mvarId : MVarId) (fvars : Array Expr) (e : Expr) : Bool := -let rec visit (e : Expr) : Bool := - if !e.hasExprMVar && !e.hasFVar then - true - else match e with - | e@(Expr.mdata _ b _) => visit b - | e@(Expr.proj _ _ s _) => visit s - | e@(Expr.app f a _) => visit f && visit a - | e@(Expr.lam _ d b _) => visit d && visit b - | e@(Expr.forallE _ d b _) => visit d && visit b - | e@(Expr.letE _ t v b _) => visit t && visit v && visit b - | Expr.bvar .. => true - | Expr.sort .. => true - | Expr.const .. => true - | Expr.lit .. => true - | Expr.fvar fvarId .. => - if mvarDecl.lctx.contains fvarId then true - else match lctx.find? fvarId with - | some (LocalDecl.ldecl _ _ _ _ v _) => false -- need expensive CheckAssignment.check - | _ => - if fvars.any $ fun x => x.fvarId! == fvarId then true - else false -- We could throw an exception here, but we would have to use ExceptM. So, we let CheckAssignment.check do it - | e@(Expr.mvar mvarId' _) => do - match mctx.getExprAssignment? mvarId' with - | some _ => false -- use CheckAssignment.check to instantiate - | none => - if mvarId' == mvarId then false -- occurs check failed, use CheckAssignment.check to throw exception - else match mctx.findDecl? mvarId' with - | none => false - | some mvarDecl' => - if hasCtxLocals then false -- use CheckAssignment.check - else if mvarDecl'.lctx.isSubPrefixOf mvarDecl.lctx fvars then true - else if mvarDecl'.depth != mctx.depth || mvarDecl'.kind.isSyntheticOpaque then false -- use CheckAssignment.check - else if ctxApprox && mvarDecl.lctx.isSubPrefixOf mvarDecl'.lctx then false -- use CheckAssignment.check - else true - | Expr.localE .. => unreachable! -visit e + let rec visit (e : Expr) : Bool := + if !e.hasExprMVar && !e.hasFVar then + true + else match e with + | Expr.mdata _ b _ => visit b + | Expr.proj _ _ s _ => visit s + | Expr.app f a _ => visit f && visit a + | Expr.lam _ d b _ => visit d && visit b + | Expr.forallE _ d b _ => visit d && visit b + | Expr.letE _ t v b _ => visit t && visit v && visit b + | Expr.bvar .. => true + | Expr.sort .. => true + | Expr.const .. => true + | Expr.lit .. => true + | Expr.fvar fvarId .. => + if mvarDecl.lctx.contains fvarId then true + else match lctx.find? fvarId with + | some (LocalDecl.ldecl _ _ _ _ v _) => false -- need expensive CheckAssignment.check + | _ => + if fvars.any $ fun x => x.fvarId! == fvarId then true + else false -- We could throw an exception here, but we would have to use ExceptM. So, we let CheckAssignment.check do it + | Expr.mvar mvarId' _ => + match mctx.getExprAssignment? mvarId' with + | some _ => false -- use CheckAssignment.check to instantiate + | none => + if mvarId' == mvarId then false -- occurs check failed, use CheckAssignment.check to throw exception + else match mctx.findDecl? mvarId' with + | none => false + | some mvarDecl' => + if hasCtxLocals then false -- use CheckAssignment.check + else if mvarDecl'.lctx.isSubPrefixOf mvarDecl.lctx fvars then true + else if mvarDecl'.depth != mctx.depth || mvarDecl'.kind.isSyntheticOpaque then false -- use CheckAssignment.check + else if ctxApprox && mvarDecl.lctx.isSubPrefixOf mvarDecl'.lctx then false -- use CheckAssignment.check + else true + | Expr.localE .. => unreachable! + visit e end CheckAssignmentQuick -- See checkAssignment def checkAssignmentAux (mvarId : MVarId) (fvars : Array Expr) (hasCtxLocals : Bool) (v : Expr) : DefEqM (Option Expr) := do -CheckAssignment.run (CheckAssignment.check v) mvarId fvars hasCtxLocals v + CheckAssignment.run (CheckAssignment.check v) mvarId fvars hasCtxLocals v /-- Auxiliary function for handling constraints of the form `?m a₁ ... aₙ =?= v`. @@ -612,23 +612,23 @@ CheckAssignment.run (CheckAssignment.check v) mvarId fvars hasCtxLocals v 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) : DefEqM (Option Expr) := do -if !v.hasExprMVar && !v.hasFVar then - pure (some v) -else - let mvarDecl ← getMVarDecl mvarId - let hasCtxLocals := fvars.any $ fun fvar => mvarDecl.lctx.containsFVar fvar - let ctx ← read - let mctx ← getMCtx - if CheckAssignmentQuick.check hasCtxLocals ctx.config.ctxApprox mctx ctx.lctx mvarDecl mvarId fvars v then + if !v.hasExprMVar && !v.hasFVar then pure (some v) else - let v ← instantiateMVars v - checkAssignmentAux mvarId fvars hasCtxLocals v + let mvarDecl ← getMVarDecl mvarId + let hasCtxLocals := fvars.any $ fun fvar => mvarDecl.lctx.containsFVar fvar + let ctx ← read + let mctx ← getMCtx + if CheckAssignmentQuick.check hasCtxLocals ctx.config.ctxApprox mctx ctx.lctx mvarDecl mvarId fvars v then + pure (some v) + else + let v ← instantiateMVars v + checkAssignmentAux mvarId fvars hasCtxLocals v 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 + match v with + | Expr.app f a _ => Meta.isExprDefEqAux args.back a <&&> Meta.isExprDefEqAux (mkAppRange mvar 0 (args.size - 1) args) f + | _ => pure false /- Auxiliary method for applying first-order unification. It is an approximation. @@ -647,170 +647,170 @@ match v with def ITactic := Tactic Unit -/ private partial def processAssignmentFOApprox (mvar : Expr) (args : Array Expr) (v : Expr) : DefEqM Bool := -let rec loop (v : Expr) := do - let cfg ← getConfig - if !cfg.foApprox then - pure false - else - trace[Meta.isDefEq.foApprox]! "{mvar} {args} := {v}" - if (← commitWhen $ processAssignmentFOApproxAux mvar args v) then - pure true + let rec loop (v : Expr) := do + let cfg ← getConfig + if !cfg.foApprox then + pure false else - match (← unfoldDefinition? v) with - | none => pure false - | some v => loop v -loop v + trace[Meta.isDefEq.foApprox]! "{mvar} {args} := {v}" + if (← commitWhen $ processAssignmentFOApproxAux mvar args v) then + pure true + else + match (← unfoldDefinition? v) with + | none => pure false + | some v => loop v + loop v private partial def simpAssignmentArgAux : Expr → DefEqM Expr -| Expr.mdata _ e _ => simpAssignmentArgAux e -| e@(Expr.fvar fvarId _) => do - let decl ← getLocalDecl fvarId - match decl.value? with - | some value => simpAssignmentArgAux value - | _ => pure e -| e => pure e + | Expr.mdata _ e _ => simpAssignmentArgAux e + | e@(Expr.fvar fvarId _) => do + let decl ← getLocalDecl fvarId + match decl.value? with + | some value => simpAssignmentArgAux value + | _ => pure e + | e => pure e /- 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) : DefEqM Expr := do -let arg ← if arg.getAppFn.hasExprMVar then instantiateMVars arg else pure arg -simpAssignmentArgAux arg + let arg ← if arg.getAppFn.hasExprMVar then instantiateMVars arg else pure arg + simpAssignmentArgAux arg /- Assign `mvar := fun a_1 ... a_{numArgs} => v`. We use it at `processConstApprox` and `isDefEqMVarSelf` -/ private def assignConst (mvar : Expr) (numArgs : Nat) (v : Expr) : DefEqM Bool := do -let mvarDecl ← getMVarDecl mvar.mvarId! -forallBoundedTelescope mvarDecl.type numArgs fun xs _ => do - if xs.size != numArgs then - pure false - else - let v ← mkLambdaFVars xs v - trace[Meta.isDefEq.constApprox]! "{mvar} := {v}" - checkTypesAndAssign mvar v + let mvarDecl ← getMVarDecl mvar.mvarId! + forallBoundedTelescope mvarDecl.type numArgs fun xs _ => do + if xs.size != numArgs then + pure false + else + let v ← mkLambdaFVars xs v + trace[Meta.isDefEq.constApprox]! "{mvar} := {v}" + checkTypesAndAssign mvar v private def processConstApprox (mvar : Expr) (numArgs : Nat) (v : Expr) : DefEqM Bool := do -let cfg ← getConfig -let mvarId := mvar.mvarId! -let mvarDecl ← getMVarDecl mvarId -if mvarDecl.numScopeArgs == numArgs || cfg.constApprox then - match (← checkAssignment mvarId #[] v) with - | none => pure false - | some v => assignConst mvar numArgs v -else - pure false + let cfg ← getConfig + let mvarId := mvar.mvarId! + let mvarDecl ← getMVarDecl mvarId + if mvarDecl.numScopeArgs == numArgs || cfg.constApprox then + match (← checkAssignment mvarId #[] v) with + | none => pure false + | some v => assignConst mvar numArgs v + else + pure false /-- Tries to solve `?m a₁ ... aₙ =?= v` by assigning `?m`. It assumes `?m` is unassigned. -/ private partial def processAssignment (mvarApp : Expr) (v : Expr) : DefEqM Bool := -traceCtx `Meta.isDefEq.assign do - trace[Meta.isDefEq.assign]! "{mvarApp} := {v}" - let mvar := mvarApp.getAppFn - let mvarDecl ← getMVarDecl mvar.mvarId! - let rec process (i : Nat) (args : Array Expr) (v : Expr) := do - let cfg ← getConfig - let useFOApprox (args : Array Expr) : DefEqM Bool := - processAssignmentFOApprox mvar args v <||> processConstApprox mvar args.size v - if h : i < args.size then - let arg := args.get ⟨i, h⟩ - let arg ← simpAssignmentArg arg - let args := args.set ⟨i, h⟩ arg - match arg with - | Expr.fvar fvarId _ => - if args.anyRange 0 i (fun prevArg => prevArg == arg) then + traceCtx `Meta.isDefEq.assign do + trace[Meta.isDefEq.assign]! "{mvarApp} := {v}" + let mvar := mvarApp.getAppFn + let mvarDecl ← getMVarDecl mvar.mvarId! + let rec process (i : Nat) (args : Array Expr) (v : Expr) := do + let cfg ← getConfig + let useFOApprox (args : Array Expr) : DefEqM Bool := + processAssignmentFOApprox mvar args v <||> processConstApprox mvar args.size v + if h : i < args.size then + let arg := args.get ⟨i, h⟩ + let arg ← simpAssignmentArg arg + let args := args.set ⟨i, h⟩ arg + match arg with + | Expr.fvar fvarId _ => + if args.anyRange 0 i (fun prevArg => prevArg == arg) then + useFOApprox args + else if mvarDecl.lctx.contains fvarId && !cfg.quasiPatternApprox then + useFOApprox args + else + process (i+1) args v + | _ => useFOApprox args - else if mvarDecl.lctx.contains fvarId && !cfg.quasiPatternApprox then + else + let v ← instantiateMVars v -- enforce A4 + if v.getAppFn == mvar then + -- using A6 useFOApprox args else - process (i+1) args v - | _ => - useFOApprox args - else - let v ← instantiateMVars v -- enforce A4 - if v.getAppFn == mvar then - -- using A6 - useFOApprox args - else - let mvarId := mvar.mvarId! - match (← checkAssignment mvarId args v) with - | none => useFOApprox args - | some v => do - trace[Meta.isDefEq.assign.beforeMkLambda]! "{mvar} {args} := {v}" - let v ← mkLambdaFVars args v - 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 -/ - if (← isTypeCorrect v) then - checkTypesAndAssign mvar v + let mvarId := mvar.mvarId! + match (← checkAssignment mvarId args v) with + | none => useFOApprox args + | some v => do + trace[Meta.isDefEq.assign.beforeMkLambda]! "{mvar} {args} := {v}" + let v ← mkLambdaFVars args v + 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 -/ + if (← isTypeCorrect v) then + checkTypesAndAssign mvar v + else + trace[Meta.isDefEq.assign.typeError]! "{mvar} := {v}" + useFOApprox args else - trace[Meta.isDefEq.assign.typeError]! "{mvar} := {v}" - useFOApprox args - else - checkTypesAndAssign mvar v - process 0 mvarApp.getAppArgs v + checkTypesAndAssign mvar v + process 0 mvarApp.getAppArgs v private def isDeltaCandidate? (t : Expr) : DefEqM (Option ConstantInfo) := -match t.getAppFn with -| Expr.const c _ _ => liftM $ getConst? c -| _ => pure none + match t.getAppFn with + | Expr.const c _ _ => liftM $ getConst? c + | _ => pure none /-- Auxiliary method for isDefEqDelta -/ private def isListLevelDefEq (us vs : List Level) : DefEqM LBool := -toLBoolM $ isListLevelDefEqAux us vs + toLBoolM $ isListLevelDefEqAux us vs /-- Auxiliary method for isDefEqDelta -/ private def isDefEqLeft (fn : Name) (t s : Expr) : DefEqM LBool := do -trace[Meta.isDefEq.delta.unfoldLeft]! fn -toLBoolM $ Meta.isExprDefEqAux t s + trace[Meta.isDefEq.delta.unfoldLeft]! fn + toLBoolM $ Meta.isExprDefEqAux t s /-- Auxiliary method for isDefEqDelta -/ private def isDefEqRight (fn : Name) (t s : Expr) : DefEqM LBool := do -trace[Meta.isDefEq.delta.unfoldRight]! fn -toLBoolM $ Meta.isExprDefEqAux t s + trace[Meta.isDefEq.delta.unfoldRight]! fn + toLBoolM $ Meta.isExprDefEqAux t s /-- Auxiliary method for isDefEqDelta -/ private def isDefEqLeftRight (fn : Name) (t s : Expr) : DefEqM LBool := do -trace[Meta.isDefEq.delta.unfoldLeftRight]! fn -toLBoolM $ Meta.isExprDefEqAux t s + 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) : DefEqM Bool := -let tFn := t.getAppFn -let sFn := s.getAppFn -traceCtx `Meta.isDefEq.delta do - commitWhen do - let b ← isDefEqArgs tFn t.getAppArgs s.getAppArgs - <&&> - isListLevelDefEqAux tFn.constLevels! sFn.constLevels! - unless b do - trace[Meta.isDefEq.delta]! "heuristic failed {t} =?= {s}" - pure b + let tFn := t.getAppFn + let sFn := s.getAppFn + traceCtx `Meta.isDefEq.delta do + commitWhen do + let b ← isDefEqArgs tFn t.getAppArgs s.getAppArgs + <&&> + isListLevelDefEqAux tFn.constLevels! sFn.constLevels! + unless b do + trace[Meta.isDefEq.delta]! "heuristic failed {t} =?= {s}" + pure b /-- Auxiliary method for isDefEqDelta -/ private abbrev unfold {α} (e : Expr) (failK : DefEqM α) (successK : Expr → DefEqM α) : DefEqM α := do -match (← unfoldDefinition? e) with -| some e => successK e -| none => failK + match (← unfoldDefinition? e) with + | some e => successK e + | none => failK /-- Auxiliary method for isDefEqDelta -/ private def unfoldBothDefEq (fn : Name) (t s : Expr) : DefEqM LBool := do -match t, s with -| Expr.const _ ls₁ _, Expr.const _ ls₂ _ => isListLevelDefEq ls₁ ls₂ -| Expr.app _ _ _, Expr.app _ _ _ => - if (← tryHeuristic t s) then - pure LBool.true - else - unfold t - (unfold s (pure LBool.false) (fun s => isDefEqRight fn t s)) - (fun t => unfold s (isDefEqLeft fn t s) (fun s => isDefEqLeftRight fn t s)) -| _, _ => pure LBool.false + match t, s with + | Expr.const _ ls₁ _, Expr.const _ ls₂ _ => isListLevelDefEq ls₁ ls₂ + | Expr.app _ _ _, Expr.app _ _ _ => + if (← tryHeuristic t s) then + pure LBool.true + else + unfold t + (unfold s (pure LBool.false) (fun s => isDefEqRight fn t s)) + (fun t => unfold s (isDefEqLeft fn t s) (fun s => isDefEqLeftRight fn t s)) + | _, _ => pure LBool.false private def sameHeadSymbol (t s : Expr) : Bool := -match t.getAppFn, s.getAppFn with -| Expr.const c₁ _ _, Expr.const c₂ _ _ => true -| _, _ => false + match t.getAppFn, s.getAppFn with + | Expr.const c₁ _ _, Expr.const c₂ _ _ => true + | _, _ => false /-- - If headSymbol (unfold t) == headSymbol s, then unfold t @@ -819,21 +819,21 @@ match t.getAppFn, s.getAppFn with Auxiliary method for isDefEqDelta -/ 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 - (fun s => isDefEqRight sInfo.name t s)) - (fun tNew => - if sameHeadSymbol tNew s then - isDefEqLeft tInfo.name tNew s - else - unfold s - (isDefEqLeft tInfo.name tNew s) - (fun sNew => - if sameHeadSymbol t sNew then - isDefEqRight sInfo.name t sNew - else - isDefEqLeftRight tInfo.name tNew sNew)) + unfold t + (unfold s + (pure LBool.undef) -- `t` and `s` failed to be unfolded + (fun s => isDefEqRight sInfo.name t s)) + (fun tNew => + if sameHeadSymbol tNew s then + isDefEqLeft tInfo.name tNew s + else + unfold s + (isDefEqLeft tInfo.name tNew s) + (fun sNew => + if sameHeadSymbol t sNew then + isDefEqRight sInfo.name t sNew + else + isDefEqLeftRight tInfo.name tNew sNew)) /-- If `t` and `s` do not contain metavariables, then use kernel definitional equality heuristics. @@ -841,17 +841,17 @@ unfold t Auxiliary method for isDefEqDelta -/ 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. -/ - if tInfo.hints.lt sInfo.hints then - unfold t (unfoldComparingHeadsDefEq tInfo sInfo t s) $ fun t => isDefEqLeft tInfo.name t s - else if sInfo.hints.lt tInfo.hints then - unfold s (unfoldComparingHeadsDefEq tInfo sInfo t s) $ fun s => isDefEqRight sInfo.name t s + if !t.hasExprMVar && !s.hasExprMVar then + /- If `t` and `s` do not contain metavariables, + we simulate strategy used in the kernel. -/ + if tInfo.hints.lt sInfo.hints then + unfold t (unfoldComparingHeadsDefEq tInfo sInfo t s) $ fun t => isDefEqLeft tInfo.name t s + else if sInfo.hints.lt tInfo.hints then + unfold s (unfoldComparingHeadsDefEq tInfo sInfo t s) $ fun s => isDefEqRight sInfo.name t s + else + unfoldComparingHeadsDefEq tInfo sInfo t s else unfoldComparingHeadsDefEq tInfo sInfo t s -else - unfoldComparingHeadsDefEq tInfo sInfo t s /-- When `TransparencyMode` is set to `default` or `all`. @@ -862,17 +862,17 @@ else Auxiliary method for isDefEqDelta -/ private def unfoldReducibeDefEq (tInfo sInfo : ConstantInfo) (t s : Expr) : DefEqM LBool := do -if (← shouldReduceReducibleOnly) then - unfoldDefEq tInfo sInfo t s -else - let tReducible ← liftM $ Meta.isReducible tInfo.name - let 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 - unfold s (unfoldDefEq tInfo sInfo t s) fun s => isDefEqRight sInfo.name t s - else + if (← shouldReduceReducibleOnly) then unfoldDefEq tInfo sInfo t s + else + let tReducible ← liftM $ Meta.isReducible tInfo.name + let 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 + unfold s (unfoldDefEq tInfo sInfo t s) fun s => isDefEqRight sInfo.name t s + else + unfoldDefEq tInfo sInfo t s /-- If `t` is a projection function application and `s` is not ==> `isDefEqRight t (unfold s)` @@ -882,15 +882,15 @@ else Auxiliary method for isDefEqDelta -/ private def unfoldNonProjFnDefEq (tInfo sInfo : ConstantInfo) (t s : Expr) : DefEqM LBool := do -let env ← getEnv -let tProj? := env.isProjectionFn tInfo.name -let sProj? := env.isProjectionFn sInfo.name -if tProj? && !sProj? then - unfold s (unfoldDefEq tInfo sInfo t s) $ fun s => isDefEqRight sInfo.name t s -else if !tProj? && sProj? then - unfold t (unfoldDefEq tInfo sInfo t s) $ fun t => isDefEqLeft tInfo.name t s -else - unfoldReducibeDefEq tInfo sInfo t s + let env ← getEnv + let tProj? := env.isProjectionFn tInfo.name + let sProj? := env.isProjectionFn sInfo.name + if tProj? && !sProj? then + unfold s (unfoldDefEq tInfo sInfo t s) $ fun s => isDefEqRight sInfo.name t s + else if !tProj? && sProj? then + unfold t (unfoldDefEq tInfo sInfo t s) $ fun t => isDefEqLeft tInfo.name t s + else + unfoldReducibeDefEq tInfo sInfo t s /-- isDefEq by lazy delta reduction. @@ -914,222 +914,221 @@ else 11- Otherwise, unfold `t` and `s` and continue. Remark: 9&10&11 are implemented by `unfoldComparingHeadsDefEq` -/ private def isDefEqDelta (t s : Expr) : DefEqM LBool := do -let tInfo? ← isDeltaCandidate? t.getAppFn -let sInfo? ← isDeltaCandidate? s.getAppFn -match tInfo?, sInfo? with -| none, none => pure LBool.undef -| some tInfo, none => unfold t (pure LBool.undef) fun t => isDefEqLeft tInfo.name t s -| none, some sInfo => unfold s (pure LBool.undef) fun s => isDefEqRight sInfo.name t s -| some tInfo, some sInfo => - if tInfo.name == sInfo.name then - unfoldBothDefEq tInfo.name t s - else - unfoldNonProjFnDefEq tInfo sInfo t s + let tInfo? ← isDeltaCandidate? t.getAppFn + let sInfo? ← isDeltaCandidate? s.getAppFn + match tInfo?, sInfo? with + | none, none => pure LBool.undef + | some tInfo, none => unfold t (pure LBool.undef) fun t => isDefEqLeft tInfo.name t s + | none, some sInfo => unfold s (pure LBool.undef) fun s => isDefEqRight sInfo.name t s + | some tInfo, some sInfo => + if tInfo.name == sInfo.name then + unfoldBothDefEq tInfo.name t s + else + unfoldNonProjFnDefEq tInfo sInfo t s private def isAssigned : Expr → DefEqM Bool -| Expr.mvar mvarId _ => isExprMVarAssigned mvarId -| _ => pure false + | Expr.mvar mvarId _ => isExprMVarAssigned mvarId + | _ => pure false private def isDelayedAssignedHead (tFn : Expr) (t : Expr) : DefEqM Bool := do -match tFn with -| Expr.mvar mvarId _ => - if (← isDelayedAssigned mvarId) then - let tNew ← instantiateMVars t - pure $ tNew != t - else - pure false -| _ => pure false + match tFn with + | Expr.mvar mvarId _ => + if (← isDelayedAssigned mvarId) then + let tNew ← instantiateMVars t + pure $ tNew != t + else + pure false + | _ => pure false private def isSynthetic : Expr → DefEqM Bool -| Expr.mvar mvarId _ => do - let mvarDecl ← getMVarDecl mvarId - match mvarDecl.kind with - | MetavarKind.synthetic => pure true - | MetavarKind.syntheticOpaque => pure true - | MetavarKind.natural => pure false -| _ => pure false + | Expr.mvar mvarId _ => do + let mvarDecl ← getMVarDecl mvarId + match mvarDecl.kind with + | MetavarKind.synthetic => pure true + | MetavarKind.syntheticOpaque => pure true + | MetavarKind.natural => pure false + | _ => pure false private def isAssignable : Expr → DefEqM Bool -| Expr.mvar mvarId _ => do let b ← isReadOnlyOrSyntheticOpaqueExprMVar mvarId; pure (!b) -| _ => pure false + | Expr.mvar mvarId _ => do let b ← isReadOnlyOrSyntheticOpaqueExprMVar mvarId; pure (!b) + | _ => pure false private def etaEq (t s : Expr) : Bool := -match t.etaExpanded? with -| some t => t == s -| none => false + match t.etaExpanded? with + | some t => t == s + | none => false private def isLetFVar (fvarId : FVarId) : DefEqM Bool := do -let decl ← getLocalDecl fvarId -pure decl.isLet + let decl ← getLocalDecl fvarId + pure decl.isLet private def isDefEqProofIrrel (t s : Expr) : DefEqM LBool := do -let status ← isProofQuick t -match status with -| LBool.false => - pure LBool.undef -| LBool.true => - let tType ← inferType t - let sType ← inferType s - toLBoolM $ Meta.isExprDefEqAux tType sType -| LBool.undef => - let tType ← inferType t - if (← isProp tType) then + let status ← isProofQuick t + match status with + | LBool.false => + pure LBool.undef + | LBool.true => + let tType ← inferType t let sType ← inferType s toLBoolM $ Meta.isExprDefEqAux tType sType - else - pure LBool.undef + | LBool.undef => + let tType ← inferType t + if (← isProp tType) then + let sType ← inferType s + toLBoolM $ Meta.isExprDefEqAux tType sType + else + pure LBool.undef /- Try to solve constraint of the form `?m args₁ =?= ?m args₂`. - First try to unify `args₁` and `args₂`, and return true if successful - Otherwise, try to assign `?m` to a constant function of the form `fun x_1 ... x_n => ?n` where `?n` is a fresh metavariable. See `processConstApprox`. -/ private def isDefEqMVarSelf (mvar : Expr) (args₁ args₂ : Array Expr) : DefEqM Bool := do -if args₁.size != args₂.size then - pure false -else if (← isDefEqArgs mvar args₁ args₂) then - pure true -else if !(← isAssignable mvar) then - pure false -else - let cfg ← getConfig - let mvarId := mvar.mvarId! - let mvarDecl ← getMVarDecl mvarId - if mvarDecl.numScopeArgs == args₁.size || cfg.constApprox then - let type ← inferType (mkAppN mvar args₁) - let auxMVar ← mkAuxMVar mvarDecl.lctx mvarDecl.localInstances type - assignConst mvar args₁.size auxMVar - else + if args₁.size != args₂.size then pure false + else if (← isDefEqArgs mvar args₁ args₂) then + pure true + else if !(← isAssignable mvar) then + pure false + else + let cfg ← getConfig + let mvarId := mvar.mvarId! + let mvarDecl ← getMVarDecl mvarId + if mvarDecl.numScopeArgs == args₁.size || cfg.constApprox then + let type ← inferType (mkAppN mvar args₁) + let auxMVar ← mkAuxMVar mvarDecl.lctx mvarDecl.localInstances type + assignConst mvar args₁.size auxMVar + else + pure false /- Remove unnecessary let-decls -/ private def consumeLet : Expr → Expr -| e@(Expr.letE _ _ _ b _) => if b.hasLooseBVars then e else consumeLet b -| e => e + | e@(Expr.letE _ _ _ b _) => if b.hasLooseBVars then e else consumeLet b + | e => e mutual private partial def isDefEqQuick (t s : Expr) : DefEqM LBool := -let t := consumeLet t -let s := consumeLet s -match t, s with -| 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 -| t@(Expr.forallE _ _ _ _), s@(Expr.forallE _ _ _ _) => if t == s then pure LBool.true else toLBoolM $ isDefEqBinding t s -| Expr.mdata _ t _, s => isDefEqQuick t s -| t, Expr.mdata _ s _ => isDefEqQuick t s -| t@(Expr.fvar fvarId₁ _), s@(Expr.fvar fvarId₂ _) => do - if (← isLetFVar fvarId₁ <||> isLetFVar fvarId₂) then - pure LBool.undef - else if fvarId₁ == fvarId₂ then - pure LBool.true - else - isDefEqProofIrrel t s -| t, s => - isDefEqQuickOther t s + let t := consumeLet t + let s := consumeLet s + match t, s with + | 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 + | t@(Expr.forallE _ _ _ _), s@(Expr.forallE _ _ _ _) => if t == s then pure LBool.true else toLBoolM $ isDefEqBinding t s + | Expr.mdata _ t _, s => isDefEqQuick t s + | t, Expr.mdata _ s _ => isDefEqQuick t s + | t@(Expr.fvar fvarId₁ _), s@(Expr.fvar fvarId₂ _) => do + if (← isLetFVar fvarId₁ <||> isLetFVar fvarId₂) then + pure LBool.undef + else if fvarId₁ == fvarId₂ then + pure LBool.true + else + isDefEqProofIrrel t s + | t, s => + isDefEqQuickOther t s private partial def isDefEqQuickOther (t s : Expr) : DefEqM LBool := do -if t == s then - pure LBool.true -else if etaEq t s || etaEq s t then - pure LBool.true -- t =?= (fun xs => t xs) -else - let tFn := t.getAppFn - let sFn := s.getAppFn - if !tFn.isMVar && !sFn.isMVar then - pure LBool.undef - else if (← isAssigned tFn) then - let t ← instantiateMVars t - isDefEqQuick t s - else if (← isAssigned sFn) then - let s ← instantiateMVars s - isDefEqQuick t s - else if (← isDelayedAssignedHead tFn t) then - let t ← instantiateMVars t - isDefEqQuick t s - else if (← isDelayedAssignedHead sFn s) then - let s ← instantiateMVars s - isDefEqQuick t s - else if (← isSynthetic tFn <&&> trySynthPending tFn) then - let t ← instantiateMVars t - isDefEqQuick t s - else if (← isSynthetic sFn <&&> trySynthPending sFn) then - let s ← instantiateMVars s - isDefEqQuick t s - else if tFn.isMVar && sFn.isMVar && tFn == sFn then - Bool.toLBool <$> isDefEqMVarSelf tFn t.getAppArgs s.getAppArgs + if t == s then + pure LBool.true + else if etaEq t s || etaEq s t then + pure LBool.true -- t =?= (fun xs => t xs) else - let tAssign? ← isAssignable tFn - let sAssign? ← isAssignable sFn - let assignableMsg (b : Bool) := if b then "[assignable]" else "[nonassignable]" - trace[Meta.isDefEq]! "{t} {assignableMsg tAssign?} =?= {s} {assignableMsg sAssign?}" - let assign (t s : Expr) : DefEqM LBool := toLBoolM $ processAssignment t s - if tAssign? && !sAssign? then - toLBoolM $ processAssignment t s - else if !tAssign? && sAssign? then - toLBoolM $ processAssignment s t - else if !tAssign? && !sAssign? then - if tFn.isMVar || sFn.isMVar then - let ctx ← read - if ctx.config.isDefEqStuckEx then do - trace[Meta.isDefEq.stuck]! "{t} =?= {s}" - Meta.throwIsDefEqStuck - else - pure LBool.false - else - pure LBool.undef + let tFn := t.getAppFn + let sFn := s.getAppFn + if !tFn.isMVar && !sFn.isMVar then + pure LBool.undef + else if (← isAssigned tFn) then + let t ← instantiateMVars t + isDefEqQuick t s + else if (← isAssigned sFn) then + let s ← instantiateMVars s + isDefEqQuick t s + else if (← isDelayedAssignedHead tFn t) then + let t ← instantiateMVars t + isDefEqQuick t s + else if (← isDelayedAssignedHead sFn s) then + let s ← instantiateMVars s + isDefEqQuick t s + else if (← isSynthetic tFn <&&> trySynthPending tFn) then + let t ← instantiateMVars t + isDefEqQuick t s + else if (← isSynthetic sFn <&&> trySynthPending sFn) then + let s ← instantiateMVars s + isDefEqQuick t s + else if tFn.isMVar && sFn.isMVar && tFn == sFn then + Bool.toLBool <$> isDefEqMVarSelf tFn t.getAppArgs s.getAppArgs else - isDefEqQuickMVarMVar t s + let tAssign? ← isAssignable tFn + let sAssign? ← isAssignable sFn + let assignableMsg (b : Bool) := if b then "[assignable]" else "[nonassignable]" + trace[Meta.isDefEq]! "{t} {assignableMsg tAssign?} =?= {s} {assignableMsg sAssign?}" + let assign (t s : Expr) : DefEqM LBool := toLBoolM $ processAssignment t s + if tAssign? && !sAssign? then + toLBoolM $ processAssignment t s + else if !tAssign? && sAssign? then + toLBoolM $ processAssignment s t + else if !tAssign? && !sAssign? then + if tFn.isMVar || sFn.isMVar then + let ctx ← read + if ctx.config.isDefEqStuckEx then do + trace[Meta.isDefEq.stuck]! "{t} =?= {s}" + Meta.throwIsDefEqStuck + else + pure LBool.false + else + pure LBool.undef + else + isDefEqQuickMVarMVar t s -- Both `t` and `s` are terms of the form `?m ...` private partial def isDefEqQuickMVarMVar (t s : Expr) : DefEqM LBool := do -let tFn := t.getAppFn -let sFn := s.getAppFn -let tMVarDecl ← getMVarDecl tFn.mvarId! -let sMVarDecl ← getMVarDecl sFn.mvarId! -if s.isMVar && !t.isMVar then - /- Solve `?m t =?= ?n` by trying first `?n := ?m t`. - Reason: this assignment is precise. -/ - if (← commitWhen (processAssignment s t)) then - pure LBool.true - else - toLBoolM $ processAssignment t s -else - if (← commitWhen (processAssignment t s)) then - pure LBool.true - else - toLBoolM $ processAssignment s t + let tFn := t.getAppFn + let sFn := s.getAppFn + let tMVarDecl ← getMVarDecl tFn.mvarId! + let sMVarDecl ← getMVarDecl sFn.mvarId! + if s.isMVar && !t.isMVar then + /- Solve `?m t =?= ?n` by trying first `?n := ?m t`. + Reason: this assignment is precise. -/ + if (← commitWhen (processAssignment s t)) then + pure LBool.true + else + toLBoolM $ processAssignment t s + else + if (← commitWhen (processAssignment t s)) then + pure LBool.true + else + toLBoolM $ processAssignment s t end @[inline] def whenUndefDo (x : DefEqM LBool) (k : DefEqM Bool) : DefEqM Bool := do -let status ← x -match status with -| LBool.true => pure true -| LBool.false => pure false -| LBool.undef => k + let status ← x + match status with + | LBool.true => pure true + | LBool.false => pure false + | LBool.undef => k @[specialize] private def unstuckMVar (e : Expr) (successK : Expr → DefEqM Bool) (failK : DefEqM Bool): DefEqM Bool := do -match (← getStuckMVar? e) with -| some mvarId => - if (← Meta.synthPending mvarId) then - let e ← instantiateMVars e - successK e - else - failK -| none => failK + match (← getStuckMVar? e) with + | some mvarId => + if (← Meta.synthPending mvarId) then + let e ← instantiateMVars e + successK e + else + failK + | none => failK 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 + unstuckMVar t (fun t => Meta.isExprDefEqAux t s) $ + unstuckMVar s (fun s => Meta.isExprDefEqAux t s) $ + pure false private def isDefEqProj : Expr → Expr → DefEqM Bool -| Expr.proj _ i t _, Expr.proj _ j s _ => pure (i == j) <&&> Meta.isExprDefEqAux t s -| _, _ => pure false + | Expr.proj _ i t _, Expr.proj _ j s _ => pure (i == j) <&&> Meta.isExprDefEqAux t s + | _, _ => pure false -partial def isExprDefEqAuxImpl : Expr → Expr → DefEqM Bool -| t, s => do +partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : DefEqM Bool := do trace[Meta.isDefEq.step]! "{t} =?= {s}" withNestedTraces do whenUndefDo (isDefEqQuick t s) $ @@ -1156,7 +1155,8 @@ partial def isExprDefEqAuxImpl : Expr → Expr → DefEqM Bool whenUndefDo (isDefEqStringLit t s) $ isDefEqOnFailure t s -builtin_initialize isExprDefEqAuxRef.set isExprDefEqAuxImpl +builtin_initialize + isExprDefEqAuxRef.set isExprDefEqAuxImpl builtin_initialize registerTraceClass `Meta.isDefEq diff --git a/src/Lean/Meta/LevelDefEq.lean b/src/Lean/Meta/LevelDefEq.lean index f2dc8ba98f..1150b9c05a 100644 --- a/src/Lean/Meta/LevelDefEq.lean +++ b/src/Lean/Meta/LevelDefEq.lean @@ -9,169 +9,168 @@ import Lean.Meta.InferType namespace Lean.Meta private partial def decAux? : Level → MetaM (Option Level) -| Level.zero _ => pure none -| Level.param _ _ => pure none -| Level.mvar mvarId _ => do - let mctx ← getMCtx - match mctx.getLevelAssignment? mvarId with - | some u => decAux? u - | none => - if (← isReadOnlyLevelMVar mvarId) then - pure none - else - let u ← mkFreshLevelMVar - assignLevelMVar mvarId (mkLevelSucc u) - pure u -| Level.succ u _ => pure u -| u => - let process (u v : Level) : MetaM (Option Level) := do - match (← decAux? u) with - | none => pure none - | some u => do - match (← decAux? v) with + | Level.zero _ => pure none + | Level.param _ _ => pure none + | Level.mvar mvarId _ => do + let mctx ← getMCtx + match mctx.getLevelAssignment? mvarId with + | some u => decAux? u + | none => + if (← isReadOnlyLevelMVar mvarId) then + pure none + else + let u ← mkFreshLevelMVar + assignLevelMVar mvarId (mkLevelSucc u) + pure u + | Level.succ u _ => pure u + | u => + let process (u v : Level) : MetaM (Option Level) := do + match (← decAux? u) with | none => pure none - | some v => pure $ mkLevelMax u v - match u with - | Level.max u v _ => process u v - /- Remark: If `decAux? v` returns `some ...`, then `imax u v` is equivalent to `max u v`. -/ - | Level.imax u v _ => process u v - | _ => unreachable! + | some u => do + match (← decAux? v) with + | none => pure none + | some v => pure $ mkLevelMax u v + match u with + | Level.max u v _ => process u v + /- Remark: If `decAux? v` returns `some ...`, then `imax u v` is equivalent to `max u v`. -/ + | Level.imax u v _ => process u v + | _ => unreachable! variables {m : Type → Type} [MonadLiftT MetaM m] private def decLevelImp (u : Level) : MetaM (Option Level) := do -let mctx ← getMCtx -match (← decAux? u) with -| some v => pure $ some v -| none => do - modify fun s => { s with mctx := mctx } - pure none + let mctx ← getMCtx + match (← decAux? u) with + | some v => pure $ some v + | none => do + modify fun s => { s with mctx := mctx } + pure none def decLevel? (u : Level) : m (Option Level) := -liftMetaM $ decLevelImp u + liftMetaM $ decLevelImp u def decLevel (u : Level) : m Level := liftMetaM do -match (← decLevel? u) with -| some u => pure u -| none => throwError! "invalid universe level, {u} is not greater than 0" + match (← decLevel? u) with + | some u => pure u + | none => throwError! "invalid universe level, {u} is not greater than 0" /- This method is useful for inferring universe level parameters for function that take arguments such as `{α : Type u}`. Recall that `Type u` is `Sort (u+1)` in Lean. Thus, given `α`, we must infer its universe level, and then decrement 1 to obtain `u`. -/ def getDecLevel (type : Expr) : m Level := liftMetaM do -let u ← getLevel type -decLevel u + let u ← getLevel type + decLevel u private def strictOccursMaxAux (lvl : Level) : Level → Bool -| Level.max u v _ => strictOccursMaxAux lvl u || strictOccursMaxAux lvl v -| u => u != lvl && lvl.occurs u + | Level.max u v _ => strictOccursMaxAux lvl u || strictOccursMaxAux lvl v + | u => u != lvl && lvl.occurs u /-- Return true iff `lvl` occurs in `max u_1 ... u_n` and `lvl != u_i` for all `i in [1, n]`. That is, `lvl` is a proper level subterm of some `u_i`. -/ private def strictOccursMax (lvl : Level) : Level → Bool -| Level.max u v _ => strictOccursMaxAux lvl u || strictOccursMaxAux lvl v -| _ => false + | Level.max u v _ => strictOccursMaxAux lvl u || strictOccursMaxAux lvl v + | _ => false /-- `mkMaxArgsDiff mvarId (max u_1 ... (mvar mvarId) ... u_n) v` => `max v u_1 ... u_n` -/ private def mkMaxArgsDiff (mvarId : MVarId) : Level → Level → Level -| Level.max u v _, acc => mkMaxArgsDiff mvarId v $ mkMaxArgsDiff mvarId u acc -| l@(Level.mvar id _), acc => if id != mvarId then mkLevelMax acc l else acc -| l, acc => mkLevelMax acc l + | Level.max u v _, acc => mkMaxArgsDiff mvarId v $ mkMaxArgsDiff mvarId u acc + | l@(Level.mvar id _), acc => if id != mvarId then mkLevelMax acc l else acc + | l, acc => mkLevelMax acc l /-- Solve `?m =?= max ?m v` by creating a fresh metavariable `?n` and assigning `?m := max ?n v` -/ private def solveSelfMax (mvarId : MVarId) (v : Level) : MetaM Unit := do -let n ← mkFreshLevelMVar -assignLevelMVar mvarId $ mkMaxArgsDiff mvarId v n + let n ← mkFreshLevelMVar + assignLevelMVar mvarId $ mkMaxArgsDiff mvarId v n private def postponeIsLevelDefEq (lhs : Level) (rhs : Level) : DefEqM Unit := -modify fun postponed => postponed.push { lhs := lhs, rhs := rhs } + modify fun postponed => postponed.push { lhs := lhs, rhs := rhs } mutual private partial def solve (u v : Level) : DefEqM LBool := do -match u, v with -| Level.mvar mvarId _, _ => - if (← isReadOnlyLevelMVar mvarId) then - pure LBool.undef - else if !u.occurs v then - assignLevelMVar u.mvarId! v - pure LBool.true - else if !strictOccursMax u v then - solveSelfMax u.mvarId! v - pure LBool.true - else - pure LBool.undef -| Level.zero _, Level.max v₁ v₂ _ => - Bool.toLBool <$> (isLevelDefEqAux levelZero v₁ <&&> isLevelDefEqAux levelZero v₂) -| Level.zero _, Level.imax _ v₂ _ => - Bool.toLBool <$> isLevelDefEqAux levelZero v₂ -| Level.succ u _, v => - match (← Meta.decLevel? v) with - | some v => Bool.toLBool <$> isLevelDefEqAux u v - | none => pure LBool.undef -| _, _ => pure LBool.undef + match u, v with + | Level.mvar mvarId _, _ => + if (← isReadOnlyLevelMVar mvarId) then + pure LBool.undef + else if !u.occurs v then + assignLevelMVar u.mvarId! v + pure LBool.true + else if !strictOccursMax u v then + solveSelfMax u.mvarId! v + pure LBool.true + else + pure LBool.undef + | Level.zero _, Level.max v₁ v₂ _ => + Bool.toLBool <$> (isLevelDefEqAux levelZero v₁ <&&> isLevelDefEqAux levelZero v₂) + | Level.zero _, Level.imax _ v₂ _ => + Bool.toLBool <$> isLevelDefEqAux levelZero v₂ + | Level.succ u _, v => + match (← Meta.decLevel? v) with + | some v => Bool.toLBool <$> isLevelDefEqAux u v + | none => pure LBool.undef + | _, _ => pure LBool.undef partial def isLevelDefEqAux : Level → Level → DefEqM Bool -| Level.succ lhs _, Level.succ rhs _ => isLevelDefEqAux lhs rhs -| lhs, rhs => do - if lhs == rhs then - pure true - else - trace[Meta.isLevelDefEq.step]! "{lhs} =?= {rhs}" - let lhs' ← instantiateLevelMVars lhs - let lhs' := lhs'.normalize - let rhs' ← instantiateLevelMVars rhs - let rhs' := rhs'.normalize - if lhs != lhs' || rhs != rhs' then - isLevelDefEqAux lhs' rhs' + | Level.succ lhs _, Level.succ rhs _ => isLevelDefEqAux lhs rhs + | lhs, rhs => do + if lhs == rhs then + pure true else - let r ← solve lhs rhs; - if r != LBool.undef then - pure $ r == LBool.true + trace[Meta.isLevelDefEq.step]! "{lhs} =?= {rhs}" + let lhs' ← instantiateLevelMVars lhs + let lhs' := lhs'.normalize + let rhs' ← instantiateLevelMVars rhs + let rhs' := rhs'.normalize + if lhs != lhs' || rhs != rhs' then + isLevelDefEqAux lhs' rhs' else - let r ← solve rhs lhs; + let r ← solve lhs rhs; if r != LBool.undef then pure $ r == LBool.true - else do - let mctx ← getMCtx - if !mctx.hasAssignableLevelMVar lhs && !mctx.hasAssignableLevelMVar rhs then - let ctx ← read - if ctx.config.isDefEqStuckEx && (lhs.isMVar || rhs.isMVar) then do - trace[Meta.isLevelDefEq.stuck]! "{lhs} =?= {rhs}" - Meta.throwIsDefEqStuck + else + let r ← solve rhs lhs; + if r != LBool.undef then + pure $ r == LBool.true + else do + let mctx ← getMCtx + if !mctx.hasAssignableLevelMVar lhs && !mctx.hasAssignableLevelMVar rhs then + let ctx ← read + if ctx.config.isDefEqStuckEx && (lhs.isMVar || rhs.isMVar) then do + trace[Meta.isLevelDefEq.stuck]! "{lhs} =?= {rhs}" + Meta.throwIsDefEqStuck + else + pure false else - pure false - else - postponeIsLevelDefEq lhs rhs; pure true + postponeIsLevelDefEq lhs rhs; pure true end def isListLevelDefEqAux : List Level → List Level → DefEqM Bool -| [], [] => pure true -| u::us, v::vs => isLevelDefEqAux u v <&&> isListLevelDefEqAux us vs -| _, _ => pure false + | [], [] => pure true + | u::us, v::vs => isLevelDefEqAux u v <&&> isListLevelDefEqAux us vs + | _, _ => pure false private def getNumPostponed : DefEqM Nat := do -pure (← get).size + pure (← get).size open Std (PersistentArray) private def getResetPostponed : DefEqM (PersistentArray PostponedEntry) := do -let ps ← get -modify fun _ => {} -pure ps + let ps ← get + modify fun _ => {} + pure ps private def processPostponedStep : DefEqM Bool := -traceCtx `Meta.isLevelDefEq.postponed.step do - let ps ← getResetPostponed - for p in ps do - unless (← isLevelDefEqAux p.lhs p.rhs) do - return false - return true + traceCtx `Meta.isLevelDefEq.postponed.step do + let ps ← getResetPostponed + for p in ps do + unless (← isLevelDefEqAux p.lhs p.rhs) do + return false + return true -private partial def processPostponedAux : Unit → DefEqM Bool -| _ => do +private partial def processPostponedAux : DefEqM Bool := do let numPostponed ← getNumPostponed if numPostponed == 0 then pure true @@ -184,20 +183,22 @@ private partial def processPostponedAux : Unit → DefEqM Bool if numPostponed' == 0 then pure true else if numPostponed' < numPostponed then - processPostponedAux () + processPostponedAux else do trace[Meta.isLevelDefEq.postponed]! "no progress solving pending is-def-eq level constraints" pure false private def processPostponed : DefEqM Bool := do -let numPostponed ← getNumPostponed -if numPostponed == 0 then pure true -else traceCtx `Meta.isLevelDefEq.postponed $ processPostponedAux () +if (← getNumPostponed) == 0 then + pure true +else + traceCtx `Meta.isLevelDefEq.postponed do + processPostponedAux private def restore (env : Environment) (mctx : MetavarContext) (postponed : PersistentArray PostponedEntry) : DefEqM Unit := do -setEnv env -setMCtx mctx -set postponed + setEnv env + setMCtx mctx + set postponed /-- `commitWhen x` executes `x` and process all postponed universe level constraints produced by `x`. @@ -206,49 +207,49 @@ set postponed Remark: postponed universe level constraints must be solved before returning. Otherwise, we don't know whether `x` really succeeded. -/ @[specialize] def commitWhen (x : DefEqM Bool) : DefEqM Bool := do -let env ← getEnv -let mctx ← getMCtx -let postponed ← getResetPostponed -try - if (← x) then - if (← processPostponed) then - pure true + let env ← getEnv + let mctx ← getMCtx + let postponed ← getResetPostponed + try + if (← x) then + if (← processPostponed) then + pure true + else + restore env mctx postponed + pure false else restore env mctx postponed pure false - else + catch ex => restore env mctx postponed - pure false -catch ex => - restore env mctx postponed - throw ex + throw ex private def runDefEqM (x : DefEqM Bool) : MetaM Bool := -(commitWhen x).run' {} + (commitWhen x).run' {} def isLevelDefEq (u v : Level) : m Bool := liftMetaM do -traceCtx `Meta.isLevelDefEq do - let b ← runDefEqM $ Meta.isLevelDefEqAux u v - trace[Meta.isLevelDefEq]! "{u} =?= {v} ... {if b then "success" else "failure"}" - pure b + traceCtx `Meta.isLevelDefEq do + let 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 - let b ← runDefEqM $ Meta.isExprDefEqAux t s - trace[Meta.isDefEq]! "{t} =?= {s} ... {if b then "success" else "failure"}" - pure b + traceCtx `Meta.isDefEq $ do + let b ← runDefEqM $ Meta.isExprDefEqAux t s + trace[Meta.isDefEq]! "{t} =?= {s} ... {if b then "success" else "failure"}" + pure b abbrev isDefEq (t s : Expr) : m Bool := -isExprDefEq t s + isExprDefEq t s def isExprDefEqGuarded (a b : Expr) : m Bool := liftMetaM do -try isExprDefEq a b catch _ => pure false + try isExprDefEq a b catch _ => pure false abbrev isDefEqGuarded (t s : Expr) : m Bool := -isExprDefEqGuarded t s + isExprDefEqGuarded t s def isDefEqNoConstantApprox (t s : Expr) : m Bool := liftMetaM do -approxDefEq $ isDefEq t s + approxDefEq $ isDefEq t s builtin_initialize registerTraceClass `Meta.isLevelDefEq