// Compiler: lowers AST -> Semantic IR -> Execution IR
// Pure function, no browser dependencies

import type {
  RelationAssertion,
  SemanticIr,
  ExecutionIr,
  SemanticClause,
  SemanticSubject,
  SemanticFrame,
  SemanticState,
  SemanticTimeline,
  SemanticTolerance,
  SemanticEnvGuard,
  Diagnostic,
  Position,
  ImhotepId,
  FormulaNode,
  VariableRef,
  DomainRef,
  TupleBinding,
  PredicateCall,
  AssertionNode,
  SizeAssertion,
  TopologyAssertion,
  CompoundAssertion,
  SelectorRef,
} from 'imhotep-core'

import { createEmptySemanticIr, getDefaultContext } from 'imhotep-core'
import { parseTolerance, parseGap } from './validator.js'

// DSL grammar FOL types (distinct from solver FormulaNode imported above)
import type {
  FormulaNode as DslFormulaNode,
  ForAllFormula as DslForAll,
  ExistsFormula as DslExists,
  AndFormula as DslAnd,
  OrFormula as DslOr,
  NotFormula as DslNot,
  ImpliesFormula as DslImplies,
  PredicateCall as DslPredicateCall,
  VariableRef as DslVariableRef,
  DomainRef as DslDomainRef,
} from './logic-fluent.js'

// ---- Compiler Options (dependency injection) ----

export interface CompilerOptions {
  // Injected id generator for determinism in tests
  generateId?: (prefix: string) => string
  // Default frame when none specified
  defaultFrameKind?: string
  // Default tolerance when none specified
  defaultTolerance?: { value: number; unit: 'px' | 'jnd' }
}

// ---- Id Generator ----

function defaultNextId(prefix: string): string {
  return `${prefix}_${getDefaultContext().idGenerator()}`
}

// ---- Option Value Normalization ----
// INVARIANT: Both fluent API and string DSL must lower to equivalent Execution IR.
// The string parser produces LiteralNode / ToleranceLiteralNode AST wrappers,
// while the fluent API stores raw numbers. These normalizers extract the scalar
// value from both formats so parseGap / parseTolerance receive consistent input.
//
// Bug fixed: Previously parseGap(LiteralNode) silently returned null because
// String(object) === "[object Object]", causing string DSL gap options to be
// lost in compilation. The extractGapValue helper now handles range literals.

function normalizeOptionValue(raw: unknown): number | string | undefined {
  if (raw === undefined || raw === null) return undefined
  if (typeof raw === 'number' || typeof raw === 'string') return raw

  // String-parser/fluent path: LiteralNode or ToleranceLiteralNode
  if (typeof raw === 'object') {
    const obj = raw as Record<string, unknown>
    if ('value' in obj && typeof obj.value === 'number') {
      if ('unit' in obj && typeof obj.unit === 'string') {
        return `${obj.value}${obj.unit}`
      }
      return obj.value
    }
  }

  return undefined
}

// Extract a numeric gap value from fluent raw numbers, string-parser LiteralNodes,
// or string-parser range LiteralNodes ( picking min or max edge ).
function extractGapValue(raw: unknown, edge: 'min' | 'max'): number | undefined {
  if (raw === undefined || raw === null) return undefined
  if (typeof raw === 'number') return raw
  if (typeof raw === 'string') {
    const num = parseFloat(raw.trim())
    if (!Number.isNaN(num)) return num
    return undefined
  }

  if (typeof raw === 'object') {
    const obj = raw as Record<string, unknown>

    // Simple length literal: { type: 'Literal', kind: 'length', value: number }
    if ('value' in obj && typeof obj.value === 'number') {
      return obj.value
    }

    // Range literal: { type: 'Literal', kind: 'range', value: { min: { value }, max: { value } } }
    if (obj.kind === 'range' && obj.value && typeof obj.value === 'object') {
      const range = obj.value as Record<string, unknown>
      const target = edge === 'min' ? range.min : range.max
      if (target && typeof target === 'object') {
        const targetObj = target as Record<string, unknown>
        if (typeof targetObj.value === 'number') {
          return targetObj.value
        }
      }
    }
  }

  return undefined
}

// ---- Semantic Lowering ----

function toSemanticIr(
  ast: RelationAssertion[],
  opts: CompilerOptions,
): { semanticIr: SemanticIr; diagnostics: Diagnostic[] } {
  const generateId = opts.generateId || defaultNextId
  const ir = createEmptySemanticIr()
  const diagnostics: Diagnostic[] = []

  // Default frame
  const defaultFrameId = generateId('frame')
  ir.frames.set(defaultFrameId, {
    id: defaultFrameId,
    kind: (opts.defaultFrameKind || 'viewport') as SemanticFrame['kind'],
    originX: 0,
    originY: 0,
    writingMode: 'horizontal-tb',
    origin: { astNodeIds: [], positions: [] },
  })

  // Default state
  const defaultStateId = generateId('state')
  ir.states.set(defaultStateId, {
    id: defaultStateId,
    kind: 'default',
    origin: { astNodeIds: [], positions: [] },
  })

  // Default timeline
  const defaultTimelineId = generateId('timeline')
  ir.timelines.set(defaultTimelineId, {
    id: defaultTimelineId,
    mode: 'static',
    origin: { astNodeIds: [], positions: [] },
  })

  // Default tolerance
  const defaultToleranceId = generateId('tolerance')
  ir.tolerances.set(defaultToleranceId, {
    id: defaultToleranceId,
    value: opts.defaultTolerance?.value ?? 0,
    unit: opts.defaultTolerance?.unit ?? 'px',
    origin: { astNodeIds: [], positions: [] },
  })

  for (const assertion of ast) {
    // Build origin from source span
    const origin = buildOrigin(assertion.position)

    // Access extended DSL properties via cast
    const extended = assertion as unknown as Record<string, unknown>

    // Subject
    const subjectId = generateId('subject')
    const subjectDef: SemanticSubject = {
      id: subjectId,
      selector: assertion.subject.value,
      kind: 'element',
      origin,
    }
    ir.subjects.set(subjectId, subjectDef)

    // Reference
    const referenceId = generateId('subject')
    const referenceDef: SemanticSubject = {
      id: referenceId,
      selector: assertion.reference.value,
      kind: 'element',
      origin,
    }
    ir.subjects.set(referenceId, referenceDef)

    // Frame
    let frameId = defaultFrameId
    const frameNode = extended.frame as { kind: string; selector?: string; name?: string } | undefined
    if (frameNode) {
      frameId = generateId('frame')
      const frameDef: SemanticFrame = {
        id: frameId,
        kind: frameNode.kind as SemanticFrame['kind'],
        selector: frameNode.selector,
        name: frameNode.name,
        originX: 0,
        originY: 0,
        writingMode: 'horizontal-tb',
        origin,
      }
      ir.frames.set(frameId, frameDef)
    }

    // State
    let stateId = defaultStateId
    const stateNode = extended.state as { kind: string; name?: string } | undefined
    if (stateNode) {
      stateId = generateId('state')
      const stateDef: SemanticState = {
        id: stateId,
        kind: stateNode.kind as SemanticState['kind'],
        name: stateNode.name,
        origin,
      }
      ir.states.set(stateId, stateDef)
    }

    // Tolerance
    let toleranceId = defaultToleranceId
    const rawOpts = assertion.options as unknown as Record<string, unknown> | undefined
    const tol = parseTolerance(normalizeOptionValue(rawOpts?.tolerance))
    if (tol) {
      toleranceId = generateId('tolerance')
      ir.tolerances.set(toleranceId, {
        id: toleranceId,
        value: tol.value,
        unit: tol.unit,
        origin,
      })
    }

    // Environment guard
    const envGuardId = generateId('guard')
    const envGuard = extended.envGuard as { condition: string } | undefined
    const guardDef: SemanticEnvGuard = {
      id: envGuardId,
      expression: envGuard?.condition || 'true',
      normalizedCases: [],
      origin,
    }
    ir.envGuards.set(envGuardId, guardDef)

    // Bounds
    const bounds: SemanticClause['bounds'] = {}
    if (rawOpts) {
      if ('minGap' in rawOpts) {
        const minVal = extractGapValue(rawOpts.minGap, 'min')
        if (minVal !== undefined) {
          bounds.minGap = { value: minVal, unit: 'px' }
        }
      }
      if ('maxGap' in rawOpts) {
        const maxVal = extractGapValue(rawOpts.maxGap, 'max')
        if (maxVal !== undefined) {
          bounds.maxGap = { value: maxVal, unit: 'px' }
        }
      }
    }

    // Flags
    let flags = 0
    const quantifier = extended.quantifier as string | undefined
    if (quantifier === 'all') flags |= 1
    if (quantifier === 'any') flags |= 2
    if (quantifier === 'none') flags |= 4
    if (rawOpts?.inStackingContext) flags |= 8
    if ((assertion as any).negated) flags |= 16

    // Clause
    const clauseId = generateId('clause')
    const clause: SemanticClause = {
      id: clauseId,
      origin,
      subjectRef: subjectId,
      referenceRef: referenceId,
      relation: assertion.relation,
      frameRef: frameId,
      stateRef: stateId,
      timelineRef: defaultTimelineId,
      envGuardRef: envGuardId,
      toleranceRef: toleranceId,
      bounds,
    }

    // Attach flags via cast since core SemanticClause doesn't have flags field yet
    ;(clause as unknown as Record<string, unknown>).flags = flags

    ir.clauses.set(clauseId, clause)
  }

  return { semanticIr: ir, diagnostics }
}

function buildOrigin(position?: Position): { astNodeIds: string[]; positions: Position[] } {
  if (position) {
    return { astNodeIds: [], positions: [position] }
  }
  return { astNodeIds: [], positions: [] }
}

// ---- Execution IR Compilation ----

function toExecutionIr(semanticIr: SemanticIr): ExecutionIr {
  const clauses = Array.from(semanticIr.clauses.values())
  const count = clauses.length

  if (count === 0) {
    return {
      clauseCount: 0,
      clauseType: new Uint16Array(0),
      clauseSubject: new Uint32Array(0),
      clauseReference: new Uint32Array(0),
      clauseFrame: new Uint32Array(0),
      clauseState: new Uint32Array(0),
      clauseTimeline: new Uint32Array(0),
      clauseTolerance: new Uint32Array(0),
      clauseEnvGuard: new Uint32Array(0),
      clauseArg0: new Float64Array(0),
      clauseArg1: new Float64Array(0),
      clauseFlags: new Uint32Array(0),
      clauseOrigin: new Uint32Array(0),
    }
  }

  // Build lookup maps for numeric indices — iterate Maps directly to avoid Array.from().
  const subjectIndex = new Map<ImhotepId, number>()
  let idx = 0
  for (const k of semanticIr.subjects.keys()) subjectIndex.set(k, idx++)

  const frameIndex = new Map<ImhotepId, number>()
  idx = 0
  for (const k of semanticIr.frames.keys()) frameIndex.set(k, idx++)

  const stateIndex = new Map<ImhotepId, number>()
  idx = 0
  for (const k of semanticIr.states.keys()) stateIndex.set(k, idx++)

  const timelineIndex = new Map<ImhotepId, number>()
  idx = 0
  for (const k of semanticIr.timelines.keys()) timelineIndex.set(k, idx++)

  const toleranceIndex = new Map<ImhotepId, number>()
  idx = 0
  for (const k of semanticIr.tolerances.keys()) toleranceIndex.set(k, idx++)

  const guardIndex = new Map<ImhotepId, number>()
  idx = 0
  for (const k of semanticIr.envGuards.keys()) guardIndex.set(k, idx++)

  // Encode relation as small integer
  const relationCodes: Record<string, number> = {
    leftOf: 1,
    rightOf: 2,
    above: 3,
    below: 4,
    alignedWith: 5,
    leftAlignedWith: 6,
    rightAlignedWith: 7,
    topAlignedWith: 8,
    bottomAlignedWith: 9,
    centeredWithin: 10,
    inside: 11,
    contains: 12,
    overlaps: 13,
    separatedFrom: 14,
    aspectRatioBetween: 15,
    between: 16,
  }

  const clauseType = new Uint16Array(count)
  const clauseSubject = new Uint32Array(count)
  const clauseReference = new Uint32Array(count)
  const clauseFrame = new Uint32Array(count)
  const clauseState = new Uint32Array(count)
  const clauseTimeline = new Uint32Array(count)
  const clauseTolerance = new Uint32Array(count)
  const clauseEnvGuard = new Uint32Array(count)
  const clauseArg0 = new Float64Array(count)
  const clauseArg1 = new Float64Array(count)
  const clauseFlags = new Uint32Array(count)
  const clauseOrigin = new Uint32Array(count)

  for (let i = 0; i < count; i++) {
    const c = clauses[i]
    clauseType[i] = relationCodes[c.relation] || 0
    clauseSubject[i] = subjectIndex.get(c.subjectRef) ?? 0
    clauseReference[i] = c.referenceRef ? (subjectIndex.get(c.referenceRef) ?? 0) : 0
    clauseFrame[i] = frameIndex.get(c.frameRef) ?? 0
    clauseState[i] = stateIndex.get(c.stateRef) ?? 0
    clauseTimeline[i] = timelineIndex.get(c.timelineRef) ?? 0
    clauseTolerance[i] = toleranceIndex.get(c.toleranceRef) ?? 0
    clauseEnvGuard[i] = guardIndex.get(c.envGuardRef) ?? 0
    clauseOrigin[i] = i // origin index same as clause index for now

    // Retrieve flags via cast
    const flags = (c as unknown as Record<string, unknown>).flags as number | undefined
    clauseFlags[i] = flags || 0

    // Pack bounds into arg0/arg1 where applicable
    if (c.bounds.minGap && c.bounds.maxGap) {
      clauseArg0[i] = c.bounds.minGap.value
      clauseArg1[i] = c.bounds.maxGap.value
    } else if (c.bounds.minGap) {
      clauseArg0[i] = c.bounds.minGap.value
      clauseArg1[i] = Number.POSITIVE_INFINITY
    } else if (c.bounds.maxGap) {
      clauseArg0[i] = Number.NEGATIVE_INFINITY
      clauseArg1[i] = c.bounds.maxGap.value
    } else {
      clauseArg0[i] = Number.NEGATIVE_INFINITY
      clauseArg1[i] = Number.POSITIVE_INFINITY
    }
  }

  return {
    clauseCount: count,
    clauseType,
    clauseSubject,
    clauseReference,
    clauseFrame,
    clauseState,
    clauseTimeline,
    clauseTolerance,
    clauseEnvGuard,
    clauseArg0,
    clauseArg1,
    clauseFlags,
    clauseOrigin,
  }
}

// ---- FOL Formula Compilation ----

const subjectVar: VariableRef = { type: 'VariableRef', name: '$subject' }
const referenceVar: VariableRef = { type: 'VariableRef', name: '$reference' }

function makeDomain(selector: string): DomainRef {
  return { type: 'DomainRef', domain: 'elements', selector }
}

function makeBinding(varName: string, selector: string): TupleBinding {
  return {
    type: 'TupleBinding',
    variables: [varName],
    domain: makeDomain(selector),
  }
}

function buildOptionsFromAssertion(assertion: RelationAssertion | SizeAssertion | TopologyAssertion): Record<string, unknown> {
  const options: Record<string, unknown> = {}

  if (assertion.type === 'RelationAssertion') {
    const opts = assertion.options as unknown as Record<string, unknown>
    if (opts?.minGap !== undefined) {
      const v = normalizeOptionValue(opts.minGap)
      if (v !== undefined) options.minGap = v
    }
    if (opts?.maxGap !== undefined) {
      const v = normalizeOptionValue(opts.maxGap)
      if (v !== undefined) options.maxGap = v
    }
    if (opts?.tolerance !== undefined) {
      const tol = parseTolerance(normalizeOptionValue(opts.tolerance))
      if (tol) {
        options.tolerance = tol.value
        options.toleranceUnit = tol.unit
      }
    }
    if (opts?.axis !== undefined) options.axis = opts.axis
    if (opts?.inStackingContext === true) options.inStackingContext = true
  }

  if (assertion.type === 'SizeAssertion') {
    const bounds = assertion.bounds as unknown as Record<string, unknown>
    if (bounds?.min && typeof (bounds.min as any).value === 'number') {
      options.min = (bounds.min as any).value
      options.value = (bounds.min as any).value
    }
    if (bounds?.max && typeof (bounds.max as any).value === 'number') {
      options.max = (bounds.max as any).value
    }
    if (bounds?.exact && typeof (bounds.exact as any).value === 'number') {
      options.value = (bounds.exact as any).value
    }
    if (assertion.property) {
      options.dimension = assertion.property
    }
  }

  if (assertion.type === 'TopologyAssertion') {
    const opts = assertion.options as unknown as Record<string, unknown>
    if (opts?.tolerance !== undefined) {
      const tol = parseTolerance(normalizeOptionValue(opts.tolerance))
      if (tol) {
        options.tolerance = tol.value
        options.toleranceUnit = tol.unit
      }
    }
  }

  return options
}

function compileSimpleAssertionToFormula(
  assertion: RelationAssertion | SizeAssertion | TopologyAssertion,
): FormulaNode {
  const options = buildOptionsFromAssertion(assertion)
  const isUnary = assertion.type === 'SizeAssertion'
    || (assertion.type === 'RelationAssertion'
      && (assertion.relation === 'atLeast' || assertion.relation === 'atMost'))

  let predicateName: string
  let args: VariableRef[]

  if (assertion.type === 'RelationAssertion') {
    predicateName = assertion.relation
    args = isUnary ? [subjectVar] : [subjectVar, referenceVar]
  } else if (assertion.type === 'SizeAssertion') {
    if (assertion.property === 'aspectRatio') {
      predicateName = 'aspectRatio'
    } else if (assertion.bounds.min && assertion.bounds.max) {
      predicateName = 'between'
    } else if (assertion.bounds.max) {
      predicateName = 'atMost'
    } else if (assertion.bounds.min) {
      predicateName = 'atLeast'
    } else {
      predicateName = 'atLeast'
    }
    args = [subjectVar]
  } else {
    predicateName = assertion.predicate
    args = assertion.reference ? [subjectVar, referenceVar] : [subjectVar]
  }

  let body: FormulaNode = {
    type: 'FormulaNode',
    kind: 'predicate',
    predicate: predicateName,
    args,
    ...(Object.keys(options).length > 0 ? { options } : {}),
  } as FormulaNode

  // Negation
  if ((assertion as any).negated) {
    body = {
      type: 'FormulaNode',
      kind: 'not',
      operand: body,
    }
  }

  // Bindings
  const subjectBinding = makeBinding('$subject', assertion.subject.value)
  const bindings: TupleBinding[] = [subjectBinding]

  if (!isUnary && assertion.type !== 'TopologyAssertion') {
    const ref = (assertion as RelationAssertion).reference
    if (ref?.value) {
      bindings.push(makeBinding('$reference', ref.value))
    }
  }
  if (assertion.type === 'TopologyAssertion' && assertion.reference?.value) {
    bindings.push(makeBinding('$reference', assertion.reference.value))
  }

  return {
    type: 'FormulaNode',
    kind: 'forall',
    bindings,
    body,
  } as FormulaNode
}

function compileQuantifierToFormula(
  assertion: CompoundAssertion,
  body: FormulaNode,
): FormulaNode {
  const quantifier = assertion.quantifier?.kind
  const subject = (assertion.children[0] as any).subject as SelectorRef
  const reference = (assertion.children[0] as any).reference as SelectorRef | undefined

  const subjectBinding = makeBinding('$subject', subject.value)

  if (quantifier === 'any') {
    const refBinding = reference?.value
      ? makeBinding('$reference', reference.value)
      : null
    return {
      type: 'FormulaNode',
      kind: 'exists',
      bindings: [subjectBinding],
      body: refBinding
        ? {
            type: 'FormulaNode',
            kind: 'forall',
            bindings: [refBinding],
            body,
          }
        : body,
    } as FormulaNode
  }

  if (quantifier === 'none') {
    const refBinding = reference?.value
      ? makeBinding('$reference', reference.value)
      : null
    return {
      type: 'FormulaNode',
      kind: 'forall',
      bindings: [subjectBinding],
      body: {
        type: 'FormulaNode',
        kind: 'not',
        operand: refBinding
          ? {
              type: 'FormulaNode',
              kind: 'exists',
              bindings: [refBinding],
              body,
            }
          : body,
      },
    } as FormulaNode
  }

  // Default / 'all'
  const bindings: TupleBinding[] = [subjectBinding]
  if (reference?.value) {
    bindings.push(makeBinding('$reference', reference.value))
  }
  return {
    type: 'FormulaNode',
    kind: 'forall',
    bindings,
    body,
  } as FormulaNode
}

/**
 * Compile a single DSL assertion AST node to a FOL FormulaNode.
 * Handles RelationAssertion, SizeAssertion, TopologyAssertion,
 * and CompoundAssertion (with operators and/or quantifiers).
 */
export function compileToFormula(assertion: AssertionNode): FormulaNode | null {
  if (!assertion) return null

  // Compound assertion: operator (and/or) or quantifier wrapper
  if (assertion.type === 'CompoundAssertion') {
    const compound = assertion as CompoundAssertion

    if (compound.operator) {
      // Logical compound: compile children and wrap in and/or
      const children = (compound.children || [])
        .map((child) => compileToFormula(child))
        .filter((f): f is FormulaNode => f !== null)

      if (children.length === 0) return null
      if (children.length === 1) return children[0]

      let result = children[0]
      for (let i = 1; i < children.length; i++) {
        result = {
          type: 'FormulaNode',
          kind: compound.operator,
          left: result,
          right: children[i],
        } as FormulaNode
      }

      // If quantifier is present, wrap the whole compound
      if (compound.quantifier) {
        return compileQuantifierToFormula(compound, result)
      }
      return result
    }

    // Quantifier-only compound
    const childFormulas = (compound.children || [])
      .map((child) => compileToFormula(child))
      .filter((f): f is FormulaNode => f !== null)

    if (childFormulas.length === 0) return null
    const body = childFormulas.length === 1
      ? childFormulas[0]
      : childFormulas.reduce((left, right) => ({
          type: 'FormulaNode',
          kind: 'and',
          left,
          right,
        } as FormulaNode))

    return compileQuantifierToFormula(compound, body)
  }

  // Simple assertions
  if (
    assertion.type === 'RelationAssertion'
    || assertion.type === 'SizeAssertion'
    || assertion.type === 'TopologyAssertion'
  ) {
    return compileSimpleAssertionToFormula(assertion as RelationAssertion | SizeAssertion | TopologyAssertion)
  }

  return null
}

// ---- Dense DSL FOL Compilation (bypasses canonical lowering) ----

/**
 * Convert a DSL grammar FOL formula AST node to a solver FormulaNode.
 *
 * Dense DSL forall/exists formulas use a distinct AST shape from the solver's
 * FormulaNode (e.g. type: 'ForAll' vs type: 'FormulaNode' kind: 'forall').
 * This function bridges the two representations so that parsed dense FOL specs
 * can be evaluated directly by evaluateLogic() without going through canonical
 * clause descriptors.
 *
 * String arguments inside PredicateCall are lifted into implicit forall
 * bindings because the solver only accepts VariableRef and AccessorTerm
 * as predicate arguments.
 */
export function compileDenseFOLToFormula(dslFormula: DslFormulaNode): FormulaNode {
  let freshVarCounter = 0
  function makeFreshVar(): string {
    freshVarCounter += 1
    return `$str_${freshVarCounter}`
  }

  function compile(node: DslFormulaNode): FormulaNode {
    switch (node.type) {
      case 'ForAll': {
        const fa = node as DslForAll
        return {
          type: 'FormulaNode',
          kind: 'forall',
          bindings: [makeTupleBinding(fa.variable, fa.domain)],
          body: compile(fa.body),
        } as FormulaNode
      }
      case 'Exists': {
        const ex = node as DslExists
        return {
          type: 'FormulaNode',
          kind: 'exists',
          bindings: [makeTupleBinding(ex.variable, ex.domain)],
          body: compile(ex.body),
        } as FormulaNode
      }
      case 'And': {
        const a = node as DslAnd
        return {
          type: 'FormulaNode',
          kind: 'and',
          left: compile(a.left),
          right: compile(a.right),
        } as FormulaNode
      }
      case 'Or': {
        const o = node as DslOr
        return {
          type: 'FormulaNode',
          kind: 'or',
          left: compile(o.left),
          right: compile(o.right),
        } as FormulaNode
      }
      case 'Not': {
        const n = node as DslNot
        return {
          type: 'FormulaNode',
          kind: 'not',
          operand: compile(n.operand),
        } as FormulaNode
      }
      case 'Implies': {
        const imp = node as DslImplies
        return {
          type: 'FormulaNode',
          kind: 'implies',
          antecedent: compile(imp.left),
          consequent: compile(imp.right),
        } as FormulaNode
      }
      case 'PredicateCall': {
        const pc = node as DslPredicateCall
        const implicitBindings: TupleBinding[] = []
        const compiledArgs: VariableRef[] = []

        for (const arg of pc.args) {
          if (typeof arg === 'string') {
            const varName = makeFreshVar()
            implicitBindings.push({
              type: 'TupleBinding',
              variables: [varName],
              domain: { type: 'DomainRef', domain: 'elements', selector: arg },
            })
            compiledArgs.push({ type: 'VariableRef', name: varName })
          } else if (typeof arg === 'number') {
            // Numbers are not supported as predicate args in the solver.
            // Skip them — the caller should have encoded numeric values
            // in predicate options instead.
            continue
          } else {
            compiledArgs.push(convertTerm(arg) as VariableRef)
          }
        }

        // Size predicates with comparison operators: width($x) >= 44 → size.atLeast
        let predicateBody: FormulaNode
        if (['width', 'height', 'size'].includes(pc.name) && pc.operator && pc.right !== undefined) {
          const options: Record<string, unknown> = {}
          if (pc.name === 'width') options.dimension = 'width'
          else if (pc.name === 'height') options.dimension = 'height'
          else options.dimension = 'width' // size defaults to width

          let predicateName: string
          switch (pc.operator) {
            case '>=':
              predicateName = 'atLeast'
              options.min = pc.right
              break
            case '<=':
              predicateName = 'atMost'
              options.max = pc.right
              break
            case '==':
              predicateName = 'between'
              options.min = pc.right
              options.max = pc.right
              break
            case '!=':
              // Not-equal is compiled as negated equality
              predicateBody = {
                type: 'FormulaNode',
                kind: 'not',
                operand: {
                  type: 'FormulaNode',
                  kind: 'predicate',
                  predicate: 'between',
                  args: compiledArgs,
                  options: { ...options, min: pc.right, max: pc.right },
                } as FormulaNode,
              } as FormulaNode
              // Wrap implicit bindings if any
              return wrapInForAll(implicitBindings, predicateBody)
            case '>':
              predicateName = 'atLeast'
              options.min = pc.right
              break
            case '<':
              predicateName = 'atMost'
              options.max = pc.right
              break
            default:
              predicateName = pc.name
          }

          predicateBody = {
            type: 'FormulaNode',
            kind: 'predicate',
            predicate: predicateName,
            args: compiledArgs,
            ...(Object.keys(options).length > 0 ? { options } : {}),
          } as FormulaNode
        } else {
          predicateBody = {
            type: 'FormulaNode',
            kind: 'predicate',
            predicate: pc.name,
            args: compiledArgs,
          } as FormulaNode
        }

        // Wrap implicit forall bindings around the predicate body.
        // String literals in predicate args are treated as universally
        // quantified domains (same semantics as canonical clause compilation).
        return wrapInForAll(implicitBindings, predicateBody)
      }
      case 'VariableRef':
      case 'DomainRef':
        // VariableRef and DomainRef are terms, not formulas. They should only
        // appear as arguments inside PredicateCall, never as top-level formulas.
        throw new Error(`DSL ${node.type} is a term, not a formula, and cannot be compiled standalone`)
      default:
        throw new Error(`Unknown DSL formula node type: ${(node as any).type}`)
    }
  }

  return compile(dslFormula)
}

function wrapInForAll(bindings: TupleBinding[], body: FormulaNode): FormulaNode {
  if (bindings.length === 0) return body
  let result = body
  // Wrap from last binding to first so that the outermost forall
  // corresponds to the leftmost argument.
  for (let i = bindings.length - 1; i >= 0; i--) {
    result = {
      type: 'FormulaNode',
      kind: 'forall',
      bindings: [bindings[i]],
      body: result,
    } as FormulaNode
  }
  return result
}

function makeTupleBinding(variable: DslVariableRef, domain: DslDomainRef): TupleBinding {
  return {
    type: 'TupleBinding',
    variables: [variable.name],
    domain: convertDomain(domain),
  }
}

function convertDomain(domain: DslDomainRef): DomainRef {
  const selectorFromVar = domain.variableSelector
    ? `$${domain.variableSelector.name}`
    : undefined
  const extraArgFromVar = domain.variableExtraArg
    ? `$${domain.variableExtraArg.name}`
    : undefined

  // Descendant domains use the first argument as parent and second as filter:
  // descendants($card, '.title') => parentVar: '$card', selector: '.title'
  if (domain.kind === 'descendants') {
    const parentVar = selectorFromVar ?? domain.selector
    const selector = extraArgFromVar ?? (domain as any).extraArg
    return {
      type: 'DomainRef',
      domain: domain.kind,
      selector,
      parentVar,
    }
  }

  // Default mapping for non-descendant domains.
  const selector = selectorFromVar ?? domain.selector
  const parentVar = extraArgFromVar ?? (domain as any).extraArg
  return {
    type: 'DomainRef',
    domain: domain.kind,
    selector,
    parentVar,
  }
}

function convertTerm(term: DslVariableRef | string | number): VariableRef | string | number {
  if (typeof term === 'object' && term !== null && term.type === 'VariableRef') {
    return { type: 'VariableRef', name: (term as DslVariableRef).name }
  }
  return term
}

// ---- Public Compiler ----

export interface CompileResult {
  ast: { type: 'Program'; children: RelationAssertion[] }
  semanticIr: SemanticIr
  executionIr: ExecutionIr
  diagnostics: Diagnostic[]
}

export function compile(
  ast: RelationAssertion[],
  options: CompilerOptions = {},
): CompileResult {
  const programNode = {
    type: 'Program' as const,
    children: ast,
  }

  const { semanticIr, diagnostics } = toSemanticIr(ast, options)
  const executionIr = toExecutionIr(semanticIr)

  return {
    ast: programNode,
    semanticIr,
    executionIr,
    diagnostics,
  }
}