From 873634be7e22745b87affafb37622b727252cb98 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 9 Jan 2021 14:07:32 -0800 Subject: [PATCH] feat: hierarchical `InfoTree` --- src/Init/Data/Format/Basic.lean | 9 +- src/Lean/Elab/Command.lean | 27 +++- src/Lean/Elab/InfoTree.lean | 226 ++++++++++++++++++++++-------- src/Lean/Elab/SyntheticMVars.lean | 15 +- src/Lean/Elab/Tactic/Basic.lean | 93 ++++++------ src/Lean/Elab/Term.lean | 32 +++-- src/Lean/Server/FileWorker.lean | 6 +- tests/lean/run/infoTree.lean | 23 +++ 8 files changed, 302 insertions(+), 129 deletions(-) create mode 100644 tests/lean/run/infoTree.lean diff --git a/src/Init/Data/Format/Basic.lean b/src/Init/Data/Format/Basic.lean index 4212d3b4b2..999480411c 100644 --- a/src/Init/Data/Format/Basic.lean +++ b/src/Init/Data/Format/Basic.lean @@ -174,6 +174,12 @@ def defIndent := 2 def defUnicode := true def defWidth := 120 +def nestD (f : Format) : Format := + nest defIndent f + +def indentD (f : Format) : Format := + nestD (Format.line ++ f) + @[export lean_format_pretty] def pretty (f : Format) (w : Nat := defWidth) : String := let (_, st) := be w [{ flb := FlattenBehavior.allOrNone, flatten := false, items := [{ f := f, indent := 0 }] }] {}; @@ -209,6 +215,3 @@ def Format.joinSuffix {α : Type u} [ToFormat α] : List α → Format → Forma | a::as, suffix => format a ++ suffix ++ joinSuffix as suffix end Std - -open Std -open Std.Format diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index f846d03171..5784b2f26a 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -64,6 +64,10 @@ def addLinter (l : Linter) : IO Unit := do let ls ← lintersRef.get lintersRef.set (ls.push l) +instance : MonadInfoTree CommandElabM where + getInfoState := return (← get).infoState + modifyInfoState f := modify fun s => { s with infoState := f s.infoState } + instance : MonadEnv CommandElabM where getEnv := do pure (← get).env modifyEnv f := modify fun s => { s with env := f s.env } @@ -257,6 +261,12 @@ private def mkTermContext (ctx : Context) (s : State) (declName? : Option Name) currMacroScope := ctx.currMacroScope declName? := declName? } +private def mkTermState (scope : Scope) (s : State) : Term.State := { + messages := {} + levelNames := scope.levelNames + infoState.enabled := s.infoState.enabled +} + private def addTraceAsMessages (ctx : Context) (log : MessageLog) (traceState : TraceState) : MessageLog := traceState.traces.foldl (fun (log : MessageLog) traceElem => @@ -271,16 +281,19 @@ def liftTermElabM {α} (declName? : Option Name) (x : TermElabM α) : CommandEla let scope := s.scopes.head! -- We execute `x` with an empty message log. Thus, `x` cannot modify/view messages produced by previous commands. -- This is useful for implementing `runTermElabM` where we use `Term.resetMessageLog` - let x : MetaM _ := (observing x).run (mkTermContext ctx s declName?) { messages := {}, levelNames := scope.levelNames } + let x : MetaM _ := (observing x).run (mkTermContext ctx s declName?) (mkTermState scope s) let x : CoreM _ := x.run mkMetaContext {} let x : EIO _ _ := x.run (mkCoreContext ctx s) { env := s.env, ngen := s.ngen, nextMacroScope := s.nextMacroScope } - let (((ea, termS), _), coreS) ← liftEIO x + let (((ea, termS), metaS), coreS) ← liftEIO x + let infoTrees := termS.infoState.trees.map fun tree => + let tree := tree.substitute termS.infoState.assignment + InfoTree.context { env := coreS.env, mctx := metaS.mctx, currNamespace := scope.currNamespace, openDecls := scope.openDecls, options := scope.opts } tree modify fun s => { s with - env := coreS.env - messages := addTraceAsMessages ctx (s.messages ++ termS.messages) coreS.traceState - nextMacroScope := coreS.nextMacroScope - ngen := coreS.ngen - infoState := { s.infoState with trees := s.infoState.trees.append termS.infoState.trees } + env := coreS.env + messages := addTraceAsMessages ctx (s.messages ++ termS.messages) coreS.traceState + nextMacroScope := coreS.nextMacroScope + ngen := coreS.ngen + infoState.trees := s.infoState.trees.append infoTrees } match ea with | Except.ok a => pure a diff --git a/src/Lean/Elab/InfoTree.lean b/src/Lean/Elab/InfoTree.lean index 261f08e275..da26b37f60 100644 --- a/src/Lean/Elab/InfoTree.lean +++ b/src/Lean/Elab/InfoTree.lean @@ -2,76 +2,70 @@ Copyright (c) 2020 Wojciech Nawrocki. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Wojciech Nawrocki +Authors: Wojciech Nawrocki, Leonardo de Moura -/ import Lean.Data.Position import Lean.Expr import Lean.Message import Lean.Data.Json +import Lean.Meta.Basic +import Lean.Meta.PPGoal namespace Lean.Elab -open Std (PersistentArray PersistentArray.empty) +open Std (PersistentArray PersistentArray.empty PersistentHashMap) -/-- A (go-to-def clickable) link to a source module -/ -structure SrcLink where - modName : Name := `MyMod - srcPos : String.Pos := 0 - srcEndPos : String.Pos := 0 +/- Context after executing `liftTermElabM`. + Note that the term information collected during elaboration may contain metavariables, and their + assignments are stored at `mctx`. -/ +structure ContextInfo where + env : Environment + mctx : MetavarContext := {} + options : Options := {} + currNamespace : Name := Name.anonymous + openDecls : List OpenDecl := [] deriving Inhabited -/-- An elaborated term -/ structure TermInfo where - /- Elaboratad expression -/ - e : Expr - stx : Syntax - srcLink? : Option SrcLink := none + lctx : LocalContext -- The local context when the term was elaborated. + expr : Expr + stx : Syntax deriving Inhabited -structure TacticState +/- We store the list of goals before and after the execution of a tactic. + We also store the metavariable context at each time since, we want to unassigned metavariables + at tactic execution time to be displayed as `?m...`. -/ +structure TacticInfo where + mctxBefore : MetavarContext + goalsBefore : List MVarId + stx : Syntax + mctxAfter : MetavarContext + goalsAfter : List MVarId + deriving Inhabited -structure MacroExpansionInfo +structure MacroExpansionInfo where + lctx : LocalContext -- The local context when the macro was expanded. + before : Syntax + after : Syntax + deriving Inhabited -/-- Tree of semantic information about a term or command. -See `MessageData` for a similar type used for messages. -/ -inductive InfoTree +inductive Info where + | ofTacticInfo (i : TacticInfo) | ofTermInfo (i : TermInfo) - -- NOTE(WN): perhaps withContext carries the same information and this is redundant? - | ofTacticState (s : TacticState) - | ofJson (j : Json) -- For user data - | withContext (ctx : MessageDataContext) (t : InfoTree) - | withNamingContext (nctx : NamingContext) (t : InfoTree) - | withMacro (m : MacroExpansionInfo) (t : InfoTree) - | node (k : SyntaxNodeKind) (args : PersistentArray InfoTree) + | ofMacroExpansionInfo (i : MacroExpansionInfo) deriving Inhabited -namespace InfoTree - -open MessageData in -partial def formatAux : NamingContext → Option MessageDataContext → InfoTree → IO Format - | nCtx, some ctx, ofTermInfo i => ppExpr (mkPPContext nCtx ctx) i.e - | nCtx, none, ofTermInfo i => pure s!"({i.e})" - | _, _, ofTacticState .. => pure "⊢" - | _, _, ofJson j => pure <| toString j - | nCtx, _, withContext ctx d => formatAux nCtx ctx d - | _, ctx?, withNamingContext nCtx d => formatAux nCtx ctx? d - | nCtx, ctx?, withMacro m t => do let t ← formatAux nCtx ctx? t; pure s!"(withMacro (..) {t})" - | nCtx, ctx, node k args => do - let ts ← Format.nest 2 <$> args.foldlM (fun r t => do let t ← formatAux nCtx ctx t; pure $ r ++ Format.line ++ t) Format.nil - return (toString k) ++ Format.line ++ ts - -protected def format (t : InfoTree) : IO Format := - formatAux { currNamespace := Name.anonymous, openDecls := [] } none t - -protected def toString (t : InfoTree) : IO String := do - let fmt ← t.format - pure $ toString fmt - -end InfoTree +inductive InfoTree where + | context (i : ContextInfo) (t : InfoTree) -- The context object is created by `liftTermElabM` at `Command.lean` + | node (i : Info) (children : PersistentArray InfoTree) -- The children contains information for nested term elaboration and tactic evaluation + | ofJson (j : Json) -- For user data + | hole (mvarId : MVarId) -- The elaborator creates holes (aka metavariables) for tactics and postponed terms + deriving Inhabited structure InfoState where - enabled : Bool := true - trees : PersistentArray InfoTree := {} -- NOTE(WN): Just a flat array in this experiment + enabled : Bool := false + assignment : PersistentHashMap MVarId InfoTree := {} -- map from holeId to InfoTree + trees : PersistentArray InfoTree := {} deriving Inhabited class MonadInfoTree (m : Type → Type) where @@ -84,21 +78,135 @@ instance (m n) [MonadInfoTree m] [MonadLift m n] : MonadInfoTree n where getInfoState := liftM (getInfoState : m _) modifyInfoState f := liftM (modifyInfoState f : m _) +partial def InfoTree.substitute (tree : InfoTree) (assignment : PersistentHashMap MVarId InfoTree) : InfoTree := + match tree with + | node i c => node i <| c.map (substitute · assignment) + | context i t => context i (substitute t assignment) + | ofJson j => ofJson j + | hole id => match assignment.find? id with + | none => hole id + | some tree => substitute tree assignment + +def ContextInfo.runMetaM (info : ContextInfo) (lctx : LocalContext) (x : MetaM α) : IO α := do + let x := x.run { lctx := lctx } { mctx := info.mctx } + let ((a, _), _) ← x.toIO { options := info.options, currNamespace := info.currNamespace, openDecls := info.openDecls } { env := info.env } + return a + +def ContextInfo.toPPContext (info : ContextInfo) (lctx : LocalContext) : PPContext := + { env := info.env, mctx := info.mctx, lctx := lctx, + opts := info.options, currNamespace := info.currNamespace, openDecls := info.openDecls } + +def ContextInfo.ppSyntax (info : ContextInfo) (lctx : LocalContext) (stx : Syntax) : IO Format := do + ppTerm (info.toPPContext lctx) stx + +def TermInfo.format (cinfo : ContextInfo) (info : TermInfo) : IO Format := do + cinfo.runMetaM info.lctx do + return f!"{← Meta.ppExpr info.expr} : {← Meta.ppExpr (← Meta.inferType info.expr)}" + +def ContextInfo.ppGoals (cinfo : ContextInfo) (goals : List MVarId) : IO Format := + if goals.isEmpty then + return "no goals" + else + cinfo.runMetaM {} (return Std.Format.prefixJoin "\n" (← goals.mapM Meta.ppGoal)) + +def TacticInfo.format (cinfo : ContextInfo) (info : TacticInfo) : IO Format := do + let cinfoB := { cinfo with mctx := info.mctxBefore } + let cinfoA := { cinfo with mctx := info.mctxAfter } + let goalsBefore ← cinfoB.ppGoals info.goalsBefore + let goalsAfter ← cinfoA.ppGoals info.goalsAfter + return f!"Tactic\nbefore {goalsBefore}\nafter {goalsAfter}" + +def MacroExpansionInfo.format (cinfo : ContextInfo) (info : MacroExpansionInfo) : IO Format := do + let before ← cinfo.ppSyntax info.lctx info.before + let after ← cinfo.ppSyntax info.lctx info.after + return f!"Macro expansion\n{before}\n===>\n{after}" + +def Info.format (cinfo : ContextInfo) : Info → IO Format + | ofTacticInfo i => i.format cinfo + | ofTermInfo i => i.format cinfo + | ofMacroExpansionInfo i => i.format cinfo + +partial def InfoTree.format (tree : InfoTree) (cinfo? : Option ContextInfo := none) : IO Format := do + match tree with + | ofJson j => return toString j + | hole id => return toString id + | context i t => format t i + | node i cs => match cinfo? with + | none => return "" + | some cinfo => + if cs.size == 0 then + i.format cinfo + else + return f!"{← i.format cinfo}{Std.Format.nestD <| Std.Format.prefixJoin "\n" (← cs.toList.mapM fun c => format c cinfo?)}" + section variables [Monad m] [MonadInfoTree m] -def modifyInfoTrees (f : PersistentArray InfoTree → PersistentArray InfoTree) - : m Unit := - modifyInfoState (fun s => { s with trees := f s.trees }) +@[inline] private def modifyInfoTrees (f : PersistentArray InfoTree → PersistentArray InfoTree) : m Unit := + modifyInfoState fun s => { s with trees := f s.trees } + +private def getResetInfoTrees : m (PersistentArray InfoTree) := do + let trees := (← getInfoState).trees + modifyInfoTrees fun _ => {} + return trees def pushInfoTree (t : InfoTree) : m Unit := do - if (←getInfoState).enabled then - modifyInfoTrees (fun ts => ts.push t) - pure () + if (← getInfoState).enabled then + modifyInfoTrees fun ts => ts.push t -def mkInfoNode (k : SyntaxNodeKind) : m Unit := do - if (←getInfoState).enabled then - modifyInfoTrees (fun ts => PersistentArray.empty.push <| InfoTree.node k ts) +def mkInfoNode (info : Info) : m Unit := do + if (← getInfoState).enabled then + modifyInfoTrees fun ts => PersistentArray.empty.push <| InfoTree.node info ts + +@[inline] def withInfoContext' [MonadFinally m] (x : m α) (mkInfo : α → m (Sum Info MVarId)) : m α := do + if (← getInfoState).enabled then + let treesSaved ← getResetInfoTrees + Prod.fst <$> MonadFinally.tryFinally' x fun a? => do + match a? with + | none => modifyInfoTrees fun _ => treesSaved + | some a => modifyInfoTrees fun trees => + match (← mkInfo a) with + | Sum.inl info => treesSaved.push <| InfoTree.node info trees + | Sum.inr mvaId => treesSaved.push <| InfoTree.hole mvaId + else + x + +@[inline] def withInfoContext [MonadFinally m] (x : m α) (mkInfo : m Info) : m α := + withInfoContext' x fun _ => return Sum.inl (← mkInfo) + +def getInfoHoleIdAssignment? (mvarId : MVarId) : m (Option InfoTree) := + return (← getInfoState).assignment[mvarId] + +def assignInfoHoleId (mvarId : MVarId) (infoTree : InfoTree) : m Unit := do + assert! (← getInfoHoleIdAssignment? mvarId).isNone + modifyInfoState fun s => { s with assignment := s.assignment.insert mvarId infoTree } end -end Lean.Elab \ No newline at end of file +def withMacroExpansionInfo [MonadFinally m] [Monad m] [MonadInfoTree m] [MonadLCtx m] (before after : Syntax) (x : m α) : m α := + let mkInfo : m Info := do + return Info.ofMacroExpansionInfo { + lctx := (← getLCtx) + before := before + after := after + } + withInfoContext x mkInfo + +@[inline] def withInfoHole [MonadFinally m] [Monad m] [MonadInfoTree m] (mvarId : MVarId) (x : m α) : m α := do + if (← getInfoState).enabled then + let treesSaved ← getResetInfoTrees + Prod.fst <$> MonadFinally.tryFinally' x fun a? => do + match a? with + | none => modifyInfoTrees fun _ => treesSaved + | some a => modifyInfoState fun s => + assert! s.trees.size == 1 -- if size is not one, then API is being misused. + { s with trees := treesSaved, assignment := s.assignment.insert mvarId s.trees[0] } + else + x + +def enableInfoTree [MonadInfoTree m] (flag := true) : m Unit := + modifyInfoState fun s => { s with enabled := flag } + +def getInfoTrees [MonadInfoTree m] [Monad m] : m (PersistentArray InfoTree) := + return (← getInfoState).trees + +end Lean.Elab diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean index 1bbd093d64..722fae2190 100644 --- a/src/Lean/Elab/SyntheticMVars.lean +++ b/src/Lean/Elab/SyntheticMVars.lean @@ -26,7 +26,7 @@ def runTactic (mvarId : MVarId) (tacticCode : Syntax) : TermElabM Unit := do We store the `by` because in the future we want to save the initial state information at the `by` position. -/ let code := tacticCode[1] modifyThe Meta.State fun s => { s with mctx := s.mctx.instantiateMVarDeclMVars mvarId } - let remainingGoals ← liftTacticElabM mvarId do evalTactic code; getUnsolvedGoals + let remainingGoals ← withInfoHole mvarId do liftTacticElabM mvarId do evalTactic code; getUnsolvedGoals unless remainingGoals.isEmpty do reportUnsolvedGoals remainingGoals /-- Auxiliary function used to implement `synthesizeSyntheticMVars`. -/ @@ -46,12 +46,13 @@ private def resumePostponed (macroStack : MacroStack) (declName? : Option Name) withReader (fun ctx => { ctx with macroStack := macroStack, declName? := declName? }) do let mvarDecl ← getMVarDecl mvarId let expectedType ← instantiateMVars mvarDecl.type - let result ← resumeElabTerm stx expectedType (!postponeOnError) - /- We must ensure `result` has the expected type because it is the one expected by the method that postponed stx. - That is, the method does not have an opportunity to check whether `result` has the expected type or not. -/ - let result ← withRef stx $ ensureHasType expectedType result - assignExprMVar mvarId result - pure true + withInfoHole mvarId do + let result ← resumeElabTerm stx expectedType (!postponeOnError) + /- We must ensure `result` has the expected type because it is the one expected by the method that postponed stx. + That is, the method does not have an opportunity to check whether `result` has the expected type or not. -/ + let result ← withRef stx $ ensureHasType expectedType result + assignExprMVar mvarId result + pure true catch | ex@(Exception.internal id _) => if id == postponeExceptionId then diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean index 6398c777a1..a41ce823ad 100644 --- a/src/Lean/Elab/Tactic/Basic.lean +++ b/src/Lean/Elab/Tactic/Basic.lean @@ -110,58 +110,73 @@ private def evalTacticUsing (s : SavedState) (stx : Syntax) (tactics : List Tact throw ex loop tactics -/- Elaborate `x` with `stx` on the macro stack -/ -@[inline] -def withMacroExpansion {α} (beforeStx afterStx : Syntax) (x : TacticM α) : TacticM α := - withTheReader Term.Context (fun ctx => { ctx with macroStack := { before := beforeStx, after := afterStx } :: ctx.macroStack }) x +def getGoals : TacticM (List MVarId) := do pure (← get).goals mutual -partial def expandTacticMacroFns (stx : Syntax) (macros : List Macro) : TacticM Unit := - let rec loop : List Macro → TacticM Unit - | [] => throwErrorAt! stx "tactic '{stx.getKind}' has not been implemented" - | m::ms => do - let scp ← getCurrMacroScope - try - let stx' ← adaptMacro m stx - evalTactic stx' - catch ex => - if ms.isEmpty then throw ex - loop ms - loop macros + partial def expandTacticMacroFns (stx : Syntax) (macros : List Macro) : TacticM Unit := + let rec loop : List Macro → TacticM Unit + | [] => throwErrorAt! stx "tactic '{stx.getKind}' has not been implemented" + | m::ms => do + let scp ← getCurrMacroScope + try + let stx' ← adaptMacro m stx + evalTactic stx' + catch ex => + if ms.isEmpty then throw ex + loop ms + loop macros -partial def expandTacticMacro (stx : Syntax) : TacticM Unit := do - let k := stx.getKind - let table := (macroAttribute.ext.getState (← getEnv)).table - let macroFns := (table.find? k).getD [] - expandTacticMacroFns stx macroFns + partial def expandTacticMacro (stx : Syntax) : TacticM Unit := do + let k := stx.getKind + let table := (macroAttribute.ext.getState (← getEnv)).table + let macroFns := (table.find? k).getD [] + expandTacticMacroFns stx macroFns -partial def evalTactic : Syntax → TacticM Unit - | stx => withRef stx $ withIncRecDepth $ withFreshMacroScope $ match stx with - | Syntax.node k args => - if k == nullKind then - -- Macro writers create a sequence of tactics `t₁ ... tₙ` using `mkNullNode #[t₁, ..., tₙ]` - stx.getArgs.forM evalTactic - else do - trace `Elab.step fun _ => stx - let env ← getEnv - let s ← saveAllState - let table := (tacticElabAttribute.ext.getState env).table - let k := stx.getKind - match table.find? k with - | some evalFns => evalTacticUsing s stx evalFns - | none => expandTacticMacro stx - | _ => throwError "unexpected command" + partial def evalTacticAux (stx : Syntax) : TacticM Unit := + withRef stx $ withIncRecDepth $ withFreshMacroScope $ match stx with + | Syntax.node k args => + if k == nullKind then + -- Macro writers create a sequence of tactics `t₁ ... tₙ` using `mkNullNode #[t₁, ..., tₙ]` + stx.getArgs.forM evalTactic + else do + trace `Elab.step fun _ => stx + let env ← getEnv + let s ← saveAllState + let table := (tacticElabAttribute.ext.getState env).table + let k := stx.getKind + match table.find? k with + | some evalFns => evalTacticUsing s stx evalFns + | none => expandTacticMacro stx + | _ => throwError "unexpected command" + + partial def mkTacticInfo (mctxBefore : MetavarContext) (goalsBefore : List MVarId) (stx : Syntax) : TacticM Info := + return Info.ofTacticInfo { + mctxBefore := mctxBefore + goalsBefore := goalsBefore + stx := stx + mctxAfter := (← getMCtx) + goalsAfter := (← getGoals) + } + + partial def evalTactic (stx : Syntax) : TacticM Unit := do + let mctxBefore ← getMCtx + let goalsBefore ← getGoals + withInfoContext (evalTacticAux stx) (mkTacticInfo mctxBefore goalsBefore stx) end +/- Elaborate `x` with `stx` on the macro stack -/ +@[inline] +def withMacroExpansion {α} (beforeStx afterStx : Syntax) (x : TacticM α) : TacticM α := + withMacroExpansionInfo beforeStx afterStx do + withTheReader Term.Context (fun ctx => { ctx with macroStack := { before := beforeStx, after := afterStx } :: ctx.macroStack }) x + /-- Adapt a syntax transformation to a regular tactic evaluator. -/ def adaptExpander (exp : Syntax → TacticM Syntax) : Tactic := fun stx => do let stx' ← exp stx withMacroExpansion stx stx' $ evalTactic stx' -def getGoals : TacticM (List MVarId) := do pure (← get).goals - def setGoals (gs : List MVarId) : TacticM Unit := modify $ fun s => { s with goals := gs } def appendGoals (gs : List MVarId) : TacticM Unit := modify $ fun s => { s with goals := s.goals ++ gs } diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 684d4374e8..d657541f04 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -257,8 +257,8 @@ instance : MonadQuotation TermElabM where withFreshMacroScope := Term.withFreshMacroScope instance : MonadInfoTree TermElabM where - getInfoState := (·.infoState) <$> get - modifyInfoState f := modify (fun s => { s with infoState := f s.infoState }) + getInfoState := return (← get).infoState + modifyInfoState f := modify fun s => { s with infoState := f s.infoState } unsafe def mkTermElabAttributeUnsafe : IO (KeyedDeclsAttribute TermElab) := mkElabAttribute TermElab `Lean.Elab.Term.termElabAttribute `builtinTermElab `termElab `Lean.Parser.Term `Lean.Elab.Term.TermElab "term" @@ -341,7 +341,8 @@ def elabLevel (stx : Syntax) : TermElabM Level := /- Elaborate `x` with `stx` on the macro stack -/ @[inline] def withMacroExpansion {α} (beforeStx afterStx : Syntax) (x : TermElabM α) : TermElabM α := - withReader (fun ctx => { ctx with macroStack := { before := beforeStx, after := afterStx } :: ctx.macroStack }) x + withMacroExpansionInfo beforeStx afterStx do + withReader (fun ctx => { ctx with macroStack := { before := beforeStx, after := afterStx } :: ctx.macroStack }) x /- Add the given metavariable to the list of pending synthetic metavariables. @@ -986,6 +987,20 @@ private partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone : | some expectedType => elabImplicitLambda stx catchExPostpone expectedType #[] | none => elabUsingElabFns stx expectedType? catchExPostpone +def mkTermInfo (stx : Syntax) (e : Expr) : TermElabM (Sum Info MVarId) := do + let isHole? : TermElabM (Option MVarId) := do + match e with + | Expr.mvar mvarId _ => + let isHole := (← get).syntheticMVars.any fun d => match d.kind with + | SyntheticMVarKind.tactic .. => true + | SyntheticMVarKind.postponed .. => true + | _ => false + if isHole then pure mvarId else pure none + | _ => pure none + match (← isHole?) with + | none => return Sum.inl <| Info.ofTermInfo { lctx := (← getLCtx), expr := e, stx := stx } + | some mvarId => return Sum.inr mvarId + /-- Main function for elaborating terms. It extracts the elaboration methods from the environment using the node kind. @@ -1000,16 +1015,7 @@ private partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone : The option `catchExPostpone == false` is used to implement `resumeElabTerm` to prevent the creation of another synthetic metavariable when resuming the elaboration. -/ def elabTerm (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone := true) : TermElabM Expr := - withRef stx do - let e ← elabTermAux expectedType? catchExPostpone true stx - -- HACK(WN) - let eType ← inferType e - if !eType.hasExprMVar then - pushInfoTree <| InfoTree.ofTermInfo { - e := eType -- NOTE(WN): just e here is better, we can infer the type on demand in the server - stx := stx - } - e + withInfoContext' (withRef stx <| elabTermAux expectedType? catchExPostpone true stx) (mkTermInfo stx) def elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone := true) (errorMsgHeader? : Option String := none) : TermElabM Expr := do let e ← elabTerm stx expectedType? catchExPostpone diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index 172c6d8436..26e2855d1c 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -273,14 +273,18 @@ section RequestHandling | Except.error TaskError.eof => pure $ Except.ok none | Except.ok (some snap) => do - let mut infoRanges := #[] + /- TODO: FIX -/ + let mut infoRanges : Array (Nat × String.Pos × String.Pos × Expr) := #[] for t in snap.toCmdState.infoState.trees do + /- if let Elab.InfoTree.ofTermInfo i := t then match i.stx.getPos, i.stx.getTailPos with | some pos, some endPos => if pos ≤ hoverPos ∧ hoverPos ≤ endPos then infoRanges := infoRanges.push (endPos - pos, pos, endPos, i.e) | _, _ => pure () + -/ + pure () match infoRanges.getMax? fun a b => a.1 > b.1 with | some (_, pos, endPos, e) => --st.hLog.putStrLn s!"Picked from {infoRanges.size}" diff --git a/tests/lean/run/infoTree.lean b/tests/lean/run/infoTree.lean new file mode 100644 index 0000000000..94eb8c2929 --- /dev/null +++ b/tests/lean/run/infoTree.lean @@ -0,0 +1,23 @@ +import Lean + +open Lean.Elab + +elab "enableInfo!" : command => enableInfoTree + +elab "showInfoTrees!" : command => do + let trees ← getInfoTrees + trees.forM fun tree => do + IO.println f!"{← tree.format}" + +enableInfo! + +def f (x : Nat) : Nat × Nat := + let y := ⟨x, x⟩ + id y + +def h : (x : Nat) → x + 0 = x := + fun x => by + simp + exact rfl + +showInfoTrees!