From eac5371da1e90e7b9269f58641be27a95214e17f Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 24 Jul 2026 07:29:03 +0000 Subject: [PATCH] =?UTF-8?q?Aether=2030.0=20=E2=80=94=20comprehensions=20gr?= =?UTF-8?q?ow=20up:=20pattern=20generators,=20let-qualifiers=20&=20range?= =?UTF-8?q?=20literals?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit List comprehensions previously bound only a plain name and filtered with boolean guards, and there were no range literals. This release adds, as pure parser sugar desugared into the existing core (so the type checker and all three backends see only ordinary map/filter/concat/match): - range literals `[a .. b]` (inclusive) and `[a, s .. b]` (stepped), backed by two new prelude functions `enumFromTo` / `enumFromThenTo`; - pattern generators `(a,b) <- ps`, `Som x <- opts`, `h :: _ <- rows`, where a refutable pattern drops the non-matching elements (the list-monad fail); - `let`-qualifiers `let y = f x`, scoped over the qualifiers to their right. Verification: a new 200-program differential fuzzer (comprehensionFuzz.ts) checks each random comprehension against an independent TypeScript reference evaluator and the JavaScript backend (VM ≡ reference ≡ JS); a new 19-case in-app `comprehensions` battery (suite 147 → 166); four gallery examples incl. a turtle "comprehension garden"; About/parser-note and stdlib updates. No regression to existing suites. Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_01BSXUJbL86qsEW8zJqvUppq --- projects/aether-lang-c3d8/JOURNAL.md | 87 ++++- projects/aether-lang-c3d8/src/examples.ts | 86 +++++ .../src/lang/comprehensionFuzz.ts | 340 ++++++++++++++++++ projects/aether-lang-c3d8/src/lang/lexer.ts | 1 + projects/aether-lang-c3d8/src/lang/parser.ts | 142 +++++++- projects/aether-lang-c3d8/src/lang/prelude.ts | 16 + .../aether-lang-c3d8/src/lang/testSuite.ts | 122 +++++++ projects/aether-lang-c3d8/src/pages/About.tsx | 13 +- projects/aether-lang-c3d8/src/pages/Tests.tsx | 46 +++ 9 files changed, 834 insertions(+), 19 deletions(-) create mode 100644 projects/aether-lang-c3d8/src/lang/comprehensionFuzz.ts diff --git a/projects/aether-lang-c3d8/JOURNAL.md b/projects/aether-lang-c3d8/JOURNAL.md index 1df7c622..db538da2 100644 --- a/projects/aether-lang-c3d8/JOURNAL.md +++ b/projects/aether-lang-c3d8/JOURNAL.md @@ -63,6 +63,61 @@ compile the same optimized core — and the equivalence checks prove it preserve ## Ideas / backlog +### Aether 30.0 — comprehensions grow up: pattern generators, `let`-qualifiers & range literals (planned + shipped this session) + +Aether has had list comprehensions since early on, but only in their most basic form: a generator +could bind a **plain name** (`x <- xs`) and a qualifier could be a boolean **guard** — nothing else. +That leaves out the three things every working programmer reaches for the moment they have +comprehensions at all, and it left the language without the one piece of list sugar every ML/Haskell +descendant ships: **range literals**. 30.0 closes that gap, and does it the way the language is proud +of — as **pure front-end sugar**. Every new form is desugared *in the parser* into the existing core +(`concat`/`map`/`if`/`let`/`match`, plus two tiny new prelude functions), so the type checker, the +optimizing middle-end and all **three backends** (bytecode VM · JavaScript · WebAssembly) never see a +comprehension or a range at all. That makes the whole release **strictly additive**: an old program +takes the exact pre-30.0 path, and the risk surface is confined to a few hundred lines of the parser. + +The plan, step by step: + +- [x] **A `..` token.** Add `..` to the lexer's operator table (longest-match, so `1..10` lexes as + `1 · .. · 10` while `r.field` keeps its single-`.` field access and floats like `1.5` are + unaffected — the number scanner only treats a `.` as a decimal point when a digit follows). +- [x] **Range literals.** `[a .. b]` is the **inclusive** integer enumeration `a, a+1, …, b`; + `[a, s .. b]` is the arithmetic sequence with the step read off the first two elements + (`a, s, s+(s−a), …`), ascending or descending, bounded by `b`. They desugar to two new prelude + functions, `enumFromTo` and `enumFromThenTo`, written in Aether itself (a zero step terminates as + the empty list rather than diverging — a deliberate, total choice for a strict language). Only the + *second* element may precede `..`, so `[1, 2, 3 .. 9]` is a clean parse error, not a silent guess. +- [x] **Pattern generators.** A generator's binder becomes any **pattern**, not just a name: + `(a, b) <- pairs`, `Som x <- opts`, `h :: _ <- rows`. An **irrefutable** binder (a variable or + wildcard) keeps the old clean `map`-a-bare-lambda desugaring; any other pattern maps a + `fn v -> match v with pat -> [e|Q] | _ -> []` — the wildcard arm **drops** the elements that don't + match, exactly the list-monad `fail`, so `[ x | Som x <- xs ]` keeps only the `Som`s. Detecting a + generator now means scanning for a top-level `<-` at bracket depth 0 before the qualifier ends, + which lets an arbitrary pattern precede the arrow with no speculative parse. +- [x] **`let`-qualifiers.** `[ e | x <- xs, let y = f x, y > 0 ]` binds `y` for every qualifier to its + right; it desugars to a `let` (or a single-arm `match` for a destructuring pattern, which stays + exhaustive for products so no spurious warning fires). +- [x] **Multiple generators & guards** keep composing as before (a cartesian product, with guards + pruning early) — now over ranges and patterns. +- [x] **A differential fuzzer** (`comprehensionFuzz.ts`): 200 random comprehensions per run — nested + generators, inclusive/stepped ranges, guards, `let`-qualifiers and tuple/`Som`/cons pattern + generators — each proved sound two ways: the compiled program's **VM result equals an independent + reference** (the same comprehension evaluated by nested iteration in TypeScript, never touching the + parser's desugaring), and that value **re-appears on the JavaScript backend**. A badge on the Tests + page; deterministic, so it's stable. +- [x] **An in-app battery** (19 cases in a new `comprehensions` group) + gallery examples + (comprehensions tour, quicksort, a prime sieve, and a turtle **"comprehension garden"** driven by a + stepped range) + About/parser-note updates + two new stdlib entries. +- [ ] **Float / `Char` / generic `Enum` ranges** — today `[a .. b]` is `Int`-only (the desugaring + targets the `Int` prelude helpers). A `class Enum a` with `enumFromTo`/`enumFromThenTo` methods would + let `['a' .. 'z']` and `[1.0, 1.5 .. 3.0]` share the syntax, resolved by the dictionary machinery. +- [ ] **Comprehension-aware fusion** — a range generator immediately consumed (`sum [ f x | x <- [1..n] ]`) + still builds the intermediate list; teaching short-cut fusion the `enumFromTo`/`concat`/`map` shape + the desugarer emits would let it collapse to a single loop, as the hand-written combinator form + already does. +- [ ] **Parallel comprehensions** (the GHC `| … | …` zip extension) and a **`then`/group** clause — + more exotic, but they'd exercise the qualifier grammar further. + ### Aether 29.0 — the type system grows a spine: signatures, ascription & GADTs (planned + shipped this session) Until now Aether inferred *everything* with zero annotations — a point of pride, but also a @@ -2145,13 +2200,43 @@ finds `sum x`, `abs x`, `max x 0` (clamp), `reverse x`, `map (fn h -> h + h) x`, ## Standard library -- list: `map filter foldl foldr length append reverse sum range take drop elem all any concat zip replicate` +- list: `map filter foldl foldr length append reverse sum range enumFromTo enumFromThenTo take drop elem all any concat zip replicate` + (`enumFromTo`/`enumFromThenTo` back the `[a .. b]` / `[a, s .. b]` range literals) - string: `strlen toUpper toLower chars join parseInt` (+ `show`, `^`) - primitives: `head tail empty print sqrt sin cos floor toFloat pi abs min max` - operators: `+ - * / % | +. -. *. /. | == != < > <= >= | && || ! | :: ++ ^ | |> | ;` ## Session log +- 2026-07-24 (claude): **Aether 30.0 — comprehensions grow up: pattern generators, `let`-qualifiers & + range literals.** The language had list comprehensions, but only the thinnest slice: a generator + bound a **plain name** and a qualifier was a boolean **guard** — and there were no **range + literals** at all, the one piece of list sugar every ML/Haskell descendant ships. 30.0 closes the + gap as **pure front-end sugar**, desugared *in the parser* into the existing core, so the type + checker, the optimizing middle-end and all three backends (VM · JS · WASM) never see a comprehension + or a range — making the whole release **strictly additive** (an old program takes the exact pre-30.0 + path). New: a `..` lexer token (longest-match, so `1..10` splits cleanly while `r.field` and floats + are untouched); **range literals** `[a .. b]` (inclusive) and `[a, s .. b]` (stepped, ascending or + descending, a zero step terminating as `[]`), backed by two new prelude functions `enumFromTo` / + `enumFromThenTo` written in Aether itself; **pattern generators** `(a,b) <- ps`, `Som x <- opts`, + `h :: _ <- rows` where an irrefutable binder keeps the bare-`map` desugaring and any other pattern + maps a `match … | _ -> []` whose wildcard arm **drops** the non-matches (the list-monad `fail`); and + **`let`-qualifiers** `let y = f x` scoped over the qualifiers to their right. Generator detection now + scans for a top-level `<-` at bracket depth 0, so an arbitrary pattern can precede the arrow with no + speculative parse. **Verification:** a new **200-program differential fuzzer** (`comprehensionFuzz.ts`) + generates random comprehensions — nested generators, inclusive/stepped ranges, guards, + `let`-qualifiers and tuple/`Som`/cons pattern generators — and proves each sound two ways: the + compiled program's **VM result equals an independent TypeScript reference** (the comprehension + re-evaluated by nested iteration, never touching the desugaring) **and** the value **re-appears on + the JavaScript backend** (VM ≡ JS); it holds at **200/200** here and across seven seeds × 300 runs + (2,100 programs, ~12k list elements, zero failures), with a stable badge on the Tests page. A new + 19-case in-app `comprehensions` battery (VM + JS ≡ VM, all green; the head-less harness also re-runs + each on WASM) grows the suite **147 → 166**, four new gallery examples (a comprehensions tour, + two-line quicksort, a prime sieve, and a turtle **"comprehension garden"** driven by a stepped + range), plus About/parser-note and stdlib updates. The existing suites are unchanged (166/166 + in-app, WASM ≡ VM 150/150, semantics 19/19, and the optimizer/SpecConstr/SROA fuzzers still pass — no + regression). Full CI gate (scope + conformance + lint + tsc + build) green. + - 2026-07-04 (claude): **Aether 28.0 — the synthesizer learns to recurse (+ Auto-CEGIS).** The `Synthesize` engine could write straight-line code, the four combinators with synthesized lambdas, and a top-level `if` — but nothing that calls itself. 28.0 adds a **structural-recursion tier** diff --git a/projects/aether-lang-c3d8/src/examples.ts b/projects/aether-lang-c3d8/src/examples.ts index ae17cda6..760a1f73 100644 --- a/projects/aether-lang-c3d8/src/examples.ts +++ b/projects/aether-lang-c3d8/src/examples.ts @@ -1589,6 +1589,92 @@ let rec ramp = fn n -> fn acc -> (ramp 50 0, tag 7, tag 42, tag 99) `, }, + { + id: 'comprehensions', + title: 'List comprehensions & ranges', + blurb: 'Generators, guards, let-bindings, pattern generators and range literals — Aether 30.0.', + visual: false, + code: `// Aether 30.0 — comprehensions & ranges. All pure sugar: the parser lowers +// each form to the existing core, so the type checker and all three backends +// (VM · JavaScript · WebAssembly) see only ordinary map/filter/concat/match. +// (Open the AST panel to watch a comprehension turn into its desugaring.) + +// Range literals: inclusive [a .. b] and stepped [a, s .. b]. +let counting = [1 .. 10] in // [1, …, 10] +let evens = [0, 2 .. 20] in // step 2 +let countdown = [10, 8 .. 0] in // a descending step + +// Generators + guards. Multiple generators nest (a cartesian product); +// a guard filters the tuples seen so far. +let pyth = [ (a, b, c) + | c <- [1 .. 20], b <- [1 .. c], a <- [1 .. b] + , a * a + b * b == c * c ] in + +// A 'let'-qualifier names an intermediate; it's in scope to its right. +let scaled = [ y | x <- [1 .. 6], let y = x * x, y > 4 ] in + +// Pattern generators bind by destructuring — and a *refutable* one silently +// drops the elements that don't match (the list-monad 'fail'). +type Opt = Non | Som Int in +let justs = [ x * 10 | Som x <- [Som 1, Non, Som 2, Non, Som 3] ] in + +(counting, evens, countdown, pyth, scaled, justs)`, + }, + { + id: 'quicksort', + title: 'Quicksort in two lines', + blurb: 'The classic comprehension quicksort — partition with two comprehensions, recurse.', + visual: false, + code: `// Quicksort reads like its own specification when you have comprehensions: +// everything below the pivot, then the pivot, then everything at-or-above. +let rec qsort xs = match xs with + | [] -> [] + | p :: rest -> + append (qsort [ y | y <- rest, y < p ]) + (p :: qsort [ y | y <- rest, y >= p ]) in + +qsort [3, 8, 1, 4, 1, 5, 9, 2, 6, 5, 3, 5]`, + }, + { + id: 'sieve', + title: 'Primes by comprehension', + blurb: 'A trial-division sieve: keep n whose divisor-comprehension is empty.', + visual: false, + code: `// A number is prime when it has no divisor strictly between 1 and itself — +// so keep the n whose "divisors" comprehension comes back empty. +let rec divides d n = + if n < d then false + else if n == d then true + else divides d (n - d) in + +let primesUpTo = fn hi -> + [ n | n <- [2 .. hi], length [ d | d <- [2 .. n - 1], divides d n ] == 0 ] in + +primesUpTo 60`, + }, + { + id: 'comprehension-garden', + title: 'Comprehension garden', + blurb: 'A stepped range drives a comprehension of angles; a fold walks the turtle into a burst.', + visual: true, + code: `// A stepped range [0, 9 .. 351] enumerates the spoke angles; a comprehension +// turns them to floats (dropping every fifth for a little rhythm), and a fold +// walks the turtle through the list — one petal per angle. +let spokes = [ toFloat a | a <- [0, 9 .. 351], a % 5 != 0 ] in + +let petal = fn ang -> ( + push (); + color (120 + floor (ang *. 0.35)) 200 (210 - floor (ang *. 0.45)); + turn ang; + forward (72.0 +. ang *. 0.26); + turn 40.0; + forward 24.0; + pop (); + () +) in + +foldl (fn _ ang -> petal ang) () spokes`, + }, ] export const DEFAULT_CODE = EXAMPLES[0].code diff --git a/projects/aether-lang-c3d8/src/lang/comprehensionFuzz.ts b/projects/aether-lang-c3d8/src/lang/comprehensionFuzz.ts new file mode 100644 index 00000000..d9f2a587 --- /dev/null +++ b/projects/aether-lang-c3d8/src/lang/comprehensionFuzz.ts @@ -0,0 +1,340 @@ +// Aether — an in-browser DIFFERENTIAL FUZZER for list comprehensions & ranges. +// +// The comprehension surface (Aether 30.0) is pure syntactic sugar: `[ e | q… ]` +// desugars in the parser to `concat`/`map`/`if`/`let`/`match`, and range literals +// `[a .. b]` / `[a, s .. b]` desugar to the `enumFromTo` / `enumFromThenTo` +// prelude functions. Sugar is exactly where a subtle bug hides — a wrong +// desugaring type-checks and runs, it just computes the wrong *set*. So this +// harness generates hundreds of random comprehensions and proves, for each: +// +// • the compiled program's VM result equals an INDEPENDENT reference — the same +// comprehension evaluated directly here in TypeScript by nested iteration, +// never touching the parser's desugaring. This pins the sugar to its spec: +// inclusive ranges, cartesian nesting, guards, `let`-qualifiers, refutable +// pattern generators that drop non-matches (the list-monad `fail`); and +// • that same value re-appears from the JavaScript backend (VM ≡ JS), so the +// sugar is sound on *all* of Aether's backends, not just the tree-walker. +// +// Deterministic given the seed, so the Tests page shows a stable badge; pure +// logic, so it also runs head-less under Node. + +import { runPipeline } from './pipeline.ts' +import { compileToJs, runJsModule } from './jsBackend.ts' +import { valueToString } from './values.ts' + +export interface ComprehensionFuzzResult { + total: number + passed: number + /** how many programs used a refutable (dropping) pattern generator */ + refutable: number + /** how many programs used a non-trivial pattern generator (tuple / `Som` / cons) */ + patterned: number + /** total number of list elements produced across the whole batch */ + elements: number + /** the first few divergences, if any (empty ⇒ the sugar is sound here) */ + failures: { code: string; detail: string }[] +} + +// --------------------------------------------------------------------------- +// a tiny deterministic LCG (same shape as the optimizer fuzzer's) +// --------------------------------------------------------------------------- + +type Rng = () => number + +function makeRng(seed: number): Rng { + let s = seed >>> 0 + return () => { + s = (s * 1664525 + 1013904223) >>> 0 + return s / 4294967296 + } +} + +const pick = (rng: Rng, xs: readonly T[]): T => xs[Math.floor(rng() * xs.length) | 0] +const int = (rng: Rng, lo: number, hi: number): number => lo + (Math.floor(rng() * (hi - lo + 1)) | 0) + +// --------------------------------------------------------------------------- +// a small Int/Bool expression language over the in-scope variables, with both +// an `emit` (to Aether source) and an `eval` (the reference). Kept syntactically +// identical on both sides — the whole point is that they must agree. +// --------------------------------------------------------------------------- + +type Env = Record + +interface IntExpr { + emit: () => string + eval: (env: Env) => number +} +interface BoolExpr { + emit: () => string + eval: (env: Env) => boolean +} + +const ARITH: readonly ['+' | '-' | '*', (a: number, b: number) => number][] = [ + ['+', (a, b) => a + b], + ['-', (a, b) => a - b], + ['*', (a, b) => a * b], +] +const CMP: readonly ['==' | '!=' | '<' | '>' | '<=' | '>=', (a: number, b: number) => boolean][] = [ + ['==', (a, b) => a === b], + ['!=', (a, b) => a !== b], + ['<', (a, b) => a < b], + ['>', (a, b) => a > b], + ['<=', (a, b) => a <= b], + ['>=', (a, b) => a >= b], +] + +// an Int expression over `ctx` (guaranteed non-empty when this is reached); +// literals are kept NON-NEGATIVE so `Som n`-style constructor args never lex as +// a subtraction and every emitted atom is a plain juxtaposable token. +function genInt(rng: Rng, ctx: string[], d: number): IntExpr { + if (d <= 0 || rng() < 0.4) { + if (ctx.length > 0 && rng() < 0.6) { + const v = pick(rng, ctx) + return { emit: () => v, eval: (env) => env[v] } + } + const n = int(rng, 0, 6) + return { emit: () => String(n), eval: () => n } + } + const [op, fn] = pick(rng, ARITH) + const l = genInt(rng, ctx, d - 1) + const r = genInt(rng, ctx, d - 1) + return { + emit: () => `(${l.emit()} ${op} ${r.emit()})`, + eval: (env) => fn(l.eval(env), r.eval(env)), + } +} + +function genBool(rng: Rng, ctx: string[]): BoolExpr { + const [op, fn] = pick(rng, CMP) + const l = genInt(rng, ctx, 2) + const r = genInt(rng, ctx, 2) + return { + emit: () => `${l.emit()} ${op} ${r.emit()}`, + eval: (env) => fn(l.eval(env), r.eval(env)), + } +} + +// --------------------------------------------------------------------------- +// qualifiers — each carries how to render itself AND how to drive the reference +// iteration (bind a variable and recurse, or filter, or skip) +// --------------------------------------------------------------------------- + +type Qual = + | { t: 'range'; v: string; lo: number; hi: number } + | { t: 'step'; v: string; a: number; then: number; hi: number } + | { t: 'pair'; v1: string; v2: string; pairs: [number, number][] } + | { t: 'opt'; v: string; items: (number | null)[] } + | { t: 'cons'; v: string; lists: number[][] } + | { t: 'let'; v: string; expr: IntExpr } + | { t: 'guard'; expr: BoolExpr } + +// the inclusive integer sequence a, then, … bounded by hi — the exact spec of +// the `enumFromThenTo` prelude helper the `[a, s .. b]` literal desugars to. +function stepSeq(a: number, then: number, hi: number): number[] { + const step = then - a + if (step === 0) return [] + const out: number[] = [] + let x = a + if (step > 0) for (; x <= hi; x += step) out.push(x) + else for (; x >= hi; x += step) out.push(x) + return out +} + +function emitQual(q: Qual): string { + switch (q.t) { + case 'range': + return `${q.v} <- [${q.lo} .. ${q.hi}]` + case 'step': + return `${q.v} <- [${q.a}, ${q.then} .. ${q.hi}]` + case 'pair': + return `(${q.v1}, ${q.v2}) <- [${q.pairs.map(([a, b]) => `(${a}, ${b})`).join(', ')}]` + case 'opt': + return `Som ${q.v} <- [${q.items.map((i) => (i === null ? 'Non' : `Som ${i}`)).join(', ')}]` + case 'cons': + return `${q.v} :: _ <- [${q.lists.map((l) => `[${l.join(', ')}]`).join(', ')}]` + case 'let': + return `let ${q.v} = ${q.expr.emit()}` + case 'guard': + return q.expr.emit() + } +} + +// drive the reference: fold the qualifiers left-to-right over the environment, +// pushing `out.eval(env)` once every qualifier has been satisfied. +function referenceRun(quals: Qual[], out: IntExpr): number[] { + const acc: number[] = [] + const go = (i: number, env: Env): void => { + if (i >= quals.length) { + acc.push(out.eval(env)) + return + } + const q = quals[i] + switch (q.t) { + case 'range': + for (let x = q.lo; x <= q.hi; x++) go(i + 1, { ...env, [q.v]: x }) + break + case 'step': + for (const x of stepSeq(q.a, q.then, q.hi)) go(i + 1, { ...env, [q.v]: x }) + break + case 'pair': + for (const [a, b] of q.pairs) go(i + 1, { ...env, [q.v1]: a, [q.v2]: b }) + break + case 'opt': + for (const it of q.items) if (it !== null) go(i + 1, { ...env, [q.v]: it }) + break + case 'cons': + for (const l of q.lists) if (l.length > 0) go(i + 1, { ...env, [q.v]: l[0] }) + break + case 'let': + go(i + 1, { ...env, [q.v]: q.expr.eval(env) }) + break + case 'guard': + if (q.expr.eval(env)) go(i + 1, env) + break + } + } + go(0, {}) + return acc +} + +// --------------------------------------------------------------------------- +// generate one random comprehension: a program string + its reference value +// --------------------------------------------------------------------------- + +interface Generated { + code: string + reference: number[] + usedOpt: boolean + usedPattern: boolean +} + +function generate(rng: Rng): Generated { + const quals: Qual[] = [] + const scope: string[] = [] + let counter = 0 + const fresh = (): string => `v${counter++}` + let usedOpt = false + let usedPattern = false + + const nGen = int(rng, 1, 3) // 1–3 generators keeps the cartesian product small + let gensSoFar = 0 + const maxQuals = nGen + int(rng, 0, 3) + + while (quals.length < maxQuals) { + const needGen = gensSoFar < nGen && (gensSoFar === 0 || rng() < 0.7) + if (needGen) { + gensSoFar++ + const kind = pick(rng, ['range', 'range', 'step', 'pair', 'opt', 'cons'] as const) + if (kind === 'range') { + const lo = int(rng, 0, 5) + quals.push({ t: 'range', v: pushVar(), lo, hi: lo + int(rng, 0, 5) }) + } else if (kind === 'step') { + const a = int(rng, 0, 4) + const step = int(rng, 1, 3) + quals.push({ t: 'step', v: pushVar(), a, then: a + step, hi: a + int(rng, 0, 9) }) + } else if (kind === 'pair') { + usedPattern = true + const n = int(rng, 1, 4) + const pairs: [number, number][] = [] + for (let k = 0; k < n; k++) pairs.push([int(rng, 0, 6), int(rng, 0, 6)]) + const v1 = pushVar() + const v2 = pushVar() + quals.push({ t: 'pair', v1, v2, pairs }) + } else if (kind === 'opt') { + usedPattern = true + usedOpt = true + const n = int(rng, 1, 5) + const items: (number | null)[] = [] + for (let k = 0; k < n; k++) items.push(rng() < 0.4 ? null : int(rng, 0, 6)) + quals.push({ t: 'opt', v: pushVar(), items }) + } else { + usedPattern = true + const n = int(rng, 1, 4) + const lists: number[][] = [] + for (let k = 0; k < n; k++) { + const len = int(rng, 0, 3) + const l: number[] = [] + for (let j = 0; j < len; j++) l.push(int(rng, 0, 6)) + lists.push(l) + } + quals.push({ t: 'cons', v: pushVar(), lists }) + } + } else if (scope.length > 0 && rng() < 0.5) { + // a let-qualifier binds a fresh variable to an expression over the scope + const expr = genInt(rng, scope, 2) + quals.push({ t: 'let', v: pushVar(), expr }) + } else if (scope.length > 0) { + quals.push({ t: 'guard', expr: genBool(rng, scope) }) + } else { + continue + } + } + + const out = genInt(rng, scope, 3) + const prefix = usedOpt ? 'type Opt = Non | Som Int in\n' : '' + const code = `${prefix}[ ${out.emit()} | ${quals.map(emitQual).join(', ')} ]` + return { code, reference: referenceRun(quals, out), usedOpt, usedPattern } + + // helper: allocate a fresh variable and bring it into scope for later exprs + function pushVar(): string { + const v = fresh() + scope.push(v) + return v + } +} + +// --------------------------------------------------------------------------- +// the batch +// --------------------------------------------------------------------------- + +export function runComprehensionFuzz(runs = 200, seed = 0xc0117e): ComprehensionFuzzResult { + const rng = makeRng(seed) + let passed = 0 + let refutable = 0 + let patterned = 0 + let elements = 0 + const failures: { code: string; detail: string }[] = [] + + for (let i = 0; i < runs; i++) { + const g = generate(rng) + if (g.usedOpt) refutable++ + if (g.usedPattern) patterned++ + const expected = `[${g.reference.join(', ')}]` + elements += g.reference.length + + let vm: string + let coreAst + try { + const r = runPipeline(g.code, { execute: true }) + if (r.error) { + if (failures.length < 8) failures.push({ code: g.code, detail: `${r.error.stage}: ${r.error.message}` }) + continue + } + coreAst = r.optimizedCoreAst ?? r.coreAst + vm = r.run?.result ? valueToString(r.run.result) : '()' + } catch (e) { + if (failures.length < 8) failures.push({ code: g.code, detail: `threw: ${String(e)}` }) + continue + } + + if (vm !== expected) { + if (failures.length < 8) failures.push({ code: g.code, detail: `VM ${vm} ≠ reference ${expected}` }) + continue + } + + // VM ≡ JS backend + let jsOk = false + try { + const js = runJsModule(compileToJs(coreAst!).full) + jsOk = js.error === null && js.result === vm + if (!jsOk && failures.length < 8) { + failures.push({ code: g.code, detail: `JS ${js.error ?? js.result} ≠ VM ${vm}` }) + } + } catch (e) { + if (failures.length < 8) failures.push({ code: g.code, detail: `JS threw: ${String(e)}` }) + } + if (jsOk) passed++ + } + + return { total: runs, passed, refutable, patterned, elements, failures } +} diff --git a/projects/aether-lang-c3d8/src/lang/lexer.ts b/projects/aether-lang-c3d8/src/lang/lexer.ts index 3520147f..bcef97b2 100644 --- a/projects/aether-lang-c3d8/src/lang/lexer.ts +++ b/projects/aether-lang-c3d8/src/lang/lexer.ts @@ -71,6 +71,7 @@ const OPERATORS = [ '->', '<-', '::', + '..', '++', '|>', '<=', diff --git a/projects/aether-lang-c3d8/src/lang/parser.ts b/projects/aether-lang-c3d8/src/lang/parser.ts index 3cf7f14b..3f51b59d 100644 --- a/projects/aether-lang-c3d8/src/lang/parser.ts +++ b/projects/aether-lang-c3d8/src/lang/parser.ts @@ -21,9 +21,15 @@ import type { Span, Token } from './lexer.ts' import { tokenize } from './lexer.ts' import { DERIVABLE, deriveInstances, isDerivable } from './deriving.ts' -// A list-comprehension qualifier: a generator `name <- src` or a boolean guard. +// A list-comprehension qualifier. Three forms, mirroring Haskell: +// • a generator `pat <- src` — draw elements from a list, keeping only the +// ones that match `pat` (a refutable pattern silently drops non-matches, the +// list-monad `fail`); +// • a `let pat = rhs` binding, in scope for every qualifier to its right; +// • a boolean guard — any expression, filtering the elements seen so far. type Qualifier = - | { kind: 'gen'; name: string; src: Expr } + | { kind: 'gen'; pat: Pattern; src: Expr } + | { kind: 'let'; pat: Pattern; rhs: Expr } | { kind: 'guard'; test: Expr } export class ParseError extends Error { @@ -327,28 +333,63 @@ class Parser { const span = this.spanFrom(open.span, close.span) return this.desugarComprehension(first, quals, 0, span) } - // ordinary list literal + // range literal `[ a .. b ]` — the inclusive Int enumeration a, a+1, …, b. + if (this.at('op', '..')) { + this.next() + const to = this.parseExpr(0) + const close = this.expect('punc', ']') + const span = this.spanFrom(open.span, close.span) + return this.enumApp('enumFromTo', [first, to], span) + } + // ordinary list literal — or a stepped range `[ a, s .. b ]`. const elements: Expr[] = [first] while (this.at('punc', ',')) { this.next() - elements.push(this.parseExpr(0)) + const next = this.parseExpr(0) + // stepped range: `[ a, s .. b ]` enumerates a, s, s+(s-a), …, ≤ b (or ≥ b + // when the step is negative). Only the *second* element may precede `..`. + if (elements.length === 1 && this.at('op', '..')) { + this.next() + const to = this.parseExpr(0) + const close = this.expect('punc', ']') + const span = this.spanFrom(open.span, close.span) + return this.enumApp('enumFromThenTo', [first, next, to], span) + } + elements.push(next) } const close = this.expect('punc', ']') return { kind: 'list', elements, span: this.spanFrom(open.span, close.span) } } - // comprehension qualifiers: a `,`-separated list of generators (`x <- xs`) - // and boolean guards (any expression). + // Build the saturated application of a prelude enumeration helper to its + // range bounds, e.g. `enumFromTo a b` ⇒ ((enumFromTo a) b). + private enumApp(fn: string, args: Expr[], span: Span): Expr { + let acc: Expr = { kind: 'var', name: fn, span } + for (const a of args) { + acc = { kind: 'app', fn: acc, arg: a, span } + } + return acc + } + + // comprehension qualifiers: a `,`-separated list of generators (`pat <- xs`), + // `let pat = rhs` bindings and boolean guards (any expression). private parseQualifiers(): Qualifier[] { const quals: Qualifier[] = [] for (;;) { - const t = this.peek() - const ahead = this.toks[this.pos + 1] - if (t.kind === 'ident' && ahead && ahead.kind === 'op' && ahead.value === '<-') { - const name = this.next().value - this.next() // '<-' + if (this.at('keyword', 'let')) { + // `let pat = rhs` — a binding scoped over the qualifiers to its right. + this.next() + const pat = this.parsePattern() + this.expect('op', '=') + const rhs = this.parseExpr(0) + quals.push({ kind: 'let', pat, rhs }) + } else if (this.generatorAhead()) { + // `pat <- src` — a generator. `pat` may be any pattern; refutable + // patterns drop the elements that don't match. + const pat = this.parsePattern() + this.expect('op', '<-') const src = this.parseExpr(0) - quals.push({ kind: 'gen', name, src }) + quals.push({ kind: 'gen', pat, src }) } else { quals.push({ kind: 'guard', test: this.parseExpr(0) }) } @@ -361,10 +402,38 @@ class Parser { return quals } - // Desugar `[ e | q0, q1, … ]` into core AST using `concat`, `map` and `if`: - // [ e | ] ⇒ [e] - // [ e | b, Q ] ⇒ if b then [ e | Q ] else [] - // [ e | x <- xs, Q ] ⇒ concat (map (fn x -> [ e | Q ]) xs) + // Is the next qualifier a generator? True iff a top-level `<-` appears before + // the qualifier ends (a `,` at depth 0, or the closing `]`). Scanning at + // bracket depth lets an arbitrary pattern precede the arrow without a parse + // attempt — `(a, b) <- ps`, `Just x <- opts`, `h :: t <- rows` all qualify, + // while a plain guard such as `a * a == c * c` has no depth-0 `<-` and falls + // through to the guard branch. + private generatorAhead(): boolean { + let depth = 0 + for (let j = this.pos; j < this.toks.length; j++) { + const t = this.toks[j] + if (t.kind === 'eof') return false + if (t.kind === 'punc') { + if (t.value === '(' || t.value === '[' || t.value === '{') depth++ + else if (t.value === ')' || t.value === '}') depth-- + else if (t.value === ']') { + if (depth === 0) return false + depth-- + } else if (t.value === ',' && depth === 0) return false + } else if (t.kind === 'op' && t.value === '<-' && depth === 0) { + return true + } + } + return false + } + + // Desugar `[ e | q0, q1, … ]` into core AST using `concat`, `map`, `if`, `let` + // and (for refutable patterns) `match`: + // [ e | ] ⇒ [e] + // [ e | b, Q ] ⇒ if b then [ e | Q ] else [] + // [ e | let p = r, Q ] ⇒ let p = r in [ e | Q ] (via `match` if p isn't a name) + // [ e | x <- xs, Q ] ⇒ concat (map (fn x -> [ e | Q ]) xs) + // [ e | p <- xs, Q ] ⇒ concat (map (fn v -> match v with p -> [e|Q] | _ -> []) xs) private desugarComprehension( elem: Expr, quals: Qualifier[], @@ -380,7 +449,23 @@ class Parser { const empty: Expr = { kind: 'list', elements: [], span } return { kind: 'if', cond: q.test, then: rest, else: empty, span } } - const lambda: Expr = { kind: 'lambda', param: q.name, body: rest, span } + if (q.kind === 'let') { + // an irrefutable `let`: bind a name directly, or destructure via a + // single-arm `match` (products stay exhaustive, so no spurious warning). + if (q.pat.kind === 'pvar') { + return { kind: 'let', name: q.pat.name, value: q.rhs, body: rest, recursive: false, span } + } + return { + kind: 'match', + scrutinee: q.rhs, + cases: [{ pattern: q.pat, body: rest }], + span, + } + } + // a generator. A plain-name (or wildcard) pattern is irrefutable, so we can + // map a bare lambda over the source; any other pattern needs a `match` whose + // wildcard arm drops the elements that don't fit. + const lambda = this.generatorLambda(q.pat, rest, span) const mapVar: Expr = { kind: 'var', name: 'map', span } const concatVar: Expr = { kind: 'var', name: 'concat', span } const mapped: Expr = { @@ -392,6 +477,29 @@ class Parser { return { kind: 'app', fn: concatVar, arg: mapped, span } } + // Build the per-element lambda for a generator over pattern `pat` producing + // `rest` (already the [e|Q] tail). Irrefutable binders skip the `match`. + private generatorLambda(pat: Pattern, rest: Expr, span: Span): Expr { + if (pat.kind === 'pvar') { + return { kind: 'lambda', param: pat.name, body: rest, span } + } + if (pat.kind === 'pwild') { + return { kind: 'lambda', param: this.freshName(), body: rest, span } + } + const v = this.freshName() + const empty: Expr = { kind: 'list', elements: [], span } + const body: Expr = { + kind: 'match', + scrutinee: { kind: 'var', name: v, span }, + cases: [ + { pattern: pat, body: rest }, + { pattern: { kind: 'pwild', span }, body: empty }, + ], + span, + } + return { kind: 'lambda', param: v, body, span } + } + private parseLambda(): Expr { const start = this.expect('keyword', 'fn') // each parameter is either a plain name or a destructuring pattern (a `(`/`{`/ diff --git a/projects/aether-lang-c3d8/src/lang/prelude.ts b/projects/aether-lang-c3d8/src/lang/prelude.ts index 44b61305..387e809c 100644 --- a/projects/aether-lang-c3d8/src/lang/prelude.ts +++ b/projects/aether-lang-c3d8/src/lang/prelude.ts @@ -255,6 +255,22 @@ export const PRELUDE_DEFS: PreludeDef[] = [ doc: 'range a b — the ints [a, b)', src: 'fn a b -> if a >= b then [] else a :: range (a + 1) b', }, + { + name: 'enumFromTo', + recursive: true, + doc: 'enumFromTo a b — the inclusive ints a, a+1, …, b (the `[a .. b]` literal)', + src: 'fn a b -> if a > b then [] else a :: enumFromTo (a + 1) b', + }, + { + name: 'enumFromThenTo', + recursive: true, + doc: 'enumFromThenTo a s b — the arithmetic sequence a, s, … bounded by b (the `[a, s .. b]` literal)', + src: `fn a s b -> + let step = s - a in + if step == 0 then [] + else if step > 0 then (if a > b then [] else a :: enumFromThenTo s (s + step) b) + else (if a < b then [] else a :: enumFromThenTo s (s + step) b)`, + }, { name: 'take', recursive: true, diff --git a/projects/aether-lang-c3d8/src/lang/testSuite.ts b/projects/aether-lang-c3d8/src/lang/testSuite.ts index 1dbba57f..b8ce7cc2 100644 --- a/projects/aether-lang-c3d8/src/lang/testSuite.ts +++ b/projects/aether-lang-c3d8/src/lang/testSuite.ts @@ -1261,6 +1261,128 @@ let f = fn e -> match e with | ILit n -> n | BLit b -> b in 0`, expected: null, expectError: true, }, + + // ---- comprehensions & ranges (Aether 30.0) ---- + // Every case runs on the VM and is re-checked against the JavaScript backend + // (JS ≡ VM); the headless differential harness also re-runs them on WASM. + { + group: 'comprehensions', + name: 'range literal [a .. b] is inclusive', + code: '[1 .. 5]', + expected: '[1, 2, 3, 4, 5]', + }, + { + group: 'comprehensions', + name: 'a backwards range is empty', + code: '[5 .. 1]', + expected: '[]', + }, + { + group: 'comprehensions', + name: 'single-point range', + code: '[7 .. 7]', + expected: '[7]', + }, + { + group: 'comprehensions', + name: 'stepped range [a, s .. b]', + code: '[1, 3 .. 11]', + expected: '[1, 3, 5, 7, 9, 11]', + }, + { + group: 'comprehensions', + name: 'descending stepped range', + code: '[10, 8 .. 0]', + expected: '[10, 8, 6, 4, 2, 0]', + }, + { + group: 'comprehensions', + name: 'a zero-step range terminates (empty)', + code: '[1, 1 .. 9]', + expected: '[]', + }, + { + group: 'comprehensions', + name: 'range drives a comprehension', + code: '[ x * x | x <- [1 .. 6] ]', + expected: '[1, 4, 9, 16, 25, 36]', + }, + { + group: 'comprehensions', + name: 'tuple-pattern generator', + code: 'let ps = [(1, 10), (2, 20), (3, 30)] in [ a + b | (a, b) <- ps ]', + expected: '[11, 22, 33]', + }, + { + group: 'comprehensions', + name: 'refutable generator drops non-matches (list-monad fail)', + code: 'type Opt = Non | Som Int in [ x * x | Som x <- [Som 2, Non, Som 4, Non] ]', + expected: '[4, 16]', + }, + { + group: 'comprehensions', + name: 'cons-pattern generator over a list of lists', + code: '[ h | h :: _ <- [[1, 2], [], [3, 4], [5]] ]', + expected: '[1, 3, 5]', + }, + { + group: 'comprehensions', + name: 'let-qualifier binds for the qualifiers to its right', + code: '[ y | x <- [1 .. 5], let y = x * x, y > 4 ]', + expected: '[9, 16, 25]', + }, + { + group: 'comprehensions', + name: 'let-qualifier with a tuple pattern', + code: '[ s | x <- [1 .. 3], let (lo, hi) = (x, x * 10), let s = lo + hi ]', + expected: '[11, 22, 33]', + }, + { + group: 'comprehensions', + name: 'multiple generators form a cartesian product', + code: '[ (x, y) | x <- [1 .. 2], y <- [1 .. 3] ]', + expected: '[(1, 1), (1, 2), (1, 3), (2, 1), (2, 2), (2, 3)]', + }, + { + group: 'comprehensions', + name: 'guard between generators prunes early', + code: '[ (a, b) | a <- [1 .. 3], a != 2, b <- [1 .. 2] ]', + expected: '[(1, 1), (1, 2), (3, 1), (3, 2)]', + }, + { + group: 'comprehensions', + name: 'Pythagorean triples', + code: '[ (a, b, c) | c <- [1 .. 15], b <- [1 .. c], a <- [1 .. b], a * a + b * b == c * c ]', + expected: '[(3, 4, 5), (6, 8, 10), (5, 12, 13), (9, 12, 15)]', + }, + { + group: 'comprehensions', + name: 'quicksort via two comprehensions', + code: `let rec qsort xs = match xs with + | [] -> [] + | p :: rest -> append (qsort [ y | y <- rest, y < p ]) (p :: qsort [ y | y <- rest, y >= p ]) +in qsort [3, 1, 4, 1, 5, 9, 2, 6]`, + expected: '[1, 1, 2, 3, 4, 5, 6, 9]', + }, + { + group: 'comprehensions', + name: 'primes by trial division inside a comprehension', + code: `let rec divides d n = if n < d then false else if n == d then true else divides d (n - d) in +[ n | n <- [2 .. 20], length [ d | d <- [2 .. n - 1], divides d n ] == 0 ]`, + expected: '[2, 3, 5, 7, 11, 13, 17, 19]', + }, + { + group: 'comprehensions', + name: 'nested comprehension builds a multiplication table', + code: '[ [ r * c | c <- [1 .. 3] ] | r <- [1 .. 3] ]', + expected: '[[1, 2, 3], [2, 4, 6], [3, 6, 9]]', + }, + { + group: 'comprehensions', + name: 'wildcard generator counts elements', + code: 'sum [ 1 | _ <- [10, 20, 30, 40] ]', + expected: '4', + }, ] export function runCase(tc: TestCase): TestResult { diff --git a/projects/aether-lang-c3d8/src/pages/About.tsx b/projects/aether-lang-c3d8/src/pages/About.tsx index c91f59e1..f21ce50f 100644 --- a/projects/aether-lang-c3d8/src/pages/About.tsx +++ b/projects/aether-lang-c3d8/src/pages/About.tsx @@ -7,7 +7,7 @@ const STAGES = [ { n: 2, title: 'Parser', - body: 'A Pratt (precedence-climbing) parser builds the AST. Function application is juxtaposition and binds tighter than every operator; let / fn / if are prefix forms. Multi-argument functions desugar to curried lambdas, list comprehensions [ e | x <- xs, guard ] desugar to concat / map / if, and monadic do { x <- e; … } desugars to bind e (fn x -> …) — so each is typed and compiled like any other core expression.', + body: 'A Pratt (precedence-climbing) parser builds the AST. Function application is juxtaposition and binds tighter than every operator; let / fn / if are prefix forms. Multi-argument functions desugar to curried lambdas; list comprehensions [ e | q… ] desugar to concat / map / if / let / match — a qualifier is a generator pat <- xs (a refutable pattern drops the non-matches via a wildcard arm, the list-monad fail), a let pat = e binding, or a boolean guard — while range literals [a .. b] and [a, s .. b] desugar to the enumFromTo / enumFromThenTo prelude functions; and monadic do { x <- e; … } desugars to bind e (fn x -> …). Each is typed and compiled like any other core expression, so the type checker and all three backends never see the sugar.', }, { n: 3, @@ -198,6 +198,17 @@ export default function About() { usefulness algorithm — non-exhaustive matches are reported with a concrete witness pattern, and unreachable clauses are flagged. +
  • + List comprehensions & ranges.{' '} + [ e | q… ] supports generators (pat <- xs, where a{' '} + refutable pattern like Som x silently drops the non-matches),{' '} + let-qualifiers and boolean guards; range literals write an enumeration as{' '} + [a .. b] or, with a step, [a, s .. b]. All of it is pure + parser sugar — it lowers to concat/map/match and + the enumFromTo prelude — so the type checker and all three backends see only + ordinary core, and a 200-program differential fuzzer checks each comprehension against an + independent reference evaluator. +
  • Aether Check is from-scratch property-based testing (QuickCheck) driven by the type checker: it generates random inputs from each prop_…{' '} diff --git a/projects/aether-lang-c3d8/src/pages/Tests.tsx b/projects/aether-lang-c3d8/src/pages/Tests.tsx index c5164932..07527d43 100644 --- a/projects/aether-lang-c3d8/src/pages/Tests.tsx +++ b/projects/aether-lang-c3d8/src/pages/Tests.tsx @@ -5,6 +5,8 @@ import { runPropertySuite } from '../lang/propertySuite.ts' import type { PropSelfResult } from '../lang/propertySuite.ts' import { runOptimizerFuzz, runSpecConstrFuzz, runSroaFuzz } from '../lang/optFuzz.ts' import type { OptFuzzResult, SpecConstrFuzzResult, SroaFuzzResult } from '../lang/optFuzz.ts' +import { runComprehensionFuzz } from '../lang/comprehensionFuzz.ts' +import type { ComprehensionFuzzResult } from '../lang/comprehensionFuzz.ts' import { runSemanticsSelfCheck } from '../lang/semanticsSelfCheck.ts' import type { SemSelfResult } from '../lang/semanticsSelfCheck.ts' @@ -14,6 +16,7 @@ export default function Tests() { const [optFuzz, setOptFuzz] = useState(null) const [scFuzz, setScFuzz] = useState(null) const [sroaFuzz, setSroaFuzz] = useState(null) + const [compFuzz, setCompFuzz] = useState(null) const [semResults, setSemResults] = useState(null) const [running, setRunning] = useState(false) @@ -26,6 +29,7 @@ export default function Tests() { setOptFuzz(runOptimizerFuzz()) setScFuzz(runSpecConstrFuzz()) setSroaFuzz(runSroaFuzz()) + setCompFuzz(runComprehensionFuzz()) setSemResults(runSemanticsSelfCheck()) setRunning(false) }, 10) @@ -285,6 +289,48 @@ export default function Tests() { )} + {compFuzz && ( +
    +
    +

    + Comprehension fuzz — list-comprehension & range desugaring soundness{' '} + + {compFuzz.passed}/{compFuzz.total} + +

    +

    + {compFuzz.total} randomly generated list comprehensions — nested generators,{' '} + inclusive and stepped ranges ([a .. b],{' '} + [a, s .. b]), boolean guards, let-qualifiers and{' '} + pattern generators (tuple, Som x, h :: _).{' '} + {compFuzz.patterned} used a pattern generator and {compFuzz.refutable} a{' '} + refutable one that must drop the non-matching elements (the + list-monad fail). Each is proved sound two ways: the compiled program's{' '} + VM result equals an independent reference — the same comprehension + evaluated by nested iteration in TypeScript, never touching the parser's desugaring — + and that value re-appears on the JavaScript backend (VM ≡ JS). Across + the batch it produced {compFuzz.elements.toLocaleString()} list elements. + Deterministic, so this badge is stable. +

    + {compFuzz.failures.length > 0 && ( + + + {compFuzz.failures.map((f, i) => ( + + + + + ))} + +
    ✗ + {f.detail} +
    {f.code}
    +
    + )} +
    +
    + )} + {!results && (

    Press “Run all tests” to execute the suite live.

    )}