The printer: expressions to tokens

def escSet (c : Char) : Bool

The characters escaped by a backslash inside \mathit{}, \operatorname{}, \esm{} and a name subscript’s \mathrm{}.

def escT : List Char → List Char

Escape the text of \mathit{} and the like.

def unescT : List Char → List Char

Undo escT .

def keySpecial (c : Char) : Bool

Characters of a field key written as {\char NNN} (three decimal digits) in LaTeX: they would end a Markdown math span ($), start a comment (%), be read as an alignment tab (&), a macro parameter (#), a space (~), a superscript (^) or a control sequence (\). With _, {, } written \_, \{, \}, a key is as safe inside \mathrm{} as a JSON string value is (Esm.Document.Math.Latex.quoteL).

def dig3 (n : Nat) : List Char

Three decimal digits.

def escK : List Char → List Char

Escape a field key for \mathrm{}.

def unescK : List Char → List Char

Undo escK .

def natChars (n : Nat) : List Char

The digits of a natural number.

def grp (sf : Sf) (ts : List Tok) : List Tok

Grouping parentheses.

def rpG (sf : Sf) : Tok

The closing token of a grouping parenthesis.

def sepBy (sep : List Tok) : List (List Tok) → List Tok

Items joined by a separator.

def baseTok (g : List Char) : Tok

A single letter or a Greek name as a token.

def subTxt (sf : Sf) (r : List Char) : List Tok

The subscript text of a name: upright.

def formulaRaw (g : List Char) : List Char

The raw \mathrm{} content of a formula: counts as _{n}.

def formTok (sf : Sf) (g : List Char) : Tok

A formula name.

def segToks (sf : Sf) (g : List Char) : List Tok

One segment of a name, by its shape.

def explicitName (S : Sym) (s : String) : Bool

A name never prints bare where the parser would read it otherwise: an undeclared e (bare e^{x} reads as exp) and an undeclared d (bare \frac{d N}{d t} reads as a derivative) print in the explicit form.

def plainLast (s : String) : Bool

The last segment of a name prints with no subscript, so an index subscript may follow it.

def fnKw : List (String × Kw)

Unary functions with a native spelling, and their keyword.

def cmpKw : List (String × Kw)

Comparisons and their token.

def callOps : List String

Core operators in the call form.

def reservedOpn : List String

Names \operatorname{…} never means a template or an open operator by.

def coreOps : List String

coreOpNames of Notation.

def opnOK (s : String) : Bool

A name \operatorname{…} can carry: identifier characters and dots.

def keyOK (s : String) : Bool

A field key printed upright in a call: an identifier.

def insKV (kv : String × Json) : List (String × Json) → List (String × Json)

Sorted insertion by key.

def fieldsOf (kvs : List (String × Json)) : List (String × Json)

The fields of a node other than op and args.

def mkNode (o : String) (as : List Json) (fs : List (String × Json)) : Json

A node from its operator, operands and other fields (sorted keys).

def node (o : String) (as : List Json) : Json

The plain two-field node.

def simpleTok : Tok → Bool

Typst exponent and subscript tokens that need no parentheses: a nonnegative number in positional spelling, a letter, a Greek name.

def tparams (S : Sym) (n : String) : Option (List String)

The template parameter list, when the symbol table knows it.

def positional (S : Sym) (n : String) (bs : List (String × Json)) : Option (List String)

Positional template arguments: the table knows the parameters, they are distinct, and the bindings bind exactly them.

def rawB : Nat → List Char → Option (List Char × List Char)

Balanced text up to the } that closes depth 0; \x is one unit.

def balOK (raw : List Char) : Bool

Raw text that rawB reads back whole (the LaTeX lexer reads \mathrm{…} and \text{…} contents with rawB ).

def factorsOf (u : String) : List Esm.Units.Factor

The two-sided factor list of a units string ([] when it does not parse).

def unitsOK (sf : Sf) (u : String) : Bool

The units of a quantity print typeset when the string is the canonical spelling of a non-dimensionless unit whose typeset form reads back (Phase 1: every canonical unit does).

def wrap (sf : Sf) (L : Nat) (p : Nat × List Tok) : List Tok

Wrap a printed form for a position needing level L.

def mulToks : List (List Tok) → List Tok

A * chain: juxtaposition, \cdot before a factor that starts with a number.

inductive OpK where
  | minus | div | pow | lnot | tru | fls | ite | ic | index
  | cmp (k : Kw) | un (k : Kw) | plus | times | land | lor | mm (k : Kw) | call | other
  deriving DecidableEq

How a plain node (op and args only) prints, by its operator.

def unKw : List (String × Kw)

Unary functions with a native spelling: their keyword (log10 is \log_{10}).

def kindTable : List (String × OpK)

The plain-node operators with their own notation.

structure Out where
  lvl : Nat
  toks : List Tok
  crow : List Tok

The printed form of an expression and its level. crow is the form as the last rows of a cases block: an ifelse chain contributes its rows, anything else is the otherwise row.

def escToks (sf : Sf) (o : String) (fs : List (String × Json)) (args : List (List Tok)) :
    List Tok

The escape form: LaTeX \esm{op}{fields}{args} with the fields as JSON, Typst esm.node("op", #(fields), args).

def lpC (_sf : Sf) : Tok

The call parenthesis ( (LaTeX (, Typst ( right after a name).

def callToks (sf : Sf) (head : List Tok) (args : List (List Tok)) : List Tok

A call: name(args) with call parentheses.

def unToks (sf : Sf) (k : Kw) (t : List Tok) : List Tok

A unary function applied to the printed operand t.

def caseRow (sf : Sf) (v cnd : List Tok) : List Tok

One cases row, value & \text{if } condition, then the row break.

def icTail (sf : Sf) : List Tok

t_{0} in an initial condition N(t_{0}).

def subList (sf : Sf) (simp : Option Tok) (args : List (List Tok)) : List Tok

A subscript list: LaTeX _{a, b}; Typst _a for one simple token, else _(a, b).

def simpleE (c : Ctx) : Json → Option Tok

The one token a Typst exponent or subscript may be written as without parentheses: a nonnegative number in positional spelling, or a one-letter or Greek name.

def subOK (S : Sym) (base : Json) (is : List Json) : Bool

The index prints with a subscript unless the base is not a plain name, or the subscript would collide with a name: one formula-shaped name (it would read as the upright subscript of a name), or one digit literal n when base_n is declared (k_{1} would look like the name k_1; decision 5).

def subPat4 (sf : Sf) : Tok → Tok → Tok → Tok → Bool

Four tokens of an upright name subscript.

def subPat (sf : Sf) : List Tok → Bool

An upright name subscript: a name before it would read it as part of the name.

def inlineD (o : Out) : Bool

Derivative operand printed inline (\frac{\mathrm{d} N}{\mathrm{d} t}) when it is postfix-level or tighter, and not a negative literal.

def keyToks (sf : Sf) (k : String) : List Tok

A field key, upright.

def jsonVal (sf : Sf) (v : Json) : List Tok

A field value that is not an expression, as JSON.

def openToks (sf : Sf) (o : String) (args fields : List (List Tok)) : List Tok

The open-operator call: positional operands, then ; and the fields.

def dTime (sf : Sf) (a : Out) : Out

The time derivative.

def dSpace (sf : Sf) (w : List Tok) (a : Out) : Out

The spatial derivative along the axis printed w.

def dCall (sf : Sf) (w : List Tok) (args : List (List Tok)) : List Tok

A spatial derivative with trailing operands: \operatorname{D}_{x}(u, a, b).

def qtyToks (n : JNum) (l : List Esm.Units.Factor) : List Tok

The quantity 3\,\mathrm{m/s} / 3 thin upright("m") thin upright("s")^(-1): the number, then the unit as one token.

def numsOf : List Json → Option (List JNum)

The entries of a list that are all well-formed numbers.

def rowsOf : List Json → Option (List (List JNum))

The rows of a list of number lists.

inductive AForm where
  | col (ns : List JNum)
  | mat (rs : List (List JNum))

The two array shapes with a native spelling.

def arrForm : Json → Option AForm

A constant array printed natively: a column for rank 1, or a matrix of at least two columns (a single-column matrix would print like a column), at most 16 entries, every entry a well-formed number.

def arrToks (sf : Sf) : AForm → List Tok

The array: LaTeX bmatrix, Typst vec(…) / mat(…).

def unitToks (l : List Esm.Units.Factor) : List Tok

The unit after a number or an array.

def jbeq : Json → Json → Bool

Equality of JSON values as a check.

def idxBase (kvs : List (String × Json)) : Option String

The array an index node reads, when it names one.

def basesJ : Json → List String → List String

The arrays an expression indexes, in first-use order (appended to acc).

inductive RedK where
  | sum | prod | max | min
  deriving DecidableEq

The reductions with a native spelling.

structure FaqForm where
  red : RedK
  marked : Bool
  out : List Json
  ranges : List (String × Json)
  expr : Json
  filter : Option Json

A faq node with a native spelling, by its parts. marked: args lists the arrays the body indexes (otherwise it is empty).

def faqCand (kvs : List (String × Json)) : Option FaqForm

The parts a faq node would have.

def faqForm (kvs : List (String × Json)) : Option FaqForm

The parts of a faq node, when it is exactly the node they rebuild: no semiring, join, distinct or key, reduce absent or *, max, min, ranges absent or not empty, args empty or the arrays the body indexes.

def rangeOK : Json → Bool

A range a row can spell: [a, b], {"from": S} or {"from": S, "of": [i, …]}.

def outOK (j : Json) : Bool

An output entry: a name, or the singleton dimension 1.

def occursJ (k : String) : Json → Bool

A bare name occurs in an expression.

def faqOK (F : FaqForm) : Bool

The conditions under which the native spelling reads back.

def rowToks (c : Ctx) (P : Json → Out) (kv : String × Json) : List Tok

A range row: a \le k \le b, k \in S, k \in S(i, j).

def redRanges (F : FaqForm) : List (String × Json)

The reduced ranges: those of indices that are not output indices.

def subRows (c : Ctx) (P : Json → Out) (F : FaqForm) : List (List Tok)

The rows of the subscript: the reduced ranges, then the filter.

def headToks (sf : Sf) (F : FaqForm) : List Tok

The operator, marked when args is listed.

def subToksL (c : Ctx) (P : Json → Out) (F : FaqForm) : List Tok

The LaTeX subscript: none, one row, a lone dense range _{k=a}^{b}, or \substack.

def subToksT (c : Ctx) (P : Json → Out) (F : FaqForm) : List Tok

The Typst subscript: rows in _( … ), stacked with \.

def redToks (c : Ctx) (P : Json → Out) (F : FaqForm) : List Tok

The reduction: operator, subscript, body at level 5.

def entryToks (c : Ctx) (P : Json → Out) (F : FaqForm) (j : Json) : List Tok

An output entry: its range row when it has one.

def faqOut (c : Ctx) (P : Json → Out) (F : FaqForm) : Out

The native faq: the reduction, wrapped with its output indices when it has some.

def faqSubs (F : FaqForm) : List Json

The sub-expressions a native faq prints.

def tableP (t : List (Json × Out)) (x : Json) : Out

A printer given by a table of printed sub-expressions.

def tnameOK (n : String) : Bool

A template the call form can name: an identifier that is not a reserved operator name.

def pr (c : Ctx) (e : Json) : Out

The printer.

def pa (c : Ctx) (L : Nat) (e : Json) : List Tok

The tokens of an expression for a position needing level L.

def print (sf : Sf) (S : Sym) (e : Json) : List Tok

The tokens of a whole expression.