proof(xml-7-44): discharge Xml744.Element proof debts

Four PROOF_TODO / totality failures in `Xml744.Element` blocked the
toolkit build past step 4/6.

1. `tagName s = case decEq (isValidName s) True of ...` — same `decEq`
   baseline-rot as `attrName`. Replaced with the `with proof` form,
   binding `prf : isValidName s = True` for `MkTagName`'s auto-implicit.

2. `unsafeTagName s = cast (MkTagName s)` — same never-compiled
   placeholder as `unsafeAttrName`. Bumped to `(s : String) -> {auto
   prf : isValidName s = True} -> TagName`, discharged by `Refl` for
   literals.

3. `render` failed totality through `concatMap render children` —
   Idris2's size-change checker cannot see structural decrease through
   the higher-order call. Refactored into a `mutual` block with a
   first-order `renderList : List XmlNode -> String` helper. Each
   `renderList (n :: ns)` call peels one element and recurses on the
   tail; `render Element` calls `renderList children` on the children
   list, which is a structural sub-term of the element.

4. `renderPretty.go` had the same shape (`unlines (map go children)`)
   and the same fix: `mutual` block with `renderPrettyList : Nat ->
   List XmlNode -> String`. Child-separator semantics (trailing
   newline after each child) match the previous `unlines` behaviour.

Knock-on signature changes to propagate the validity proofs through
the smart constructors:

- `el`, `emptyEl` now take `{auto prf : isValidName tag = True}`.
- `wEl`, `wEmptyEl` now take `{auto prf : isValidName ("w:" ++ tag)
  = True}` (the string-concat reduces at elaboration; all existing
  call sites use literal `tag`).

All 15 exports check `is total`. `grep` for `assert_total` /
`assert_smaller` / `believe_me` / `%unsafe` / `PROOF_TODO` /
`idris_crash` / `partial ` in the file returns no matches.

Toolkit build now advances 4/6 → 5/6. `Xml744.Document` errors
("Expected end of input" at `prefix : String` field) appear next —
separate baseline-rot follow-up.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

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

@@ -15,17 +15,25 @@ public export
 data TagName : Type where
   MkTagName : (n : String) -> {auto prf : isValidName n = True} -> TagName
 
+||| Try to create a tag name (returns Nothing if invalid).
+|||
+||| Mirrors `Xml744.Attribute.attrName` — uses `with proof` so the matched
+||| branch binds `prf : isValidName s = True` for `MkTagName`'s auto-implicit.
+||| Replaces the previous `decEq (isValidName s) True` form (`decEq` for
+||| `Bool` is not in scope on Idris2 0.8.0 with the current imports).
 export
-tagName : String -> Maybe TagName
-tagName s = case decEq (isValidName s) True of
-  Yes prf => Just (MkTagName s)
-  No _ => Nothing
-
+tagName : (s : String) -> Maybe TagName
+tagName s with (isValidName s) proof prf
+  tagName s | True  = Just (MkTagName s)
+  tagName s | False = Nothing
+
+||| Tag-name constructor for strings whose validity Idris2 can verify at
+||| elaboration time. Replaces the previous `cast (MkTagName s)` placeholder,
+||| which never compiled. The auto-implicit `isValidName s = True` discharges
+||| by `Refl` for any literal.
 export
-unsafeTagName : String -> TagName
--- PROOF_TODO: Replace cast with actual proof
--- PROOF_TODO: Replace cast with actual proof
-unsafeTagName s = cast (MkTagName s)
+unsafeTagName : (s : String) -> {auto prf : isValidName s = True} -> TagName
+unsafeTagName s = MkTagName s
 
 ||| Get the string representation of a tag name
 export
@@ -49,61 +57,91 @@ export
 txt : String -> XmlNode
 txt s = TextNode (text s)
 
-||| Create an element
+||| Create an element. Tag validity is discharged at elaboration time for
+||| any literal (or compile-time-reducible) tag string.
 export
-el : String -> List XmlAttr -> List XmlNode -> XmlNode
+el : (tag : String) -> {auto prf : isValidName tag = True} ->
+     List XmlAttr -> List XmlNode -> XmlNode
 el tag attrs children = Element (unsafeTagName tag) attrs children
 
-||| Create a self-closing element
+||| Create a self-closing element.
 export
-emptyEl : String -> List XmlAttr -> XmlNode
+emptyEl : (tag : String) -> {auto prf : isValidName tag = True} ->
+          List XmlAttr -> XmlNode
 emptyEl tag attrs = EmptyElement (unsafeTagName tag) attrs
 
-||| Render XML node to string
-export
-render : XmlNode -> String
-render (TextNode t) = toXml t
-render (Element tag attrs children) =
-  let attrsStr = if null attrs then "" else " " ++ unwords (map renderAttr attrs)
-      childrenStr = concatMap render children
-  in "<" ++ tag.str ++ attrsStr ++ ">" ++ childrenStr ++ "</" ++ tag.str ++ ">"
-render (EmptyElement tag attrs) =
-  let attrsStr = if null attrs then "" else " " ++ unwords (map renderAttr attrs)
-  in "<" ++ tag.str ++ attrsStr ++ "/>"
-render (RawXml s) = s
-
-||| Render with indentation (pretty print)
-export
-renderPretty : (indent : Nat) -> XmlNode -> String
-renderPretty n node = go n node
-  where
-    spaces : Nat -> String
-    spaces k = pack (replicate k ' ')
-
-    go : Nat -> XmlNode -> String
-    go i (TextNode t) = toXml t
-    go i (Element tag attrs []) =
-      let attrsStr = if null attrs then "" else " " ++ unwords (map renderAttr attrs)
-      in spaces i ++ "<" ++ tag.str ++ attrsStr ++ "></" ++ tag.str ++ ">"
-    go i (Element tag attrs children) =
-      let attrsStr = if null attrs then "" else " " ++ unwords (map renderAttr attrs)
-          childrenStr = unlines (map (go (i + 2)) children)
-      in spaces i ++ "<" ++ tag.str ++ attrsStr ++ ">\n" ++ childrenStr ++ "\n" ++ spaces i ++ "</" ++ tag.str ++ ">"
-    go i (EmptyElement tag attrs) =
-      let attrsStr = if null attrs then "" else " " ++ unwords (map renderAttr attrs)
-      in spaces i ++ "<" ++ tag.str ++ attrsStr ++ "/>"
-    go i (RawXml s) = spaces i ++ s
+-- Render XML node to string. Mutually recursive with `renderList` over
+-- `List XmlNode` so Idris2's size-change termination checker sees the
+-- structural decrease — the earlier `concatMap render children` opaqued
+-- the recursion through a higher-order call and failed totality on
+-- Idris2 0.8.0.
+mutual
+  ||| Render XML node to string.
+  export
+  render : XmlNode -> String
+  render (TextNode t)                       = toXml t
+  render (Element tag attrs children)       =
+    let attrsStr = if null attrs then "" else " " ++ unwords (map renderAttr attrs)
+    in "<" ++ tag.str ++ attrsStr ++ ">" ++
+       renderList children ++
+       "</" ++ tag.str ++ ">"
+  render (EmptyElement tag attrs)           =
+    let attrsStr = if null attrs then "" else " " ++ unwords (map renderAttr attrs)
+    in "<" ++ tag.str ++ attrsStr ++ "/>"
+  render (RawXml s)                         = s
+
+  renderList : List XmlNode -> String
+  renderList []        = ""
+  renderList (n :: ns) = render n ++ renderList ns
+
+||| Indentation helper used by `renderPretty`.
+spaces : Nat -> String
+spaces k = pack (replicate k ' ')
+
+-- Render with indentation (pretty print). Mutually recursive with
+-- `renderPrettyList` for the same structural-termination reason as
+-- `render` / `renderList`. The child-separator semantics match the
+-- previous `unlines (map (go (i+2)) children)`: trailing newline after
+-- each rendered child.
+mutual
+  ||| Render XML node with indentation (pretty print).
+  export
+  renderPretty : (indent : Nat) -> XmlNode -> String
+  renderPretty _ (TextNode t)                = toXml t
+  renderPretty i (Element tag attrs [])      =
+    let attrsStr = if null attrs then "" else " " ++ unwords (map renderAttr attrs)
+    in spaces i ++ "<" ++ tag.str ++ attrsStr ++ "></" ++ tag.str ++ ">"
+  renderPretty i (Element tag attrs (c :: cs)) =
+    let attrsStr    = if null attrs then "" else " " ++ unwords (map renderAttr attrs)
+        childrenStr = renderPrettyList (i + 2) (c :: cs)
+    in spaces i ++ "<" ++ tag.str ++ attrsStr ++ ">\n" ++
+       childrenStr ++ "\n" ++
+       spaces i ++ "</" ++ tag.str ++ ">"
+  renderPretty i (EmptyElement tag attrs)    =
+    let attrsStr = if null attrs then "" else " " ++ unwords (map renderAttr attrs)
+    in spaces i ++ "<" ++ tag.str ++ attrsStr ++ "/>"
+  renderPretty i (RawXml s)                  = spaces i ++ s
+
+  renderPrettyList : (indent : Nat) -> List XmlNode -> String
+  renderPrettyList _ []        = ""
+  renderPrettyList i (n :: ns) = renderPretty i n ++ "\n" ++ renderPrettyList i ns
 
 -- OOXML (Word) specific helpers
 
-||| Create w: namespaced element (WordprocessingML)
+||| Create w: namespaced element (WordprocessingML). The auto-implicit
+||| proof obligation `isValidName ("w:" ++ tag) = True` discharges by
+||| `Refl` for any literal `tag`.
 export
-wEl : String -> List XmlAttr -> List XmlNode -> XmlNode
+wEl : (tag : String) ->
+      {auto prf : isValidName ("w:" ++ tag) = True} ->
+      List XmlAttr -> List XmlNode -> XmlNode
 wEl tag = el ("w:" ++ tag)
 
 ||| Create w: namespaced empty element
 export
-wEmptyEl : String -> List XmlAttr -> XmlNode
+wEmptyEl : (tag : String) ->
+           {auto prf : isValidName ("w:" ++ tag) = True} ->
+           List XmlAttr -> XmlNode
 wEmptyEl tag = emptyEl ("w:" ++ tag)
 
 ||| Word text run: <w:r><w:t>content</w:t></w:r>