Skip to content

Commit 094750c

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
proof(xml-7-44): discharge Xml744.Element proof debts (#81)
## Summary Discharges four proof / totality debts in `Xml744.Element` that blocked the toolkit build past step 4/6. 1. **`tagName`** — same `decEq` baseline-rot as `attrName`. Replaced with `with (isValidName s) proof prf` so `MkTagName`'s auto-implicit discharges in the matched branch. 2. **`unsafeTagName`** — same never-compiled `cast (MkTagName s)` placeholder as `unsafeAttrName`. Bumped to `(s : String) -> {auto prf : isValidName s = True} -> TagName`; `Refl` discharges for literals. 3. **`render`** — failed totality via `concatMap render children` (higher-order call opaques the size-change recursion). Refactored into a `mutual` block with a first-order `renderList : List XmlNode -> String` helper: ```idris mutual render (Element tag attrs children) = "<" ++ ... ++ renderList children ++ ... renderList [] = "" renderList (n :: ns) = render n ++ renderList ns ``` Each `renderList (n :: ns)` peels one element; `render Element` calls `renderList children` on a structural sub-term. 4. **`renderPretty.go`** — same shape (`unlines (map go children)`), same fix: `mutual` block with `renderPrettyList : Nat -> List XmlNode -> String`. The child-separator semantics (trailing newline after each rendered child) match the previous `unlines` behaviour exactly. ## Knock-on signature changes (smart-constructor proof propagation) To keep the API total without proof escapes, the validity proofs need to flow through the smart constructors: - `el`, `emptyEl` → `(tag : String) -> {auto prf : isValidName tag = True} -> ...` - `wEl`, `wEmptyEl` → `(tag : String) -> {auto prf : isValidName (\"w:\" ++ tag) = True} -> ...` All existing call sites pass literals (`wEl \"r\"`, `wEl \"t\"`, `wEl \"p\"`, `wEmptyEl \"commentReference\"`, etc.), so every proof discharges by `Refl` at elaboration time. The probe (verified locally) confirms `isValidName (\"w:\" ++ \"id\") = True` reduces. ## Verification ``` $ idris2 -p contrib Xml744/Element.idr 1/4: Building Xml744.Escape 2/4: Building Xml744.Text 3/4: Building Xml744.Attribute 4/4: Building Xml744.Element Xml744.Element> :total Xml744.Element.tagName --> is total Xml744.Element> :total Xml744.Element.unsafeTagName --> is total Xml744.Element> :total Xml744.Element.render --> is total Xml744.Element> :total Xml744.Element.renderList --> is total Xml744.Element> :total Xml744.Element.renderPretty --> is total Xml744.Element> :total Xml744.Element.renderPrettyList--> is total Xml744.Element> :total Xml744.Element.el --> is total Xml744.Element> :total Xml744.Element.emptyEl --> is total Xml744.Element> :total Xml744.Element.wEl --> is total Xml744.Element> :total Xml744.Element.wEmptyEl --> is total Xml744.Element> :total Xml744.Element.wText --> is total Xml744.Element> :total Xml744.Element.wPara --> is total Xml744.Element> :total Xml744.Element.wCommentRef --> is total Xml744.Element> :total Xml744.Element.wCommentStart --> is total Xml744.Element> :total Xml744.Element.wCommentEnd --> is total ``` `grep -E 'assert_total|assert_smaller|believe_me|%unsafe|PROOF_TODO|idris_crash|partial ' src/Xml744/Element.idr` → no matches. Toolkit build advances 4/6 → 5/6. `Xml744.Document` errors ("Expected end of input" at `prefix : String` field — `prefix` likely reserved on Idris2 0.8.0) are pre-existing baseline-rot, not caused by this branch. Stacks on top of #80 (`proof-debt/xml744-attribute-discharge`) which stacks on #79 (`proof-debt/xml744-escape-totality`). Base is `main` per the orphan-trap guidance; cumulative diff until earlier PRs land, then rebases to a single-file change. ## Test plan - [ ] CI green - [ ] `idris2 --build idris2-ecosystem/xml-toolkit/xml-7-44.ipkg` builds modules 1–4 cleanly (verified locally) 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 34dc2de commit 094750c

1 file changed

Lines changed: 88 additions & 50 deletions

File tree

‎idris2-ecosystem/xml-toolkit/src/Xml744/Element.idr‎

Lines changed: 88 additions & 50 deletions
Original file line numberDiff line numberDiff line change
@@ -15,17 +15,25 @@ public export
1515
data TagName : Type where
1616
MkTagName : (n : String) -> {auto prf : isValidName n = True} -> TagName
1717

18+
||| Try to create a tag name (returns Nothing if invalid).
19+
|||
20+
||| Mirrors `Xml744.Attribute.attrName` — uses `with proof` so the matched
21+
||| branch binds `prf : isValidName s = True` for `MkTagName`'s auto-implicit.
22+
||| Replaces the previous `decEq (isValidName s) True` form (`decEq` for
23+
||| `Bool` is not in scope on Idris2 0.8.0 with the current imports).
1824
export
19-
tagName : String -> Maybe TagName
20-
tagName s = case decEq (isValidName s) True of
21-
Yes prf => Just (MkTagName s)
22-
No _ => Nothing
23-
25+
tagName : (s : String) -> Maybe TagName
26+
tagName s with (isValidName s) proof prf
27+
tagName s | True = Just (MkTagName s)
28+
tagName s | False = Nothing
29+
30+
||| Tag-name constructor for strings whose validity Idris2 can verify at
31+
||| elaboration time. Replaces the previous `cast (MkTagName s)` placeholder,
32+
||| which never compiled. The auto-implicit `isValidName s = True` discharges
33+
||| by `Refl` for any literal.
2434
export
25-
unsafeTagName : String -> TagName
26-
-- PROOF_TODO: Replace cast with actual proof
27-
-- PROOF_TODO: Replace cast with actual proof
28-
unsafeTagName s = cast (MkTagName s)
35+
unsafeTagName : (s : String) -> {auto prf : isValidName s = True} -> TagName
36+
unsafeTagName s = MkTagName s
2937

3038
||| Get the string representation of a tag name
3139
export
@@ -49,61 +57,91 @@ export
4957
txt : String -> XmlNode
5058
txt s = TextNode (text s)
5159

52-
||| Create an element
60+
||| Create an element. Tag validity is discharged at elaboration time for
61+
||| any literal (or compile-time-reducible) tag string.
5362
export
54-
el : String -> List XmlAttr -> List XmlNode -> XmlNode
63+
el : (tag : String) -> {auto prf : isValidName tag = True} ->
64+
List XmlAttr -> List XmlNode -> XmlNode
5565
el tag attrs children = Element (unsafeTagName tag) attrs children
5666

57-
||| Create a self-closing element
67+
||| Create a self-closing element.
5868
export
59-
emptyEl : String -> List XmlAttr -> XmlNode
69+
emptyEl : (tag : String) -> {auto prf : isValidName tag = True} ->
70+
List XmlAttr -> XmlNode
6071
emptyEl tag attrs = EmptyElement (unsafeTagName tag) attrs
6172

62-
||| Render XML node to string
63-
export
64-
render : XmlNode -> String
65-
render (TextNode t) = toXml t
66-
render (Element tag attrs children) =
67-
let attrsStr = if null attrs then "" else " " ++ unwords (map renderAttr attrs)
68-
childrenStr = concatMap render children
69-
in "<" ++ tag.str ++ attrsStr ++ ">" ++ childrenStr ++ "</" ++ tag.str ++ ">"
70-
render (EmptyElement tag attrs) =
71-
let attrsStr = if null attrs then "" else " " ++ unwords (map renderAttr attrs)
72-
in "<" ++ tag.str ++ attrsStr ++ "/>"
73-
render (RawXml s) = s
74-
75-
||| Render with indentation (pretty print)
76-
export
77-
renderPretty : (indent : Nat) -> XmlNode -> String
78-
renderPretty n node = go n node
79-
where
80-
spaces : Nat -> String
81-
spaces k = pack (replicate k ' ')
82-
83-
go : Nat -> XmlNode -> String
84-
go i (TextNode t) = toXml t
85-
go i (Element tag attrs []) =
86-
let attrsStr = if null attrs then "" else " " ++ unwords (map renderAttr attrs)
87-
in spaces i ++ "<" ++ tag.str ++ attrsStr ++ "></" ++ tag.str ++ ">"
88-
go i (Element tag attrs children) =
89-
let attrsStr = if null attrs then "" else " " ++ unwords (map renderAttr attrs)
90-
childrenStr = unlines (map (go (i + 2)) children)
91-
in spaces i ++ "<" ++ tag.str ++ attrsStr ++ ">\n" ++ childrenStr ++ "\n" ++ spaces i ++ "</" ++ tag.str ++ ">"
92-
go i (EmptyElement tag attrs) =
93-
let attrsStr = if null attrs then "" else " " ++ unwords (map renderAttr attrs)
94-
in spaces i ++ "<" ++ tag.str ++ attrsStr ++ "/>"
95-
go i (RawXml s) = spaces i ++ s
73+
-- Render XML node to string. Mutually recursive with `renderList` over
74+
-- `List XmlNode` so Idris2's size-change termination checker sees the
75+
-- structural decrease — the earlier `concatMap render children` opaqued
76+
-- the recursion through a higher-order call and failed totality on
77+
-- Idris2 0.8.0.
78+
mutual
79+
||| Render XML node to string.
80+
export
81+
render : XmlNode -> String
82+
render (TextNode t) = toXml t
83+
render (Element tag attrs children) =
84+
let attrsStr = if null attrs then "" else " " ++ unwords (map renderAttr attrs)
85+
in "<" ++ tag.str ++ attrsStr ++ ">" ++
86+
renderList children ++
87+
"</" ++ tag.str ++ ">"
88+
render (EmptyElement tag attrs) =
89+
let attrsStr = if null attrs then "" else " " ++ unwords (map renderAttr attrs)
90+
in "<" ++ tag.str ++ attrsStr ++ "/>"
91+
render (RawXml s) = s
92+
93+
renderList : List XmlNode -> String
94+
renderList [] = ""
95+
renderList (n :: ns) = render n ++ renderList ns
96+
97+
||| Indentation helper used by `renderPretty`.
98+
spaces : Nat -> String
99+
spaces k = pack (replicate k ' ')
100+
101+
-- Render with indentation (pretty print). Mutually recursive with
102+
-- `renderPrettyList` for the same structural-termination reason as
103+
-- `render` / `renderList`. The child-separator semantics match the
104+
-- previous `unlines (map (go (i+2)) children)`: trailing newline after
105+
-- each rendered child.
106+
mutual
107+
||| Render XML node with indentation (pretty print).
108+
export
109+
renderPretty : (indent : Nat) -> XmlNode -> String
110+
renderPretty _ (TextNode t) = toXml t
111+
renderPretty i (Element tag attrs []) =
112+
let attrsStr = if null attrs then "" else " " ++ unwords (map renderAttr attrs)
113+
in spaces i ++ "<" ++ tag.str ++ attrsStr ++ "></" ++ tag.str ++ ">"
114+
renderPretty i (Element tag attrs (c :: cs)) =
115+
let attrsStr = if null attrs then "" else " " ++ unwords (map renderAttr attrs)
116+
childrenStr = renderPrettyList (i + 2) (c :: cs)
117+
in spaces i ++ "<" ++ tag.str ++ attrsStr ++ ">\n" ++
118+
childrenStr ++ "\n" ++
119+
spaces i ++ "</" ++ tag.str ++ ">"
120+
renderPretty i (EmptyElement tag attrs) =
121+
let attrsStr = if null attrs then "" else " " ++ unwords (map renderAttr attrs)
122+
in spaces i ++ "<" ++ tag.str ++ attrsStr ++ "/>"
123+
renderPretty i (RawXml s) = spaces i ++ s
124+
125+
renderPrettyList : (indent : Nat) -> List XmlNode -> String
126+
renderPrettyList _ [] = ""
127+
renderPrettyList i (n :: ns) = renderPretty i n ++ "\n" ++ renderPrettyList i ns
96128

97129
-- OOXML (Word) specific helpers
98130

99-
||| Create w: namespaced element (WordprocessingML)
131+
||| Create w: namespaced element (WordprocessingML). The auto-implicit
132+
||| proof obligation `isValidName ("w:" ++ tag) = True` discharges by
133+
||| `Refl` for any literal `tag`.
100134
export
101-
wEl : String -> List XmlAttr -> List XmlNode -> XmlNode
135+
wEl : (tag : String) ->
136+
{auto prf : isValidName ("w:" ++ tag) = True} ->
137+
List XmlAttr -> List XmlNode -> XmlNode
102138
wEl tag = el ("w:" ++ tag)
103139

104140
||| Create w: namespaced empty element
105141
export
106-
wEmptyEl : String -> List XmlAttr -> XmlNode
142+
wEmptyEl : (tag : String) ->
143+
{auto prf : isValidName ("w:" ++ tag) = True} ->
144+
List XmlAttr -> XmlNode
107145
wEmptyEl tag = emptyEl ("w:" ++ tag)
108146

109147
||| Word text run: <w:r><w:t>content</w:t></w:r>

0 commit comments

Comments
 (0)