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

refactor: KernelException at MetaM

Browse source
This commit is contained in:
Leonardo de Moura 2020-03-20 17:46:19 -07:00
parent 86784594d6
commit b705142ae4
3 changed files with 41 additions and 38 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

37
src/Init/Lean/Message.lean
View file

@ -178,4 +178,41 @@ def toList (log : MessageLog) : List Message :=
(log.msgs.foldl (fun acc msg => msg :: acc) []).reverse
end MessageLog
def indentExpr (msg : MessageData) : MessageData :=
MessageData.nest 2 (Format.line ++ msg)
namespace KernelException
private def mkCtx (env : Environment) (lctx : LocalContext) (opts : Options) (msg : MessageData) : MessageData :=
MessageData.withContext { env := env, mctx := {}, lctx := lctx, opts := opts } msg
def toMessageData (e : KernelException) (opts : Options) : MessageData :=
match e with
| unknownConstant env constName => mkCtx env {} opts $ "(kernel) unknown constant " ++ constName
| alreadyDeclared env constName => mkCtx env {} opts $ "(kernel) constant has already been declared " ++ constName
| declTypeMismatch env decl givenType =>
let process (n : Name) (expectedType : Expr) : MessageData :=
"(kernel) declaration type mismatch " ++ n
++ Format.line ++ "has type" ++ indentExpr givenType
++ Format.line ++ "but it is expected to have type" ++ indentExpr expectedType;
match decl with
| Declaration.defnDecl { name := n, type := type, .. } => process n type
| Declaration.thmDecl { name := n, type := type, .. } => process n type
| _ => "(kernel) declaration type mismatch" -- TODO fix type checker, type mismatch for mutual decls does not have enough information
| declHasMVars env constName _ => mkCtx env {} opts $ "(kernel) declaration has metavariables " ++ constName
| declHasFVars env constName _ => mkCtx env {} opts $ "(kernel) declaration has free variables " ++ constName
| funExpected env lctx e => mkCtx env lctx opts $ "(kernel) function expected" ++ indentExpr e
| typeExpected env lctx e => mkCtx env lctx opts $ "(kernel) type expected" ++ indentExpr e
| letTypeMismatch env lctx n _ _ => mkCtx env lctx opts $ "(kernel) let-declaration type mismatch " ++ n
| exprTypeMismatch env lctx e _ => mkCtx env lctx opts $ "(kernel) type mismatch at " ++ indentExpr e
| appTypeMismatch env lctx e fnType argType =>
mkCtx env lctx opts $
"application type mismatch" ++ indentExpr e
++ "argument has type" ++ indentExpr argType
++ "but function has type" ++ indentExpr fnType
| invalidProj env lctx e => mkCtx env lctx opts $ "(kernel) invalid projection" ++ indentExpr e
| other msg => "(kernel) " ++ msg
end KernelException
end Lean

3
src/Init/Lean/Meta/Exception.lean
View file

@ -37,6 +37,7 @@ inductive Exception
| appBuilder (op : Name) (msg : String) (args : Array Expr) (ctx : ExceptionContext)
| synthInstance (inst : Expr) (ctx : ExceptionContext)
| tactic (tacticName : Name) (mvarId : MVarId) (msg : MessageData) (ctx : ExceptionContext)
| kernel (ex : KernelException) (opts : Options)
| bug (b : Bug) (ctx : ExceptionContext)
| other (msg : String)
@ -64,6 +65,7 @@ def toStr : Exception → String
| appBuilder _ _ _ _ => "application builder failure"
| synthInstance _ _ => "type class instance synthesis failed"
| tactic tacName _ _ _ => "tactic '" ++ toString tacName ++ "' failed"
| kernel _ _ => "kernel exception"
| bug _ _ => "bug"
| other s => s
@ -93,6 +95,7 @@ def toTraceMessageData : Exception → MessageData
| appBuilder op msg args ctx => mkCtx ctx $ `appBuilder ++ " " ++ op ++ " " ++ args ++ " " ++ msg
| synthInstance inst ctx => mkCtx ctx $ `synthInstance ++ " " ++ inst
| tactic tacName mvarId msg ctx => mkCtx ctx $ `tacticFailure ++ " " ++ tacName ++ " " ++ msg
| kernel ex opts => ex.toMessageData opts
| bug _ _ => "internal bug" -- TODO improve
| other s => s

39
src/Init/Lean/Meta/Message.lean
View file

@ -7,10 +7,6 @@ prelude
import Init.Lean.Meta.Basic
namespace Lean
def indentExpr (msg : MessageData) : MessageData :=
MessageData.nest 2 (Format.line ++ msg)
namespace Meta
namespace Exception
@ -79,6 +75,7 @@ def toMessageData : Exception → MessageData
| appBuilder op msg args ctx => mkCtx ctx $ "application builder failure " ++ op ++ " " ++ args ++ " " ++ msg
| synthInstance inst ctx => mkCtx ctx $ "failed to synthesize" ++ indentExpr inst
| tactic tacName mvarId msg ctx => mkCtx ctx $ "tactic '" ++ tacName ++ "' failed, " ++ msg ++ Format.line ++ MessageData.ofGoal mvarId
| kernel ex opts => ex.toMessageData opts
| bug _ _ => "internal bug" -- TODO improve
| other s => s
@ -95,38 +92,4 @@ instance MetaHasEval {α} [MetaHasEval α] : MetaHasEval (MetaM α) :=
throw (IO.userError (toString (format err.toMessageData)))⟩
end Meta
namespace KernelException
private def mkCtx (env : Environment) (lctx : LocalContext) (opts : Options) (msg : MessageData) : MessageData :=
MessageData.withContext { env := env, mctx := {}, lctx := lctx, opts := opts } msg
def toMessageData (e : KernelException) (opts : Options) : MessageData :=
match e with
| unknownConstant env constName => mkCtx env {} opts $ "(kernel) unknown constant " ++ constName
| alreadyDeclared env constName => mkCtx env {} opts $ "(kernel) constant has already been declared " ++ constName
| declTypeMismatch env decl givenType =>
let process (n : Name) (expectedType : Expr) : MessageData :=
"(kernel) declaration type mismatch " ++ n
++ Format.line ++ "has type" ++ indentExpr givenType
++ Format.line ++ "but it is expected to have type" ++ indentExpr expectedType;
match decl with
| Declaration.defnDecl { name := n, type := type, .. } => process n type
| Declaration.thmDecl { name := n, type := type, .. } => process n type
| _ => "(kernel) declaration type mismatch" -- TODO fix type checker, type mismatch for mutual decls does not have enough information
| declHasMVars env constName _ => mkCtx env {} opts $ "(kernel) declaration has metavariables " ++ constName
| declHasFVars env constName _ => mkCtx env {} opts $ "(kernel) declaration has free variables " ++ constName
| funExpected env lctx e => mkCtx env lctx opts $ "(kernel) function expected" ++ indentExpr e
| typeExpected env lctx e => mkCtx env lctx opts $ "(kernel) type expected" ++ indentExpr e
| letTypeMismatch env lctx n _ _ => mkCtx env lctx opts $ "(kernel) let-declaration type mismatch " ++ n
| exprTypeMismatch env lctx e _ => mkCtx env lctx opts $ "(kernel) type mismatch at " ++ indentExpr e
| appTypeMismatch env lctx e _ _ =>
match e with
| Expr.app f a _ => "(kernel) " ++ Meta.Exception.mkAppTypeMismatchMessage f a { env := env, lctx := lctx, mctx := {}, opts := opts }
| _ => "(kernel) application type mismatch at" ++ indentExpr e
| invalidProj env lctx e => mkCtx env lctx opts $ "(kernel) invalid projection" ++ indentExpr e
| other msg => "(kernel) " ++ msg
end KernelException
end Lean