The parser: tokens to expressions

def close (o : String) : List Json → Json

Close an n-ary chain: one operand is itself, more make a node.

def cmpOf : Kw → Option String

The comparison a token spells.

def fnOf : Kw → Option String

The unary function a keyword spells.

def atomStart : Tok → Bool

Tokens that can start an operand of a product: juxtaposition continues a product when the next token is one of these.

def isLp : Tok → Bool

An opening parenthesis: ( or \left(; the parser reads them alike.

def isRp : Tok → Bool

The closing token of a group: ) or \right).

def decodeFormula (raw : List Char) : List Char

The name a formula token spells, if it is formula-shaped.

def subOrPlain (sf : Sf) (b : List Char) (r : List Tok) : List Char × List Tok

A single letter or Greek base, then an optional upright name subscript.

def pSeg (sf : Sf) : List Tok → Option (List Char × List Tok)

One name segment.

def pNameLoop (sf : Sf) : Nat → List Char → List Tok → Option (List Char × List Tok)

A name: segments joined by the scope dot.

def negTok : Tok → Bool

A negative literal token.

def negate : JNum → JNum

The number with the opposite sign.

def negTail : List Tok → Option (List Tok)

A negative literal right after an operand (k-1, k -1) is a binary minus and a positive number: the tokens with the sign moved off the number, when the number without its sign has a canonical form (the negation of -2^63 has none, so that spelling is refused after an operand).

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

Rebuild a node with fields: op and args go back to their sorted places.

inductive CallArg where
  | pos (v : Json)
  | named (k : String) (v : Json)

What pCallArgs read: positional arguments, or named ones.

def sortKV : List (String × Json) → List (String × Json)

Sort bindings by key (insertion).

def unitsOfRaw (raw : String) : Option (List Esm.Units.Factor)

The unit a LaTeX \mathrm{…} after a number spells.

def qty (n : JNum) (l : List Esm.Units.Factor) : Json

A quantity node.

def dNode (x : Json) (w : String) : Json

A derivative node.

def tNode (n : String) (bs : List (String × Json)) : Json

A template application node.

def constNode (v : Json) : Option String → Json

A constant node: the value, and the units when there are some.

def pCells (sep : Kw) : List Tok → Option (List JNum × List Tok)

Numbers separated by sep, up to the first other token.

def pGrid (csep rsep close : Kw) : Nat → List Tok → Option (List (List JNum) × List Tok)

Rows of numbers: cells separated by csep, rows by rsep, closed by close .

def gridJson (rows : List (List JNum)) : Json

A LaTeX bmatrix: one cell per row is a column (rank 1).

def constTail (v : Json) (r : List Tok) : Option (Json × List Tok)

The unit after an array, if any.

def icTailP (sf : Sf) : List Tok → Option (List Tok)

The ic tail (t_{0}) / (t_0).

def jsonStart : List Tok → Bool

A LaTeX field value that is JSON starts with {, [, a string or a word.

def keyOf (c : Ctx) (ts : List Tok) : Option (String × List Tok)

A field key: LaTeX \mathrm{key} =, Typst upright("key") =.

def dCallNode (w : String) (xs : List Json) : Json

A spatial derivative with trailing operands.

def eulerHead (c : Ctx) : List Tok → Bool

The input starts with Euler’s number raised to a power: an upright e, or an italic e when no variable e is declared.

def pNamePrim (c : Ctx) (ts : List Tok) : Option (Json × List Tok)

A name, or an initial condition N(t_{0}).

def pWord (c : Ctx) (w : String) (r : List Tok) : Option (Json × List Tok)

A bare run of letters (RT): the declared name when only it is declared, the product of its letters when only they are, refused otherwise (ambiguous or unknown).

def dName (c : Ctx) (k : Kw) : List Tok → Option (String × List Tok)

d then a name, up to a closing token k: dN} (a run of letters that is not itself a declared name) or d N}.

def pItalicD (c : Ctx) (r : List Tok) : Option (Json × List Tok)

The italic-d derivative variant, when no variable d is declared and neither dN nor dt written as one word is a declared name (a declared whole word wins, as in pWord : \frac{dx}{dt} with dx and dt declared is their quotient): LaTeX \frac{dN}{dt} after \frac{, Typst (d N)/(d t) after the first (.

def isKw (k : Kw) : Tok → Bool

The token is the keyword k.

inductive Row where
  | rng (k : String) (v : Json)
  | filt (x : Json)

A row of a reduction’s subscript, or an output entry: a range, or an expression (the filter, or a bare output entry).

def pRedHead (sf : Sf) : List Tok → Option (RedK × Bool × List Tok)

The operator of a reduction and whether it is marked (args listed): LaTeX \sum\limits, Typst limits(sum).

def pNames (sf : Sf) : Nat → List Tok → Option (List String × List Tok)

Names separated by commas.

def rowParts : List Row → Option (List (String × Json) × Option Json)

The ranges and the filter of a list of rows: ranges, then at most one filter, last.

def entryParts : List Row → Option (List Json × List (String × Json))

The output entries of a list of entry rows, with their ranges.

def withOut (F : FaqForm) (outs : List Json) (ors : List (String × Json)) : FaqForm

The node an output form reads: the reduction’s parts with the output entries.

def pOr (c : Ctx) : Nat → List Tok → Option (Json × List Tok)

Level 1: an or chain.

def pAnd (c : Ctx) : Nat → List Tok → Option (Json × List Tok)

Level 2: an and chain.

def pCmp (c : Ctx) : Nat → List Tok → Option (Json × List Tok)

Level 3: one comparison (comparisons do not chain: a \le k \le b is a range row of a reduction, never an expression).

def pAdd (c : Ctx) : Nat → List Tok → Option (Json × List Tok)

Level 4: + chains and binary -, including a negative literal right after an operand (negTail ). x :: acc is the pending + chain.

def pMul (c : Ctx) : Nat → List Tok → Option (Json × List Tok)

Level 5: unary minus, and * chains (juxtaposition, \cdot, \times; LaTeX inline / groups to the left). A negative literal never continues a product by juxtaposition (k -1 is k - 1); after \cdot it is a factor (k \cdot -1).

def pNot (c : Ctx) : Nat → List Tok → Option (Json × List Tok)

Level 6: not.

def pFrac (c : Ctx) : Nat → List Tok → Option (Json × List Tok)

Level 7: the Typst fraction, grouping to the left.

def pPow (c : Ctx) : Nat → List Tok → Option (Json × List Tok)

Level 8: a power.

def pExpo (c : Ctx) : Nat → List Tok → Option (Json × List Tok)

An exponent: LaTeX {…}; Typst (…) or one simple token.

def pPost (c : Ctx) : Nat → List Tok → Option (Json × List Tok)

Level 9: postfix index, _{…} or […].

def pList (c : Ctx) : Nat → Nat → List Tok → Option (List Json × List Tok)

A comma-separated list of expressions at level L (1 or 4), possibly empty when the next token closes it.

def pLv (c : Ctx) : Nat → Nat → List Tok → Option (Json × List Tok)

Parse at level 1 or level 4.

def pCallArgs (c : Ctx) : Nat → List Tok → Option (List CallArg × List Tok)

Call arguments at level 4: each positional, or name = value.

def pFields (c : Ctx) : Nat → List Tok → Option (List (String × Json) × List Tok)

Open-operator fields after ;: key = value, the value as math or as JSON.

def pVal (c : Ctx) : Nat → List Tok → Option (Json × List Tok)

A field value: JSON (LaTeX JSON tokens, Typst #value) or an expression.

def pOpn (c : Ctx) : Nat → String → List Tok → Option (Json × List Tok)

\operatorname{n}(…): a call-form core operator, a deprecated one (rewritten), a template (by the symbol table, positional or named), or an open operator.

def pDCall (c : Ctx) : Nat → List Tok → Option (Json × List Tok)

\operatorname{D}_{x}(u, a, b) after the _.

def pPrim (c : Ctx) : Nat → List Tok → Option (Json × List Tok)

A primary.

def pEulerExp (c : Ctx) : Nat → List Tok → Option (Json × List Tok)

\exp written as a power of e.

def pRange (c : Ctx) : Nat → List Tok → Option (Row × List Tok)

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

def pRow (c : Ctx) : Nat → (Tok → Bool) → List Tok → Option (Row × List Tok)

A row ending at a token isEnd accepts: an expression read whole first (it never reads a range row whole: a range row has \in or a second \le), else a range.

def pRows (c : Ctx) : Nat → Kw → Kw → List Tok → Option (List Row × List Tok)

Rows separated by sep, up to close (consumed).

def pRedBody (c : Ctx) : Nat → RedK → Bool → List Tok → Option (FaqForm × List Tok)

A reduction after its operator: the subscript rows (LaTeX: one row, a lone dense range k=a with ^{b}, or \substack; Typst: rows in _( … )), then the body.

def pRed (c : Ctx) : Nat → List Tok → Option (Json × List Tok)

A rank-0 reduction, or a reduction wrapped with its output entries.

def pFn1 (c : Ctx) : Nat → String → List Tok → Option (Json × List Tok)

f(x) after the opening parenthesis.

def pFracL (c : Ctx) : Nat → List Tok → Option (Json × List Tok)

After \frac{: a time or spatial derivative, the italic-d variant, or a quotient.

def pDT (c : Ctx) : Nat → Kw → List Tok → Option (Json × List Tok)

(dif N)/(dif t) and (partial u)/(partial x) after the first (dif / (partial.

def pDApply (c : Ctx) : Nat → String → List Tok → Option (Json × List Tok)

A derivative operator applied to a parenthesized operand.

def pCases (c : Ctx) : Nat → List Tok → Option (Json × List Tok)

cases rows: value & if cond then a row break, ending with value & otherwise; a chain re-nests to the right.

def pEscArgs (c : Ctx) : Nat → List Tok → Option (List Json × List Tok)

Typst escape arguments: , a repeated, then ).