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.

    )}