Typeset unit spellings: LaTeX and Typst, with no unit package
A const with units prints in a document as the number, a thin space, then the
canonical unit (Esm.Document.Notation
). This module gives the two typeset
forms of a canonical factor list (CanonFactors
, Esm.Units.Canonical
), a
parser for each, and the round-trip theorems.
LaTeX (latex
): the canonical spelling’s layout inside \mathrm{…}.
The numerator factors are joined by a thin space \,, a denominator follows
/, parenthesized when it has more than one factor; an exponent is a braced
superscript ^{3} or ^{1/3} (braces are required: ^12 would raise only
the 1). Inside \mathrm{} an underscore is a subscript and % starts a
comment, so a symbol’s _ is written \_ and its % is written \%. So
J/(K*mol) is \mathrm{J/(K\,mol)}, short_ton/yr is \mathrm{short\_ton/yr}.
Typst (typst
): one upright("sym")^(exp) per factor, with its SIGNED
exponent and no /: the positive-exponent factors, then the negative ones, each
group in symbol order (the order the canonical spelling reads in). The exponent is omitted when it is 1, is
^3 for a positive integer, ^(-1) for a negative one and ^(1\/3) or
^(-1\/3) for a non-integer (\/ is Typst’s literal slash; a bare / in
math would build a fraction). Factors are separated by thin: Typst math
sets two adjacent upright texts with no space between them (cm³molec⁻¹),
so the thin space is what keeps the factors apart. Symbols are % or runs of
[A-Za-z0-9_], so no character in a Typst string needs escaping. The
dimensionless unit is 1 in both forms.
Theorems: parseLatex_latex
and parseTypst_typst
, over every canonical factor
list.
Shared parsing pieces
theorem dropPrefix?_append (p rest : List Char) : (p ++ rest).dropPrefix? p = some rest
Stripping a literal prefix (List.dropPrefix?) undoes prepending it.
The literal prefixes below that are spelled as String.toList are @[noinline]: the
compiler otherwise specializes List.dropPrefix? to the literal and tries to evaluate
String.toList at compile time, which makes compiling these definitions very slow.
def pDigits (cs : List Char) : Option (ℕ × List Char)
A run of digits, read as a natural number.
def NoDigitHead (rest : List Char) : Prop
What may follow a digit run without extending it.
def joinWith (pr : Factor → List Char) (sep : List Char) : List Factor → List Char
Items printed by pr, joined by sep.
def pSepBy (pf : List Char → Option (Factor × List Char)) (sep : List Char) :
ℕ → List Char → Option (List Factor × List Char)
Items read by pf, separated by sep; at least one.
theorem pSepBy_joinWith (pf : List Char → Option (Factor × List Char)) (pr : Factor → List Char)
(sep : List Char) (P : Factor → Prop) (Stop : List Char → Prop)
(hpf : ∀ f, P f → ∀ rest, Stop rest → pf (pr f ++ rest) = some (f, rest))
(hsep : ∀ x, Stop (sep ++ x)) :
∀ (fs : List Factor) (f : Factor) (rest : List Char), (∀ g ∈ f :: fs, P g) → Stop rest →
rest.dropPrefix? sep = none → ∀ n, fs.length < n →
pSepBy pf sep n (joinWith pr sep (f :: fs) ++ rest) = some (f :: fs, rest)
Reading back a joined list: each item reads back before anything satisfying
Stop, the separator is such a thing, and the list ends before something that is
not a separator.
LaTeX
def latexExp (q : ℚ) : List Char
A positive exponent as a braced superscript (nothing for 1).
def latexFactor (f : Factor) : List Char
One factor, with the absolute value of its exponent.
def pLSym : List Char → List Char × List Char
Read a symbol: identifier characters, %, and the escapes \_, \%.
def pLExp : List Char → Option (ℚ × List Char)
Read a braced superscript, or nothing (exponent 1).
def pLDen (r : List Char) : Option (List Factor)
Read a LaTeX denominator (after the /): one factor, or a parenthesized list.
def parseLatex (s : String) : Option (List Factor)
Read a LaTeX unit back to its two-sided factor list.
The LaTeX round trip
def LStop (rest : List Char) : Prop
What stops a LaTeX symbol run: not a symbol character, not an escape.
theorem pLExp_latexExp (q : ℚ) (hq : 0 < q) (rest : List Char) (hr : ∀ r, rest ≠ '^' :: r) :
pLExp (latexExp q ++ rest) = some (q, rest)
A positive exponent reads back.
theorem pLFactor_latexFactor (f : Factor) (hs : SymChars f.1.toList) (hq : 0 < f.2)
(rest : List Char) (hr : LStop rest) : pLFactor (latexFactor f ++ rest) = some (f, rest)
One LaTeX factor reads back (with its positive exponent).
theorem pSepBy_latex (fs : List Factor) (f : Factor)
(hP : ∀ g ∈ f :: fs, SymChars g.1.toList ∧ 0 < g.2) (rest : List Char) (hS : LStop rest)
(hD : rest.dropPrefix? latexSep = none) (n : ℕ) (hn : fs.length < n) :
pSepBy pLFactor latexSep n (joinWith latexFactor latexSep (f :: fs) ++ rest) =
some (f :: fs, rest)
A list of positive-exponent factors reads back from its LaTeX join.
theorem parseLatex_latex :
∀ l : List Factor, CanonFactors l → parseLatex (latex l) = some l
LaTeX round trip. Every canonical factor list reads back from its LaTeX form.
Typst
def typstExp (q : ℚ) : List Char
A signed exponent: nothing for 1, ^n, ^(-n), ^(p\/q), ^(-p\/q).
def typstFactor (f : Factor) : List Char
One factor: upright("sym") and its signed exponent.
def typst (l : List Factor) : String
The Typst form of a canonical factor list (1 when it is empty): the
positive-exponent factors, then the negative ones, each group in symbol order
(the order the canonical spelling reads in).
def pTParen (cs : List Char) : Option (ℚ × List Char)
After ^(: '-'? digits (')' | '\/' digits ')').
def pTExp (cs : List Char) : Option (ℚ × List Char)
An optional exponent (none means 1).
def parseTypst (s : String) : Option (List Factor)
Read a Typst unit back to its two-sided factor list.
The Typst round trip
def TStop (rest : List Char) : Prop
What may follow a Typst factor: not an exponent, not a digit.
theorem parseTypst_typst :
∀ l : List Factor, CanonFactors l → parseTypst (typst l) = some l
Typst round trip. Every canonical factor list reads back from its Typst form.