The Typst lexer lemma
Every list of Typst tokens (tokOK
) in which each call parenthesis follows a token
after which ( is a call parenthesis (CallOK) reads back from its rendering. The
proof goes token by token, as for LaTeX; the one Typst-specific step is the
parenthesis: the lexer tells a call ( from a grouping ( by the character before
it, and the renderer writes a space before a grouping ( exactly when that
character would make it a call.
Tokens
def kwOK : Kw → Bool
Typst keywords: the ones with a Typst spelling, except times (the printer
never writes it; it would run into the times 10^… of a scientific number).
def Sep (t : Tok) (X : List Char) : Prop
What may follow the spelling of t: nothing that extends it.
Characters
Dispatch
Numbers
theorem sciExp_head (c : Char) (r : List Char) (h1 : isWsT c = false) (h2 : c ≠ 't') :
sciExp (c :: r) = none
No scientific tail where times does not come first.
theorem sciExp_tail (e : Int) (X : List Char) (hX : Number.NumStop X) :
sciExp (timesTen ++ ((if e < 0 then '(' :: Number.printInt e ++ [')'] else Number.printInt e) ++ X)) =
some (e, X)
The printed scientific tail reads back as its exponent.
Identifier tokens
Upright pieces
One token
Heads
What may follow a number or a unit block
Token lists
def Adj : List Tok → Prop
Neighbouring tokens: a call parenthesis follows a token after which ( is a call
parenthesis, and a unit block never follows a unit block.
def HC (t : Tok) (S : List Char) (prev : Option Char) : Prop
What the lexer needs to tell the first token’s parenthesis right.
theorem lex_render (ts : List Tok) (h : ∀ t ∈ ts, tokOK t) (ha : Adj ts)
(hfirst : ∀ r, ts ≠ .kw .lp :: r) : lex (render ts) = some ts
The Typst lexer lemma: a list of Typst tokens whose call parentheses each follow a name-like token, and whose unit blocks are not adjacent, reads back from its rendering.