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

feat: hierarchical InfoTree

Browse source
This commit is contained in:
Leonardo de Moura 2021-01-09 14:07:32 -08:00
parent 9576f4a390
commit 873634be7e
8 changed files with 302 additions and 129 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/Init/Data/Format/Basic.lean
View file

@ -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

27
src/Lean/Elab/Command.lean
View file

@ -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

226
src/Lean/Elab/InfoTree.lean
View file

@ -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 "<context-not-available>"
| 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
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

15
src/Lean/Elab/SyntheticMVars.lean
View file

@ -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

93
src/Lean/Elab/Tactic/Basic.lean
View file

@ -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 }

32
src/Lean/Elab/Term.lean
View file

@ -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

6
src/Lean/Server/FileWorker.lean
View file

@ -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}"

23
tests/lean/run/infoTree.lean Normal file
View file

@ -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!