Add coverage corpus

This commit is contained in:
developtheweb 2026-07-09 18:44:33 -04:00
parent 6f1db6de95
commit 42ade676db
193 changed files with 511 additions and 0 deletions

91
conformance/SURFACE.md Normal file
View file

@ -0,0 +1,91 @@
# SURFACE — what `js/mpl.js` actually implements
Audited from the source of `js/mpl.js` (Stage 2, C3) and pinned by the
corpus. This file describes the implemented surface — exactly, no more.
Nothing here is ratified; where behavior looks accidental it is flagged in
`conformance/JUDGMENT_CALLS.md`, but it is recorded as observed.
## Lexer
- Whitespace: space, tab, CR, LF.
- Comments: line `-- …`; block `{- … -}`, nesting tracked (unterminated →
`err_comment`).
- Strings: `"…"`, escape `\n` → newline, `\t` → tab, any other `\x``x`
(the backslash is silently dropped — `\q` becomes `q`); unterminated →
`err_string`.
- ASCII escapes: `\word` for word ∈ {lambda, forall, in, coloneq,
leftarrow, implies, and, or, neq, leq, geq, times, div, trace, bot,
parallel, circ, ast}; unknown word → `err_escape`.
- Numbers: `[0-9]+(.[0-9]+)?` via `parseFloat` (all numbers are JS
doubles; no scientific notation, no leading `.`).
- Identifiers: `[a-zA-Z][a-zA-Z0-9_]*`; `true`/`false` are boolean
literals. A leading `_` is not an identifier start (`err_char`).
- Type symbols ` 𝔹` lex as identifiers (code-point-safe; 𝔹 is
supplementary-plane).
- Single-char tokens: `✎ λ ∀ ∈ ≜ ← ⟹ ∧ ≠ ≤ ≥ × ÷ ∘ ‖ ⊥ + - / = < > |
; : , ( ) [ ] { }`.
- Anything else → `err_char`.
## Parser (loosest to tightest)
`;` sequence → `‖` (desugars to sequence!) → `≜` (right-assoc, id target
only) → `←` (right-assoc, id target only) → `|` (left-assoc) → `⟹`
(right-assoc) → ```∧` → comparison (`= ≠ < > ≤ ≥`, non-associative —
`1 < 2 < 3` is a parse error) → `+ -``× ÷ /` → unary (`✎`, `-`) →
call `f(a, …)` (postfix, nullary `f()` parses) → atom.
Atoms: number/string/bool literals, `⊥`, identifiers,
`λ params [∈ constraint] : body` (≥ 1 parameter; the constraint is parsed
and **discarded unevaluated**), `∀ id ∈ expr : body`, list `[…]`, parens
`( expr )` (a single expression — `;` inside parens is a parse error),
braces `{ seq }` (`{}` evaluates to `⊥`).
Parse-class error keys: `err_char`, `err_escape`, `err_string`,
`err_comment`, `err_expect`, `err_unexpected`, `err_def_target`,
`err_assign_target`.
Lexed but unusable: `∘` (compose) has a token and an escape but **no
parser rule** — any use is `err_expect`.
## Evaluator
- Values: number (double), string, boolean, list, closure, `⊥`.
- `✎ e` prints `show(value)` and returns the value.
- `show`: `⊥``⊥`; strings bare at top level but **quoted inside
lists**; lists `[a, b]`; closures → `λ`; booleans `true`/`false`;
numbers via JS `String()` (integral doubles print without `.0`).
- `+` is numeric addition unless either side is a string — then it is
concatenation of `show`-rendered operands. `- × ÷ /` are numeric only
(`err_num`), `÷ 0``err_div0`.
- Guards: `c ⟹ e` fires iff `c` is `true` **or a non-zero number**;
strings/lists/`⊥` never fire. A non-firing guard yields NOMATCH, which
`|` catches; NOMATCH surfacing anywhere else becomes `⊥`.
- `∧ `: short-circuit; operands are tested with `=== true`, so non-boolean
operands behave as false (`1 ∧ true``false` — contrast with `⟹`).
- Comparison: `=`/`≠` via JSON serialization (structural for lists,
cross-type → `false`, `⊥ = ⊥``true`, comparing a self-referential
closure crashes keyless); `< > ≤ ≥` are raw JS comparisons (mixed-type
coercion applies).
- `≜` binds in the **current** scope; `←` mutates the nearest enclosing
binding, creating one in the current scope if none exists. Both return
the value; both may rebind.
- Braces `{…}` do **not** create a scope (bindings leak out). λ bodies and
each `∀` iteration do (the `∀` variable shadows and is restored).
- Closures capture the defining **environment** (later mutations are
visible), enabling recursion via `≜`.
- `∀ x ∈ list : body` requires a list (`err_iter`), evaluates the body per
element, and yields the last body value (`⊥` for an empty list).
- Errors carry a key + 1-based line:col. Runtime keys: `err_undef`,
`err_num`, `err_div0`, `err_notfn`, `err_arity`, `err_iter`,
`err_steps` (evaluation-step budget: 500 000).
- Deep recursion overflows the host stack **before** the step budget —
a keyless RangeError, unpinnable by the corpus (see JUDGMENT_CALLS).
## Explicitly out of corpus scope
- `‖` — parses, and the evaluator runs it as plain sequencing, but its
semantics are an M1 design question (locked decision 6): no corpus
entry pins it.
- Everything the grammar has that `js/mpl.js` does not implement (modules,
resources, channels, exceptions, metaprogramming, records, sets, choice
types, …) — Stage 4/5 artifacts, not Stage 2 ones.

View file

@ -0,0 +1,5 @@
14
20
5
2
4

View file

@ -0,0 +1 @@
{"status": "unratified", "source": "coverage", "decision": "", "notes": "× ÷ bind tighter than + -; + - and × ÷ left-associative"}

View file

@ -0,0 +1,5 @@
✎(2 + 3 × 4);
✎((2 + 3) × 4);
✎(10 - 2 - 3);
✎(20 ÷ 2 ÷ 5);
✎(2 + 12 ÷ 4 - 1);

View file

@ -0,0 +1,5 @@
-5
5
5
-6
-3

View file

@ -0,0 +1 @@
{"status": "unratified", "source": "coverage", "decision": "", "notes": "unary minus, including doubled and against binary minus"}

View file

@ -0,0 +1,5 @@
✎(-5);
✎(- -5);
✎(3 - -2);
✎(-2 × 3);
✎(-(1 + 2));

View file

@ -0,0 +1,3 @@
2.5
2.5
3

View file

@ -0,0 +1 @@
{"status": "unratified", "source": "coverage", "decision": "", "notes": "/ is an ASCII alias of ÷"}

View file

@ -0,0 +1,3 @@
✎(10 / 4);
✎(10 ÷ 4);
✎(9 / 3);

View file

@ -0,0 +1,6 @@
42
1.5
0.5
2
7
0.5

View file

@ -0,0 +1 @@
{"status": "unratified", "source": "coverage", "decision": "", "notes": "integral doubles display without decimal point; literals normalize"}

View file

@ -0,0 +1,6 @@
✎ 42;
✎ 1.5;
✎(1 ÷ 2);
✎(4 ÷ 2);
✎ 007;
✎ 0.50;

View file

@ -0,0 +1,3 @@
3.75
0.30000000000000004
6

View file

@ -0,0 +1 @@
{"status": "unratified", "source": "coverage", "decision": "", "notes": "IEEE double arithmetic, including the 0.1+0.2 representation artifact"}

View file

@ -0,0 +1,3 @@
✎(1.5 + 2.25);
✎(0.1 + 0.2);
✎(3.0 × 2);

View file

@ -0,0 +1,5 @@
a
b
a b
q"q
b\b

View file

@ -0,0 +1 @@
{"status": "unratified", "source": "coverage", "decision": "", "notes": "string escapes \\n \\t \\\" \\\\ (unknown escapes like \\q diverge from the grammar — see DIVERGENCES.md, not corpus-pinnable)"}

View file

@ -0,0 +1,4 @@
✎ "a\nb";
✎ "a\tb";
✎ "q\"q";
✎ "b\\b";

View file

@ -0,0 +1,6 @@
n=5
5!
l=[1, 2]
b=true
v=⊥
ab

View file

@ -0,0 +1 @@
{"status": "unratified", "source": "coverage", "decision": "", "notes": "+ concatenates when either operand is a string, rendering the other via show"}

View file

@ -0,0 +1,6 @@
✎("n=" + 5);
✎(5 + "!");
✎("l=" + [1, 2]);
✎("b=" + true);
✎("v=" + ⊥);
✎("a" + "b");

View file

@ -0,0 +1,3 @@
مرحبا
你好
Salaam

View file

@ -0,0 +1 @@
{"status": "unratified", "source": "coverage", "decision": "", "notes": "non-ASCII string content passes through byte-intact"}

View file

@ -0,0 +1,3 @@
✎ "مرحبا";
✎ "你好";
✎ "Salaam";

View file

@ -0,0 +1,3 @@
[1, "two", true, [3, 4], ⊥]
[]
[λ]

View file

@ -0,0 +1 @@
{"status": "unratified", "source": "coverage", "decision": "", "notes": "lists display with strings quoted inside; closures display as λ"}

View file

@ -0,0 +1,4 @@
id ≜ λx: x;
✎ [1, "two", true, [3, 4], ⊥];
✎ [];
✎ [id];

View file

@ -0,0 +1,3 @@
λ
7
1

View file

@ -0,0 +1 @@
{"status": "unratified", "source": "coverage", "decision": "", "notes": "λ definition, display, application, multiple parameters"}

View file

@ -0,0 +1,5 @@
id ≜ λx: x;
✎ id;
✎ id(7);
fst ≜ λa, b: a;
✎ fst(1, 2);

View file

@ -0,0 +1,2 @@
11
21

View file

@ -0,0 +1 @@
{"status": "unratified", "source": "coverage", "decision": "", "notes": "closures capture the environment, not values at definition time"}

View file

@ -0,0 +1,5 @@
x ← 10;
f ≜ λy: x + y;
✎ f(1);
x ← 20;
✎ f(1);

View file

@ -0,0 +1,2 @@
42
15

View file

@ -0,0 +1 @@
{"status": "unratified", "source": "coverage", "decision": "", "notes": "curried application and λ literals as call arguments"}

View file

@ -0,0 +1,5 @@
twice ≜ λf: λx: f(f(x));
inc ≜ λn: n + 1;
✎ twice(inc)(40);
apply ≜ λf, v: f(v);
✎ apply(λn: n × 3, 5);

View file

@ -0,0 +1 @@
55

View file

@ -0,0 +1 @@
{"status": "unratified", "source": "coverage", "decision": "", "notes": "binary recursion through a guarded alternative"}

View file

@ -0,0 +1,2 @@
fib ≜ λn: (n ≤ 1 ⟹ n) | (fib(n - 1) + fib(n - 2));
✎ fib(10);

View file

@ -0,0 +1 @@
125250

View file

@ -0,0 +1 @@
{"status": "unratified", "source": "coverage", "decision": "", "notes": "linear recursion 500 deep (within the host stack)"}

View file

@ -0,0 +1,2 @@
sum ≜ λn: (n = 0 ⟹ 0) | (n + sum(n - 1));
✎ sum(500);

View file

@ -0,0 +1 @@
55

View file

@ -0,0 +1 @@
{"status": "unratified", "source": "coverage", "decision": "", "notes": "∀ with an accumulating assignment"}

View file

@ -0,0 +1,3 @@
t ← 0;
∀ n ∈ [1, 2, 3, 4, 5]: t ← t + n × n;
✎ t;

View file

@ -0,0 +1,2 @@
6

View file

@ -0,0 +1 @@
{"status": "unratified", "source": "coverage", "decision": "", "notes": "a ∀ expression yields the last body value; empty collection yields ⊥"}

View file

@ -0,0 +1,2 @@
✎(∀ n ∈ [1, 2, 3]: n × 2);
✎(∀ n ∈ []: n);

View file

@ -0,0 +1,3 @@
1
2
100

View file

@ -0,0 +1 @@
{"status": "unratified", "source": "coverage", "decision": "", "notes": "the ∀ variable shadows per iteration and the outer binding survives"}

View file

@ -0,0 +1,3 @@
n ← 100;
∀ n ∈ [1, 2]: ✎ n;
✎ n;

View file

@ -0,0 +1,3 @@
A
B
C

View file

@ -0,0 +1 @@
{"status": "unratified", "source": "coverage", "decision": "", "notes": "the canonical conditional: guarded alternatives with fallback"}

View file

@ -0,0 +1,4 @@
grade ≜ λs: (s ≥ 90 ⟹ "A") | ((s ≥ 80 ⟹ "B") | "C");
✎ grade(95);
✎ grade(85);
✎ grade(70);

View file

@ -0,0 +1,2 @@

View file

@ -0,0 +1 @@
{"status": "unratified", "source": "coverage", "decision": "", "notes": "a guard that never fires, with no | fallback, surfaces as ⊥"}

View file

@ -0,0 +1,3 @@
✎((false ⟹ 1));
x ← (false ⟹ 1);
✎ x;

View file

@ -0,0 +1,5 @@
one
no
num
no
no

View file

@ -0,0 +1 @@
{"status": "unratified", "source": "coverage", "decision": "", "notes": "guard conditions: true or non-zero number fire; strings/lists never do"}

View file

@ -0,0 +1,5 @@
✎((1 ⟹ "one") | "no");
✎((0 ⟹ "zero") | "no");
✎((2.5 ⟹ "num") | "no");
✎(("s" ⟹ "str") | "no");
✎(([1] ⟹ "list") | "no");

View file

@ -0,0 +1,2 @@
3
2

View file

@ -0,0 +1 @@
{"status": "unratified", "source": "coverage", "decision": "", "notes": "fall-through chains take the first firing arm"}

View file

@ -0,0 +1,2 @@
✎((false ⟹ 1) | (false ⟹ 2) | 3);
✎((false ⟹ 1) | (true ⟹ 2) | 3);

View file

@ -0,0 +1,4 @@
1
2
3
5

View file

@ -0,0 +1 @@
{"status": "unratified", "source": "coverage", "decision": "", "notes": "≜ and ← both rebind freely; ← works without a prior ≜"}

View file

@ -0,0 +1,8 @@
x ≜ 1;
✎ x;
x ← 2;
✎ x;
x ≜ 3;
✎ x;
y ← 5;
✎ y;

View file

@ -0,0 +1,4 @@
7
8
2
2

View file

@ -0,0 +1 @@
{"status": "unratified", "source": "coverage", "decision": "", "notes": "both binding forms are expressions returning the bound value; ≜ chains right"}

View file

@ -0,0 +1,5 @@
✎(a ≜ 7);
✎(a ← 8);
b ≜ c ≜ 2;
✎ b;
✎ c;

View file

@ -0,0 +1,2 @@
99
99

View file

@ -0,0 +1 @@
{"status": "unratified", "source": "coverage", "decision": "", "notes": "inside a λ, ← mutates the captured outer binding; ≜ creates a local one"}

View file

@ -0,0 +1,7 @@
x ← 1;
f ≜ λy: {x ← 99; x};
f(0);
✎ x;
g ≜ λy: {x ≜ 55; x};
g(0);
✎ x;

View file

@ -0,0 +1,3 @@
3
4

View file

@ -0,0 +1 @@
{"status": "unratified", "source": "coverage", "decision": "", "notes": "a block yields its last expression; {} yields ⊥; trailing ; permitted"}

View file

@ -0,0 +1,3 @@
✎({1; 2; 3});
✎({});
✎({4;});

View file

@ -0,0 +1 @@
9

View file

@ -0,0 +1 @@
{"status": "unratified", "source": "coverage", "decision": "", "notes": "braces do NOT create a scope: bindings made inside leak out"}

View file

@ -0,0 +1,2 @@
{y ← 9; 0};
✎ y;

View file

@ -0,0 +1,3 @@
1
2
3

View file

@ -0,0 +1 @@
{"status": "unratified", "source": "coverage", "decision": "", "notes": "line comments and nested block comments"}

View file

@ -0,0 +1,4 @@
-- line comment
✎ 1; {- block -} ✎ 2;
{- outer {- nested -} outer -}
✎ 3;

View file

@ -0,0 +1,3 @@
x⊥
[⊥, 1]

View file

@ -0,0 +1 @@
{"status": "unratified", "source": "coverage", "decision": "", "notes": "⊥ displays as ⊥ and concatenates/nests as a value"}

View file

@ -0,0 +1,3 @@
✎ ⊥;
✎("x" + ⊥);
✎ [⊥, 1];

View file

@ -0,0 +1,8 @@
42
1.5
s
true
false
[1]
λ

View file

@ -0,0 +1 @@
{"status": "unratified", "source": "coverage", "decision": "", "notes": "one ✎ per value type"}

View file

@ -0,0 +1,9 @@
f ≜ λx: x;
✎ 42;
✎ 1.5;
✎ "s";
✎ true;
✎ false;
✎ [1];
✎ ⊥;
✎ f;

View file

@ -0,0 +1,6 @@
true
true
false
false
true
true

View file

@ -0,0 +1 @@
{"status": "unratified", "source": "coverage", "decision": "", "notes": "all six comparison operators on numbers"}

View file

@ -0,0 +1,6 @@
✎(1 < 2);
✎(2 ≤ 2);
✎(3 > 4);
✎(4 ≥ 5);
✎(1 = 1);
✎(1 ≠ 2);

View file

@ -0,0 +1,4 @@
true
true
true
true

View file

@ -0,0 +1 @@
{"status": "unratified", "source": "coverage", "decision": "", "notes": "lexicographic order and structural equality on strings"}

View file

@ -0,0 +1,4 @@
✎("a" < "b");
✎("abc" = "abc");
✎("abc" ≠ "abd");
✎("b" ≥ "a");

View file

@ -0,0 +1,6 @@
false
false
true
true
true
false

View file

@ -0,0 +1 @@
{"status": "unratified", "source": "coverage", "decision": "", "notes": "equality is structural per type and false across types; ⊥ equals ⊥"}

View file

@ -0,0 +1,6 @@
✎(1 = "1");
✎(true = 1);
✎([1] = [1]);
✎([] = []);
✎(⊥ = ⊥);
✎("" = ⊥);

View file

@ -0,0 +1,3 @@
true
false
true

View file

@ -0,0 +1 @@
{"status": "unratified", "source": "coverage", "decision": "", "notes": "ordering across types follows host coercion — observed, flagged as a judgment call"}

View file

@ -0,0 +1,3 @@
✎(1 < "2");
✎("10" < 9);
✎(true < 2);

Some files were not shown because too many files have changed in this diff Show more