Claude/hopeful fermi i xnba - #107
Conversation
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
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
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
Two warnings-as-errors surfaced when compiling the echo/product additions
for the first time on a real OCaml toolchain:
compiler/lib/typecheck.ml — `strand_type_of_ty` had no arms for TProd/TEcho.
compiler/bin/main.ml — the debug token printer had no arms for the 8 new
echo keyword tokens (ECHOCLOSE LOWER RESIDUE PAIR
FST SND ECHOADD ECHOEQ).
Both are straightforward exhaustiveness gaps; the design is preserved.
Both get StrandDefault / print_string "<NAME>" mirroring the nearest
neighbouring cases.
Also extend the TG-4 round-trip corpus in test_roundtrip.ml with one entry
per new echo constructor (echoClose, lower, residue, pair, fst, snd, echoAdd,
echoEq) so the parse/pretty/parse round-trip guarantee is explicitly exercised
for every form added by this PR.
Before: dune build fails; 532 tests (not reached)
After: dune build succeeds; 548/548 tests pass (16 new TG-4 entries)
![gitar-bot[bot]](https://avatars.githubusercontent.com/in/827041?s=60&v=4){kind=small}
|
Note Automatic reviews are paused because your trial's included automatic processing has been used for this period. Upgrade now, or comment "Gitar review" to run a review anytime. Code Review ✅ Approved 2 resolved / 2 findingsIntegrates echo and product types into the OCaml typechecker, parser, and evaluator alongside TangleIR residue-threading contract documentation. Consider checking keyword shadowing for identifiers like lower and pair, and aligning the echoEq type rule with its evaluator operand support.
✅ 2 resolved✅ Quality: New reserved words shadow plausible user identifiers
✅ Quality: echoEq type rule omits Bool operands that eval supports
OptionsDisplay: compact → Showing less information. Comment with these commands to change the behavior for this request:
Was this helpful? React with 👍 / 👎 | Gitar |
|
|
Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com>
2 participants
Summary
Closes #
Type of change
How has this been verified?
Checklist
git commit -S).SPDX-License-Identifier(code/configMPL-2.0,prose
CC-BY-SA-4.0); I did not relicense existing files.Notes for reviewers
Summary by Gitar
docs/spec/ECHO-TANGLEIR-THREADING.mdThis will update automatically on new commits.