The Typst container

Lean module Esm.Document.Source.Typst, formal/Esm/Document/Source/Typst.lean at 184aa13d35e5
Imports Esm.Document.Source.Reaction, Esm.Document.Source.Equation

An ESM document in Typst is markup plus the functions of an esm Typst package:

#import "@preview/esm:0.1.0": *
#show: esm-document.with(esm: "2.1.0", name: "Decay")

#description[First\-order radioactive decay.]

#model("Decay")

#var($N$, default: 100, units: "mol")

$ (dif N)/(dif t) = -lambda N $

The constructs (Esm.Document.Source.RItem ), and where they may appear:

the header: the #import line, then #show: esm-document.with(…) with the front-matter entries as named arguments (values in the Typst value syntax, Esm.Document.TypstDict );
at the start of a line: #description[…] (the text with Typst’s markup characters escaped by a backslash), #esm-block("key", value) (a path block), #model("Name") or #reaction-system("Name"), and a display equation $ … $ (optionally followed by a label <eq-x>, which is discarded);
at the start of a line: a reaction, #ce[…] <id> on one line, in typsium (Esm.Document.Source.Reaction ) with the rate as Typst math over the arrow, ->[$k$], and the reaction’s id as the label; a reaction with other fields is wrapped as #reaction(key: value, …)[#ce[…]] <id>;
at the start of a line: #initialization[$ … $] or #constraints[$ … $], an initialization equation or a constraint;
at the start of a line: #subsystem("Name", ref: "…", …), a subsystem included by reference;
at the start of a line: a template, $ op("f")(a, b) := body $ (wrapped as #template(key: value, …)[$ … $] with other fields), or a rule, #rule("r", $lhs$, $rhs$, key: value, …);
at the start of a line: #plot(key: value, …), an analysis with exactly one plot: the analysis’s fields, the plot as the argument plot;
anywhere: a declaration #var($N$, …), #param(…) or #species(…), the name in Typst math and the attributes as named arguments.

Everything else is prose, which the parser skips, so the parse depends only on the sequence of constructs (lex_render ). Prose may not contain a declaration opener (#var(, #param(, #species(), nor start a line with a block opener; in particular a line starting with $ is always a model equation, so outside a model it rejects the file. Conversely a model equation must start its line: display math $ … $ after other text on a line is prose (Typst typesets it, but it is not part of the model). Raw text (`…`) is not skipped whole: a declaration opener inside it is still read.

The reader first drops a leading byte-order mark and, when the first line ends in CRLF, reads every CRLF as LF (decodeText ).

Spellings

def oRole source

def oRole : Role → List Char

The opener of the equation container of a role.

def header source

def header : List Char

The header’s first line and the start of its second.

Description text

def mustEsc source

def mustEsc (bol : Bool) (c : Char) (next : Option Char) : Bool

Whether a character of a description is written escaped: Typst’s markup characters always; =, - and + at the start of a line (a heading or a list item); / before / or * (a comment).

def escT source

def escT : Bool → List Char → List Char

A description’s text in a content block.

def readEsc source

def readEsc : List Char → Option (List Char × List Char)

The text of a content block up to its unescaped ].

Named arguments

def argT source

def argT (a : String × Json) : List Char

key: value.

def pArg source

def pArg (F : Nat) (s : List Char) : Option ((String × Json) × List Char)

One named argument at its key.

def pArgsMore source

def pArgsMore (F : Nat) : Nat → List Char → Option (List (String × Json) × List Char)

, key: value repeated, up to ).

def pArgsFirst source

def pArgsFirst (F f : Nat) : List Char → Option (List (String × Json) × List Char)

Arguments directly after (.

def argsMoreT source

def argsMoreT (as : List (String × Json)) : List Char

Arguments after a first positional one: each , key: value.

def argsFirstT source

def argsFirstT : List (String × Json) → List Char

Arguments directly after (.

def argOK source

def argOK (a : String × Json) : Bool

A named argument Typst can carry: an identifier key that is not a keyword.

Constructs

def declT source

def declT (d : Decl) : List Char

#var($N$, default: 100).

def lineEnd source

def lineEnd (t : List Char) : Option (List Char)

The rest of a construct’s line must be blank.

Reactions

def typR source

def typR : RSurf

The math surface of reaction sides: Typst math under the empty symbol table.

def coreT source

def coreT (x : Rxn String) : List Char

The chemistry of a reaction: the sides and the rate over the arrow.

def rxnT source

def rxnT (x : Rxn String) : List Char

A reaction line: #ce[…] <id>, or #reaction(…)[#ce[…]] <id> with its other fields.

def coreAt source

def coreAt (F : Nat) (u : List Char) :
    Option (Option (List Term) × List Char × Option (List Term) × List Char)

The chemistry of a reaction: subs, rate, prods, and the text after the products.

def labelAt source

def labelAt (u : List Char) : Option (String × List Char)

The label <id> and the end of the line.

def ceAt source

def ceAt (F : Nat) (u : List Char) : Option (RItem × List Char)

A reaction after #ce[.

def rxnAtT source

def rxnAtT (F : Nat) (u : List Char) : Option (RItem × List Char)

A reaction after #reaction(.

Templates and rules

A template is a display whose math starts with its header, $ op("f")(a, b) := body $ ; with other fields it is wrapped, #template(key: value, …)[$ op("f")(a, b) := body $]. A rule is #rule("r", $lhs$, $rhs$, key: value, …). The header (the name, the parameters as names under the empty symbol table) is read here, by the lexer; only the body and the left-hand side are math.

def tmRawT source

def tmRawT (t : Tm String) : List Char

The math text of a template display (one line).

def nameLenT source

def nameLenT : Nat → Bool → List Char → Nat

The length of a parameter name’s Typst math: up to the first , or ) outside parentheses and string literals, since a name prints with both (italic("Ea"), A_(upright("pre"))). d is the parenthesis depth, q whether inside a string.

def pNameT source

def pNameT (s : List Char) : Option (String × List Char)

A parameter name in a template header, read as Typst math.

def tmLexT source

def tmLexT (raw : List Char) : Option (String × List String × List Char)

Read the math text of a display as a template: its name, parameters and body text.

def itemT source

def itemT : RItem → List Char

The text of a construct.

def eqnLabeled source

def eqnLabeled (raw : String) (label : List Char) : List Char

A display equation with a label after it ( <eq-x>).

def labelOK source

def labelOK (sl : List Char) : Bool

A label after a display equation: nothing, or <id>, with spaces around.

The lexer

def dispItem source

def dispItem (raw : List Char) : RItem

A display’s construct from its math text: a template when it reads as one, else an equation.

def tmplAtT source

def tmplAtT (F : Nat) (u : List Char) : Option (RItem × List Char)

A template with other fields, after #template(.

def ruleAtT source

def ruleAtT (F : Nat) (u : List Char) : Option (RItem × List Char)

A rule, after #rule(.

def eqxAt source

def eqxAt (ro : Role) (u : List Char) : Option (RItem × List Char)

An equation in a container after its opener: $ … $].

def subAtT source

def subAtT (F : Nat) (u : List Char) : Option (RItem × List Char)

A subsystem directive after #subsystem(.

def plotAtT source

def plotAtT (F : Nat) (u : List Char) : Option (RItem × List Char)

A plot directive after #plot(.

def lex source

def lex : Nat → Bool → List Char → Option (List RItem)

The Typst lexer: the constructs of a text, skipping prose one character at a time.

Reading back the pieces

theorem size_le_argT proved source

theorem size_le_argT (a : String × Json) : a.2.size ≤ (argT a).length

The fuel the value reader needs, bounded by the text.

def typsiumOK source

def typsiumOK (x : Rxn String) : Bool

What typsium and the Typst parser read as written inside #ce[…]: no // or /*, which would open a comment and swallow the rest of the line.

def rxnOK source

def rxnOK (x : Rxn String) : Bool

A reaction the Typst syntax can hold: sides the side syntax holds, a rate on one line without $, an id label, named arguments Typst can carry, and nothing typsium misreads.

def declOK source

def declOK (d : Decl) : Bool

A declaration the Typst syntax can hold.

Documents, prose and validity

inductive Seg source

inductive Seg where
  | item (it : RItem)
  | labeled (raw : String) (label : List Char)
  | prose (p : List Char)

A piece of a Typst document: a construct, a labelled equation, or prose.

def itemOK source

def itemOK : RItem → Bool

What each construct’s content must satisfy for its text to read back.

def Inert source

def Inert : Bool → List Char → List Char → Prop

Prose that the lexer skips.

Lexing, construct by construct

Containers

Subsystems

Plots

Templates and rules

Reactions

theorem lex_render proved source

theorem lex_render : ∀ (segs : List Seg) (bol : Bool), Valid bol segs →
    ∀ f, (render segs).length < f → lex f bol (render segs) = some (segItems segs)

The Typst lexer reads back every valid document body: exactly its constructs, whatever prose surrounds them and whatever labels the equations carry.

This module also proves 49 lemmas without doc comments; they are in the source.