Skip to content

Commit 9e1ff79

Browse files
claudeclaude
committed
feat(echo): runtime eval + surface parser for echo/product forms
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
1 parent e021007 commit 9e1ff79

4 files changed

Lines changed: 101 additions & 7 deletions

File tree

‎compiler/lib/eval.ml‎

Lines changed: 68 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -42,6 +42,9 @@ type value =
4242
| VFun of string list * expr * env (** Closure: params, body, captured env *)
4343
| VUnit (** Unit / void result *)
4444
| VInvariant of string * string (** Invariant name, result string *)
45+
| VEcho of value * value (** Formed echo: residue, result —
46+
mirrors [echoVal] in proofs/Tangle.lean *)
47+
| VPair of value * value (** Product value *)
4548

4649
(** Runtime environment: association list of name-value bindings. *)
4750
and env = (string * value) list
@@ -77,7 +80,7 @@ let pp_braid (gens : gen list) : string =
7780
| _ -> "braid[" ^ String.concat ", " (List.map pp_gen gens) ^ "]"
7881

7982
(** Pretty-print a value. *)
80-
let pp_value (v : value) : string =
83+
let rec pp_value (v : value) : string =
8184
match v with
8285
| VInt n -> string_of_int n
8386
| VFloat f -> Printf.sprintf "%g" f
@@ -89,6 +92,10 @@ let pp_value (v : value) : string =
8992
| VFun _ -> "<function>"
9093
| VUnit -> "()"
9194
| VInvariant (name, result) -> Printf.sprintf "%s = %s" name result
95+
| VEcho (res, result) ->
96+
"echo(" ^ pp_value res ^ ", " ^ pp_value result ^ ")"
97+
| VPair (a, b) ->
98+
"(" ^ pp_value a ^ ", " ^ pp_value b ^ ")"
9299

93100
(* ================================================================== *)
94101
(* Environment operations *)
@@ -430,12 +437,66 @@ let rec eval_expr (env : env) (e : expr) : value =
430437
try_arms arms
431438

432439
(* ---- Echo types (structured loss) ----
433-
* These are typed by typecheck.ml (mirroring proofs/Tangle.lean). Runtime
434-
* evaluation needs echo/product value forms and is a deliberate follow-on;
435-
* the typechecker is the scoped deliverable. *)
436-
| EchoClose _ | Lower _ | Residue _ | Pair _ | Fst _ | Snd _ | EchoAdd _ | EchoEq _ ->
437-
eval_error "echo-type evaluation is not yet implemented (typecheck-only); \
438-
see proofs/Tangle.lean for the intended small-step semantics"
440+
* Mirror the small-step Step rules in proofs/Tangle.lean:
441+
* echoCloseWord : echoClose(braidLit gs) ⟶ echoVal (braidLit gs) identity
442+
* lowerVal : lower (echoVal r v) ⟶ v
443+
* residueVal : residue (echoVal r v) ⟶ r
444+
* fstPair : fst (pair a b) ⟶ a
445+
* sndPair : snd (pair a b) ⟶ b
446+
* echoAddNums : echoAdd (num a) (num b) ⟶ echoVal (pair a b) (num (a+b))
447+
* echoEqNums : echoEq a b ⟶ echoVal (pair a b) (boolLit (a==b))
448+
* The result component of a closure echo is the identity value (Word[0]),
449+
* matching the [closeId]/[closeWord] reduct used elsewhere in this file. *)
450+
451+
| EchoClose e1 ->
452+
(* echo-preserving closure: residue retains the witness; the result is the
453+
identity value (Word[0]), the same point the empty/identity close yields. *)
454+
let v = eval_expr env e1 in
455+
VEcho (v, VBraid [])
456+
457+
| Lower e1 ->
458+
begin match eval_expr env e1 with
459+
| VEcho (_, r) -> r
460+
| v -> eval_error "lower expects an echo value, got %s" (pp_value v)
461+
end
462+
463+
| Residue e1 ->
464+
begin match eval_expr env e1 with
465+
| VEcho (res, _) -> res
466+
| v -> eval_error "residue expects an echo value, got %s" (pp_value v)
467+
end
468+
469+
| Pair (e1, e2) ->
470+
(* Force left-to-right evaluation (Lean pairLeft reduces e1 first). *)
471+
let a = eval_expr env e1 in
472+
let b = eval_expr env e2 in
473+
VPair (a, b)
474+
475+
| Fst e1 ->
476+
begin match eval_expr env e1 with
477+
| VPair (a, _) -> a
478+
| v -> eval_error "fst expects a pair, got %s" (pp_value v)
479+
end
480+
481+
| Snd e1 ->
482+
begin match eval_expr env e1 with
483+
| VPair (_, b) -> b
484+
| v -> eval_error "snd expects a pair, got %s" (pp_value v)
485+
end
486+
487+
| EchoAdd (e1, e2) ->
488+
(* Residue = the summand pair; result = their sum (reuse the Add logic). *)
489+
let v1 = eval_expr env e1 in
490+
let v2 = eval_expr env e2 in
491+
let sum = eval_binop Add v1 v2 in
492+
VEcho (VPair (v1, v2), sum)
493+
494+
| EchoEq (e1, e2) ->
495+
(* Residue = the operand pair; result = their equality (reuse the Eq logic). *)
496+
let v1 = eval_expr env e1 in
497+
let v2 = eval_expr env e2 in
498+
let b = eval_binop Eq v1 v2 in
499+
VEcho (VPair (v1, v2), b)
439500

440501
(** Evaluate a binary operation on two values. *)
441502
and eval_binop (op : binop) (v1 : value) (v2 : value) : value =

‎compiler/lib/lexer.mll‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -45,6 +45,15 @@
4545
| "cap" -> CAP
4646
| "cup" -> CUP
4747
| "braid" -> BRAID
48+
(* Echo / product forms — surface syntax mirrors pretty.ml output. *)
49+
| "echoClose" -> ECHOCLOSE
50+
| "lower" -> LOWER
51+
| "residue" -> RESIDUE
52+
| "pair" -> PAIR
53+
| "fst" -> FST
54+
| "snd" -> SND
55+
| "echoAdd" -> ECHOADD
56+
| "echoEq" -> ECHOEQ
4857
| "jones" -> JONES
4958
| "alexander" -> ALEXANDER
5059
| "homfly" -> HOMFLY

‎compiler/lib/parser.mly‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,9 @@
3232
%token IDENTITY TRUE FALSE
3333
%token CLOSE MIRROR REVERSE SIMPLIFY CAP CUP BRAID
3434

35+
(* Echo / product forms — surface syntax mirrors pretty.ml output *)
36+
%token ECHOCLOSE LOWER RESIDUE PAIR FST SND ECHOADD ECHOEQ
37+
3538
(* Invariant names *)
3639
%token JONES ALEXANDER HOMFLY KAUFFMAN WRITHE LINKING
3740

@@ -263,6 +266,18 @@ unary_expr:
263266
{ Cap (e1, e2) }
264267
| CUP LPAREN e1 = expr COMMA e2 = expr RPAREN
265268
{ Cup (e1, e2) }
269+
(* ---- Echo / product forms (mirror pretty.ml output) ---- *)
270+
| ECHOCLOSE LPAREN e = expr RPAREN { EchoClose e }
271+
| LOWER LPAREN e = expr RPAREN { Lower e }
272+
| RESIDUE LPAREN e = expr RPAREN { Residue e }
273+
| FST LPAREN e = expr RPAREN { Fst e }
274+
| SND LPAREN e = expr RPAREN { Snd e }
275+
| PAIR LPAREN e1 = expr COMMA e2 = expr RPAREN
276+
{ Pair (e1, e2) }
277+
| ECHOADD LPAREN e1 = expr COMMA e2 = expr RPAREN
278+
{ EchoAdd (e1, e2) }
279+
| ECHOEQ LPAREN e1 = expr COMMA e2 = expr RPAREN
280+
{ EchoEq (e1, e2) }
266281
| t = twist_expr { t }
267282
| MINUS e = primary_expr { UnaryOp (Neg, e) }
268283
| e = primary_expr { e }

‎compiler/lib/token.ml‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -52,6 +52,15 @@ and token =
5252
| CAP
5353
| CUP
5454
| BRAID
55+
(* Echo / product forms *)
56+
| ECHOCLOSE
57+
| LOWER
58+
| RESIDUE
59+
| PAIR
60+
| FST
61+
| SND
62+
| ECHOADD
63+
| ECHOEQ
5564

5665
(* ---- Invariant names ---- *)
5766
| JONES

0 commit comments

Comments
 (0)