sir: text format for Vars - #21

Open

Eduardogbg wants to merge 36 commits into

sir/loweringfrom

sir/text-format

Commits on Aug 19, 2026

sir: a text-format parser and printer
Eduardogbg
committed
98badc6
sir: prove the two-function witness parses
Eduardogbg
committed
1245fe5
sir: extract a parsed program as Lean source
Eduardogbg
committed
7e72742
sir: check well-formedness by returning its proof
Eduardogbg
committed
934cabe
sir: print and reparse every example program
Eduardogbg
committed
c3b68cc
sir: round-trip the lexer on renderable tokens
Eduardogbg
committed
901fc97
sir: prove every printer token renderable
Eduardogbg
committed
d768030
sir: number variables in the order they are printed
Eduardogbg
committed
9669510
sir: canonicalize variable identities
Eduardogbg
committed
f613bcf
sir: prove parsed programs canonical
Eduardogbg
committed
388de23
sir: replace docstrings with line comments
Eduardogbg
committed
31feff0
sir: characterize printable programs
Eduardogbg
committed
d0c697e
sir: prove parsed programs printable
Eduardogbg
committed
0a52744
sir: round-trip printed statements
Eduardogbg
committed
8f25b92
sir: round-trip printed terminators
Eduardogbg
committed
64eadf9
sir: round-trip printed block bodies
Eduardogbg
committed
942f6e8
sir: round-trip printed block headers
Eduardogbg
committed
1e0c1f1
sir: round-trip printed blocks
Eduardogbg
committed
1f0bf25
sir: split printed blocks
Eduardogbg
committed
f1eb9f2
sir: round-trip printed functions
Eduardogbg
committed
9f49eda
sir: round-trip printed programs
Eduardogbg
committed
853997c
sir: derive text round-trip corollaries
Eduardogbg
committed
d6d802b
sir: derive printed example round trips
Eduardogbg
committed
2e20368
sir: identify alpha classes with canonical programs
Eduardogbg
committed
260ca4f
sir: factor the printed-statement head out of parseStatement_printed
Eduardogbg
committed
275608f
sir: give Text and Check the module layout
Eduardogbg
committed
3bb1c4d
sir: keep printability under renaming and canonicalisation
Eduardogbg
committed
2e3699f
sir: apply the linter's simp-argument reductions in Text
Eduardogbg
committed
8617140
sir: export the alpha-equivalence theorems
Eduardogbg
committed
8f3f634
sir: rename canonicalize to normalize

Eduardogbg
and
claude
committed
0092e22
sir: run the iret arity check in the extractor

Eduardogbg
and
claude
committed
52b227d
sir: roundtrip on WellFormed, Printable deleted
Eduardogbg
committed
6c1b1a8
sir: drop the redundant alpha-equivalence exports
Eduardogbg
committed
64edf03
sir: check every well-formedness clause
Eduardogbg
committed
b8f4f96
sir: check well-formedness by a decider with a soundness theorem
Eduardogbg
committed
0fdcd58
sir: table-driven mnemonic parsing

Eduardogbg
and
claude
committed
b8b3fab