From 96f9ee2a41e7e77ef011009107f5f3671d8a0d6c Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 13 Mar 2025 16:09:00 +0100 Subject: [PATCH] feat: allow async elab tasks to contribute to info trees reported to linters and request handlers (#7457) This PR ensures info tree users such as linters and request handlers have access to info subtrees created by async elab task by introducing API to leave holes filled by such tasks. **Breaking change**: other metaprogramming users of `Command.State.infoState` may need to call `InfoState.substituteLazy` on it manually to fill all holes. --- src/Init.lean | 1 + src/Init/System/IO.lean | 7 +- src/Init/Task.lean | 29 ++++ src/Lean/CoreM.lean | 3 +- src/Lean/Elab/Command.lean | 51 +++--- src/Lean/Elab/Frontend.lean | 4 +- src/Lean/Elab/InfoTree/Main.lean | 8 + src/Lean/Elab/InfoTree/Types.lean | 5 + src/Lean/Elab/InfoTrees.lean | 2 +- src/Lean/Language/Lean.lean | 71 +++++--- src/Lean/Language/Lean/Types.lean | 20 ++- src/Lean/Server/FileWorker/Utils.lean | 4 +- src/Lean/Server/Requests.lean | 7 +- src/Lean/Server/Snapshots.lean | 6 +- .../1018unknowMVarIssue.lean.expected.out | 153 +++++++++--------- tests/lean/binopInfoTree.lean.expected.out | 152 ++++++++--------- 16 files changed, 306 insertions(+), 217 deletions(-) create mode 100644 src/Init/Task.lean diff --git a/src/Init.lean b/src/Init.lean index 2f99ab920c..54792ce061 100644 --- a/src/Init.lean +++ b/src/Init.lean @@ -40,3 +40,4 @@ import Init.Syntax import Init.Internal import Init.Try import Init.BinderNameHint +import Init.Task diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean index 6a70d09000..2e565ee7ac 100644 --- a/src/Init/System/IO.lean +++ b/src/Init/System/IO.lean @@ -137,9 +137,14 @@ def mapTasks (f : List α → BaseIO β) (tasks : List (Task α)) (prio := Task. go tasks [] where go + | [], as => + if sync then + return .pure (← f as.reverse) + else + f as.reverse |>.asTask prio + | [t], as => BaseIO.mapTask (fun a => f (a :: as).reverse) t prio sync | t::ts, as => BaseIO.bindTask t (fun a => go ts (a :: as)) prio sync - | [], as => f as.reverse |>.asTask prio end BaseIO diff --git a/src/Init/Task.lean b/src/Init/Task.lean new file mode 100644 index 0000000000..47f5cc40e0 --- /dev/null +++ b/src/Init/Task.lean @@ -0,0 +1,29 @@ +/- +Copyright (c) 2025 Lean FRO. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sebastian Ullrich + +Additional `Task` definitions. +-/ +prelude +import Init.Core +import Init.Data.List.Basic + +namespace Task + +/-- +Creates a task that, when all `tasks` have finished, computes the result of `f` applied to their +results. +-/ +def mapList (f : List α → β) (tasks : List (Task α)) (prio := Task.Priority.default) + (sync := false) : Task β := + go tasks [] +where + go + | [], as => + if sync then + .pure <| f as.reverse + else + Task.spawn (prio := prio) fun _ => f as.reverse + | [t], as => t.map (fun a => f (a :: as).reverse) prio sync + | t::ts, as => t.bind (fun a => go ts (a :: as)) prio sync diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index 56069eaa38..d61abf1124 100644 --- a/src/Lean/CoreM.lean +++ b/src/Lean/CoreM.lean @@ -462,11 +462,12 @@ def wrapAsyncAsSnapshot (act : Unit → CoreM Unit) (cancelTk? : Option IO.Cance let t ← wrapAsync (cancelTk? := cancelTk?) fun _ => do IO.FS.withIsolatedStreams (isolateStderr := stderrAsMessages.get (← getOptions)) do let tid ← IO.getTID - -- reset trace state and message log so as not to report them twice + -- reset trace/info state and message log so as not to report them twice modify fun st => { st with messages := st.messages.markAllReported traceState := { tid } snapshotTasks := #[] + infoState := {} } try withTraceNode `Elab.async (fun _ => return desc) do diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index aeb0b820e3..e83c3f4d1e 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -226,13 +226,16 @@ private def runCore (x : CoreM α) : CommandElabM α := do } let (ea, coreS) ← liftM x modify fun s => { s with - env := coreS.env - nextMacroScope := coreS.nextMacroScope - ngen := coreS.ngen - infoState.trees := s.infoState.trees.append coreS.infoState.trees - traceState.traces := coreS.traceState.traces.map fun t => { t with ref := replaceRef t.ref ctx.ref } - snapshotTasks := coreS.snapshotTasks - messages := s.messages ++ coreS.messages + env := coreS.env + nextMacroScope := coreS.nextMacroScope + ngen := coreS.ngen + infoState.trees := s.infoState.trees.append coreS.infoState.trees + -- we assume substitution of `assingment` has already happened, but for lazy assignments we only + -- do it at the very end + infoState.lazyAssignment := coreS.infoState.lazyAssignment + traceState.traces := coreS.traceState.traces.map fun t => { t with ref := replaceRef t.ref ctx.ref } + snapshotTasks := coreS.snapshotTasks + messages := s.messages ++ coreS.messages } return ea @@ -299,20 +302,20 @@ Interrupt and abort exceptions are caught but not logged. EIO.catchExceptions (withLogging x ctx ref) (fun _ => pure ()) @[inherit_doc Core.wrapAsync] -def wrapAsync (act : Unit → CommandElabM α) (cancelTk? : Option IO.CancelToken) : - CommandElabM (EIO Exception α) := do +def wrapAsync {α β : Type} (act : α → CommandElabM β) (cancelTk? : Option IO.CancelToken) : + CommandElabM (α → EIO Exception β) := do let ctx ← read let ctx := { ctx with cancelTk? } let st ← get - return act () |>.run ctx |>.run' st + return (act · |>.run ctx |>.run' st) open Language in @[inherit_doc Core.wrapAsyncAsSnapshot] -- `CoreM` and `CommandElabM` are too different to meaningfully share this code -def wrapAsyncAsSnapshot (act : Unit → CommandElabM Unit) (cancelTk? : Option IO.CancelToken) +def wrapAsyncAsSnapshot {α : Type} (act : α → CommandElabM Unit) (cancelTk? : Option IO.CancelToken) (desc : String := by exact decl_name%.toString) : - CommandElabM (BaseIO SnapshotTree) := do - let t ← wrapAsync (cancelTk? := cancelTk?) fun _ => do + CommandElabM (α → BaseIO SnapshotTree) := do + let f ← wrapAsync (cancelTk? := cancelTk?) fun a => do IO.FS.withIsolatedStreams (isolateStderr := Core.stderrAsMessages.get (← getOptions)) do let tid ← IO.getTID -- reset trace state and message log so as not to report them twice @@ -323,15 +326,15 @@ def wrapAsyncAsSnapshot (act : Unit → CommandElabM Unit) (cancelTk? : Option I } try withTraceNode `Elab.async (fun _ => return desc) do - act () + act a catch e => logError e.toMessageData finally addTraceAsMessages get let ctx ← read - return do - match (← t.toBaseIO) with + return fun a => do + match (← (f a).toBaseIO) with | .ok (output, st) => let mut msgs := st.messages if !output.isEmpty then @@ -353,6 +356,7 @@ def wrapAsyncAsSnapshot (act : Unit → CommandElabM Unit) (cancelTk? : Option I def logSnapshotTask (task : Language.SnapshotTask Language.SnapshotTree) : CommandElabM Unit := modify fun s => { s with snapshotTasks := s.snapshotTasks.push task } +open Language in def runLintersAsync (stx : Syntax) : CommandElabM Unit := do if !Elab.async.get (← getOptions) then withoutModifyingEnv do @@ -362,8 +366,13 @@ def runLintersAsync (stx : Syntax) : CommandElabM Unit := do -- We only start one task for all linters for now as most linters are fast and we simply want -- to unblock elaboration of the next command let cancelTk ← IO.CancelToken.new - let lintAct ← wrapAsyncAsSnapshot (cancelTk? := cancelTk) fun _ => runLinters stx - logSnapshotTask { stx? := none, task := (← BaseIO.asTask lintAct), cancelTk? := cancelTk } + let lintAct ← wrapAsyncAsSnapshot (cancelTk? := cancelTk) fun infoSt => do + modifyInfoState fun _ => infoSt + runLinters stx + + -- linters should have access to the complete info tree + let task ← BaseIO.mapTask (t := (← getInfoState).substituteLazy) lintAct + logSnapshotTask { stx? := none, task, cancelTk? := cancelTk } protected def getCurrMacroScope : CommandElabM Nat := do pure (← read).currMacroScope protected def getMainModule : CommandElabM Name := do pure (← getEnv).mainModule @@ -579,11 +588,7 @@ def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do pro if let some snap := (← read).snap? then snap.new.resolve default - -- note the order: first process current messages & info trees, then add back old messages & trees, - -- then convert new traces to messages - let mut msgs := (← get).messages - for tree in (← getInfoTrees) do - trace[Elab.info] (← tree.format) + let msgs := (← get).messages modify fun st => { st with messages := initMsgs ++ msgs infoState := { st.infoState with trees := initInfoTrees ++ st.infoState.trees } diff --git a/src/Lean/Elab/Frontend.lean b/src/Lean/Elab/Frontend.lean index 99b177799a..6e6d5ff85c 100644 --- a/src/Lean/Elab/Frontend.lean +++ b/src/Lean/Elab/Frontend.lean @@ -112,9 +112,9 @@ where |>.foldl (· ++ ·) {} -- In contrast to messages, we should collect info trees only from the top-level command -- snapshots as they subsume any info trees reported incrementally by their children. - let trees := commands.map (·.finishedSnap.get.infoTree?) |>.filterMap id |>.toPArray' + let trees := commands.map (·.infoTreeSnap.get.infoTree?) |>.filterMap id |>.toPArray' return { - commandState := { snap.finishedSnap.get.cmdState with messages, infoState.trees := trees } + commandState := { snap.resultSnap.get.cmdState with messages, infoState.trees := trees } parserState := snap.parserState cmdPos := snap.parserState.pos commands := commands.map (·.stx) diff --git a/src/Lean/Elab/InfoTree/Main.lean b/src/Lean/Elab/InfoTree/Main.lean index 2069c7138a..04af8563cc 100644 --- a/src/Lean/Elab/InfoTree/Main.lean +++ b/src/Lean/Elab/InfoTree/Main.lean @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Wojciech Nawrocki, Leonardo de Moura, Sebastian Ullrich -/ prelude +import Init.Task import Lean.Meta.PPGoal import Lean.ReservedNameAction @@ -95,6 +96,13 @@ partial def InfoTree.substitute (tree : InfoTree) (assignment : PersistentHashMa | none => hole id | some tree => substitute tree assignment +/-- Applies `s.lazyAssignment` to `s.trees`, asynchronously. -/ +def InfoState.substituteLazy (s : InfoState) : Task InfoState := + Task.mapList (tasks := s.lazyAssignment.toList.map (·.2)) fun _ => { s with + trees := s.trees.map (·.substitute <| s.lazyAssignment.map (·.get)) + lazyAssignment := {} + } + /-- Embeds a `CoreM` action in `IO` by supplying the information stored in `info`. -/ def ContextInfo.runCoreM (info : ContextInfo) (x : CoreM α) : IO α := do /- diff --git a/src/Lean/Elab/InfoTree/Types.lean b/src/Lean/Elab/InfoTree/Types.lean index dd22148866..8f54b3dc78 100644 --- a/src/Lean/Elab/InfoTree/Types.lean +++ b/src/Lean/Elab/InfoTree/Types.lean @@ -255,6 +255,11 @@ structure InfoState where enabled : Bool := true /-- Map from holes in the infotree to child infotrees. -/ assignment : PersistentHashMap MVarId InfoTree := {} + /-- + Assignments fulfilled by other elaboration tasks. We substitute them only just before reporting + the info tree via a snapshot to avoid premature blocking. + -/ + lazyAssignment : PersistentHashMap MVarId (Task InfoTree) := {} /-- Pending child trees of a node. -/ trees : PersistentArray InfoTree := {} deriving Inhabited diff --git a/src/Lean/Elab/InfoTrees.lean b/src/Lean/Elab/InfoTrees.lean index 82c5128581..dfcfeaed9a 100644 --- a/src/Lean/Elab/InfoTrees.lean +++ b/src/Lean/Elab/InfoTrees.lean @@ -17,7 +17,7 @@ def elabInfoTrees : CommandElab logError "Info trees are disabled, can not use `#info_trees`." else elabCommand cmd - let infoTrees ← getInfoTrees + let infoTrees := (← getInfoState).substituteLazy.get.trees for t in infoTrees do logInfoAt tk (← t.format) | _ => throwUnsupportedSyntax diff --git a/src/Lean/Language/Lean.lean b/src/Lean/Language/Lean.lean index 9200aa518e..288913eb27 100644 --- a/src/Lean/Language/Lean.lean +++ b/src/Lean/Language/Lean.lean @@ -524,12 +524,12 @@ where if let some oldNext := old.nextCmdSnap? then do let newProm ← IO.Promise.new -- can reuse range, syntax unchanged - BaseIO.chainTask (sync := true) old.finishedSnap.task fun oldFinished => + BaseIO.chainTask (sync := true) old.resultSnap.task fun oldResult => -- also wait on old command parse snapshot as parsing is cheap and may allow for -- elaboration reuse BaseIO.chainTask (sync := true) oldNext.task fun oldNext => do let cancelTk ← IO.CancelToken.new - parseCmd oldNext newParserState oldFinished.cmdState newProm sync cancelTk ctx + parseCmd oldNext newParserState oldResult.cmdState newProm sync cancelTk ctx prom.resolve <| { old with nextCmdSnap? := some { stx? := none reportingRange? := some ⟨newParserState.pos, ctx.input.endPos⟩ @@ -582,7 +582,8 @@ where prom.resolve <| { diagnostics := .empty, stx := .missing, parserState elabSnap := default - finishedSnap := .finished none { diagnostics := .empty, cmdState } + resultSnap := .finished none { diagnostics := .empty, cmdState } + infoTreeSnap := .finished none { diagnostics := .empty } reportSnap := default nextCmdSnap? := none } @@ -592,6 +593,7 @@ where let _ ← (if sync then BaseIO.asTask else (.pure <$> ·)) do -- definitely resolved in `doElab` task let elabPromise ← IO.Promise.new + let resultPromise ← IO.Promise.new let finishedPromise ← IO.Promise.new let reportPromise ← IO.Promise.new let minimalSnapshots := internal.cmdlineSnapshots.get cmdState.scopes.head!.opts @@ -602,11 +604,6 @@ where -- report terminal tasks on first line of decl such as not to hide incremental tactics' -- progress let initRange? := getNiceCommandStartPos? stx |>.map fun pos => ⟨pos, pos⟩ - let finishedSnap := { - stx? := stx' - reportingRange? := initRange? - task := finishedPromise.result! - } let next? ← if Parser.isTerminalCommand stx then pure none -- for now, wait on "command finished" snapshot before parsing next command else some <$> IO.Promise.new @@ -621,21 +618,55 @@ where -- use per-command cancellation token for elaboration so that let elabCmdCancelTk ← IO.CancelToken.new prom.resolve { - diagnostics, finishedSnap, nextCmdSnap? + diagnostics, nextCmdSnap? stx := stx', parserState := parserState' elabSnap := { stx? := stx', task := elabPromise.result!, cancelTk? := some elabCmdCancelTk } + resultSnap := { stx? := stx', reportingRange? := initRange?, task := resultPromise.result! } + infoTreeSnap := { stx? := stx', reportingRange? := initRange?, task := finishedPromise.result! } reportSnap := { stx? := none, reportingRange? := initRange?, task := reportPromise.result! } } let cmdState ← doElab stx cmdState beginPos { old? := old?.map fun old => ⟨old.stx, old.elabSnap⟩, new := elabPromise } - finishedPromise elabCmdCancelTk ctx + elabCmdCancelTk ctx + + let mut reportedCmdState := cmdState + let cmdline := internal.cmdlineSnapshots.get scope.opts && !Parser.isTerminalCommand stx + if cmdline then + -- discard all metadata apart from the environment; see `internal.cmdlineSnapshots` + reportedCmdState := { env := reportedCmdState.env, maxRecDepth := 0 } + resultPromise.resolve { + diagnostics := (← Snapshot.Diagnostics.ofMessageLog cmdState.messages) + traces := cmdState.traceState + cmdState := reportedCmdState + } + + -- report info tree when relevant tasks are finished + BaseIO.chainTask (sync := true) (t := cmdState.infoState.substituteLazy) fun infoSt => do + let infoTree := infoSt.trees[0]! + let opts := cmdState.scopes.head!.opts + let mut msgLog := MessageLog.empty + if (← isTracingEnabledForCore `Elab.info opts) then + if let .ok msg ← infoTree.format.toBaseIO then + let data := .tagged `trace <| .trace { cls := `Elab.info } .nil #[msg] + msgLog := msgLog.add { + fileName := ctx.fileName + severity := MessageSeverity.information + pos := ctx.fileMap.toPosition beginPos + data := data + } + finishedPromise.resolve { + diagnostics := (← Snapshot.Diagnostics.ofMessageLog msgLog) + infoTree? := infoTree + } + + -- report traces when *all* tasks are finished let traceTask ← if (← isTracingEnabledForCore `Elab.snapshotTree cmdState.scopes.head!.opts) then -- We want to trace all of `CommandParsedSnapshot` but `traceTask` is part of it, so let's -- create a temporary snapshot tree containing all tasks but it let snaps := #[ { stx? := stx', task := elabPromise.result!.map (sync := true) toSnapshotTree }, - { stx? := stx', task := finishedPromise.result!.map (sync := true) toSnapshotTree }] ++ + { stx? := stx', task := resultPromise.result!.map (sync := true) toSnapshotTree }] ++ cmdState.snapshotTasks let tree := SnapshotTree.mk { diagnostics := .empty } snaps BaseIO.bindTask (← tree.waitAll) fun _ => do @@ -665,8 +696,8 @@ where parseCmd none parserState cmdState next (sync := false) elabCmdCancelTk ctx doElab (stx : Syntax) (cmdState : Command.State) (beginPos : String.Pos) - (snap : SnapshotBundle DynamicSnapshot) (finishedPromise : IO.Promise CommandFinishedSnapshot) - (cancelTk : IO.CancelToken) : LeanProcessingM Command.State := do + (snap : SnapshotBundle DynamicSnapshot) (cancelTk : IO.CancelToken) : + LeanProcessingM Command.State := do let ctx ← read let scope := cmdState.scopes.head! -- reset per-command state @@ -693,21 +724,9 @@ where data := output } let cmdState : Command.State := { cmdState with messages } - let mut reportedCmdState := cmdState -- definitely resolve eventually snap.new.resolve <| .ofTyped { diagnostics := .empty : SnapshotLeaf } - let infoTree : InfoTree := cmdState.infoState.trees[0]! - let cmdline := internal.cmdlineSnapshots.get scope.opts && !Parser.isTerminalCommand stx - if cmdline then - -- discard all metadata apart from the environment; see `internal.cmdlineSnapshots` - reportedCmdState := { env := reportedCmdState.env, maxRecDepth := 0 } - finishedPromise.resolve { - diagnostics := (← Snapshot.Diagnostics.ofMessageLog cmdState.messages) - infoTree? := infoTree - traces := cmdState.traceState - cmdState := reportedCmdState - } -- The reported `cmdState` in the snapshot may be minimized as seen above, so we return the full -- state here for further processing on the same thread return cmdState @@ -735,6 +754,6 @@ where goCmd snap := if let some next := snap.nextCmdSnap? then goCmd next.get else - snap.finishedSnap.get.cmdState + snap.resultSnap.get.cmdState end Lean diff --git a/src/Lean/Language/Lean/Types.lean b/src/Lean/Language/Lean/Types.lean index 7aa3b02658..5462d18e9e 100644 --- a/src/Lean/Language/Lean/Types.lean +++ b/src/Lean/Language/Lean/Types.lean @@ -25,12 +25,15 @@ private def pushOpt (a? : Option α) (as : Array α) : Array α := /-! The hierarchy of Lean snapshot types -/ -/-- Snapshot after elaboration of the entire command. -/ -structure CommandFinishedSnapshot extends Language.Snapshot where +/-- +Snapshot after command elaborator has returned. Also contains diagnostics from the elaborator's main +task. Asynchronous elaboration tasks may not yet be finished. +-/ +structure CommandResultSnapshot extends Language.Snapshot where /-- Resulting elaboration state. -/ cmdState : Command.State deriving Nonempty -instance : ToSnapshotTree CommandFinishedSnapshot where +instance : ToSnapshotTree CommandResultSnapshot where toSnapshotTree s := ⟨s.toSnapshot, #[]⟩ /-- State after a command has been parsed. -/ @@ -44,8 +47,12 @@ structure CommandParsedSnapshot extends Snapshot where elaborator. -/ elabSnap : SnapshotTask DynamicSnapshot - /-- State after processing is finished. -/ - finishedSnap : SnapshotTask CommandFinishedSnapshot + /-- State after command elaborator has returned. -/ + resultSnap : SnapshotTask CommandResultSnapshot + /-- + State after all elaborator tasks are finished. In particular, contains the complete info tree. + -/ + infoTreeSnap : SnapshotTask SnapshotLeaf /-- Additional, untyped snapshots used for reporting, not reuse. -/ reportSnap : SnapshotTask SnapshotTree /-- Next command, unless this is a terminal command. -/ @@ -55,7 +62,8 @@ partial instance : ToSnapshotTree CommandParsedSnapshot where toSnapshotTree := go where go s := ⟨s.toSnapshot, #[s.elabSnap.map (sync := true) toSnapshotTree, - s.finishedSnap.map (sync := true) toSnapshotTree, + s.resultSnap.map (sync := true) toSnapshotTree, + s.infoTreeSnap.map (sync := true) toSnapshotTree, s.reportSnap] |> pushOpt (s.nextCmdSnap?.map (·.map (sync := true) go))⟩ diff --git a/src/Lean/Server/FileWorker/Utils.lean b/src/Lean/Server/FileWorker/Utils.lean index 49fc89a549..539f639cfa 100644 --- a/src/Lean/Server/FileWorker/Utils.lean +++ b/src/Lean/Server/FileWorker/Utils.lean @@ -28,11 +28,11 @@ private partial def mkCmdSnaps (initSnap : Language.Lean.InitialSnapshot) : } <| .delayed <| headerSuccess.firstCmdSnap.task.asServerTask.bindCheap go where go cmdParsed := - cmdParsed.finishedSnap.task.asServerTask.mapCheap fun finished => + cmdParsed.resultSnap.task.asServerTask.mapCheap fun result => .ok <| .cons { stx := cmdParsed.stx mpState := cmdParsed.parserState - cmdState := finished.cmdState + cmdState := result.cmdState } (match cmdParsed.nextCmdSnap? with | some next => .delayed <| next.task.asServerTask.bindCheap go | none => .nil) diff --git a/src/Lean/Server/Requests.lean b/src/Lean/Server/Requests.lean index 223dde1dfd..41817245a4 100644 --- a/src/Lean/Server/Requests.lean +++ b/src/Lean/Server/Requests.lean @@ -304,10 +304,9 @@ def findCmdDataAtPos findCmdParsedSnap doc hoverPos |>.bindCheap fun | some cmdParsed => toSnapshotTree cmdParsed |>.findInfoTreeAtPos doc.meta.text hoverPos includeStop |>.bindCheap fun | some infoTree => .pure <| some (cmdParsed.stx, infoTree) - | none => cmdParsed.finishedSnap.task.asServerTask.mapCheap fun s => - -- the parser returns exactly one command per snapshot, and the elaborator creates exactly one node per command - assert! s.cmdState.infoState.trees.size == 1 - some (cmdParsed.stx, s.cmdState.infoState.trees[0]!) + | none => cmdParsed.infoTreeSnap.task.asServerTask.mapCheap fun s => + assert! s.infoTree?.isSome + some (cmdParsed.stx, s.infoTree?.get!) | none => .pure none open Language in diff --git a/src/Lean/Server/Snapshots.lean b/src/Lean/Server/Snapshots.lean index a8d098c0f2..b8b4c7ade5 100644 --- a/src/Lean/Server/Snapshots.lean +++ b/src/Lean/Server/Snapshots.lean @@ -39,9 +39,11 @@ def msgLog (s : Snapshot) : MessageLog := s.cmdState.messages def infoTree (s : Snapshot) : InfoTree := + -- TODO: we should not block here! + let infoState := s.cmdState.infoState.substituteLazy.get -- the parser returns exactly one command per snapshot, and the elaborator creates exactly one node per command - assert! s.cmdState.infoState.trees.size == 1 - s.cmdState.infoState.trees[0]! + assert! infoState.trees.size == 1 + infoState.trees[0]! def isAtEnd (s : Snapshot) : Bool := Parser.isTerminalCommand s.stx diff --git a/tests/lean/1018unknowMVarIssue.lean.expected.out b/tests/lean/1018unknowMVarIssue.lean.expected.out index 22ad57e8dd..f56dd99011 100644 --- a/tests/lean/1018unknowMVarIssue.lean.expected.out +++ b/tests/lean/1018unknowMVarIssue.lean.expected.out @@ -1,6 +1,7 @@ -[Elab.info] • command @ ⟨6, 0⟩-⟨6, 31⟩ @ Lean.Elab.Command.elabSetOption - • [.] (Command.set_option "set_option" `trace.Elab.info []) @ ⟨6, 0⟩-⟨6, 26⟩ - • option trace.Elab.info @ ⟨6, 11⟩-⟨6, 26⟩ +[Elab.info] + • command @ ⟨6, 0⟩-⟨6, 31⟩ @ Lean.Elab.Command.elabSetOption + • [.] (Command.set_option "set_option" `trace.Elab.info []) @ ⟨6, 0⟩-⟨6, 26⟩ + • option trace.Elab.info @ ⟨6, 11⟩-⟨6, 26⟩ 1018unknowMVarIssue.lean:9:18-9:19: error: don't know how to synthesize placeholder context: α✝ β : Type @@ -8,75 +9,77 @@ x : Fam2 α✝ β α : Type a : α ⊢ α -[Elab.info] • command @ ⟨7, 0⟩-⟨10, 19⟩ @ Lean.Elab.Command.elabDeclaration - • α : Type @ ⟨7, 13⟩-⟨7, 14⟩ @ Lean.Elab.Term.elabIdent - • [.] α : some Sort.{?_uniq} @ ⟨7, 13⟩-⟨7, 14⟩ - • α : Type @ ⟨7, 13⟩-⟨7, 14⟩ - • a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩ - • Fam2 α β : Type 1 @ ⟨7, 21⟩-⟨7, 29⟩ @ Lean.Elab.Term.elabApp - • [.] Fam2 : some Sort.{?_uniq} @ ⟨7, 21⟩-⟨7, 25⟩ - • Fam2 : Type → Type → Type 1 @ ⟨7, 21⟩-⟨7, 25⟩ - • α : Type @ ⟨7, 26⟩-⟨7, 27⟩ @ Lean.Elab.Term.elabIdent - • [.] α : some Type @ ⟨7, 26⟩-⟨7, 27⟩ - • α : Type @ ⟨7, 26⟩-⟨7, 27⟩ - • β : Type @ ⟨7, 28⟩-⟨7, 29⟩ @ Lean.Elab.Term.elabIdent - • [.] β : some Type @ ⟨7, 28⟩-⟨7, 29⟩ - • β : Type @ ⟨7, 28⟩-⟨7, 29⟩ - • x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩ - • β : Type @ ⟨7, 33⟩-⟨7, 34⟩ @ Lean.Elab.Term.elabIdent - • [.] β : some Sort.{?_uniq} @ ⟨7, 33⟩-⟨7, 34⟩ - • β : Type @ ⟨7, 33⟩-⟨7, 34⟩ - • CustomInfo(Lean.Elab.InlayHint) - • _example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩†!-⟨7, 7⟩†! - • a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩ - • x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩ - • CustomInfo(Lean.Elab.Term.BodyInfo) - • Partial term @ ⟨8, 2⟩-⟨10, 19⟩ @ Lean.Elab.Term.Quotation.elabMatchSyntax - • match α, β, x, a with - | α_1, .(α_1), Fam2.any, a => ?m x α_1 a - | .(Nat), .(Nat), Fam2.nat n, a => n : β @ ⟨8, 2⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabMatch - • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩ @ Lean.Elab.Term.elabIdent - • [.] x : none @ ⟨8, 8⟩-⟨8, 9⟩ - • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩ - • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩ @ Lean.Elab.Term.elabIdent - • [.] x : none @ ⟨8, 8⟩-⟨8, 9⟩ - • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩ - • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩ - • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩ - • @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩ - • [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩ - • Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩ - • [.] n : none @ ⟨10, 13⟩-⟨10, 14⟩ - • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩ - • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩ - • @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩ - • [.] a : none @ ⟨8, 2⟩†-⟨10, 19⟩† - • [.] Fam2.any : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨9, 4⟩-⟨9, 12⟩ - • [.] a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩† - • α (isBinder := true) : Type @ ⟨8, 2⟩†-⟨10, 19⟩† - • α : Type @ ⟨8, 2⟩†-⟨10, 19⟩† - • Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩† - • α : Type @ ⟨9, 4⟩†-⟨9, 12⟩† - • a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩† - • FVarAlias a: _uniq.592 -> _uniq.319 - • FVarAlias α: _uniq.591 -> _uniq.317 - • ?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole - • [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩ - • Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩ - • [.] n : none @ ⟨10, 13⟩-⟨10, 14⟩ - • [.] a : none @ ⟨8, 2⟩†-⟨10, 19⟩† - • [.] Fam2.nat : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨10, 4⟩-⟨10, 12⟩ - • [.] n : some Nat @ ⟨10, 13⟩-⟨10, 14⟩ - • [.] a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩† - • Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩† - • Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩† - • Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩ - • n (isBinder := true) : Nat @ ⟨10, 13⟩-⟨10, 14⟩ - • a (isBinder := true) : Nat @ ⟨8, 2⟩†-⟨10, 19⟩† - • FVarAlias a: _uniq.623 -> _uniq.319 - • FVarAlias n: _uniq.622 -> _uniq.317 - • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent - • [.] n : some Nat @ ⟨10, 18⟩-⟨10, 19⟩ - • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ - • @_example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩-⟨7, 7⟩ -[Elab.info] • command @ ⟨11, 0⟩-⟨11, 0⟩ @ Lean.Elab.Command.elabEoi +[Elab.info] + • command @ ⟨7, 0⟩-⟨10, 19⟩ @ Lean.Elab.Command.elabDeclaration + • α : Type @ ⟨7, 13⟩-⟨7, 14⟩ @ Lean.Elab.Term.elabIdent + • [.] α : some Sort.{?_uniq} @ ⟨7, 13⟩-⟨7, 14⟩ + • α : Type @ ⟨7, 13⟩-⟨7, 14⟩ + • a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩ + • Fam2 α β : Type 1 @ ⟨7, 21⟩-⟨7, 29⟩ @ Lean.Elab.Term.elabApp + • [.] Fam2 : some Sort.{?_uniq} @ ⟨7, 21⟩-⟨7, 25⟩ + • Fam2 : Type → Type → Type 1 @ ⟨7, 21⟩-⟨7, 25⟩ + • α : Type @ ⟨7, 26⟩-⟨7, 27⟩ @ Lean.Elab.Term.elabIdent + • [.] α : some Type @ ⟨7, 26⟩-⟨7, 27⟩ + • α : Type @ ⟨7, 26⟩-⟨7, 27⟩ + • β : Type @ ⟨7, 28⟩-⟨7, 29⟩ @ Lean.Elab.Term.elabIdent + • [.] β : some Type @ ⟨7, 28⟩-⟨7, 29⟩ + • β : Type @ ⟨7, 28⟩-⟨7, 29⟩ + • x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩ + • β : Type @ ⟨7, 33⟩-⟨7, 34⟩ @ Lean.Elab.Term.elabIdent + • [.] β : some Sort.{?_uniq} @ ⟨7, 33⟩-⟨7, 34⟩ + • β : Type @ ⟨7, 33⟩-⟨7, 34⟩ + • CustomInfo(Lean.Elab.InlayHint) + • _example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩†!-⟨7, 7⟩†! + • a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩ + • x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩ + • CustomInfo(Lean.Elab.Term.BodyInfo) + • Partial term @ ⟨8, 2⟩-⟨10, 19⟩ @ Lean.Elab.Term.Quotation.elabMatchSyntax + • match α, β, x, a with + | α_1, .(α_1), Fam2.any, a => ?m x α_1 a + | .(Nat), .(Nat), Fam2.nat n, a => n : β @ ⟨8, 2⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabMatch + • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩ @ Lean.Elab.Term.elabIdent + • [.] x : none @ ⟨8, 8⟩-⟨8, 9⟩ + • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩ + • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩ @ Lean.Elab.Term.elabIdent + • [.] x : none @ ⟨8, 8⟩-⟨8, 9⟩ + • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩ + • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩ + • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩ + • @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩ + • [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩ + • Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩ + • [.] n : none @ ⟨10, 13⟩-⟨10, 14⟩ + • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩ + • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩ + • @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩ + • [.] a : none @ ⟨8, 2⟩†-⟨10, 19⟩† + • [.] Fam2.any : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨9, 4⟩-⟨9, 12⟩ + • [.] a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩† + • α (isBinder := true) : Type @ ⟨8, 2⟩†-⟨10, 19⟩† + • α : Type @ ⟨8, 2⟩†-⟨10, 19⟩† + • Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩† + • α : Type @ ⟨9, 4⟩†-⟨9, 12⟩† + • a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩† + • FVarAlias a: _uniq.592 -> _uniq.319 + • FVarAlias α: _uniq.591 -> _uniq.317 + • ?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole + • [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩ + • Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩ + • [.] n : none @ ⟨10, 13⟩-⟨10, 14⟩ + • [.] a : none @ ⟨8, 2⟩†-⟨10, 19⟩† + • [.] Fam2.nat : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨10, 4⟩-⟨10, 12⟩ + • [.] n : some Nat @ ⟨10, 13⟩-⟨10, 14⟩ + • [.] a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩† + • Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩† + • Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩† + • Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩ + • n (isBinder := true) : Nat @ ⟨10, 13⟩-⟨10, 14⟩ + • a (isBinder := true) : Nat @ ⟨8, 2⟩†-⟨10, 19⟩† + • FVarAlias a: _uniq.623 -> _uniq.319 + • FVarAlias n: _uniq.622 -> _uniq.317 + • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent + • [.] n : some Nat @ ⟨10, 18⟩-⟨10, 19⟩ + • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ + • @_example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩-⟨7, 7⟩ +[Elab.info] + • command @ ⟨11, 0⟩-⟨11, 0⟩ @ Lean.Elab.Command.elabEoi diff --git a/tests/lean/binopInfoTree.lean.expected.out b/tests/lean/binopInfoTree.lean.expected.out index fe614bbbd9..4872b7485a 100644 --- a/tests/lean/binopInfoTree.lean.expected.out +++ b/tests/lean/binopInfoTree.lean.expected.out @@ -1,76 +1,80 @@ -[Elab.info] • command @ ⟨3, 0⟩-⟨3, 31⟩ @ Lean.Elab.Command.elabSetOption - • [.] (Command.set_option "set_option" `trace.Elab.info []) @ ⟨3, 0⟩-⟨3, 26⟩ - • option trace.Elab.info @ ⟨3, 11⟩-⟨3, 26⟩ +[Elab.info] + • command @ ⟨3, 0⟩-⟨3, 31⟩ @ Lean.Elab.Command.elabSetOption + • [.] (Command.set_option "set_option" `trace.Elab.info []) @ ⟨3, 0⟩-⟨3, 26⟩ + • option trace.Elab.info @ ⟨3, 11⟩-⟨3, 26⟩ 1 + 2 + 3 : Nat -[Elab.info] • command @ ⟨5, 0⟩-⟨5, 16⟩ @ Lean.Elab.Command.elabCheck - • 1 + 2 + 3 : Nat @ ⟨5, 7⟩-⟨5, 16⟩ @ «_aux_Init_Notation___macroRules_term_+__2» - • Macro expansion - 1 + 2 + - 3 - -- should propagate through multiple macro expansions - ===> - binop% HAdd.hAdd✝ (1 + 2) - 3 - -- should propagate through multiple macro expansions - • 1 + 2 + 3 : Nat @ ⟨5, 7⟩†-⟨5, 16⟩† @ Lean.Elab.Term.Op.elabBinOp - • 1 + 2 + 3 : Nat @ ⟨5, 7⟩†-⟨5, 16⟩† - • 1 + 2 : Nat @ ⟨5, 7⟩-⟨5, 12⟩ @ «_aux_Init_Notation___macroRules_term_+__2» - • Macro expansion - 1 + 2 - ===> - binop% HAdd.hAdd✝ 1 2 - • 1 + 2 : Nat @ ⟨5, 7⟩†-⟨5, 12⟩† - • [.] HAdd.hAdd✝ : none @ ⟨5, 7⟩†-⟨5, 16⟩† - • [.] HAdd.hAdd✝ : none @ ⟨5, 7⟩†-⟨5, 12⟩† - • 1 : Nat @ ⟨5, 7⟩-⟨5, 8⟩ @ Lean.Elab.Term.elabNumLit - • 2 : Nat @ ⟨5, 11⟩-⟨5, 12⟩ @ Lean.Elab.Term.elabNumLit - • 3 : Nat @ ⟨5, 15⟩-⟨5, 16⟩ @ Lean.Elab.Term.elabNumLit +[Elab.info] + • command @ ⟨5, 0⟩-⟨5, 16⟩ @ Lean.Elab.Command.elabCheck + • 1 + 2 + 3 : Nat @ ⟨5, 7⟩-⟨5, 16⟩ @ «_aux_Init_Notation___macroRules_term_+__2» + • Macro expansion + 1 + 2 + + 3 + -- should propagate through multiple macro expansions + ===> + binop% HAdd.hAdd✝ (1 + 2) + 3 + -- should propagate through multiple macro expansions + • 1 + 2 + 3 : Nat @ ⟨5, 7⟩†-⟨5, 16⟩† @ Lean.Elab.Term.Op.elabBinOp + • 1 + 2 + 3 : Nat @ ⟨5, 7⟩†-⟨5, 16⟩† + • 1 + 2 : Nat @ ⟨5, 7⟩-⟨5, 12⟩ @ «_aux_Init_Notation___macroRules_term_+__2» + • Macro expansion + 1 + 2 + ===> + binop% HAdd.hAdd✝ 1 2 + • 1 + 2 : Nat @ ⟨5, 7⟩†-⟨5, 12⟩† + • [.] HAdd.hAdd✝ : none @ ⟨5, 7⟩†-⟨5, 16⟩† + • [.] HAdd.hAdd✝ : none @ ⟨5, 7⟩†-⟨5, 12⟩† + • 1 : Nat @ ⟨5, 7⟩-⟨5, 8⟩ @ Lean.Elab.Term.elabNumLit + • 2 : Nat @ ⟨5, 11⟩-⟨5, 12⟩ @ Lean.Elab.Term.elabNumLit + • 3 : Nat @ ⟨5, 15⟩-⟨5, 16⟩ @ Lean.Elab.Term.elabNumLit fun n m l => ↑n + (↑m + ↑l) : Nat → Nat → Nat → Int -[Elab.info] • command @ ⟨7, 0⟩-⟨7, 48⟩ @ Lean.Elab.Command.elabCheck - • fun n m l => ↑n + (↑m + ↑l) : Nat → Nat → Nat → Int @ ⟨7, 7⟩-⟨7, 48⟩ @ Lean.Elab.Term.elabFun - • Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩ @ Lean.Elab.Term.elabIdent - • [.] Nat : some Sort.{?_uniq} @ ⟨7, 20⟩-⟨7, 23⟩ - • Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩ - • n (isBinder := true) : Nat @ ⟨7, 12⟩-⟨7, 13⟩ - • Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩ @ Lean.Elab.Term.elabIdent - • [.] Nat : some Sort.{?_uniq} @ ⟨7, 20⟩-⟨7, 23⟩ - • Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩ - • m (isBinder := true) : Nat @ ⟨7, 14⟩-⟨7, 15⟩ - • Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩ @ Lean.Elab.Term.elabIdent - • [.] Nat : some Sort.{?_uniq} @ ⟨7, 20⟩-⟨7, 23⟩ - • Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩ - • l (isBinder := true) : Nat @ ⟨7, 16⟩-⟨7, 17⟩ - • ↑n + (↑m + ↑l) : Int @ ⟨7, 28⟩-⟨7, 48⟩ @ Lean.Elab.Term.elabTypeAscription - • Int : Type @ ⟨7, 44⟩-⟨7, 47⟩ @ Lean.Elab.Term.elabIdent - • [.] Int : some Sort.{?_uniq} @ ⟨7, 44⟩-⟨7, 47⟩ - • Int : Type @ ⟨7, 44⟩-⟨7, 47⟩ - • ↑n + (↑m + ↑l) : Int @ ⟨7, 29⟩-⟨7, 41⟩ @ «_aux_Init_Notation___macroRules_term_+__2» - • Macro expansion - n + (m +' l) - ===> - binop% HAdd.hAdd✝ n (m +' l) - • ↑n + (↑m + ↑l) : Int @ ⟨7, 29⟩†-⟨7, 41⟩† @ Lean.Elab.Term.Op.elabBinOp - • ↑n + (↑m + ↑l) : Int @ ⟨7, 29⟩†-⟨7, 41⟩† - • [.] HAdd.hAdd✝ : none @ ⟨7, 29⟩†-⟨7, 41⟩† - • n : Nat @ ⟨7, 29⟩-⟨7, 30⟩ @ Lean.Elab.Term.elabIdent - • [.] n : none @ ⟨7, 29⟩-⟨7, 30⟩ - • n : Nat @ ⟨7, 29⟩-⟨7, 30⟩ - • ↑m + ↑l : Int @ ⟨7, 34⟩-⟨7, 40⟩ @ «_aux_binopInfoTree___macroRules_term_+'__1» - • Macro expansion - m +' l - ===> - m + l - • ↑m + ↑l : Int @ ⟨7, 34⟩†-⟨7, 40⟩† @ «_aux_Init_Notation___macroRules_term_+__2» - • Macro expansion - m + l - ===> - binop% HAdd.hAdd✝ m l - • ↑m + ↑l : Int @ ⟨7, 34⟩†-⟨7, 40⟩† - • [.] HAdd.hAdd✝ : none @ ⟨7, 34⟩†-⟨7, 40⟩† - • m : Nat @ ⟨7, 34⟩-⟨7, 35⟩ @ Lean.Elab.Term.elabIdent - • [.] m : none @ ⟨7, 34⟩-⟨7, 35⟩ - • m : Nat @ ⟨7, 34⟩-⟨7, 35⟩ - • l : Nat @ ⟨7, 39⟩-⟨7, 40⟩ @ Lean.Elab.Term.elabIdent - • [.] l : none @ ⟨7, 39⟩-⟨7, 40⟩ - • l : Nat @ ⟨7, 39⟩-⟨7, 40⟩ -[Elab.info] • command @ ⟨8, 0⟩-⟨8, 0⟩ @ Lean.Elab.Command.elabEoi +[Elab.info] + • command @ ⟨7, 0⟩-⟨7, 48⟩ @ Lean.Elab.Command.elabCheck + • fun n m l => ↑n + (↑m + ↑l) : Nat → Nat → Nat → Int @ ⟨7, 7⟩-⟨7, 48⟩ @ Lean.Elab.Term.elabFun + • Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩ @ Lean.Elab.Term.elabIdent + • [.] Nat : some Sort.{?_uniq} @ ⟨7, 20⟩-⟨7, 23⟩ + • Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩ + • n (isBinder := true) : Nat @ ⟨7, 12⟩-⟨7, 13⟩ + • Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩ @ Lean.Elab.Term.elabIdent + • [.] Nat : some Sort.{?_uniq} @ ⟨7, 20⟩-⟨7, 23⟩ + • Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩ + • m (isBinder := true) : Nat @ ⟨7, 14⟩-⟨7, 15⟩ + • Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩ @ Lean.Elab.Term.elabIdent + • [.] Nat : some Sort.{?_uniq} @ ⟨7, 20⟩-⟨7, 23⟩ + • Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩ + • l (isBinder := true) : Nat @ ⟨7, 16⟩-⟨7, 17⟩ + • ↑n + (↑m + ↑l) : Int @ ⟨7, 28⟩-⟨7, 48⟩ @ Lean.Elab.Term.elabTypeAscription + • Int : Type @ ⟨7, 44⟩-⟨7, 47⟩ @ Lean.Elab.Term.elabIdent + • [.] Int : some Sort.{?_uniq} @ ⟨7, 44⟩-⟨7, 47⟩ + • Int : Type @ ⟨7, 44⟩-⟨7, 47⟩ + • ↑n + (↑m + ↑l) : Int @ ⟨7, 29⟩-⟨7, 41⟩ @ «_aux_Init_Notation___macroRules_term_+__2» + • Macro expansion + n + (m +' l) + ===> + binop% HAdd.hAdd✝ n (m +' l) + • ↑n + (↑m + ↑l) : Int @ ⟨7, 29⟩†-⟨7, 41⟩† @ Lean.Elab.Term.Op.elabBinOp + • ↑n + (↑m + ↑l) : Int @ ⟨7, 29⟩†-⟨7, 41⟩† + • [.] HAdd.hAdd✝ : none @ ⟨7, 29⟩†-⟨7, 41⟩† + • n : Nat @ ⟨7, 29⟩-⟨7, 30⟩ @ Lean.Elab.Term.elabIdent + • [.] n : none @ ⟨7, 29⟩-⟨7, 30⟩ + • n : Nat @ ⟨7, 29⟩-⟨7, 30⟩ + • ↑m + ↑l : Int @ ⟨7, 34⟩-⟨7, 40⟩ @ «_aux_binopInfoTree___macroRules_term_+'__1» + • Macro expansion + m +' l + ===> + m + l + • ↑m + ↑l : Int @ ⟨7, 34⟩†-⟨7, 40⟩† @ «_aux_Init_Notation___macroRules_term_+__2» + • Macro expansion + m + l + ===> + binop% HAdd.hAdd✝ m l + • ↑m + ↑l : Int @ ⟨7, 34⟩†-⟨7, 40⟩† + • [.] HAdd.hAdd✝ : none @ ⟨7, 34⟩†-⟨7, 40⟩† + • m : Nat @ ⟨7, 34⟩-⟨7, 35⟩ @ Lean.Elab.Term.elabIdent + • [.] m : none @ ⟨7, 34⟩-⟨7, 35⟩ + • m : Nat @ ⟨7, 34⟩-⟨7, 35⟩ + • l : Nat @ ⟨7, 39⟩-⟨7, 40⟩ @ Lean.Elab.Term.elabIdent + • [.] l : none @ ⟨7, 39⟩-⟨7, 40⟩ + • l : Nat @ ⟨7, 39⟩-⟨7, 40⟩ +[Elab.info] + • command @ ⟨8, 0⟩-⟨8, 0⟩ @ Lean.Elab.Command.elabEoi