feat: incrementality for careful command macros such as set_option in theorem, theorem foo.bar, lemma (#4364)
See Note [Incremental Macros] for the caveat on correct `withRef` use
This commit is contained in:
Sebastian Ullrich
GitHub
parent
e33c32fb00
commit
9d47377bda
9 changed files with 173 additions and 49 deletions
|
|
@ -461,7 +461,9 @@ def elabRunMeta : CommandElab := fun stx =>
|
|||
modifyScope fun scope => { scope with opts := options }
|
||||
|
||||
@[builtin_macro Lean.Parser.Command.«in»] def expandInCmd : Macro
|
||||
| `($cmd₁ in $cmd₂) => `(section $cmd₁:command $cmd₂ end)
|
||||
| `($cmd₁ in%$tk $cmd₂) =>
|
||||
-- Limit ref variability for incrementality; see Note [Incremental Macros]
|
||||
withRef tk `(section $cmd₁:command $cmd₂ end)
|
||||
| _ => Macro.throwUnsupported
|
||||
|
||||
@[builtin_command_elab Parser.Command.addDocString] def elabAddDeclDoc : CommandElab := fun stx => do
|
||||
|
|
|
|||
|
|
@ -338,6 +338,26 @@ instance : MonadRecDepth CommandElabM where
|
|||
|
||||
builtin_initialize registerTraceClass `Elab.command
|
||||
|
||||
open Language in
|
||||
/-- Snapshot after macro expansion of a command. -/
|
||||
structure MacroExpandedSnapshot extends Snapshot where
|
||||
/-- The declaration name of the macro. -/
|
||||
macroDecl : Name
|
||||
/-- The expanded syntax tree. -/
|
||||
newStx : Syntax
|
||||
/-- `State.nextMacroScope` after expansion. -/
|
||||
newNextMacroScope : Nat
|
||||
/-- Whether any traces were present after expansion. -/
|
||||
hasTraces : Bool
|
||||
/--
|
||||
Follow-up elaboration snapshots, one per command if `newStx` is a sequence of commands.
|
||||
-/
|
||||
next : Array (SnapshotTask DynamicSnapshot)
|
||||
deriving TypeName
|
||||
open Language in
|
||||
instance : ToSnapshotTree MacroExpandedSnapshot where
|
||||
toSnapshotTree s := ⟨s.toSnapshot, s.next.map (·.map (sync := true) toSnapshotTree)⟩
|
||||
|
||||
partial def elabCommand (stx : Syntax) : CommandElabM Unit := do
|
||||
withLogging <| withRef stx <| withIncRecDepth <| withFreshMacroScope do
|
||||
match stx with
|
||||
|
|
@ -345,8 +365,8 @@ partial def elabCommand (stx : Syntax) : CommandElabM Unit := do
|
|||
if k == nullKind then
|
||||
-- list of commands => elaborate in order
|
||||
-- The parser will only ever return a single command at a time, but syntax quotations can return multiple ones
|
||||
-- TODO: support incrementality at least for some cases such as expansions of
|
||||
-- `set_option in` or `def a.b`
|
||||
-- Incrementality is currently limited to the common case where the sequence is the direct
|
||||
-- output of a macro, see below.
|
||||
withoutCommandIncrementality true do
|
||||
args.forM elabCommand
|
||||
else withTraceNode `Elab.command (fun _ => return stx) (tag :=
|
||||
|
|
@ -358,7 +378,51 @@ partial def elabCommand (stx : Syntax) : CommandElabM Unit := do
|
|||
withInfoTreeContext (mkInfoTree := mkInfoTree decl stx) do
|
||||
let stxNew ← liftMacroM <| liftExcept stxNew?
|
||||
withMacroExpansion stx stxNew do
|
||||
elabCommand stxNew
|
||||
-- Support incrementality; see also Note [Incremental Macros]
|
||||
if let some snap := (←read).snap? then
|
||||
-- Unpack nested commands; see `MacroExpandedSnapshot.next`
|
||||
let cmds := if stxNew.isOfKind nullKind then stxNew.getArgs else #[stxNew]
|
||||
let nextMacroScope := (← get).nextMacroScope
|
||||
let hasTraces := (← getTraceState).traces.size > 0
|
||||
let oldSnap? := do
|
||||
let oldSnap ← snap.old?
|
||||
let oldSnap ← oldSnap.val.get.toTyped? MacroExpandedSnapshot
|
||||
guard <| oldSnap.macroDecl == decl && oldSnap.newNextMacroScope == nextMacroScope
|
||||
-- check absence of traces; see Note [Incremental Macros]
|
||||
guard <| !oldSnap.hasTraces && !hasTraces
|
||||
return oldSnap
|
||||
let oldCmds? := oldSnap?.map fun old =>
|
||||
if old.newStx.isOfKind nullKind then old.newStx.getArgs else #[old.newStx]
|
||||
Language.withAlwaysResolvedPromises cmds.size fun promises => do
|
||||
snap.new.resolve <| .ofTyped {
|
||||
diagnostics := .empty
|
||||
macroDecl := decl
|
||||
newStx := stxNew
|
||||
newNextMacroScope := nextMacroScope
|
||||
hasTraces
|
||||
next := promises.zipWith cmds fun promise arg =>
|
||||
{ range? := arg.getRange?, task := promise.result }
|
||||
: MacroExpandedSnapshot
|
||||
}
|
||||
-- After the first command whose syntax tree changed, we must disable
|
||||
-- incremental reuse
|
||||
let mut reusedCmds := true
|
||||
let opts ← getOptions
|
||||
-- For each command, associate it with new promise and old snapshot, if any, and
|
||||
-- elaborate recursively
|
||||
for cmd in cmds, promise in promises, i in [0:cmds.size] do
|
||||
let oldCmd? := oldCmds?.bind (·[i]?)
|
||||
withReader ({ · with snap? := some {
|
||||
new := promise
|
||||
old? := do
|
||||
guard reusedCmds
|
||||
let old ← oldSnap?
|
||||
return { stx := (← oldCmd?), val := (← old.next[i]?) }
|
||||
} }) do
|
||||
elabCommand cmd
|
||||
reusedCmds := reusedCmds && oldCmd?.any (·.structRangeEqWithTraceReuse opts cmd)
|
||||
else
|
||||
elabCommand stxNew
|
||||
| _ =>
|
||||
match commandElabAttribute.getEntries s.env k with
|
||||
| [] =>
|
||||
|
|
|
|||
|
|
@ -188,34 +188,42 @@ def elabClassInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Uni
|
|||
let v ← classInductiveSyntaxToView modifiers stx
|
||||
elabInductiveViews #[v]
|
||||
|
||||
/--
|
||||
Macro that expands a declaration with a complex name into an explicit `namespace` block.
|
||||
Implementing this step as a macro means that reuse checking is handled by `elabCommand`.
|
||||
-/
|
||||
@[builtin_macro Lean.Parser.Command.declaration]
|
||||
def expandNamespacedDeclaration : Macro := fun stx => do
|
||||
match (← expandDeclNamespace? stx) with
|
||||
| some (ns, newStx) => do
|
||||
-- Limit ref variability for incrementality; see Note [Incremental Macros]
|
||||
let declTk := stx[1][0]
|
||||
let ns := mkIdentFrom declTk ns
|
||||
withRef declTk `(namespace $ns $(⟨newStx⟩) end $ns)
|
||||
| none => Macro.throwUnsupported
|
||||
|
||||
@[builtin_command_elab declaration, builtin_incremental]
|
||||
def elabDeclaration : CommandElab := fun stx => do
|
||||
match (← liftMacroM <| expandDeclNamespace? stx) with
|
||||
| some (ns, newStx) => do
|
||||
let ns := mkIdentFrom stx ns
|
||||
let newStx ← `(namespace $ns $(⟨newStx⟩) end $ns)
|
||||
withMacroExpansion stx newStx <| elabCommand newStx
|
||||
| none => do
|
||||
let decl := stx[1]
|
||||
let declKind := decl.getKind
|
||||
if isDefLike decl then
|
||||
-- only case implementing incrementality currently
|
||||
elabMutualDef #[stx]
|
||||
else withoutCommandIncrementality true do
|
||||
if declKind == ``Lean.Parser.Command.«axiom» then
|
||||
let modifiers ← elabModifiers stx[0]
|
||||
elabAxiom modifiers decl
|
||||
else if declKind == ``Lean.Parser.Command.«inductive» then
|
||||
let modifiers ← elabModifiers stx[0]
|
||||
elabInductive modifiers decl
|
||||
else if declKind == ``Lean.Parser.Command.classInductive then
|
||||
let modifiers ← elabModifiers stx[0]
|
||||
elabClassInductive modifiers decl
|
||||
else if declKind == ``Lean.Parser.Command.«structure» then
|
||||
let modifiers ← elabModifiers stx[0]
|
||||
elabStructure modifiers decl
|
||||
else
|
||||
throwError "unexpected declaration"
|
||||
let decl := stx[1]
|
||||
let declKind := decl.getKind
|
||||
if isDefLike decl then
|
||||
-- only case implementing incrementality currently
|
||||
elabMutualDef #[stx]
|
||||
else withoutCommandIncrementality true do
|
||||
if declKind == ``Lean.Parser.Command.«axiom» then
|
||||
let modifiers ← elabModifiers stx[0]
|
||||
elabAxiom modifiers decl
|
||||
else if declKind == ``Lean.Parser.Command.«inductive» then
|
||||
let modifiers ← elabModifiers stx[0]
|
||||
elabInductive modifiers decl
|
||||
else if declKind == ``Lean.Parser.Command.classInductive then
|
||||
let modifiers ← elabModifiers stx[0]
|
||||
elabClassInductive modifiers decl
|
||||
else if declKind == ``Lean.Parser.Command.«structure» then
|
||||
let modifiers ← elabModifiers stx[0]
|
||||
elabStructure modifiers decl
|
||||
else
|
||||
throwError "unexpected declaration"
|
||||
|
||||
/-- Return true if all elements of the mutual-block are inductive declarations. -/
|
||||
private def isMutualInductive (stx : Syntax) : Bool :=
|
||||
|
|
@ -306,6 +314,10 @@ def expandMutualElement : Macro := fun stx => do
|
|||
let mut elemsNew := #[]
|
||||
let mut modified := false
|
||||
for elem in stx[1].getArgs do
|
||||
-- Don't trigger the `expandNamespacedDecl` macro, the namespace is handled by the mutual def
|
||||
-- elaborator directly instead
|
||||
if elem.isOfKind ``Parser.Command.declaration then
|
||||
continue
|
||||
match (← expandMacro? elem) with
|
||||
| some elemNew => elemsNew := elemsNew.push elemNew; modified := true
|
||||
| none => elemsNew := elemsNew.push elem
|
||||
|
|
|
|||
|
|
@ -201,32 +201,20 @@ where
|
|||
withReader ({ · with elaborator := m.declName }) do
|
||||
withTacticInfoContext stx do
|
||||
let stx' ← adaptMacro m.value stx
|
||||
/-
|
||||
If we have a macro, we can always support incrementality: we can assume that in the
|
||||
old and new version, behavior is determined solely by the unfolding and can rely on
|
||||
its incrementality guarantees. We only have to update `tacSnap?` to point to the old
|
||||
unfolding.
|
||||
|
||||
Caveat 1: Apart from the unfolding itself, macro execution does have two additional
|
||||
outputs: modifications to the next macro scope and to the traces. We check that the
|
||||
next macro scope is unchanged below but choose to ignore the traces as they should not
|
||||
have an effect on functional correctness of reuse and usually should not depend on the
|
||||
nested tactics that we are trying to make incremental.
|
||||
|
||||
Caveat 2: As the default `ref` of a macro spans its entire syntax tree and is applied
|
||||
to any token created from a quotation, the ref usually has to be changed to a less
|
||||
variable source to achieve incrementality. See the implementation of tactic `have` for
|
||||
an example.
|
||||
-/
|
||||
-- Support incrementality; see also Note [Incremental Macros]
|
||||
if evalFns.isEmpty && ms.isEmpty then -- Only try incrementality in one branch
|
||||
if let some snap := (← readThe Term.Context).tacSnap? then
|
||||
let nextMacroScope := (← getThe Core.State).nextMacroScope
|
||||
let traceState ← getTraceState
|
||||
let old? := do
|
||||
let old ← snap.old?
|
||||
-- If the kind is equal, we can assume the old version was a macro as well
|
||||
guard <| old.stx.isOfKind stx.getKind
|
||||
let state ← old.val.get.data.finished.get.state?
|
||||
guard <| state.term.meta.core.nextMacroScope == nextMacroScope
|
||||
-- check absence of traces; see Note [Incremental Macros]
|
||||
guard <| state.term.meta.core.traceState.traces.size == 0
|
||||
guard <| traceState.traces.size == 0
|
||||
return old.val.get
|
||||
Language.withAlwaysResolvedPromise fun promise => do
|
||||
-- Store new unfolding in the snapshot tree
|
||||
|
|
|
|||
|
|
@ -228,7 +228,6 @@ structure DynamicSnapshot where
|
|||
val : Dynamic
|
||||
/-- Snapshot tree retrieved from `val` before erasure. -/
|
||||
tree : SnapshotTree
|
||||
deriving Nonempty
|
||||
|
||||
instance : ToSnapshotTree DynamicSnapshot where
|
||||
toSnapshotTree s := s.tree
|
||||
|
|
@ -243,6 +242,9 @@ def DynamicSnapshot.toTyped? (α : Type) [TypeName α] (snap : DynamicSnapshot)
|
|||
Option α :=
|
||||
snap.val.get? α
|
||||
|
||||
instance : Inhabited DynamicSnapshot where
|
||||
default := .ofTyped { diagnostics := .empty : SnapshotLeaf }
|
||||
|
||||
/--
|
||||
Runs a tree of snapshots to conclusion, incrementally performing `f` on each snapshot in tree
|
||||
preorder. -/
|
||||
|
|
|
|||
|
|
@ -140,6 +140,26 @@ times, here is a summary of what it has to do to implement incrementality:
|
|||
a wildcard pattern
|
||||
-/
|
||||
|
||||
/-
|
||||
# Note [Incremental Macros]
|
||||
|
||||
If we have a macro, we can cheaply support incrementality: as a macro is a pure function, if all
|
||||
outputs apart from the expanded syntax tree itself are identical in two document versions, we can
|
||||
simply delegate reuse detection to the subsequently called elaborator. All we have to do is to
|
||||
forward the old unfolding, if any, to it in the appropriate context field and store the new
|
||||
unfolding for that purpose in a new snapshot node whose child will be filled by the called
|
||||
elaborator. This is currently implemented for command and tactic macros.
|
||||
|
||||
Caveat 1: Traces are an additional output of macro expansion but because they are hard to compare
|
||||
and should not be active in standard use cases, we disable incrementality if either version produced
|
||||
traces.
|
||||
|
||||
Caveat 2: As the default `ref` of a macro spans its entire syntax tree and is applied to any token
|
||||
created from a quotation, the ref usually has to be changed to a less variable source using
|
||||
`withRef` to achieve effective incrementality. See `Elab.Command.expandNamespacedDeclaration` for a
|
||||
simple example and the implementation of tactic `have` for a complex example.
|
||||
-/
|
||||
|
||||
set_option linter.missingDocs true
|
||||
|
||||
namespace Lean.Language.Lean
|
||||
|
|
|
|||
|
|
@ -38,3 +38,29 @@ def map' {α β} (f : α → β) : List α → List β :=
|
|||
--^ collectDiagnostics
|
||||
--^ insert: "\n"
|
||||
--^ collectDiagnostics
|
||||
|
||||
/-! Reuse should work through the namespaced decl macro. -/
|
||||
-- RESET
|
||||
def ns.n : (by dbg_trace "ns 0"; exact Nat) := by
|
||||
dbg_trace "ns 1"
|
||||
--^ sync
|
||||
--^ insert: ".5"
|
||||
exact 0
|
||||
|
||||
/-! Changing the namespace should prohibit def reuse. -/
|
||||
-- RESET
|
||||
def nt.n : (by dbg_trace "nt 0"; exact Nat) := by
|
||||
--^ sync
|
||||
--^ change: "t" "u"
|
||||
dbg_trace "nt 1"
|
||||
exact 0
|
||||
|
||||
/-! Reuse should support `in`. -/
|
||||
-- RESET
|
||||
set_option trace.Elab.definition.body true in
|
||||
def so : Nat := by
|
||||
dbg_trace "so 0"
|
||||
dbg_trace "so 1"
|
||||
--^ sync
|
||||
--^ insert: ".5"
|
||||
exact 0
|
||||
|
|
|
|||
|
|
@ -19,3 +19,13 @@ h 0 1
|
|||
h 1 1
|
||||
{"version": 1, "uri": "file:///incrementalMutual.lean", "diagnostics": []}
|
||||
{"version": 2, "uri": "file:///incrementalMutual.lean", "diagnostics": []}
|
||||
ns 0
|
||||
ns 1
|
||||
ns 1.5
|
||||
nt 0
|
||||
nt 1
|
||||
nt 0
|
||||
nt 1
|
||||
so 0
|
||||
so 1
|
||||
so 1.5
|
||||
|
|
|
|||
|
|
@ -19,7 +19,7 @@ inst✝ inst : α
|
|||
shadow.lean:17:0-17:1: error: don't know how to synthesize placeholder
|
||||
context:
|
||||
α : Type u_1
|
||||
inst.71 : Inhabited α
|
||||
inst.75 : Inhabited α
|
||||
inst inst : α
|
||||
⊢ {β δ : Type} → α → β → δ → α × β × δ
|
||||
shadow.lean:20:0-20:1: error: don't know how to synthesize placeholder
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue