Function classifyEntry

scripts/fungrim/guard-census.ts:80–125

(
  ce: ReturnType<typeof createEngine>,
  e: Entry
)

}

function classifyEntry(
  ce: ReturnType<typeof createEngine>,
  e: Entry
): EntryOutcome {
  const conjuncts = conjunctsOf(e.assumptions);

  ce.pushScope();
  try {
    let assumable = true;
    let failure: EntryOutcome | undefined;

    for (const c of conjuncts) {
      let result: string;
      try {
        result = ce.assume(ce.expr(c as any, { canonical: !hasPartHead(c) }));
      } catch {
        assumable = false;
        failure ??= 'assume-threw';
        continue;
      }
      if (result !== 'ok' && result !== 'tautology') {
        assumable = false;
        if (result === 'contradiction') failure ??= 'contradiction';
        else if (result === 'internal-error') failure ??= 'internal-error';
        else failure ??= 'not-a-predicate';
      }
    }

    if (!assumable) return failure!;

    // Dischargeability: verify the full assumptions expression. Box
    // canonically — verify() itself boxes raw, which would leave plain
    // MathJSON unbound.
    let verified: boolean | undefined;
    try {
      verified = ce.verify(ce.expr(e.assumptions as any));
    } catch {
      return 'verify-threw';
    }
    if (verified === true) return 'dischargeable';
    if (verified === false) return 'verify-false';
    return 'verify-undefined';
  } finally {
    ce.popScope();
  }
}

function main(): void {
  const corpus = loadCorpus(DATA_DIR);