Function boxCheckEntry

scripts/fungrim/box-check.ts:66–95

(
  ce: ComputeEngine,
  e: Entry,
  knownHeads: Set<string>
)

}

export function boxCheckEntry(
  ce: ComputeEngine,
  e: Entry,
  knownHeads: Set<string>
): BoxResult {
  const familyHeads = new Set(e.indexedFamilies ?? []);
  const unknownHeads = e.heads.filter(
    (h) => !knownHeads.has(h) && !familyHeads.has(h)
  );
  return withEntryScope(ce, e, () => {
    const errors: string[] = [];
    try {
      collectErrors(ce.expr(e.formula as any).canonical, errors);
      if (e.assumptions != null)
        collectErrors(ce.expr(e.assumptions as any).canonical, errors);
    } catch (err: any) {
      errors.push(`THROW: ${String(err?.message ?? err).slice(0, 200)}`);
    }
    if (errors.length === 0) return { id: e.id, topic: e.topic, outcome: 'ok' };
    if (unknownHeads.length > 0)
      return {
        id: e.id,
        topic: e.topic,
        outcome: 'unknown-symbol',
        errors,
        unknownHeads,
      };
    return { id: e.id, topic: e.topic, outcome: 'box-error', errors };
  });
}

export type Stage1Report = {
  total: number;