The document skeleton

def sortedDeep : Json → Bool

Every object, at every depth, has strictly increasing keys.

def canonDoc : Json → Bool

A document in canonical form: a JSON object, well formed (canonical numbers, distinct keys) with sorted keys at every depth.

def canonVal (v : Json) : Bool

A value that is canonical as a part of a document: well formed, sorted keys.

inductive Kind where
  | model
  | rs
  deriving DecidableEq, Repr

The two kinds of component, each with its own directive.

inductive DKind where
  | var
  | param
  | species
  | sub
  deriving DecidableEq, Repr

The declaration directives. sub is a subsystem included by reference, printed as a directive of its own line.

structure Decl where
  kind : DKind
  name : String
  attrs : List (String × Json)

A declaration: the directive, the declared name, and the other fields of the declared object as attributes.

structure Eqn where
  comment : Option String
  lhs : Json
  rhs : Json

An equation: lhs = rhs, with its optional _comment.

inductive Role where
  | eqn
  | init
  | cons
  deriving DecidableEq, Repr

The field an equation belongs to.

structure Term where
  species : String
  coef : JNum

One term of a reaction side: a species and its stoichiometric coefficient.

structure Rxn (ρ : Type) where
  id : String
  subs : Option (List Term)
  prods : Option (List Term)
  rate : ρ
  attrs : List (String × Json)

A reaction: its id, its sides (none for an empty side, JSON null), its rate (ρ: the expression, or its math text), and its other fields.

structure Tm (ρ : Type) where
  name : String
  params : List String
  lhs : Option ρ
  body : ρ
  attrs : List (String × Json)

An entry of expression_templates: a template (lhs = none, applied by name) or a rewrite rule (lhs = some m, its match). Its name, its parameter list (a template’s, from its header; a rule’s params stay among its attributes, params here is []), its body (ρ: the expression, or its math text), and its other fields.

inductive Mx (α ρ : Type) where
  | eq (r : Role) (e : α)
  | rxn (x : Rxn ρ)
  | plot (attrs : List (String × Json))
  | tm (t : Tm ρ)

A list entry of a component: an equation of one of the three equation fields (α: the equation, or its math text), a reaction, an analysis with one plot (its fields, with plots replaced by plot, the one plot), or an entry of expression_templates.

abbrev MC

A math entry as read.

abbrev MR

A math entry as the container’s text.

def Mx.field {α ρ : Type} : Mx α ρ → String

The field a math entry belongs to.

def Mx.key {α ρ : Type} : Mx α ρ → String

The key of an entry of an object-valued field (a template’s name).

def mathFields : List String

The fields with entries of their own, in key order. expression_templates is an object (its entries keyed by name); the others are lists.

structure Comp (α : Type) where
  kind : Kind
  name : String
  desc : Option String
  decls : List Decl
  math : List α
  mathBlocks : List (String × Json)
  blocks : List (String × Json)

One component section. α is how a math entry is held: MC in the semantic skeleton, MR (the container’s math text) in the raw one. mathBlocks holds the math fields that are not printed natively.

structure Doc (α : Type) where
  front : List (String × Json)
  desc : Option String
  blocks : List (String × Json)
  math : List α
  comps : List (Comp α)

A document skeleton: the front matter entries, the document description, the top-level path blocks, the top-level templates (expression_templates of a library file), and the component sections in order.

def Comp.mapMath {α β : Type} (f : Comp α → α → β) (c : Comp α) : Comp β

Change how math entries are held.

def keysOf : Option Json → List String

The keys of an object value.

def strsOf : Option Json → List String

The string entries of an array value.

def templatesOf : Option Json → List (String × List String)

The parameter list of every template of an expression_templates value.

def Tm.ps {ρ : Type} (t : Tm ρ) : List String

The parameter list a template or rule brings into its body’s scope: a template’s header parameters; a rule’s params attribute.

def Mx.head {α ρ : Type} : Mx α ρ → Option (String × List String)

The symbol-table entry of a template or rule: its name and parameters.

def Tm.scope {ρ : Type} (S : Sym) (t : Tm ρ) : Sym

The symbol table a template’s body is read under: the table around it, with the template’s parameters declared.

def rootTs {α ρ : Type} (root : List (String × Json)) (rm : List (Mx α ρ)) :
    List (String × List String)

The templates of the document: those of the top-level block, then the top-level template entries.

def compTs {α ρ : Type} (c : Comp (Mx α ρ)) : List (String × List String)

The templates of a component: those of its block, then its template entries.

def symWith {α : Type} (root : List (String × Json)) (rt : List (String × List String))
    (c : Comp α) (ct : List (String × List String)) : Sym

A component’s symbol table, given the document’s templates rt and the component’s own ct: the names it declares (its declarations and the entries of its declaration fields printed as blocks) and the document’s index sets.

def symFor {α ρ : Type} (D : Doc (Mx α ρ)) (c : Comp (Mx α ρ)) : Sym

The symbol table of a component (Phase 2 Sym): its declared names and the document’s index sets; the templates of the document and of the component. It reads the top-level blocks, the component’s declarations and blocks, and the headers of the template entries (name and parameters, never the math of a body), so the parser builds it before reading any math.

def topSym {α ρ : Type} (D : Doc (Mx α ρ)) : Sym

The symbol table of the top-level templates: the document’s index sets and templates.

def HeadsKept {α ρ β σ : Type} (f : Mx α ρ → Mx β σ) : Prop

A map of entries that keeps every header.

structure Caps where
  /-- A front-matter key (Typst: a named argument, so an identifier). -/
  frontKey : String → Bool
  /-- A description text. -/
  desc : String → Bool
  /-- A component name in its directive. -/
  compName : String → Bool
  /-- A declared name (printed as math). -/
  declName : String → Bool
  /-- A declaration attribute. -/
  attr : String × Json → Bool
  /-- An equation under the component's symbol table. -/
  eqn : Sym → Eqn → Bool
  /-- A reaction under the component's symbol table. -/
  rxn : Sym → Rxn Json → Bool
  /-- The fields of a plot directive. -/
  plot : List (String × Json) → Bool
  /-- A template or rule, under its body's symbol table (`Tm.scope`). -/
  tm : Sym → Tm Json → Bool

The container-specific predicates. A value failing one of them falls back to a path block (or, for an equation, the whole equations field does).

def Caps.item (caps : Caps) (S : Sym) : MC → Bool

A list entry the container spells.

def eqnJson (e : Eqn) : Json

The JSON value of an equation.

def eqnOf : Json → Option Eqn

The equation a JSON value is, when it has exactly the keys lhs, rhs and optionally a string _comment, and both sides are well-formed expressions.

def sideJson : Option (List Term) → Json

A reaction side: JSON null for an empty side, else a non-empty array.

def rxnKeys : List String

The keys of a reaction with a surface of their own; every other key is an attribute.

def rxnOf (v : Json) : Option (Rxn Json)

The reaction a JSON value is, checked by printing it back: its id is a string, both sides are present, and the rate is an expression.

def plotJson (attrs : List (String × Json)) : Json

The analysis a plot directive stands for: its fields, with plot back as the one-element plots.

def plotOf (v : Json) : Option (List (String × Json))

The plot directive an analysis is, when it has exactly one plot and no plot field, checked by printing it back.

def tmKeys (t : Tm Json) : List String

The keys of a template or rule with a surface of their own.

def strList : List Json → Option (List String)

The string entries of a list, when every entry is a string.

def tmOf (n : String) (v : Json) : Option (Tm Json)

The template (no match, params a list of strings) or the rule (a match) an entry of expression_templates is, checked by printing it back; the body and the match are expressions.

def tmWF (t : Tm Json) : Bool

Well-formed expressions in a template or rule.

def itemJson : MC → Json

The JSON value of a list entry.

def fieldJson (f : String) (ms : List MC) : Json

The value of a field from its entries: an object keyed by the entries’ names for expression_templates, a list otherwise.

def roleOf (f : String) : Option Role

The role of an equation field.

def itemOf (f : String) (v : Json) : Option MC

The math entry an entry of the math field f is.

def mathWF : MC → Bool

Well-formed expressions throughout.

def tmItem (kv : String × Json) : Option MC

The template entry an entry (name, value) of expression_templates is.

def mathOf (caps : Caps) (S : Sym) (f : String) : Json → Option (List MC)

The entries of a math field, when all of them print natively.

def descOf (caps : Caps) : Option Json → Option String

A description that prints natively.

def metaOf (caps : Caps) : Option Json → Option (List (String × Json) × Option String)

metadata printed in the front matter: a non-empty object without an esm key whose keys the container can spell there. Returns the front-matter entries and the description.

def pickVar (caps : Caps) (n : String) (v : Json) : Option Decl

A model variable as a declaration: :param for type: "parameter", :var otherwise; the type attribute is left out when it is "unknown" (the meaning of :var) or "parameter". A variable without type stays in the block.

def pickPlain (caps : Caps) (k : DKind) (n : String) (v : Json) : Option Decl

A reaction-system species or parameter as a declaration of kind k.

def pickSub (caps : Caps) (n : String) (v : Json) : Option Decl

A subsystem included by reference (it has a ref) as a declaration.

def declFields (caps : Caps) : Kind → List (String × (String → Json → Option Decl))

The declaration fields of a component kind, with their pickers.

def declField : Kind → DKind → Option String

The field a declaration of kind k belongs to, in a component of kind K.

def backDecl (K : Kind) (d : Decl) : Option (String × Json)

The entry a declaration stands for, in a component of kind K.

def compBlock (caps : Caps) (K : Kind) (desc : Option String) (kv : String × Json) :
    Option (String × Json)

Where an entry of a component goes when it is not a native surface: the description when it does not print natively, every entry without a surface of its own, and the residue of each declaration field; the math fields are decided later.

def compBase (caps : Caps) (K : Kind) (name : String) (kvs : List (String × Json)) : Comp MC

A component, before its equations are decided: its description, its declarations, and its blocks.

def mathPart (caps : Caps) (S : Sym) (kvs : List (String × Json)) (f : String) :
    List MC × Option (String × Json)

One math field of a component: its entries when every one prints natively under the symbol table S, else its block.

def compSym (root : List (String × Json)) (rt : List (String × List String)) (K : Kind)
    (caps : Caps) (name : String) (kvs : List (String × Json)) : Sym

The symbol table of a component’s entries, from the document’s templates rt: the component’s own templates are read from its expression_templates value, which is what the finished section’s table reads from its template entries or its block (compTs_compOf ).

def compOf (caps : Caps) (root : List (String × Json)) (rt : List (String × List String))
    (K : Kind) (name : String) (kvs : List (String × Json)) : Comp MC

A component: compBase , then its math fields, each native when every entry prints natively under the component’s symbol table, else a block.

def pickComp (caps : Caps) (n : String) (v : Json) : Option (String × List (String × Json))

A component entry prints as a directive when its name does and it is an object.

def topSymOf (kvs : List (String × Json)) : Sym

The symbol table of the top-level templates: the document’s index sets and its templates, read from the expression_templates value.

def topMath (caps : Caps) (kvs : List (String × Json)) : Option (List MC)

The top-level templates, when every one prints natively.

def rootBlock (caps : Caps) (tn : Bool) (kv : String × Json) : Option (String × Json)

Where a top-level entry goes when it is not a native surface: every entry without a surface of its own, the residues of models and reaction_systems, metadata when it is not in the front matter, and expression_templates when it is not native (tn).

def rootBlocks (caps : Caps) (tn : Bool) (kvs : List (String × Json)) : List (String × Json)

The top-level blocks.

def toDoc (caps : Caps) : Json → Doc MC

The skeleton of a document.

def optKv (k : String) : Option Json → List (String × Json)

An optional entry as a list.

def mathKv (c : Comp MC) (f : String) : Option (List (String × Json))

One rebuilt math field: its entries, or its block, or neither.

def mathKvs (c : Comp MC) : Option (List (String × Json))

The rebuilt math fields.

def declFieldNames : Kind → List String

The names of the declaration fields of a component kind.

def declKv (K : Kind) (c : Comp MC) (f : String) : Option (List (String × Json))

One rebuilt declaration field: its declarations joined with its residue block.

def declKvs (K : Kind) (c : Comp MC) : Option (List (String × Json))

The rebuilt declaration fields; a declaration of a kind the component does not have (:species in a model) is refused.

def ofComp (c : Comp MC) : Option Json

A component rebuilt from its section.

def backComp (c : Comp MC) : Option (String × Json)

A component back to its entry.

def ofDoc (D : Doc MC) : Option Json

A document rebuilt from its skeleton. The result is checked to be canonical, which rejects a field written twice (once natively and once in a block, say).