Round trip, case by case: reductions (faq), rows
theorem pOr_cmp (c : Ctx) (f : Nat) (ts r r' : List Tok) (x y : Json) (k : Kw) (o : String)
(h1 : pAdd c (f + 1) ts = some (x, .kw k :: r)) (hk : cmpOf k = some o)
(h2 : pAdd c f r = some (y, r')) (hl : ∀ r'', r' ≠ .kw .land :: r'') (ho : ∀ r'', r' ≠ .kw .lor :: r'') :
pOr c (f + 4) ts = some (node o [x, y], r')
pOr
over a comparison whose right side is followed by something that does not
continue an and or or chain.
Rows
theorem pRow_range (c : Ctx) (P : Json → Out) (k : String) (v : Json) (hk : nameOK k = true)
(hv : rangeOK v = true) (hM : ∀ a b, v = .arr [a, b] → M c a ∧ M c b ∧ P a = pr c a ∧ P b = pr c b)
(isEnd : Tok → Bool) (hle : isEnd (.kw .le) = false) (hin : isEnd (.kw .inn) = false)
(E : Kw) (hE : EndTok E) (R : List Tok) (f : Nat)
(hf : 30 * (rowToks c P (k, v)).length + 11 ≤ f) :
pRow c (f + 1) isEnd (rowToks c P (k, v) ++ .kw E :: R) = some (.rng k v, .kw E :: R)
A printed range row reads back as that range.
theorem pRows_read (c : Ctx) (sep close : Kw) (hsc : sep ≠ close) (R : List Tok) :
∀ (rs : List (Row × List Tok)), rs ≠ [] →
(∀ p ∈ rs, ∀ E, (E = sep ∨ E = close) → ∀ R' f, 30 * p.2.length + 11 ≤ f →
pRow c (f + 1) (fun t => isKw sep t || isKw close t) (p.2 ++ .kw E :: R') = some (p.1, .kw E :: R')) →
∀ f, 30 * (sepBy [.kw sep] (rs.map Prod.snd)).length + 12 ≤ f →
pRows c (f + 1) sep close (sepBy [.kw sep] (rs.map Prod.snd) ++ .kw close :: R) = some (rs.map Prod.fst, R)
Rows separated by sep and closed by close
read back, each row as printed.
def rowsL (c : Ctx) (f : Nat) (ts : List Tok) : Option (List Row × List Tok)
The LaTeX subscript, as pRedBody
reads it.
def rowsT (c : Ctx) (f : Nat) (ts : List Tok) : Option (List Row × List Tok)
The Typst subscript, as pRedBody
reads it.
The subscript
structure FaqH (c : Ctx) (F : FaqForm) (P : Json → Out) : Prop where
hE : M c F.expr
hPe : P F.expr = pr c F.expr
hFl : ∀ x, F.filter = some x → M c x ∧ P x = pr c x
hR : ∀ kv ∈ F.ranges, nameOK kv.1 = true ∧ rangeOK kv.2 = true ∧
∀ a b, kv.2 = .arr [a, b] → M c a ∧ M c b ∧ P a = pr c a ∧ P b = pr c b
What the round trip of a native faq knows of its parts.
theorem faqRows_head {c : Ctx} {F : FaqForm} {P : Json → Out} (h : FaqH c F P) :
∀ p ∈ faqRows c P F, ∃ t r, p.2 = t :: r ∧ (startA t = true ∨ t = .kw .minus)
Every printed row starts as an expression does.
theorem faqRows_ok {c : Ctx} {F : FaqForm} {P : Json → Out} (h : FaqH c F P) (isEnd : Tok → Bool)
(hle : isEnd (.kw .le) = false) (hin : isEnd (.kw .inn) = false) :
∀ p ∈ faqRows c P F, ∀ E, EndTok E → isEnd (.kw E) = true → ∀ R f, 30 * p.2.length + 11 ≤ f →
pRow c (f + 1) isEnd (p.2 ++ .kw E :: R) = some (p.1, .kw E :: R)
Every printed row reads back, before any end token the row reader accepts.
theorem pRedBody_readL {c : Ctx} {F : FaqForm} {P : Json → Out} (h : FaqH c F P) (hsf : c.sf = .latex)
(rest : List Tok) (hr : Fol c.sf 5 rest) (f : Nat)
(hf : 30 * (subToksL c P F ++ (P F.expr).at c.sf 5).length + 20 ≤ f) :
pRedBody c (f + 1) F.red F.marked (subToksL c P F ++ ((P F.expr).at c.sf 5 ++ rest)) =
some (⟨F.red, F.marked, [], redRanges F, F.expr, F.filter⟩, rest)
The LaTeX subscript and body read back.
theorem pRedBody_readT {c : Ctx} {F : FaqForm} {P : Json → Out} (h : FaqH c F P) (hsf : c.sf = .typst)
(rest : List Tok) (hr : Fol c.sf 5 rest) (f : Nat)
(hf : 30 * (subToksT c P F ++ (P F.expr).at c.sf 5).length + 20 ≤ f) :
pRedBody c (f + 1) F.red F.marked (subToksT c P F ++ ((P F.expr).at c.sf 5 ++ rest)) =
some (⟨F.red, F.marked, [], redRanges F, F.expr, F.filter⟩, rest)
The Typst subscript and body read back.
Operator, entries, ranges
def outRanges (F : FaqForm) : List (String × Json)
The range of an output index, when it has one.
The node
theorem pRows_entries {c : Ctx} {F : FaqForm} {P : Json → Out} (h : FaqH c F P)
(hO : ∀ j ∈ F.out, outOK j = true) (hout : F.out ≠ []) (close : Kw) (hc : EndTok close)
(hcc : close ≠ .comma) (R : List Tok) (f : Nat)
(hf : 30 * (sepBy [.kw .comma] (F.out.map (entryToks c P F))).length + 12 ≤ f) :
pRows c (f + 1) .comma close (sepBy [.kw .comma] (F.out.map (entryToks c P F)) ++ .kw close :: R) =
some (F.out.map (entryRow F), R)
The output entries read back as rows.
theorem M_faq (c : Ctx) (kvs : List (String × Json)) (F : FaqForm) (hF : faqForm kvs = some F)
(hok : faqOK F = true) (P : Json → Out) (hP : ∀ x ∈ faqSubs F, P x = pr c x)
(hpr : pr c (.obj kvs) = faqOut c P F) (hM : ∀ x ∈ faqSubs F, M c x) : M c (.obj kvs)
A native faq reads back.