1. Geb
  2. Prototypes
  3. CanonicalSExpr
Imports
/- Copyright (c) 2026 Terence Rokop. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Terence Rokop -/ module public import Geb.Prototypes.ConcreteSyntax public import Mathlib.Data.Fin.VecNotation

Canonical S-expressions as a data type

[FormalSExpr] models canonical S-expressions as a family indexed by the octet string representing them, with an atom's index base10 (length xs) ++ [58] ++ xs and a list's index 40 :: xs ++ [41]. CSexp is the non-dependent form of that family and CSexp.render is the index function: 58, 40 and 41 being :, ( and ), the atom index is Geb.Csexp.printVerbatim and the list index is the parenthesized concatenation of the children's.

The point of carrying the family separately is Csexp.print_eq_render_toCSexp. Geb.Csexp.parse_print says the local parser accepts what the local printer emits; it does not say the output is a canonical S-expression. Factoring the printer through CSexp says exactly that, every CSexp over ASCII atoms rendering to one by construction; the implementation notes below give the condition.

Rose.toCSexp is the other map into the family: a rose node becomes the list whose head is its label and whose tail is its children, which is the S-expression convention for applying a function to arguments and agrees with the reading Geb.Ast.toRose fixes. It is a different encoding of the same trees from Ast.toCSexp, and GebTests.Prototypes.CanonicalSExpr exhibits a tree they spell differently.

Main definitions

    CSexp — canonical S-expressions, the W-type on CSexp.Shape.

    CSexp.render — the octet string a term is indexed by.

    Ast.toCSexp — the map underlying the implemented syntax.

    Rose.toCSexp — the label-applied-to-arguments encoding, with Rose.print its rendering and Ast.printViaRose its composite with the rose bijection.

    Rose.parse, Ast.parseViaRose — the parsers matching Rose.print and Ast.printViaRose, built from Geb.Rose.parseChildren, the bounded loop over a node's children that Geb.Prototypes.ConcreteSyntax supplies to every spelling closing a child list with ')'.

Main statements

    Csexp.print_eq_render_toCSexp — the implemented printer's output is the rendering of a canonical S-expression.

    Rose.parse_print, Ast.parseViaRose_printViaRose — the retraction law for the rose spelling, on Rose and on Ast, with Rose.format_idem and Rose.print_injective instantiating the generic corollaries at the first.

Implementation notes

CSexp.render is canonical over ASCII atoms only. [RFC9804] counts an atom's length in octets where Csexp.printVerbatim counts Chars, so CSexp.atom ['é'] renders as 1:é where the format requires 2:é. Every atom this module constructs is ASCII — Csexp.leafTok, Csexp.forkTok, and Csexp.decOf applied to a label, whose digits come from Csexp.digitChar — so Csexp.print_eq_render_toCSexp states conformance for the trees at hand. An atom type over octets would discharge the condition outright.

A rose node's arity is unbounded, so Geb.Rose.parseChildren — shared, and declared in Geb.Prototypes.ConcreteSyntax for that reason — reads until the closing parenthesis where Geb.Csexp.parseStep reads exactly two at a fork and none at a leaf. Two consequences follow. First, the loop needs a recursion bound, and it is Rose.parseAux's own Nat, used at each layer in two roles: undecremented as the loop's bound, and decremented as the child parser's fuel. A measure M therefore has to satisfy two inequalities at every node of n children: M ≥ n + 1, so that the loop reaches the closing parenthesis, and M > M' for each child's M', so that one decrement still leaves that child enough. Second, the loop returns a List (Rose k) where a node takes a Fin n-indexed tuple; Geb.Rose.ofList is that transport and Geb.Rose.ofList_ofFn the equation justifying it.

A node count satisfies both — 1 + Σ over the children majorises n + 1 because each child counts at least one, and majorises 1 + M' for each child because a sum majorises each summand. The printed length is taken not for any greater reach — it exceeds the node count several times over — but because Rose.parse supplies the input length in any case, so taking the bound in those terms leaves no node count to define and no counterpart to Geb.Csexp.size_le_length_printAst to prove. The bound is correspondingly far from tight.

CSexp.render concatenates a node's children by Fin.foldr, while the parser produces them as a List; CSexp.render_list_eq_flatten states their equality, and Rose.print_node is the resulting spelling equation. Rose.parseAux_print rewrites with it, having to read a node's own label and children. Where all that is needed of a child is that its spelling opens with a parenthesis, the weaker Rose.exists_print_eq_cons serves: Rose.parseChildren_print uses it to identify the head of a child's spelling, and Rose.parseAux_print to bound a node's arity by the length of its children's spellings.

References

    [FormalSExpr]

    [RFC9804]

Tags

canonical S-expression, conformance, parser, retraction, W-type

@[expose] public sectionnamespace Gebnamespace CSexp

The node shapes of a canonical S-expression: an atom carrying its octets, or a list of a given length. [FormalSExpr]'s MkCanonicalHint has no shape here; display hints have no counterpart in this development, and nothing below emits one.

An atom, carrying its octets.

A list of the given length.

inductive Shape where | atom : List Char → Shape | list : Nat → Shape deriving DecidableEq

The child index type: an atom has no children, a list of length n has n. A def rather than an abbrev, so that instance search at a shape already a literal cannot reduce past it to Empty or Fin n and select mathlib's Classical.choice-dependent FinEnum; deciding equality asks for the family at a general shape and reaches the named instance either way.

def Arity : Shape → Type | .atom _ => Empty | .list n => Fin n

Every arity is finitely enumerable.

instance instFinEnumArity (s : Shape) : FinEnum (Arity s) := match s with | .atom _ => finEnumEmpty | .list n => finEnumFin n
end CSexp

Canonical S-expressions, the non-dependent form of [FormalSExpr]'s CanonicalSExpr.

abbrev CSexp : Type := WType CSexp.Arity
namespace CSexp

An atom carrying the octets s.

def atom (s : List Char) : CSexp := WType.mk (.atom s) Empty.elim

A list of n elements.

def list {n : Nat} (f : Fin n → CSexp) : CSexp := WType.mk (.list n) f

The octet string a term is indexed by in [FormalSExpr]: an atom renders as its verbatim encoding, a list as its elements' renderings concatenated between parentheses.

def render : CSexp → List Char := WType.elim (List Char) fun x ↦ match x with | ⟨.atom s, _⟩ => Csexp.printVerbatim s | ⟨.list n, ch⟩ => '(' :: (Fin.foldr n (fun j acc ↦ ch j ++ acc) [] ++ [')'])
@[simp] theorem render_atom (s : List Char) : render (atom s) = Csexp.printVerbatim s := rfl@[simp] theorem render_list {n : Nat} (f : Fin n → CSexp) : render (list f) = '(' :: (Fin.foldr n (fun j acc ↦ render (f j) ++ acc) [] ++ [')']) := rfl

render_list with the children's renderings as a List. render concatenates a node's children by Fin.foldr where the parser produces them as a List; Rose.print_node is proved from this equality.

theorem render_list_eq_flatten {n : Nat} (f : Fin n → CSexp) : render (list f) = '(' :: (((List.ofFn f).map render).flatten ++ [')']) := n:ℕf:Fin n → CSexp⊢ (list f).render = '(' :: ((List.map render (List.ofFn f)).flatten ++ [')']) n:ℕf:Fin n → CSexp⊢ '(' :: (Fin.foldr n (fun j acc ↦ (f j).render ++ acc) [] ++ [')']) = '(' :: ((List.map render (List.ofFn f)).flatten ++ [')']) All goals completed! 🐙
end CSexpnamespace Ast

The canonical S-expression the implemented syntax prints: a leaf is the two-element list (leaf label), a fork the three-element list (fork left right).

def toCSexp {k : Nat} : Ast k → CSexp := WType.elim CSexp fun x ↦ match x with | ⟨.leaf i, _⟩ => CSexp.list ![CSexp.atom Csexp.leafTok, CSexp.atom (Csexp.decOf i.val)] | ⟨.fork, ch⟩ => CSexp.list ![CSexp.atom Csexp.forkTok, ch (0 : Fin 2), ch (1 : Fin 2)]
@[simp] theorem toCSexp_leaf {k : Nat} (i : Fin k) : (leaf i).toCSexp = CSexp.list ![CSexp.atom Csexp.leafTok, CSexp.atom (Csexp.decOf i.val)] := rfl@[simp] theorem toCSexp_fork {k : Nat} (l r : Ast k) : (fork l r).toCSexp = CSexp.list ![CSexp.atom Csexp.forkTok, l.toCSexp, r.toCSexp] := rflend Astnamespace Rose

The canonical S-expression of a rose tree: the head is the atom of the node's label and the tail is its children, so a node is spelled as its label applied to its arguments.

def toCSexp {k : Nat} : Rose k → CSexp := WType.elim CSexp fun x ↦ CSexp.list (Fin.cases (CSexp.atom (Csexp.decOf x.1.1.val)) x.2)
@[simp] theorem toCSexp_node {k : Nat} (i : Fin k) {n : Nat} (f : Fin n → Rose k) : (node i f).toCSexp = CSexp.list (Fin.cases (CSexp.atom (Csexp.decOf i.val)) fun j ↦ (f j).toCSexp) := rfl

Print a rose tree as a canonical S-expression.

def print {k : Nat} (r : Rose k) : List Char := CSexp.render r.toCSexp

The spelling of a node: its label as a verbatim atom, then its children in order, all between parentheses.

theorem print_node {k : Nat} (i : Fin k) {n : Nat} (f : Fin n → Rose k) : print (node i f) = '(' :: (Csexp.printVerbatim (Csexp.decOf i.val) ++ ((List.ofFn f).map print).flatten ++ [')']) := k:ℕi:Fin kn:ℕf:Fin n → Rose k⊢ (node i f).print = '(' :: (Csexp.printVerbatim (Csexp.decOf ↑i) ++ (List.map print (List.ofFn f)).flatten ++ [')']) k:ℕi:Fin kn:ℕf:Fin n → Rose k⊢ '(' :: ((List.map CSexp.render (Fin.cases (CSexp.atom (Csexp.decOf ↑i)) (fun j ↦ (f j).toCSexp) 0 :: List.ofFn fun i_1 ↦ Fin.cases (CSexp.atom (Csexp.decOf ↑i)) (fun j ↦ (f j).toCSexp) i_1.succ)).flatten ++ [')']) = '(' :: (Csexp.printVerbatim (Csexp.decOf ↑i) ++ (List.map print (List.ofFn f)).flatten ++ [')']) k:ℕi:Fin kn:ℕf:Fin n → Rose k⊢ '(' :: (Csexp.printVerbatim (Csexp.decOf ↑i) ++ ((List.ofFn (CSexp.render ∘ fun j ↦ (f j).toCSexp)).flatten ++ [')'])) = '(' :: (Csexp.printVerbatim (Csexp.decOf ↑i) ++ ((List.ofFn (print ∘ f)).flatten ++ [')'])) All goals completed! 🐙

Every spelling opens with a parenthesis, which is what tells a child of a node from the parenthesis that closes the child list.

theorem exists_print_eq_cons {k : Nat} (r : Rose k) : ∃ cs : List Char, print r = '(' :: cs := k:ℕr:Rose k⊢ ∃ cs, r.print = '(' :: cs k:ℕi:Fin kn:ℕf:Arity (i, n) → WType Arity⊢ ∃ cs, print (WType.mk (i, n) f) = '(' :: cs All goals completed! 🐙

Parser

One layer of the recursive descent: read a single s-expression, delegating each child to childParse and the loop over them to parseChildren with loopFuel.

def parseStep (k : Nat) (childParse : List Char → Option (Rose k × List Char)) (loopFuel : Nat) : List Char → Option (Rose k × List Char) | [] => none | c :: cs => if c = '(' then match Csexp.readVerbatim cs with | some (ds, cs1) => match Csexp.digitsVal ds with | some m => if h : m < k then (parseChildren childParse loopFuel cs1).map fun p ↦ (ofList ⟨m, h⟩ p.1, p.2) else none | none => none | none => none else none

Recursive descent over the rose spelling, returning the tree and the unconsumed input. The Nat argument bounds the recursion, as it does in Geb.Csexp.parseAst, and serves in two roles at each layer: undecremented as the child loop's bound, and decremented as the child parser's fuel. parse supplies the input length, which parseAux_print shows admits every tree the printer emits.

def parseAux (k : Nat) : Nat → List Char → Option (Rose k × List Char) := Nat.rec (motive := fun _ ↦ List Char → Option (Rose k × List Char)) (fun _ ↦ none) fun f ih ↦ parseStep k ih (f + 1)
@[simp] theorem parseAux_succ (k f : Nat) : parseAux k (f + 1) = parseStep k (parseAux k f) (f + 1) := rfl

The parser of the rose spelling, rejecting trailing input.

def parse (k : Nat) (cs : List Char) : Option (Rose k) := match parseAux k cs.length cs with | some (r, []) => some r | _ => none

The retraction law

The child loop reads back a printed child sequence, given a child parser that reads back each of them and one unit of fuel per child plus one for the closing parenthesis.

theorem parseChildren_print {k : Nat} (childParse : List Char → Option (Rose k × List Char)) : ∀ (ts : List (Rose k)) (fuel : Nat) (rest : List Char), (∀ t ∈ ts, ∀ r : List Char, childParse (print t ++ r) = some (t, r)) → ts.length < fuel → parseChildren childParse fuel ((ts.map print).flatten ++ ')' :: rest) = some (ts, rest) := List.rec (motive := fun ts ↦ ∀ (fuel : Nat) (rest : List Char), (∀ t ∈ ts, ∀ r : List Char, childParse (print t ++ r) = some (t, r)) → ts.length < fuel → parseChildren childParse fuel ((ts.map print).flatten ++ ')' :: rest) = some (ts, rest)) (fun fuel rest _ hfuel ↦ k:ℕchildParse:List Char → Option (Rose k × List Char)fuel:ℕrest:List Charx✝:∀ t ∈ [], ∀ (r : List Char), childParse (t.print ++ r) = some (t, r)hfuel:[].length < fuel⊢ parseChildren childParse fuel ((List.map print []).flatten ++ ')' :: rest) = some ([], rest) k:ℕchildParse:List Char → Option (Rose k × List Char)rest:List Charx✝:∀ t ∈ [], ∀ (r : List Char), childParse (t.print ++ r) = some (t, r)g:ℕhfuel:[].length < g + 1⊢ parseChildren childParse (g + 1) ((List.map print []).flatten ++ ')' :: rest) = some ([], rest) All goals completed! 🐙) (fun t ts ih fuel rest hchild hfuel ↦ k:ℕchildParse:List Char → Option (Rose k × List Char)t:Rose kts:List (Rose k)ih:∀ (fuel : ℕ) (rest : List Char), (∀ t ∈ ts, ∀ (r : List Char), childParse (t.print ++ r) = some (t, r)) → ts.length < fuel → parseChildren childParse fuel ((List.map print ts).flatten ++ ')' :: rest) = some (ts, rest)fuel:ℕrest:List Charhchild:∀ t_1 ∈ t :: ts, ∀ (r : List Char), childParse (t_1.print ++ r) = some (t_1, r)hfuel:(t :: ts).length < fuel⊢ parseChildren childParse fuel ((List.map print (t :: ts)).flatten ++ ')' :: rest) = some (t :: ts, rest) k:ℕchildParse:List Char → Option (Rose k × List Char)t:Rose kts:List (Rose k)ih:∀ (fuel : ℕ) (rest : List Char), (∀ t ∈ ts, ∀ (r : List Char), childParse (t.print ++ r) = some (t, r)) → ts.length < fuel → parseChildren childParse fuel ((List.map print ts).flatten ++ ')' :: rest) = some (ts, rest)rest:List Charhchild:∀ t_1 ∈ t :: ts, ∀ (r : List Char), childParse (t_1.print ++ r) = some (t_1, r)g:ℕhfuel:(t :: ts).length < g + 1⊢ parseChildren childParse (g + 1) ((List.map print (t :: ts)).flatten ++ ')' :: rest) = some (t :: ts, rest) k:ℕchildParse:List Char → Option (Rose k × List Char)t:Rose kts:List (Rose k)ih:∀ (fuel : ℕ) (rest : List Char), (∀ t ∈ ts, ∀ (r : List Char), childParse (t.print ++ r) = some (t, r)) → ts.length < fuel → parseChildren childParse fuel ((List.map print ts).flatten ++ ')' :: rest) = some (ts, rest)rest:List Charhchild:∀ t_1 ∈ t :: ts, ∀ (r : List Char), childParse (t_1.print ++ r) = some (t_1, r)g:ℕhfuel:(t :: ts).length < g + 1body:List Charhbody:t.print = '(' :: body⊢ parseChildren childParse (g + 1) ((List.map print (t :: ts)).flatten ++ ')' :: rest) = some (t :: ts, rest) k:ℕchildParse:List Char → Option (Rose k × List Char)t:Rose kts:List (Rose k)ih:∀ (fuel : ℕ) (rest : List Char), (∀ t ∈ ts, ∀ (r : List Char), childParse (t.print ++ r) = some (t, r)) → ts.length < fuel → parseChildren childParse fuel ((List.map print ts).flatten ++ ')' :: rest) = some (ts, rest)rest:List Charhchild:∀ t_1 ∈ t :: ts, ∀ (r : List Char), childParse (t_1.print ++ r) = some (t_1, r)g:ℕhfuel:(t :: ts).length < g + 1body:List Charhbody:t.print = '(' :: bodyhne:'(' ≠ ')'⊢ parseChildren childParse (g + 1) ((List.map print (t :: ts)).flatten ++ ')' :: rest) = some (t :: ts, rest) k:ℕchildParse:List Char → Option (Rose k × List Char)t:Rose kts:List (Rose k)ih:∀ (fuel : ℕ) (rest : List Char), (∀ t ∈ ts, ∀ (r : List Char), childParse (t.print ++ r) = some (t, r)) → ts.length < fuel → parseChildren childParse fuel ((List.map print ts).flatten ++ ')' :: rest) = some (ts, rest)rest:List Charhchild:∀ t_1 ∈ t :: ts, ∀ (r : List Char), childParse (t_1.print ++ r) = some (t_1, r)g:ℕhfuel:(t :: ts).length < g + 1body:List Charhbody:t.print = '(' :: bodyhne:'(' ≠ ')'hlt:ts.length < g⊢ parseChildren childParse (g + 1) ((List.map print (t :: ts)).flatten ++ ')' :: rest) = some (t :: ts, rest) k:ℕchildParse:List Char → Option (Rose k × List Char)t:Rose kts:List (Rose k)ih:∀ (fuel : ℕ) (rest : List Char), (∀ t ∈ ts, ∀ (r : List Char), childParse (t.print ++ r) = some (t, r)) → ts.length < fuel → parseChildren childParse fuel ((List.map print ts).flatten ++ ')' :: rest) = some (ts, rest)rest:List Charhchild:∀ t_1 ∈ t :: ts, ∀ (r : List Char), childParse (t_1.print ++ r) = some (t_1, r)g:ℕhfuel:(t :: ts).length < g + 1body:List Charhbody:t.print = '(' :: bodyhne:'(' ≠ ')'hlt:ts.length < ghcons:t.print ++ ((List.map print ts).flatten ++ ')' :: rest) = '(' :: (body ++ ((List.map print ts).flatten ++ ')' :: rest))⊢ parseChildren childParse (g + 1) ((List.map print (t :: ts)).flatten ++ ')' :: rest) = some (t :: ts, rest) All goals completed! 🐙)

The parser inverts the printer on printed input, given fuel at least the printed length, and returns the unconsumed remainder. The module docstring's implementation notes say what a measure has to satisfy and why this one is taken.

theorem parseAux_print {k : Nat} (r : Rose k) : ∀ (f : Nat) (rest : List Char), (print r).length ≤ f → parseAux k f (print r ++ rest) = some (r, rest) := WType.rec (motive := fun r ↦ ∀ (f : Nat) (rest : List Char), (print r).length ≤ f → parseAux k f (print r ++ rest) = some (r, rest)) (fun s ch ih f rest hf ↦ k:ℕr:Rose ks:Shape kch:Arity s → WType Arityih:∀ (a : Arity s) (f : ℕ) (rest : List Char), (print (ch a)).length ≤ f → parseAux k f (print (ch a) ++ rest) = some (ch a, rest)f:ℕrest:List Charhf:(print (WType.mk s ch)).length ≤ f⊢ parseAux k f (print (WType.mk s ch) ++ rest) = some (WType.mk s ch, rest) k:ℕr:Rose kf:ℕrest:List Chari:Fin kn:ℕch:Arity (i, n) → WType Arityih:∀ (a : Arity (i, n)) (f : ℕ) (rest : List Char), (print (ch a)).length ≤ f → parseAux k f (print (ch a) ++ rest) = some (ch a, rest)hf:(print (WType.mk (i, n) ch)).length ≤ f⊢ parseAux k f (print (WType.mk (i, n) ch) ++ rest) = some (WType.mk (i, n) ch, rest) k:ℕr:Rose kf:ℕrest:List Chari:Fin kn:ℕch:Arity (i, n) → WType Arityih:∀ (a : Arity (i, n)) (f : ℕ) (rest : List Char), (print (ch a)).length ≤ f → parseAux k f (print (ch a) ++ rest) = some (ch a, rest)hf:(node i ch).print.length ≤ f⊢ parseAux k f (print (WType.mk (i, n) ch) ++ rest) = some (WType.mk (i, n) ch, rest) k:ℕr:Rose kf:ℕrest:List Chari:Fin kn:ℕch:Arity (i, n) → WType Arityih:∀ (a : Arity (i, n)) (f : ℕ) (rest : List Char), (print (ch a)).length ≤ f → parseAux k f (print (ch a) ++ rest) = some (ch a, rest)hf:(node i ch).print.length ≤ f⊢ parseAux k f ((node i ch).print ++ rest) = some (node i ch, rest) k:ℕr:Rose kf:ℕrest:List Chari:Fin kn:ℕch:Arity (i, n) → WType Arityih:∀ (a : Arity (i, n)) (f : ℕ) (rest : List Char), (print (ch a)).length ≤ f → parseAux k f (print (ch a) ++ rest) = some (ch a, rest)hf:('(' :: (Csexp.printVerbatim (Csexp.decOf ↑i) ++ (List.map print (List.ofFn ch)).flatten ++ [')'])).length ≤ f⊢ parseAux k f ('(' :: (Csexp.printVerbatim (Csexp.decOf ↑i) ++ (List.map print (List.ofFn ch)).flatten ++ [')']) ++ rest) = some (node i ch, rest) cases f with k:ℕr:Rose krest:List Chari:Fin kn:ℕch:Arity (i, n) → WType Arityih:∀ (a : Arity (i, n)) (f : ℕ) (rest : List Char), (print (ch a)).length ≤ f → parseAux k f (print (ch a) ++ rest) = some (ch a, rest)hf:('(' :: (Csexp.printVerbatim (Csexp.decOf ↑i) ++ (List.map print (List.ofFn ch)).flatten ++ [')'])).length ≤ 0⊢ parseAux k 0 ('(' :: (Csexp.printVerbatim (Csexp.decOf ↑i) ++ (List.map print (List.ofFn ch)).flatten ++ [')']) ++ rest) = some (node i ch, rest) All goals completed! 🐙 k:ℕr:Rose krest:List Chari:Fin kn:ℕch:Arity (i, n) → WType Arityih:∀ (a : Arity (i, n)) (f : ℕ) (rest : List Char), (print (ch a)).length ≤ f → parseAux k f (print (ch a) ++ rest) = some (ch a, rest)g:ℕhf:('(' :: (Csexp.printVerbatim (Csexp.decOf ↑i) ++ (List.map print (List.ofFn ch)).flatten ++ [')'])).length ≤ g + 1⊢ parseAux k (g + 1) ('(' :: (Csexp.printVerbatim (Csexp.decOf ↑i) ++ (List.map print (List.ofFn ch)).flatten ++ [')']) ++ rest) = some (node i ch, rest) k:ℕr:Rose krest:List Chari:Fin kn:ℕch:Arity (i, n) → WType Arityih:∀ (a : Arity (i, n)) (f : ℕ) (rest : List Char), (print (ch a)).length ≤ f → parseAux k f (print (ch a) ++ rest) = some (ch a, rest)g:ℕhf:('(' :: (Csexp.printVerbatim (Csexp.decOf ↑i) ++ (List.map print (List.ofFn ch)).flatten ++ [')'])).length ≤ g + 1hL:(List.map print (List.ofFn ch)).flatten.length ≤ g⊢ parseAux k (g + 1) ('(' :: (Csexp.printVerbatim (Csexp.decOf ↑i) ++ (List.map print (List.ofFn ch)).flatten ++ [')']) ++ rest) = some (node i ch, rest) k:ℕr:Rose krest:List Chari:Fin kn:ℕch:Arity (i, n) → WType Arityih:∀ (a : Arity (i, n)) (f : ℕ) (rest : List Char), (print (ch a)).length ≤ f → parseAux k f (print (ch a) ++ rest) = some (ch a, rest)g:ℕhf:('(' :: (Csexp.printVerbatim (Csexp.decOf ↑i) ++ (List.map print (List.ofFn ch)).flatten ++ [')'])).length ≤ g + 1hL:(List.map print (List.ofFn ch)).flatten.length ≤ ghchild:∀ t ∈ List.ofFn ch, ∀ (r : List Char), parseAux k g (print t ++ r) = some (t, r)⊢ parseAux k (g + 1) ('(' :: (Csexp.printVerbatim (Csexp.decOf ↑i) ++ (List.map print (List.ofFn ch)).flatten ++ [')']) ++ rest) = some (node i ch, rest) k:ℕr:Rose krest:List Chari:Fin kn:ℕch:Arity (i, n) → WType Arityih:∀ (a : Arity (i, n)) (f : ℕ) (rest : List Char), (print (ch a)).length ≤ f → parseAux k f (print (ch a) ++ rest) = some (ch a, rest)g:ℕhf:('(' :: (Csexp.printVerbatim (Csexp.decOf ↑i) ++ (List.map print (List.ofFn ch)).flatten ++ [')'])).length ≤ g + 1hL:(List.map print (List.ofFn ch)).flatten.length ≤ ghchild:∀ t ∈ List.ofFn ch, ∀ (r : List Char), parseAux k g (print t ++ r) = some (t, r)hfuel:(List.ofFn ch).length < g + 1⊢ parseAux k (g + 1) ('(' :: (Csexp.printVerbatim (Csexp.decOf ↑i) ++ (List.map print (List.ofFn ch)).flatten ++ [')']) ++ rest) = some (node i ch, rest) k:ℕr:Rose krest:List Chari:Fin kn:ℕch:Arity (i, n) → WType Arityih:∀ (a : Arity (i, n)) (f : ℕ) (rest : List Char), (print (ch a)).length ≤ f → parseAux k f (print (ch a) ++ rest) = some (ch a, rest)g:ℕhf:('(' :: (Csexp.printVerbatim (Csexp.decOf ↑i) ++ (List.map print (List.ofFn ch)).flatten ++ [')'])).length ≤ g + 1hL:(List.map print (List.ofFn ch)).flatten.length ≤ ghchild:∀ t ∈ List.ofFn ch, ∀ (r : List Char), parseAux k g (print t ++ r) = some (t, r)hfuel:(List.ofFn ch).length < g + 1⊢ parseStep k (parseAux k g) (g + 1) ('(' :: (Csexp.printVerbatim (Csexp.decOf ↑i) ++ (List.map print (List.ofFn ch)).flatten ++ [')'] ++ rest)) = some (node i ch, rest) All goals completed! 🐙) r

The retraction law for the rose spelling: printing a rose tree and parsing the result returns that tree.

theorem parse_print {k : Nat} (r : Rose k) : parse k (print r) = some r := k:ℕr:Rose k⊢ parse k r.print = some r k:ℕr:Rose k⊢ (match parseAux k r.print.length r.print with | some (r, []) => some r | x => none) = some r All goals completed! 🐙

The generic corollaries, instantiated here

parse_print in the form the generic corollaries consume.

theorem retraction (k : Nat) : Retraction (parse k) (print (k := k)) := parse_print

Geb.format_idem at the rose spelling.

theorem format_idem (k : Nat) (c : List Char) : (format (parse k) print c).bind (format (parse k) print) = format (parse k) print c := Geb.format_idem _ _ (retraction k) c

Geb.print_injective at the rose spelling.

theorem print_injective (k : Nat) : Function.Injective (print (k := k)) := Geb.print_injective _ _ (retraction k)
end Rosenamespace Ast

Print an abstract syntax tree through the rose presentation. Not the same spelling as Geb.Csexp.print, which prints from Ast directly; see GebTests.Prototypes.CanonicalSExpr.

def printViaRose {k : Nat} (a : Ast k) : List Char := Rose.print a.toRose

Parse an abstract syntax tree from the rose spelling, by parsing a rose tree and crossing the bijection.

def parseViaRose (k : Nat) (cs : List Char) : Option (Ast k) := (Rose.parse k cs).map ofRose

The retraction law for the rose spelling read as a syntax on Ast: the rose retraction transported along Ast.ofRose_toRose.

theorem parseViaRose_printViaRose {k : Nat} (a : Ast k) : parseViaRose k (printViaRose a) = some a := k:ℕa:Ast k⊢ parseViaRose k a.printViaRose = some a All goals completed! 🐙
end Astnamespace Csexp

The implemented printer's output is the rendering of a canonical S-expression, hence a canonical S-expression by construction.

theorem printAst_eq_render_toCSexp {k : Nat} (a : Ast k) : printAst a = CSexp.render a.toCSexp := Ast.ind (motive := fun a ↦ printAst a = CSexp.render a.toCSexp) (fun i ↦ k:ℕa:Ast ki:Fin k⊢ printAst (Ast.leaf i) = (Ast.leaf i).toCSexp.render All goals completed! 🐙) (fun l r ihl ihr ↦ k:ℕa:Ast kl:Ast kr:Ast kihl:printAst l = l.toCSexp.renderihr:printAst r = r.toCSexp.render⊢ printAst (l.fork r) = (l.fork r).toCSexp.render All goals completed! 🐙) a

printAst_eq_render_toCSexp at the syntax's printer. This is the conformance statement parse_print does not make: that law says only that the local parser accepts the local printer's output.

theorem print_eq_render_toCSexp {k : Nat} (a : Ast k) : print a = CSexp.render a.toCSexp := printAst_eq_render_toCSexp a
end Csexpend Geb