diff --git a/DECISIONS.md b/DECISIONS.md index fd42726..e032c5a 100644 --- a/DECISIONS.md +++ b/DECISIONS.md @@ -36,3 +36,5 @@ against the existing examples. - **Stage-1 exception: the imported interpreter's header comment was corrected in place** (`tested: 18/18` → the provable `10 tests in js/test/`) — a falsified claim inside the canonical artifact outranks byte identity with the pre-Stage-1 deploy; end-state identity is restored when the site deploys the pinned file. - **Stage-3 ratification (2026-07-09): the 26 judgment calls are ruled; JUDGMENT_CALLS.md is the semantic record of MPL M0.** Per-ruling record: (1) ÷0 is `err_div0`; (2) a `∀` expression is always `⊥`; (3) an unmatched guard yields `⊥` unless caught by `|`; (4) numbers are exact rationals — BigInt num/den, lowest terms, den > 0, decimal literals exact, display `n` or `n/d` (re-evaluates to itself); IEEE doubles rejected; (5) `✎` rendering spec'd per type; (6) `⊥` is first-class, arithmetic on it `err_num`; (7) equality is structural on data, cross-type `=` false, `0.5 = 1/2` true, any function in `=`/`≠` raises `err_fn_eq`; (8) ordering is number×number and string×string (code-point) only, else `err_compare`; (9) closures capture the environment; (10) λ-application depth counter, limit 10000, `err_depth` — no keyless host error may remain reachable; (11) the 500000-step budget is an environment resource limit, not semantics — corpus entry 053 moved to js/test; (12) string escapes are exactly `\n \t \" \\`, anything else `err_escape` (grammar ESC amended to match); (13) guard conditions must be boolean, else `err_bool`; (14) `∧ ∨` short-circuit and demand booleans on evaluated operands (`err_bool`); (15) braces group, binders scope; (16) `≜` binds once per scope (`err_redef`; inner shadowing legal), `←` mutates an existing binding only (`err_unbound`); (17) type constraints parse, unenforced; (18) nullary `λ: e` admitted (grammar amended); (19) `∗` ≡ `×`; (20) the empty program is valid; (21) `( seqExpr )` — the interpreter now implements it; (22) `∘` is composition, `(f ∘ g)(x…) = f(g(x…))`, non-function operand `err_notfn`; (23) set literals parse, evaluate to `err_notyet`; (24) record literals likewise; (25) `λ(a, b):` rejected everywhere; (26) `λ` is reserved — never an identifier — while other Greek letters remain identifiers. - **Standing M1 decisions logged at ratification**: `√` vs ℚ (irrationals); an explicit local-binding construct (let/where); set semantics; record semantics; comprehension notation; `‖` parallel semantics. +- **Grammar-only surface gaps are on the record** (SURFACE.md "Grammar-only surface" section): `≈`/`∼` comparisons, `"""raw strings"""`, hex/binary/exponent literals, and `_` as a λ pattern all parse in the grammar and fail in the Stage-3 interpreter — Stage 4+ material, no ruling; `err_comment` is dead pending removal at the next legitimate interpreter change. +- **Ruling 12's enumeration governs string escapes**: the grammar's ESC fragment was narrowed to exactly `\n \t \" \\` — `\r`, `\0` and `\u{hex}` were removed from the grammar; they were never in the ratified set. diff --git a/conformance/SURFACE.md b/conformance/SURFACE.md index 7c9c717..0b5fc6d 100644 --- a/conformance/SURFACE.md +++ b/conformance/SURFACE.md @@ -84,6 +84,26 @@ parser rule** — any use is `err_expect`. - Deep recursion overflows the host stack **before** the step budget — a keyless RangeError, unpinnable by the corpus (see JUDGMENT_CALLS). +## Grammar-only surface (no ruling, Stage 4+ material) + +The grammar accepts these; the Stage-3 interpreter does not. No ruling +covers them and the fuzzer's generator does not emit them — they are on +the record here so the gap is a listed fact, not a surprise: + +- `≈` (APPROX) and `∼` (SIM) comparison operators — interpreter: `err_char`. +- `"""raw strings"""` (RAWSTRING) — interpreter: `err_char` at the second + quote pair's content or `err_string`/`err_expect` depending on context. +- Hex (`0x1F`), binary (`0b101`) and exponent (`1.5e3`) number literals — + interpreter lexes the leading digits as a plain number and fails to + parse the rest (`err_expect`). +- `_` as a λ pattern (patternAtom UNDERSCORE) — interpreter: `err_char`. + +Dead key: `err_comment` can no longer be raised — since the comment lexer +matched the grammar (a `{-` without its `-}` is a brace, not an +unterminated comment), no code path produces it. It stays in the error-key +list pending removal at the next legitimate interpreter change (no hash +churn for hygiene alone). + ## Explicitly out of corpus scope - `‖` — parses, and the evaluator runs it as plain sequencing, but its