You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Split out of #88(B). conformance/valid/v11_add_block.tangle — def x = add{ 1 + 2 + 3 } — is the last program in the corpus the parser rejects, and it is the only one that is not a parse-rule gap.
add{ … } is a sub-language, specified across 288 lines and 12 sections of docs/spec/FORMAL-SEMANTICS.md (§6.1–§10).
What the spec requires
§6.2 — its own expression grammar (⊢_hd terms, not Tangle expressions):
he ::= n | "s" | true | false -- literals
| x -- variable (resolves in Π)
| he₁ op he₂ -- arithmetic, op ∈ {+,-,*,/}
| he₁ == he₂ -- equality
| he₁ && he₂ | he₁ || he₂ -- boolean operators
| !he -- negation
| f(he₁, …, heₖ) -- call (f must be in Π)
| if he₁ then he₂ else he₃ -- conditional, total (both branches)
Explicitly: "NO side effects, NO loops, NO assignments. Guaranteed terminating (D2.1)."
§7.1 — its own type system: Int, Float, Rational, Hex, Binary, Bool, String, Symbolic.
§7.2 — Embed / Unembed between Harvard and Tangle types (Embed(Int) = Num, Embed(Bool) = Bool, …), in both directions (§9.4).
§8 — extended environments: the Π environment (§8.2) with visibility rules (§8.1).
§9.3 — a separate typing judgement⊢_hd, distinct from HasType.
Note harvard{ hp } (the control block, §6.3) is specified alongside it and is a further, statement-level construct.
Why it needs to be its own piece of work
None of the above is reachable by adding a grammar production. It needs new AST, new tokens (if/then/else, &&, ||, !), a second typing judgement, a conversion layer, and an evaluator — and a decision about how much of it to build.
A partial implementation is worse than none here: shipping add{ 1 + 2 + 3 } alone would claim support for a construct whose spec promises conditionals, a distinct numeric tower, and cross-language calls. The corpus file would go green while the feature stayed absent — the exact fake-gate pattern #89 was built to prevent.
Suggested shape
Decide the scope first. Is the Harvard layer still wanted as specified? It predates the KRL de-conflation (docs: de-conflate Tangle from KRL; drop two dead Jekyll Pages workflows #78), and ECHO-TANGLEIR-THREADING.md is from the same era — worth confirming it is not similarly stale before building 288 lines of spec.
If yes: the arithmetic/boolean fragment + Embed is a coherent first rung, with if/then/else, Π visibility, and calling as later ones.
If no: correct the spec and remove v11_add_block from the conformance corpus rather than leaving a permanently-failing "valid" program.
Until then it is the single entry in scripts/check-corpus.sh's CONFORMANCE_KNOWN_UNPARSED, so it cannot be forgotten and cannot regress silently.
Split out of #88(B).
conformance/valid/v11_add_block.tangle—def x = add{ 1 + 2 + 3 }— is the last program in the corpus the parser rejects, and it is the only one that is not a parse-rule gap.add{ … }is a sub-language, specified across 288 lines and 12 sections ofdocs/spec/FORMAL-SEMANTICS.md(§6.1–§10).What the spec requires
§6.2 — its own expression grammar (
⊢_hdterms, not Tangle expressions):Explicitly: "NO side effects, NO loops, NO assignments. Guaranteed terminating (D2.1)."
§7.1 — its own type system:
Int,Float,Rational,Hex,Binary,Bool,String,Symbolic.§7.2 — Embed / Unembed between Harvard and Tangle types (
Embed(Int) = Num,Embed(Bool) = Bool, …), in both directions (§9.4).§8 — extended environments: the
Πenvironment (§8.2) with visibility rules (§8.1).§9.3 — a separate typing judgement
⊢_hd, distinct fromHasType.§9.5, §9.6 — Harvard calling Tangle (D2.9) and module imports (D2.6, D2.11).
§10 — extended operational semantics.
Note
harvard{ hp }(the control block, §6.3) is specified alongside it and is a further, statement-level construct.Why it needs to be its own piece of work
None of the above is reachable by adding a grammar production. It needs new AST, new tokens (
if/then/else,&&,||,!), a second typing judgement, a conversion layer, and an evaluator — and a decision about how much of it to build.A partial implementation is worse than none here: shipping
add{ 1 + 2 + 3 }alone would claim support for a construct whose spec promises conditionals, a distinct numeric tower, and cross-language calls. The corpus file would go green while the feature stayed absent — the exact fake-gate pattern #89 was built to prevent.Suggested shape
ECHO-TANGLEIR-THREADING.mdis from the same era — worth confirming it is not similarly stale before building 288 lines of spec.if/then/else,Πvisibility, and calling as later ones.v11_add_blockfrom the conformance corpus rather than leaving a permanently-failing "valid" program.Until then it is the single entry in
scripts/check-corpus.sh'sCONFORMANCE_KNOWN_UNPARSED, so it cannot be forgotten and cannot regress silently.