diff --git a/.github/workflows/bar.yml b/.github/workflows/bar.yml
new file mode 100644
index 0000000..32457ed
--- /dev/null
+++ b/.github/workflows/bar.yml
@@ -0,0 +1,21 @@
+name: verified bar
+
+on:
+ push:
+ pull_request:
+ # Rerun when the spec reviewer approves, or an approval is dismissed.
+ pull_request_review:
+ types: [submitted, dismissed]
+
+jobs:
+ bar:
+ # pull-requests: read lets the check confirm the spec approval on GitHub.
+ permissions:
+ contents: read
+ pull-requests: read
+ # Both lines pin the same commit of Proven-Commons/mission: bar v2, as
+ # proposed in its pull request #2. Move both to a release tag once
+ # mission publishes one.
+ uses: Proven-Commons/mission/.github/workflows/verified-bar.yml@6ba85c27abaaf07905c9316aa96dc29f7b5847a2
+ with:
+ bar-ref: 6ba85c27abaaf07905c9316aa96dc29f7b5847a2
diff --git a/.gitignore b/.gitignore
index 01f8cdb..ae73679 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1,2 @@
.lake/
+__pycache__/
diff --git a/Main.lean b/Main.lean
new file mode 100644
index 0000000..d8bfd04
--- /dev/null
+++ b/Main.lean
@@ -0,0 +1,87 @@
+/-
+ Command line front end, used by the tests.
+
+ Reads one request per line and prints one answer per line. A
+ request is an operation and its input as comma-separated decimal
+ character codes.
+
+ parse 60,97,62,120,60,47,97,62 prints ok:60,97,62,120,60,47,97,62
+ parse 60,97,47,62 prints ok:60,97,47,62
+ parse 120 prints none
+
+ The one operation is `parse`. Its input is the character codes of
+ an XML text in the safe subset. Its answer is `ok:` and the
+ character codes of the canonical print of the parsed document,
+ or `none` when the text is rejected.
+
+ A request is an operation, then optionally one space and its
+ numbers; with no numbers after the space, the input is empty. A
+ malformed request prints `error`: any other line, an unknown
+ operation, a number that is not plain decimal digits, or a
+ character code that is not a Unicode scalar value. A line may end
+ in LF or CR LF; nothing else around a request is ignored.
+
+ The parsing and printing here call `Xml.parse` and `Xml.print`
+ directly. The line handling is covered by the tests, not by a
+ proof.
+-/
+
+import Xml
+
+open Xml
+
+/-- A number in plain decimal digits. Longer numbers than any
+ character code are refused before they are converted, since
+ that takes time quadratic in their length. -/
+def number (t : String) : Option Nat :=
+ let ds := t.toList
+ if ds.isEmpty || !ds.all Char.isDigit || (ds.dropWhile (· = '0')).length > 7 then none
+ else t.toNat?
+
+/-- The comma-separated numbers in `s`. -/
+def numbers (s : String) : Option (List Nat) :=
+ if s.isEmpty then some [] else (s.splitOn ",").mapM number
+
+def toChars (ns : List Nat) : Option (List Char) :=
+ ns.mapM fun n => if n.isValidChar then some (Char.ofNat n) else none
+
+def showCodes (cs : List Char) : String :=
+ ",".intercalate (cs.map fun c => toString c.toNat)
+
+/-- The answer to one request, or `none` when the request is
+ malformed. -/
+def answer (op : String) (ns : List Nat) : Option String :=
+ match op with
+ | "parse" =>
+ match toChars ns with
+ | none => none
+ | some cs =>
+ match parse cs with
+ | some d => some ("ok:" ++ showCodes (print d))
+ | none => some "none"
+ | _ => none
+
+/-- The answer to one line: an operation, then optionally one space
+ and its numbers. -/
+def request (line : String) : Option String :=
+ match line.splitOn " " with
+ | [op] => answer op []
+ | [op, arg] => numbers arg >>= answer op
+ | _ => none
+
+/-- The line without its line ending: LF, or CR LF. -/
+def chomp (line : String) : String :=
+ let cs := line.toList
+ if cs.getLast? = some '\n' then
+ let cs := cs.dropLast
+ String.ofList (if cs.getLast? = some '\r' then cs.dropLast else cs)
+ else line
+
+def main : IO Unit := do
+ let stdin ← IO.getStdin
+ let stdout ← IO.getStdout
+ repeat
+ let line ← stdin.getLine
+ if line.isEmpty then break
+ let line := chomp line
+ stdout.putStrLn ((request line).getD "error")
diff --git a/Proofs.lean b/Proofs.lean
new file mode 100644
index 0000000..08943dd
--- /dev/null
+++ b/Proofs.lean
@@ -0,0 +1,5 @@
+import Proofs.RoundTrip
+import Proofs.LineEnds
+import Proofs.ParseWF
+import Proofs.Refusals
+import Proofs.SpecProofs
diff --git a/Proofs/LineEnds.lean b/Proofs/LineEnds.lean
new file mode 100644
index 0000000..fbc7cf6
--- /dev/null
+++ b/Proofs/LineEnds.lean
@@ -0,0 +1,148 @@
+/-
+ Line ends: the parser normalizes them before it reads, as XML 1.0
+ section 2.11 requires. The lemmas here say how the normalization
+ `normEol` acts on a text made of two parts, and the two theorems
+ at the end say what that means for `parse`: a carriage return
+ followed by a line feed reads as one line feed, and a carriage
+ return followed by anything else reads as a line feed.
+-/
+
+import Xml
+import Proofs.RoundTrip
+
+namespace Xml.Proofs
+
+open Xml
+
+/-! ## Line ends in a text with a printed head -/
+
+/-- Normalizing a text whose head holds no carriage return leaves
+ the head as it is. -/
+theorem normEol_append_noCR : ∀ (A B : List Char), '\r' ∉ A →
+ normEol (A ++ B) = A ++ normEol B
+ | [], _, _ => rfl
+ | c :: A, B, h => by
+ have hc : c ≠ '\r' := fun e => h (e ▸ List.mem_cons_self)
+ have hA : '\r' ∉ A := fun m => h (List.mem_cons_of_mem _ m)
+ rw [List.cons_append, normEol_cons_ne hc, normEol_append_noCR A B hA,
+ List.cons_append]
+
+/-- The head of a normalized text is the head of the text, or a
+ line feed. -/
+theorem normEol_head (cs : List Char) (c : Char)
+ (h : (normEol cs).head? = some c) : cs.head? = some c ∨ c = '\n' := by
+ match cs with
+ | [] => simp [normEol] at h
+ | '\r' :: '\n' :: rest =>
+ rw [normEol.eq_2] at h
+ exact Or.inr (Option.some.inj h).symm
+ | '\r' :: [] =>
+ rw [normEol.eq_3 _ (by intro r e; cases e)] at h
+ exact Or.inr (Option.some.inj h).symm
+ | '\r' :: d :: rest =>
+ by_cases hd : d = '\n'
+ · subst hd
+ rw [normEol.eq_2] at h
+ exact Or.inr (Option.some.inj h).symm
+ · rw [normEol.eq_3 _ (by intro r e; exact hd (List.cons.inj e).1)] at h
+ exact Or.inr (Option.some.inj h).symm
+ | d :: rest =>
+ by_cases hd : d = '\r'
+ · subst hd
+ cases rest with
+ | nil =>
+ rw [normEol.eq_3 _ (by intro r e; cases e)] at h
+ exact Or.inr (Option.some.inj h).symm
+ | cons e rest' =>
+ by_cases he : e = '\n'
+ · subst he
+ rw [normEol.eq_2] at h
+ exact Or.inr (Option.some.inj h).symm
+ · rw [normEol.eq_3 _ (by intro r e2; exact he (List.cons.inj e2).1)] at h
+ exact Or.inr (Option.some.inj h).symm
+ · rw [normEol_cons_ne hd] at h
+ exact Or.inl h
+
+/-- A text whose head is not a name character keeps that property
+ when its line ends are normalized. -/
+theorem normEol_head_not_name (cs : List Char)
+ (h : ∀ c, cs.head? = some c → ¬ IsNameChar c) :
+ ∀ c, (normEol cs).head? = some c → isNameChar c = false := by
+ intro c hc
+ rcases normEol_head cs c hc with h1 | h1
+ · exact isNameChar_false_of (h c h1)
+ · subst h1
+ decide
+
+/-- Normalizing a text made of two parts is normalizing each part,
+ when the first part does not end with a carriage return (which
+ could pair with a line feed at the head of the second). -/
+theorem normEol_append (A B : List Char) (h : ∀ x, A ≠ x ++ ['\r']) :
+ normEol (A ++ B) = normEol A ++ normEol B := by
+ induction A using normEol.induct with
+ | case1 => simp [normEol.eq_1]
+ | case2 rest ih =>
+ have h' : ∀ x, rest ≠ x ++ ['\r'] := by
+ intro x e
+ exact h ('\r' :: '\n' :: x) (by rw [e]; rfl)
+ rw [List.cons_append, List.cons_append, normEol.eq_2, normEol.eq_2,
+ ih h', List.cons_append]
+ | case3 rest hrest ih =>
+ cases rest with
+ | nil => exact absurd rfl (h [])
+ | cons d ds =>
+ have h' : ∀ x, d :: ds ≠ x ++ ['\r'] := by
+ intro x e
+ exact h ('\r' :: x) (by rw [e]; rfl)
+ have hne : ∀ r, d :: ds ++ B ≠ '\n' :: r := by
+ intro r e
+ rw [List.cons_append] at e
+ exact hrest ds (by rw [(List.cons.inj e).1])
+ rw [List.cons_append, normEol.eq_3 _ hne, normEol.eq_3 _ hrest,
+ ih h', List.cons_append]
+ | case4 c rest _ hc ih =>
+ have h' : ∀ x, rest ≠ x ++ ['\r'] := by
+ intro x e
+ exact h (c :: x) (by rw [e]; rfl)
+ rw [List.cons_append, normEol_cons_ne hc, normEol_cons_ne hc,
+ ih h', List.cons_append]
+
+/-- A carriage return followed by a line feed reads as one line
+ feed, wherever it stands, unless the text before it ends with
+ a carriage return (which would pair with the line feed
+ first). -/
+theorem crlf_reads_as_lf (pre post : List Char)
+ (hpre : pre.getLast? ≠ some '\r') :
+ parse (pre ++ '\r' :: '\n' :: post) = parse (pre ++ '\n' :: post) := by
+ have h : ∀ x, pre ≠ x ++ ['\r'] := by
+ intro x e
+ exact hpre (List.getLast?_eq_some_iff.mpr ⟨x, e⟩)
+ have e1 : normEol (pre ++ '\r' :: '\n' :: post) =
+ normEol (pre ++ '\n' :: post) := by
+ rw [normEol_append _ _ h, normEol_append _ _ h, normEol.eq_2,
+ normEol_cons_ne (by decide)]
+ show parseDocument ((normEol _).length + 1) (normEol _) =
+ parseDocument ((normEol _).length + 1) (normEol _)
+ rw [e1]
+
+/-- A carriage return not followed by a line feed reads as a line
+ feed, wherever it stands, unless the text before it ends with
+ a carriage return. -/
+theorem cr_reads_as_lf (pre post : List Char)
+ (hpre : pre.getLast? ≠ some '\r') (hpost : post.head? ≠ some '\n') :
+ parse (pre ++ '\r' :: post) = parse (pre ++ '\n' :: post) := by
+ have h : ∀ x, pre ≠ x ++ ['\r'] := by
+ intro x e
+ exact hpre (List.getLast?_eq_some_iff.mpr ⟨x, e⟩)
+ have hp : ∀ r, post ≠ '\n' :: r := by
+ intro r e
+ rw [e] at hpost
+ exact hpost rfl
+ have e1 : normEol (pre ++ '\r' :: post) = normEol (pre ++ '\n' :: post) := by
+ rw [normEol_append _ _ h, normEol_append _ _ h,
+ normEol.eq_3 _ (fun r e => hp r e), normEol_cons_ne (by decide)]
+ show parseDocument ((normEol _).length + 1) (normEol _) =
+ parseDocument ((normEol _).length + 1) (normEol _)
+ rw [e1]
+
+end Xml.Proofs
diff --git a/Proofs/ParseWF.lean b/Proofs/ParseWF.lean
new file mode 100644
index 0000000..0752033
--- /dev/null
+++ b/Proofs/ParseWF.lean
@@ -0,0 +1,1105 @@
+/-
+ Every document the parser accepts is well formed: `parse cs = some d`
+ gives `WF d`, for every text `cs`. Together with the round trip,
+ printing an accepted document gives a text that parses back to the
+ same document, which is the plan's main claim as written.
+
+ The proof goes layer by layer, as the parser does. For each reader
+ it shows what the reader gives back (legal characters, a valid
+ name, a comment body with no `--`, and so on), and that the text
+ left over is made of characters of the text it was given. That
+ second fact carries one more property through: the parser reads a
+ text whose line ends were normalized, so it holds no carriage
+ return, and neither does any part of it, so no comment body and no
+ processing instruction data can hold one.
+
+ The one property that is not local is that no two text runs stand
+ next to each other in element content. The content reader takes
+ all character data up to the next markup in one step, so the text
+ after a text run is empty or starts with a less sign that does not
+ open a CDATA section, and the content reader never starts its
+ answer with a text run at such a text.
+-/
+
+import Xml
+import Proofs.RoundTrip
+
+namespace Xml.Proofs
+
+open Xml
+
+/-! ## Small facts -/
+
+theorem sub_refl (cs : List Char) : cs ⊆ cs := fun _ h => h
+
+theorem sub_cons {r cs : List Char} (c : Char) (h : r ⊆ cs) : r ⊆ c :: cs :=
+ fun _ hx => List.mem_cons_of_mem _ (h hx)
+
+theorem sub_trans {a b c : List Char} (h1 : a ⊆ b) (h2 : b ⊆ c) : a ⊆ c :=
+ fun _ hx => h2 (h1 hx)
+
+theorem sub_append_right (a b : List Char) : b ⊆ a ++ b :=
+ fun _ hx => List.mem_append_right _ hx
+
+theorem sub_append_left (a b : List Char) : a ⊆ a ++ b :=
+ fun _ hx => List.mem_append_left _ hx
+
+theorem toNat_ofNat_valid (n : Nat) (h : n.isValidChar) :
+ (Char.ofNat n).toNat = n := by
+ simp only [Char.ofNat, h, dite_true]
+ rfl
+
+/-- A character reference that the reader accepts names a legal
+ character. -/
+theorem charRefChar_legal {n : Nat} {c : Char} (h : charRefChar n = some c) :
+ LegalChar c := by
+ unfold charRefChar at h
+ split at h
+ · rename_i hn
+ cases h
+ have hv : n.isValidChar := by
+ unfold Nat.isValidChar
+ omega
+ unfold LegalChar
+ rw [toNat_ofNat_valid n hv]
+ exact hn
+ · cases h
+
+theorem legal_of_test {c : Char} (h : isLegalChar c = true) : LegalChar c :=
+ isLegalChar_iff.mp h
+
+theorem legal_space : LegalChar ' ' := legal_of_test (by decide)
+
+/-! ## Whitespace and names -/
+
+theorem skipWs_sub : ∀ cs, skipWs cs ⊆ cs
+ | [] => sub_refl _
+ | c :: cs => by
+ simp only [skipWs]
+ split
+ · exact sub_cons c (skipWs_sub cs)
+ · exact sub_refl _
+
+theorem skipWs_head : ∀ (cs : List Char) (c : Char),
+ (skipWs cs).head? = some c → isWs c = false
+ | [], c, h => by simp [skipWs] at h
+ | d :: cs, c, h => by
+ simp only [skipWs] at h
+ split at h
+ · exact skipWs_head cs c h
+ · rename_i hd
+ simp only [List.head?_cons, Option.some.injEq] at h
+ subst h
+ simpa using hd
+
+theorem takeNameChars_spec : ∀ (cs ds r : List Char),
+ takeNameChars cs = (ds, r) → cs = ds ++ r ∧ ∀ d ∈ ds, isNameChar d = true
+ | [], ds, r, h => by
+ simp only [takeNameChars, Prod.mk.injEq] at h
+ obtain ⟨rfl, rfl⟩ := h
+ simp
+ | c :: cs, ds, r, h => by
+ simp only [takeNameChars] at h
+ split at h
+ · rename_i hc
+ rcases hp : takeNameChars cs with ⟨ds', r'⟩
+ rw [hp] at h
+ simp only [Prod.mk.injEq] at h
+ obtain ⟨rfl, rfl⟩ := h
+ obtain ⟨h1, h2⟩ := takeNameChars_spec cs ds' r' hp
+ refine ⟨by simp [h1], ?_⟩
+ intro d hd
+ rcases List.mem_cons.mp hd with e | hd
+ · rw [e]; exact hc
+ · exact h2 d hd
+ · simp only [Prod.mk.injEq] at h
+ obtain ⟨rfl, rfl⟩ := h
+ simp
+
+theorem parseName_spec {cs n r : List Char} (h : parseName cs = some (n, r)) :
+ ValidName n ∧ cs = n ++ r := by
+ match cs, h with
+ | c :: rest, h =>
+ simp only [parseName] at h
+ split at h
+ · rename_i hc
+ rcases hp : takeNameChars rest with ⟨ds, r'⟩
+ rw [hp] at h
+ simp only [Option.some.injEq, Prod.mk.injEq] at h
+ obtain ⟨rfl, rfl⟩ := h
+ obtain ⟨h1, h2⟩ := takeNameChars_spec rest ds r' hp
+ exact ⟨⟨c, ds, rfl, isNameStart_iff.mp hc,
+ fun x hx => isNameChar_iff.mp (h2 x hx)⟩, by simp [h1]⟩
+ · cases h
+
+theorem parseName_sub {cs n r : List Char} (h : parseName cs = some (n, r)) :
+ r ⊆ cs := by
+ obtain ⟨_, e⟩ := parseName_spec h
+ rw [e]
+ exact sub_append_right _ _
+
+/-! ## References -/
+
+theorem takeDigits_spec : ∀ (cs ds r : List Char),
+ takeDigits cs = (ds, r) → cs = ds ++ r
+ | [], ds, r, h => by
+ simp only [takeDigits, Prod.mk.injEq] at h
+ obtain ⟨rfl, rfl⟩ := h
+ rfl
+ | c :: cs, ds, r, h => by
+ simp only [takeDigits] at h
+ split at h
+ · rcases hp : takeDigits cs with ⟨ds', r'⟩
+ rw [hp] at h
+ simp only [Prod.mk.injEq] at h
+ obtain ⟨rfl, rfl⟩ := h
+ simp [takeDigits_spec cs ds' r' hp]
+ · simp only [Prod.mk.injEq] at h
+ obtain ⟨rfl, rfl⟩ := h
+ rfl
+
+theorem takeHexDigits_spec : ∀ (cs ds r : List Char),
+ takeHexDigits cs = (ds, r) → cs = ds ++ r
+ | [], ds, r, h => by
+ simp only [takeHexDigits, Prod.mk.injEq] at h
+ obtain ⟨rfl, rfl⟩ := h
+ rfl
+ | c :: cs, ds, r, h => by
+ simp only [takeHexDigits] at h
+ split at h
+ · rcases hp : takeHexDigits cs with ⟨ds', r'⟩
+ rw [hp] at h
+ simp only [Prod.mk.injEq] at h
+ obtain ⟨rfl, rfl⟩ := h
+ simp [takeHexDigits_spec cs ds' r' hp]
+ · simp only [Prod.mk.injEq] at h
+ obtain ⟨rfl, rfl⟩ := h
+ rfl
+
+/-- A reference the reader accepts stands for a legal character, and
+ the text after it is part of the text it was read from. -/
+theorem parseRef_spec {cs : List Char} {ch : Char} {r : List Char}
+ (h : parseRef cs = some (ch, r)) : LegalChar ch ∧ r ⊆ cs := by
+ unfold parseRef at h
+ split at h
+ · cases h
+ exact ⟨legal_of_test (by decide),
+ sub_cons _ (sub_cons _ (sub_cons _ (sub_refl _)))⟩
+ · cases h
+ exact ⟨legal_of_test (by decide),
+ sub_cons _ (sub_cons _ (sub_cons _ (sub_refl _)))⟩
+ · cases h
+ exact ⟨legal_of_test (by decide),
+ sub_cons _ (sub_cons _ (sub_cons _ (sub_cons _ (sub_refl _))))⟩
+ · cases h
+ exact ⟨legal_of_test (by decide), sub_cons _ (sub_cons _
+ (sub_cons _ (sub_cons _ (sub_cons _ (sub_refl _)))))⟩
+ · cases h
+ exact ⟨legal_of_test (by decide), sub_cons _ (sub_cons _
+ (sub_cons _ (sub_cons _ (sub_cons _ (sub_refl _)))))⟩
+ · rename_i rest
+ split at h
+ · rcases hp : takeHexDigits rest.tail with ⟨ds, r1⟩
+ rw [hp] at h
+ have hsub : r1 ⊆ '#' :: rest := by
+ have e := takeHexDigits_spec _ ds r1 hp
+ intro x hx
+ apply List.mem_cons_of_mem
+ cases rest with
+ | nil => simp at e; rw [e.2] at hx; exact absurd hx (by simp)
+ | cons y ys =>
+ simp only [List.tail_cons] at e
+ rw [e]
+ exact List.mem_cons_of_mem _ (List.mem_append_right _ hx)
+ split at h
+ rename_i ds' r' heq
+ simp only [Prod.mk.injEq] at heq
+ obtain ⟨rfl, rfl⟩ := heq
+ split at h
+ · rename_i r2
+ rw [Option.map_eq_some_iff] at h
+ obtain ⟨c, hc, e⟩ := h
+ simp only [Prod.mk.injEq] at e
+ obtain ⟨rfl, rfl⟩ := e
+ exact ⟨charRefChar_legal hc,
+ sub_trans (sub_cons ';' (sub_refl r2)) hsub⟩
+ · cases h
+ · rcases hp : takeDigits rest with ⟨ds, r1⟩
+ rw [hp] at h
+ have hsub : r1 ⊆ '#' :: rest := by
+ rw [takeDigits_spec _ ds r1 hp]
+ exact sub_cons _ (sub_append_right _ _)
+ split at h
+ rename_i ds' r' heq
+ simp only [Prod.mk.injEq] at heq
+ obtain ⟨rfl, rfl⟩ := heq
+ split at h
+ · rename_i r2
+ rw [Option.map_eq_some_iff] at h
+ obtain ⟨c, hc, e⟩ := h
+ simp only [Prod.mk.injEq] at e
+ obtain ⟨rfl, rfl⟩ := e
+ exact ⟨charRefChar_legal hc,
+ sub_trans (sub_cons ';' (sub_refl r2)) hsub⟩
+ · cases h
+ · cases h
+
+/-! ## Text, CDATA, comments, processing instruction data, values -/
+
+/-- A pattern-matching map that puts a character in front of the
+ first part of the result, undone. -/
+theorem map_cons_some {o : Option (List Char × List Char)} {c : Char}
+ {t r : List Char}
+ (h : (o.map fun (x : List Char × List Char) => (c :: x.1, x.2)) = some (t, r)) :
+ ∃ t', o = some (t', r) ∧ t = c :: t' := by
+ cases o with
+ | none => cases h
+ | some p =>
+ obtain ⟨t', r'⟩ := p
+ simp only [Option.map_some, Option.some.injEq, Prod.mk.injEq] at h
+ obtain ⟨rfl, rfl⟩ := h
+ exact ⟨t', rfl, rfl⟩
+
+theorem legal_cons {c : Char} {t : List Char} (hc : LegalChar c)
+ (ht : ∀ x ∈ t, LegalChar x) : ∀ x ∈ c :: t, LegalChar x := by
+ intro x hx
+ rcases List.mem_cons.mp hx with e | hx
+ · rw [e]; exact hc
+ · exact ht x hx
+
+theorem parseTextRun_spec : ∀ (f : Nat) (cs t r : List Char),
+ parseTextRun f cs = some (t, r) → (∀ c ∈ t, LegalChar c) ∧ r ⊆ cs
+ | 0, cs, t, r, h => by
+ rw [parseTextRun] at h
+ cases h
+ | f + 1, [], t, r, h => by
+ rw [parseTextRun] at h
+ simp only [Option.some.injEq, Prod.mk.injEq] at h
+ obtain ⟨rfl, rfl⟩ := h
+ exact ⟨by simp, sub_refl _⟩
+ | f + 1, c :: rest, t, r, h => by
+ rw [parseTextRun] at h
+ split at h
+ · simp only [Option.some.injEq, Prod.mk.injEq] at h
+ obtain ⟨rfl, rfl⟩ := h
+ exact ⟨by simp, sub_refl _⟩
+ · split at h
+ · split at h
+ · rename_i ch r1 hr
+ rw [Option.map_eq_some_iff] at h
+ obtain ⟨⟨t', r2⟩, h1, e⟩ := h
+ simp only [Prod.mk.injEq] at e
+ obtain ⟨rfl, rfl⟩ := e
+ obtain ⟨hl, hs⟩ := parseTextRun_spec f r1 t' r2 h1
+ obtain ⟨hcl, hrs⟩ := parseRef_spec hr
+ exact ⟨legal_cons hcl hl, sub_trans hs (sub_trans hrs (sub_cons _ (sub_refl _)))⟩
+ · cases h
+ · split at h
+ · rename_i hb
+ split at h
+ · cases h
+ · obtain ⟨t', h1, rfl⟩ := map_cons_some h
+ obtain ⟨hl, hs⟩ := parseTextRun_spec f rest t' r h1
+ rw [hb]
+ exact ⟨legal_cons (legal_of_test (by decide)) hl, sub_cons _ hs⟩
+ · split at h
+ · rename_i hlc
+ obtain ⟨t', h1, rfl⟩ := map_cons_some h
+ obtain ⟨hl, hs⟩ := parseTextRun_spec f rest t' r h1
+ exact ⟨legal_cons (legal_of_test hlc) hl, sub_cons _ hs⟩
+ · cases h
+
+theorem parseCDATABody_spec : ∀ (cs t r : List Char),
+ parseCDATABody cs = some (t, r) → (∀ c ∈ t, LegalChar c) ∧ r ⊆ cs
+ | [], t, r, h => by
+ unfold parseCDATABody at h
+ cases h
+ | c :: rest, t, r, h => by
+ unfold parseCDATABody at h
+ split at h
+ · rename_i heq
+ cases heq
+ · rename_i rest' heq
+ simp only [Option.some.injEq, Prod.mk.injEq] at h
+ obtain ⟨rfl, rfl⟩ := h
+ rw [heq]
+ exact ⟨by simp, sub_cons _ (sub_cons _ (sub_cons _ (sub_refl _)))⟩
+ · rename_i c' rest' _ heq
+ simp only [List.cons.injEq] at heq
+ obtain ⟨rfl, rfl⟩ := heq
+ split at h
+ · rename_i hlc
+ obtain ⟨t', h1, rfl⟩ := map_cons_some h
+ obtain ⟨hl, hs⟩ := parseCDATABody_spec rest t' r h1
+ exact ⟨legal_cons (legal_of_test hlc) hl, sub_cons _ hs⟩
+ · cases h
+
+/-- The text where character data stops: the end, or a less sign
+ that does not open a CDATA section. -/
+def StopCD (r : List Char) : Prop :=
+ r = [] ∨ ∃ r', r = '<' :: r' ∧
+ ∀ x, r' ≠ '!' :: '[' :: 'C' :: 'D' :: 'A' :: 'T' :: 'A' :: '[' :: x
+
+theorem parseCharData_spec : ∀ (f : Nat) (cs t r : List Char),
+ parseCharData f cs = some (t, r) →
+ (∀ c ∈ t, LegalChar c) ∧ r ⊆ cs ∧ StopCD r
+ | 0, cs, t, r, h => by
+ unfold parseCharData at h
+ cases h
+ | f + 1, cs, t, r, h => by
+ unfold parseCharData at h
+ split at h
+ · rename_i heq
+ exact absurd heq (by omega)
+ · simp only [Option.some.injEq, Prod.mk.injEq] at h
+ obtain ⟨rfl, rfl⟩ := h
+ exact ⟨by simp, sub_refl _, Or.inl rfl⟩
+ · rename_i fuel rest heq
+ have hf : f = fuel := Nat.succ.inj heq
+ subst hf
+ split at h
+ · rename_i t1 r1 h1
+ rw [Option.map_eq_some_iff] at h
+ obtain ⟨⟨t2, r2⟩, h2, e⟩ := h
+ simp only [Prod.mk.injEq] at e
+ obtain ⟨rfl, rfl⟩ := e
+ obtain ⟨hl1, hs1⟩ := parseCDATABody_spec rest t1 r1 h1
+ obtain ⟨hl2, hs2, hst⟩ := parseCharData_spec f r1 t2 r2 h2
+ refine ⟨?_, ?_, hst⟩
+ · intro x hx
+ rcases List.mem_append.mp hx with hx | hx
+ · exact hl1 x hx
+ · exact hl2 x hx
+ · exact sub_trans hs2 (sub_trans hs1 (fun _ hx => by simp [hx]))
+ · cases h
+ · rename_i fuel rest hne heq
+ simp only [Option.some.injEq, Prod.mk.injEq] at h
+ obtain ⟨rfl, rfl⟩ := h
+ refine ⟨by simp, sub_refl _, Or.inr ⟨rest, rfl, ?_⟩⟩
+ intro x e
+ exact hne x e
+ · rename_i cs' _ _ fuel heq _ _ _
+ have hf : f = fuel := Nat.succ.inj heq
+ subst hf
+ split at h
+ · rename_i t1 r1 h1
+ rw [Option.map_eq_some_iff] at h
+ obtain ⟨⟨t2, r2⟩, h2, e⟩ := h
+ simp only [Prod.mk.injEq] at e
+ obtain ⟨rfl, rfl⟩ := e
+ obtain ⟨hl1, hs1⟩ := parseTextRun_spec f cs' t1 r1 h1
+ obtain ⟨hl2, hs2, hst⟩ := parseCharData_spec f r1 t2 r2 h2
+ refine ⟨?_, sub_trans hs2 hs1, hst⟩
+ intro x hx
+ rcases List.mem_append.mp hx with hx | hx
+ · exact hl1 x hx
+ · exact hl2 x hx
+ · cases h
+
+theorem sub_cons_cons {a b : List Char} (c : Char) (h : a ⊆ b) :
+ c :: a ⊆ c :: b := by
+ intro x hx
+ rcases List.mem_cons.mp hx with e | hx
+ · rw [e]; exact List.mem_cons_self
+ · exact List.mem_cons_of_mem _ (h hx)
+
+theorem noDashDash_nil : NoDashDash [] := by
+ intro pre suf e
+ have := congrArg List.length e
+ simp at this
+
+theorem notDashEnd_nil : NotDashEnd [] := by
+ intro pre e
+ have := congrArg List.length e
+ simp at this
+
+/-- What the comment body reader gives back: a body with no `--`,
+ not ending with `-`, of legal characters, made of characters of
+ the text, and the text after the closing marks. The last part
+ says how the body starts, which the induction needs: an empty
+ body means the text started with the closing marks. -/
+theorem parseCommentBody_spec : ∀ (cs b r : List Char),
+ parseCommentBody cs = some (b, r) →
+ NoDashDash b ∧ NotDashEnd b ∧ (∀ c ∈ b, LegalChar c) ∧ b ⊆ cs ∧
+ r ⊆ cs ∧ ((b = [] ∧ cs.head? = some '-') ∨ (b ≠ [] ∧ b.head? = cs.head?))
+ | [], b, r, h => by
+ unfold parseCommentBody at h
+ cases h
+ | c :: rest, b, r, h => by
+ unfold parseCommentBody at h
+ split at h
+ · rename_i hc
+ split at h
+ · rename_i r'
+ simp only [Option.some.injEq, Prod.mk.injEq] at h
+ obtain ⟨rfl, rfl⟩ := h
+ refine ⟨noDashDash_nil, notDashEnd_nil, by simp, by simp, ?_,
+ Or.inl ⟨rfl, by simp [hc]⟩⟩
+ exact sub_cons _ (sub_cons _ (sub_cons _ (sub_refl _)))
+ · cases h
+ · rename_i hn1 hn2
+ obtain ⟨b', h1, rfl⟩ := map_cons_some h
+ obtain ⟨hdd, hde, hl, hbs, hrs, hhead⟩ := parseCommentBody_spec rest b' r h1
+ have hb' : b' ≠ [] ∧ b'.head? ≠ some '-' := by
+ rcases hhead with ⟨_, hh⟩ | ⟨hne, hh⟩
+ · exfalso
+ cases rest with
+ | nil => simp at hh
+ | cons x xs =>
+ simp only [List.head?_cons, Option.some.injEq] at hh
+ subst hh
+ exact hn2 xs rfl
+ · refine ⟨hne, ?_⟩
+ rw [hh]
+ intro e
+ cases rest with
+ | nil => simp at e
+ | cons x xs =>
+ simp only [List.head?_cons, Option.some.injEq] at e
+ subst e
+ exact hn2 xs rfl
+ subst hc
+ refine ⟨?_, ?_, legal_cons (legal_of_test (by decide)) hl,
+ sub_cons_cons _ hbs, sub_cons _ hrs, Or.inr ⟨by simp, rfl⟩⟩
+ · intro pre suf e
+ cases pre with
+ | nil =>
+ simp only [List.nil_append, List.cons.injEq, true_and] at e
+ exact hb'.2 (by rw [e]; rfl)
+ | cons y pre' =>
+ simp only [List.cons_append, List.cons.injEq] at e
+ exact hdd pre' suf e.2
+ · intro pre e
+ cases pre with
+ | nil =>
+ simp only [List.nil_append, List.cons.injEq, true_and] at e
+ exact hb'.1 e
+ | cons y pre' =>
+ simp only [List.cons_append, List.cons.injEq] at e
+ exact hde pre' e.2
+ · split at h
+ · rename_i hc hlc
+ obtain ⟨b', h1, rfl⟩ := map_cons_some h
+ obtain ⟨hdd, hde, hl, hbs, hrs, _⟩ := parseCommentBody_spec rest b' r h1
+ refine ⟨?_, ?_, legal_cons (legal_of_test hlc) hl,
+ sub_cons_cons _ hbs, sub_cons _ hrs, Or.inr ⟨by simp, rfl⟩⟩
+ · intro pre suf e
+ cases pre with
+ | nil =>
+ simp only [List.nil_append, List.cons.injEq] at e
+ exact hc e.1
+ | cons y pre' =>
+ simp only [List.cons_append, List.cons.injEq] at e
+ exact hdd pre' suf e.2
+ · intro pre e
+ cases pre with
+ | nil =>
+ simp only [List.nil_append, List.cons.injEq] at e
+ exact hc e.1
+ | cons y pre' =>
+ simp only [List.cons_append, List.cons.injEq] at e
+ exact hde pre' e.2
+ · cases h
+
+theorem noQClose_nil : NoQClose [] := by
+ intro pre suf e
+ have := congrArg List.length e
+ simp at this
+
+/-- What the processing instruction data reader gives back: data
+ with no `?>`, of legal characters, made of characters of the
+ text, and the text after the closing marks; and how the data
+ starts. -/
+theorem parsePIData_spec : ∀ (cs d r : List Char),
+ parsePIData cs = some (d, r) →
+ NoQClose d ∧ (∀ c ∈ d, LegalChar c) ∧ d ⊆ cs ∧ r ⊆ cs ∧
+ ((d = [] ∧ cs.head? = some '?') ∨ (d ≠ [] ∧ d.head? = cs.head?))
+ | [], d, r, h => by
+ unfold parsePIData at h
+ cases h
+ | c :: rest, d, r, h => by
+ unfold parsePIData at h
+ split at h
+ · rename_i hc
+ split at h
+ · rename_i r'
+ simp only [Option.some.injEq, Prod.mk.injEq] at h
+ obtain ⟨rfl, rfl⟩ := h
+ exact ⟨noQClose_nil, by simp, by simp,
+ sub_cons _ (sub_cons _ (sub_refl _)), Or.inl ⟨rfl, by simp [hc]⟩⟩
+ · rename_i hn
+ obtain ⟨d', h1, rfl⟩ := map_cons_some h
+ obtain ⟨hq, hl, hds, hrs, hhead⟩ := parsePIData_spec rest d' r h1
+ subst hc
+ refine ⟨?_, legal_cons (legal_of_test (by decide)) hl,
+ sub_cons_cons _ hds, sub_cons _ hrs, Or.inr ⟨by simp, rfl⟩⟩
+ intro pre suf e
+ cases pre with
+ | nil =>
+ simp only [List.nil_append, List.cons.injEq, true_and] at e
+ subst e
+ rcases hhead with ⟨hne, _⟩ | ⟨_, hh⟩
+ · exact List.cons_ne_nil _ _ hne
+ · cases rest with
+ | nil => simp at hh
+ | cons x xs =>
+ simp only [List.head?_cons, Option.some.injEq] at hh
+ subst hh
+ exact hn xs rfl
+ | cons y pre' =>
+ simp only [List.cons_append, List.cons.injEq] at e
+ exact hq pre' suf e.2
+ · split at h
+ · rename_i hc hlc
+ obtain ⟨d', h1, rfl⟩ := map_cons_some h
+ obtain ⟨hq, hl, hds, hrs, _⟩ := parsePIData_spec rest d' r h1
+ refine ⟨?_, legal_cons (legal_of_test hlc) hl,
+ sub_cons_cons _ hds, sub_cons _ hrs, Or.inr ⟨by simp, rfl⟩⟩
+ intro pre suf e
+ cases pre with
+ | nil =>
+ simp only [List.nil_append, List.cons.injEq] at e
+ exact hc e.1
+ | cons y pre' =>
+ simp only [List.cons_append, List.cons.injEq] at e
+ exact hq pre' suf e.2
+ · cases h
+
+/-- What the attribute value reader gives back: legal characters,
+ and the text after the closing quote. -/
+theorem parseAttrValue_spec (q : Char) : ∀ (f : Nat) (cs v r : List Char),
+ parseAttrValue q f cs = some (v, r) → (∀ c ∈ v, LegalChar c) ∧ r ⊆ cs
+ | 0, cs, v, r, h => by
+ rw [parseAttrValue] at h
+ cases h
+ | f + 1, [], v, r, h => by
+ rw [parseAttrValue] at h
+ cases h
+ | f + 1, c :: rest, v, r, h => by
+ rw [parseAttrValue] at h
+ split at h
+ · simp only [Option.some.injEq, Prod.mk.injEq] at h
+ obtain ⟨rfl, rfl⟩ := h
+ exact ⟨by simp, sub_cons _ (sub_refl _)⟩
+ · split at h
+ · cases h
+ · split at h
+ · split at h
+ · rename_i ch r1 hr
+ rw [Option.map_eq_some_iff] at h
+ obtain ⟨⟨v', r2⟩, h1, e⟩ := h
+ simp only [Prod.mk.injEq] at e
+ obtain ⟨rfl, rfl⟩ := e
+ obtain ⟨hl, hs⟩ := parseAttrValue_spec q f r1 v' r2 h1
+ obtain ⟨hcl, hrs⟩ := parseRef_spec hr
+ exact ⟨legal_cons hcl hl,
+ sub_trans hs (sub_trans hrs (sub_cons _ (sub_refl _)))⟩
+ · cases h
+ · split at h
+ · obtain ⟨v', h1, rfl⟩ := map_cons_some h
+ obtain ⟨hl, hs⟩ := parseAttrValue_spec q f rest v' r h1
+ exact ⟨legal_cons legal_space hl, sub_cons _ hs⟩
+ · split at h
+ · rename_i hlc
+ obtain ⟨v', h1, rfl⟩ := map_cons_some h
+ obtain ⟨hl, hs⟩ := parseAttrValue_spec q f rest v' r h1
+ exact ⟨legal_cons (legal_of_test hlc) hl, sub_cons _ hs⟩
+ · cases h
+
+/-! ## Processing instructions and attribute lists -/
+
+theorem not_IsWs_of_false {c : Char} (h : isWs c = false) : ¬ IsWs c := by
+ intro hw
+ have : isWs c = true := by
+ rcases hw with e | e | e | e <;> rw [e] <;> decide
+ rw [this] at h
+ cases h
+
+/-- What the processing instruction reader gives back: an
+ instruction, well formed when the text holds no carriage
+ return, and the text after it. -/
+theorem parsePI_spec {cs : List Char} {n : Node} {r : List Char}
+ (h : parsePI cs = some (n, r)) :
+ ('\r' ∉ cs → WFNode n) ∧ (∃ t d, n = .pi t d) ∧ r ⊆ cs := by
+ unfold parsePI at h
+ split at h
+ · rename_i target r1 hpn
+ obtain ⟨hvn, hcs⟩ := parseName_spec hpn
+ split at h
+ · cases h
+ · rename_i hres
+ split at h
+ · rename_i r2
+ simp only [Option.some.injEq, Prod.mk.injEq] at h
+ obtain ⟨rfl, rfl⟩ := h
+ refine ⟨fun _ => ?_, ⟨target, [], rfl⟩, ?_⟩
+ · exact WFNode.pi hvn hres noQClose_nil (by simp) (Or.inl rfl) (by simp)
+ · rw [hcs]
+ exact sub_trans (sub_cons _ (sub_cons _ (sub_refl _))) (sub_append_right _ _)
+ · rename_i c tl _
+ split at h
+ · split at h
+ · rename_i d r2 hpd
+ simp only [Option.some.injEq, Prod.mk.injEq] at h
+ obtain ⟨rfl, rfl⟩ := h
+ obtain ⟨hq, hl, hds, hrs, hhead⟩ := parsePIData_spec _ d r2 hpd
+ have hsk : skipWs (c :: tl) ⊆ cs := by
+ rw [hcs]
+ exact sub_trans (skipWs_sub _) (sub_append_right _ _)
+ refine ⟨fun hcr => ?_, ⟨target, d, rfl⟩, sub_trans hrs hsk⟩
+ refine WFNode.pi hvn hres hq hl ?_ (fun m => hcr (hsk (hds m)))
+ rcases hhead with ⟨hd, _⟩ | ⟨_, hh⟩
+ · exact Or.inl hd
+ · right
+ intro x xs e
+ subst e
+ exact not_IsWs_of_false (skipWs_head _ x (by rw [← hh]; rfl))
+ · cases h
+ · cases h
+ · cases h
+ · cases h
+
+theorem AttrsOk_append : ∀ (acc : List (List Char × List Char)) (a v : List Char),
+ AttrsOk acc → ValidName a → a ≠ xmlnsName → (∀ c ∈ v, LegalChar c) →
+ (∀ kv ∈ acc, kv.1 ≠ a) → AttrsOk (acc ++ [(a, v)])
+ | [], a, v, _, h1, h2, h3, _ => by
+ simp only [List.nil_append, AttrsOk]
+ exact ⟨h1, h2, h3, by simp, trivial⟩
+ | kv :: rest, a, v, hok, h1, h2, h3, h4 => by
+ simp only [List.cons_append, AttrsOk] at hok ⊢
+ obtain ⟨g1, g2, g3, g4, g5⟩ := hok
+ refine ⟨g1, g2, g3, ?_, AttrsOk_append rest a v g5 h1 h2 h3
+ (fun k hk => h4 k (List.mem_cons_of_mem _ hk))⟩
+ intro kv2 hkv2
+ rcases List.mem_append.mp hkv2 with hk | hk
+ · exact g4 kv2 hk
+ · simp only [List.mem_singleton] at hk
+ subst hk
+ exact fun e => h4 kv List.mem_cons_self e.symm
+
+/-- What the attribute reader gives back: on top of a list of
+ attributes that meets `AttrsOk`, a list that meets it too, and
+ the text after the tag. -/
+theorem parseAttrs_spec : ∀ (f : Nat) (acc : List (List Char × List Char))
+ (cs : List Char) (attrs : List (List Char × List Char)) (r : List Char)
+ (b : Bool), parseAttrs f acc cs = some (attrs, r, b) → AttrsOk acc →
+ AttrsOk attrs ∧ r ⊆ cs
+ | 0, acc, cs, attrs, r, b, h, _ => by
+ rw [parseAttrs] at h
+ cases h
+ | f + 1, acc, cs, attrs, r, b, h, hok => by
+ rw [parseAttrs] at h
+ have hsk := skipWs_sub cs
+ split at h
+ · rename_i rest heq
+ simp only [Option.some.injEq, Prod.mk.injEq] at h
+ obtain ⟨rfl, rfl, rfl⟩ := h
+ rw [heq] at hsk
+ exact ⟨hok, sub_trans (sub_cons _ (sub_cons _ (sub_refl _))) hsk⟩
+ · rename_i rest heq
+ simp only [Option.some.injEq, Prod.mk.injEq] at h
+ obtain ⟨rfl, rfl, rfl⟩ := h
+ rw [heq] at hsk
+ exact ⟨hok, sub_trans (sub_cons _ (sub_refl _)) hsk⟩
+ · split at h
+ · split at h
+ · rename_i aname r1 hpn
+ obtain ⟨hvn, hcs⟩ := parseName_spec hpn
+ have hr1 : r1 ⊆ cs := by
+ rw [hcs] at hsk
+ exact sub_trans (sub_append_right _ _) hsk
+ split at h
+ · cases h
+ · rename_i hnx
+ split at h
+ · rename_i r2 heq2
+ have hr2 : r2 ⊆ cs := by
+ have := skipWs_sub r1
+ rw [heq2] at this
+ exact sub_trans (sub_trans (sub_cons _ (sub_refl _)) this) hr1
+ split at h
+ · rename_i r3 heq3
+ have hr3 : r3 ⊆ cs := by
+ have := skipWs_sub r2
+ rw [heq3] at this
+ exact sub_trans (sub_trans (sub_cons _ (sub_refl _)) this) hr2
+ split at h
+ · rename_i v r4 hv
+ obtain ⟨hlv, hr4⟩ := parseAttrValue_spec _ f r3 v r4 hv
+ split at h
+ · cases h
+ · rename_i hany
+ have hd : ∀ kv ∈ acc, kv.1 ≠ aname := by
+ intro kv hkv e
+ apply hany
+ exact List.any_eq_true.mpr ⟨kv, hkv, by simp [e]⟩
+ obtain ⟨hA, hR⟩ := parseAttrs_spec f _ r4 attrs r b h
+ (AttrsOk_append acc aname v hok hvn hnx hlv hd)
+ exact ⟨hA, sub_trans hR (sub_trans hr4 hr3)⟩
+ · cases h
+ · rename_i r3 heq3
+ have hr3 : r3 ⊆ cs := by
+ have := skipWs_sub r2
+ rw [heq3] at this
+ exact sub_trans (sub_trans (sub_cons _ (sub_refl _)) this) hr2
+ split at h
+ · rename_i v r4 hv
+ obtain ⟨hlv, hr4⟩ := parseAttrValue_spec _ f r3 v r4 hv
+ split at h
+ · cases h
+ · rename_i hany
+ have hd : ∀ kv ∈ acc, kv.1 ≠ aname := by
+ intro kv hkv e
+ apply hany
+ exact List.any_eq_true.mpr ⟨kv, hkv, by simp [e]⟩
+ obtain ⟨hA, hR⟩ := parseAttrs_spec f _ r4 attrs r b h
+ (AttrsOk_append acc aname v hok hvn hnx hlv hd)
+ exact ⟨hA, sub_trans hR (sub_trans hr4 hr3)⟩
+ · cases h
+ · cases h
+ · cases h
+ · cases h
+ · cases h
+ · cases h
+
+/-! ## Elements and content -/
+
+theorem map_cons_some_node {o : Option (List Node × List Char)} {n : Node}
+ {ns : List Node} {r : List Char}
+ (h : (o.map fun (x : List Node × List Char) => (n :: x.1, x.2)) = some (ns, r)) :
+ ∃ ns', o = some (ns', r) ∧ ns = n :: ns' := by
+ cases o with
+ | none => cases h
+ | some p =>
+ obtain ⟨ns', r'⟩ := p
+ simp only [Option.map_some, Option.some.injEq, Prod.mk.injEq] at h
+ obtain ⟨rfl, rfl⟩ := h
+ exact ⟨ns', rfl, rfl⟩
+
+/-- The element reader only ever gives back an element. -/
+theorem parseElement_is_elem {f : Nat} {cs : List Char} {n : Node}
+ {r : List Char} (h : parseElement f cs = some (n, r)) :
+ ∃ nm a c, n = .elem nm a c := by
+ cases f with
+ | zero =>
+ unfold parseElement at h
+ cases h
+ | succ f =>
+ unfold parseElement at h
+ iterate 8 (all_goals (try (split at h)))
+ all_goals first
+ | (cases h; done)
+ | (simp only [Option.some.injEq, Prod.mk.injEq] at h
+ obtain ⟨rfl, rfl⟩ := h
+ exact ⟨_, _, _, rfl⟩)
+
+/-- At a text where character data stops, the content reader never
+ starts its answer with a text run. This is what keeps two text
+ runs from standing next to each other in the tree. -/
+theorem nodes_head_not_text (f : Nat) (r : List Char) (ns : List Node)
+ (r2 : List Char) (hst : StopCD r) (h : parseNodes f r = some (ns, r2)) :
+ ∀ x, ns.head? ≠ some (.text x) := by
+ cases f with
+ | zero =>
+ unfold parseNodes at h
+ cases h
+ | succ f =>
+ unfold parseNodes at h
+ split at h
+ · simp only [Option.some.injEq, Prod.mk.injEq] at h
+ obtain ⟨rfl, rfl⟩ := h
+ intro x e
+ cases e
+ · simp only [Option.some.injEq, Prod.mk.injEq] at h
+ obtain ⟨rfl, rfl⟩ := h
+ intro x e
+ cases e
+ · split at h
+ · obtain ⟨ns', _, rfl⟩ := map_cons_some_node h
+ intro x e
+ cases e
+ · cases h
+ · exfalso
+ rcases hst with e | ⟨r', e, hn⟩
+ · cases e
+ · simp only [List.cons.injEq, true_and] at e
+ rename_i tail
+ exact hn tail e.symm
+ · split at h
+ · rename_i n r1 hpi
+ obtain ⟨_, ⟨t, d, rfl⟩, _⟩ := parsePI_spec hpi
+ obtain ⟨ns', _, rfl⟩ := map_cons_some_node h
+ intro x e
+ cases e
+ · cases h
+ · split at h
+ · split at h
+ · rename_i n r1 hel
+ obtain ⟨nm, a, c, rfl⟩ := parseElement_is_elem hel
+ obtain ⟨ns', _, rfl⟩ := map_cons_some_node h
+ intro x e
+ cases e
+ · cases h
+ · cases h
+ · cases h
+ · exfalso
+ rename_i h1 _ _ _ _ h6 h7
+ rcases hst with e | ⟨r', e, _⟩
+ · exact h1 e
+ · cases r' with
+ | nil => exact h7 e
+ | cons c tl => exact h6 c tl e
+
+/-- The element and content readers, together, by induction on the
+ fuel: on a text with no carriage return, the element reader gives
+ a well formed element, the content reader a well formed content
+ list, and each leaves a part of the text. -/
+theorem elem_nodes_wf : ∀ f,
+ (∀ cs n r, parseElement f cs = some (n, r) → '\r' ∉ cs →
+ WFNode n ∧ r ⊆ cs) ∧
+ (∀ cs ns r, parseNodes f cs = some (ns, r) → '\r' ∉ cs →
+ WFNodes ns ∧ r ⊆ cs)
+ | 0 => by
+ refine ⟨fun cs n r h _ => ?_, fun cs ns r h _ => ?_⟩
+ · unfold parseElement at h
+ cases h
+ · unfold parseNodes at h
+ cases h
+ | f + 1 => by
+ obtain ⟨ihE, ihN⟩ := elem_nodes_wf f
+ constructor
+ · intro cs n r h hcr
+ unfold parseElement at h
+ split at h
+ · rename_i rest
+ split at h
+ · rename_i name r1 hpn
+ obtain ⟨hvn, hcs⟩ := parseName_spec hpn
+ have hr1 : r1 ⊆ '<' :: rest := by
+ rw [hcs]
+ exact sub_cons _ (sub_append_right _ _)
+ split at h
+ · rename_i attrs r2 hat
+ obtain ⟨hA, hr2⟩ := parseAttrs_spec f [] r1 attrs r2 true hat trivial
+ simp only [Option.some.injEq, Prod.mk.injEq] at h
+ obtain ⟨rfl, rfl⟩ := h
+ exact ⟨WFNode.elem hvn hA WFNodes.nil, sub_trans hr2 hr1⟩
+ · rename_i attrs r2 hat
+ obtain ⟨hA, hr2⟩ := parseAttrs_spec f [] r1 attrs r2 false hat trivial
+ split at h
+ · rename_i content r3 hn
+ obtain ⟨hW, hr3⟩ := ihN r2 content r3 hn
+ (fun m => hcr (hr1 (hr2 m)))
+ split at h
+ · rename_i r4
+ split at h
+ · rename_i ename r5 hpe
+ have hr5 : r5 ⊆ r4 := parseName_sub hpe
+ split at h
+ · rename_i r6 heq6
+ split at h
+ · simp only [Option.some.injEq, Prod.mk.injEq] at h
+ obtain ⟨rfl, rfl⟩ := h
+ refine ⟨WFNode.elem hvn hA hW, ?_⟩
+ have h6 : r6 ⊆ skipWs r5 := by
+ rw [heq6]
+ exact sub_cons _ (sub_refl _)
+ exact sub_trans h6 (sub_trans (skipWs_sub r5)
+ (sub_trans hr5 (sub_trans
+ (sub_cons _ (sub_cons _ (sub_refl _)))
+ (sub_trans hr3 (sub_trans hr2 hr1)))))
+ · cases h
+ · cases h
+ · cases h
+ · cases h
+ · cases h
+ · cases h
+ · cases h
+ · cases h
+ · intro cs ns r h hcr
+ unfold parseNodes at h
+ split at h
+ · simp only [Option.some.injEq, Prod.mk.injEq] at h
+ obtain ⟨rfl, rfl⟩ := h
+ exact ⟨WFNodes.nil, sub_refl _⟩
+ · simp only [Option.some.injEq, Prod.mk.injEq] at h
+ obtain ⟨rfl, rfl⟩ := h
+ exact ⟨WFNodes.nil, sub_refl _⟩
+ · rename_i rest
+ split at h
+ · rename_i body r1 hcb
+ obtain ⟨hdd, hde, hl, hbs, hr1, _⟩ := parseCommentBody_spec rest body r1 hcb
+ have hrest : rest ⊆ '<' :: '!' :: '-' :: '-' :: rest :=
+ sub_cons _ (sub_cons _ (sub_cons _ (sub_cons _ (sub_refl _))))
+ obtain ⟨ns', h1, rfl⟩ := map_cons_some_node h
+ obtain ⟨hW, hr⟩ := ihN r1 ns' r h1 (fun m => hcr (hrest (hr1 m)))
+ refine ⟨WFNodes.cons
+ (WFNode.comment hdd hde hl (fun m => hcr (hrest (hbs m)))) hW ?_,
+ sub_trans hr (sub_trans hr1 hrest)⟩
+ intro ⟨x, e⟩
+ cases e
+ · cases h
+ · split at h
+ · rename_i t r1 hcd
+ obtain ⟨hl, hr1, hst⟩ := parseCharData_spec f _ t r1 hcd
+ split at h
+ · obtain ⟨hW, hr⟩ := ihN r1 ns r h (fun m => hcr (hr1 m))
+ exact ⟨hW, sub_trans hr hr1⟩
+ · rename_i hne
+ obtain ⟨ns', h1, rfl⟩ := map_cons_some_node h
+ obtain ⟨hW, hr⟩ := ihN r1 ns' r h1 (fun m => hcr (hr1 m))
+ exact ⟨WFNodes.cons (WFNode.text hne hl) hW
+ (fun _ => nodes_head_not_text f r1 ns' r hst h1),
+ sub_trans hr hr1⟩
+ · cases h
+ · rename_i rest
+ split at h
+ · rename_i n r1 hpi
+ obtain ⟨hwf, ⟨t, d, rfl⟩, hr1⟩ := parsePI_spec hpi
+ have hrest : rest ⊆ '<' :: '?' :: rest :=
+ sub_cons _ (sub_cons _ (sub_refl _))
+ obtain ⟨ns', h1, rfl⟩ := map_cons_some_node h
+ obtain ⟨hW, hr⟩ := ihN r1 ns' r h1 (fun m => hcr (hrest (hr1 m)))
+ refine ⟨WFNodes.cons (hwf (fun m => hcr (hrest m))) hW ?_,
+ sub_trans hr (sub_trans hr1 hrest)⟩
+ intro ⟨x, e⟩
+ cases e
+ · cases h
+ · split at h
+ · split at h
+ · rename_i n r1 hel
+ obtain ⟨hwf, hr1⟩ := ihE _ n r1 hel hcr
+ obtain ⟨nm, a, c, rfl⟩ := parseElement_is_elem hel
+ obtain ⟨ns', h1, rfl⟩ := map_cons_some_node h
+ obtain ⟨hW, hr⟩ := ihN r1 ns' r h1 (fun m => hcr (hr1 m))
+ refine ⟨WFNodes.cons hwf hW ?_, sub_trans hr hr1⟩
+ intro ⟨x, e⟩
+ cases e
+ · cases h
+ · cases h
+ · cases h
+ · split at h
+ · rename_i t r1 hcd
+ obtain ⟨hl, hr1, hst⟩ := parseCharData_spec f _ t r1 hcd
+ split at h
+ · obtain ⟨hW, hr⟩ := ihN r1 ns r h (fun m => hcr (hr1 m))
+ exact ⟨hW, sub_trans hr hr1⟩
+ · rename_i hne
+ obtain ⟨ns', h1, rfl⟩ := map_cons_some_node h
+ obtain ⟨hW, hr⟩ := ihN r1 ns' r h1 (fun m => hcr (hr1 m))
+ exact ⟨WFNodes.cons (WFNode.text hne hl) hW
+ (fun _ => nodes_head_not_text f r1 ns' r hst h1),
+ sub_trans hr hr1⟩
+ · cases h
+
+/-! ## Prolog, epilog, document -/
+
+theorem parseMisc_spec : ∀ (f : Nat) (cs : List Char) (ns : List Node)
+ (r : List Char), parseMisc f cs = some (ns, r) → '\r' ∉ cs →
+ MiscOk ns ∧ r ⊆ cs
+ | 0, cs, ns, r, h, _ => by
+ unfold parseMisc at h
+ cases h
+ | f + 1, cs, ns, r, h, hcr => by
+ unfold parseMisc at h
+ dsimp only at h
+ have hsk := skipWs_sub cs
+ split at h
+ · rename_i rest heq
+ split at h
+ · rename_i body r1 hcb
+ obtain ⟨hdd, hde, hl, hbs, hr1, _⟩ := parseCommentBody_spec rest body r1 hcb
+ have hrest : rest ⊆ cs := by
+ rw [heq] at hsk
+ exact sub_trans
+ (sub_cons _ (sub_cons _ (sub_cons _ (sub_cons _ (sub_refl _))))) hsk
+ obtain ⟨ns', h1, rfl⟩ := map_cons_some_node h
+ obtain ⟨hM, hr⟩ := parseMisc_spec f r1 ns' r h1
+ (fun m => hcr (hrest (hr1 m)))
+ refine ⟨?_, sub_trans hr (sub_trans hr1 hrest)⟩
+ intro n hn
+ rcases List.mem_cons.mp hn with e | hn
+ · subst e
+ exact ⟨WFNode.comment hdd hde hl (fun m => hcr (hrest (hbs m))),
+ Or.inl ⟨body, rfl⟩⟩
+ · exact hM n hn
+ · cases h
+ · rename_i rest heq
+ split at h
+ · rename_i n r1 hpi
+ obtain ⟨hwf, ⟨t, d, rfl⟩, hr1⟩ := parsePI_spec hpi
+ have hrest : rest ⊆ cs := by
+ rw [heq] at hsk
+ exact sub_trans (sub_cons _ (sub_cons _ (sub_refl _))) hsk
+ obtain ⟨ns', h1, rfl⟩ := map_cons_some_node h
+ obtain ⟨hM, hr⟩ := parseMisc_spec f r1 ns' r h1
+ (fun m => hcr (hrest (hr1 m)))
+ refine ⟨?_, sub_trans hr (sub_trans hr1 hrest)⟩
+ intro n hn
+ rcases List.mem_cons.mp hn with e | hn
+ · subst e
+ exact ⟨hwf (fun m => hcr (hrest m)), Or.inr ⟨t, d, rfl⟩⟩
+ · exact hM n hn
+ · cases h
+ · simp only [Option.some.injEq, Prod.mk.injEq] at h
+ obtain ⟨rfl, rfl⟩ := h
+ exact ⟨fun n hn => absurd hn List.not_mem_nil, hsk⟩
+
+theorem parseDocument_wf {f : Nat} {cs : List Char} {d : Document}
+ (h : parseDocument f cs = some d) (hcr : '\r' ∉ cs) : WF d := by
+ unfold parseDocument at h
+ split at h
+ · rename_i prolog r1 hm
+ obtain ⟨hP, hr1⟩ := parseMisc_spec f cs prolog r1 hm hcr
+ split at h
+ · rename_i root r2 he
+ obtain ⟨hR, hr2⟩ := (elem_nodes_wf f).1 r1 root r2 he (fun m => hcr (hr1 m))
+ obtain ⟨nm, a, c, hshape⟩ := parseElement_is_elem he
+ split at h
+ · rename_i epilog r3 hm2
+ obtain ⟨hE, _⟩ := parseMisc_spec f r2 epilog r3 hm2
+ (fun m => hcr (hr1 (hr2 m)))
+ split at h
+ · simp only [Option.some.injEq] at h
+ subst h
+ exact ⟨hP, hR, ⟨nm, a, c, hshape⟩, hE⟩
+ · cases h
+ · cases h
+ · cases h
+ · cases h
+
+/-- The normalized text holds no carriage return. -/
+theorem normEol_noCR (cs : List Char) : '\r' ∉ normEol cs := by
+ induction cs using normEol.induct with
+ | case1 => simp [normEol.eq_1]
+ | case2 rest ih =>
+ rw [normEol.eq_2]
+ intro m
+ rcases List.mem_cons.mp m with e | m
+ · cases e
+ · exact ih m
+ | case3 rest hrest ih =>
+ rw [normEol.eq_3 _ hrest]
+ intro m
+ rcases List.mem_cons.mp m with e | m
+ · cases e
+ · exact ih m
+ | case4 c rest _ hc ih =>
+ rw [normEol_cons_ne hc]
+ intro m
+ rcases List.mem_cons.mp m with e | m
+ · exact hc e.symm
+ · exact ih m
+
+/-- Every document the parser accepts is well formed. -/
+theorem parse_wf (cs : List Char) (d : Document) (h : parse cs = some d) :
+ WF d :=
+ parseDocument_wf h (normEol_noCR cs)
+
+/-- The plan's main claim: printing a parsed document gives a text
+ that parses to the same document. -/
+theorem print_parse (cs : List Char) (d : Document) (h : parse cs = some d) :
+ parse (print d) = some d :=
+ parse_print d (parse_wf cs d h)
+
+end Xml.Proofs
diff --git a/Proofs/Refusals.lean b/Proofs/Refusals.lean
new file mode 100644
index 0000000..6aaa4da
--- /dev/null
+++ b/Proofs/Refusals.lean
@@ -0,0 +1,1654 @@
+/-
+ Refusal proofs: texts the parser turns away, stated for whole
+ families of inputs rather than single examples.
+
+ Each family is a text whose head is a well formed prolog printed
+ in canonical form and the start of a root element, followed by
+ the forbidden form and then anything at all. The proofs follow
+ the parser through the prolog and the start tag with the round
+ trip lemmas of `Proofs/RoundTrip.lean`, then show the step that
+ turns the forbidden form away.
+-/
+
+import Xml
+import Proofs.RoundTrip
+import Proofs.LineEnds
+import Proofs.ParseWF
+
+namespace Xml.Proofs
+
+open Xml
+
+/-! ## The root element -/
+
+/-- A text made of a printed prolog and then a less sign and a name
+ start character is refused when the element reader refuses the
+ root, with its line ends normalized, at every fuel large
+ enough. -/
+theorem parse_root_none (prolog : List Node) (hpro : MiscOk prolog)
+ (c : Char) (cs0 : List Char) (hc : IsNameStart c)
+ (he : ∀ f, (normEol cs0).length + 3 ≤ f →
+ parseElement f ('<' :: c :: normEol cs0) = none) :
+ parse (printNodes prolog ++ '<' :: c :: cs0) = none := by
+ have hcr : c ≠ '\r' := fun e => not_nameChar_cr (e ▸ IsNameStart.toNameChar hc)
+ have hn : normEol (printNodes prolog ++ '<' :: c :: cs0) =
+ printNodes prolog ++ '<' :: c :: normEol cs0 := by
+ rw [normEol_append_noCR _ _ (noCR_printNodes_misc prolog hpro),
+ normEol_cons_ne (by decide), normEol_cons_ne hcr]
+ show parseDocument ((normEol (printNodes prolog ++ '<' :: c :: cs0)).length + 1)
+ (normEol (printNodes prolog ++ '<' :: c :: cs0)) = none
+ rw [hn]
+ generalize normEol cs0 = cs at he
+ have hstop : ∀ f, 1 ≤ f →
+ parseMisc f ('<' :: c :: cs) = some ([], skipWs ('<' :: c :: cs)) := by
+ intro f hf
+ cases f with
+ | zero => omega
+ | succ f' =>
+ rw [skipWs_cons (show isWs '<' = false by decide)]
+ exact parseMisc_stop hc
+ have hm := parseMisc_print prolog ('<' :: c :: cs) hpro hstop
+ ((printNodes prolog ++ '<' :: c :: cs).length + 1)
+ (by simp only [List.length_append]; omega)
+ rw [skipWs_cons (show isWs '<' = false by decide)] at hm
+ have hroot := he ((printNodes prolog ++ '<' :: c :: cs).length + 1)
+ (by simp only [List.length_append, List.length_cons]; omega)
+ simp only [parseDocument, hm, hroot]
+
+/-- The element reader at a start tag whose name is read whole: it
+ refuses when the attribute reader refuses. -/
+theorem parseElement_attrs_none {g : Nat} {name tail : List Char}
+ (hn : ValidName name)
+ (ht : ∀ c, tail.head? = some c → isNameChar c = false)
+ (ha : parseAttrs g [] tail = none) :
+ parseElement (g + 1) ('<' :: (name ++ tail)) = none := by
+ simp [parseElement, parseName_append hn ht, ha]
+
+/-- The text after a name, when it starts with the printed
+ attributes and then more text, does not start with a name
+ character, as long as the more text does not. -/
+theorem printAttrs_head_not_name (attrs : List (List Char × List Char))
+ (tail : List Char)
+ (ht : ∀ c, tail.head? = some c → isNameChar c = false) :
+ ∀ c, (printAttrs attrs ++ tail).head? = some c → isNameChar c = false := by
+ intro c hc
+ cases attrs with
+ | nil => exact ht c (by simpa [printAttrs] using hc)
+ | cons kv as =>
+ simp only [printAttrs, List.cons_append, List.head?_cons] at hc
+ rw [← Option.some.inj hc]
+ exact isNameChar_false_of not_nameChar_space
+
+/-- A root start tag with printed attributes, at the head of a text
+ after a printed prolog, is refused when the attribute reader
+ refuses whatever follows the printed attributes, with its line
+ ends normalized, at any fuel from one up. -/
+theorem parse_attrs_none (prolog : List Node) (hpro : MiscOk prolog)
+ (name : List Char) (hname : ValidName name)
+ (attrs : List (List Char × List Char)) (hattrs : AttrsOk attrs)
+ (tail0 : List Char)
+ (ht : ∀ c, (printAttrs attrs ++ normEol tail0).head? = some c →
+ isNameChar c = false)
+ (hcont : ∀ f, 1 ≤ f → parseAttrs f attrs (normEol tail0) = none) :
+ parse (printNodes prolog ++ '<' :: (name ++ (printAttrs attrs ++ tail0))) =
+ none := by
+ have hnn := noCR_validName hname
+ obtain ⟨c0, ds, hq, hc0, hds⟩ := hname
+ subst hq
+ rw [List.cons_append]
+ apply parse_root_none prolog hpro c0 _ hc0
+ have hds' : '\r' ∉ ds := fun m => hnn (List.mem_cons_of_mem _ m)
+ rw [normEol_append_noCR _ _ hds',
+ normEol_append_noCR _ _ (noCR_printAttrs attrs hattrs)]
+ generalize normEol tail0 = tail at ht hcont
+ intro f hf
+ cases f with
+ | zero => omega
+ | succ g =>
+ have hlen : ds.length + (printAttrs attrs).length + tail.length + 2 ≤ g := by
+ have h := hf
+ simp only [List.length_append] at h
+ omega
+ have hpa := printAttrs_length_ge attrs
+ have hpv := printAttrs_length_ge_value attrs
+ have ha : parseAttrs g [] (printAttrs attrs ++ tail) = none := by
+ apply parseAttrs_print attrs [] tail g none hattrs
+ (by intro kv _ e; simp at e)
+ · intro kv hkv
+ have h1 := hpv kv hkv
+ omega
+ · omega
+ · intro f' hf'
+ simpa using hcont f' hf'
+ exact parseElement_attrs_none (name := c0 :: ds) ⟨c0, ds, rfl, hc0, hds⟩
+ ht ha
+
+/-! ## The name `xmlns` -/
+
+theorem validName_xmlns : ValidName xmlnsName :=
+ ⟨'x', ['m', 'l', 'n', 's'], rfl, isNameStart_iff.mp (by decide),
+ by intro x hx; simp at hx; rcases hx with rfl | rfl | rfl | rfl <;>
+ exact isNameChar_iff.mp (by decide)⟩
+
+/-- The attribute reader refuses an attribute named `xmlns`, read
+ whole, whatever comes after the name. -/
+theorem parseAttrs_xmlns (f : Nat) (hf : 1 ≤ f)
+ (acc : List (List Char × List Char)) (rest : List Char)
+ (hr : ∀ c, rest.head? = some c → isNameChar c = false) :
+ parseAttrs f acc (' ' :: (xmlnsName ++ rest)) = none := by
+ cases f with
+ | zero => omega
+ | succ g =>
+ have hsk : skipWs (' ' :: (xmlnsName ++ rest)) =
+ 'x' :: 'm' :: 'l' :: 'n' :: 's' :: rest := by
+ simp [skipWs, isWs, xmlnsName]
+ have hpn : parseName ('x' :: 'm' :: 'l' :: 'n' :: 's' :: rest) =
+ some (xmlnsName, rest) :=
+ parseName_append validName_xmlns hr
+ rw [parseAttrs, hsk, hpn]
+ rfl
+
+/-- An attribute named `xmlns` on the root element is refused,
+ after any well formed prolog and any well formed attributes
+ before it, whatever follows the name. -/
+theorem rejects_xmlns (prolog : List Node) (name : List Char)
+ (attrs : List (List Char × List Char)) (rest : List Char)
+ (hpro : MiscOk prolog) (hname : ValidName name)
+ (hattrs : AttrsOk attrs)
+ (hrest : ∀ c, rest.head? = some c → ¬ IsNameChar c) :
+ parse (printNodes prolog ++ '<' :: name ++ printAttrs attrs ++
+ ' ' :: xmlnsName ++ rest) = none := by
+ have e : printNodes prolog ++ '<' :: name ++ printAttrs attrs ++
+ ' ' :: xmlnsName ++ rest =
+ printNodes prolog ++ '<' :: (name ++ (printAttrs attrs ++
+ ' ' :: (xmlnsName ++ rest))) := by
+ simp [List.append_assoc]
+ rw [e]
+ have hn : normEol (' ' :: (xmlnsName ++ rest)) =
+ ' ' :: (xmlnsName ++ normEol rest) := by
+ rw [normEol_cons_ne (by decide),
+ normEol_append_noCR _ _ (by decide)]
+ apply parse_attrs_none prolog hpro name hname attrs hattrs
+ · rw [hn]
+ apply printAttrs_head_not_name
+ intro c hc
+ simp at hc
+ rw [← hc]
+ exact isNameChar_false_of not_nameChar_space
+ · intro f hf
+ rw [hn]
+ exact parseAttrs_xmlns f hf attrs (normEol rest)
+ (normEol_head_not_name rest hrest)
+
+/-! ## Whitespace between attributes -/
+
+/-- The printed attributes, when there is at least one, start with
+ a space, which is not a name character. -/
+theorem printAttrs_head_space (attrs : List (List Char × List Char))
+ (hne : attrs ≠ []) (tail : List Char) :
+ ∀ c, (printAttrs attrs ++ tail).head? = some c →
+ isNameChar c = false := by
+ intro c hc
+ cases attrs with
+ | nil => exact absurd rfl hne
+ | cons kv as =>
+ simp only [printAttrs, List.cons_append, List.head?_cons] at hc
+ rw [← Option.some.inj hc]
+ exact isNameChar_false_of not_nameChar_space
+
+/-- The attribute reader refuses a name that starts right where
+ the text does, with no whitespace before it. -/
+theorem parseAttrs_no_space (f : Nat) (hf : 1 ≤ f)
+ (acc : List (List Char × List Char)) (c : Char) (rest : List Char)
+ (hc : IsNameStart c) :
+ parseAttrs f acc (c :: rest) = none := by
+ cases f with
+ | zero => omega
+ | succ g =>
+ have hw : isWs c = false := isWs_false_of_not (IsNameStart.ne_ws hc)
+ have h1 : c ≠ '/' := IsNameStart.ne_slash hc
+ have h2 : c ≠ '>' := IsNameStart.ne_of_test hc (by decide)
+ simp only [parseAttrs, skipWs, hw, startsWithWs, Bool.and_false,
+ Bool.false_eq_true, ite_false]
+ split
+ · rename_i r e
+ exact absurd (List.cons.inj e).1 h1
+ · rename_i r e
+ exact absurd (List.cons.inj e).1 h2
+ · rfl
+ · rfl
+
+/-- An attribute name that starts right after the closing quote of
+ the attribute before it, with no whitespace between them, is
+ refused, on the root element after any well formed prolog and
+ at least one well formed attribute, printed, whatever follows
+ the first character of the name. -/
+theorem rejects_attribute_without_space (prolog : List Node)
+ (name : List Char) (attrs : List (List Char × List Char))
+ (c : Char) (rest : List Char)
+ (hpro : MiscOk prolog) (hname : ValidName name)
+ (hattrs : AttrsOk attrs) (hne : attrs ≠ []) (hc : IsNameStart c) :
+ parse (printNodes prolog ++ '<' :: name ++ printAttrs attrs ++
+ c :: rest) = none := by
+ have e : printNodes prolog ++ '<' :: name ++ printAttrs attrs ++
+ c :: rest =
+ printNodes prolog ++ '<' :: (name ++ (printAttrs attrs ++
+ c :: rest)) := by
+ simp [List.append_assoc]
+ rw [e]
+ have hcr : c ≠ '\r' := fun e => not_nameChar_cr (e ▸ IsNameStart.toNameChar hc)
+ apply parse_attrs_none prolog hpro name hname attrs hattrs (c :: rest)
+ (printAttrs_head_space attrs hne _)
+ intro f hf
+ rw [normEol_cons_ne hcr]
+ exact parseAttrs_no_space f hf attrs c (normEol rest) hc
+
+/-! ## Toolkit: after the prolog -/
+
+/-- A text made of a printed prolog and then a part where the prolog
+ reader stops and the element reader refuses, with its line ends
+ normalized, is refused. -/
+theorem parse_prolog_none (prolog : List Node) (hpro : MiscOk prolog)
+ (X0 : List Char)
+ (hstop : ∀ f, 1 ≤ f →
+ parseMisc f (normEol X0) = some ([], skipWs (normEol X0)))
+ (he : ∀ f, 1 ≤ f → parseElement f (skipWs (normEol X0)) = none) :
+ parse (printNodes prolog ++ X0) = none := by
+ have hn : normEol (printNodes prolog ++ X0) = printNodes prolog ++ normEol X0 :=
+ normEol_append_noCR _ _ (noCR_printNodes_misc prolog hpro)
+ show parseDocument ((normEol (printNodes prolog ++ X0)).length + 1)
+ (normEol (printNodes prolog ++ X0)) = none
+ rw [hn]
+ generalize normEol X0 = X at hstop he
+ have hm := parseMisc_print prolog X hpro hstop
+ ((printNodes prolog ++ X).length + 1)
+ (by simp only [List.length_append]; omega)
+ have hroot := he ((printNodes prolog ++ X).length + 1) (by omega)
+ simp only [parseDocument, hm, hroot]
+
+/-- The prolog reader stops at a less sign followed by a character
+ that is neither the bang of a comment nor a question mark. -/
+theorem parseMisc_stop_lt {f : Nat} {c : Char} {cs : List Char}
+ (h1 : c ≠ '!') (h2 : c ≠ '?') :
+ parseMisc (f + 1) ('<' :: c :: cs) = some ([], '<' :: c :: cs) := by
+ have h3 : skipWs ('<' :: c :: cs) = '<' :: c :: cs :=
+ skipWs_cons (by decide)
+ simp [parseMisc, h3, h1, h2]
+
+/-- The prolog reader stops at a less sign, a character that is not
+ a question mark, and a character that is not a dash. The two
+ characters are variables here: the nanoda kernel recurses past
+ its stack when it has to compare a character literal with a
+ different literal pattern while checking a matcher, so the
+ literal case below instantiates this one. -/
+theorem parseMisc_stop_two {f : Nat} {b c : Char} {cs : List Char}
+ (hb : b ≠ '?') (hc : c ≠ '-') :
+ parseMisc (f + 1) ('<' :: b :: c :: cs) =
+ some ([], '<' :: b :: c :: cs) := by
+ have h3 : skipWs ('<' :: b :: c :: cs) = '<' :: b :: c :: cs :=
+ skipWs_cons (by decide)
+ simp [parseMisc, h3, hb, hc]
+
+/-- The prolog reader stops at ` rfl
+ | succ f =>
+ unfold parseElement
+ split
+ · rename_i rest heq
+ exact absurd (List.cons.inj heq).1 hc
+ · rfl
+
+/-- The element reader refuses a less sign that a name does not
+ follow. -/
+theorem parseElement_bad_name {f : Nat} {cs : List Char}
+ (h : parseName cs = none) : parseElement f ('<' :: cs) = none := by
+ cases f with
+ | zero => rfl
+ | succ f =>
+ unfold parseElement
+ split
+ · rename_i rest heq
+ cases heq
+ rw [h]
+ · rename_i hne
+ exact absurd rfl (hne cs)
+
+theorem parseName_not_start {c : Char} {cs : List Char}
+ (h : isNameStart c = false) : parseName (c :: cs) = none := by
+ simp [parseName, h]
+
+/-! ## Toolkit: root content -/
+
+/-- The element reader refuses when the start tag is read and the
+ content reader refuses. -/
+theorem parseElement_content_none {g : Nat} {rest name r1 : List Char}
+ {attrs : List (List Char × List Char)} {r2 : List Char}
+ (hpn : parseName rest = some (name, r1))
+ (hat : parseAttrs g [] r1 = some (attrs, r2, false))
+ (hn : parseNodes g r2 = none) : parseElement (g + 1) ('<' :: rest) = none := by
+ unfold parseElement
+ split
+ · rename_i rest' heq
+ cases heq
+ rw [hpn]
+ split
+ · rename_i name' r1' heq2
+ cases heq2
+ rw [hat]
+ split
+ · rename_i heq3
+ cases heq3
+ · rename_i attrs' r2' heq3
+ cases heq3
+ rw [hn]
+ · rename_i heq3
+ cases heq3
+ · rename_i heq2
+ cases heq2
+ · rename_i hne
+ exact absurd rfl (hne rest)
+
+/-- A root start tag with printed attributes and a closing bracket,
+ after a printed prolog, is refused when the content reader
+ refuses what follows, with its line ends normalized, at every
+ fuel from one up. -/
+theorem parse_content_none (prolog : List Node) (hpro : MiscOk prolog)
+ (name : List Char) (hname : ValidName name)
+ (attrs : List (List Char × List Char)) (hattrs : AttrsOk attrs)
+ (tail0 : List Char)
+ (hcont : ∀ f, 1 ≤ f → parseNodes f (normEol tail0) = none) :
+ parse (printNodes prolog ++ '<' :: (name ++ (printAttrs attrs ++ '>' :: tail0))) =
+ none := by
+ have hnn := noCR_validName hname
+ obtain ⟨c0, ds, hq, hc0, hds⟩ := hname
+ subst hq
+ rw [List.cons_append]
+ apply parse_root_none prolog hpro c0 _ hc0
+ have hds' : '\r' ∉ ds := fun m => hnn (List.mem_cons_of_mem _ m)
+ rw [normEol_append_noCR _ _ hds',
+ normEol_append_noCR _ _ (noCR_printAttrs attrs hattrs),
+ normEol_cons_ne (by decide)]
+ generalize normEol tail0 = tail at hcont
+ intro f hf
+ cases f with
+ | zero => omega
+ | succ g =>
+ have hlen : ds.length + (printAttrs attrs).length + tail.length + 2 ≤ g := by
+ have h := hf
+ simp only [List.length_append, List.length_cons] at h
+ omega
+ have hpv := printAttrs_length_ge_value attrs
+ have hat : parseAttrs g [] (printAttrs attrs ++ '>' :: tail) =
+ some (attrs, tail, false) := by
+ have h := parseAttrs_print_open attrs [] tail g hattrs
+ (by intro kv _ e; simp at e)
+ (fun kv hkv => by have := hpv kv hkv; omega)
+ (by have := printAttrs_length_ge attrs; omega)
+ simpa using h
+ have hpn : parseName (c0 :: (ds ++ (printAttrs attrs ++ '>' :: tail))) =
+ some (c0 :: ds, printAttrs attrs ++ '>' :: tail) :=
+ parseName_append (cs := c0 :: ds) ⟨c0, ds, rfl, hc0, hds⟩
+ (printAttrs_head_not_name attrs _ (by
+ intro c hc
+ simp at hc
+ rw [← hc]
+ exact isNameChar_false_of not_nameChar_gt))
+ exact parseElement_content_none hpn hat (hcont g (by omega))
+
+/-! ## Toolkit: readers that fail -/
+
+/-- Normalizing a text made of two parts is normalizing each part,
+ when the second part does not start with a line feed. -/
+theorem normEol_append_of_head (A B : List Char) (hB : B.head? ≠ some '\n') :
+ normEol (A ++ B) = normEol A ++ normEol B := by
+ induction A using normEol.induct with
+ | case1 => simp [normEol.eq_1]
+ | case2 rest ih =>
+ rw [List.cons_append, List.cons_append, normEol.eq_2, normEol.eq_2, ih,
+ List.cons_append]
+ | case3 rest hrest ih =>
+ have hne : ∀ r, rest ++ B ≠ '\n' :: r := by
+ intro r e
+ cases rest with
+ | nil =>
+ simp only [List.nil_append] at e
+ rw [e] at hB
+ exact hB rfl
+ | cons x xs =>
+ simp only [List.cons_append, List.cons.injEq] at e
+ exact hrest xs (by rw [e.1])
+ rw [List.cons_append, normEol.eq_3 _ hne, normEol.eq_3 _ hrest, ih,
+ List.cons_append]
+ | case4 c rest _ hc ih =>
+ rw [List.cons_append, normEol_cons_ne hc, normEol_cons_ne hc, ih,
+ List.cons_append]
+
+/-- A character of a normalized text is a character of the text,
+ or a line feed. -/
+theorem normEol_mem (cs : List Char) (x : Char) (h : x ∈ normEol cs) :
+ x ∈ cs ∨ x = '\n' := by
+ induction cs using normEol.induct with
+ | case1 => simp [normEol.eq_1] at h
+ | case2 rest ih =>
+ rw [normEol.eq_2] at h
+ rcases List.mem_cons.mp h with e | h
+ · exact Or.inr e
+ · rcases ih h with h | h
+ · exact Or.inl (List.mem_cons_of_mem _ (List.mem_cons_of_mem _ h))
+ · exact Or.inr h
+ | case3 rest hrest ih =>
+ rw [normEol.eq_3 _ hrest] at h
+ rcases List.mem_cons.mp h with e | h
+ · exact Or.inr e
+ · rcases ih h with h | h
+ · exact Or.inl (List.mem_cons_of_mem _ h)
+ · exact Or.inr h
+ | case4 c rest _ hc ih =>
+ rw [normEol_cons_ne hc] at h
+ rcases List.mem_cons.mp h with e | h
+ · exact Or.inl (e ▸ List.mem_cons_self)
+ · rcases ih h with h | h
+ · exact Or.inl (List.mem_cons_of_mem _ h)
+ · exact Or.inr h
+
+theorem normEol_not_mem {cs : List Char} {x : Char} (h : x ∉ cs)
+ (hx : x ≠ '\n') : x ∉ normEol cs := by
+ intro m
+ rcases normEol_mem cs x m with m | e
+ · exact h m
+ · exact hx e
+
+/-- A text run reader fails on a part with no less sign and no
+ ampersand followed by a text it fails on, at every fuel. -/
+theorem parseTextRun_fail : ∀ (pre X : List Char), '<' ∉ pre → '&' ∉ pre →
+ (∀ f, parseTextRun f X = none) → ∀ f, parseTextRun f (pre ++ X) = none
+ | [], X, _, _, hX, f => hX f
+ | c :: pre, X, hlt, hamp, hX, f => by
+ have hc1 : c ≠ '<' := fun e => hlt (e ▸ List.mem_cons_self)
+ have hc2 : c ≠ '&' := fun e => hamp (e ▸ List.mem_cons_self)
+ have ih := parseTextRun_fail pre X (fun m => hlt (List.mem_cons_of_mem _ m))
+ (fun m => hamp (List.mem_cons_of_mem _ m)) hX
+ cases f with
+ | zero => rfl
+ | succ f =>
+ rw [List.cons_append, parseTextRun.eq_3, ite_eq_right hc1, ite_eq_right hc2]
+ split
+ · split
+ · rfl
+ · rw [ih f]
+ rfl
+ · split
+ · rw [ih f]
+ rfl
+ · rfl
+
+/-- The character data reader fails on a text that does not start
+ with a less sign and on which the text run reader fails. -/
+theorem parseCharData_fail (cs : List Char) (hne : cs ≠ [])
+ (hlt : cs.head? ≠ some '<') (hT : ∀ f, parseTextRun f cs = none) :
+ ∀ f, parseCharData f cs = none := by
+ intro f
+ cases f with
+ | zero => rfl
+ | succ f =>
+ unfold parseCharData
+ split
+ · rename_i heq
+ exact absurd heq (by omega)
+ · exact absurd rfl hne
+ · exact absurd rfl hlt
+ · exact absurd rfl hlt
+ · rename_i fuel heq _ _ _
+ have hf : f = fuel := Nat.succ.inj heq
+ subst hf
+ rw [hT f]
+
+/-- The content reader fails on a text that does not start with a
+ less sign and on which the character data reader fails. -/
+theorem parseNodes_fail (cs : List Char) (hne : cs ≠ [])
+ (hlt : cs.head? ≠ some '<') (hC : ∀ f, parseCharData f cs = none) :
+ ∀ f, parseNodes f cs = none := by
+ intro f
+ cases f with
+ | zero => rfl
+ | succ f =>
+ unfold parseNodes
+ split
+ · exact absurd rfl hne
+ · exact absurd rfl hlt
+ · exact absurd rfl hlt
+ · exact absurd rfl hlt
+ · exact absurd rfl hlt
+ · exact absurd rfl hlt
+ · exact absurd rfl hlt
+ · rw [hC f]
+
+/-- The head of a text made of a part with no less sign and then a
+ text that does not start with a less sign is not a less sign. -/
+theorem head_not_lt (A X : List Char) (hA : '<' ∉ A) (hX : X.head? ≠ some '<') :
+ (A ++ X).head? ≠ some '<' := by
+ cases A with
+ | nil => simpa using hX
+ | cons a as =>
+ intro e
+ simp only [List.cons_append, List.head?_cons, Option.some.injEq] at e
+ exact hA (e ▸ List.mem_cons_self)
+
+/-- Root content that starts with character data (no less sign, no
+ ampersand), then a text the text run reader fails on, is
+ refused. -/
+theorem content_fail (pre X : List Char) (hlt : '<' ∉ pre) (hamp : '&' ∉ pre)
+ (hX : X ≠ []) (hXlt : X.head? ≠ some '<')
+ (hT : ∀ f, parseTextRun f X = none) :
+ ∀ f, 1 ≤ f → parseNodes f (pre ++ X) = none := by
+ intro f _
+ apply parseNodes_fail
+ · intro e
+ exact hX (List.append_eq_nil_iff.mp e).2
+ · exact head_not_lt pre X hlt hXlt
+ · apply parseCharData_fail
+ · intro e
+ exact hX (List.append_eq_nil_iff.mp e).2
+ · exact head_not_lt pre X hlt hXlt
+ · exact parseTextRun_fail pre X hlt hamp hT
+
+/-! ## Undefined entities and bad character references -/
+
+theorem not_nameChar_semicolon : ¬ IsNameChar ';' :=
+ not_nameChar_of_test (by decide)
+
+theorem noSemi_validName {cs : List Char} (h : ValidName cs) : ';' ∉ cs := by
+ obtain ⟨c, ds, rfl, hc, hds⟩ := h
+ intro m
+ rcases List.mem_cons.mp m with e | e
+ · exact not_nameChar_semicolon (e ▸ IsNameStart.toNameChar hc)
+ · exact not_nameChar_semicolon (hds _ e)
+
+theorem eq_of_append_semicolon : ∀ (w e post rest : List Char), ';' ∉ e →
+ ';' ∉ w → e ++ ';' :: post = w ++ ';' :: rest → e = w
+ | [], e, post, rest, he, _, h => by
+ cases e with
+ | nil => rfl
+ | cons x xs =>
+ simp only [List.cons_append, List.nil_append, List.cons.injEq] at h
+ exact absurd (by rw [← h.1]; exact List.mem_cons_self) he
+ | x :: w, e, post, rest, he, hw, h => by
+ cases e with
+ | nil =>
+ simp only [List.nil_append, List.cons_append, List.cons.injEq] at h
+ exact absurd (by rw [h.1]; exact List.mem_cons_self) hw
+ | cons y e' =>
+ simp only [List.cons_append, List.cons.injEq] at h
+ obtain ⟨rfl, h2⟩ := h
+ rw [eq_of_append_semicolon w e' post rest
+ (fun m => he (List.mem_cons_of_mem _ m))
+ (fun m => hw (List.mem_cons_of_mem _ m)) h2]
+
+/-- The names of the five predefined entities. -/
+abbrev fiveEntities : List (List Char) :=
+ [['l', 't'], ['g', 't'], ['a', 'm', 'p'], ['a', 'p', 'o', 's'],
+ ['q', 'u', 'o', 't']]
+
+/-- The reference reader refuses a reference to any valid name other
+ than the five predefined entities, whatever follows it. -/
+theorem parseRef_undefined (e post : List Char) (he : ValidName e)
+ (hfive : e ∉ fiveEntities) : parseRef (e ++ ';' :: post) = none := by
+ have hsemi : ';' ∉ e := noSemi_validName he
+ unfold parseRef
+ split
+ · rename_i rest heq
+ have := eq_of_append_semicolon ['l', 't'] e post rest hsemi (by decide) heq
+ exact absurd (by rw [this]; decide) hfive
+ · rename_i rest heq
+ have := eq_of_append_semicolon ['g', 't'] e post rest hsemi (by decide) heq
+ exact absurd (by rw [this]; decide) hfive
+ · rename_i rest heq
+ have := eq_of_append_semicolon ['a', 'm', 'p'] e post rest hsemi (by decide) heq
+ exact absurd (by rw [this]; decide) hfive
+ · rename_i rest heq
+ have := eq_of_append_semicolon ['a', 'p', 'o', 's'] e post rest hsemi
+ (by decide) heq
+ exact absurd (by rw [this]; decide) hfive
+ · rename_i rest heq
+ have := eq_of_append_semicolon ['q', 'u', 'o', 't'] e post rest hsemi
+ (by decide) heq
+ exact absurd (by rw [this]; decide) hfive
+ · rename_i rest heq
+ obtain ⟨c, ds, rfl, hc, _⟩ := he
+ simp only [List.cons_append, List.cons.injEq] at heq
+ exact absurd heq.1 (IsNameStart.ne_of_test hc (by decide))
+ · rfl
+
+theorem textRun_undefined (e post : List Char) (he : ValidName e)
+ (hfive : e ∉ fiveEntities) :
+ ∀ f, parseTextRun f ('&' :: (e ++ ';' :: post)) = none := by
+ intro f
+ cases f with
+ | zero => rfl
+ | succ f =>
+ rw [parseTextRun.eq_3, ite_eq_right (by decide), ite_eq_left rfl,
+ parseRef_undefined e post he hfive]
+
+theorem textRun_surrogate (post : List Char) :
+ ∀ f, parseTextRun f
+ ('&' :: '#' :: 'x' :: 'D' :: '8' :: '0' :: '0' :: ';' :: post) = none := by
+ intro f
+ cases f with
+ | zero => rfl
+ | succ f => rfl
+
+theorem textRun_zero (post : List Char) :
+ ∀ f, parseTextRun f ('&' :: '#' :: '0' :: ';' :: post) = none := by
+ intro f
+ cases f with
+ | zero => rfl
+ | succ f => rfl
+
+theorem textRun_cdata_close (post : List Char) :
+ ∀ f, parseTextRun f (']' :: ']' :: '>' :: post) = none := by
+ intro f
+ cases f with
+ | zero => rfl
+ | succ f => rfl
+
+/-- Normalizing a text run that ends in a fixed tail with no carriage
+ return and no leading line feed. -/
+theorem normEol_pre_tail (pre T : List Char) (hT : '\r' ∉ T)
+ (hh : T.head? ≠ some '\n') : normEol (pre ++ T) = normEol pre ++ T := by
+ rw [normEol_append_of_head _ _ hh, normEol_of_noCR _ hT]
+
+/-! ## Attribute values that fail -/
+
+/-- The attribute value reader fails on a part with no double quote
+ and no ampersand followed by a text it fails on. -/
+theorem parseAttrValue_fail : ∀ (pre X : List Char), '"' ∉ pre → '&' ∉ pre →
+ (∀ f, parseAttrValue '"' f X = none) →
+ ∀ f, parseAttrValue '"' f (pre ++ X) = none
+ | [], X, _, _, hX, f => hX f
+ | c :: pre, X, hq, hamp, hX, f => by
+ have hc1 : c ≠ '"' := fun e => hq (e ▸ List.mem_cons_self)
+ have hc2 : c ≠ '&' := fun e => hamp (e ▸ List.mem_cons_self)
+ have ih := parseAttrValue_fail pre X (fun m => hq (List.mem_cons_of_mem _ m))
+ (fun m => hamp (List.mem_cons_of_mem _ m)) hX
+ cases f with
+ | zero => rfl
+ | succ f =>
+ rw [List.cons_append, parseAttrValue.eq_3, ite_eq_right hc1]
+ split
+ · rfl
+ · split
+ · rw [ih f]
+ rfl
+ · split
+ · rw [ih f]
+ rfl
+ · rfl
+
+theorem attrValue_lt (rest : List Char) :
+ ∀ f, parseAttrValue '"' f ('<' :: rest) = none := by
+ intro f
+ cases f with
+ | zero => rfl
+ | succ f => rfl
+
+theorem attrValue_undefined (e post : List Char) (he : ValidName e)
+ (hfive : e ∉ fiveEntities) :
+ ∀ f, parseAttrValue '"' f ('&' :: (e ++ ';' :: post)) = none := by
+ intro f
+ cases f with
+ | zero => rfl
+ | succ f =>
+ rw [parseAttrValue.eq_3, ite_eq_right (by decide), ite_eq_right (by decide),
+ ite_eq_left rfl, parseRef_undefined e post he hfive]
+
+/-! ## One attribute step -/
+
+theorem AttrsOk_mem : ∀ (attrs : List (List Char × List Char))
+ (kv : List Char × List Char), AttrsOk attrs → kv ∈ attrs →
+ ValidName kv.1 ∧ kv.1 ≠ xmlnsName
+ | [], _, _, h => absurd h List.not_mem_nil
+ | kv0 :: rest, kv, hok, h => by
+ rcases List.mem_cons.mp h with e | h
+ · subst e
+ exact ⟨hok.1, hok.2.1⟩
+ · exact AttrsOk_mem rest kv hok.2.2.2.2 h
+
+/-- The attribute reader at a space, a valid name, an equals sign
+ and a double quote: it refuses when the value reader refuses, or
+ when the name is already among the attributes read. -/
+theorem parseAttrs_dq_none (g : Nat) (acc : List (List Char × List Char))
+ (a W : List Char) (ha : ValidName a)
+ (H : ∀ v r4, parseAttrValue '"' g W = some (v, r4) →
+ (acc.any fun kv => decide (kv.1 = a)) = true) :
+ parseAttrs (g + 1) acc (' ' :: (a ++ '=' :: '"' :: W)) = none := by
+ obtain ⟨c0, ds, rfl, hc0, hds⟩ := ha
+ have hw0 : isWs c0 = false := isWs_false_of_not (IsNameStart.ne_ws hc0)
+ have hsk : skipWs (' ' :: ((c0 :: ds) ++ '=' :: '"' :: W)) =
+ c0 :: (ds ++ '=' :: '"' :: W) := by
+ rw [List.cons_append, skipWs.eq_2, ite_eq_left (by decide)]
+ exact skipWs_cons hw0
+ have hpn : parseName (c0 :: (ds ++ '=' :: '"' :: W)) =
+ some (c0 :: ds, '=' :: '"' :: W) :=
+ parseName_append (cs := c0 :: ds) ⟨c0, ds, rfl, hc0, hds⟩ (by
+ intro c hc
+ simp at hc
+ rw [← hc]
+ exact isNameChar_false_of not_nameChar_eq)
+ rw [parseAttrs.eq_2, hsk]
+ split
+ · rename_i rest heq
+ exact absurd (List.cons.inj heq).1 (IsNameStart.ne_slash hc0)
+ · rename_i rest heq
+ exact absurd (List.cons.inj heq).1 (IsNameStart.ne_of_test hc0 (by decide))
+ · rename_i c tl _ _ heq
+ obtain ⟨rfl, rfl⟩ := List.cons.inj heq
+ rw [ite_eq_left (by simp [isNameStart_of hc0, startsWithWs, isWs]), hpn]
+ split
+ · rename_i aname r1 heq2
+ obtain ⟨rfl, rfl⟩ := Prod.mk.inj (Option.some.inj heq2)
+ split
+ · rfl
+ · rw [skipWs_cons (by decide : isWs '=' = false)]
+ split
+ · rename_i r2 heq3
+ obtain ⟨_, rfl⟩ := List.cons.inj heq3
+ rw [skipWs_cons (by decide : isWs '"' = false)]
+ split
+ · rename_i r3 heq4
+ obtain ⟨_, rfl⟩ := List.cons.inj heq4
+ split
+ · rename_i v r4 hv
+ rw [ite_eq_left (H v r4 hv)]
+ · rfl
+ · rename_i r3 heq4
+ exact absurd (List.cons.inj heq4).1 (by decide)
+ · rfl
+ · rfl
+ · rename_i heq2
+ cases heq2
+ · rename_i heq
+ cases heq
+
+/-- The attribute reader at a space, a valid name, an equals sign
+ and a character that is no quote and no whitespace: refused. -/
+theorem parseAttrs_unquoted_none (g : Nat) (acc : List (List Char × List Char))
+ (a : List Char) (c : Char) (W : List Char) (ha : ValidName a)
+ (hc1 : c ≠ '"') (hc2 : c ≠ '\'') (hcw : isWs c = false) :
+ parseAttrs (g + 1) acc (' ' :: (a ++ '=' :: c :: W)) = none := by
+ obtain ⟨c0, ds, rfl, hc0, hds⟩ := ha
+ have hw0 : isWs c0 = false := isWs_false_of_not (IsNameStart.ne_ws hc0)
+ have hsk : skipWs (' ' :: ((c0 :: ds) ++ '=' :: c :: W)) =
+ c0 :: (ds ++ '=' :: c :: W) := by
+ rw [List.cons_append, skipWs.eq_2, ite_eq_left (by decide)]
+ exact skipWs_cons hw0
+ have hpn : parseName (c0 :: (ds ++ '=' :: c :: W)) =
+ some (c0 :: ds, '=' :: c :: W) :=
+ parseName_append (cs := c0 :: ds) ⟨c0, ds, rfl, hc0, hds⟩ (by
+ intro x hx
+ simp at hx
+ rw [← hx]
+ exact isNameChar_false_of not_nameChar_eq)
+ rw [parseAttrs.eq_2, hsk]
+ split
+ · rename_i rest heq
+ exact absurd (List.cons.inj heq).1 (IsNameStart.ne_slash hc0)
+ · rename_i rest heq
+ exact absurd (List.cons.inj heq).1 (IsNameStart.ne_of_test hc0 (by decide))
+ · rename_i c' tl _ _ heq
+ obtain ⟨rfl, rfl⟩ := List.cons.inj heq
+ rw [ite_eq_left (by simp [isNameStart_of hc0, startsWithWs, isWs]), hpn]
+ split
+ · rename_i aname r1 heq2
+ obtain ⟨rfl, rfl⟩ := Prod.mk.inj (Option.some.inj heq2)
+ split
+ · rfl
+ · rw [skipWs_cons (by decide : isWs '=' = false)]
+ split
+ · rename_i r2 heq3
+ obtain ⟨_, rfl⟩ := List.cons.inj heq3
+ rw [skipWs_cons hcw]
+ split
+ · rename_i r3 heq4
+ exact absurd (List.cons.inj heq4).1 hc1
+ · rename_i r3 heq4
+ exact absurd (List.cons.inj heq4).1 hc2
+ · rfl
+ · rfl
+ · rename_i heq2
+ cases heq2
+ · rename_i heq
+ cases heq
+
+/-- The attribute reader refuses a text that starts with a
+ character that is no whitespace, no slash and no closing
+ bracket: an attribute needs whitespace before it. -/
+theorem parseAttrs_head_none (f : Nat) (hf : 1 ≤ f)
+ (acc : List (List Char × List Char)) (c : Char) (rest : List Char)
+ (hw : isWs c = false) (h1 : c ≠ '/') (h2 : c ≠ '>') :
+ parseAttrs f acc (c :: rest) = none := by
+ cases f with
+ | zero => omega
+ | succ g =>
+ rw [parseAttrs.eq_2, skipWs_cons hw]
+ split
+ · rename_i r heq
+ exact absurd (List.cons.inj heq).1 h1
+ · rename_i r heq
+ exact absurd (List.cons.inj heq).1 h2
+ · rename_i c' tl _ _ heq
+ obtain ⟨rfl, rfl⟩ := List.cons.inj heq
+ rw [ite_eq_right (by simp [startsWithWs, hw])]
+ · rename_i heq
+ cases heq
+
+/-! ## Element-level helpers -/
+
+/-- The element reader refuses when the end tag names another
+ element. -/
+theorem parseElement_mismatch {g : Nat} {rest name r1 : List Char}
+ {attrs : List (List Char × List Char)} {r2 : List Char}
+ {content : List Node} {other R : List Char}
+ (hpn : parseName rest = some (name, r1))
+ (hat : parseAttrs g [] r1 = some (attrs, r2, false))
+ (hn : parseNodes g r2 = some (content, '<' :: '/' :: (other ++ '>' :: R)))
+ (hon : parseName (other ++ '>' :: R) = some (other, '>' :: R))
+ (hne : other ≠ name) :
+ parseElement (g + 1) ('<' :: rest) = none := by
+ unfold parseElement
+ split
+ · rename_i rest' heq
+ cases heq
+ rw [hpn]
+ split
+ · rename_i name' r1' heq2
+ obtain ⟨rfl, rfl⟩ := Prod.mk.inj (Option.some.inj heq2)
+ rw [hat]
+ split
+ · rename_i heq3
+ cases heq3
+ · rename_i attrs' r2' heq3
+ cases heq3
+ rw [hn]
+ split
+ · rename_i content' r3 heq4
+ obtain ⟨rfl, rfl⟩ := Prod.mk.inj (Option.some.inj heq4)
+ split
+ · rename_i r4 heq5
+ obtain ⟨-, heq5⟩ := List.cons.inj heq5
+ obtain ⟨-, rfl⟩ := List.cons.inj heq5
+ rw [hon]
+ split
+ · rename_i ename r5 heq6
+ obtain ⟨rfl, rfl⟩ := Prod.mk.inj (Option.some.inj heq6)
+ rw [skipWs_cons (by decide : isWs '>' = false)]
+ split
+ · rw [ite_eq_right hne]
+ · rfl
+ · rename_i heq6
+ cases heq6
+ · rename_i hne'
+ exact absurd rfl (hne' _)
+ · rename_i heq4
+ cases heq4
+ · rename_i heq3
+ cases heq3
+ · rename_i heq2
+ cases heq2
+ · rename_i hne'
+ exact absurd rfl (hne' rest)
+
+/-- The element reader refuses when the content reader stops at the
+ end of the text, with no end tag. -/
+theorem parseElement_unclosed {g : Nat} {rest name r1 : List Char}
+ {attrs : List (List Char × List Char)} {r2 : List Char}
+ (hpn : parseName rest = some (name, r1))
+ (hat : parseAttrs g [] r1 = some (attrs, r2, false))
+ (hn : ∀ ns r3, parseNodes g r2 = some (ns, r3) → r3 = []) :
+ parseElement (g + 1) ('<' :: rest) = none := by
+ unfold parseElement
+ split
+ · rename_i rest' heq
+ cases heq
+ rw [hpn]
+ split
+ · rename_i name' r1' heq2
+ obtain ⟨rfl, rfl⟩ := Prod.mk.inj (Option.some.inj heq2)
+ rw [hat]
+ split
+ · rename_i heq3
+ cases heq3
+ · rename_i attrs' r2' heq3
+ cases heq3
+ split
+ · rename_i content r3 hc
+ have := hn content r3 hc
+ subst this
+ rfl
+ · rfl
+ · rename_i heq3
+ cases heq3
+ · rename_i heq2
+ cases heq2
+ · rename_i hne'
+ exact absurd rfl (hne' rest)
+
+/-- A comment body reader refuses a body a well formed comment may
+ hold followed by two dashes and anything but a closing bracket. -/
+theorem parseCommentBody_dashdash : ∀ (body Z : List Char),
+ NoDashDash body → NotDashEnd body → (∀ c ∈ body, LegalChar c) →
+ Z.head? ≠ some '>' → parseCommentBody (body ++ '-' :: '-' :: Z) = none
+ | [], Z, _, _, _, hZ => by
+ rw [List.nil_append]
+ unfold parseCommentBody
+ rw [ite_eq_left rfl]
+ split
+ · rename_i r heq
+ obtain ⟨-, rfl⟩ := List.cons.inj heq
+ exact absurd rfl hZ
+ · rfl
+ · rename_i h1 h2
+ exact absurd rfl (h2 Z)
+ | c :: body, Z, hdd, hde, hlegal, hZ => by
+ have hlegal' : ∀ x ∈ body, LegalChar x :=
+ fun x hx => hlegal x (List.mem_cons_of_mem c hx)
+ have hdd' : NoDashDash body := by
+ intro pre suf h
+ exact hdd (c :: pre) suf (by simp [h])
+ have hde' : NotDashEnd body := by
+ intro pre h
+ exact hde (c :: pre) (by simp [h])
+ have ih := parseCommentBody_dashdash body Z hdd' hde' hlegal' hZ
+ by_cases hc : c = '-'
+ · subst hc
+ cases body with
+ | nil => exact absurd rfl (hde [])
+ | cons d ds =>
+ have hd : d ≠ '-' := by
+ intro e
+ subst e
+ exact hdd [] ds (by simp)
+ rw [List.cons_append, List.cons_append, parseCommentBody_dash_cons hd,
+ ← List.cons_append, ih]
+ rfl
+ · rw [List.cons_append]
+ unfold parseCommentBody
+ rw [ite_eq_right hc, ite_eq_left (isLegalChar_of (hlegal c List.mem_cons_self)),
+ ih]
+ rfl
+
+/-- The content reader at ``. The body must not
+ contain `--` and must not end with `-`. Both are XML's rules,
+ and they keep the closing marks unambiguous.
+- The body is carried as the characters between the marks.
+- A comment may appear in the prolog, in content, or in the
+ epilog, and is a node in place.
+
+## Processing instructions
+
+- A processing instruction is `` at once,
+ or whitespace and data up to `?>`.
+- The target `xml` in any letter case is reserved and rejects
+ (see Documents).
+- The data is carried as text. It may be empty. It must not
+ contain `?>`, and in the model it never starts with
+ whitespace: the whitespace after the target is a separator,
+ not part of the data.
+
+## Document type declarations and other ``. An element read from `` has no content
+ and also prints as ``: same tree, different spelling.
+- In text: `&` as `&`, `<` as `<`, `>` as `>` (always
+ escaping `>` keeps `]]>` from ever forming in printed text),
+ and carriage return as `
`. Every other character prints
+ as itself.
+- In attribute values: `&` as `&`, `<` as `<`, `"` as
+ `"`, and tab, line feed, and carriage return as
+ ` `, `
`, `
`. A literal tab in a printed value
+ would read back as a space under normalization, so character
+ references are how those characters are kept.
+- A processing instruction with no data prints as ``;
+ with data, as `` with one space.
+- A document prints as its prolog, its root, and its epilog,
+ with nothing between them.
+
+## Well formed trees
+
+The round trip is claimed for trees that satisfy a well
+formedness predicate (`WF` in `Xml/Value.lean`):
+
+- every name matches the name rule above;
+- attribute names are unique per element and none is `xmlns`,
+ and attribute values hold only legal XML characters;
+- text nodes are not empty, hold only legal XML characters,
+ and two text nodes never stand next to each other (the
+ parser merges them, so an unmerged tree could not come
+ back);
+- comment bodies hold only legal characters, contain no `--`,
+ do not end with `-`, and hold no carriage return;
+- processing instruction targets are valid names and not the
+ reserved word, their data holds only legal characters, never
+ contains `?>`, never starts with whitespace, and holds no
+ carriage return;
+- the root is an element, and the prolog and epilog hold only
+ comments and processing instructions.
+
+## Properties and their theorems
+
+Each property a reader can check in the page (`README.md`)
+names its theorem, with the same words there. The theorems
+are stated in `Spec.lean` and proved in
+`Proofs/SpecProofs.lean`, under the same names.
+
+The first five hold for every text or every well formed
+document. Each refusal after them is about a family of
+texts, and its row says which. Most families share a
+shape: a well formed prolog (`MiscOk`), printed in canonical
+form; then, for most, the root's start tag with any valid
+name and any attributes that meet `AttrsOk`, also printed;
+then the form the rule turns away; then anything. No
+refusal statement covers its rule in every position: the
+rows say where. The tests in `tests/` check the other
+positions.
+
+| Property | Theorem |
+|----------|---------|
+| Parsing the printed form of a well formed document gives the document back | `Spec.parse_print` |
+| Every text the parser accepts gives a well formed document (`Xml.WF`, described below): among other things, no name anywhere in the tree holds a colon or starts with a digit, no attribute name stands twice on one element and none is `xmlns`, every character is a legal XML character, and comment bodies hold no `--` | `Spec.parse_wf` |
+| Printing a document the parser accepted gives a text that parses back to the same document (the plan's main claim, as written) | `Spec.print_parse` |
+| A carriage return followed by a line feed reads exactly as one line feed, anywhere in a text, unless the text before it ends with a carriage return (XML 1.0 section 2.11) | `Spec.crlf_reads_as_lf` |
+| A carriage return not followed by a line feed reads exactly as a line feed, anywhere in a text, unless the text before it ends with a carriage return | `Spec.cr_reads_as_lf` |
+| After a printed prolog, `` is refused, whatever follows | `Spec.rejects_cdata_close_in_text` |
+| For a comment that is the root's first content: `"
+ if kind == "pi":
+ if n[2] == "":
+ return ""
+ return ""
+ _, name, attrs, content = n
+ parts = ["<" + name]
+ for k, v in attrs:
+ parts.append(" " + k + '="' + escape_attr(v) + '"')
+ if not content:
+ parts.append("/>")
+ else:
+ parts.append(">")
+ for c in content:
+ parts.append(print_node(c))
+ parts.append("")
+ return "".join(parts)
+
+
+def print_doc(doc):
+ prolog, root, epilog = doc
+ return ("".join(print_node(n) for n in prolog)
+ + print_node(root)
+ + "".join(print_node(n) for n in epilog))
+
+
+# ----------------------------------------------------------------
+# ElementTree reading, converted to the model. Only the root
+# element is compared: ElementTree drops the prolog and epilog.
+
+
+def et_to_model(elem):
+ if elem.tag is ET.Comment:
+ return ("comment", elem.text or "")
+ if elem.tag is ET.ProcessingInstruction:
+ text = elem.text or ""
+ if " " in text:
+ target, data = text.split(" ", 1)
+ else:
+ target, data = text, ""
+ return ("pi", target, data)
+ content = []
+ if elem.text:
+ content.append(("text", elem.text))
+ for child in elem:
+ content.append(et_to_model(child))
+ if child.tail:
+ content.append(("text", child.tail))
+ return ("elem", elem.tag, list(elem.attrib.items()), content)
+
+
+def et_parse(text):
+ """ElementTree's reading of a text. ET.XMLParser always runs
+ expat with namespace processing on; there is no subset setting.
+ Documents outside the subset are therefore told apart by the
+ named rejection list, not by the oracle."""
+ builder = ET.TreeBuilder(insert_comments=True, insert_pis=True)
+ return ET.fromstring(text, parser=ET.XMLParser(target=builder))
+
+
+# ----------------------------------------------------------------
+# The tool driver: one request per line, character codes.
+
+
+def codes(text):
+ return ",".join(str(ord(c)) for c in text)
+
+
+def request(text):
+ return "parse " + codes(text)
+
+
+def run_tool(lines, failures, part, timeout=TIMEOUT):
+ """Send the request lines to the tool and return one answer per
+ line. The run fails closed: a non-zero exit status, or a number
+ of answers that differs from the number of requests, is recorded
+ as a failure of `part`, and missing answers read as ``,
+ which no check accepts."""
+ try:
+ proc = subprocess.run(
+ [str(EXE)], input=("\n".join(lines) + "\n").encode(),
+ capture_output=True, timeout=timeout)
+ except subprocess.TimeoutExpired:
+ failures.append("%s: tool did not answer within %d seconds"
+ % (part, timeout))
+ return [""] * len(lines)
+ answers = proc.stdout.decode(errors="replace").splitlines()
+ if proc.returncode != 0:
+ failures.append("%s: tool exited with status %d"
+ % (part, proc.returncode))
+ if len(answers) != len(lines):
+ failures.append("%s: tool gave %d answers for %d requests"
+ % (part, len(answers), len(lines)))
+ answers = (answers + [""] * len(lines))[:len(lines)]
+ return answers
+
+
+def run_requests(texts, failures, part):
+ lines = [request(t) for t in texts]
+ answers = []
+ for i in range(0, len(lines), CHUNK):
+ answers.extend(run_tool(lines[i:i + CHUNK], failures, part))
+ return answers
+
+
+# ----------------------------------------------------------------
+# Fixed cases: (input, expected canonical print).
+
+FIXED = [
+ ("", ""),
+ ("", ""),
+ ("x", "x"),
+ ("deep", "deep"),
+ ("t", 't'),
+ ("x", 'x'),
+ ("x", "x"),
+ # literal tab and newline in a value read as a space; a
+ # character reference to a tab stays a tab
+ ("", ''),
+ ("", ''),
+ ("",
+ ''),
+ ("<>&'"", "<>&'\""),
+ ("ABc", "ABc"),
+ ("éé", "éé"),
+ ("1 > 0 and 2 < 3", "1 > 0 and 2 < 3"),
+ (" & z]]>", "x <y> & z"),
+ ("t1t3", "t1t2t3"),
+ ("]]>", "]>"),
+ ("", ""),
+ ("", ""),
+ ("", ""),
+ ("", ""),
+ ("", ""),
+ ("", ""),
+ ("", ""),
+ ("xyzw", "xyzw"),
+ ("", ''),
+ ("x", "x"),
+ ("
", "
"),
+ ("", ''),
+ ("text with ] and ]] but no close",
+ "text with ] and ]] but no close"),
+ ("<_x.y-z_9/>", "<_x.y-z_9/>"),
+ ("", ''),
+ ("\n spaced\n", "\n spaced\n"),
+ ("", ""),
+ ("t",
+ "t"),
+ # only the exact name xmlns declares a namespace; these are
+ # ordinary attribute names, and an element may be named xmlns
+ ("",
+ ''),
+ ("", ""),
+ # any whitespace separates attributes: space, tab, line feed
+ ("", ''),
+ # line ends: CR LF and a lone CR read as LF (XML 1.0 2.11),
+ # everywhere; only a character reference keeps a CR
+ ("x\r\ny", "x\ny"),
+ ("x\ry", "x\ny"),
+ ("x\r\r\ny\n\rz\r", "x\n\ny\n\nz\n"),
+ ("
\r\n
", "
\n
"),
+ # a reference keeps a CR in any spelling and position, not only
+ # in a canonical print (no theorem covers these; see README)
+ ("", ''),
+ ("
y
",
+ '
y
'),
+ ("", "x\ny\nz"),
+ ("", ""),
+ ("", ""),
+ ("", ''),
+ ("\r\n\r", ''),
+ ("x", "x"),
+]
+
+# Named rejections: (rule, input). ElementTree's verdict is
+# recorded for each; where it accepts, the case is an out of
+# subset disagreement, not a failure.
+REJECTIONS = [
+ ("document type declaration", ""),
+ ("document type declaration with internal subset",
+ "]>&e;"),
+ ("entity declaration door (any other "),
+ ("undefined entity", " "),
+ ("undefined entity in an attribute", ""),
+ ("mismatched tags", ""),
+ ("mismatched tags, nested", ""),
+ ("unclosed element", ""),
+ ("unclosed element after content", ""),
+ ("a second root element", ""),
+ ("text before the root", "x"),
+ ("text after the root", "x"),
+ ("duplicate attribute", ""),
+ ("raw < in an attribute value", ""),
+ ("]]> in text", "x]]>y"),
+ ("-- inside a comment", ""),
+ ("comment ending in a dash", ""),
+ ("surrogate character reference", "�"),
+ ("zero character reference", "�"),
+ ("character reference past the last character",
+ "�"),
+ ("colon in a name", ""),
+ ("colon in an attribute name", ""),
+ ("default namespace declaration", ""),
+ ("empty default namespace declaration", ""),
+ ("default namespace declaration, single quotes",
+ ""),
+ ("default namespace declaration after another attribute",
+ ""),
+ ("default namespace declaration on a child element",
+ ""),
+ ("prefixed namespace declaration", ""),
+ ("name starting with a digit", "<1a/>"),
+ ("attribute name starting with a digit", ""),
+ ("unquoted attribute value", ""),
+ ("no whitespace between attributes", ""),
+ ("no whitespace between attributes, single quotes",
+ ""),
+ ("no whitespace between attributes (W3C o-p40fail1)",
+ ""),
+ ("no whitespace between attributes in an empty element tag",
+ ""),
+ ("no whitespace between attributes on a child element",
+ ""),
+ ("missing equals", ""),
+ ("CDATA section in the prolog", ""),
+ ("CDATA section in the epilog", ""),
+ ("the XML declaration form", ""),
+ ("the XML declaration, upper case target",
+ ""),
+ ("bare ampersand in text", "a & b"),
+ ("reference without a semicolon", "&"),
+ ("empty reference", "&;"),
+ ("hex reference with no digits", "&#x;"),
+ ("control character reference", " "),
+ ("raw control character in text", "x\x0by"),
+ ("unterminated comment", ""),
+ ("CDATA section after a processing instruction", ""),
+ ("xml declaration target in mixed case", ""),
+ ("text after a prolog", "x"),
+ ("second element after a document with an epilog", ""),
+ ("digit element name after a prolog", "<9/>"),
+ ("colon in a name after a prolog", ""),
+ ("mismatched end tag after content and attributes",
+ "x"),
+ ("unclosed element with attributes", ""),
+ ("undefined entity after text", "text &e; more"),
+ ("undefined entity in an attribute after text", ""),
+ ("surrogate reference after text", "x�"),
+ ("zero reference after text", "x�"),
+ ("]]> after text", "text]]>"),
+ ("-- in a comment after a well formed body",
+ ""),
+ ("duplicate attribute after another", ""),
+ ("raw < after text in an attribute value", ""),
+ ("unquoted value after another attribute", ""),
+ # undefined entities where no theorem covers them (the refusal
+ # statements reach the root's first text run and the root's
+ # attribute values only; see SPEC.md and README)
+ ("undefined entity in a nested element", "&e;"),
+ ("undefined entity after a child element", "&e;"),
+ ("undefined entity after a comment", "&e;"),
+ ("undefined entity after a CDATA section",
+ "&e;"),
+ ("undefined entity after a predefined one", "&&e;"),
+ ("undefined entity in a nested element's attribute",
+ ""),
+ ("undefined entity in an attribute after a reference",
+ ""),
+ # inputs review 1 (finding 7) listed as missing
+ ("hex reference with an upper case X", "A"),
+ ("reference to a non-character", ""),
+ ("document type declaration in content", ""),
+ ("xml declaration after the root", ""),
+ ("empty document", ""),
+ ("whitespace only document", " \n "),
+ ("comment only document", ""),
+]
+
+MALFORMED = [
+ "parse x",
+ "parse 60,,62",
+ "parse 60, 62",
+ "parse -1",
+ "parse 1114112",
+ "parse 55296",
+ "print 60",
+ "PARSE 60",
+ "parse 60 62",
+ "",
+]
+
+# parse with no codes is a plain empty input, not malformed:
+# it must answer none (the empty text is not a document).
+
+
+# ----------------------------------------------------------------
+# The generator: random trees in the subset, spelled with random
+# choices that do not change the tree. Each generated case is
+# (spelling, model document). The model is built alongside the
+# spelling, token by token, so that the two always agree: a
+# literal tab spelled in an attribute value is a space in the
+# model, a character reference to a tab is a tab in the model.
+
+NAME_START = "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ_"
+NAME_CHARS = NAME_START + "0123456789.-"
+TEXT_PLAIN = ("abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ"
+ "0123456789 .,;:!?()[]{}+-*/=_%$#@~^|"
+ "\u00e9\u4e2d\ufffd\U0001f600")
+COMMENT_WORDS = ["note", "a", "draft-1", "x", "see above", "ok",
+ "todo: fix", "caf\u00e9", "na\u00efve", "123"]
+
+
+def gen_name(rng):
+ n = rng.randint(1, 7)
+ return rng.choice(NAME_START) + "".join(
+ rng.choice(NAME_CHARS) for _ in range(n - 1))
+
+
+def spell_line_end(rng, next_char):
+ """One spelling of a line feed of the tree: a line feed, a
+ carriage return and line feed pair, or a lone carriage return.
+ A lone carriage return is chosen only when the next character
+ of the spelling cannot be a literal line feed, which would
+ pair with it."""
+ if next_char == "\n":
+ return rng.choice(["\n", "\r\n"])
+ return rng.choice(["\n", "\r\n", "\r"])
+
+
+def spell_text_char(rng, c, emitted, next_char=None):
+ """One spelling of a text character, and it is never a raw
+ less sign, a raw ampersand, or a raw greater sign right after
+ two right brackets."""
+ if c == "\n":
+ return spell_line_end(rng, next_char)
+ if c == "&":
+ return "&"
+ if c == "<":
+ return "<"
+ if c == ">":
+ if rng.random() < 0.5:
+ return ">"
+ return ">"
+ if c == "\r":
+ return rng.choice(["
", "
"])
+ if c == "\t":
+ return c
+ r = rng.random()
+ if r < 0.06:
+ return "&#%d;" % ord(c)
+ if r < 0.10:
+ return "&#x%X;" % ord(c)
+ return c
+
+
+def gen_text_run(rng):
+ """A text run: returns (spelling, model text). The spelling
+ may split the run into plain pieces and CDATA sections; the
+ model is one merged run."""
+ n = rng.randint(1, 14)
+ chars = []
+ for _ in range(n):
+ r = rng.random()
+ if r < 0.72:
+ chars.append(rng.choice(TEXT_PLAIN))
+ elif r < 0.78:
+ chars.append("&")
+ elif r < 0.84:
+ chars.append("<")
+ elif r < 0.90:
+ chars.append(">")
+ elif r < 0.92:
+ chars.append("\r")
+ elif r < 0.95:
+ chars.append("\n")
+ elif r < 0.97:
+ chars.append("'")
+ else:
+ chars.append('"')
+ model = "".join(chars)
+ # Spell it: choose up to two cut points where a CDATA section
+ # starts or ends. Inside CDATA everything is literal except
+ # the model holds no ]]> (it cannot: > after ]] is possible,
+ # so keep CDATA pieces free of a ] ] > run by construction:
+ # a CDATA piece may not end with ]] when the next model char
+ # is >, and may not contain ]]> at all. The generator simply
+ # avoids CDATA around ] characters.
+ pieces = []
+ i = 0
+ emitted = ""
+ while i < len(chars):
+ if (rng.random() < 0.3 and chars[i] != "]"
+ and (i + 1 >= len(chars) or chars[i + 1] != "]")):
+ j = i
+ buf = []
+ while (j < len(chars) and chars[j] not in "<&"
+ and chars[j] != "\r"
+ and not (chars[j] == "]" and j + 1 < len(chars)
+ and chars[j + 1] == "]")):
+ buf.append(chars[j])
+ j += 1
+ if buf and buf[-1] != "]":
+ pieces.append("")
+ emitted += "".join(buf)
+ i = j
+ continue
+ nxt = chars[i + 1] if i + 1 < len(chars) else None
+ sp = spell_text_char(rng, chars[i], emitted, nxt)
+ pieces.append(sp)
+ emitted += chars[i]
+ i += 1
+ return "".join(pieces), model
+
+
+def gen_attr_value(rng):
+ """Returns (spelling inside the quotes, model value, quote).
+ The quote is chosen so a literal quote of the other kind may
+ appear."""
+ quote = rng.choice(['"', "'"])
+ toks = []
+ model = []
+ for _ in range(rng.randint(0, 10)):
+ r = rng.random()
+ if r < 0.55:
+ c = rng.choice(TEXT_PLAIN)
+ toks.append(c)
+ model.append(c)
+ elif r < 0.62:
+ toks.append("\t") # literal tab: model space
+ model.append(" ")
+ elif r < 0.68:
+ # literal newline: a model space, unless it completes
+ # a literal CRLF pair, which reads as one space
+ if not (toks and toks[-1] == "\r"):
+ model.append(" ")
+ toks.append("\n")
+ elif r < 0.72:
+ toks.append("\r") # literal CR: model space
+ model.append(" ")
+ elif r < 0.78:
+ toks.append(" ")
+ model.append("\t")
+ elif r < 0.82:
+ toks.append("
")
+ model.append("\n")
+ elif r < 0.86:
+ toks.append("
")
+ model.append("\r")
+ elif r < 0.90:
+ toks.append("<")
+ model.append("<")
+ elif r < 0.93:
+ toks.append("&")
+ model.append("&")
+ elif r < 0.96:
+ other = "'" if quote == '"' else '"'
+ toks.append(other)
+ model.append(other)
+ else:
+ toks.append(""" if quote == '"' else "'")
+ model.append(quote)
+ return "".join(toks), "".join(model), quote
+
+
+def join_words(rng, words):
+ """Words joined by a space or, now and then, by a line end:
+ returns (spelling, model). Words never start with a line
+ feed, so a lone carriage return is safe between them."""
+ sp = []
+ model = []
+ for i, w in enumerate(words):
+ if i > 0:
+ if rng.random() < 0.2:
+ sp.append(spell_line_end(rng, None))
+ model.append("\n")
+ else:
+ sp.append(" ")
+ model.append(" ")
+ sp.append(w)
+ model.append(w)
+ return "".join(sp), "".join(model)
+
+
+def gen_comment(rng):
+ words = [rng.choice(COMMENT_WORDS)
+ for _ in range(rng.randint(0, 4))]
+ sp, model = join_words(rng, words)
+ body_sp = " " + sp + " " if words else ""
+ body = " " + model + " " if words else ""
+ if rng.random() < 0.3:
+ body_sp = body_sp + "- x "
+ body = body + "- x "
+ return "", ("comment", body)
+
+
+def gen_pi(rng):
+ target = gen_name(rng)
+ while target.lower() == "xml":
+ target = gen_name(rng)
+ if rng.random() < 0.35:
+ return "", ("pi", target, "")
+ words = [rng.choice(COMMENT_WORDS)
+ for _ in range(rng.randint(1, 3))]
+ sp, data = join_words(rng, words)
+ return ("",
+ ("pi", target, data))
+
+
+# Whitespace inside tags and at the top level. A separator before an
+# attribute is never empty: XML 1.0 [40] and [44] require one.
+SEPS = [" ", " ", " ", " ", "\t", "\n", " \n\t", "\r\n", "\r"]
+OPT_WS = ["", "", "", " ", "\n", "\t ", "\r\n", "\r"]
+
+
+def gen_sep(rng):
+ return rng.choice(SEPS)
+
+
+def gen_opt_ws(rng):
+ return rng.choice(OPT_WS)
+
+
+def gen_element(rng, depth):
+ name = gen_name(rng)
+ used = set()
+ attrs = []
+ attr_spell = []
+ for _ in range(rng.randint(0, 3)):
+ an = gen_name(rng)
+ if an in used or an == "xmlns":
+ continue
+ used.add(an)
+ sp, val, q = gen_attr_value(rng)
+ attrs.append((an, val))
+ eq = rng.choice(["=", " = ", "= ", " ="])
+ attr_spell.append(gen_sep(rng) + an + eq + q + sp + q)
+ content = []
+ content_spell = []
+ if depth < 4:
+ for _ in range(rng.randint(0, 4)):
+ r = rng.random()
+ if r < 0.38:
+ sub_sp, sub = gen_element(rng, depth + 1)
+ content.append(sub)
+ content_spell.append(sub_sp)
+ elif r < 0.52:
+ sp, node = gen_comment(rng)
+ content.append(node)
+ content_spell.append(sp)
+ elif r < 0.62:
+ sp, node = gen_pi(rng)
+ content.append(node)
+ content_spell.append(sp)
+ else:
+ sp, model = gen_text_run(rng)
+ if content and content[-1][0] == "text":
+ content[-1] = ("text", content[-1][1] + model)
+ else:
+ content.append(("text", model))
+ content_spell.append(sp)
+ model = ("elem", name, attrs, content)
+ stag = "<" + name + "".join(attr_spell) + gen_opt_ws(rng)
+ etag = ""
+ if not content:
+ if rng.random() < 0.5:
+ return stag + "/>", model
+ return stag + ">" + etag, model
+ return stag + ">" + "".join(content_spell) + etag, model
+
+
+def gen_document(rng):
+ prolog = []
+ prolog_spell = []
+ for _ in range(rng.randint(0, 2)):
+ if rng.random() < 0.5:
+ sp, node = gen_comment(rng)
+ else:
+ sp, node = gen_pi(rng)
+ prolog.append(node)
+ prolog_spell.append(sp)
+ root_sp, root = gen_element(rng, 0)
+ epilog = []
+ epilog_spell = []
+ for _ in range(rng.randint(0, 2)):
+ if rng.random() < 0.5:
+ sp, node = gen_comment(rng)
+ else:
+ sp, node = gen_pi(rng)
+ epilog.append(node)
+ epilog_spell.append(sp)
+ text = (gen_opt_ws(rng)
+ + "".join(sp + gen_opt_ws(rng) for sp in prolog_spell)
+ + root_sp
+ + "".join(gen_opt_ws(rng) + sp for sp in epilog_spell)
+ + gen_opt_ws(rng))
+ return text, (prolog, root, epilog)
+
+
+# ----------------------------------------------------------------
+
+
+def lake_env():
+ env = dict(os.environ)
+ env["PATH"] = str(Path.home() / ".elan" / "bin") + ":" + env["PATH"]
+ return env
+
+
+def build_exe():
+ """Always run `lake build`: it does nothing when the build is
+ current, and rebuilds the tool after a source change, so a stale
+ binary is never tested."""
+ out = subprocess.run(["lake", "build"], cwd=ROOT, capture_output=True,
+ text=True, timeout=BUILD_TIMEOUT, env=lake_env())
+ if out.returncode != 0:
+ sys.stderr.write(out.stdout + out.stderr)
+ raise SystemExit("lake build failed with status %d"
+ % out.returncode)
+
+
+def lean_version():
+ out = subprocess.run(["lean", "--version"], capture_output=True,
+ text=True, timeout=60, cwd=ROOT, env=lake_env())
+ return out.stdout.strip() or "unknown"
+
+
+def main():
+ ap = argparse.ArgumentParser()
+ ap.add_argument("--seed", type=int, default=SEED_DEFAULT)
+ ap.add_argument("--count", type=int, default=COUNT_DEFAULT)
+ args = ap.parse_args()
+ rng = random.Random(args.seed)
+
+ build_exe()
+ failures = []
+
+ # Part 1: fixed cases.
+ inputs = [t for t, _ in FIXED]
+ answers = run_requests(inputs, failures, "fixed cases")
+ fixed_answers = answers
+ fixed_ok = 0
+ for (text, expected), ans in zip(FIXED, answers):
+ want = "ok:" + codes(expected)
+ if ans == want:
+ fixed_ok += 1
+ else:
+ failures.append("fixed case %r: got %r, want %r"
+ % (text, ans, want))
+
+ # Part 2: generated differential. Every failing document is
+ # counted; only the printed list is cut short.
+ gen_inputs = []
+ gen_docs = []
+ for _ in range(args.count):
+ text, doc = gen_document(rng)
+ gen_inputs.append(text)
+ gen_docs.append(doc)
+ answers = run_requests(gen_inputs, failures, "generated")
+ gen_answers = answers
+ gen_ok = 0
+ et_ok = 0
+ for text, doc, ans in zip(gen_inputs, gen_docs, answers):
+ want = "ok:" + codes(print_doc(doc))
+ why = []
+ if ans != want:
+ why.append("tool answered %r" % (ans[:120],))
+ try:
+ et_root = et_parse(text)
+ if et_to_model(et_root) != doc[1]:
+ why.append("ElementTree read a different tree")
+ else:
+ et_ok += 1
+ et_canon = et_parse(print_doc(doc))
+ if et_to_model(et_canon) != doc[1]:
+ why.append("ElementTree read a different tree "
+ "from the canonical print")
+ except ET.ParseError as e:
+ why.append("ElementTree rejected it: %s" % e)
+ if why:
+ failures.append("generated %r: %s" % (text, "; ".join(why)))
+ else:
+ gen_ok += 1
+
+ # Part 3: print then parse. Every canonical print the tool gave
+ # in parts 1 and 2 is sent back; the answer must be the same
+ # print (Spec.print_parse, run on the compiled tool).
+ printed = []
+ for ans in fixed_answers + gen_answers:
+ if ans.startswith("ok:") and len(ans) > 3:
+ printed.append("".join(chr(int(x)) for x in ans[3:].split(",")))
+ re_answers = run_requests(printed, failures, "print then parse")
+ reprint_ok = 0
+ for text, ans in zip(printed, re_answers):
+ if ans == "ok:" + codes(text):
+ reprint_ok += 1
+ else:
+ failures.append("print then parse %r: got %r" % (text, ans[:120]))
+
+ # Part 4: named rejections. Also record ElementTree's verdict
+ # on each: accepted means an out of subset disagreement.
+ rej_inputs = [t for _, t in REJECTIONS]
+ answers = run_requests(rej_inputs, failures, "named rejections")
+ rej_ok = 0
+ oos = []
+ for (rule, text), ans in zip(REJECTIONS, answers):
+ if ans == "none":
+ rej_ok += 1
+ else:
+ failures.append("rejection %s: tool answered %r for %r"
+ % (rule, ans, text))
+ try:
+ et_parse(text)
+ oos.append(rule)
+ except ET.ParseError:
+ pass
+
+ # Malformed requests.
+ bad_answers = run_tool(MALFORMED, failures, "malformed requests")
+ bad_ok = 0
+ for line, ans in zip(MALFORMED, bad_answers):
+ if ans == "error":
+ bad_ok += 1
+ else:
+ failures.append("malformed %r: got %r, want error"
+ % (line, ans))
+ empty_ans = run_tool(["parse", "parse "], failures, "bare parse")
+ if empty_ans != ["none", "none"]:
+ failures.append("bare 'parse' answered %r, want two nones"
+ % (empty_ans,))
+
+ lines = []
+ lines.append("# Test results")
+ lines.append("")
+ lines.append("Written by `tests/run_tests.py`. Rerun it to "
+ "check these numbers.")
+ lines.append("")
+ total = (len(FIXED) + len(gen_inputs) + len(printed)
+ + len(REJECTIONS) + len(MALFORMED) + 2)
+ lines.append("- Oracle: Python %s `xml.etree.ElementTree`, "
+ "%s (`ET.XMLParser`, which turns namespace "
+ "processing on, with a `TreeBuilder` that keeps "
+ "comments and processing instructions)"
+ % (sys.version.split()[0], pyexpat.EXPAT_VERSION))
+ lines.append("- Lean tool: %s" % lean_version())
+ lines.append("- Seed: %d" % args.seed)
+ lines.append("- Inputs: %d" % total)
+ lines.append(" - every request sent to the tool: the fixed cases, "
+ "the generated documents, the canonical prints sent "
+ "back, the named rejections, the malformed requests, "
+ "and two bare parse requests")
+ lines.append("- Fixed cases passed: %d of %d"
+ % (fixed_ok, len(FIXED)))
+ lines.append("- Generated in-subset documents: %d" % len(gen_inputs))
+ lines.append("- Generated documents where the tool's canonical "
+ "print matches the tree and ElementTree agrees on "
+ "the tree: %d" % gen_ok)
+ lines.append("- ElementTree tree agreements on generated "
+ "documents: %d" % et_ok)
+ lines.append("- Canonical prints that parse back to the same "
+ "print: %d of %d" % (reprint_ok, len(printed)))
+ lines.append("- Named rejections rejected by the tool: %d of %d"
+ % (rej_ok, len(REJECTIONS)))
+ lines.append("- Out of subset disagreements (ElementTree "
+ "accepts, this slice rejects, by design): %d"
+ % len(oos))
+ for rule in oos:
+ lines.append(" - %s" % rule)
+ lines.append("- Malformed requests answered error: %d of %d"
+ % (bad_ok, len(MALFORMED)))
+ lines.append("- Bare parse requests answered none: %s"
+ % ("yes" if empty_ans == ["none", "none"] else "no"))
+ lines.append("- Failures: %d" % len(failures))
+ for f in failures[:40]:
+ lines.append(" - %s" % f)
+ if len(failures) > 40:
+ lines.append(" - (%d more not shown)" % (len(failures) - 40))
+ RESULTS.write_text("\n".join(lines) + "\n")
+ print("\n".join(lines))
+ return 1 if failures else 0
+
+
+if __name__ == "__main__":
+ sys.exit(main())