( ce: ComputeEngine, guards: ReadonlyArray<GuardSpec> )
| 548 | ce: ComputeEngine, |
| 549 | guards: ReadonlyArray<GuardSpec> |
| 550 | ): ((sub: Sub) => boolean)[] { |
| 551 | const boxGuardExpr = (x: MathJSON): Expression => { |
| 552 | try { |
| 553 | const b = ce.expr(x as never); |
| 554 | if (b.isValid) return b; |
| 555 | } catch { |
| 556 | /* fall through to raw boxing */ |
| 557 | } |
| 558 | return ce.expr(x as never, { form: 'raw' }); |
| 559 | }; |
| 560 | |
| 561 | return guards.map((g) => { |
| 562 | switch (g.k) { |
| 563 | case 'type': { |
| 564 | if (g.t === 'complex') { |
| 565 | // Fungrim CC = FINITE complex numbers. Literal fast path via the |
| 566 | // type lattice; symbols go through the boxed Element evaluation |
| 567 | // (mirrors `ComplexNumbers.contains`, and consults the Track-3 |
| 568 | // type refinements made by `assume(Element(z, ComplexNumbers))`). |
| 569 | const pred = boxGuardExpr(['Element', g.wc, 'ComplexNumbers']); |
| 570 | return (sub: Sub) => { |
| 571 | const v = sub[g.wc]; |
| 572 | if (v === undefined) return false; |
| 573 | if (v.type.matches('finite_complex')) return true; |
| 574 | try { |
| 575 | return pred.subs(sub).evaluate().json === 'True'; |
| 576 | } catch { |
| 577 | return false; |
| 578 | } |
| 579 | }; |
| 580 | } |
| 581 | return (sub: Sub) => { |
| 582 | const v = sub[g.wc]; |
| 583 | if (v === undefined) return false; |
| 584 | // Fungrim's declared domains (ZZ/QQ/RR) are FINITE, matching the |
| 585 | // 'complex' guard above. A value PROVABLY non-finite (a ±∞ or ~∞ |
| 586 | // literal has `isFinite === false`) is blocked; note that |
| 587 | // `(+∞).isExtendedReal === true`, so without this gate a real guard |
| 588 | // would fail open at infinity. Unknown finiteness |
| 589 | // (`isFinite === undefined`, e.g. a plain declared-real symbol) |
| 590 | // still passes, so ordinary symbols discharge as before. This |
| 591 | // mirrors the runtime twin in |
| 592 | // `src/compute-engine/fungrim/loader.ts`; the two must stay in step |
| 593 | // or a rule admitted at build time is refused at run time. |
| 594 | if (v.isFinite === false) return false; |
| 595 | if (g.t === 'integer') return v.isInteger === true; |
| 596 | if (g.t === 'real') return v.isExtendedReal === true; |
| 597 | return v.isRational === true; |
| 598 | }; |
| 599 | } |
| 600 | case 'part-cmp': { |
| 601 | // Compare a part extractor of the substituted value: literal |
| 602 | // substitutions fold numerically (Re(1+2i) → 1); symbol |
| 603 | // substitutions consult the Track-3 part-bound facts |
| 604 | // (assume(Re(s) > 1) ⇒ Greater(Re(s), 0) evaluates to True). |
| 605 | // Fail-closed: anything but a literal True/False stays blocking. |
| 606 | const pred = boxGuardExpr([ |
| 607 | CMP_TO_OPERATOR[g.op], |
no test coverage detected