(v: string, dom: MathJSON)
| 326 | if (typeof dom === 'string') { |
| 327 | switch (dom) { |
| 328 | case 'Integers': |
| 329 | guards.push({ k: 'type', wc: wc(v), t: 'integer' }); |
| 330 | return null; |
| 331 | case 'NonNegativeIntegers': |
| 332 | guards.push({ k: 'type', wc: wc(v), t: 'integer' }); |
| 333 | guards.push({ k: 'cmp', wc: wc(v), op: 'ge', bound: 0 }); |
| 334 | return null; |
| 335 | case 'PositiveIntegers': |
| 336 | guards.push({ k: 'type', wc: wc(v), t: 'integer' }); |
| 337 | guards.push({ k: 'cmp', wc: wc(v), op: 'gt', bound: 0 }); |
| 338 | return null; |
| 339 | case 'NegativeIntegers': |
| 340 | guards.push({ k: 'type', wc: wc(v), t: 'integer' }); |
| 341 | guards.push({ k: 'cmp', wc: wc(v), op: 'lt', bound: 0 }); |
| 342 | return null; |
| 343 | case 'NonPositiveIntegers': |
| 344 | guards.push({ k: 'type', wc: wc(v), t: 'integer' }); |
| 345 | guards.push({ k: 'cmp', wc: wc(v), op: 'le', bound: 0 }); |
| 346 | return null; |
| 347 | case 'RealNumbers': |
| 348 | guards.push({ k: 'type', wc: wc(v), t: 'real' }); |
| 349 | return null; |
| 350 | case 'RationalNumbers': |
| 351 | guards.push({ k: 'type', wc: wc(v), t: 'rational' }); |
| 352 | return null; |
| 353 | case 'ComplexNumbers': |
| 354 | // Fungrim's CC is the FINITE complex numbers; the runtime closure |
| 355 | // mirrors `ComplexNumbers.contains` (typeMembership finite_complex) |
| 356 | // via the boxed Element evaluation. |
| 357 | guards.push({ k: 'type', wc: wc(v), t: 'complex' }); |
| 358 | return null; |
| 359 | case 'Primes': |
| 360 | // CE's `Primes` is a shell with no membership evaluator; compile to |
| 361 | // the built-in IsPrime predicate (still fail-closed: fires only on |
| 362 | // a literal True). |
| 363 | guards.push({ k: 'type', wc: wc(v), t: 'integer' }); |
| 364 | guards.push({ k: 'eval', pred: ['IsPrime', wc(v)] }); |
| 365 | return null; |
| 366 | case 'HH': |
| 367 | // Fungrim's HH is the open upper half-plane {z : Im z > 0}. Compile |
| 368 | // membership directly to the part-predicate Im(v) > 0 so it |
| 369 | // discharges through the part-cmp machinery (e.g. assume Im(v) > 0), |
| 370 | // rather than an opaque stored-membership exact match. This keeps HH |
| 371 | // off the guard/discharge surface entirely: the 249 modular/theta |
| 372 | // guards now fire under a plain `assume(Im(tau) > 0)`. (HH survives |
| 373 | // only as a set literal in the ModularLambdaFundamentalDomain |
| 374 | // definition, where it is structural, not a guard.) |
| 375 | guards.push({ k: 'part-cmp', wc: wc(v), part: 'im', op: 'gt', bound: 0 }); |
| 376 | return null; |
| 377 | default: |
| 378 | return `unsupported domain "${dom}"`; |
| 379 | } |
| 380 | } |
| 381 | if (Array.isArray(dom)) { |
| 382 | const op = dom[0]; |
| 383 | if (op === 'Interval' && dom.length === 3) { |
| 384 | guards.push({ k: 'type', wc: wc(v), t: 'real' }); |
| 385 | pushBound(v, dom[1], 'gt', 'ge'); |
no test coverage detected