bbc1f4d461
We use it from `TermElabM` and `MetaM`, and they have different `TermElabM` implementations.
124 lines
3.7 KiB
Text
124 lines
3.7 KiB
Text
/-
|
||
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
|
||
Released under Apache 2.0 license as described in the file LICENSE.
|
||
Authors: Leonardo de Moura
|
||
-/
|
||
import Lean.Meta.InferType
|
||
import Lean.Meta.LevelDefEq
|
||
|
||
/-
|
||
This is not the Kernel type checker, but an auxiliary method for checking
|
||
whether terms produced by tactics and `isDefEq` are type correct.
|
||
-/
|
||
|
||
namespace Lean
|
||
namespace Meta
|
||
|
||
private def ensureType (e : Expr) : MetaM Unit := do
|
||
_ ← getLevel e; pure ()
|
||
|
||
def throwLetTypeMismatchMessage {α} (fvarId : FVarId) : MetaM α := do
|
||
lctx ← getLCtx;
|
||
match lctx.find? fvarId with
|
||
| some (LocalDecl.ldecl _ _ n t v _) => do
|
||
vType ← inferType v;
|
||
throwError $
|
||
"invalid let declaration, term" ++ indentExpr v
|
||
++ Format.line ++ "has type " ++ indentExpr vType
|
||
++ Format.line ++ "but 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 {
|
||
xDecl ← getFVarLocalDecl x;
|
||
match xDecl with
|
||
| LocalDecl.cdecl _ _ _ t _ => do
|
||
ensureType t;
|
||
check t
|
||
| LocalDecl.ldecl _ _ _ t v _ => do
|
||
ensureType t;
|
||
check t;
|
||
vType ← inferType v;
|
||
unlessM (isDefEq t vType) $ 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 {
|
||
xDecl ← getFVarLocalDecl x;
|
||
ensureType xDecl.type;
|
||
check xDecl.type
|
||
};
|
||
ensureType b;
|
||
check b
|
||
|
||
private def checkConstant (constName : Name) (us : List Level) : MetaM Unit := do
|
||
cinfo ← getConstInfo constName;
|
||
unless (us.length == cinfo.lparams.length) $ throwIncorrectNumberOfLevels constName us
|
||
|
||
private def getFunctionDomain (f : Expr) : MetaM Expr := do
|
||
fType ← inferType f;
|
||
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;
|
||
aType ← inferType a;
|
||
expectedType ← liftM $ getFunctionDomain f;
|
||
throwError $
|
||
"application type mismatch" ++ indentExpr e
|
||
++ Format.line ++ "argument" ++ indentExpr a
|
||
++ Format.line ++ "has type" ++ indentExpr aType
|
||
++ Format.line ++ "but 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;
|
||
fType ← inferType f;
|
||
fType ← whnf fType;
|
||
match fType with
|
||
| Expr.forallE _ d _ _ => do
|
||
aType ← inferType a;
|
||
unlessM (isDefEq d aType) $ 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 ()
|
||
|
||
def check (e : Expr) : MetaM Unit :=
|
||
traceCtx `Meta.check $
|
||
withTransparency TransparencyMode.all $ checkAux e
|
||
|
||
def isTypeCorrect (e : Expr) : MetaM Bool :=
|
||
catch
|
||
(do check e; pure true)
|
||
(fun ex => do
|
||
trace! `Meta.typeError ex.toMessageData;
|
||
pure false)
|
||
|
||
@[init] private def regTraceClasses : IO Unit := do
|
||
registerTraceClass `Meta.check;
|
||
registerTraceClass `Meta.typeError
|
||
|
||
end Meta
|
||
end Lean
|