lemmascript - npm Package Compare versions

Comparing version 0.5.13 to 0.5.14

package.json

 {
   "name": "lemmascript",
-  "version": "0.5.13",
+  "version": "0.5.14",
   "description": "A verification toolchain for TypeScript — generates Lean 4 or Dafny from annotated TS",
@@ -35,3 +35,3 @@ "type": "module",
   },
-  "homepage": "https://lemmascript.com",
+  "homepage": "https://lemmascript.org",
   "keywords": [
@@ -38,0 +38,0 @@ "lemmascript",

tools/dist/dafny-emit.js

@@ -5,3 +5,3 @@ /**
 import { usesName, usesNameInDecl } from "./ir.js";
-import { freshName } from "./names.js";
+import { freshName, userNames } from "./names.js";
 import { renameFreeVar } from "./transform.js";
@@ -46,3 +46,3 @@ /** Fresh binder for a comprehension wrapping the given subexpressions: `base`
         }
-        case "user": return ty.name;
+        case "user": return escapeName(ty.name);
         case "fn": return `(${ty.params.map(tyToDafny).join(", ")}) -> ${tyToDafny(ty.result)}`;
@@ -80,25 +80,79 @@ // Out-of-subset (`any`/`unknown`); opaque so real ops on it fail loudly
 // The Dafny out-parameter name for the method currently being emitted. Default
-// `res`, but bumped (e.g. `res_`) when a parameter is named `res` — set by
-// methodHeader and reset per decl. `\result` in an ensures must use the *same*
-// name, so escapeName routes it here.
+// `res`, but bumped (e.g. `res'`) when the method's own scope uses `res` — set
+// by methodHeader and reset per decl. `\result` in an ensures must use the
+// *same* name, so escapeName routes it here.
 let _resultName = "res";
+// ── Dafny name allocation ──────────────────────────────────
+//
+// freshName (names.ts) freshens in the *raw TS* namespace — but that is not the
+// namespace Dafny sees. Escaping maps `_x`→`i_x` and keyword `match`→`match_`,
+// so two raw-distinct names can collapse *after* escaping: a raw-freshened temp
+// `_t0'`→`i_t0'` colliding with a user `_t0` that escaped-and-primed to `i_t0'`.
+// So Dafny hygiene is a second allocator, layered at emission: escape to a base,
+// then freshen against the names already claimed in the Dafny namespace. User
+// names are allocated up front (Dafny-safe ones kept exact); generated names are
+// allocated on first sight and cached so a decl and its references agree. Reset
+// per file. (The raw freshName layer stays — Lean has a different escaping story.)
+function dafnyBaseName(name) {
+    if (DAFNY_KEYWORDS.has(name))
+        return `${name}_`;
+    if (name.startsWith("_"))
+        return `i${name}`; // Dafny forbids leading `_`
+    return name;
+}
+let _userDafnyNames = new Map();
+let _generatedDafnyNames = new Map();
+let _takenDafnyNames = new Set();
+/** `base`, primed until free in the Dafny namespace. A prime can't occur in a
+ *  TS identifier, so priming always leaves user-name space. */
+function freshDafnyName(base) {
+    let out = base;
+    while (_takenDafnyNames.has(out))
+        out += "'";
+    return out;
+}
+function resetDafnyNameCache() {
+    _userDafnyNames = new Map();
+    _generatedDafnyNames = new Map();
+    _takenDafnyNames = new Set();
+    const raws = [...userNames()].sort();
+    // Dafny-safe source names keep their spelling; names that must mangle are then
+    // freshened in the emitted namespace (safe-first, sorted → deterministic).
+    for (const raw of raws)
+        if (dafnyBaseName(raw) === raw) {
+            _userDafnyNames.set(raw, raw);
+            _takenDafnyNames.add(raw);
+        }
+    for (const raw of raws)
+        if (dafnyBaseName(raw) !== raw) {
+            const emitted = freshDafnyName(dafnyBaseName(raw));
+            _userDafnyNames.set(raw, emitted);
+            _takenDafnyNames.add(emitted);
+        }
+}
 function escapeName(name) {
-    // \result is carried through the IR as the var name "\\result"; render it
-    // as the current method's out-parameter name.
+    // \result is carried through the IR as var "\\result"; render it as the
+    // current method's out-parameter name (chosen locally by methodHeader).
     if (name === "\\result")
         return _resultName;
-    let out = name;
-    if (DAFNY_KEYWORDS.has(name))
-        out = `${name}_`;
-    // Dafny doesn't allow identifiers starting with _
-    else if (name.startsWith("_"))
-        out = `i${name}`;
-    else
-        return name;
-    // Mangling must stay injective: the mangled form may itself be a name the
-    // user wrote (`match` → `match_` beside a real `match_`, `_x` → `i_x` beside
-    // a real `i_x`), silently merging two distinct variables. `freshName` primes
-    // it clear of user-name space (a prime can't occur in a TS identifier).
-    return freshName(out);
+    const user = _userDafnyNames.get(name);
+    if (user !== undefined)
+        return user;
+    return escapeGeneratedName(name);
 }
+/** Allocate a toolchain-generated name (an ANF temp, a comprehension binder, a
+ *  companion `_ensures` lemma). Escapes to a base, then freshens in the Dafny
+ *  namespace so it can't collapse onto an escaped user name. Bypasses the user
+ *  map on purpose: the raw name is synthesized, so it must be freshened *away
+ *  from* a same-spelled user name, not aliased onto it. Cached so a declaration
+ *  and its references render identically. */
+function escapeGeneratedName(name) {
+    const cached = _generatedDafnyNames.get(name);
+    if (cached !== undefined)
+        return cached;
+    const emitted = freshDafnyName(dafnyBaseName(name));
+    _generatedDafnyNames.set(name, emitted);
+    _takenDafnyNames.add(emitted);
+    return emitted;
+}
 /** Format a typed parameter list for Dafny: "x: int, y: seq<int>" */
@@ -145,3 +199,3 @@ function paramList(params) {
         const ann = dty === "string" ? "" : `: ${dty}`;
-        vars.push(`${body.var}${ann}`);
+        vars.push(`${escapeName(body.var)}${ann}`);
         body = body.body;
@@ -344,3 +398,3 @@ }
                     // Local check — only this comprehension's own operands can collide.
-                    const k = freshBinder("k", e.obj, e.args[0]);
+                    const k = escapeName(freshBinder("k", e.obj, e.args[0]));
                     return `(map ${k} | ${k} in ${obj} && ${k} != ${args[0]} :: ${obj}[${k}])`;
@@ -493,5 +547,7 @@ }
             const obj = emitExpr(e.obj);
-            if (e.field === "size" || e.field === "length" || e.field === "collectionSize")
+            // `size`/`length`/`keys` are collection intrinsics unless the transform
+            // proved this is a declared datatype field (then project it).
+            if (!e.datatypeField && (e.field === "size" || e.field === "length" || e.field === "collectionSize"))
                 return `|${obj}|`;
-            if (e.field === "keys")
+            if (!e.datatypeField && e.field === "keys")
                 return `${obj}.Keys`;
@@ -728,10 +784,10 @@ if (e.field === "toNat")
             });
-            return `datatype ${d.name}${tp} = ${ctors.join(" | ")}`;
+            return `datatype ${escapeName(d.name)}${tp} = ${ctors.join(" | ")}`;
         }
         case "structure": {
             const tp = d.typeParams?.length ? `<${d.typeParams.join(", ")}>` : "";
-            return `datatype ${d.name}${tp} = ${d.name}(${paramList(d.fields)})`;
+            return `datatype ${escapeName(d.name)}${tp} = ${escapeName(d.name)}(${paramList(d.fields)})`;
         }
         case "type-alias": {
-            return `type ${d.name} = ${tyToDafny(d.target)}`;
+            return `type ${escapeName(d.name)} = ${tyToDafny(d.target)}`;
         }
@@ -741,7 +797,7 @@ case "opaque-type": {
             // that derive structural equality. Never constructed or destructured.
-            return `type ${d.name}(==)`;
+            return `type ${escapeName(d.name)}(==)`;
         }
         case "def": {
             const tp = d.typeParams.length > 0 ? `<${d.typeParams.join(", ")}>` : "";
-            const lines = [`function ${d.name}${tp}(${paramList(d.params)}): ${tyToDafny(d.returnType)}`];
+            const lines = [`function ${escapeName(d.name)}${tp}(${paramList(d.params)}): ${tyToDafny(d.returnType)}`];
             for (const r of d.requires)
@@ -759,3 +815,3 @@ lines.push(`  requires ${emitExpr(r)}`);
                 lines.push("");
-                lines.push(`lemma ${d.name}_ensures${lemmaTP}(${paramList(d.params)})`);
+                lines.push(`lemma ${escapeGeneratedName(`${d.name}_ensures`)}${lemmaTP}(${paramList(d.params)})`);
                 for (const r of d.requires)
@@ -772,3 +828,3 @@ lines.push(`  requires ${emitExpr(r)}`);
             const tp = d.typeParams.length > 0 ? `<${d.typeParams.join(", ")}>` : "";
-            const lines = [`function ${d.name}${tp}(${paramList(d.params)}): ${tyToDafny(d.returnType)}`];
+            const lines = [`function ${escapeName(d.name)}${tp}(${paramList(d.params)}): ${tyToDafny(d.returnType)}`];
             for (const r of d.requires)
@@ -787,3 +843,3 @@ lines.push(`  requires ${emitExpr(r)}`);
             const tp = d.typeParams.length > 0 ? `<${d.typeParams.join(", ")}>` : "";
-            const lines = [methodHeader(`method ${d.name}${tp}`, d.params, d.returnType, d)];
+            const lines = [methodHeader(`method ${escapeName(d.name)}${tp}`, d.params, d.returnType, d)];
             for (const r of d.requires)
@@ -801,3 +857,3 @@ lines.push(`  requires ${emitExpr(r)}`);
         case "class": {
-            const lines = [`class ${d.name} {`];
+            const lines = [`class ${escapeName(d.name)} {`];
             for (const f of d.fields) {
@@ -809,3 +865,3 @@ lines.push(`  var ${escapeName(f.name)}: ${tyToDafny(f.type)}`);
             for (const m of d.methods) {
-                lines.push(`  ${methodHeader(`method ${m.name}`, m.params, m.returnType, m)}`);
+                lines.push(`  ${methodHeader(`method ${escapeName(m.name)}`, m.params, m.returnType, m)}`);
                 for (const r of m.requires)
@@ -1265,17 +1321,13 @@ lines.push(`    requires ${emitExpr(r)}`);
 const CTOR_MAP = { "some": "Some", "none": "None" };
-function translatePattern(pattern) {
-    if (pattern === "_")
+function translatePattern(p) {
+    if (p.kind === "wild")
         return "_";
-    const m = pattern.match(/^\.(\w+)\s*(.*)$/);
-    if (!m)
-        return pattern;
-    const ctorName = CTOR_MAP[m[1]] ?? escapeName(m[1]);
-    const fields = m[2].trim();
-    if (!fields)
+    const ctorName = CTOR_MAP[p.ctor] ?? escapeName(p.ctor);
+    if (p.binders.length === 0)
         return ctorName;
-    const fieldNames = fields.split(/\s+/).map(escapeName);
-    return `${ctorName}(${fieldNames.join(", ")})`;
+    return `${ctorName}(${p.binders.map(escapeName).join(", ")})`;
 }
 export function emitDafnyFile(file, tsFileName, opts) {
     _useSafeSlice = !!opts?.safeSlice;
+    resetDafnyNameCache();
     buildRecordCtorMap(file.decls);
@@ -1282,0 +1334,0 @@ _neededPreambles.clear();

tools/dist/ir.js

@@ -7,2 +7,15 @@ /**
  */
+export const pWild = () => ({ kind: "wild" });
+export const pCtor = (ctor, ...binders) => ({ kind: "ctor", ctor, binders });
+/** Binder identifiers a pattern introduces (`[]` for wildcard / nullary ctor). */
+export function patternBinders(p) {
+    return p.kind === "ctor" ? p.binders : [];
+}
+export function patternCtor(p) {
+    return p.kind === "ctor" ? p.ctor : null;
+}
+/** Does the pattern bind `name`? */
+export function patternBinds(p, name) {
+    return patternBinders(p).includes(name);
+}
 export function anyExpr(e, pred) {
@@ -79,6 +92,30 @@ if (pred(e))
 }
-/** Does a declaration's spec (requires/ensures) or body reference `name`? The
- *  scope a method's out-parameter binder must dodge, shared by both emitters. */
+/** Names a statement tree *binds, targets, or introduces* — `let`/`let-bind`/
+ *  `ghostLet` names, `assign`/`bind`/`ghostAssign` targets, `for-in` indices,
+ *  and `match`-arm pattern binders — recursing through nested blocks. Distinct
+ *  from `usesNameInStmts` (expression references only): an unread or assign-only
+ *  local still duplicate-declares against a method's out-parameter in Dafny. */
+export function bindsNameInStmts(stmts, name) {
+    return stmts.some(s => {
+        switch (s.kind) {
+            case "let":
+            case "let-bind":
+            case "ghostLet": return s.name === name;
+            case "assign":
+            case "bind":
+            case "ghostAssign": return s.target === name;
+            case "forin": return s.idx === name || bindsNameInStmts(s.body, name);
+            case "if": return bindsNameInStmts(s.then, name) || bindsNameInStmts(s.else, name);
+            case "while": return bindsNameInStmts(s.body, name);
+            case "match": return s.arms.some(a => patternBinds(a.pattern, name) || bindsNameInStmts(a.body, name));
+            default: return false;
+        }
+    });
+}
+/** Every occurrence of `name` a method's out-parameter binder must dodge —
+ *  referenced in a spec (requires/ensures) or body, *or* bound/targeted anywhere
+ *  in the body (an unread local still duplicate-declares). Both emitters share it. */
 export function usesNameInDecl(requires, ensures, body, name) {
-    return requires.some(e => usesName(e, name)) || ensures.some(e => usesName(e, name)) || usesNameInStmts(body, name);
+    return requires.some(e => usesName(e, name)) || ensures.some(e => usesName(e, name))
+        || usesNameInStmts(body, name) || bindsNameInStmts(body, name);
 }

tools/dist/lean-emit.js

@@ -5,3 +5,3 @@ /**
  */
-import { anyExpr, usesNameInDecl } from "./ir.js";
+import { anyExpr, usesNameInDecl, patternBinders } from "./ir.js";
 import { freshName } from "./names.js";
@@ -182,2 +182,6 @@ // ── Ty → Lean type string ──────────────────────────────────
 let _boolCtx = false;
+/** Render a match pattern to Lean syntax: `_`, `.none`, `.some x`, `.syn seq`. */
+function renderLeanPattern(p) {
+    return p.kind === "wild" ? "_" : "." + [p.ctor, ...p.binders].join(" ");
+}
 // A Bool-valued atom that does NOT coerce to Prop: an inlined union discriminator
@@ -470,3 +474,3 @@ // (lowered to a match-bool `match x with | .C .. => true | _ => false`) or a raw
             // bleed into the last `.none` case without explicit bracketing.
-            const arms = e.arms.map(a => `| ${a.pattern} => ${emitExpr(a.body)}`);
+            const arms = e.arms.map(a => `| ${renderLeanPattern(a.pattern)} => ${emitExpr(a.body)}`);
             const scrut = typeof e.scrutinee === "string" ? e.scrutinee : emitExpr(e.scrutinee);
@@ -563,6 +567,6 @@ return `(match ${scrut} with ${arms.join(" ")})`;
             if (s.arms.length === 2) {
-                const someArm = s.arms.find(a => a.pattern.startsWith(".some "));
-                const noneArm = s.arms.find(a => a.pattern === ".none");
+                const someArm = s.arms.find(a => a.pattern.kind === "ctor" && a.pattern.ctor === "some");
+                const noneArm = s.arms.find(a => a.pattern.kind === "ctor" && a.pattern.ctor === "none");
                 if (someArm && noneArm) {
-                    const boundVar = someArm.pattern.slice(6); // strip ".some "
+                    const boundVar = patternBinders(someArm.pattern)[0]; // ".some x" ⇒ "x"
                     const hName = `h_${scrut.replace(/[^a-zA-Z0-9_]/g, "_")}`;
@@ -592,3 +596,3 @@ const lines = [
             for (const arm of s.arms) {
-                lines.push(`${pad}| ${arm.pattern} =>`);
+                lines.push(`${pad}| ${renderLeanPattern(arm.pattern)} =>`);
                 if (arm.body.length === 0) {
@@ -752,3 +756,3 @@ lines.push(`${pad}  pure ()`);
             for (const arm of e.arms) {
-                lines.push(`${pad}| ${arm.pattern} =>`);
+                lines.push(`${pad}| ${renderLeanPattern(arm.pattern)} =>`);
                 lines.push(emitPureExpr(arm.body, indent + 1));
@@ -755,0 +759,0 @@ }

tools/dist/names.js

@@ -37,2 +37,7 @@ /**
 }
+/** The raw user identifiers, for a backend that needs to allocate its own
+ *  emitted names against them (e.g. Dafny escaping — see dafny-emit). */
+export function userNames() {
+    return [..._userNames];
+}
 /** A toolchain-internal name: `base` verbatim, primed on collision. The one
@@ -39,0 +44,0 @@ *  place the priming rule lives. `taken` says what counts as a collision —

tools/dist/narrow.js

@@ -420,2 +420,22 @@ /**
 }
+/** Apply an optional chain's steps (field / index / call) to a base expr —
+ *  shared by `ruleOptChain` (base = binder) and `ruleOptChainIndex` (base = arr[i]). */
+function applyChain(body, chain) {
+    for (const step of chain) {
+        if (step.kind === "field")
+            body = { kind: "field", obj: body, field: step.name, ty: step.ty };
+        else if (step.kind === "index")
+            body = { kind: "index", obj: body, idx: step.idx, ty: step.ty };
+        else
+            body = { kind: "call", fn: body, args: step.args, ty: step.ty, callKind: step.callKind };
+    }
+    return body;
+}
+/** `0 <= idx && idx < arr.length` — the in-bounds guard for an array index. */
+function arrayBoundsCond(arr, idx) {
+    const len = { kind: "field", obj: arr, field: "length", ty: { kind: "int" } };
+    const lo = { kind: "binop", op: "<=", left: { kind: "num", value: 0, ty: { kind: "int" } }, right: idx, ty: { kind: "bool" } };
+    const hi = { kind: "binop", op: "<", left: idx, right: len, ty: { kind: "bool" } };
+    return { kind: "binop", op: "&&", left: lo, right: hi, ty: { kind: "bool" } };
+}
 /** Rule (expression): `left ?? right` — nullish coalescing.
@@ -452,7 +472,3 @@ *  → `someMatch left { Some(_v) => _v, None => right }`.
         return null;
-    const idx = e.left.idx;
-    const len = { kind: "field", obj: e.left.obj, field: "length", ty: { kind: "int" } };
-    const lo = { kind: "binop", op: "<=", left: { kind: "num", value: 0, ty: { kind: "int" } }, right: idx, ty: { kind: "bool" } };
-    const hi = { kind: "binop", op: "<", left: idx, right: len, ty: { kind: "bool" } };
-    const cond = { kind: "binop", op: "&&", left: lo, right: hi, ty: { kind: "bool" } };
+    const cond = arrayBoundsCond(e.left.obj, e.left.idx);
     return { kind: "conditional", cond, then: e.left, else: e.right, ty: e.ty };
@@ -475,19 +491,4 @@ }
         return null;
-    const idx = e.obj.idx;
-    const len = { kind: "field", obj: e.obj.obj, field: "length", ty: { kind: "int" } };
-    const lo = { kind: "binop", op: "<=", left: { kind: "num", value: 0, ty: { kind: "int" } }, right: idx, ty: { kind: "bool" } };
-    const hi = { kind: "binop", op: "<", left: idx, right: len, ty: { kind: "bool" } };
-    const cond = { kind: "binop", op: "&&", left: lo, right: hi, ty: { kind: "bool" } };
-    let body = e.obj; // arr[i] — in bounds under `cond`
-    for (const step of e.chain) {
-        if (step.kind === "field") {
-            body = { kind: "field", obj: body, field: step.name, ty: step.ty };
-        }
-        else if (step.kind === "index") {
-            body = { kind: "index", obj: body, idx: step.idx, ty: step.ty };
-        }
-        else {
-            body = { kind: "call", fn: body, args: step.args, ty: step.ty, callKind: step.callKind };
-        }
-    }
+    const cond = arrayBoundsCond(e.obj.obj, e.obj.idx);
+    const body = applyChain(e.obj, e.chain); // arr[i] — in bounds under `cond`
     const undef = { kind: "var", name: "undefined", ty: { kind: "void" } };
@@ -507,14 +508,3 @@ return { kind: "conditional", cond, then: body, else: undef, ty: e.ty };
     const binder = freshName(`_oc${_ocCounter++}_val`);
-    let body = { kind: "var", name: binder, ty: innerTy };
-    for (const step of e.chain) {
-        if (step.kind === "field") {
-            body = { kind: "field", obj: body, field: step.name, ty: step.ty };
-        }
-        else if (step.kind === "index") {
-            body = { kind: "index", obj: body, idx: step.idx, ty: step.ty };
-        }
-        else {
-            body = { kind: "call", fn: body, args: step.args, ty: step.ty, callKind: step.callKind };
-        }
-    }
+    const body = applyChain({ kind: "var", name: binder, ty: innerTy }, e.chain);
     const noneBody = { kind: "var", name: "undefined", ty: { kind: "void" } };
@@ -611,17 +601,18 @@ return {
 }
-/** Extract an optional check from any position in an `&&` chain.
- *  `(x !== undefined && b) && c` → { check, restCond: b && c }.
- *  `a && (x !== undefined)`     → { check, restCond: a }.
- *  Conjunct order doesn't carry semantic weight, so either side is fine. */
-function extractLeftmostOptionalCheck(cond) {
+/** Find the leftmost `parse`-matching conjunct anywhere in an `&&` chain,
+ *  returning it plus the remaining conjunction. Conjunct order doesn't carry
+ *  semantic weight, so either side is fine. Shared by the optional and
+ *  Array.isArray chain extractors — they differ only in `parse`.
+ *  `(x !== undefined && b) && c` → { check, restCond: b && c }. */
+function extractLeftmostCheck(cond, parse) {
     if (cond.kind !== "binop" || cond.op !== "&&")
         return null;
-    const leftCheck = parseSimpleOptionalCheck(cond.left);
-    if (leftCheck && !leftCheck.negated)
-        return { check: leftCheck, restCond: cond.right };
-    const rightCheck = parseSimpleOptionalCheck(cond.right);
-    if (rightCheck && !rightCheck.negated)
-        return { check: rightCheck, restCond: cond.left };
+    const left = parse(cond.left);
+    if (left)
+        return { check: left, restCond: cond.right };
+    const right = parse(cond.right);
+    if (right)
+        return { check: right, restCond: cond.left };
     if (cond.left.kind === "binop" && cond.left.op === "&&") {
-        const inner = extractLeftmostOptionalCheck(cond.left);
+        const inner = extractLeftmostCheck(cond.left, parse);
         if (inner)
@@ -631,3 +622,3 @@ return { check: inner.check, restCond: { ...cond, left: inner.restCond } };
     if (cond.right.kind === "binop" && cond.right.op === "&&") {
-        const inner = extractLeftmostOptionalCheck(cond.right);
+        const inner = extractLeftmostCheck(cond.right, parse);
         if (inner)
@@ -638,2 +629,9 @@ return { check: inner.check, restCond: { ...cond, right: inner.restCond } };
 }
+/** `&&`-chain extractor for a positive optional check. */
+function extractLeftmostOptionalCheck(cond) {
+    return extractLeftmostCheck(cond, e => {
+        const c = parseSimpleOptionalCheck(e);
+        return c && !c.negated ? c : null;
+    });
+}
 /** Rule: `if (x !== undefined && rest) then` (no else) where x is a pure
@@ -755,27 +753,7 @@ *  access path.
 }
-/** Mirror of `extractLeftmostOptionalCheck` for synth-array-union checks:
- *  finds `Array.isArray(path)` somewhere in a `&&` chain, returns it plus
- *  the remaining conjunction. The check must be the positive form (negated
- *  `!Array.isArray(...)` would narrow to the wrong variant for then-body
- *  consumers, so we leave those to the existing untouched-conditional path). */
+/** `&&`-chain extractor for `Array.isArray(path)` (positive form only — a negated
+ *  `!Array.isArray(...)` would narrow to the wrong variant for then-body consumers,
+ *  so those are left to the untouched-conditional path). */
 function extractLeftmostArrayIsArrayCheck(cond) {
-    if (cond.kind !== "binop" || cond.op !== "&&")
-        return null;
-    const leftCheck = parseArrayIsArrayCall(cond.left);
-    if (leftCheck)
-        return { check: leftCheck, restCond: cond.right };
-    const rightCheck = parseArrayIsArrayCall(cond.right);
-    if (rightCheck)
-        return { check: rightCheck, restCond: cond.left };
-    if (cond.left.kind === "binop" && cond.left.op === "&&") {
-        const inner = extractLeftmostArrayIsArrayCheck(cond.left);
-        if (inner)
-            return { check: inner.check, restCond: { ...cond, left: inner.restCond } };
-    }
-    if (cond.right.kind === "binop" && cond.right.op === "&&") {
-        const inner = extractLeftmostArrayIsArrayCheck(cond.right);
-        if (inner)
-            return { check: inner.check, restCond: { ...cond, right: inner.restCond } };
-    }
-    return null;
+    return extractLeftmostCheck(cond, parseArrayIsArrayCall);
 }
@@ -782,0 +760,0 @@ /** Detect `x.kind === "variant"`, `'key' in x`, or `Array.isArray(x)` (synth

tools/dist/peephole.js

@@ -0,1 +1,2 @@
+import { patternCtor, patternBinders } from "./ir.js";
 // ── Generic walkers (same shape as transform.ts) ─────────────
@@ -47,10 +48,8 @@ function mapExpr(e, f) {
 }
-/** Parse Some-arm pattern like ".some _val" — returns binder name, or null for ".some _" or unparseable. */
-function parseSomeBinder(pattern) {
-    if (!pattern.startsWith(".some"))
+/** Binder of a Some arm — its name, or null for `.some _` / a non-`some` pattern. */
+function parseSomeBinder(p) {
+    if (patternCtor(p) !== "some")
         return null;
-    const rest = pattern.slice(5).trim();
-    if (rest === "" || rest === "_")
-        return null;
-    return rest.split(/\s+/)[0];
+    const b = patternBinders(p)[0];
+    return b === undefined || b === "_" ? null : b;
 }
@@ -61,4 +60,4 @@ /** Identify a Some/None match's arms. */
         return null;
-    const someArm = arms.find(a => a.pattern.startsWith(".some"));
-    const noneArm = arms.find(a => a.pattern === ".none");
+    const someArm = arms.find(a => patternCtor(a.pattern) === "some");
+    const noneArm = arms.find(a => patternCtor(a.pattern) === "none");
     if (!someArm || !noneArm)
@@ -65,0 +64,0 @@ return null;

No alert changes

Improved metrics

Total package byte prevSize

621910

0.66%

Lines of code

12170

0.6%

No dependency changes