From 2f57d64322a5eee4b0dced3454ea5555cf0aaf70 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 14 Jun 2026 03:24:40 +0000 Subject: [PATCH 1/3] feat(echo): integrate echo + product types into the OCaml typechecker MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Mirrors the Lean spec (proofs/Tangle.lean) into the OCaml checker so echo types are a feature of the actual typechecker, not only the metatheory. - typecheck.ml: `ty` gains `TProd of ty*ty` and `TEcho of ty*ty`; `pp_ty` is now `let rec` and prints them; `infer_expr` gains the eight typing rules [T-Echo-Close]/[T-Lower]/[T-Residue]/[T-Pair]/[T-Fst]/[T-Snd]/[T-Echo-Add]/ [T-Echo-Eq], matching the HasType rules. - ast.ml: `expr` gains EchoClose/Lower/Residue/Pair/Fst/Snd/EchoAdd/EchoEq. - pretty.ml: pp_expr prints the new forms (kept exhaustive). - eval.ml: eval_expr gets an explicit "not yet implemented" arm for the echo forms (runtime evaluation is a scoped follow-on; the typechecker is the deliverable). Stays exhaustive. Scope: the typechecker. Surface parser syntax + runtime eval are follow-ons. NOTE: no OCaml toolchain or OCaml CI exists in this environment, so this was NOT compiled here — it is a careful by-hand integration (exhaustiveness audited via the Ast-only `Twist` probe: pretty/eval/typecheck are the only exhaustive Ast.expr matchers; compositional's of_ast_expr has a catch-all; repl matches no expr). Verify with `dune build` in compiler/. https://claude.ai/code/session_01PgHpCFzwYB7Qy9L6kmR8CE --- compiler/lib/ast.ml | 12 +++++++ compiler/lib/eval.ml | 8 +++++ compiler/lib/pretty.ml | 46 +++++++++++++++++++++++++++ compiler/lib/typecheck.ml | 67 ++++++++++++++++++++++++++++++++++++++- 4 files changed, 132 insertions(+), 1 deletion(-) diff --git a/compiler/lib/ast.ml b/compiler/lib/ast.ml index c272c78..0221e3a 100644 --- a/compiler/lib/ast.ml +++ b/compiler/lib/ast.ml @@ -80,6 +80,18 @@ and expr = | Cup of expr * expr | Twist of expr + (* ---- Echo types (structured loss) — mirror the Lean spec in + * proofs/Tangle.lean (Ty.echo / Ty.prod and the echo operations). + * Typed by typecheck.ml; surface parser syntax is a follow-on. ---- *) + | EchoClose of expr (* echo-preserving closure (residue-retaining close) *) + | Lower of expr (* project an echo to its result *) + | Residue of expr (* project an echo to its residue (recover witness) *) + | Pair of expr * expr (* product introduction *) + | Fst of expr (* first projection *) + | Snd of expr (* second projection *) + | EchoAdd of expr * expr (* echo-preserving addition (residue = summand pair) *) + | EchoEq of expr * expr (* echo-preserving equality (residue = operand pair) *) + (* ---- Literals ---- *) | BraidLit of generator list | Identity diff --git a/compiler/lib/eval.ml b/compiler/lib/eval.ml index ee2ed9f..fb5bb08 100644 --- a/compiler/lib/eval.ml +++ b/compiler/lib/eval.ml @@ -429,6 +429,14 @@ let rec eval_expr (env : env) (e : expr) : value = in try_arms arms + (* ---- Echo types (structured loss) ---- + * These are typed by typecheck.ml (mirroring proofs/Tangle.lean). Runtime + * evaluation needs echo/product value forms and is a deliberate follow-on; + * the typechecker is the scoped deliverable. *) + | EchoClose _ | Lower _ | Residue _ | Pair _ | Fst _ | Snd _ | EchoAdd _ | EchoEq _ -> + eval_error "echo-type evaluation is not yet implemented (typecheck-only); \ + see proofs/Tangle.lean for the intended small-step semantics" + (** Evaluate a binary operation on two values. *) and eval_binop (op : binop) (v1 : value) (v2 : value) : value = match op with diff --git a/compiler/lib/pretty.ml b/compiler/lib/pretty.ml index bcedb75..c96db47 100644 --- a/compiler/lib/pretty.ml +++ b/compiler/lib/pretty.ml @@ -171,6 +171,52 @@ let rec pp_expr ctx = function pp_expr ctx e; emit ctx ")" + | EchoClose e -> + emit ctx "echoClose("; + pp_expr ctx e; + emit ctx ")" + + | Lower e -> + emit ctx "lower("; + pp_expr ctx e; + emit ctx ")" + + | Residue e -> + emit ctx "residue("; + pp_expr ctx e; + emit ctx ")" + + | Pair (e1, e2) -> + emit ctx "pair("; + pp_expr ctx e1; + emit ctx ", "; + pp_expr ctx e2; + emit ctx ")" + + | Fst e -> + emit ctx "fst("; + pp_expr ctx e; + emit ctx ")" + + | Snd e -> + emit ctx "snd("; + pp_expr ctx e; + emit ctx ")" + + | EchoAdd (e1, e2) -> + emit ctx "echoAdd("; + pp_expr ctx e1; + emit ctx ", "; + pp_expr ctx e2; + emit ctx ")" + + | EchoEq (e1, e2) -> + emit ctx "echoEq("; + pp_expr ctx e1; + emit ctx ", "; + pp_expr ctx e2; + emit ctx ")" + | BraidLit gens -> emit ctx "braid["; List.iteri (fun i g -> diff --git a/compiler/lib/typecheck.ml b/compiler/lib/typecheck.ml index 74dd58e..204d7d7 100644 --- a/compiler/lib/typecheck.ml +++ b/compiler/lib/typecheck.ml @@ -41,6 +41,9 @@ type ty = | TNum (** Num — integers and floats *) | TBool (** Bool — booleans *) | TStr (** Str — strings *) + | TProd of ty * ty (** ρ × σ — product / residue carrier for lossy ops *) + | TEcho of ty * ty (** Echo[ρ, τ] — structured loss: residue ρ, result τ. + Mirrors Ty.echo in proofs/Tangle.lean. *) (** Function signature: (param_types) -> return_type. *) type fun_sig = { @@ -89,12 +92,14 @@ let pp_boundary (b : boundary) : string = "[" ^ String.concat ", " (List.map pp_strand_type b) ^ "]" (** Pretty-print a type. *) -let pp_ty = function +let rec pp_ty = function | TWord n -> Printf.sprintf "Word[%d]" n | TTangle (a, b) -> Printf.sprintf "Tangle[%s, %s]" (pp_boundary a) (pp_boundary b) | TNum -> "Num" | TBool -> "Bool" | TStr -> "Str" + | TProd (a, b) -> Printf.sprintf "(%s * %s)" (pp_ty a) (pp_ty b) + | TEcho (r, t) -> Printf.sprintf "Echo[%s, %s]" (pp_ty r) (pp_ty t) (* ================================================================== *) (* Environment operations *) @@ -373,6 +378,66 @@ let rec infer_expr (gamma : env) (sigma : strand_ctx) (e : expr) : ty = ) arm_types; result_ty + (* ---- Echo types (structured loss) ---- + * Mirror the HasType rules in proofs/Tangle.lean: + * [T-Echo-Close] echoClose e : Echo[Word[n], Word[0]] when e : Word[n] + * [T-Lower] lower e : τ when e : Echo[ρ, τ] + * [T-Residue] residue e : ρ when e : Echo[ρ, τ] + * [T-Pair]/[T-Fst]/[T-Snd] product intro + projections + * [T-Echo-Add] echoAdd a b : Echo[Num × Num, Num] + * [T-Echo-Eq] echoEq a b : Echo[ρ × ρ, Bool] for ρ ∈ {Num, Str, Word[n]} + *) + | EchoClose e1 -> + begin match infer_expr gamma sigma e1 with + | TWord n -> TEcho (TWord n, TWord 0) + | t -> type_error "echoClose requires Word[n], got %s" (pp_ty t) + end + + | Lower e1 -> + begin match infer_expr gamma sigma e1 with + | TEcho (_, t) -> t + | t -> type_error "lower requires Echo[_, _], got %s" (pp_ty t) + end + + | Residue e1 -> + begin match infer_expr gamma sigma e1 with + | TEcho (r, _) -> r + | t -> type_error "residue requires Echo[_, _], got %s" (pp_ty t) + end + + | Pair (e1, e2) -> + let t1 = infer_expr gamma sigma e1 in + let t2 = infer_expr gamma sigma e2 in + TProd (t1, t2) + + | Fst e1 -> + begin match infer_expr gamma sigma e1 with + | TProd (a, _) -> a + | t -> type_error "fst requires a product, got %s" (pp_ty t) + end + + | Snd e1 -> + begin match infer_expr gamma sigma e1 with + | TProd (_, b) -> b + | t -> type_error "snd requires a product, got %s" (pp_ty t) + end + + | EchoAdd (e1, e2) -> + begin match infer_expr gamma sigma e1, infer_expr gamma sigma e2 with + | TNum, TNum -> TEcho (TProd (TNum, TNum), TNum) + | t1, t2 -> type_error "echoAdd requires Num, Num, got %s, %s" (pp_ty t1) (pp_ty t2) + end + + | EchoEq (e1, e2) -> + begin match infer_expr gamma sigma e1, infer_expr gamma sigma e2 with + | TNum, TNum -> TEcho (TProd (TNum, TNum), TBool) + | TStr, TStr -> TEcho (TProd (TStr, TStr), TBool) + | TWord n, TWord m when n = m -> TEcho (TProd (TWord n, TWord n), TBool) + | t1, t2 -> + type_error "echoEq requires matching Num/Str/Word[n] operands, got %s, %s" + (pp_ty t1) (pp_ty t2) + end + (** Infer the type of a binary operation given operand types. * Implements rules from sections 3.4, 3.5, 3.6. *) From e021007bc94853c49a18e3ad4eefc29f10ab0485 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 14 Jun 2026 03:33:08 +0000 Subject: [PATCH 2/3] docs(echo): TangleIR residue-threading cross-repo contract Specifies how echoClose's residue (the pre-closure braid) threads through TangleIR to QuandleDB's quandle_presentation. TangleIR itself lives in KRLAdapter.jl (Julia, out of scope), so this is the coordination contract from the semantics owner (tangle), not an IR code change. https://claude.ai/code/session_01PgHpCFzwYB7Qy9L6kmR8CE --- docs/spec/ECHO-TANGLEIR-THREADING.md | 90 ++++++++++++++++++++++++++++ 1 file changed, 90 insertions(+) create mode 100644 docs/spec/ECHO-TANGLEIR-THREADING.md diff --git a/docs/spec/ECHO-TANGLEIR-THREADING.md b/docs/spec/ECHO-TANGLEIR-THREADING.md new file mode 100644 index 0000000..8127db0 --- /dev/null +++ b/docs/spec/ECHO-TANGLEIR-THREADING.md @@ -0,0 +1,90 @@ + +# Echo residue threading into TangleIR — cross-repo contract + +**Status:** design / coordination contract (2026-06-14). Authored in `tangle` +(the semantics owner). The TangleIR type change and the QuandleDB consumer +change live in **`KRLAdapter.jl`** (TangleIR definition + adapters) and +**`quandledb`** — both Julia, outside this session's scope — so this file is +the *contract* those repos implement, not the implementation. + +## 1. Why threading the residue matters + +Tangle's `close : Word[n] → Word[0]` is the canonical **lossy** map: it +collapses a braid to the identity, discarding the word. Echo types +(`proofs/Tangle.lean` §ECHO-TYPES; `compiler/lib/typecheck.ml`) make that loss +recoverable — `echoClose b` retains the braid as a **residue**, and +`residue (echoClose b) ⟶ b` (`echo_residue_recovers`). + +The seam with QuandleDB is exact, not incidental: + +> A **quandle presentation is an invariant of the knot**, and the knot is the +> **closure of the braid**. `close` is precisely the braid→knot step. So the +> residue retained by `echoClose` — the *pre-closure braid* — is exactly the +> object `quandle_presentation(ir::TangleIR)::QuandlePresentation` derives the +> quandle from. + +`echo_distinguishes_collapsed` (Lean) says distinct braids can close to the +same diagram while keeping distinct residues. Threading the residue therefore +gives QuandleDB **provenance**: which braid produced a given closed diagram, +disambiguating cases that plain `close` would conflate. + +## 2. The contract per layer + +| Layer | Repo | Responsibility | +|---|---|---| +| Semantics | `tangle` (this repo) | Defines echo types + residue semantics. `residue (echoClose b) = b`; `lower (echoClose b) = identity`. Mechanised in `proofs/Tangle.lean`; checked in `typecheck.ml` (`TEcho`/`TProd`, rules `[T-Echo-Close]`/`[T-Lower]`/`[T-Residue]`). | +| Interchange | `KRLAdapter.jl` | TangleIR represents an echo-closed term **carrying the residue braid alongside the closed result** (see §3). A plain `close` node is unchanged (no residue). | +| Consumer | `quandledb` | `quandle_presentation` reads the residue braid of an echo-closed node to compute the quandle (the pre-closure braid determines the knot). Plain-`close` behaviour unchanged. | + +## 3. Proposed TangleIR representation (for KRLAdapter.jl) + +Mirror the Lean `echoVal (residue, result)` shape. Two equivalent options; +recommend (a): + +* **(a) Residue-carrying closure node.** Add an IR node + `EchoClosed(residue::BraidWord, result::ClosedDiagram)` — the closed diagram + plus the braid it came from. `lower`/`residue` IR projections read `.result` + / `.residue`. This keeps the closed diagram identical to the plain-`close` + output (so existing consumers are unaffected) while exposing the braid. +* **(b) Residue as closure metadata.** Keep the existing closure node and attach + the pre-closure braid as an optional metadata field + (`residue::Union{BraidWord,Nothing}`). Lighter, but makes the residue + optional rather than type-guaranteed — weaker than the Lean guarantee. + +Products (`Ty.prod` / `pair`/`fst`/`snd`) are the residue carrier for the +binary lossy ops (`echoAdd`/`echoEq`): their residue is the **pair of operands**. +If TangleIR needs to represent those, add a `Pair(a, b)` IR node with `fst`/`snd` +projections. (For QuandleDB specifically, only the `echoClose` residue is +knot-relevant; `echoAdd`/`echoEq` residues are scalar provenance.) + +## 4. Consumer contract (for quandledb) + +``` +quandle_presentation(ir::TangleIR) = + case ir of + EchoClosed(residue, _result) -> quandle_of_braid(residue) # use the braid + Close(diagram) -> quandle_of_diagram(diagram) # unchanged + ... +``` + +The invariant to preserve: for any braid `b`, +`quandle_presentation(EchoClosed(b, close(b)))` ≡ +`quandle_presentation(Close(close(b)))` whenever the closed diagram alone +suffices — the residue path must agree with the diagram path on the quandle, +and additionally retains `b` for provenance. This mirrors +`echo_roundtrip_typed` (the residue/result projections are well-typed) and the +`lower`/`residue` agreement in the Lean model. + +## 5. Scope / coordination + +- **No TangleIR or QuandleDB code is changed by this document.** Those are + KRLAdapter.jl/quandledb (Julia) changes, to be made by the quandle session. +- This contract is additive and conservative: plain `close` is untouched, so + existing TangleIR producers/consumers keep working; echo-closed nodes are new. +- Cross-reference: `proofs/Tangle.lean` (`echo_residue_recovers`, + `echo_distinguishes_collapsed`, `echo_roundtrip_typed`), + `.machine_readable/6a2/ECOSYSTEM.a2ml` (the echo↔quandle seam), + and `quandledb`'s `quandle_presentation`. From 9e1ff792fb615d58363b5ef1efca538986f86103 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 14 Jun 2026 03:35:27 +0000 Subject: [PATCH 3/3] feat(echo): runtime eval + surface parser for echo/product forms MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Implements the two follow-ons to the echo typechecker integration: PART 1 — eval.ml runtime evaluation - Add value forms VEcho (residue, result) and VPair (a, b), mirroring echoVal / pair in proofs/Tangle.lean. - Replace the not-yet-implemented stub arm with real eval_expr arms for EchoClose / Lower / Residue / Pair / Fst / Snd / EchoAdd / EchoEq, following the Lean small-step Step rules (echoCloseWord, lowerVal, residueVal, fstPair, sndPair, echoAddNums, echoEqNums). echoAdd/echoEq reuse eval_binop Add / Eq for the result component. - Extend pp_value (now recursive) with echo(...) / (...) rendering. PART 2 — lexer.mll + parser.mly surface syntax - Add dedicated keyword tokens ECHOCLOSE/LOWER/RESIDUE/PAIR/FST/SND/ ECHOADD/ECHOEQ (lexer keyword table + parser %token + token.ml mirror), following the existing close/mirror/cap/cup mechanism. - Add unary_expr productions in the same precedence group as close/cap, so pretty.ml output round-trips: echoClose(E), lower(E), residue(E), pair(E,E), fst(E), snd(E), echoAdd(E,E), echoEq(E,E). https://claude.ai/code/session_01PgHpCFzwYB7Qy9L6kmR8CE --- compiler/lib/eval.ml | 75 +++++++++++++++++++++++++++++++++++++---- compiler/lib/lexer.mll | 9 +++++ compiler/lib/parser.mly | 15 +++++++++ compiler/lib/token.ml | 9 +++++ 4 files changed, 101 insertions(+), 7 deletions(-) diff --git a/compiler/lib/eval.ml b/compiler/lib/eval.ml index fb5bb08..dc742a8 100644 --- a/compiler/lib/eval.ml +++ b/compiler/lib/eval.ml @@ -42,6 +42,9 @@ type value = | VFun of string list * expr * env (** Closure: params, body, captured env *) | VUnit (** Unit / void result *) | VInvariant of string * string (** Invariant name, result string *) + | VEcho of value * value (** Formed echo: residue, result — + mirrors [echoVal] in proofs/Tangle.lean *) + | VPair of value * value (** Product value *) (** Runtime environment: association list of name-value bindings. *) and env = (string * value) list @@ -77,7 +80,7 @@ let pp_braid (gens : gen list) : string = | _ -> "braid[" ^ String.concat ", " (List.map pp_gen gens) ^ "]" (** Pretty-print a value. *) -let pp_value (v : value) : string = +let rec pp_value (v : value) : string = match v with | VInt n -> string_of_int n | VFloat f -> Printf.sprintf "%g" f @@ -89,6 +92,10 @@ let pp_value (v : value) : string = | VFun _ -> "" | VUnit -> "()" | VInvariant (name, result) -> Printf.sprintf "%s = %s" name result + | VEcho (res, result) -> + "echo(" ^ pp_value res ^ ", " ^ pp_value result ^ ")" + | VPair (a, b) -> + "(" ^ pp_value a ^ ", " ^ pp_value b ^ ")" (* ================================================================== *) (* Environment operations *) @@ -430,12 +437,66 @@ let rec eval_expr (env : env) (e : expr) : value = try_arms arms (* ---- Echo types (structured loss) ---- - * These are typed by typecheck.ml (mirroring proofs/Tangle.lean). Runtime - * evaluation needs echo/product value forms and is a deliberate follow-on; - * the typechecker is the scoped deliverable. *) - | EchoClose _ | Lower _ | Residue _ | Pair _ | Fst _ | Snd _ | EchoAdd _ | EchoEq _ -> - eval_error "echo-type evaluation is not yet implemented (typecheck-only); \ - see proofs/Tangle.lean for the intended small-step semantics" + * Mirror the small-step Step rules in proofs/Tangle.lean: + * echoCloseWord : echoClose(braidLit gs) ⟶ echoVal (braidLit gs) identity + * lowerVal : lower (echoVal r v) ⟶ v + * residueVal : residue (echoVal r v) ⟶ r + * fstPair : fst (pair a b) ⟶ a + * sndPair : snd (pair a b) ⟶ b + * echoAddNums : echoAdd (num a) (num b) ⟶ echoVal (pair a b) (num (a+b)) + * echoEqNums : echoEq a b ⟶ echoVal (pair a b) (boolLit (a==b)) + * The result component of a closure echo is the identity value (Word[0]), + * matching the [closeId]/[closeWord] reduct used elsewhere in this file. *) + + | EchoClose e1 -> + (* echo-preserving closure: residue retains the witness; the result is the + identity value (Word[0]), the same point the empty/identity close yields. *) + let v = eval_expr env e1 in + VEcho (v, VBraid []) + + | Lower e1 -> + begin match eval_expr env e1 with + | VEcho (_, r) -> r + | v -> eval_error "lower expects an echo value, got %s" (pp_value v) + end + + | Residue e1 -> + begin match eval_expr env e1 with + | VEcho (res, _) -> res + | v -> eval_error "residue expects an echo value, got %s" (pp_value v) + end + + | Pair (e1, e2) -> + (* Force left-to-right evaluation (Lean pairLeft reduces e1 first). *) + let a = eval_expr env e1 in + let b = eval_expr env e2 in + VPair (a, b) + + | Fst e1 -> + begin match eval_expr env e1 with + | VPair (a, _) -> a + | v -> eval_error "fst expects a pair, got %s" (pp_value v) + end + + | Snd e1 -> + begin match eval_expr env e1 with + | VPair (_, b) -> b + | v -> eval_error "snd expects a pair, got %s" (pp_value v) + end + + | EchoAdd (e1, e2) -> + (* Residue = the summand pair; result = their sum (reuse the Add logic). *) + let v1 = eval_expr env e1 in + let v2 = eval_expr env e2 in + let sum = eval_binop Add v1 v2 in + VEcho (VPair (v1, v2), sum) + + | EchoEq (e1, e2) -> + (* Residue = the operand pair; result = their equality (reuse the Eq logic). *) + let v1 = eval_expr env e1 in + let v2 = eval_expr env e2 in + let b = eval_binop Eq v1 v2 in + VEcho (VPair (v1, v2), b) (** Evaluate a binary operation on two values. *) and eval_binop (op : binop) (v1 : value) (v2 : value) : value = diff --git a/compiler/lib/lexer.mll b/compiler/lib/lexer.mll index 5d97efd..4064104 100644 --- a/compiler/lib/lexer.mll +++ b/compiler/lib/lexer.mll @@ -45,6 +45,15 @@ | "cap" -> CAP | "cup" -> CUP | "braid" -> BRAID + (* Echo / product forms — surface syntax mirrors pretty.ml output. *) + | "echoClose" -> ECHOCLOSE + | "lower" -> LOWER + | "residue" -> RESIDUE + | "pair" -> PAIR + | "fst" -> FST + | "snd" -> SND + | "echoAdd" -> ECHOADD + | "echoEq" -> ECHOEQ | "jones" -> JONES | "alexander" -> ALEXANDER | "homfly" -> HOMFLY diff --git a/compiler/lib/parser.mly b/compiler/lib/parser.mly index 20353bd..526c1a9 100644 --- a/compiler/lib/parser.mly +++ b/compiler/lib/parser.mly @@ -32,6 +32,9 @@ %token IDENTITY TRUE FALSE %token CLOSE MIRROR REVERSE SIMPLIFY CAP CUP BRAID +(* Echo / product forms — surface syntax mirrors pretty.ml output *) +%token ECHOCLOSE LOWER RESIDUE PAIR FST SND ECHOADD ECHOEQ + (* Invariant names *) %token JONES ALEXANDER HOMFLY KAUFFMAN WRITHE LINKING @@ -263,6 +266,18 @@ unary_expr: { Cap (e1, e2) } | CUP LPAREN e1 = expr COMMA e2 = expr RPAREN { Cup (e1, e2) } + (* ---- Echo / product forms (mirror pretty.ml output) ---- *) + | ECHOCLOSE LPAREN e = expr RPAREN { EchoClose e } + | LOWER LPAREN e = expr RPAREN { Lower e } + | RESIDUE LPAREN e = expr RPAREN { Residue e } + | FST LPAREN e = expr RPAREN { Fst e } + | SND LPAREN e = expr RPAREN { Snd e } + | PAIR LPAREN e1 = expr COMMA e2 = expr RPAREN + { Pair (e1, e2) } + | ECHOADD LPAREN e1 = expr COMMA e2 = expr RPAREN + { EchoAdd (e1, e2) } + | ECHOEQ LPAREN e1 = expr COMMA e2 = expr RPAREN + { EchoEq (e1, e2) } | t = twist_expr { t } | MINUS e = primary_expr { UnaryOp (Neg, e) } | e = primary_expr { e } diff --git a/compiler/lib/token.ml b/compiler/lib/token.ml index a5d7820..4b0cb35 100644 --- a/compiler/lib/token.ml +++ b/compiler/lib/token.ml @@ -52,6 +52,15 @@ and token = | CAP | CUP | BRAID + (* Echo / product forms *) + | ECHOCLOSE + | LOWER + | RESIDUE + | PAIR + | FST + | SND + | ECHOADD + | ECHOEQ (* ---- Invariant names ---- *) | JONES