From 9d53fa701c8431f6870e29654ca4788b4beccf7a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 22 Dec 2019 09:15:04 -0800 Subject: [PATCH] chore: combine `MessageData.context` + `MessageData.withOptions` into `MessageData.context` --- src/Init/Lean/Elab/Command.lean | 13 ++++++--- src/Init/Lean/Elab/Term.lean | 2 +- src/Init/Lean/Elab/TermApp.lean | 3 ++- src/Init/Lean/Meta/Basic.lean | 6 ++--- src/Init/Lean/Meta/Exception.lean | 7 +++-- src/Init/Lean/Meta/Message.lean | 26 +++++++++--------- src/Init/Lean/Meta/SynthInstance.lean | 2 +- src/Init/Lean/Util/Message.lean | 38 ++++++++++++++------------- src/Init/Lean/Util/Sorry.lean | 4 +-- 9 files changed, 54 insertions(+), 47 deletions(-) diff --git a/src/Init/Lean/Elab/Command.lean b/src/Init/Lean/Elab/Command.lean index e67e015234..ea5ea90984 100644 --- a/src/Init/Lean/Elab/Command.lean +++ b/src/Init/Lean/Elab/Command.lean @@ -21,7 +21,7 @@ structure Context := structure Scope := (kind : String) (header : String) -(options : Options := {}) +(opts : Options := {}) (currNamespace : Name := Name.anonymous) (openDecls : List OpenDecl := []) (univNames : List Name := []) @@ -38,7 +38,7 @@ structure State := instance State.inhabited : Inhabited State := ⟨{ env := arbitrary _ }⟩ def mkState (env : Environment) (messages : MessageLog := {}) (opts : Options := {}) : State := -{ env := env, messages := messages, scopes := [{ kind := "root", header := "", options := opts }] } +{ env := env, messages := messages, scopes := [{ kind := "root", header := "", opts := opts }] } abbrev CommandElabM := ReaderT Context (EStateM Exception State) abbrev CommandElab := SyntaxNode → CommandElabM Unit @@ -103,7 +103,7 @@ stx.ifNode private def mkTermContext (ctx : Context) (s : State) : Term.Context := let scope := s.scopes.head!; -{ config := { opts := scope.options, foApprox := true, ctxApprox := true, quasiPatternApprox := true, isDefEqStuckEx := true }, +{ config := { opts := scope.opts, foApprox := true, ctxApprox := true, quasiPatternApprox := true, isDefEqStuckEx := true }, fileName := ctx.fileName, fileMap := ctx.fileMap, cmdPos := s.cmdPos, @@ -139,6 +139,9 @@ modify $ fun s => { env := newEnv, .. s } def getScope : CommandElabM Scope := do s ← get; pure s.scopes.head! +def getOptions : CommandElabM Options := do +scope ← getScope; pure scope.opts + def getCurrNamespace : CommandElabM Name := do scope ← getScope; pure scope.currNamespace @@ -230,7 +233,9 @@ fun stx => do env ← getEnv; match env.addDecl Declaration.quotDecl with | Except.ok env => setEnv env - | Except.error ex => throwError stx.val ex.toMessageData + | Except.error ex => do + opts ← getOptions; + throwError stx.val (ex.toMessageData opts) def getOpenDecls : CommandElabM (List OpenDecl) := do scope ← getScope; pure scope.openDecls diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean index 294d9e5c41..7f5442d8b9 100644 --- a/src/Init/Lean/Elab/Term.lean +++ b/src/Init/Lean/Elab/Term.lean @@ -199,7 +199,7 @@ def assignExprMVar (mvarId : MVarId) (val : Expr) : TermElabM Unit := modify $ f def addContext (msg : MessageData) : TermElabM MessageData := do ctx ← read; s ← get; -pure $ MessageData.withOptions ctx.config.opts $ MessageData.context s.env s.mctx ctx.lctx msg +pure $ MessageData.withContext { env := s.env, mctx := s.mctx, lctx := ctx.lctx, opts := ctx.config.opts } msg instance tracer : SimpleMonadTracerAdapter TermElabM := { getOptions := getOptions, diff --git a/src/Init/Lean/Elab/TermApp.lean b/src/Init/Lean/Elab/TermApp.lean index 974938b96c..5e90171489 100644 --- a/src/Init/Lean/Elab/TermApp.lean +++ b/src/Init/Lean/Elab/TermApp.lean @@ -367,8 +367,9 @@ else applyResult $ successes.get! 0 else if successes.size > 1 then do lctx ← getLCtx; + opts ← getOptions; let msgs : Array MessageData := successes.map $ fun success => match success with - | EStateM.Result.ok e s => MessageData.context s.env s.mctx lctx e + | EStateM.Result.ok e s => MessageData.withContext { env := s.env, mctx := s.mctx, lctx := lctx, opts := opts } e | _ => unreachable!; throwError f ("ambiguous, possible interpretations " ++ MessageData.ofArray msgs) else diff --git a/src/Init/Lean/Meta/Basic.lean b/src/Init/Lean/Meta/Basic.lean index 52a16ccca1..9dfa41838f 100644 --- a/src/Init/Lean/Meta/Basic.lean +++ b/src/Init/Lean/Meta/Basic.lean @@ -232,7 +232,7 @@ pure $ mkLevelMVar mvarId @[inline] def throwEx {α} (f : ExceptionContext → Exception) : MetaM α := do ctx ← read; s ← get; -throw (f {env := s.env, mctx := s.mctx, lctx := ctx.lctx }) +throw (f {env := s.env, mctx := s.mctx, lctx := ctx.lctx, opts := ctx.config.opts }) def throwBug {α} (b : Bug) : MetaM α := throwEx $ Exception.bug b @@ -323,7 +323,7 @@ s ← get; pure s.traceState def addContext (msg : MessageData) : MetaM MessageData := do ctx ← read; s ← get; -pure $ MessageData.withOptions ctx.config.opts $ MessageData.context s.env s.mctx ctx.lctx msg +pure $ MessageData.withContext { env := s.env, mctx := s.mctx, lctx := ctx.lctx, opts := ctx.config.opts } msg instance tracer : SimpleMonadTracerAdapter MetaM := { getOptions := getOptions, @@ -381,7 +381,7 @@ fun ctx s => EStateM.Result.ok e { mctx := newS.mctx, ngen := newS.ngen, .. s} | EStateM.Result.error (MetavarContext.MkBinding.Exception.revertFailure mctx lctx toRevert decl) newS => EStateM.Result.error - (Exception.revertFailure toRevert decl { lctx := lctx, mctx := mctx, env := s.env }) + (Exception.revertFailure toRevert decl { lctx := lctx, mctx := mctx, env := s.env, opts := ctx.config.opts }) { mctx := newS.mctx, ngen := newS.ngen, .. s } def mkForall (xs : Array Expr) (e : Expr) : MetaM Expr := diff --git a/src/Init/Lean/Meta/Exception.lean b/src/Init/Lean/Meta/Exception.lean index e66de6685a..bc739fe88b 100644 --- a/src/Init/Lean/Meta/Exception.lean +++ b/src/Init/Lean/Meta/Exception.lean @@ -11,8 +11,7 @@ import Init.Lean.Util.Message namespace Lean namespace Meta -structure ExceptionContext := -(env : Environment) (mctx : MetavarContext) (lctx : LocalContext) +abbrev ExceptionContext := MessageDataContext inductive Bug | overwritingExprMVar (mvarId : Name) @@ -67,8 +66,8 @@ def toStr : Exception → String instance : HasToString Exception := ⟨toStr⟩ -def mkCtx (c : ExceptionContext) (m : MessageData) : MessageData := -MessageData.context c.env c.mctx c.lctx m +def mkCtx (ctx : ExceptionContext) (m : MessageData) : MessageData := +MessageData.withContext ctx m /-- Generate trace message that is suitable for tracing crawlers -/ def toTraceMessageData : Exception → MessageData diff --git a/src/Init/Lean/Meta/Message.lean b/src/Init/Lean/Meta/Message.lean index cf96b92024..48888166ee 100644 --- a/src/Init/Lean/Meta/Message.lean +++ b/src/Init/Lean/Meta/Message.lean @@ -87,13 +87,13 @@ end Meta namespace KernelException -private def mkCtx (env : Environment) (lctx : LocalContext) (msg : MessageData) : MessageData := -MessageData.context env {} lctx msg +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) : MessageData := +def toMessageData (e : KernelException) (opts : Options) : MessageData := match e with -| unknownConstant env constName => mkCtx env {} $ "(kernel) unknown constant " ++ constName -| alreadyDeclared env constName => mkCtx env {} $ "(kernel) constant has already been declared " ++ constName +| 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 @@ -103,17 +103,17 @@ match e 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 {} $ "(kernel) declaration has metavariables " ++ constName -| declHasFVars env constName _ => mkCtx env {} $ "(kernel) declaration has free variables " ++ constName -| funExpected env lctx e => mkCtx env lctx $ "(kernel) function expected" ++ indentExpr e -| typeExpected env lctx e => mkCtx env lctx $ "(kernel) type expected" ++ indentExpr e -| letTypeMismatch env lctx n _ _ => mkCtx env lctx $ "(kernel) let-declaration type mismatch " ++ n -| exprTypeMismatch env lctx e _ => mkCtx env lctx $ "(kernel) type mismatch at " ++ indentExpr e +| 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 := {} } + | 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 $ "(kernel) invalid projection" ++ indentExpr e +| invalidProj env lctx e => mkCtx env lctx opts $ "(kernel) invalid projection" ++ indentExpr e | other msg => "(kernel) " ++ msg end KernelException diff --git a/src/Init/Lean/Meta/SynthInstance.lean b/src/Init/Lean/Meta/SynthInstance.lean index 1e5af0065c..fa8153a953 100644 --- a/src/Init/Lean/Meta/SynthInstance.lean +++ b/src/Init/Lean/Meta/SynthInstance.lean @@ -145,7 +145,7 @@ def getOptions : SynthM Options := do ctx ← read; pure ctx.config.opts def addContext (msg : MessageData) : SynthM MessageData := do ctx ← read; s ← get; -pure $ MessageData.context s.env s.mctx ctx.lctx msg +pure $ MessageData.withContext { env := s.env, mctx := s.mctx, lctx := ctx.lctx, opts := ctx.config.opts } msg instance tracer : SimpleMonadTracerAdapter SynthM := { getOptions := getOptions, diff --git a/src/Init/Lean/Util/Message.lean b/src/Init/Lean/Util/Message.lean index 3abd18f610..6e7e5b9531 100644 --- a/src/Init/Lean/Util/Message.lean +++ b/src/Init/Lean/Util/Message.lean @@ -19,6 +19,9 @@ fileName ++ ":" ++ toString line ++ ":" ++ toString col ++ " " ++ toString msg inductive MessageSeverity | information | warning | error +structure MessageDataContext := +(env : Environment) (mctx : MetavarContext) (lctx : LocalContext) (opts : Options) + /- Structure message data. We use it for reporting errors, trace messages, etc. -/ inductive MessageData | ofFormat : Format → MessageData @@ -26,9 +29,8 @@ inductive MessageData | ofExpr : Expr → MessageData | ofLevel : Level → MessageData | ofName : Name → MessageData -/- `context env mctx lctx d` specifies the pretty printing context `(env, mctx, lctx)` for the nested expressions in `d`. -/ -| context : Environment → MetavarContext → LocalContext → MessageData → MessageData -| withOptions : Options → MessageData → MessageData +/- `withContext ctx d` specifies the pretty printing context `(env, mctx, lctx, opts)` for the nested expressions in `d`. -/ +| withContext : MessageDataContext → MessageData → MessageData /- Lifted `Format.nest` -/ | nest : Nat → MessageData → MessageData /- Lifted `Format.group` -/ @@ -50,24 +52,24 @@ registerOption `syntaxMaxDepth { defValue := (2 : Nat), group := "", descr := "m def getSyntaxMaxDepth (opts : Options) : Nat := opts.getNat `syntaxMaxDepth 2 -partial def formatAux : Option (Environment × MetavarContext × LocalContext) → Options → MessageData → Format -| _, _, ofFormat fmt => fmt -| _, _, ofLevel u => fmt u -| _, _, ofName n => fmt n -| _, opts, ofSyntax s => s.formatStx (getSyntaxMaxDepth opts) -| none, _, ofExpr e => format (toString e) -| some (env, mctx, lctx), opts, ofExpr e => format (toString (mctx.instantiateMVars e).1) -- TODO: invoke pretty printer -| ctx, opts, context env mctx lctx d => formatAux (some (env, mctx, lctx)) opts d -| ctx, _, withOptions opts d => formatAux ctx opts d -| ctx, opts, tagged cls d => Format.sbracket (format cls) ++ " " ++ formatAux ctx opts d -| ctx, opts, nest n d => Format.nest n (formatAux ctx opts d) -| ctx, opts, compose d₁ d₂ => formatAux ctx opts d₁ ++ formatAux ctx opts d₂ -| ctx, opts, group d => Format.group (formatAux ctx opts d) -| ctx, opts, node ds => Format.nest 2 $ ds.foldl (fun r d => r ++ Format.line ++ formatAux ctx opts d) Format.nil +partial def formatAux : Option MessageDataContext → MessageData → Format +| _, ofFormat fmt => fmt +| _, ofLevel u => fmt u +| _, ofName n => fmt n +| some ctx, ofSyntax s => s.formatStx (getSyntaxMaxDepth ctx.opts) +| none, ofSyntax s => s.formatStx +| none, ofExpr e => format (toString e) +| some ctx, ofExpr e => format (toString (ctx.mctx.instantiateMVars e).1) -- TODO: invoke pretty printer +| _, withContext ctx d => formatAux (some ctx) d +| ctx, tagged cls d => Format.sbracket (format cls) ++ " " ++ formatAux ctx d +| ctx, nest n d => Format.nest n (formatAux ctx d) +| ctx, compose d₁ d₂ => formatAux ctx d₁ ++ formatAux ctx d₂ +| ctx, group d => Format.group (formatAux ctx d) +| ctx, node ds => Format.nest 2 $ ds.foldl (fun r d => r ++ Format.line ++ formatAux ctx d) Format.nil instance : HasAppend MessageData := ⟨compose⟩ -instance : HasFormat MessageData := ⟨fun d => formatAux none {} d⟩ +instance : HasFormat MessageData := ⟨fun d => formatAux none d⟩ instance coeOfFormat : HasCoe Format MessageData := ⟨ofFormat⟩ instance coeOfLevel : HasCoe Level MessageData := ⟨ofLevel⟩ diff --git a/src/Init/Lean/Util/Sorry.lean b/src/Init/Lean/Util/Sorry.lean index cc28a63bfc..c3e8300d2f 100644 --- a/src/Init/Lean/Util/Sorry.lean +++ b/src/Init/Lean/Util/Sorry.lean @@ -37,7 +37,7 @@ def Expr.hasSyntheticSorry : Expr → Bool partial def MessageData.hasSorry : MessageData → Bool | MessageData.ofExpr e => e.hasSorry -| MessageData.context _ _ _ msg => msg.hasSorry +| MessageData.withContext _ msg => msg.hasSorry | MessageData.nest _ msg => msg.hasSorry | MessageData.group msg => msg.hasSorry | MessageData.compose msg₁ msg₂ => msg₁.hasSorry || msg₂.hasSorry @@ -47,7 +47,7 @@ partial def MessageData.hasSorry : MessageData → Bool partial def MessageData.hasSyntheticSorry : MessageData → Bool | MessageData.ofExpr e => e.hasSyntheticSorry -| MessageData.context _ _ _ msg => msg.hasSyntheticSorry +| MessageData.withContext _ msg => msg.hasSyntheticSorry | MessageData.nest _ msg => msg.hasSyntheticSorry | MessageData.group msg => msg.hasSyntheticSorry | MessageData.compose msg₁ msg₂ => msg₁.hasSyntheticSorry || msg₂.hasSyntheticSorry