Expressions as JSON values, and the symbol table

Lean module Esm.Document.Math.Expr, formal/Esm/Document/Math/Expr.lean at 184aa13d35e5
Imports Esm.Document.Number, Esm.Units.Typeset

The math grammars are stated over the JSON value at an expression position (spec §4.1), not over Esm.Ast, which drops fields. An expression is

a number (Json.num), in the canonical form of CONFORMANCE §5.5.3.1;
a name (Json.str): dot-separated identifier segments (§4.6 scoped references);
a node (Json.obj): op, args and any other fields.

isE is the well-formedness check. It asks for the canonical form only where the round trip needs it: object keys strictly increasing (the sorted-key canonical serialization), canonical numbers, every args entry an expression, and an op that is neither removed (§4.2 “Removed ops”) nor deprecated (neg, pow: the printer never writes them). Every other field may hold any well-formed JSON value. The redundant spellings of Notation.spellingRules (an explicit reduce: "+", a unitless scalar const, a D without wrt) are NOT excluded: they print in the generic escape form and round-trip exactly, so the theorem covers them too.

The symbol table Sym is what a document declares: the declared names and the parameter lists of the templates in scope. The printer and the parser both consult it, and the round-trip theorem holds for every table.

Characters

Names

def splitDots source

def splitDots : List Char → List (List Char)

Split a character list at every ..

def joinDots source

def joinDots : List (List Char) → List Char

Join segments with ..

def segOK source

def segOK : List Char → Bool

An identifier segment [A-Za-z_][A-Za-z0-9_]*.

def nameOK source

def nameOK (s : String) : Bool

A name: dot-separated identifier segments (every name in the corpus has this shape).

def greek source

def greek : List String

The Greek letter names that are a command in LaTeX (\lambda) and a symbol in Typst (lambda): the lowercase letters but omicron, and the eleven uppercase letters LaTeX has.

def isSingle source

def isSingle (s : List Char) : Bool

One letter, or a Greek letter name: the single name shape.

def elements source

def elements : List String

The element symbols a chemical-formula name is built from.

def digRun source

def digRun : List Char → List Char × List Char

The maximal run of digits at the front.

def letRun source

def letRun : List Char → List Char × List Char

The maximal run of letters at the front.

def pieces source

def pieces (s : List Char) : List (List Char × List Char)

Split a formula-shaped name into pieces: a run of letters and the run of digits after it (possibly empty). CH2O is [("CH", "2"), ("O", "")].

def elemToks source

def elemToks : List Char → Option (List String)

The element-symbol tokens of a letter run: an uppercase letter, then an optional lowercase one, greedily.

def isFormula source

def isFormula (s : List Char) : Bool

A chemical-formula name (decision 2): letters and digits only, read as element symbols and counts, starting with an element, with at least two tokens. NO2, CH2O, O3, NO.

def subParts source

def subParts (s : List Char) : Option (List Char × List Char)

The subscripted shape b_r: a single letter or Greek name, _, then a nonempty rest. Returns the base and the rest.

Numbers and JSON well-formedness, as checks

def numOK source

def numOK : JNum → Bool

JNum.WF as a check.

def keysSorted source

def keysSorted : List (String × Json) → Bool

Strictly increasing keys.

def jwf source

def jwf : Json → Bool

Json.WF as a check.

Operators

def removedOps source

def removedOps : List String

Spec §4.2 “Removed ops”: refused by name.

def deprecatedOps source

def deprecatedOps : List String

Deprecated: read in the call form and rewritten, never printed.

def opOK source

def opOK (s : String) : Bool

The op pattern of the schema: [A-Za-z_][A-Za-z0-9_.]* or [-+*/^<>=!]+.

def look source

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

The value of key k.

Expressions

def opFieldOK source

def opFieldOK (kvs : List (String × Json)) : Bool

The op field is present and names an operator that is neither removed nor deprecated.

def hasArgs source

def hasArgs (kvs : List (String × Json)) : Bool

The args field is present.

def isE source

def isE : Json → Bool

Well-formed expression (canonical form), as a check.

structure Sym source

structure Sym where
  names : List String := []
  templates : List (String × List String) := []

The symbol table: the names a document declares (variables, parameters, species, index names) and the parameter list of every template in scope.

This module also proves 4 lemmas without doc comments; they are in the source.