Reaction sides, shared by the containers
A reaction prints as one line in the chemistry notation of its container (mhchem
\ce{…} in Markdown, typsium #ce[…] in Typst), the rate over the arrow
(Notation.reactionLatex). The sides are spelled the same way in both, up to the math
surface (RSurf
):
- an empty side (JSON
null) is the empty-set symbol as math,$\varnothing$/$emptyset$; - otherwise the terms, separated by
+; a term is its stoichiometric coefficient as math followed by a space,$2$, left out when it is 1, then the species; - a species whose name is formula-shaped (
NO2) is written bare, for the package to set; any other species is its name as math under the empty symbol table,$\mathit{SO4\_aer}$.
pSide_sideTxt reads a side back from its text.
structure RSurf where
pm : String → Option Json
prm : Json → List Char
empty : List Char
A math surface for the pieces of a reaction side: how a math piece prints and reads back (under the empty symbol table), and the content of the empty-set piece.
Printing
def speciesTxt (R : RSurf) (n : String) : List Char
A species: bare when formula-shaped, else its name as math.
def termTxt (R : RSurf) (t : Term) : List Char
A term: the coefficient as math and a space, unless it is 1, then the species.
def termsTxt (R : RSurf) : List Term → List Char
The terms of a non-empty side, separated by +.
def termOK (R : RSurf) (t : Term) : Bool
A term the side syntax holds: a species name and, unless it is 1, a coefficient,
whose math has no $ and is not the empty-set piece.
def sideOK (R : RSurf) : Option (List Term) → Bool
A side the syntax holds: empty, or non-empty terms that it holds.
Reading
def after (p s : List Char) : Option (List Char)
The text after the prefix p, when it is one.
def idChar (c : Char) : Bool
A character of a reaction id: the identifier characters, -, . and : (what a
Typst label and a Pandoc identifier both hold).
def pPiece (t : List Char) : Option (List Char × List Char)
A math piece after its opening $: its content and the text after the closing $.
def pSpecies (R : RSurf) : List Char → Option (String × List Char)
A species: a math piece holding a name, or a bare run of letters and digits.
def pTerm (R : RSurf) : List Char → Option (Term × List Char)
A term: a math piece holding a number is the coefficient, and a species follows after a space; otherwise the term is a species with coefficient 1.
def pTerms (R : RSurf) : Nat → List Char → Option (List Term × List Char)
Terms separated by +.
def pSide (R : RSurf) (f : Nat) (s : List Char) : Option (Option (List Term) × List Char)
A side: the empty-set piece, or terms.
Reading back
def StopOK (r : List Char) : Prop
What may follow a side: a space, } or ], and not +.
Accepted variants
theorem pSpecies_math (R : RSurf) (hR : R.OK) (n : String) (hn : nameOK n = true)
(hd : (R.prm (.str n)).contains '$' = false) (r : List Char) :
pSpecies R ('$' :: R.prm (.str n) ++ '$' :: r) = some (n, r)
A species written as math reads as that species, formula-shaped or not (the printer writes a formula-shaped one bare).
theorem pTerm_coef (R : RSurf) (hR : R.OK) (c : JNum) (hc : numOK c = true)
(hcd : (R.prm (.num c)).contains '$' = false) (n : String) (hn : nameOK n = true)
(hq : isFormula n.toList = true ∨ (R.prm (.str n)).contains '$' = false) (r : List Char)
(hr : r.head? = some ' ' ∨ r.head? = some '}' ∨ r.head? = some ']') :
pTerm R ('$' :: R.prm (.num c) ++ '$' :: ' ' :: speciesTxt R n ++ r) = some (⟨n, c⟩, r)
A coefficient written out reads as that coefficient, 1 included (the printer leaves 1 out).