Concrete syntaxes for the Geb AST (prototype)

The abstract syntax is the initial algebra of F X = Fin k + X × X. A concrete syntax is a pair parse : C → Option D, print : D → C satisfying the retraction law parse (print d) = some d; formatter idempotence and injectivity of print are corollaries, proved once here for every syntax.

This module carries the format-independent core (the abstract syntax, its annotated form, the rose presentation), one worked concrete syntax, the canonical S-expression form of [RFC9804], and the parser machinery more than one spelling shares: the decimal layer and the bounded loop over a rose node's children.

Every tree type here is a WType, so its recursion is carried by WType.elim, WType.para and WType.rec.

Main definitions

Ast — the abstract syntax, the W-type on Ast.Shape.

Ast.toRose, Ast.ofRose — the two directions of the rose presentation's bijection with Ast.

Tree — the abstract syntax with every node decorated by an A, with Tree.map, Tree.extract, Tree.duplicate its functor and comonad structure and Tree.erase the forgetful map to Ast.

Ann, Doc — the annotation vocabulary and the annotated document type Tree k Ann, with Ast.trivialDoc the empty decoration.

Rose — the rose-tree presentation of the same fixed point, with Rose.node and Rose.ofList its constructors and Rose.snoc appending a child to one.

Rose.parseChildren — the bounded loop reading a rose node's children up to the closing parenthesis, shared by every spelling of the rose presentation that closes a child list with ')'.

Retraction, format — the law skeleton a concrete syntax proves.

Csexp.print, Csexp.parse — the [RFC9804] canonical S-expression syntax.

Main statements

Ast.ind — the two-constructor induction principle on Ast.

Ast.ofRose_toRose, Ast.toRose_ofRose — the rose presentation is a bijection.

Rose.ofList_ofFn — a rose node rebuilt by Rose.ofList from the list of its children is that node. It is the equation justifying the transport a variable-arity parser needs.

Csexp.parse_print — the retraction law for the S-expression syntax, from Csexp.parseAst_printAst and Csexp.size_le_length_printAst.

Csexp.readVerbatim_append — a printed atom reads back whole, whatever it contains.

Ast.erase_trivialDoc — the trivial decoration is erased away.

Csexp.format_idem, Csexp.print_injective — the generic corollaries instantiated, which is what shows the law skeleton applies to a syntax rather than only to a hypothetical one.

Geb.format_idem, Geb.print_injective — the corollaries of a retraction, proved once for every syntax.

Tree.extract_duplicate, Tree.map_extract_duplicate, Tree.duplicate_duplicate — the comonad laws on the annotated syntax, with Tree.map_id and Tree.map_map the functor laws they presuppose and Tree.extract_map, Tree.duplicate_map the naturality of the two structure maps.

Implementation notes

Csexp.parseAst recurses on an explicit Nat bound rather than on its input: the recursion descends only through the remainder each call returns, which is not a form Lean's structural recursion accepts. Csexp.parse supplies the input length, and Csexp.size_le_length_printAst shows that bound admits every tree the printer emits.

The decimal layer is written here rather than reused, and the reason is Classical.choice throughout. mathlib's Nat.digits depends on it. Core supplies the whole layer — Nat.toDigits, which agrees with Csexp.decOf pointwise on base 10, the decoder Nat.ofDigitChars, and the same round trip in total form, Nat.ofDigitChars_ten_toDigits, where Csexp.digitsVal_decOf is partial. It cannot be used. That round trip depends on Classical.choice, and so does every lemma descending from toDigits b n to toDigits b (n / b) — Nat.toDigits_eq_if and Nat.toDigits_of_base_le — so it can be neither imported nor reproved. The boundary is not depth but direction: the printer's descent lemmas are choice-dependent, while the decoder's recursion equations and the digit-character lemmas are not.

finEnumFin and finEnumEmpty are named because mathlib's FinEnum instances for Fin n and Empty are Classical.choice-dependent.

Rose.Arity is an abbrev because a proof matching a child function's type against a lemma stated at Fin n → _ needs it reducible; Ast.ofRose_snoc and Ast.toRose_ofRose are the two here, and Rose.parseAux_print and Rsexp.parseAux_print the third and fourth, downstream. Its docstring names all four and says what the reducibility costs.

Ast.Arity and Tree.Arity are plain defs, which keeps instance search from reducing past them at a literal shape. No demand here reaches that case; the defs guard against one arising later, which would otherwise resolve through mathlib's Classical.choice-dependent FinEnum.fin.

References

[RFC9804]

[UustaluVene2011]

Tags

abstract syntax, concrete syntax, W-type, retraction, S-expression

Choice-free finite enumerations

Every Arity family below is finitely enumerable, which is what lets WType.instDecidableEq decide equality of the corresponding tree type. The #guards in the three GebTests syntax modules decide equality at Ast k, at Tree k Ann and at Rose k. The two enumerations are named because mathlib's FinEnum.fin and FinEnum.empty are built by FinEnum.ofList, whose proof obligations depend on Classical.choice, which CONTRIBUTING.md § Constructive-only forbids. Naming them suffices for that consumer: WType.instDecidableEq asks for a family at a general shape, where nothing reduces, so equality is decided choice-free however the family is declared — Rose.Arity is an abbrev and equality at Rose k is choice-free. What a reducible family gives up is FinEnum demanded at a shape already a literal, where search reduces past it to Empty or Fin n and selects mathlib's. Ast.Arity and Tree.Arity are plain defs so that such a demand would reach the named instance; nothing here makes one. Neither construction is specific to syntax.

Fin n enumerated by the identity equivalence.

Empty enumerated by the empty equivalence.

Abstract syntax

The node shapes of the Geb abstract syntax: a leaf carrying a label in Fin k, or a fork.

A leaf, labelled by an element of Fin k.

A fork, with two children.

The child index type of each shape: a leaf has none, a fork has two. Fin 2 rather than Bool, so that every non-empty arity here is enumerated by finEnumFin. A def rather than an abbrev: reducible, instance search at a concrete shape would whnf past this family to Empty or Fin 2 and select mathlib's Classical.choice-dependent FinEnum, never reaching instFinEnumArity.

Every arity is finitely enumerable.

The Geb abstract syntax: the initial algebra of F X = Fin k + X × X, presented as the W-type on Ast.Shape k.

A leaf labelled i.

A fork with left child l and right child r.

The number of nodes.

Induction on Ast in its two-constructor presentation, so that a proof driven by it need not mention the underlying shape and arity.

Annotated syntax

The node shapes of the annotated syntax: an Ast.Shape paired with the decoration carried at that node.

The child index type of an annotated shape: that of the underlying Ast.Shape, since decorating a node does not change its children. A def rather than an abbrev, for the reason Ast.Arity gives.

Every annotated arity is finitely enumerable.

Ast k with every node decorated by an A: the initial algebra of X ↦ A × F X. The initial algebra rather than the terminal coalgebra, because syntax trees are finite; the cofree comonad on F admits infinitely deep trees and is the home of execution traces, not syntax.

Relabel every node along f.

The comonad counit: the decoration at the root.

The comonad comultiplication: relabel each node with the annotated subtree rooted at it, in the sense [UustaluVene2011] gives the comultiplication of the cofree recursive comonad. A paramorphism, since the new decoration at a node is that node's own subtree.

Forget every decoration, recovering the bare tree. This is the fold induced by the second projection A × F X → F X, not the comonad counit.

The first functor law: relabelling along the identity is the identity.

The second functor law: relabelling twice is relabelling along the composite.

Naturality of the counit: reading the root decoration commutes with relabelling.

Naturality of the comultiplication: redecorating commutes with relabelling, the relabelling acting on each subtree.

The first comonad law: the subtree redecorating the root is the whole tree.

The second comonad law: taking each node's subtree and then keeping only its root decoration recovers the original decoration.

The third comonad law, coassociativity of the redecoration map.

The annotation vocabulary carried at a node. Durable metadata is an annotation value, never a lexical comment: generic parsers discard comments, and canonical forms differ over whether they are retained.

A name for the annotated occurrence.

Prose documentation of the annotated occurrence.

References to material bearing on the annotated occurrence.

An annotated Geb document.

Decorate every node with the empty annotation.

Decorating every node with the empty annotation and then erasing is the identity.

The rose presentation and its bijection

The node shapes of the rose presentation: a label in Fin k and a number of children.

The child index type of a rose shape. Reducible, and this is the one family that has to be: simp and rw match at reducible transparency, so with a plain def a child function whose type reads Rose.Arity (i, n) → _ in a goal fails to unify with a lemma stated at Fin n → _, and the proofs of Ast.ofRose_snoc and Ast.toRose_ofRose fail here, Geb.Rose.parseAux_print's and Geb.Rsexp.parseAux_print's downstream. The cost is that instFinEnumArity below is unreachable at a concrete shape: instance search reduces past this family to Fin n and selects mathlib's Classical.choice-dependent FinEnum.fin. Deciding equality at a Rose k does not incur that, WType.instDecidableEq asking for the family at a general shape and so reaching the named instance; what would pay it is a demand for FinEnum at a shape already a literal. Ast.Arity and Tree.Arity are plain defs, at which search reaches the named instance either way.

Every rose arity is finitely enumerable. Named for the same reason as the other two: WType.instDecidableEq asks for this family at a general shape, so deciding equality at a Rose k goes through this instance rather than mathlib's Classical.choice-dependent FinEnum.fin. All three GebTests syntax modules decide it. A #guard is not a declaration, so GebMeta.detectNonstandardAxiom would not catch a leak there.