From 201d8a97d252a15ef9a61be064de3ebcba57e158 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 19 Nov 2019 07:09:21 -0800 Subject: [PATCH] feat: add `Check.lean` --- library/Init/Lean/Meta.lean | 8 ++ library/Init/Lean/Meta/Basic.lean | 5 +- library/Init/Lean/Meta/Check.lean | 108 ++++++++++++++++++++++++++ library/Init/Lean/Meta/Exception.lean | 4 + library/Init/Lean/Meta/ExprDefEq.lean | 13 +--- library/Init/Lean/Meta/FunInfo.lean | 2 +- library/Init/Lean/Meta/InferType.lean | 6 +- 7 files changed, 131 insertions(+), 15 deletions(-) create mode 100644 library/Init/Lean/Meta/Check.lean diff --git a/library/Init/Lean/Meta.lean b/library/Init/Lean/Meta.lean index 4c07b08c1a..de50afa0e3 100644 --- a/library/Init/Lean/Meta.lean +++ b/library/Init/Lean/Meta.lean @@ -9,6 +9,7 @@ import Init.Lean.Meta.WHNF import Init.Lean.Meta.InferType import Init.Lean.Meta.FunInfo import Init.Lean.Meta.LevelDefEq +import Init.Lean.Meta.ExprDefEq namespace Lean namespace Meta @@ -61,5 +62,12 @@ getFunInfoAux whnf fn def getFunInfoNArgs (fn : Expr) (nargs : Nat) : MetaM FunInfo := getFunInfoNArgsAux whnf fn nargs +/-- Throws exception if `e` is not type correct. -/ +def check (e : Expr) : MetaM Unit := +checkAux whnf isDefEq e + +def isTypeCorrect (e : Expr) : MetaM Bool := +isTypeCorrectAux whnf isDefEq e + end Meta end Lean diff --git a/library/Init/Lean/Meta/Basic.lean b/library/Init/Lean/Meta/Basic.lean index 1b3c2b5316..78fa117725 100644 --- a/library/Init/Lean/Meta/Basic.lean +++ b/library/Init/Lean/Meta/Basic.lean @@ -242,6 +242,9 @@ do lctx ← getLCtx; | some d => pure d | none => throwEx $ Exception.unknownFVar fvarId +def getFVarLocalDecl (fvar : Expr) : MetaM LocalDecl := +getLocalDecl fvar.fvarId! + def getMVarDecl (mvarId : Name) : MetaM MetavarDecl := do mctx ← getMCtx; match mctx.findDecl mvarId with @@ -344,7 +347,7 @@ resettingTypeClassCache $ | i, k => if h : i < fvars.size then do let fvar := fvars.get ⟨i, h⟩; - decl ← getLocalDecl fvar.fvarId!; + decl ← getFVarLocalDecl fvar; c? ← isClassQuick decl.type; match c? with | LOption.none => withNewLocalInstances (i+1) k diff --git a/library/Init/Lean/Meta/Check.lean b/library/Init/Lean/Meta/Check.lean new file mode 100644 index 0000000000..d8aca7b73d --- /dev/null +++ b/library/Init/Lean/Meta/Check.lean @@ -0,0 +1,108 @@ +/- +Copyright (c) 2019 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +prelude +import Init.Lean.Meta.InferType + +/- +This is not the Kernel type checker, but an auxiliary method for checking +whether terms produced by tactics and `isDefEq` are type correct. +-/ + +namespace Lean +namespace Meta + +@[specialize] private def ensureType + (whnf : Expr → MetaM Expr) + (e : Expr) : MetaM Unit := +do getLevelAux whnf (inferTypeAux whnf) e; + pure () + +@[specialize] private def checkLambdaLet + (whnf : Expr → MetaM Expr) + (isDefEq : Expr → Expr → MetaM Bool) + (check : Expr → MetaM Unit) + (e : Expr) : MetaM Unit := +lambdaTelescope whnf e $ fun xs b => do + xs.forM $ fun x => do { + xDecl ← getFVarLocalDecl x; + match xDecl with + | LocalDecl.cdecl _ _ _ t _ => do + ensureType whnf t; + check t + | LocalDecl.ldecl _ _ _ t v => do + ensureType whnf t; + check t; + vType ← inferTypeAux whnf v; + unlessM (isDefEq t vType) $ throwEx $ Exception.letTypeMismatch x.fvarId!; + check v + }; + check b + +@[specialize] private def checkForall + (whnf : Expr → MetaM Expr) + (check : Expr → MetaM Unit) + (e : Expr) : MetaM Unit := +forallTelescope whnf e $ fun xs b => do + xs.forM $ fun x => do { + xDecl ← getFVarLocalDecl x; + ensureType whnf xDecl.type; + check xDecl.type + }; + ensureType whnf b; + check b + +@[specialize] private def checkConstant + (c : Name) (lvls : List Level) : MetaM Unit := +do env ← getEnv; + match env.find c with + | none => throwEx $ Exception.unknownConst c + | some cinfo => unless (lvls.length != cinfo.lparams.length) $ throwEx $ Exception.incorrectNumOfLevels c lvls + +@[specialize] private def checkApp + (whnf : Expr → MetaM Expr) + (isDefEq : Expr → Expr → MetaM Bool) + (check : Expr → MetaM Unit) + (f a : Expr) : MetaM Unit := +do check f; + check a; + fType ← inferTypeAux whnf f; + fType ← whnf fType; + match fType with + | Expr.forallE _ d _ _ => do + aType ← inferTypeAux whnf a; + unlessM (isDefEq d aType) $ throwEx $ Exception.appTypeMismatch f a + | _ => unless fType.isForall $ throwEx $ Exception.functionExpected fType #[a] + +@[specialize] private partial def checkAuxAux + (whnf : Expr → MetaM Expr) + (isDefEq : Expr → Expr → MetaM Bool) + : Expr → MetaM Unit +| e@(Expr.forallE _ _ _ _) => checkForall whnf checkAuxAux e +| e@(Expr.lam _ _ _ _) => checkLambdaLet whnf isDefEq checkAuxAux e +| e@(Expr.letE _ _ _ _ _) => checkLambdaLet whnf isDefEq checkAuxAux e +| Expr.const c lvls _ => checkConstant c lvls +| Expr.app f a _ => checkApp whnf isDefEq checkAuxAux f a +| Expr.mdata _ e _ => checkAuxAux e +| Expr.proj _ _ e _ => checkAuxAux e +| _ => pure () + +@[specialize] def checkAux + (whnf : Expr → MetaM Expr) + (isDefEq : Expr → Expr → MetaM Bool) + (e : Expr) : MetaM Unit := +usingTransparency TransparencyMode.all $ + checkAuxAux whnf isDefEq e + +@[specialize] def isTypeCorrectAux + (whnf : Expr → MetaM Expr) + (isDefEq : Expr → Expr → MetaM Bool) + (e : Expr) : MetaM Bool := +catch + (do checkAux whnf isDefEq e; pure true) + (fun _ => pure false) + +end Meta +end Lean diff --git a/library/Init/Lean/Meta/Exception.lean b/library/Init/Lean/Meta/Exception.lean index 5055006565..241d39abb3 100644 --- a/library/Init/Lean/Meta/Exception.lean +++ b/library/Init/Lean/Meta/Exception.lean @@ -28,6 +28,8 @@ inductive Exception | invalidProjection (structName : Name) (idx : Nat) (s : Expr) (ctx : ExceptionContext) | revertFailure (toRevert : Array Expr) (decl : LocalDecl) (ctx : ExceptionContext) | readOnlyMVar (mvarId : Name) (ctx : ExceptionContext) +| letTypeMismatch (fvarId : Name) (ctx : ExceptionContext) +| appTypeMismatch (f a : Expr) (ctx : ExceptionContext) | bug (b : Bug) (ctx : ExceptionContext) | other (msg : String) @@ -47,6 +49,8 @@ def toStr : Exception → String | invalidProjection _ _ _ _ => "invalid projection" | revertFailure _ _ _ => "revert failure" | readOnlyMVar _ _ => "try to assign read only metavariable" +| letTypeMismatch _ _ => "type mismatch at let-expression" +| appTypeMismatch _ _ _ => "application type mismatch" | bug _ _ => "bug" | other s => s diff --git a/library/Init/Lean/Meta/ExprDefEq.lean b/library/Init/Lean/Meta/ExprDefEq.lean index cb575444dd..919573b924 100644 --- a/library/Init/Lean/Meta/ExprDefEq.lean +++ b/library/Init/Lean/Meta/ExprDefEq.lean @@ -8,6 +8,7 @@ import Init.Lean.Meta.WHNF import Init.Lean.Meta.InferType import Init.Lean.Meta.FunInfo import Init.Lean.Meta.LevelDefEq +import Init.Lean.Meta.Check namespace Lean namespace Meta @@ -156,7 +157,7 @@ else | i, k => if h : i < fvars.size then do let fvar := fvars.get ⟨i, h⟩; - fvarDecl ← getLocalDecl fvar.fvarId!; + fvarDecl ← getFVarLocalDecl fvar; let fvarType := fvarDecl.type; let d₂ := ds₂.get! i; condM (isDefEq fvarType d₂) @@ -606,14 +607,6 @@ private def simpAssignmentArg (arg : Expr) : MetaM Expr := do arg ← if arg.getAppFn.hasExprMVar then instantiateMVars arg else pure arg; simpAssignmentArgAux arg -/- TODO: type check `e`, move to different file -/ -def isTypeCorrect - (whnf : Expr → MetaM Expr) - (isDefEq : Expr → Expr → MetaM Bool) - (synthesizePending : Expr → MetaM Bool) - (e : Expr) : MetaM Bool := -pure true - @[specialize] private partial def processAssignmentAux (whnf : Expr → MetaM Expr) (isDefEq : Expr → Expr → MetaM Bool) @@ -670,7 +663,7 @@ pure true if args.any (fun arg => mvarDecl.lctx.containsFVar arg) then /- We need to type check `v` because abstraction using `mkLambda` may have produced a type incorrect term. See discussion at A2 -/ - condM (isTypeCorrect whnf isDefEq synthesizePending v) + condM (isTypeCorrectAux whnf isDefEq v) (finalize ()) (useFOApprox ()) else diff --git a/library/Init/Lean/Meta/FunInfo.lean b/library/Init/Lean/Meta/FunInfo.lean index 6b369580e7..af979a04f1 100644 --- a/library/Init/Lean/Meta/FunInfo.lean +++ b/library/Init/Lean/Meta/FunInfo.lean @@ -62,7 +62,7 @@ checkFunInfoCache fn maxArgs? $ do pinfo ← fvars.size.foldM (fun (i : Nat) (pinfo : Array ParamInfo) => do let fvar := fvars.get! i; - decl ← getLocalDecl fvar.fvarId!; + decl ← getFVarLocalDecl fvar; prop ← isPropAux whnf decl.type; let backDeps := collectDeps fvars decl.type; let pinfo := updateHasFwdDeps pinfo backDeps; diff --git a/library/Init/Lean/Meta/InferType.lean b/library/Init/Lean/Meta/InferType.lean index e2a74b0578..be269490fd 100644 --- a/library/Init/Lean/Meta/InferType.lean +++ b/library/Init/Lean/Meta/InferType.lean @@ -79,7 +79,7 @@ do let failed : Unit → MetaM Expr := fun _ => throwEx $ Exception.invalidProje | _ => failed () | _ => failed () -@[specialize] private def getLevel +@[specialize] def getLevelAux (whnf : Expr → MetaM Expr) (inferType : Expr → MetaM Expr) (type : Expr) : MetaM Level := @@ -101,11 +101,11 @@ do typeType ← inferType type; (inferType : Expr → MetaM Expr) (e : Expr) : MetaM Expr := forallTelescope whnf e $ fun xs e => do - lvl ← getLevel whnf inferType e; + lvl ← getLevelAux whnf inferType e; lvl ← xs.foldrM (fun x lvl => do xType ← inferType x; - xTypeLvl ← getLevel whnf inferType xType; + xTypeLvl ← getLevelAux whnf inferType xType; pure $ mkLevelIMax xTypeLvl lvl) lvl; pure $ mkSort lvl.normalize