diff --git a/src/Init/Data/Format/Syntax.lean b/src/Init/Data/Format/Syntax.lean index 0a64230315..b876b030d5 100644 --- a/src/Init/Data/Format/Syntax.lean +++ b/src/Init/Data/Format/Syntax.lean @@ -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 => "" - | 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 => "" + | 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. diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 2567d50ce7..d844392858 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -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'`, diff --git a/src/Lean/Elab/Deriving/DecEq.lean b/src/Lean/Elab/Deriving/DecEq.lean index 1a6ecf526f..33b6fedb90 100644 --- a/src/Lean/Elab/Deriving/DecEq.lean +++ b/src/Lean/Elab/Deriving/DecEq.lean @@ -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 ) diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean index 499f5b9af2..3dff09a084 100644 --- a/src/Lean/Elab/Tactic/Basic.lean +++ b/src/Lean/Elab/Tactic/Basic.lean @@ -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) diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean index c0731a7125..4848281857 100644 --- a/src/Lean/Elab/Tactic/BuiltinTactic.lean +++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean @@ -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 diff --git a/src/Lean/Language/Basic.lean b/src/Lean/Language/Basic.lean index e668009e34..514b103de2 100644 --- a/src/Lean/Language/Basic.lean +++ b/src/Lean/Language/Basic.lean @@ -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 diff --git a/tests/lean/interactive/haveInfo.lean b/tests/lean/interactive/haveInfo.lean index 9f83f27bc0..72498db6b4 100644 --- a/tests/lean/interactive/haveInfo.lean +++ b/tests/lean/interactive/haveInfo.lean @@ -1,3 +1,6 @@ +-- The `fullRange` should span each entire block +--^ collectDiagnostics + example : False := by have : True := by skip diff --git a/tests/lean/interactive/haveInfo.lean.expected.out b/tests/lean/interactive/haveInfo.lean.expected.out index bed3a64ebf..786f0ecea5 100644 --- a/tests/lean/interactive/haveInfo.lean.expected.out +++ b/tests/lean/interactive/haveInfo.lean.expected.out @@ -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"]} diff --git a/tests/lean/interactive/incrementalCombinator.lean b/tests/lean/interactive/incrementalCombinator.lean index abb3a4e24b..f5d6b83886 100644 --- a/tests/lean/interactive/incrementalCombinator.lean +++ b/tests/lean/interactive/incrementalCombinator.lean @@ -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" diff --git a/tests/lean/interactive/incrementalCombinator.lean.expected.out b/tests/lean/interactive/incrementalCombinator.lean.expected.out index 340cceda22..73cde7a18c 100644 --- a/tests/lean/interactive/incrementalCombinator.lean.expected.out +++ b/tests/lean/interactive/incrementalCombinator.lean.expected.out @@ -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}}}]}