|
| 1 | +/- |
| 2 | +Copyright (c) 2026 Lean FRO LLC. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Author: David Thrane Christiansen |
| 5 | +-/ |
| 6 | +import Verso |
| 7 | +import SubVerso.Highlighting.Code |
| 8 | + |
| 9 | +/-! |
| 10 | +Highlighting a proof that uses compound tactics such as `obtain` produces nested proof states: the |
| 11 | +whole-`obtain` region carries a useful goal, and its inner tactic script closes its goal at the same |
| 12 | +position where the outer region ends. Rendering both would put two toggle widgets at the same spot, |
| 13 | +so `Highlighted.elideRedundantProofStates` drops the inner empty state before rendering. |
| 14 | +
|
| 15 | +This test highlights such a proof with SubVerso and checks that the redundant empty state has been elided. |
| 16 | +-/ |
| 17 | + |
| 18 | +open SubVerso.Compat.Frontend (processCommands) |
| 19 | +open SubVerso.Highlighting (Highlighted highlightFrontendResult) |
| 20 | +open Verso.Code (HighlightHtmlM) |
| 21 | +open Verso.Doc (Genre) |
| 22 | +open Verso.Output (Html) |
| 23 | +open Lean Elab Command |
| 24 | + |
| 25 | +namespace Verso.NestedTacticHtmlTest |
| 26 | + |
| 27 | +/-- |
| 28 | +The proof to highlight. `exists_prime_factor` proves that every number larger than 1 has a prime |
| 29 | +factor; its two `obtain` tactics each run an inner script that closes the goal at the position where |
| 30 | +the outer state ends. |
| 31 | +-/ |
| 32 | +def proofSource : String := |
| 33 | +"def IsPrime (n : Nat) := 1 < n ∧ ∀ k, 1 < k → k < n → ¬ k ∣ n |
| 34 | +
|
| 35 | +theorem exists_prime_factor : |
| 36 | + ∀ n, 1 < n → ∃ k, IsPrime k ∧ k ∣ n := by |
| 37 | + intro n h1 |
| 38 | + by_cases hprime : IsPrime n |
| 39 | + · grind [Nat.dvd_refl] |
| 40 | + · obtain ⟨k, _⟩ : ∃ k, 1 < k ∧ k < n ∧ k ∣ n := by |
| 41 | + simp_all [IsPrime] |
| 42 | + obtain ⟨p, _, _⟩ := exists_prime_factor k (by grind) |
| 43 | + grind [Nat.dvd_trans]" |
| 44 | + |
| 45 | +/-- |
| 46 | +Highlights a Lean string. |
| 47 | +-/ |
| 48 | +def highlightModule (input : String) : CommandElabM Highlighted := do |
| 49 | + let inputCtx := Parser.mkInputContext input "<nested-tactic-test>" |
| 50 | + let commandState : Command.State := { env := (← getEnv), maxRecDepth := (← get).maxRecDepth } |
| 51 | + let commandState := |
| 52 | + let sc := commandState.scopes[0]! |
| 53 | + { commandState with scopes := { sc with opts := sc.opts.setBool `pp.tagAppFns true } :: commandState.scopes.tail! } |
| 54 | + let (result, _) ← processCommands mkNullNode |
| 55 | + |>.run { inputCtx } |>.run { commandState, parserState := {}, cmdPos := 0 } |
| 56 | + let result := result.updateLeading input |
| 57 | + runTermElabM fun _ => |
| 58 | + withTheReader Core.Context (fun ctx => { ctx with fileMap := inputCtx.fileMap }) do |
| 59 | + let hls ← highlightFrontendResult result |
| 60 | + return hls.foldl (· ++ ·) .empty |
| 61 | + |
| 62 | +/-! |
| 63 | +# Recognizing the redundant pattern in the `Highlighted` tree |
| 64 | +-/ |
| 65 | + |
| 66 | +/-- Whitespace and other content that does not render as a visible element. -/ |
| 67 | +def insignificant : Highlighted → Bool |
| 68 | + | .text s => s.trimAscii.isEmpty |
| 69 | + | .unparsed s => s.trimAscii.isEmpty |
| 70 | + | hl => hl.isEmpty |
| 71 | + |
| 72 | +/-- The last visible element of `hl`, looking through `.seq` tails and `.span`. -/ |
| 73 | +partial def lastElement? : Highlighted → Option Highlighted |
| 74 | + | .seq xs => (xs.toList.reverse.find? (!insignificant ·)).bind lastElement? |
| 75 | + | .span _ x => lastElement? x |
| 76 | + | hl => if insignificant hl then none else some hl |
| 77 | + |
| 78 | +/-- |
| 79 | +Whether `hl` contains a proof state with a non-empty goal array whose last element is a proof state |
| 80 | +with an empty goals array. |
| 81 | +-/ |
| 82 | +partial def hlHasRedundant : Highlighted → Bool |
| 83 | + | .seq xs => xs.any hlHasRedundant |
| 84 | + | .span _ x => hlHasRedundant x |
| 85 | + | .tactics info _ _ content => |
| 86 | + let lastIsNoGoals := |
| 87 | + match lastElement? content with |
| 88 | + | some (.tactics innerInfo ..) => innerInfo.isEmpty |
| 89 | + | _ => false |
| 90 | + (!info.isEmpty && lastIsNoGoals) || hlHasRedundant content |
| 91 | + | _ => false |
| 92 | + |
| 93 | +/-! ## Recognizing proof states and their nesting in the rendered HTML -/ |
| 94 | + |
| 95 | +/-- A simulation of the HTML proof state tree -/ |
| 96 | +structure ProofState where |
| 97 | + /-- Whether this state shows "no goals" rather than a list of goals. -/ |
| 98 | + noGoals : Bool |
| 99 | + /-- |
| 100 | + Whether the last visible element of this state's code is itself a no-goals proof state. Such an |
| 101 | + inner state ends where this one ends, so the two toggle widgets land at the same spot. |
| 102 | + -/ |
| 103 | + endsWithNoGoals : Bool |
| 104 | + /-- The proof states nested inside this one. -/ |
| 105 | + children : List ProofState |
| 106 | + |
| 107 | +/-- Whether `attrs` assigns the CSS class `cls`. -/ |
| 108 | +def hasClass (attrs : Array (String × String)) (cls : String) : Bool := |
| 109 | + attrs.any fun (k, v) => k == "class" && (v.splitOn " ").contains cls |
| 110 | + |
| 111 | +/-- The concatenated text content of an HTML fragment. -/ |
| 112 | +partial def htmlText : Html → String |
| 113 | + | .text _ s => s |
| 114 | + | .tag _ _ contents => htmlText contents |
| 115 | + | .seq xs => xs.foldl (fun acc x => acc ++ htmlText x) "" |
| 116 | + |
| 117 | +/-- The direct children of an HTML fragment. -/ |
| 118 | +def directChildren : Html → Array Html |
| 119 | + | .seq xs => xs |
| 120 | + | hl => #[hl] |
| 121 | + |
| 122 | +/-- Whether an HTML fragment renders as nothing visible (whitespace or empty). -/ |
| 123 | +partial def htmlInsignificant : Html → Bool |
| 124 | + | .text _ s => s.trimAscii.isEmpty |
| 125 | + | .seq xs => xs.all htmlInsignificant |
| 126 | + | .tag .. => false |
| 127 | + |
| 128 | +/-- The last visible element of an HTML fragment, looking through `.seq` tails. -/ |
| 129 | +partial def htmlLastVisible? : Html → Option Html |
| 130 | + | .seq xs => (xs.toList.reverse.find? (!htmlInsignificant ·)).bind htmlLastVisible? |
| 131 | + | hl => if htmlInsignificant hl then none else some hl |
| 132 | + |
| 133 | +/-- The direct child of `contents` that is a `<span>` with the given class, if any. -/ |
| 134 | +def childSpanWithClass (contents : Html) (cls : String) : Option Html := |
| 135 | + (directChildren contents).find? fun h => |
| 136 | + match h with |
| 137 | + | .tag "span" a _ => hasClass a cls |
| 138 | + | _ => false |
| 139 | + |
| 140 | +/-- Whether `html` is a `<span class="tactic">` whose own state shows "no goals". -/ |
| 141 | +def isNoGoalsState : Html → Bool |
| 142 | + | .tag "span" attrs contents => |
| 143 | + if hasClass attrs "tactic" then |
| 144 | + match childSpanWithClass contents "tactic-state" with |
| 145 | + | some s => htmlText s |>.contains "All goals completed" |
| 146 | + | none => false |
| 147 | + else false |
| 148 | + | _ => false |
| 149 | + |
| 150 | +/-- The contents of the `<label>` child of a tactic span. -/ |
| 151 | +def labelContents (contents : Html) : Html := |
| 152 | + let html? := |
| 153 | + directChildren contents |>.findSome? fun |
| 154 | + | .tag "label" _ c => some c |
| 155 | + | _ => none |
| 156 | + html?.getD .empty |
| 157 | + |
| 158 | +/-- |
| 159 | +Extracts the proof-state toggles directly present in an HTML fragment, together with the proof |
| 160 | +states nested inside each one. A toggle is a `<span class="tactic">` whose own state is its direct |
| 161 | +`<span class="tactic-state">` child; the nested states live inside its `<label>`. |
| 162 | +-/ |
| 163 | +partial def proofStates : Html → List ProofState |
| 164 | + | .seq xs => xs.toList.flatMap proofStates |
| 165 | + | .tag name attrs contents => |
| 166 | + if name == "span" && hasClass attrs "tactic" then |
| 167 | + let label := labelContents contents |
| 168 | + [{ noGoals := isNoGoalsState (.tag name attrs contents), |
| 169 | + endsWithNoGoals := htmlLastVisible? label |>.map isNoGoalsState |>.getD false, |
| 170 | + children := proofStates label }] |
| 171 | + else |
| 172 | + proofStates contents |
| 173 | + | .text .. => [] |
| 174 | + |
| 175 | +/-- |
| 176 | +Whether any proof state with goals ends with a no-goals proof state — the redundant nesting that |
| 177 | +puts two toggle widgets at the same spot. |
| 178 | +-/ |
| 179 | +partial def htmlHasRedundant (states : List ProofState) : Bool := |
| 180 | + states.any fun s => (!s.noGoals && s.endsWithNoGoals) || htmlHasRedundant s.children |
| 181 | + |
| 182 | +/-! ## Rendering -/ |
| 183 | + |
| 184 | +private def runHtml (act : HighlightHtmlM Genre.none Html) : Html := |
| 185 | + let ctx : HighlightHtmlM.Context Genre.none := |
| 186 | + { linkTargets := {}, traverseContext := (), definitionIds := {}, options := {} } |
| 187 | + act.run ctx |>.run .empty |>.fst |
| 188 | + |
| 189 | +/-- Renders highlighted code to HTML directly, without the elision preprocessing pass. -/ |
| 190 | +def renderRaw (hl : Highlighted) : Html := runHtml (hl.toHtml) |
| 191 | + |
| 192 | +/-- Renders highlighted code to HTML through the block entry point, which applies the pass. -/ |
| 193 | +def renderBlock (hl : Highlighted) : Html := runHtml (hl.blockHtml "nested-tactic-test") |
| 194 | + |
| 195 | +/-! ## The test -/ |
| 196 | + |
| 197 | +def checkElision : CommandElabM Unit := do |
| 198 | + -- 1. Highlight the proof. |
| 199 | + let raw ← highlightModule proofSource |
| 200 | + |
| 201 | + -- 2. Sanity check: the highlighted proof really contains the redundant nesting. |
| 202 | + unless hlHasRedundant raw do |
| 203 | + throwError "expected the highlighted proof to contain a redundant no-goals state, but found none" |
| 204 | + |
| 205 | + -- 3. The preprocessing pass removes it. |
| 206 | + let elided := raw.elideRedundantProofStates |
| 207 | + if hlHasRedundant elided then |
| 208 | + throwError "`elideRedundantProofStates` left a redundant no-goals state behind" |
| 209 | + |
| 210 | + -- 4. Sanity check: the same redundant nesting is visible in the un-preprocessed HTML. |
| 211 | + unless htmlHasRedundant (proofStates (renderRaw raw)) do |
| 212 | + throwError "expected the un-preprocessed HTML to contain a redundant no-goals region, but found none" |
| 213 | + |
| 214 | + -- 5. The rendered HTML of the preprocessed proof does not. |
| 215 | + if htmlHasRedundant (proofStates (renderBlock raw)) then |
| 216 | + throwError "the rendered HTML still nests a no-goals region inside a goal-ful one" |
| 217 | + |
| 218 | +#guard_msgs in |
| 219 | +#eval checkElision |
0 commit comments