Module parse_emit_lens 

The parse / emit pair as a verified asymmetric lens with explicit law-checkers (retraction in the image of the parser). The parse / emit pair as a verified asymmetric lens.

parse and emit_pretty together form an asymmetric lens between a source-byte object B and a schema-object S(p) in the image of parse_p:

    parse_p :  B  ─▶  (S(p), C)         get-direction (with complement)
    emit_p  :  S(p) ─▶ B                put-direction (drops complement)

The complement C carries everything the schema doesn’t fix: byte positions, interstitial whitespace, comments. emit_pretty reconstitutes a canonical element of parse_p^{-1}(s) using a whitespace policy in place of the discarded complement.

In categorical terms this is a retraction in the image of the parser: for every s ∈ image(parse_p), the round-trip parse_p ∘ emit_p returns a schema with the same vertex/edge kind multiset as s. We don’t get pointwise equality because byte positions and interstitial constraints are not part of the emit_pretty image; that’s the price of a canonical section.

The law-checkers in this module verify the retraction explicitly so that any future change to emit_pretty is provably faithful.

Laws

EmitParse (the retraction law)

For all s in the image of parse_p,

    kind_multiset(parse_p(emit_p(s))) = kind_multiset(s')

where s' is s with the byte-position constraints stripped (the portion that emit_pretty cannot preserve by construction).

ParseEmit (stability under round-trip)

For all b such that parse_p(b) succeeds,

    parse_p(emit_p(strip(parse_p(b)))) ≅_kinds strip(parse_p(b))

That is, the emit_pretty image is a fixed point of the round-trip up to kind-multiset equivalence.

Structs

ParseEmitLens

A protolens for the source-bytes ↔ schema relation at one protocol.

Enums

LawViolation

Possible failures when verifying the parse/emit lens laws.

Functions

check_emit_parse

Verify the EmitParse law on a given schema:

check_parse_emit

Verify the ParseEmit stability law on a source byte string:

edge_multiset

Edge-shape multiset re-exported from panproto_schema::edge_multiset. See that module for the rationale on multiset granularity.

kind_multiset

Vertex-kind multiset re-exported from panproto_schema::kind_multiset.

strip_complement

Strip byte-position constraints from a schema.