The skeleton as a sequence of constructs

Lean module Esm.Document.Source.Items, formal/Esm/Document/Source/Items.lean at 184aa13d35e5
Imports Esm.Document.Source.SkeletonRT

A container spells a skeleton as a sequence of constructs: description blocks, path blocks, component directives, declarations, equations (model, initialization and constraint) and reactions. This is the container-independent middle layer:

items lists the constructs of a skeleton in the printer’s order;
unitems reads a construct sequence back into a skeleton. A construct belongs to the section of the last component directive before it, or to the document when there is none; within a section, constructs may come in any order (a document can interleave declarations and equations with its prose), except that the math entries of one field keep their order. unitems_items is the round trip.

Math entries are held as the container’s math text (Doc MR) at this layer; rawDoc prints them under each component’s symbol table and cookDoc reads them back (cookDoc_rawDoc ), the symbol table coming from the rest of the skeleton (symFor_mapMath), so both sides use the same table.

inductive RItem source

inductive RItem where
  | desc (s : String)
  | block (k : String) (v : Json)
  | comp (K : Kind) (name : String)
  | decl (d : Decl)
  | eqn (raw : String)
  | eqx (r : Role) (raw : String)
  | rxn (x : Rxn String)
  | plot (attrs : List (String × Json))
  | tm (t : Tm String)

One construct of a document. An equation is its math text, uninterpreted; so is a reaction’s rate. eqn is a model equation, eqx an equation of the field of its role (the containers write it for initialization equations and constraints).

def mItem source

def mItem : MR → RItem

The construct of a math entry.

def compItems source

def compItems (c : Comp MR) : List RItem

The constructs of a component section.

def items source

def items (D : Doc MR) : List RItem

The constructs of a skeleton, in the printer’s order: the document description, the top-level blocks, the top-level templates, then each component section.

Reading constructs back

def Comp.fresh source

def Comp.fresh (K : Kind) (n : String) : Comp MR

A fresh component section.

def addTo source

def addTo (c : Comp MR) : RItem → Option (Comp MR)

Add a construct to a component section. A second description is refused (and a math field written twice is refused when the section is rebuilt).

structure St source

structure St where
  desc : Option String
  blocks : List (String × Json)
  math : List MR
  comps : List (Comp MR)
  cur : Option (Comp MR)

The reader’s state: the document description, blocks and templates, the finished sections, and the open one.

def step source

def step (st : St) : RItem → Option St

Read one construct. Before the first directive only a description, blocks and templates are allowed.

def unitems source

def unitems (front : List (String × Json)) (its : List RItem) : Option (Doc MR)

Read a construct sequence (with the front matter) into a skeleton.

The round trip

def itemsOK source

def itemsOK (D : Doc MR) : Prop

A skeleton the constructs can carry: a component’s blocks are not keyed by a math field, and its math blocks are (the parser files a block by its key); the top-level entries are templates.

theorem unitems_items proved source

theorem unitems_items (D : Doc MR) (hD : itemsOK D) : unitems D.front (items D) = some D

The construct round trip.

Math entries: printed under the symbol table, and read back

def rawDoc source

def rawDoc (pr : Sym → MC → MR) (D : Doc MC) : Doc MR

Print every math entry under its symbol table: a top-level template under the document’s, a component’s entry under the component’s.

def cookComp source

def cookComp (ck : Sym → MR → Option (List MC)) (D : Doc MR) (c : Comp MR) : Option (Comp MC)

Read a component’s math entries under its symbol table; one math text may hold several equations (the multi-line variants).

def cookDoc source

def cookDoc (ck : Sym → MR → Option (List MC)) (D : Doc MR) : Option (Doc MC)

Read every math entry of a skeleton.

theorem topSym_rawDoc proved source

theorem topSym_rawDoc (pr : Sym → MC → MR) (hpr : ∀ S, HeadsKept (pr S)) (D : Doc MC) :
    topSym (rawDoc pr D) = topSym D

The tables of a printed skeleton are those of the skeleton: the printer keeps every header.

theorem cookDoc_rawDoc proved source

theorem cookDoc_rawDoc (pr : Sym → MC → MR) (ck : Sym → MR → Option (List MC))
    (hpr : ∀ S, HeadsKept (pr S)) (D : Doc MC)
    (ht : ∀ m ∈ D.math, ck (topSym D) (pr (topSym D) m) = some [m])
    (h : ∀ c ∈ D.comps, ∀ m ∈ c.math, ck (symFor D c) (pr (symFor D c) m) = some [m]) :
    cookDoc ck (rawDoc pr D) = some D

Math entries read back when each one does under its table. The table is the same on both sides: symFor and topSym read headers, never math, and the printer keeps headers.

A container’s math printer and reader, entry by entry

def prMx source

def prMx (prE : Sym → Eqn → String) (prR : Sym → Json → String) (S : Sym) : MC → MR

Print a math entry with the container’s equation printer and expression printer.

def ckMx source

def ckMx (ckE : Sym → String → Option (List Eqn)) (ckR : Sym → String → Option Json) (S : Sym) :
    MR → Option (List MC)

Read a math entry with the container’s equation reader and expression reader.

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