Imhotep/packages/imhotep-solver/src/proofs.ts

/**
 * Proof object generation.
 *
 * Every evaluated clause produces a proof object carrying used facts,
 * derived facts, failed predicates, and witness data.
 *
 * Relation-aware synthesis: generateProof inspects the clause kind and
 * metrics to produce rich, relation-specific diagnostics instead of a
 * generic left/right comparison.
 */

import {
  type ClauseResult,
  type ClauseDescriptor,
  type Proof,
  type GeometryWorld,
} from './registry.js';

let proofCounter = 0;

function nextProofId(): string {
  return `proof_${++proofCounter}`;
}

/**
 * Reset the proof counter (mainly for tests).
 */
export function resetProofCounter(): void {
  proofCounter = 0;
}

// ---------------------------------------------------------------------------
// Relation-specific proof synthesis
// ---------------------------------------------------------------------------

function buildFailedPredicate(
  clauseKind: string,
  metrics: Record<string, number>,
): Proof['failedPredicate'] {
  // Normalize kind to handle prefix forms like "relation.leftOf".
  const kind = clauseKind.includes('.')
    ? clauseKind.slice(clauseKind.indexOf('.') + 1)
    : clauseKind;

  const base = {
    op: '<',
    left: 0,
    right: 0,
    relationKind: kind,
  };

  switch (kind) {
    case 'leftOf':
    case 'rightOf':
    case 'above':
    case 'below': {
      const gap = metrics.observedGap ?? metrics.gap ?? 0;
      const min = metrics.minGap ?? 0;
      const max = metrics.maxGap ?? Infinity;
      return {
        ...base,
        op: gap < min ? '<' : '>',
        left: gap,
        right: gap < min ? min : max,
        measuredGap: gap,
        expectedMinGap: Number.isFinite(min) ? min : undefined,
        expectedMaxGap: Number.isFinite(max) ? max : undefined,
        subjectRect:
          metrics.subjectLeft !== undefined
            ? {
                left: metrics.subjectLeft,
                top: metrics.subjectTop ?? 0,
                right: metrics.subjectRight ?? 0,
                bottom: metrics.subjectBottom ?? 0,
              }
            : undefined,
        referenceRect:
          metrics.refLeft !== undefined
            ? {
                left: metrics.refLeft,
                top: metrics.refTop ?? 0,
                right: metrics.refRight ?? 0,
                bottom: metrics.refBottom ?? 0,
              }
            : undefined,
      };
    }

    case 'inside': {
      const overflowLeft = metrics.overflowLeft ?? 0;
      const overflowTop = metrics.overflowTop ?? 0;
      const overflowRight = metrics.overflowRight ?? 0;
      const overflowBottom = metrics.overflowBottom ?? 0;
      return {
        ...base,
        op: 'not-contained',
        left: 0,
        right: 0,
        overflowEdges: {
          left: overflowLeft,
          top: overflowTop,
          right: overflowRight,
          bottom: overflowBottom,
        },
        subjectRect:
          metrics.subjectLeft !== undefined
            ? {
                left: metrics.subjectLeft,
                top: metrics.subjectTop ?? 0,
                right: metrics.subjectRight ?? 0,
                bottom: metrics.subjectBottom ?? 0,
              }
            : undefined,
        referenceRect:
          metrics.refLeft !== undefined
            ? {
                left: metrics.refLeft,
                top: metrics.refTop ?? 0,
                right: metrics.refRight ?? 0,
                bottom: metrics.refBottom ?? 0,
              }
            : undefined,
      };
    }

    case 'atLeast':
    case 'atMost':
    case 'between': {
      const observed = metrics.observed ?? metrics.value ?? 0;
      const min = metrics.min ?? -Infinity;
      const max = metrics.max ?? Infinity;
      return {
        ...base,
        op: kind === 'atMost' ? '>' : '<',
        left: observed,
        right: kind === 'atMost' ? max : min,
        measuredValue: observed,
        expectedMin: Number.isFinite(min) ? min : undefined,
        expectedMax: Number.isFinite(max) ? max : undefined,
      };
    }

    case 'aspectRatio': {
      const observed = metrics.observed ?? 0;
      const minRatio = metrics.minRatio ?? -Infinity;
      const maxRatio = metrics.maxRatio ?? Infinity;
      return {
        ...base,
        op: observed < minRatio ? '<' : '>',
        left: observed,
        right: observed < minRatio ? minRatio : maxRatio,
        measuredValue: observed,
        expectedMin: Number.isFinite(minRatio) ? minRatio : undefined,
        expectedMax: Number.isFinite(maxRatio) ? maxRatio : undefined,
      };
    }

    case 'alignedWith':
    case 'centeredWithin': {
      const delta = metrics.delta ?? metrics.deltaX ?? metrics.deltaY ?? 0;
      const tolerance = metrics.tolerance ?? 0;
      return {
        ...base,
        op: '>',
        left: delta,
        right: tolerance,
        measuredValue: delta,
        expectedMax: tolerance,
      };
    }

    default:
      // Fallback to generic synthesis from the first two numeric metrics.
      const fallback = synthesizeGenericFailedPredicate(metrics);
      if (fallback) {
        return { ...fallback, relationKind: kind };
      }
      return fallback;
  }
}

function synthesizeGenericFailedPredicate(
  metrics: Record<string, number>,
): Proof['failedPredicate'] {
  const keys = Object.keys(metrics);
  if (keys.length >= 2) {
    return {
      op: '<',
      left: metrics[keys[0]] ?? 0,
      right: metrics[keys[1]] ?? 0,
    };
  }
  if (keys.length === 1) {
    return {
      op: '<',
      left: metrics[keys[0]] ?? 0,
      right: 0,
    };
  }
  return undefined;
}

// ---------------------------------------------------------------------------
// Public API
// ---------------------------------------------------------------------------

/**
 * Generate a single proof object from a clause result.
 *
 * @param result       - The evaluation result for the clause.
 * @param clause       - The clause descriptor that was evaluated.
 * @param world        - The geometry world the clause was evaluated against.
 * @param usedFacts    - Array of fact ids that were read during evaluation.
 * @param derivedFacts - Array of fact ids that were derived during evaluation.
 */
export function generateProof(
  result: ClauseResult,
  clause: ClauseDescriptor,
  world: GeometryWorld,
  usedFacts: number[] = [],
  derivedFacts: number[] = [],
): Proof {
  const proof: Proof = {
    proofId: nextProofId(),
    clauseId: result.clauseId,
    outcome: result.status,
    truth: result.truth,
    usedFacts: [...usedFacts],
    derivedFacts: [...derivedFacts],
    witness: {
      subjectId: result.witness?.subjectId ?? clause.subjectRef,
      referenceId: result.witness?.referenceId ?? clause.referenceRef,
      frameId: result.witness?.frameId ?? clause.frameRef,
      snapshotId: world.snapshotId,
    },
  };

  if (result.status === 'fail' && result.metrics) {
    proof.failedPredicate = buildFailedPredicate(
      clause.clauseKind,
      result.metrics,
    );
  }

  return proof;
}

/**
 * Batch-generate proofs for a set of clause results.
 *
 * @param results          - Array of clause results.
 * @param clauses          - Array of clause descriptors (must cover all result clauseIds).
 * @param world            - The geometry world used during evaluation.
 * @param usedFactsMap     - Optional map from clauseId to fact ids.
 * @param derivedFactsMap  - Optional map from clauseId to derived fact ids.
 */
export function generateProofs(
  results: ClauseResult[],
  clauses: ClauseDescriptor[],
  world: GeometryWorld,
  usedFactsMap: Map<string, number[]> = new Map(),
  derivedFactsMap: Map<string, number[]> = new Map(),
): Proof[] {
  const clauseMap = new Map(clauses.map((c) => [c.clauseId, c]));
  return results.map((r) => {
    const clause = clauseMap.get(r.clauseId);
    if (!clause) {
      throw new Error(`Clause descriptor not found for ${r.clauseId}`);
    }
    return generateProof(
      r,
      clause,
      world,
      usedFactsMap.get(r.clauseId),
      derivedFactsMap.get(r.clauseId),
    );
  });
}