feat(echo): echo types through the OCaml pipeline (typecheck + eval + parser) + TangleIR contract#45
Merged
Merged
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
hyperpolymath
changed the title
3 tasks
hyperpolymath
added a commit
that referenced
this pull request
Jun 14, 2026
…(PRs #45–46) - CHANGELOG.md: add echo OCaml pipeline block; fixed exhaustiveness bullets - PROOF-NEEDS.md: TG-4 → LANDED; update rule counts (16→26 HasType, 31→57 Step); TG-10 coverage expanded to include echoAdd/echoEq/product - PROOF-NARRATIVE.md: update HasType/Step rule lists; add §2.6 OCaml completeness table; add product/echoAdd/echoEq rows to §2.5 table; TG-4 → LANDED - FEATURE-COVERAGE.md: add 9 echo/product rows; update coverage summary (27→36); date bump - FORMAL-SEMANTICS.md: extend §1.2 BNF; add §1.5 extended types; add §3.16 echo/product typing rules; add §4.10 echo/product eval rules; renumber downstream sections - STATE.a2ml: update session/last-updated/milestones/blockers/next-actions/maintenance-status - tangle.directives.a2ml: date bump to 2026-06-14 - docs/echo-types-ocaml-pipeline.md: new developer wiki page for echo/product integration Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Brings echo types (and the product type) from the Lean spec (
proofs/Tangle.lean, merged) into the OCaml implementation pipeline, plus the cross-repo IR contract.2f57d64— typechecker (typecheck.ml)tygainsTProd/TEcho;pp_tymaderec;infer_exprgains the eight rules[T-Echo-Close]/[T-Lower]/[T-Residue]/[T-Pair]/[T-Fst]/[T-Snd]/[T-Echo-Add]/[T-Echo-Eq], mirroringHasType. AST (ast.ml) gains the eightexprforms;pretty.mlprints them.9e1ff79— runtime eval + surface parsereval.ml:valuegainsVEcho/VPair;eval_exprevaluates all eight forms (mirroring the Lean small-step reducts —echoClose b ↦ VEcho(b, identity),lower/residueproject,echoAdd/echoEqreuse the existing Add/Eq logic and wrap the operand pair as residue). Exhaustiveness audited across everyvaluematch.lexer.mll+parser.mly+token.ml: dedicated tokens + productions (mirroringclose/cap), so the surface syntax round-trips withpretty.ml(echoClose(e),pair(a, b), …).e021007— TangleIR threading contract (docs/spec/ECHO-TANGLEIR-THREADING.md)TangleIR lives in
KRLAdapter.jl(Julia, out of scope), so this is the contract from the semantics owner:echoClose's residue is the pre-closure braid, which is exactly what QuandleDB'squandle_presentationderives the quandle from. Specifies the IR node shape (EchoClosed(residue, result)), the consumer rule, and the conservativity invariant — for the quandle session to implement.dune build compiler/No OCaml/menhir toolchain or OCaml CI in the build environment, so none of this was compiled. It's a careful by-hand integration with a documented self-review (eval exhaustiveness audited; parser productions isomorphic to the conflict-free
close/caprules;pp_ty/pp_valuemaderec). The real gate is your localdune build— watch for menhir conflict warnings. One deliberate breaking change:pair/fst/snd/lower/residue/echoClose/echoAdd/echoEqare now reserved words (corpus grep found no real collisions).🤖 Generated with Claude Code