// Standalone FOL fluent builders for Imhotep
// Provides first-order logic quantifiers and connectives as a fluent API
// that can be used independently of the main assertion builder.

import type { Position } from 'imhotep-core'

// ---------------------------------------------------------------------------
// FOL AST Node Types (local copies matching migration plan until Stream 1)
// ---------------------------------------------------------------------------

export type FormulaNode =
  | ForAllFormula
  | ExistsFormula
  | AndFormula
  | OrFormula
  | NotFormula
  | ImpliesFormula
  | PredicateCall
  | VariableRef
  | DomainRef

export interface ForAllFormula {
  type: 'ForAll'
  variable: VariableRef
  domain: DomainRef
  body: FormulaNode
  position?: Position
}

export interface ExistsFormula {
  type: 'Exists'
  variable: VariableRef
  domain: DomainRef
  body: FormulaNode
  position?: Position
}

export interface AndFormula {
  type: 'And'
  left: FormulaNode
  right: FormulaNode
  position?: Position
}

export interface OrFormula {
  type: 'Or'
  left: FormulaNode
  right: FormulaNode
  position?: Position
}

export interface NotFormula {
  type: 'Not'
  operand: FormulaNode
  position?: Position
}

export interface ImpliesFormula {
  type: 'Implies'
  left: FormulaNode
  right: FormulaNode
  position?: Position
}

export interface PredicateCall {
  type: 'PredicateCall'
  name: string
  args: (VariableRef | string | number)[]
  /** Comparison operator for size predicates: width($x) >= 44 */
  operator?: string
  /** Right-hand side of comparison operator */
  right?: number | string
  position?: Position
}

export interface VariableRef {
  type: 'VariableRef'
  name: string
  position?: Position
}

export interface DomainRef {
  type: 'DomainRef'
  kind: string
  selector?: string
  extraArg?: string
  /** Variable reference used as selector (e.g. descendants($card, '.title')) */
  variableSelector?: VariableRef
  /** Variable reference used as extra argument */
  variableExtraArg?: VariableRef
  position?: Position
}

// ---------------------------------------------------------------------------
// Fluent Domain Builder
// ---------------------------------------------------------------------------

export class FluentDomain {
  private _kind: string
  private _selector?: string

  constructor(kind: string, selector?: string) {
    this._kind = kind
    this._selector = selector
  }

  toRef(): DomainRef {
    return {
      type: 'DomainRef',
      kind: this._kind,
      selector: this._selector,
    }
  }
}

// ---------------------------------------------------------------------------
// Fluent Formula Builder
// ---------------------------------------------------------------------------

export class FluentFormula {
  private _node: FormulaNode

  constructor(node: FormulaNode) {
    this._node = node
  }

  get node(): FormulaNode {
    return this._node
  }

  and(other: FluentFormula): FluentFormula {
    return new FluentFormula({
      type: 'And',
      left: this._node,
      right: other._node,
    })
  }

  or(other: FluentFormula): FluentFormula {
    return new FluentFormula({
      type: 'Or',
      left: this._node,
      right: other._node,
    })
  }

  implies(other: FluentFormula): FluentFormula {
    return new FluentFormula({
      type: 'Implies',
      left: this._node,
      right: other._node,
    })
  }

  not(): FluentFormula {
    return new FluentFormula({
      type: 'Not',
      operand: this._node,
    })
  }
}

// ---------------------------------------------------------------------------
// Quantifier Builders
// ---------------------------------------------------------------------------

export function forAll(variableName: string, domain: FluentDomain, body: (v: VariableRef) => FluentFormula): FluentFormula {
  const varRef: VariableRef = { type: 'VariableRef', name: variableName }
  const bodyFormula = body(varRef)
  return new FluentFormula({
    type: 'ForAll',
    variable: varRef,
    domain: domain.toRef(),
    body: bodyFormula.node,
  })
}

export function exists(variableName: string, domain: FluentDomain, body: (v: VariableRef) => FluentFormula): FluentFormula {
  const varRef: VariableRef = { type: 'VariableRef', name: variableName }
  const bodyFormula = body(varRef)
  return new FluentFormula({
    type: 'Exists',
    variable: varRef,
    domain: domain.toRef(),
    body: bodyFormula.node,
  })
}

// ---------------------------------------------------------------------------
// Predicate Builder
// ---------------------------------------------------------------------------

export function predicate(name: string, ...args: (VariableRef | string | number)[]): FluentFormula {
  return new FluentFormula({
    type: 'PredicateCall',
    name,
    args,
  })
}

// ---------------------------------------------------------------------------
// Domain Constructors
// ---------------------------------------------------------------------------

export const domain = {
  elements(selector: string): FluentDomain {
    return new FluentDomain('elements', selector)
  },
  descendants(parent: VariableRef | string, selector: string): FluentDomain {
    return new FluentDomain('descendants', selector)
  },
  lineBoxes(text: VariableRef | string): FluentDomain {
    // Store the selector argument to match string DSL semantics.
    const selector = typeof text === 'string' ? text : text.name
    return new FluentDomain('lineBoxes', selector)
  },
  custom(kind: string, selector?: string): FluentDomain {
    return new FluentDomain(kind, selector)
  },
}