/**
 * Canonical formula adapter for the Imhotep solver.
 *
 * Bridges canonical formula nodes (from Stream 0 contracts) to the solver's
 * internal logic-ast shape, and adapts solver evaluation results back to
 * canonical result shapes.
 *
 * All cross-package handoffs go through this file — no implicit casts.
 */

import type {
  // Canonical contracts
  CanonicalFormulaNode,
  CanonicalTupleBinding,
  CanonicalDomainRef,
  CanonicalVariableRef,
  CanonicalAccessorTerm,
  CanonicalTermNode,
  CanonicalDeterministicSceneResult,
  CanonicalDiagnostic,
  // Solver-facing contracts from logic-ast
  FormulaNode,
  ForAllFormula,
  ExistsFormula,
  AndFormula,
  OrFormula,
  NotFormula,
  ImpliesFormula,
  PredicateCall,
  VariableRef,
  DomainRef,
  AccessorTerm,
  TupleBinding,
} from 'imhotep-core'

import type {
  DeterministicSceneEvaluation,
  FormulaResult,
} from './logic-engine.js'

// ---------------------------------------------------------------------------
// Solver Formula Node (explicit alias for the shape the engine consumes)
// ---------------------------------------------------------------------------

/** The solver engine accepts FormulaNode from imhotep-core logic-ast. */
export type SolverFormulaNode = FormulaNode

/** The solver engine accepts DomainValue from imhotep-core domains. */
export interface SolverResult extends DeterministicSceneEvaluation {}

/** Canonical clause result produced by adapting a solver evaluation. */
export interface CanonicalClauseResult extends CanonicalDeterministicSceneResult {}

// ---------------------------------------------------------------------------
// Canonical → Solver
// ---------------------------------------------------------------------------

/**
 * Adapt a canonical formula node to the solver's FormulaNode shape.
 *
 * The canonical shape lacks the `type` discriminator on formula nodes and
 * term nodes; this adapter adds the required discriminators so the solver
 * engine can consume the formula without modification.
 */
export function adaptCanonicalFormulaToSolver(
  formula: CanonicalFormulaNode,
): SolverFormulaNode {
  switch (formula.kind) {
    case 'forall':
      return adaptForAll(formula)
    case 'exists':
      return adaptExists(formula)
    case 'and':
      return adaptAnd(formula)
    case 'or':
      return adaptOr(formula)
    case 'not':
      return adaptNot(formula)
    case 'implies':
      return adaptImplies(formula)
    case 'predicate':
      return adaptPredicate(formula)
    default:
      // Exhaustiveness check — if we hit this, canonical added a new kind.
      throw new Error(
        `Cannot adapt unknown canonical formula kind: ${(formula as CanonicalFormulaNode).kind}`,
      )
  }
}

function adaptForAll(formula: Extract<CanonicalFormulaNode, { kind: 'forall' }>): ForAllFormula {
  return {
    type: 'FormulaNode',
    kind: 'forall',
    bindings: formula.bindings.map(adaptTupleBinding),
    body: adaptCanonicalFormulaToSolver(formula.body),
  }
}

function adaptExists(formula: Extract<CanonicalFormulaNode, { kind: 'exists' }>): ExistsFormula {
  return {
    type: 'FormulaNode',
    kind: 'exists',
    bindings: formula.bindings.map(adaptTupleBinding),
    body: adaptCanonicalFormulaToSolver(formula.body),
  }
}

function adaptAnd(formula: Extract<CanonicalFormulaNode, { kind: 'and' }>): AndFormula {
  return {
    type: 'FormulaNode',
    kind: 'and',
    left: adaptCanonicalFormulaToSolver(formula.left),
    right: adaptCanonicalFormulaToSolver(formula.right),
  }
}

function adaptOr(formula: Extract<CanonicalFormulaNode, { kind: 'or' }>): OrFormula {
  return {
    type: 'FormulaNode',
    kind: 'or',
    left: adaptCanonicalFormulaToSolver(formula.left),
    right: adaptCanonicalFormulaToSolver(formula.right),
  }
}

function adaptNot(formula: Extract<CanonicalFormulaNode, { kind: 'not' }>): NotFormula {
  return {
    type: 'FormulaNode',
    kind: 'not',
    operand: adaptCanonicalFormulaToSolver(formula.operand),
  }
}

function adaptImplies(
  formula: Extract<CanonicalFormulaNode, { kind: 'implies' }>,
): ImpliesFormula {
  return {
    type: 'FormulaNode',
    kind: 'implies',
    antecedent: adaptCanonicalFormulaToSolver(formula.antecedent),
    consequent: adaptCanonicalFormulaToSolver(formula.consequent),
  }
}

function adaptPredicate(
  formula: Extract<CanonicalFormulaNode, { kind: 'predicate' }>,
): PredicateCall {
  return {
    type: 'FormulaNode',
    kind: 'predicate',
    predicate: formula.predicate,
    args: formula.args.map(adaptTerm),
  }
}

function adaptTupleBinding(binding: CanonicalTupleBinding): TupleBinding {
  return {
    type: 'TupleBinding',
    variables: binding.variables,
    domain: adaptDomainRef(binding.domain),
  }
}

function adaptDomainRef(ref: CanonicalDomainRef): DomainRef {
  return {
    type: 'DomainRef',
    domain: ref.domain,
    selector: ref.selector,
    parentVar: ref.parentVar,
  }
}

function adaptTerm(term: CanonicalTermNode): VariableRef | DomainRef | AccessorTerm {
  if ('name' in term && !('variable' in term) && !('domain' in term)) {
    return adaptVariableRef(term as CanonicalVariableRef)
  }
  if ('domain' in term) {
    return adaptDomainRef(term as CanonicalDomainRef)
  }
  if ('variable' in term && 'property' in term) {
    return adaptAccessorTerm(term as CanonicalAccessorTerm)
  }
  // Fallback for malformed term — treat as empty variable ref.
  return { type: 'VariableRef', name: '' }
}

function adaptVariableRef(ref: CanonicalVariableRef): VariableRef {
  return {
    type: 'VariableRef',
    name: ref.name,
  }
}

function adaptAccessorTerm(term: CanonicalAccessorTerm): AccessorTerm {
  return {
    type: 'AccessorTerm',
    variable: term.variable,
    property: term.property,
  }
}

// ---------------------------------------------------------------------------
// Solver → Canonical
// ---------------------------------------------------------------------------

/**
 * Adapt a solver deterministic scene evaluation to the canonical result shape.
 *
 * Maps solver-specific diagnostics to canonical diagnostics, preserves all
 * formula results, proofs, and trace events.
 */
export function adaptSolverResultToCanonical(
  result: SolverResult,
): CanonicalClauseResult {
  return {
    mode: result.mode,
    sceneId: result.sceneId,
    results: result.formulaResults.map(adaptFormulaResult),
    proofs: result.proofs,
    diagnostics: result.diagnostics.map(adaptSolverDiagnosticToCanonical),
  }
}

function adaptFormulaResult(result: FormulaResult): Record<string, unknown> {
  return {
    formulaId: result.formulaId,
    outcome: result.outcome,
    truth: result.truth,
    witness: result.witness,
    metrics: result.metrics,
  }
}

function adaptSolverDiagnosticToCanonical(
  d: {
    code: string
    severity: 'error' | 'warning' | 'info'
    category?: string
    message: string
    position?: {
      start: { line: number; column: number; offset: number }
      end: { line: number; column: number; offset: number }
    }
    clauseId?: string
  },
): CanonicalDiagnostic {
  return {
    code: d.code,
    severity: d.severity,
    category: (d.category ?? 'internal-error') as CanonicalDiagnostic['category'],
    message: d.message,
    source: 'imhotep-solver',
    clauseId: d.clauseId,
    position: d.position,
  }
}