What the skeleton of a canonical document satisfies
toDoc_ok
: the skeleton of a canonical document only holds what its container can
spell (Caps
), and only well-formed JSON values; the containers’ round trips assume
exactly this.
structure DocOK (caps : Caps) (D : Doc MC) : Prop where
front : ∀ kv ∈ D.front, caps.frontKey kv.1 = true
frontWF : jwf (.obj D.front) = true
desc : ∀ s, D.desc = some s → caps.desc s = true
blocks : ∀ kv ∈ D.blocks, jwf kv.2 = true
compName : ∀ c ∈ D.comps, caps.compName c.name = true
cdesc : ∀ c ∈ D.comps, ∀ s, c.desc = some s → caps.desc s = true
declName : ∀ c ∈ D.comps, ∀ d ∈ c.decls, caps.declName d.name = true
attrs : ∀ c ∈ D.comps, ∀ d ∈ c.decls, ∀ a ∈ d.attrs, caps.attr a = true ∧ jwf a.2 = true
math : ∀ c ∈ D.comps, ∀ m ∈ c.math, caps.item (symFor D c) m = true ∧ mathWF m = true
mathBlocks : ∀ c ∈ D.comps, ∀ kv ∈ c.mathBlocks, kv.1 ∈ mathFields ∧ jwf kv.2 = true
cblocks : ∀ c ∈ D.comps, ∀ kv ∈ c.blocks, kv.1 ∉ mathFields ∧ jwf kv.2 = true
rmath : ∀ m ∈ D.math, caps.item (topSym D) m = true ∧ mathWF m = true ∧ ∃ t, m = .tm t
What a container needs of a skeleton.
Well-formed values
A component
The document
theorem look_index_sets (caps : Caps) (tn : Bool) {kvs : List (String × Json)} (hl : keysSorted kvs = true) :
look "index_sets" (rootBlocks caps tn kvs) = look "index_sets" kvs
The top-level blocks keep index_sets as it is.
theorem rootTs_toDoc (caps : Caps) {kvs : List (String × Json)} (hl : keysSorted kvs = true) :
rootTs (toDoc caps (.obj kvs)).blocks (toDoc caps (.obj kvs)).math =
templatesOf (look "expression_templates" kvs)
The document’s templates, read from the skeleton, are those of the expression_templates
value.