Round trip, case by case: the and, or and * chains
theorem sepChain (c : Ctx) (L : Nat) (hL1 : 1 ≤ L) (hL : L ≤ 3) (sep : Kw) (o : String)
(loop : Nat → List Json → List Tok → Option (Json × List Tok))
(hstep : ∀ f acc r, loop (f + 1) acc (.kw sep :: r) =
match pLvl c f (L + 1) r with | some (y, r') => loop f (acc ++ [y]) r' | none => none)
(htop : ∀ f ts, pLvl c (f + 1) L ts =
match pLvl c f (L + 1) ts with | some (x, r) => loop f [x] r | none => none)
(hstop : ∀ f acc r, Fol c.sf L r → loop (f + 1) acc r = some (close o acc, r))
(hsepF : ∀ r, Fol c.sf (L + 1) (.kw sep :: r))
(xs : List Json) (hl : 2 ≤ xs.length) (hx : ∀ x ∈ xs, M c x) (rest : List Tok)
(hr : Fol c.sf L rest) (f : Nat)
(hf : need L (sepBy [.kw sep] (xs.map fun x => (pr c x).at c.sf (L + 1))).length ≤ f) :
pLvl c f L (sepBy [.kw sep] (xs.map fun x => (pr c x).at c.sf (L + 1)) ++ rest) =
some (node o xs, rest)
A chain x₁ sep x₂ sep … at level L, each operand at level L + 1, reads back.
def mulBlocks (c : Ctx) (ys : List Json) : List (Json × List Tok)
The blocks after the first factor of a product.
theorem factor_head {c : Ctx} {a : Json} (ha : M c a) :
∃ t r, (pr c a).at c.sf 6 = t :: r ∧ atomStart t = true ∧ conts c.sf 6 t = false
A factor’s tokens never start with what would end a product early or be read otherwise after an operand.