Parser for the Eidos concrete syntax (.eir; doc/eidos.md, section 9). ReWire.Eidos.Pretty is the other half of the round-trip contract: parse . pretty is the identity on programs modulo annotations, and pretty . parse . pretty == pretty is a tested fixpoint.

The concrete syntax does not carry a type for every binder occurrence, so (as in ReWire.Hyle.Parse) parsing is followed by an elaboration pass that reconstructs what the format leaves implicit:

• variable occurrences print bare (x#12) and receive their binder's Id (unique, occurrence text, and signature) from a scope map; an occurrence whose unique is not in scope is an error;
• the case binder prints bare and receives the scrutinee's synthesized type;
• join point labels print with no signature; a label's signature is reconstructed as arrows from its parameter types to its body's synthesized type (doc/eidos.md section 4.2).

Join point scoping, on the other hand, is resolved during parsing proper: a scope map of join binders (keyed by unique) is threaded through the expression grammar, Jump sites take their JoinId (in particular its arity) from the binding, and a jump to an unbound label is a parse-time error — labels are lexically scoped and never escape (section 3.4), so no forward references exist. Join points are not recursive: a label is not in scope in its own body.

Two lexical devices keep the grammar newline-insensitive:

• a name in expression-atom position followed by :: is not an atom (it starts the next definition's signature line) — the expression grammar itself has no bare ::;
• a occ#uniq token in type-atom position is a type variable only if its unique is bound by the enclosing signature's forall, so the equation name following a signature line never extends the signature's type. (Both rely on global binder uniqueness; a program that reuses a signature's type-variable unique as a term binder unique — ill-formed per section 2 — may misparse.)

The machine level's process declarations parse in ReWire.Synolon.Parse, which reuses this grammar and elaboration for the expressions, definitions, and datatypes a Synolon program embeds.