Markdown documents: printing, parsing, and the round trip

theorem ckMd_prMd (S : Sym) (e : Eqn) (hc : capsMd.eqn S e = true) (hl : isE e.lhs = true)
    (hr : isE e.rhs = true) : ckMd S (prMd S e) = some [e]

An equation reads back from its LaTeX, comment included.

theorem lexDoc_front (front : List (String × Json)) (hf : jwf (.obj front) = true)
    (segs : List Seg) (hv : Valid true segs) :
    lexDoc (frontMd front ++ render segs) = some (front, segItems segs)

The front matter and the body read back.

theorem decode_front (front : List (String × Json)) (X : List Char) :
    decodeText (frontMd front ++ X) = frontMd front ++ X

A document with front matter is read as written: decodeText leaves it alone.

theorem items_ok (D : Doc MC) (h : DocOK capsMd D) :
    ∀ it ∈ items (rawDoc prMdx D), itemOK it = true

Every construct of the printed skeleton satisfies itemOK .

theorem parseMd_printMd (d : Json) (hd : canonDoc d = true) : parseMd (printMd d) = some d

The Markdown round trip. Every ESM document in canonical form reads back from its Markdown spelling.

theorem parseMd_body (front : List (String × Json)) (hf : jwf (.obj front) = true)
    (segs : List Seg) (hv : Valid true segs) :
    parseMd (String.ofList (frontMd front ++ render segs)) = parseItemsMd front (segItems segs)

The parse of a Markdown document depends only on its front matter and its sequence of constructs: not on the prose between them, and not on equation labels.

theorem parseMd_eq_of_items (front : List (String × Json)) (hf : jwf (.obj front) = true)
    (s₁ s₂ : List Seg) (h₁ : Valid true s₁) (h₂ : Valid true s₂) (h : segItems s₁ = segItems s₂) :
    parseMd (String.ofList (frontMd front ++ render s₁)) =
      parseMd (String.ofList (frontMd front ++ render s₂))

Two valid documents with the same constructs parse alike.

theorem segItems_prose (a b : List Seg) (p : List Char) :
    segItems (a ++ .prose p :: b) = segItems (a ++ b)

Inserting prose leaves the constructs as they were.

theorem segItems_label (a b : List Seg) (raw : String) (l : List Char) :
    segItems (a ++ .labeled raw l :: b) = segItems (a ++ .item (.eqn raw) :: b)

Labelling an equation leaves the constructs as they were.

theorem parseMd_insert_prose (front : List (String × Json)) (hf : jwf (.obj front) = true)
    (a b : List Seg) (p : List Char) (h₁ : Valid true (a ++ b)) (h₂ : Valid true (a ++ .prose p :: b)) :
    parseMd (String.ofList (frontMd front ++ render (a ++ .prose p :: b))) =
      parseMd (String.ofList (frontMd front ++ render (a ++ b)))

Inserting prose does not change the parse (where the result is still valid: the prose is Inert and block constructs still start a line).

theorem parseMd_label (front : List (String × Json)) (hf : jwf (.obj front) = true)
    (a b : List Seg) (raw : String) (l : List Char) (h₁ : Valid true (a ++ .item (.eqn raw) :: b))
    (h₂ : Valid true (a ++ .labeled raw l :: b)) :
    parseMd (String.ofList (frontMd front ++ render (a ++ .labeled raw l :: b))) =
      parseMd (String.ofList (frontMd front ++ render (a ++ .item (.eqn raw) :: b)))

Adding an equation label does not change the parse.

theorem ckMd_aligned (S : Sym) (Ls : List Layout) (es : List Eqn)
    (hL : ∀ L ∈ Ls, L.OK) (hne : Ls ≠ [])
    (h : List.Forall₂ (fun L e => L.toks = print .latex S (eqExpr e) ∧ isE e.lhs = true ∧
      isE e.rhs = true) Ls es) :
    ckMd S (String.ofList ("\\begin{aligned}".toList ++ Latex.render (rowsToks Ls) ++
      "\\end{aligned}".toList)) = some (es.map (fun e => ⟨none, e.lhs, e.rhs⟩))

The aligned variant reads as the equations it lays out: a display \begin{aligned} … \end{aligned} whose rows lay out the canonical LaTeX of equations (Layout ) reads back as exactly those equations.