feat(jtv): the add{} injection island — Harvard data expressions (#94)

[hyperpolymath]

conformance/valid/v11_add_block.tangle was the last program the parser rejected — and the only one that wasn't a parse-rule gap. add{} is a sub-language, specified across 288 lines of FORMAL-SEMANTICS.md.

Not stale, unlike TangleIR. README-jtv.adoc documents it as deliberate design: "Computation is braiding… But sometimes, you need arithmetic." Two syntactically isolated islands give TANGLE data manipulation without polluting the topological core.

Semantic separation is the whole point

+ in TANGLE is connect-sum; + inside add{} is arithmetic. So the island gets its own grammar (hv_expr), its own type language (hv_ty), its own judgement (⊢_hd) and its own value space (hv_value) — sharing TANGLE's expr would have lost exactly the distinction the design exists to make.

Verified:

braid[s1] + braid[s2]	connect-sum
add{ 2 + 3 }	5
add{ braid[s1] }	does not parse — the island is closed

Results cross back through Embed (D2.4): Int/Float → Num, Bool → Bool, String → Str.

add is NOT reserved

My first attempt made add a keyword — which broke def add(a, b) = a . b, a valid TANGLE program that the e2e suite contains.

The spec's own first design principle points at the fix: "Delimited Syntax: add{...} cannot conflict with TANGLE operators." The delimiter is what prevents conflict, so add{ is lexed as a single ADDBRACE token. add alone stays an ordinary identifier — the token dump shows both in one file:

1:7   IDENT(add)      def add(a,b) = a . b
2:12  ADDBRACE        def z = add{ 1 }

Scope — stated, not implied

Implemented: the full operator hierarchy (+ - * / %, == != < <= > >=, && || !), the total conditional (both branches required, D2.1), and Int/Float/Bool/String literals. Guaranteed terminating: structural recursion on a finite term, no loops, no assignment, no side effects.

Not implemented, and not pretended — recorded in the source, not just here: rationals, complex, lists, tuples (§7.1); Hex/Binary/Symbolic types; variables in the Π environment and function calls (§8.2, §9.5); and the harvard{...} control block (§6.3) entirely.

The island is outside the mechanised core — ⊢_hd has no Lean image — so AddBlock joins the non-core constructors tg3_emit rejects outright, and the JEG lists T-Add-Block among its deferred rules rather than pretending to re-derive a judgement it doesn't implement.

Result

conformance 18/19 → 19/19. Both corpus manifest gap-lists are now empty: for the first time every valid program parses, typechecks and evaluates, and every invalid one is still rejected.

13 tests: precedence, conditional, logic, modulo, int-vs-float division, mixed promotion, division by zero, Embed — plus two negatives (arithmetic on a Bool; if-branches that disagree).

🤖 Generated with Claude Code

[gitar-bot]

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.
Learn more

Code Review ✅ Approved 2 resolved / 2 findings

Adds the add{} Harvard data expression sub-language to achieve full 19/19 test conformance, but float modulo crashes at runtime and equality checks on mixed numeric types always return false.

✅ 2 resolved

✅ Bug: Float modulo type-checks but crashes at runtime

📄 compiler/lib/typecheck.ml:216-225 📄 compiler/lib/eval.ml:338-342
infer_hv lumps HvMod in with the other arithmetic ops, so add{ 2.5 % 1.5 } (or any mixed/float operand) infers type Float and passes the type checker. But eval_hv's HvMod case only handles HvVInt/HvVInt and otherwise raises Eval_error "modulo requires integers". This breaks the stated soundness invariant ("the interpreter assumes the program has passed type-checking"): a well-typed program crashes at runtime, and it is not the sanctioned division-by-zero exception. Give HvMod its own case in infer_hv that requires Int, Int.

✅ Bug: add{} == on mixed Int/Float always returns false

📄 compiler/lib/eval.ml:347-348 📄 compiler/lib/typecheck.ml:232-239
infer_hv treats ==/!= as numeric across Int/Float, so add{ 2 == 2.0 } type-checks as Bool. But eval_hv implements them with raw OCaml structural equality (va = vb): HvVInt 2 = HvVFloat 2.0 is always false (different constructors), so 2 == 2.0 evaluates to false and 2 != 2.0 to true, contradicting the numeric-comparison semantics used by <, <=, etc. Promote numeric operands before comparing, e.g. by reusing cmp2 for the numeric case.

Options

Display: compact → Showing less information.

Comment with these commands to change the behavior for this request:

Compact

gitar display:verbose

_{Was this helpful? React with 👍 / 👎 | Gitar}