Std.Data.Suffix

View source →

A proof that rem is a suffix of orig, indexed by whether at least one element was consumed. This is the foundation of total lexers and parsers: recursive drivers may descend only after receiving a Consumed(..., True, ...) witness.

The indices are compile-time information. Runtime parsers carry their remainder directly; later slices erase/compact the witness while retaining the kernel-checked strictness relationship.

Functions

# fn drop(a: Type, strict: Bool, rem: List(a), orig: List(a), head: a, proof: Consumed(a, strict, rem, orig)) -> Consumed(a, True, rem, Cons(head, orig))

Extend a suffix proof across one discarded head. Regardless of the inner proof's strictness, the result is now known to have consumed input.
# fn same(a: Type, xs: List(a)) -> Consumed(a, False, xs, xs)

Reflexivity: consuming nothing leaves the original input unchanged.
# fn trans(a: Type, left: Bool, right: Bool, orig: List(a), mid: List(a), rem: List(a), first: Consumed(a, left, mid, orig), second: Consumed(a, right, rem, mid)) -> Consumed(a, `or`(left, right), rem, orig)

Transitivity. Sequencing two consumers is strict when either consumer is strict. The escaped or is an ordinary imported type-level function.

Functions

# fn drop(a: Type, strict: Bool, rem: List(a), orig: List(a), head: a, proof: Consumed(a, strict, rem, orig)) -> Consumed(a, True, rem, Cons(head, orig))

# fn same(a: Type, xs: List(a)) -> Consumed(a, False, xs, xs)

# fn trans(a: Type, left: Bool, right: Bool, orig: List(a), mid: List(a), rem: List(a), first: Consumed(a, left, mid, orig), second: Consumed(a, right, rem, mid)) -> Consumed(a, `or`(left, right), rem, orig)