From 276a8b99dd22d4c17bb2bedf9d852375bdf4f57a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 25 Nov 2020 14:17:13 -0800 Subject: [PATCH] refactor: move `ppGoal` to `Meta` We need `MetaM` methods such as `isProp` to improve `ppGoal`. This commit also moves `currNamespace` and `openDecls` to `Core.Context`. Without this change, `Meta.ppExpr` was not taking `open` commands into account. --- src/Lean/Attributes.lean | 11 +----- src/Lean/CoreM.lean | 8 +++++ src/Lean/Elab/Command.lean | 14 ++++---- src/Lean/Elab/Term.lean | 16 +++------ src/Lean/Message.lean | 1 - src/Lean/Meta.lean | 1 + src/Lean/Meta/Basic.lean | 3 +- src/Lean/{Util => Meta}/PPGoal.lean | 52 +++++++++++++++-------------- src/Lean/Meta/Tactic/Util.lean | 4 +-- src/Lean/PrettyPrinter.lean | 9 ++--- src/Lean/Util.lean | 1 - src/Lean/Util/PPExt.lean | 41 +++++++++++++---------- 12 files changed, 79 insertions(+), 82 deletions(-) rename src/Lean/{Util => Meta}/PPGoal.lean (65%) diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean index 24c10d1bb7..91256bfa08 100644 --- a/src/Lean/Attributes.lean +++ b/src/Lean/Attributes.lean @@ -20,21 +20,12 @@ def AttributeApplicationTime.beq : AttributeApplicationTime → AttributeApplica instance : BEq AttributeApplicationTime := ⟨AttributeApplicationTime.beq⟩ -structure Attr.Context := - (currNamespace : Name) - (openDecls : List OpenDecl) - -abbrev AttrM := ReaderT Attr.Context CoreM +abbrev AttrM := CoreM instance : MonadLift ImportM AttrM := { monadLift := fun x => do liftM (m := IO) (x { env := (← getEnv), opts := (← getOptions) }) } -instance : MonadResolveName AttrM := { - getCurrNamespace := do pure (← read).currNamespace, - getOpenDecls := do pure (← read).openDecls -} - structure AttributeImplCore := (name : Name) (descr : String) diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index a37c896275..d9d92813f8 100644 --- a/src/Lean/CoreM.lean +++ b/src/Lean/CoreM.lean @@ -10,6 +10,7 @@ import Lean.Exception import Lean.InternalExceptionId import Lean.Eval import Lean.MonadEnv +import Lean.ResolveName namespace Lean namespace Core @@ -27,6 +28,8 @@ structure Context := (currRecDepth : Nat := 0) (maxRecDepth : Nat := 1000) (ref : Syntax := Syntax.missing) + (currNamespace : Name := Name.anonymous) + (openDecls : List OpenDecl := []) abbrev CoreM := ReaderT Context $ StateRefT State (EIO Exception) @@ -60,6 +63,11 @@ instance : MonadRecDepth CoreM := { getMaxRecDepth := do pure (← read).maxRecDepth } +instance : MonadResolveName CoreM := { + getCurrNamespace := do pure (← read).currNamespace, + getOpenDecls := do pure (← read).openDecls +} + @[inline] def liftIOCore (x : IO α) : CoreM α := do let ref ← getRef IO.toEIO (fun (err : IO.Error) => Exception.error ref (toString err)) x diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index f50ca8a611..5a541ed5ff 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -97,11 +97,13 @@ def mkMessageAux (ctx : Context) (ref : Syntax) (msgData : MessageData) (severit mkMessageCore ctx.fileName ctx.fileMap msgData severity (ref.getPos.getD ctx.cmdPos) private def mkCoreContext (ctx : Context) (s : State) : Core.Context := - let scope := s.scopes.head!; - { options := scope.opts, - currRecDepth := ctx.currRecDepth, - maxRecDepth := s.maxRecDepth, - ref := ctx.ref } + let scope := s.scopes.head! + { options := scope.opts + currRecDepth := ctx.currRecDepth + maxRecDepth := s.maxRecDepth + ref := ctx.ref + currNamespace := scope.currNamespace + openDecls := scope.openDecls } def liftCoreM {α} (x : CoreM α) : CommandElabM α := do let s ← get @@ -260,9 +262,7 @@ private def mkTermContext (ctx : Context) (s : State) (declName? : Option Name) fileName := ctx.fileName, fileMap := ctx.fileMap, currMacroScope := ctx.currMacroScope, - currNamespace := scope.currNamespace, levelNames := scope.levelNames, - openDecls := scope.openDecls, declName? := declName? } private def addTraceAsMessages (ctx : Context) (log : MessageLog) (traceState : TraceState) : MessageLog := diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index c9b5886823..f3be52e43c 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -69,10 +69,8 @@ def setElabConfig (cfg : Meta.Config) : Meta.Config := structure Context := (fileName : String) (fileMap : FileMap) - (currNamespace : Name) (declName? : Option Name := none) (levelNames : List Name := []) - (openDecls : List OpenDecl := []) (macroStack : MacroStack := []) (currMacroScope : MacroScope := firstFrontendMacroScope) /- When `mayPostpone == true`, an elaboration function may interrupt its execution by throwing `Exception.postpone`. @@ -236,7 +234,7 @@ instance : MonadLog TermElabM := { getFileMap := do pure (← read).fileMap, getFileName := do pure (← read).fileName, logMessage := fun msg => do - let ctx ← read + let ctx ← readThe Core.Context let msg := { msg with data := MessageData.withNamingContext { currNamespace := ctx.currNamespace, openDecls := ctx.openDecls } msg.data }; modify fun s => { s with messages := s.messages.add msg } } @@ -278,11 +276,6 @@ instance : ToString LVal := ⟨fun | LVal.fieldName n => n | LVal.getOp idx => "[" ++ toString idx ++ "]"⟩ -instance : MonadResolveName TermElabM := { - getCurrNamespace := do pure (← read).currNamespace, - getOpenDecls := do pure (← read).openDecls -} - def getDeclName? : TermElabM (Option Name) := return (← read).declName? def getLetRecsToLift : TermElabM (List LetRecToLift) := return (← get).letRecsToLift def isExprMVarAssigned (mvarId : MVarId) : TermElabM Bool := return (← getMCtx).isExprAssigned mvarId @@ -465,7 +458,7 @@ def mkFreshIdent (ref : Syntax) : TermElabM Syntax := private def liftAttrM {α} (x : AttrM α) : TermElabM α := do let ctx ← read - liftCoreM $ x.run { currNamespace := ctx.currNamespace, openDecls := ctx.openDecls } + liftCoreM x private def applyAttributesCore (declName : Name) (attrs : Array Attribute) @@ -1275,9 +1268,8 @@ fun stx _ => | some msg => elabTermEnsuringType stx[2] expectedType? true msg private def mkSomeContext : Context := { - fileName := "", - fileMap := arbitrary, - currNamespace := Name.anonymous + fileName := "" + fileMap := arbitrary } @[inline] def TermElabM.run {α} (x : TermElabM α) (ctx : Context := mkSomeContext) (s : State := {}) : MetaM (α × State) := diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index ee3f631f08..db3e0ce219 100644 --- a/src/Lean/Message.lean +++ b/src/Lean/Message.lean @@ -11,7 +11,6 @@ import Lean.Syntax import Lean.MetavarContext import Lean.Environment import Lean.Util.PPExt -import Lean.Util.PPGoal namespace Lean diff --git a/src/Lean/Meta.lean b/src/Lean/Meta.lean index 44f3ed187c..937ceaed0c 100644 --- a/src/Lean/Meta.lean +++ b/src/Lean/Meta.lean @@ -25,3 +25,4 @@ import Lean.Meta.Closure import Lean.Meta.AbstractNestedProofs import Lean.Meta.ForEachExpr import Lean.Meta.Transform +import Lean.Meta.PPGoal diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 4826a663e1..3d0d54ce1a 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -995,7 +995,8 @@ def ppExprImp (e : Expr) : MetaM Format := do let mctx ← getMCtx let lctx ← getLCtx let opts ← getOptions - Lean.ppExpr { env := env, mctx := mctx, lctx := lctx, opts := opts } e + let ctxCore ← readThe Core.Context + Lean.ppExpr { env := env, mctx := mctx, lctx := lctx, opts := opts, currNamespace := ctxCore.currNamespace, openDecls := ctxCore.openDecls } e def ppExpr (e : Expr) : m Format := liftMetaM $ ppExprImp e diff --git a/src/Lean/Util/PPGoal.lean b/src/Lean/Meta/PPGoal.lean similarity index 65% rename from src/Lean/Util/PPGoal.lean rename to src/Lean/Meta/PPGoal.lean index 61acec3c14..bbeae2b1d4 100644 --- a/src/Lean/Util/PPGoal.lean +++ b/src/Lean/Meta/PPGoal.lean @@ -3,9 +3,9 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ -import Lean.Util.PPExt +import Lean.Meta.Basic -namespace Lean +namespace Lean.Meta def ppAuxDeclsDefault := false builtin_initialize @@ -13,24 +13,26 @@ builtin_initialize def getAuxDeclsOption (o : Options) : Bool := o.get `pp.auxDecls ppAuxDeclsDefault -def ppGoal (ppCtx : PPContext) (mvarId : MVarId) : IO Format := - let env := ppCtx.env - let mctx := ppCtx.mctx - let opts := ppCtx.opts - match mctx.findDecl? mvarId with +def ppInaccessibleDefault := false +builtin_initialize + registerOption `pp.inaccessible { defValue := ppInaccessibleDefault, group := "pp", descr := "display inaccessible declarations in the local context" } +def getInaccessibleOption (o : Options) : Bool := + o.get `pp.inaccessible ppInaccessibleDefault + +def ppGoal (mvarId : MVarId) : MetaM Format := do + match (← getMCtx).findDecl? mvarId with | none => pure "unknown goal" | some mvarDecl => do - let indent := 2 -- Use option - let ppAuxDecls := getAuxDeclsOption opts - let lctx := mvarDecl.lctx - let lctx := lctx.sanitizeNames.run' { options := opts } - let ppCtx := { ppCtx with lctx := lctx } - let pp (e : Expr) : IO Format := ppExpr ppCtx e - let instMVars (e : Expr) : Expr := mctx.instantiateMVars e |>.1 + let indent := 2 -- Use option + let ppAuxDecls := getAuxDeclsOption (← getOptions) + let ppInaccessible := getInaccessibleOption (← getOptions) + let lctx := mvarDecl.lctx + let lctx := lctx.sanitizeNames.run' { options := (← getOptions) } + withLCtx lctx mvarDecl.localInstances do let addLine (fmt : Format) : Format := if fmt.isNil then fmt else fmt ++ Format.line -- The followint two `let rec`s are being used to control the generated code size. -- Then should be remove after we rewrite the compiler in Lean - let rec pushPending (ids : List Name) (type? : Option Expr) (fmt : Format) : IO Format := + let rec pushPending (ids : List Name) (type? : Option Expr) (fmt : Format) : MetaM Format := if ids.isEmpty then pure fmt else @@ -39,13 +41,13 @@ def ppGoal (ppCtx : PPContext) (mvarId : MVarId) : IO Format := | [], _ => pure fmt | _, none => pure fmt | _, some type => do - let typeFmt ← pp type + let typeFmt ← ppExpr type pure $ fmt ++ (Format.joinSep ids.reverse " " ++ " :" ++ Format.nest indent (Format.line ++ typeFmt)).group - let rec ppVars (varNames : List Name) (prevType? : Option Expr) (fmt : Format) (localDecl : LocalDecl) : IO (List Name × Option Expr × Format) := do + let rec ppVars (varNames : List Name) (prevType? : Option Expr) (fmt : Format) (localDecl : LocalDecl) : MetaM (List Name × Option Expr × Format) := do match localDecl with | LocalDecl.cdecl _ _ varName type _ => let varName := varName.simpMacroScopes - let type := instMVars type + let type ← instantiateMVars type if prevType? == none || prevType? == some type then pure (varName :: varNames, some type, fmt) else do @@ -55,10 +57,10 @@ def ppGoal (ppCtx : PPContext) (mvarId : MVarId) : IO Format := let varName := varName.simpMacroScopes let fmt ← pushPending varNames prevType? fmt let fmt := addLine fmt - let type := instMVars type - let val := instMVars val - let typeFmt ← pp type - let valFmt ← pp val + let type ← instantiateMVars type + let val ← instantiateMVars val + let typeFmt ← ppExpr type + let valFmt ← ppExpr val let fmt := fmt ++ (format varName ++ " : " ++ typeFmt ++ " :=" ++ Format.nest indent (Format.line ++ valFmt)).group pure ([], none, fmt) let (varNames, type?, fmt) ← lctx.foldlM (init := ([], none, Format.nil)) fun (varNames, prevType?, fmt) (localDecl : LocalDecl) => @@ -68,10 +70,10 @@ def ppGoal (ppCtx : PPContext) (mvarId : MVarId) : IO Format := ppVars varNames prevType? fmt localDecl let fmt ← pushPending varNames type? fmt let fmt := addLine fmt - let typeFmt ← pp mvarDecl.type + let typeFmt ← ppExpr mvarDecl.type let fmt := fmt ++ "⊢" ++ " " ++ Format.nest indent typeFmt match mvarDecl.userName with | Name.anonymous => pure fmt - | name => pure $ "case " ++ format name.eraseMacroScopes ++ Format.line ++ fmt + | name => return "case " ++ format name.eraseMacroScopes ++ Format.line ++ fmt -end Lean +end Lean.Meta diff --git a/src/Lean/Meta/Tactic/Util.lean b/src/Lean/Meta/Tactic/Util.lean index 8477910d7b..994d5ee7f1 100644 --- a/src/Lean/Meta/Tactic/Util.lean +++ b/src/Lean/Meta/Tactic/Util.lean @@ -6,6 +6,7 @@ Authors: Leonardo de Moura import Lean.Meta.Basic import Lean.Meta.AppBuilder import Lean.Meta.LevelDefEq +import Lean.Meta.PPGoal namespace Lean.Meta @@ -42,9 +43,6 @@ def getMVarType (mvarId : MVarId) : MetaM Expr := do def getMVarType' (mvarId : MVarId) : MetaM Expr := do whnf (← instantiateMVars (← getMVarDecl mvarId).type) -def ppGoal (mvarId : MVarId) : MetaM Format := do - Lean.ppGoal { env := (← getEnv), mctx := (← getMCtx), opts := (← getOptions) } mvarId - builtin_initialize registerTraceClass `Meta.Tactic /-- Assign `mvarId` to `sorryAx` -/ diff --git a/src/Lean/PrettyPrinter.lean b/src/Lean/PrettyPrinter.lean index 56811184a3..d44e3f4393 100644 --- a/src/Lean/PrettyPrinter.lean +++ b/src/Lean/PrettyPrinter.lean @@ -12,10 +12,10 @@ import Lean.ParserCompiler namespace Lean def PPContext.runCoreM {α : Type} (ppCtx : PPContext) (x : CoreM α) : IO α := - Prod.fst <$> x.toIO { options := ppCtx.opts } { env := ppCtx.env } + Prod.fst <$> x.toIO { options := ppCtx.opts, currNamespace := ppCtx.currNamespace, openDecls := ppCtx.openDecls } { env := ppCtx.env } def PPContext.runMetaM {α : Type} (ppCtx : PPContext) (x : MetaM α) : IO α := - ppCtx.runCoreM $ x.run' { lctx := ppCtx.lctx } { mctx := ppCtx.mctx } + ppCtx.runCoreM <| x.run' { lctx := ppCtx.lctx } { mctx := ppCtx.mctx } namespace PrettyPrinter @@ -60,8 +60,9 @@ private def withoutContext {m} [MonadExcept Exception m] (x : m Format) : m Form builtin_initialize ppFnsRef.set { - ppExpr := fun ctx e => ctx.runMetaM $ withoutContext $ ppExpr ctx.currNamespace ctx.openDecls e, - ppTerm := fun ctx stx => ctx.runCoreM $ withoutContext $ ppTerm stx, + ppExpr := fun ctx e => ctx.runMetaM $ withoutContext $ ppExpr ctx.currNamespace ctx.openDecls e, + ppTerm := fun ctx stx => ctx.runCoreM $ withoutContext $ ppTerm stx, + ppGoal := fun ctx mvarId => ctx.runMetaM $ withoutContext $ Meta.ppGoal mvarId } builtin_initialize diff --git a/src/Lean/Util.lean b/src/Lean/Util.lean index 24177c3f0f..e15f1cbdaf 100644 --- a/src/Lean/Util.lean +++ b/src/Lean/Util.lean @@ -9,7 +9,6 @@ import Lean.Util.CollectMVars import Lean.Util.FindMVar import Lean.Util.MonadCache import Lean.Util.PPExt -import Lean.Util.PPGoal import Lean.Util.Path import Lean.Util.Profile import Lean.Util.RecDepth diff --git a/src/Lean/Util/PPExt.lean b/src/Lean/Util/PPExt.lean index 4e06805fc7..d74e3ae7c2 100644 --- a/src/Lean/Util/PPExt.lean +++ b/src/Lean/Util/PPExt.lean @@ -19,40 +19,45 @@ def getSyntaxMaxDepth (opts : Options) : Nat := def getPPRaw (opts : Options) : Bool := opts.getBool `pp.raw false -structure PPContext := - (env : Environment) - (mctx : MetavarContext := {}) - (lctx : LocalContext := {}) - (opts : Options := {}) - (currNamespace : Name := Name.anonymous) - (openDecls : List OpenDecl := []) +structure PPContext where + env : Environment + mctx : MetavarContext := {} + lctx : LocalContext := {} + opts : Options := {} + currNamespace : Name := Name.anonymous + openDecls : List OpenDecl := [] -structure PPFns := - (ppExpr : PPContext → Expr → IO Format) - (ppTerm : PPContext → Syntax → IO Format) +structure PPFns where + ppExpr : PPContext → Expr → IO Format + ppTerm : PPContext → Syntax → IO Format + ppGoal : PPContext → MVarId → IO Format -instance : Inhabited PPFns := ⟨⟨arbitrary, arbitrary⟩⟩ +instance : Inhabited PPFns := ⟨⟨arbitrary, arbitrary, arbitrary⟩⟩ builtin_initialize ppFnsRef : IO.Ref PPFns ← IO.mkRef { - ppExpr := fun ctx e => pure $ format (toString e), - ppTerm := fun ctx stx => pure $ stx.formatStx (getSyntaxMaxDepth ctx.opts), + ppExpr := fun ctx e => return format (toString e), + ppTerm := fun ctx stx => return stx.formatStx (getSyntaxMaxDepth ctx.opts) + ppGoal := fun ctx mvarId => return "goal" } builtin_initialize ppExt : EnvExtension PPFns ← - registerEnvExtension $ ppFnsRef.get + registerEnvExtension ppFnsRef.get def ppExpr (ctx : PPContext) (e : Expr) : IO Format := let e := ctx.mctx.instantiateMVars e |>.1 if getPPRaw ctx.opts then - pure $ format (toString e) + return format (toString e) else - (ppExt.getState ctx.env).ppExpr ctx e + ppExt.getState ctx.env |>.ppExpr ctx e def ppTerm (ctx : PPContext) (stx : Syntax) : IO Format := if getPPRaw ctx.opts then - pure $ stx.formatStx (getSyntaxMaxDepth ctx.opts) + return stx.formatStx (getSyntaxMaxDepth ctx.opts) else - (ppExt.getState ctx.env).ppTerm ctx stx + ppExt.getState ctx.env |>.ppTerm ctx stx + +def ppGoal (ctx : PPContext) (mvarId : MVarId) : IO Format := + ppExt.getState ctx.env |>.ppGoal ctx mvarId end Lean