Skip to content

Implement the Harvard data sub-language: add{ ... } blocks #94

Description

@hyperpolymath

Split out of #88(B). conformance/valid/v11_add_block.tangledef 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.

§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

  1. 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.
  2. If yes: the arithmetic/boolean fragment + Embed is a coherent first rung, with if/then/else, Π visibility, and calling as later ones.
  3. 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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions