Parsing constructor tokens in prefix order

A token describes a leaf, a unary constructor, or a binary constructor. parseFuel reads one value and returns the unconsumed suffix, or none on an invalid token, missing operand, or exhausted fuel. No default value or inhabitance assumption is needed. parse uses the input length as fuel, and decode additionally rejects trailing tokens.

Syntax-specific round-trip proofs imply append_injective: a value's tokens determine both the value and the following suffix. This avoids comparing every pair of constructors when proving injectivity of a flat syntax encoding. No machine resource bound is asserted for these parsers.

inductive Cslib.PrefixParser.Step (α : Type u_1) : Type u_1

The constructor represented by a token, with zero, one, or two operands.

• atom {α : Type u_1} (value : α) : Step α

  A leaf value.

• unary {α : Type u_1} (make : α → α) : Step α

  A constructor with one operand.

• binary {α : Type u_1} (make : α → α → α) : Step α

  A constructor with two operands, in input order.

def Cslib.PrefixParser.parseFuel {α : Type u_1} {τ : Type u_2} (readToken : τ → Option (Step α)) : ℕ → List τ → Option (α × List τ)

Read one prefix-coded value, with fuel bounding the depth of recursive parsing.

def Cslib.PrefixParser.parse {α : Type u_1} {τ : Type u_2} (readToken : τ → Option (Step α)) (tokens : List τ) : Option (α × List τ)

Read a prefix and its remainder, using the number of input tokens as sufficient fuel.

def Cslib.PrefixParser.decode {α : Type u_1} {τ : Type u_2} (readToken : τ → Option (Step α)) (tokens : List τ) : Option α

Read exactly one value; trailing tokens are rejected.

theorem Cslib.PrefixParser.append_injective {α : Type u_1} {τ : Type u_2} {readToken : τ → Option (Step α)} {tokens : α → List τ} (roundtrip : ∀ (value : α) (rest : List τ) (fuel : ℕ), (tokens value).length ≤ fuel → parseFuel readToken fuel (tokens value ++ rest) = some (value, rest)) {left right : α} {rest rest' : List τ} (h : tokens left ++ rest = tokens right ++ rest') : left = right ∧ rest = rest'

A prefix round-trip determines the encoded value and every following token.

theorem Cslib.PrefixParser.parse_append {α : Type u_1} {τ : Type u_2} {readToken : τ → Option (Step α)} {tokens : α → List τ} (roundtrip : ∀ (value : α) (rest : List τ) (fuel : ℕ), (tokens value).length ≤ fuel → parseFuel readToken fuel (tokens value ++ rest) = some (value, rest)) (value : α) (rest : List τ) : parse readToken (tokens value ++ rest) = some (value, rest)

Parsing an encoded value leaves the supplied suffix unchanged.

theorem Cslib.PrefixParser.decode_tokens {α : Type u_1} {τ : Type u_2} {readToken : τ → Option (Step α)} {tokens : α → List τ} (roundtrip : ∀ (value : α) (rest : List τ) (fuel : ℕ), (tokens value).length ≤ fuel → parseFuel readToken fuel (tokens value ++ rest) = some (value, rest)) (value : α) : decode readToken (tokens value) = some value

A complete encoded value decodes to itself.