feat: incremental have (#4308)
Implemented as a macro special case, with some implementation caveats
This commit is contained in:
Sebastian Ullrich
GitHub
parent
9d46961236
commit
d45952e386
10 changed files with 208 additions and 26 deletions
|
|
@ -20,24 +20,27 @@ private def formatInfo (showInfo : Bool) (info : SourceInfo) (f : Format) : Form
|
|||
| true, SourceInfo.synthetic pos endPos false => f!"{pos}:{f}:{endPos}"
|
||||
| _, _ => f
|
||||
|
||||
partial def formatStxAux (maxDepth : Option Nat) (showInfo : Bool) : Nat → Syntax → Format
|
||||
| _, atom info val => formatInfo showInfo info $ format (repr val)
|
||||
| _, ident info _ val _ => formatInfo showInfo info $ format "`" ++ format val
|
||||
| _, missing => "<missing>"
|
||||
| depth, node _ kind args =>
|
||||
partial def formatStxAux (maxDepth : Option Nat) (showInfo : Bool) (depth : Nat) : Syntax → Format
|
||||
| atom info val => formatInfo showInfo info <| format (repr val)
|
||||
| ident info _ val _ => formatInfo showInfo info <| format "`" ++ format val
|
||||
| missing => "<missing>"
|
||||
| node info kind args =>
|
||||
let depth := depth + 1;
|
||||
if kind == nullKind then
|
||||
sbracket $
|
||||
sbracket <|
|
||||
if args.size > 0 && depth > maxDepth.getD depth then
|
||||
".."
|
||||
else
|
||||
joinSep (args.toList.map (formatStxAux maxDepth showInfo depth)) line
|
||||
else
|
||||
let shorterName := kind.replacePrefix `Lean.Parser Name.anonymous;
|
||||
let header := format shorterName;
|
||||
let shorterName := kind.replacePrefix `Lean.Parser Name.anonymous
|
||||
let header := formatInfo showInfo info <| format shorterName
|
||||
let body : List Format :=
|
||||
if args.size > 0 && depth > maxDepth.getD depth then [".."] else args.toList.map (formatStxAux maxDepth showInfo depth);
|
||||
paren $ joinSep (header :: body) line
|
||||
if args.size > 0 && depth > maxDepth.getD depth then
|
||||
[".."]
|
||||
else
|
||||
args.toList.map (formatStxAux maxDepth showInfo depth)
|
||||
paren <| joinSep (header :: body) line
|
||||
|
||||
/-- Pretty print the given syntax `stx` as a `Format`.
|
||||
Nodes deeper than `maxDepth` are omitted.
|
||||
|
|
|
|||
|
|
@ -699,7 +699,37 @@ The `have` tactic is for adding hypotheses to the local context of the main goal
|
|||
For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
|
||||
hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
|
||||
-/
|
||||
macro "have " d:haveDecl : tactic => `(tactic| refine_lift have $d:haveDecl; ?_)
|
||||
syntax "have " haveDecl : tactic
|
||||
macro_rules
|
||||
-- special case: when given a nested `by` block, move it outside of the `refine` to enable
|
||||
-- incrementality
|
||||
| `(tactic| have%$haveTk $id:haveId $bs* : $type := by%$byTk $tacs*) => do
|
||||
/-
|
||||
We want to create the syntax
|
||||
```
|
||||
focus
|
||||
refine no_implicit_lambda% (have $id:haveId $bs* : $type := ?body; ?_)
|
||||
case body => $tacs*
|
||||
```
|
||||
However, we need to be very careful with the syntax infos involved:
|
||||
* We want most infos up to `tacs` to be independent of changes inside it so that incrementality
|
||||
is not prematurely disabled; we use the `have` and then the `by` token as the reference for
|
||||
this. Note that if we did nothing, the reference would be the entire `have` input and so any
|
||||
change to `tacs` would change every token synthesized below.
|
||||
* For the single node of the `case` body, we *should not* change the ref as this makes sure the
|
||||
entire tactic block is included in any "unsaved goals" message (which is emitted after
|
||||
execution of all nested tactics so it is indeed safe for `evalCase` to ignore it for
|
||||
incrementality).
|
||||
* Even after setting the ref, we still need a `with_annotate_state` to show the correct tactic
|
||||
state on `by` as the synthetic info derived from the ref is ignored for this purpose.
|
||||
-/
|
||||
let tac ← Lean.withRef byTk `(tactic| with_annotate_state $byTk ($tacs*))
|
||||
let tac ← `(tacticSeq| $tac:tactic)
|
||||
let tac ← Lean.withRef byTk `(tactic| case body => $(.mk tac):tacticSeq)
|
||||
Lean.withRef haveTk `(tactic| focus
|
||||
refine no_implicit_lambda% (have $id:haveId $bs* : $type := ?body; ?_)
|
||||
$tac)
|
||||
| `(tactic| have $d:haveDecl) => `(tactic| refine_lift have $d:haveDecl; ?_)
|
||||
|
||||
/--
|
||||
Given a main goal `ctx ⊢ t`, `suffices h : t' from e` replaces the main goal with `ctx ⊢ t'`,
|
||||
|
|
|
|||
|
|
@ -182,8 +182,7 @@ def mkDecEqEnum (declName : Name) : CommandElabM Unit := do
|
|||
fun x y =>
|
||||
if h : x.toCtorIdx = y.toCtorIdx then
|
||||
-- We use `rfl` in the following proof because the first script fails for unit-like datatypes due to etaStruct.
|
||||
-- Temporarily avoiding tactic `have` for bootstrapping
|
||||
isTrue (by first | refine_lift have aux := congrArg $ofNatIdent h; ?_; rw [$auxThmIdent:ident, $auxThmIdent:ident] at aux; assumption | rfl)
|
||||
isTrue (by first | have aux := congrArg $ofNatIdent h; rw [$auxThmIdent:ident, $auxThmIdent:ident] at aux; assumption | rfl)
|
||||
else
|
||||
isFalse fun h => by subst h; contradiction
|
||||
)
|
||||
|
|
|
|||
|
|
@ -201,6 +201,49 @@ 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.
|
||||
-/
|
||||
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 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
|
||||
return old.val.get
|
||||
Language.withAlwaysResolvedPromise fun promise => do
|
||||
-- Store new unfolding in the snapshot tree
|
||||
snap.new.resolve <| .mk {
|
||||
stx := stx'
|
||||
diagnostics := .empty
|
||||
finished := .pure { state? := (← Tactic.saveState) }
|
||||
} #[{ range? := stx'.getRange?, task := promise.result }]
|
||||
-- Update `tacSnap?` to old unfolding
|
||||
withTheReader Term.Context ({ · with tacSnap? := some {
|
||||
new := promise
|
||||
old? := do
|
||||
let old ← old?
|
||||
return ⟨old.data.stx, (← old.next.get? 0)⟩
|
||||
} }) do
|
||||
evalTactic stx'
|
||||
return
|
||||
evalTactic stx'
|
||||
catch ex => handleEx s failures ex (expandEval s ms evalFns)
|
||||
|
||||
|
|
|
|||
|
|
@ -21,10 +21,10 @@ namespace Lean.Elab.Tactic
|
|||
open Meta
|
||||
open Parser.Tactic
|
||||
|
||||
@[builtin_tactic withAnnotateState] def evalWithAnnotateState : Tactic
|
||||
| `(tactic| with_annotate_state $stx $t) =>
|
||||
withTacticInfoContext stx (evalTactic t)
|
||||
| _ => throwUnsupportedSyntax
|
||||
@[builtin_tactic withAnnotateState, builtin_incremental] def evalWithAnnotateState : Tactic :=
|
||||
fun stx =>
|
||||
withTacticInfoContext stx[1] do
|
||||
Term.withNarrowedArgTacticReuse (argIdx := 2) evalTactic stx
|
||||
|
||||
@[builtin_tactic Lean.Parser.Tactic.«done»] def evalDone : Tactic := fun _ =>
|
||||
done
|
||||
|
|
@ -114,8 +114,8 @@ where
|
|||
@[builtin_tactic seq1] def evalSeq1 : Tactic := fun stx =>
|
||||
evalSepTactics stx[0]
|
||||
|
||||
@[builtin_tactic paren] def evalParen : Tactic := fun stx =>
|
||||
evalTactic stx[1]
|
||||
@[builtin_tactic paren, builtin_incremental] def evalParen : Tactic :=
|
||||
Term.withNarrowedArgTacticReuse 1 evalTactic
|
||||
|
||||
def isCheckpointableTactic (arg : Syntax) : TacticM Bool := do
|
||||
-- TODO: make it parametric
|
||||
|
|
@ -205,12 +205,12 @@ def evalTacticCDot : Tactic := fun stx => do
|
|||
withInfoContext (pure ()) initInfo
|
||||
Term.withNarrowedArgTacticReuse (argIdx := 1) evalTactic stx
|
||||
|
||||
@[builtin_tactic Parser.Tactic.focus] def evalFocus : Tactic := fun stx => do
|
||||
@[builtin_tactic Parser.Tactic.focus, builtin_incremental] def evalFocus : Tactic := fun stx => do
|
||||
let mkInfo ← mkInitialTacticInfo stx[0]
|
||||
focus do
|
||||
-- show focused state on `focus`
|
||||
withInfoContext (pure ()) mkInfo
|
||||
evalTactic stx[1]
|
||||
Term.withNarrowedArgTacticReuse (argIdx := 1) evalTactic stx
|
||||
|
||||
private def getOptRotation (stx : Syntax) : Nat :=
|
||||
if stx.isNone then 1 else stx[0].toNat
|
||||
|
|
|
|||
|
|
@ -162,7 +162,7 @@ Always resolving promises involved in the snapshot tree is important to avoid de
|
|||
language server.
|
||||
-/
|
||||
def withAlwaysResolvedPromise [Monad m] [MonadLiftT BaseIO m] [MonadFinally m] [Inhabited α]
|
||||
(act : IO.Promise α → m Unit) : m Unit := do
|
||||
(act : IO.Promise α → m β) : m β := do
|
||||
let p ← IO.Promise.new
|
||||
try
|
||||
act p
|
||||
|
|
|
|||
|
|
@ -1,3 +1,6 @@
|
|||
-- The `fullRange` should span each entire block
|
||||
--^ collectDiagnostics
|
||||
|
||||
example : False := by
|
||||
have : True := by
|
||||
skip
|
||||
|
|
|
|||
|
|
@ -1,12 +1,49 @@
|
|||
{"version": 1,
|
||||
"uri": "file:///haveInfo.lean",
|
||||
"diagnostics":
|
||||
[{"source": "Lean 4",
|
||||
"severity": 1,
|
||||
"range":
|
||||
{"start": {"line": 4, "character": 17}, "end": {"line": 5, "character": 0}},
|
||||
"message": "unsolved goals\n⊢ True",
|
||||
"fullRange":
|
||||
{"start": {"line": 4, "character": 17}, "end": {"line": 7, "character": 8}}},
|
||||
{"source": "Lean 4",
|
||||
"severity": 1,
|
||||
"range":
|
||||
{"start": {"line": 11, "character": 17},
|
||||
"end": {"line": 12, "character": 0}},
|
||||
"message": "unsolved goals\n⊢ True",
|
||||
"fullRange":
|
||||
{"start": {"line": 11, "character": 17},
|
||||
"end": {"line": 14, "character": 8}}},
|
||||
{"source": "Lean 4",
|
||||
"severity": 1,
|
||||
"range":
|
||||
{"start": {"line": 18, "character": 17},
|
||||
"end": {"line": 19, "character": 0}},
|
||||
"message": "unsolved goals\n⊢ True",
|
||||
"fullRange":
|
||||
{"start": {"line": 18, "character": 17},
|
||||
"end": {"line": 21, "character": 8}}},
|
||||
{"source": "Lean 4",
|
||||
"severity": 1,
|
||||
"range":
|
||||
{"start": {"line": 25, "character": 17},
|
||||
"end": {"line": 26, "character": 0}},
|
||||
"message": "unsolved goals\n⊢ True",
|
||||
"fullRange":
|
||||
{"start": {"line": 25, "character": 17},
|
||||
"end": {"line": 28, "character": 8}}}]}
|
||||
{"textDocument": {"uri": "file:///haveInfo.lean"},
|
||||
"position": {"line": 2, "character": 4}}
|
||||
"position": {"line": 5, "character": 4}}
|
||||
{"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]}
|
||||
{"textDocument": {"uri": "file:///haveInfo.lean"},
|
||||
"position": {"line": 8, "character": 17}}
|
||||
"position": {"line": 11, "character": 17}}
|
||||
{"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]}
|
||||
{"textDocument": {"uri": "file:///haveInfo.lean"},
|
||||
"position": {"line": 15, "character": 17}}
|
||||
"position": {"line": 18, "character": 17}}
|
||||
{"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]}
|
||||
{"textDocument": {"uri": "file:///haveInfo.lean"},
|
||||
"position": {"line": 23, "character": 2}}
|
||||
"position": {"line": 26, "character": 2}}
|
||||
{"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]}
|
||||
|
|
|
|||
|
|
@ -20,3 +20,24 @@ def case (h : a ∨ b) : True := by
|
|||
--^ sync
|
||||
--^ insert: ".5"
|
||||
dbg_trace "d 3"
|
||||
|
||||
-- RESET
|
||||
def have : True := by
|
||||
dbg_trace "h 0"
|
||||
have : True := by
|
||||
dbg_trace "h 1"
|
||||
dbg_trace "h 2"
|
||||
--^ sync
|
||||
--^ insert: ".5"
|
||||
dbg_trace "h 3"
|
||||
|
||||
/-!
|
||||
Updating the `have` header should update the unsolved goals position (and currently re-run the body)
|
||||
-/
|
||||
-- RESET
|
||||
def spaceHave : True := by
|
||||
have : True := by
|
||||
--^ collectDiagnostics
|
||||
--^ insert: " "
|
||||
--^ collectDiagnostics
|
||||
dbg_trace "sh"
|
||||
|
|
|
|||
|
|
@ -8,3 +8,49 @@ d 2
|
|||
d 3
|
||||
d 2.5
|
||||
d 3
|
||||
h 0
|
||||
h 1
|
||||
h 2
|
||||
h 3
|
||||
h 2.5
|
||||
h 3
|
||||
sh
|
||||
{"version": 1,
|
||||
"uri": "file:///incrementalCombinator.lean",
|
||||
"diagnostics":
|
||||
[{"source": "Lean 4",
|
||||
"severity": 1,
|
||||
"range":
|
||||
{"start": {"line": 2, "character": 17}, "end": {"line": 3, "character": 0}},
|
||||
"message": "unsolved goals\n⊢ True",
|
||||
"fullRange":
|
||||
{"start": {"line": 2, "character": 17},
|
||||
"end": {"line": 6, "character": 18}}},
|
||||
{"source": "Lean 4",
|
||||
"severity": 1,
|
||||
"range":
|
||||
{"start": {"line": 1, "character": 24}, "end": {"line": 2, "character": 0}},
|
||||
"message": "unsolved goals\nthis : True\n⊢ True",
|
||||
"fullRange":
|
||||
{"start": {"line": 1, "character": 24},
|
||||
"end": {"line": 6, "character": 18}}}]}
|
||||
sh
|
||||
{"version": 2,
|
||||
"uri": "file:///incrementalCombinator.lean",
|
||||
"diagnostics":
|
||||
[{"source": "Lean 4",
|
||||
"severity": 1,
|
||||
"range":
|
||||
{"start": {"line": 2, "character": 18}, "end": {"line": 3, "character": 0}},
|
||||
"message": "unsolved goals\n⊢ True",
|
||||
"fullRange":
|
||||
{"start": {"line": 2, "character": 18},
|
||||
"end": {"line": 6, "character": 18}}},
|
||||
{"source": "Lean 4",
|
||||
"severity": 1,
|
||||
"range":
|
||||
{"start": {"line": 1, "character": 24}, "end": {"line": 2, "character": 0}},
|
||||
"message": "unsolved goals\nthis : True\n⊢ True",
|
||||
"fullRange":
|
||||
{"start": {"line": 1, "character": 24},
|
||||
"end": {"line": 6, "character": 18}}}]}
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue