From 05bd36f5750c02997cadd3a093bd25e80e0435c9 Mon Sep 17 00:00:00 2001 From: Nada Amin Date: Sat, 11 Jul 2026 21:27:16 -0400 Subject: [PATCH 1/2] narrow (ternary sibling of the if-return optChain-compare rule) --- tools/src/narrow.ts | 72 ++++++++++++++++++++++++++++++++++++-------- tools/src/resolve.ts | 18 ++++++++++- 2 files changed, 76 insertions(+), 14 deletions(-) diff --git a/tools/src/narrow.ts b/tools/src/narrow.ts index 7988f5a..364289b 100644 --- a/tools/src/narrow.ts +++ b/tools/src/narrow.ts @@ -101,6 +101,11 @@ const parseSimpleOptionalCheck = parseOptionalCheck; // ── Walkers ────────────────────────────────────────────────── function walkExpr(e: TExpr): TExpr { + // Fires on the raw conditional before `recurseExpr` rewrites the cond's + // optChain to a someMatch (which would leave `optChain === lit` unmatchable); + // it walks its own sub-branches, so recursion is preserved. + const preCond = ruleConditionalOptChainCompare(e); + if (preCond) return preCond; const r = recurseExpr(e); return ruleNullish(r) ?? ruleNullishIndex(r) ?? ruleOptChainIndex(r) ?? ruleOptChain(r) ?? ruleImplOptional(r) ?? ruleImplArrayIsArray(r) ?? ruleConditionalArrayIsArray(r) ?? ruleConditionalAndArrayIsArray(r) ?? ruleConditionalAndOptional(r) ?? ruleConditionalOptionalSimple(r) ?? ruleConditionalInMap(r) ?? ruleConditionalOptionalTruthy(r) ?? r; } @@ -351,21 +356,29 @@ function ruleEarlyReturnOrChain(s: TStmt, rest: TStmt[]): TStmt | null { * discriminant narrowing). Bound-optional companion to ruleEarlyReturnConsume, * which handles only a bare presence check (`opt !== undefined`). Restricted to * `!==` so the None case is guaranteed to terminate. */ -function ruleEarlyReturnOptChainCompare(s: TStmt, rest: TStmt[]): TStmt | null { - if (s.kind !== "if") return null; - if (rest.length === 0) return null; - if (s.else.length !== 0 || !isTerminating(s.then)) return null; - const c = s.cond; - if (c.kind !== "binop" || c.op !== "!==") return null; - const oc = c.left.kind === "optChain" ? c.left : c.right.kind === "optChain" ? c.right : null; +/** Shared core of the two `x?.disc 'lit'` narrowings — the if-return + * statement form (`ruleEarlyReturnOptChainCompare`, op `!==`) and the ternary + * expression form (`ruleConditionalOptChainCompare`, op `===`). Matches an + * optional chain compared to a concrete (non-`undefined`) literal with the + * requested operator and returns the pieces both callers need: the scrutinee + * `x`, a fresh binder for its unwrapped value, and the chain re-applied to that + * binder (with the discriminant flag restored so the re-test lowers to a + * discriminant match). A `None` base makes `x?.disc` `undefined`, which never + * equals a real literal — so the presence of `x` is implied and each caller + * routes the branches accordingly. */ +function parseOptChainLitCompare(cond: TExpr, op: "===" | "!=="): { + scrutinee: TExpr; binder: string; binderTy: Ty; unwrapped: TExpr; lit: TExpr; +} | null { + if (cond.kind !== "binop" || cond.op !== op) return null; + const oc = cond.left.kind === "optChain" ? cond.left : cond.right.kind === "optChain" ? cond.right : null; if (!oc || oc.kind !== "optChain" || oc.obj.ty.kind !== "optional") return null; - const lit = c.left === oc ? c.right : c.left; - const innerTy = oc.obj.ty.inner; + const lit = cond.left === oc ? cond.right : cond.left; + if (lit.kind === "var" && lit.name === "undefined") return null; + const binderTy = oc.obj.ty.inner; const hint = binderHintFor(oc.obj); if (hint === null) return null; const binder = freshName(hint); - const binderVar: TExpr = { kind: "var", name: binder, ty: innerTy }; - const unwrapped = applyChain(binderVar, oc.chain); + const unwrapped = applyChain({ kind: "var", name: binder, ty: binderTy }, oc.chain); // applyChain rebuilds the field without the `isDiscriminant` flag resolve sets // on a direct `x.disc`; restore it when the unwrapped access is the binder // union's discriminant, so the inner guard feeds discriminant narrowing. @@ -376,13 +389,46 @@ function ruleEarlyReturnOptChainCompare(s: TStmt, rest: TStmt[]): TStmt | null { unwrapped.isDiscriminant = true; } } - const innerGuard: TExpr = { kind: "binop", op: "!==", left: unwrapped, right: lit, ty: { kind: "bool" } }; + return { scrutinee: oc.obj, binder, binderTy, unwrapped, lit }; +} + +function ruleEarlyReturnOptChainCompare(s: TStmt, rest: TStmt[]): TStmt | null { + if (s.kind !== "if") return null; + if (rest.length === 0) return null; + if (s.else.length !== 0 || !isTerminating(s.then)) return null; + const m = parseOptChainLitCompare(s.cond, "!=="); + if (!m) return null; + const innerGuard: TExpr = { kind: "binop", op: "!==", left: m.unwrapped, right: m.lit, ty: { kind: "bool" } }; // Keep `rest` as trailing statements (not an else branch) — `s.then` terminates, // so `if (g) terminate; rest` ≡ `if (g) terminate else rest`, and the trailing // form lets the ordinary early-exit rules (e.g. discriminant narrowing) fire on // the now-non-optional inner guard when `chain` is a union discriminant. const someBody: TStmt[] = [{ kind: "if", cond: innerGuard, then: s.then, else: [] }, ...rest]; - return { kind: "someMatch", scrutinee: oc.obj, binder, binderTy: innerTy, someBody, noneBody: s.then }; + return { kind: "someMatch", scrutinee: m.scrutinee, binder: m.binder, binderTy: m.binderTy, someBody, noneBody: s.then }; +} + +/** Rule (expression): `x?.disc === 'lit' ? a : b` — the conditional-expression + * analogue of `ruleEarlyReturnOptChainCompare`. Lower to a `someMatch` on `x` + * whose Some-arm re-tests the unwrapped chain and whose None-arm takes the + * else branch (a None base can never equal the literal). + * → `someMatch x { Some(binder) => (binder.disc === 'lit' ? a : b), None => b }`. + * Runs *before* `recurseExpr` rewrites the cond's optChain to a someMatch, and + * walks its own sub-branches. The Some-arm keeps `a`/`b` referencing `x`; the + * expression-someMatch lowering (transform.ts) substitutes the `x` path with + * the binder inside them. */ +function ruleConditionalOptChainCompare(e: TExpr): TExpr | null { + if (e.kind !== "conditional") return null; + const m = parseOptChainLitCompare(e.cond, "==="); + if (!m) return null; + const innerCond: TExpr = { kind: "binop", op: "===", left: m.unwrapped, right: m.lit, ty: { kind: "bool" } }; + const someBody: TExpr = { + kind: "conditional", cond: innerCond, then: walkExpr(e.then), else: walkExpr(e.else), ty: e.ty, + }; + return { + kind: "someMatch", + scrutinee: m.scrutinee, binder: m.binder, binderTy: m.binderTy, + someBody, noneBody: walkExpr(e.else), ty: e.ty, + }; } /** Rule (expression): `e !== undefined ? a : b`. */ diff --git a/tools/src/resolve.ts b/tools/src/resolve.ts index 5209a93..4a2890f 100644 --- a/tools/src/resolve.ts +++ b/tools/src/resolve.ts @@ -188,7 +188,23 @@ function detectOptionalCheck(cond: RawExpr, ctx: Ctx): { let optExpr: RawExpr | null = null; if (cond.right.kind === "var" && cond.right.name === "undefined") optExpr = cond.left; if (cond.left.kind === "var" && cond.left.name === "undefined") optExpr = cond.right; - if (!optExpr) return null; + if (!optExpr) { + // `x?.disc === 'lit'` / `x?.disc !== 'lit'` (lit not undefined): an optional + // chain compared to a concrete literal implies its base `x` is present (a + // None base makes `x?.disc` undefined, which never equals a real literal). + // `===` narrows the then-branch; `!==` narrows the else-branch. + const oc = cond.left.kind === "optChain" ? cond.left + : cond.right.kind === "optChain" ? cond.right : null; + if (oc) { + const lit = oc === cond.left ? cond.right : cond.left; + const litIsUndef = lit.kind === "var" && lit.name === "undefined"; + if (!litIsUndef) { + const inner = classifyOptExpr(oc.obj, ctx); + if (inner) return { ...inner, inThen: cond.op === "===" }; + } + } + return null; + } const inner = classifyOptExpr(optExpr, ctx); return inner ? { ...inner, inThen: cond.op === "!==" } : null; } From 5a54e16ea39d87f14884fdad33c6d05415aeacdf Mon Sep 17 00:00:00 2001 From: Nada Amin Date: Sat, 11 Jul 2026 21:59:45 -0400 Subject: [PATCH 2/2] cleanup and tests for the change --- examples/optChainDiscriminantTernary.def.lean | 28 +++++++ examples/optChainDiscriminantTernary.dfy | 75 +++++++++++++++++++ examples/optChainDiscriminantTernary.dfy.gen | 75 +++++++++++++++++++ .../optChainDiscriminantTernary.proof.lean | 27 +++++++ examples/optChainDiscriminantTernary.ts | 44 +++++++++++ .../optChainDiscriminantTernary.types.lean | 53 +++++++++++++ lakefile.lean | 3 +- tools/src/narrow.ts | 51 ++++--------- tools/src/resolve.ts | 9 +-- 9 files changed, 324 insertions(+), 41 deletions(-) create mode 100644 examples/optChainDiscriminantTernary.def.lean create mode 100644 examples/optChainDiscriminantTernary.dfy create mode 100644 examples/optChainDiscriminantTernary.dfy.gen create mode 100644 examples/optChainDiscriminantTernary.proof.lean create mode 100644 examples/optChainDiscriminantTernary.ts create mode 100644 examples/optChainDiscriminantTernary.types.lean diff --git a/examples/optChainDiscriminantTernary.def.lean b/examples/optChainDiscriminantTernary.def.lean new file mode 100644 index 0000000..230035c --- /dev/null +++ b/examples/optChainDiscriminantTernary.def.lean @@ -0,0 +1,28 @@ +/- + Generated by lsc from optChainDiscriminantTernary.ts + Do not edit — re-run `lsc gen` to regenerate. +-/ +import «optChainDiscriminantTernary.types» + +set_option loom.semantics.termination "total" +set_option loom.semantics.choice "demonic" + +method textOr (e : Option Entry) (dflt : String) return (res : String) + ensures (match e with | .some _ => false | .none => true) → res = dflt + do + return Pure.textOr e dflt + +method textOrFlipped (e : Option Entry) (dflt : String) return (res : String) + ensures (match e with | .some _ => false | .none => true) → res = dflt + do + return Pure.textOrFlipped e dflt + +method bodyOr (r : Option Rec) (dflt : String) return (res : String) + ensures (match r with | .some _ => false | .none => true) → res = dflt + do + return Pure.bodyOr r dflt + +method firstText (e : Option Entry) (dflt : String) return (res : String) + ensures (match e with | .some _ => false | .none => true) → res = dflt + do + return Pure.firstText e dflt diff --git a/examples/optChainDiscriminantTernary.dfy b/examples/optChainDiscriminantTernary.dfy new file mode 100644 index 0000000..c4f78d6 --- /dev/null +++ b/examples/optChainDiscriminantTernary.dfy @@ -0,0 +1,75 @@ +// Generated by lsc from optChainDiscriminantTernary.ts + +datatype Option = None | Some(value: T) + +datatype Entry = msg(text: string) | sep + +datatype Rec = Rec(tag: string, body: string) + +function textOr(e: Option, dflt: string): string +{ + var t := (match e { case Some(i_e_val) => (if i_e_val.msg? then Option.Some(i_e_val.text) else Option.None) case None => Option.None }); + match t { + case Some(i_oc0_val) => + i_oc0_val + case None => + dflt + } +} + +lemma textOr_ensures(e: Option, dflt: string) + ensures ((match e { case Some(i_) => false case None => true }) ==> (textOr(e, dflt) == dflt)) +{ +} + +function textOrFlipped(e: Option, dflt: string): string +{ + var t := (match e { case Some(i_e_val) => (if i_e_val.msg? then Option.Some(i_e_val.text) else Option.None) case None => Option.None }); + match t { + case Some(i_oc1_val) => + i_oc1_val + case None => + dflt + } +} + +lemma textOrFlipped_ensures(e: Option, dflt: string) + ensures ((match e { case Some(i_) => false case None => true }) ==> (textOrFlipped(e, dflt) == dflt)) +{ +} + +function bodyOr(r: Option, dflt: string): string +{ + var b := (match r { case Some(i_r_val) => (if (i_r_val.tag == "x") then Option.Some(i_r_val.body) else Option.None) case None => Option.None }); + match b { + case Some(i_oc2_val) => + i_oc2_val + case None => + dflt + } +} + +lemma bodyOr_ensures(r: Option, dflt: string) + ensures ((match r { case Some(i_) => false case None => true }) ==> (bodyOr(r, dflt) == dflt)) +{ +} + +function firstText(e: Option, dflt: string): string +{ + match e { + case Some(i_e_val) => + match i_e_val { + case msg(i__e_val_text) => + i__e_val_text + case sep => + dflt + } + case None => + dflt + } +} + +lemma firstText_ensures(e: Option, dflt: string) + ensures ((match e { case Some(i_) => false case None => true }) ==> (firstText(e, dflt) == dflt)) +{ +} diff --git a/examples/optChainDiscriminantTernary.dfy.gen b/examples/optChainDiscriminantTernary.dfy.gen new file mode 100644 index 0000000..c4f78d6 --- /dev/null +++ b/examples/optChainDiscriminantTernary.dfy.gen @@ -0,0 +1,75 @@ +// Generated by lsc from optChainDiscriminantTernary.ts + +datatype Option = None | Some(value: T) + +datatype Entry = msg(text: string) | sep + +datatype Rec = Rec(tag: string, body: string) + +function textOr(e: Option, dflt: string): string +{ + var t := (match e { case Some(i_e_val) => (if i_e_val.msg? then Option.Some(i_e_val.text) else Option.None) case None => Option.None }); + match t { + case Some(i_oc0_val) => + i_oc0_val + case None => + dflt + } +} + +lemma textOr_ensures(e: Option, dflt: string) + ensures ((match e { case Some(i_) => false case None => true }) ==> (textOr(e, dflt) == dflt)) +{ +} + +function textOrFlipped(e: Option, dflt: string): string +{ + var t := (match e { case Some(i_e_val) => (if i_e_val.msg? then Option.Some(i_e_val.text) else Option.None) case None => Option.None }); + match t { + case Some(i_oc1_val) => + i_oc1_val + case None => + dflt + } +} + +lemma textOrFlipped_ensures(e: Option, dflt: string) + ensures ((match e { case Some(i_) => false case None => true }) ==> (textOrFlipped(e, dflt) == dflt)) +{ +} + +function bodyOr(r: Option, dflt: string): string +{ + var b := (match r { case Some(i_r_val) => (if (i_r_val.tag == "x") then Option.Some(i_r_val.body) else Option.None) case None => Option.None }); + match b { + case Some(i_oc2_val) => + i_oc2_val + case None => + dflt + } +} + +lemma bodyOr_ensures(r: Option, dflt: string) + ensures ((match r { case Some(i_) => false case None => true }) ==> (bodyOr(r, dflt) == dflt)) +{ +} + +function firstText(e: Option, dflt: string): string +{ + match e { + case Some(i_e_val) => + match i_e_val { + case msg(i__e_val_text) => + i__e_val_text + case sep => + dflt + } + case None => + dflt + } +} + +lemma firstText_ensures(e: Option, dflt: string) + ensures ((match e { case Some(i_) => false case None => true }) ==> (firstText(e, dflt) == dflt)) +{ +} diff --git a/examples/optChainDiscriminantTernary.proof.lean b/examples/optChainDiscriminantTernary.proof.lean new file mode 100644 index 0000000..d99688f --- /dev/null +++ b/examples/optChainDiscriminantTernary.proof.lean @@ -0,0 +1,27 @@ +import «optChainDiscriminantTernary.def» + +set_option loom.semantics.termination "total" +set_option loom.semantics.choice "demonic" + +-- Expression-bodied, so each method delegates to its `Pure.*` mirror; unfold it +-- and split on the optional so the discriminant/field `match` in each arm +-- reduces (mirrors truthiness.proof's optional cases). +prove_correct textOr by + loom_goals_intro + loom_unfold + all_goals (cases e <;> simp_all [Pure.textOr]) + +prove_correct textOrFlipped by + loom_goals_intro + loom_unfold + all_goals (cases e <;> simp_all [Pure.textOrFlipped]) + +prove_correct bodyOr by + loom_goals_intro + loom_unfold + all_goals (cases r <;> simp_all [Pure.bodyOr]) + +prove_correct firstText by + loom_goals_intro + loom_unfold + all_goals (cases e <;> simp_all [Pure.firstText]) diff --git a/examples/optChainDiscriminantTernary.ts b/examples/optChainDiscriminantTernary.ts new file mode 100644 index 0000000..66db1a6 --- /dev/null +++ b/examples/optChainDiscriminantTernary.ts @@ -0,0 +1,44 @@ +/** + * `x?.disc === 'lit'` narrowing in expression position — the ternary sibling of + * the `if (x?.disc !== 'lit') return` statement rule (`ruleConditionalOptChainCompare` + * / `ruleEarlyReturnOptChainCompare`, sharing `parseOptChainLitCompare`). Covers + * optChain on either side, a discriminant vs. a plain field, and the `===` + * ternary and `!==` statement forms. Mirrors flue's `classifySubmissionState` + * (`assistantEntry?.type === 'message' ? assistantEntry.message : undefined`). + */ + +type Entry = { kind: 'msg'; text: string } | { kind: 'sep' }; +type Rec = { tag: string; body: string }; + +// `===` ternary, optChain on the left, discriminant field. +export function textOr(e: Entry | undefined, dflt: string): string { + //@ verify + //@ ensures e === undefined ==> \result === dflt + const t = e?.kind === 'msg' ? e.text : undefined; + return t ?? dflt; +} + +// optChain on the right (`'lit' === x?.disc`). +export function textOrFlipped(e: Entry | undefined, dflt: string): string { + //@ verify + //@ ensures e === undefined ==> \result === dflt + const t = 'msg' === e?.kind ? e.text : undefined; + return t ?? dflt; +} + +// Plain (non-discriminant) field on a record — the unwrapped guard stays a field +// read, not a discriminant test. +export function bodyOr(r: Rec | undefined, dflt: string): string { + //@ verify + //@ ensures r === undefined ==> \result === dflt + const b = r?.tag === 'x' ? r.body : undefined; + return b ?? dflt; +} + +// `!==` statement form (early return) — exercises the shared helper's other arm. +export function firstText(e: Entry | undefined, dflt: string): string { + //@ verify + //@ ensures e === undefined ==> \result === dflt + if (e?.kind !== 'msg') return dflt; + return e.text; +} diff --git a/examples/optChainDiscriminantTernary.types.lean b/examples/optChainDiscriminantTernary.types.lean new file mode 100644 index 0000000..5f690b7 --- /dev/null +++ b/examples/optChainDiscriminantTernary.types.lean @@ -0,0 +1,53 @@ +/- + Generated by lsc — Lean types and pure function mirrors. +-/ +import LemmaScript + +inductive Entry where + | msg (text : String) : Entry + | sep : Entry +deriving Repr, Inhabited + +structure Rec where + tag : String + body : String +deriving Repr, Inhabited, DecidableEq + +namespace Pure + +def textOr (e : Option Entry) (dflt : String) : String := + let t := (match e with | .some _e_val => if (match _e_val with | .msg .. => true | _ => false) then Option.some (match _e_val with | .msg _v => _v | _ => (default : String)) else Option.none | .none => Option.none) + match t with + | .some _oc0_val => + _oc0_val + | .none => + dflt + +def textOrFlipped (e : Option Entry) (dflt : String) : String := + let t := (match e with | .some _e_val => if (match _e_val with | .msg .. => true | _ => false) then Option.some (match _e_val with | .msg _v => _v | _ => (default : String)) else Option.none | .none => Option.none) + match t with + | .some _oc1_val => + _oc1_val + | .none => + dflt + +def bodyOr (r : Option Rec) (dflt : String) : String := + let b := (match r with | .some _r_val => if _r_val.tag = "x" then Option.some _r_val.body else Option.none | .none => Option.none) + match b with + | .some _oc2_val => + _oc2_val + | .none => + dflt + +def firstText (e : Option Entry) (dflt : String) : String := + match e with + | .some _e_val => + match _e_val with + | .msg __e_val_text => + __e_val_text + | .sep => + dflt + | .none => + dflt + +end Pure diff --git a/lakefile.lean b/lakefile.lean index 6fce699..4a55a20 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -135,6 +135,7 @@ lean_lib Examples where `«andChainStmt.types», `«andChainStmt.def», `«nameClash.types», `«nameClash.def», `«tuples.types», `«tuples.def», `«tuples.proof», - `«forContinue.types», `«forContinue.def», `«forContinue.proof» + `«forContinue.types», `«forContinue.def», `«forContinue.proof», + `«optChainDiscriminantTernary.types», `«optChainDiscriminantTernary.def», `«optChainDiscriminantTernary.proof» ] extraDepTargets := #[``downloadDependencies] diff --git a/tools/src/narrow.ts b/tools/src/narrow.ts index 364289b..eb3c3f1 100644 --- a/tools/src/narrow.ts +++ b/tools/src/narrow.ts @@ -101,9 +101,8 @@ const parseSimpleOptionalCheck = parseOptionalCheck; // ── Walkers ────────────────────────────────────────────────── function walkExpr(e: TExpr): TExpr { - // Fires on the raw conditional before `recurseExpr` rewrites the cond's - // optChain to a someMatch (which would leave `optChain === lit` unmatchable); - // it walks its own sub-branches, so recursion is preserved. + // Before recurseExpr rewrites the cond's optChain (which would leave + // `optChain === lit` unmatchable); the rule walks its own sub-branches. const preCond = ruleConditionalOptChainCompare(e); if (preCond) return preCond; const r = recurseExpr(e); @@ -346,26 +345,10 @@ function ruleEarlyReturnOrChain(s: TStmt, rest: TStmt[]): TStmt | null { return inner[0]; } -/** Rule: `if (opt?.chain !== lit) terminate; rest` where `opt` is optional. - * `opt?.chain` is `undefined` when `opt` is None, and `undefined !== lit` is - * true, so the None case takes the terminating branch — falling through to - * `rest` proves `opt` is Some. Rewrite to - * someMatch opt { Some(v) => [if (v.chain !== lit) terminate; rest]; None => terminate } - * narrowing `opt` to `v` across `rest` (transform substitutes the scrutinee) and - * handing the now-non-optional inner guard to the ordinary rules (e.g. - * discriminant narrowing). Bound-optional companion to ruleEarlyReturnConsume, - * which handles only a bare presence check (`opt !== undefined`). Restricted to - * `!==` so the None case is guaranteed to terminate. */ -/** Shared core of the two `x?.disc 'lit'` narrowings — the if-return - * statement form (`ruleEarlyReturnOptChainCompare`, op `!==`) and the ternary - * expression form (`ruleConditionalOptChainCompare`, op `===`). Matches an - * optional chain compared to a concrete (non-`undefined`) literal with the - * requested operator and returns the pieces both callers need: the scrutinee - * `x`, a fresh binder for its unwrapped value, and the chain re-applied to that - * binder (with the discriminant flag restored so the re-test lowers to a - * discriminant match). A `None` base makes `x?.disc` `undefined`, which never - * equals a real literal — so the presence of `x` is implied and each caller - * routes the branches accordingly. */ +/** Shared core of the two `x?.disc 'lit'` narrowings (statement `!==` and + * ternary `===`). Matches an optChain compared to a concrete (non-`undefined`) + * literal and returns the scrutinee `x`, a fresh binder, and the chain applied + * to the binder (discriminant flag restored so the re-test lowers to a match). */ function parseOptChainLitCompare(cond: TExpr, op: "===" | "!=="): { scrutinee: TExpr; binder: string; binderTy: Ty; unwrapped: TExpr; lit: TExpr; } | null { @@ -379,9 +362,8 @@ function parseOptChainLitCompare(cond: TExpr, op: "===" | "!=="): { if (hint === null) return null; const binder = freshName(hint); const unwrapped = applyChain({ kind: "var", name: binder, ty: binderTy }, oc.chain); - // applyChain rebuilds the field without the `isDiscriminant` flag resolve sets - // on a direct `x.disc`; restore it when the unwrapped access is the binder - // union's discriminant, so the inner guard feeds discriminant narrowing. + // applyChain drops the `isDiscriminant` flag resolve sets on a direct `x.disc`; + // restore it when the unwrapped field is the binder union's discriminant. if (unwrapped.kind === "field" && unwrapped.obj.ty.kind === "user") { const base = unwrapped.obj.ty.name.replace(/<.*/, ""); const decl = _typeDecls.find(d => d.name === base); @@ -392,6 +374,8 @@ function parseOptChainLitCompare(cond: TExpr, op: "===" | "!=="): { return { scrutinee: oc.obj, binder, binderTy, unwrapped, lit }; } +/** Rule: `if (x?.disc !== 'lit') terminate; rest` — the None case takes the + * terminating branch, so falling through to `rest` proves `x` is Some. */ function ruleEarlyReturnOptChainCompare(s: TStmt, rest: TStmt[]): TStmt | null { if (s.kind !== "if") return null; if (rest.length === 0) return null; @@ -407,15 +391,12 @@ function ruleEarlyReturnOptChainCompare(s: TStmt, rest: TStmt[]): TStmt | null { return { kind: "someMatch", scrutinee: m.scrutinee, binder: m.binder, binderTy: m.binderTy, someBody, noneBody: s.then }; } -/** Rule (expression): `x?.disc === 'lit' ? a : b` — the conditional-expression - * analogue of `ruleEarlyReturnOptChainCompare`. Lower to a `someMatch` on `x` - * whose Some-arm re-tests the unwrapped chain and whose None-arm takes the - * else branch (a None base can never equal the literal). - * → `someMatch x { Some(binder) => (binder.disc === 'lit' ? a : b), None => b }`. - * Runs *before* `recurseExpr` rewrites the cond's optChain to a someMatch, and - * walks its own sub-branches. The Some-arm keeps `a`/`b` referencing `x`; the - * expression-someMatch lowering (transform.ts) substitutes the `x` path with - * the binder inside them. */ +/** Rule (expression): `x?.disc === 'lit' ? a : b` — ternary analogue of + * `ruleEarlyReturnOptChainCompare`, lowering to + * `someMatch x { Some(binder) => (binder.disc === 'lit' ? a : b), None => b }`. + * Runs *before* `recurseExpr` rewrites the cond's optChain, and walks its own + * sub-branches; `a`/`b` keep referencing `x`, which the someMatch lowering + * (transform.ts) substitutes with the binder. */ function ruleConditionalOptChainCompare(e: TExpr): TExpr | null { if (e.kind !== "conditional") return null; const m = parseOptChainLitCompare(e.cond, "==="); diff --git a/tools/src/resolve.ts b/tools/src/resolve.ts index 4a2890f..0016e06 100644 --- a/tools/src/resolve.ts +++ b/tools/src/resolve.ts @@ -189,10 +189,9 @@ function detectOptionalCheck(cond: RawExpr, ctx: Ctx): { if (cond.right.kind === "var" && cond.right.name === "undefined") optExpr = cond.left; if (cond.left.kind === "var" && cond.left.name === "undefined") optExpr = cond.right; if (!optExpr) { - // `x?.disc === 'lit'` / `x?.disc !== 'lit'` (lit not undefined): an optional - // chain compared to a concrete literal implies its base `x` is present (a - // None base makes `x?.disc` undefined, which never equals a real literal). - // `===` narrows the then-branch; `!==` narrows the else-branch. + // `x?.disc === 'lit'` implies `x` is present (a None base makes `x?.disc` + // undefined, never equal to a real literal) — narrow the then-branch. + if (cond.op !== "===") return null; const oc = cond.left.kind === "optChain" ? cond.left : cond.right.kind === "optChain" ? cond.right : null; if (oc) { @@ -200,7 +199,7 @@ function detectOptionalCheck(cond: RawExpr, ctx: Ctx): { const litIsUndef = lit.kind === "var" && lit.name === "undefined"; if (!litIsUndef) { const inner = classifyOptExpr(oc.obj, ctx); - if (inner) return { ...inner, inThen: cond.op === "===" }; + if (inner) return { ...inner, inThen: true }; } } return null;