/**
 * Pure first-order logic AST types for Imhotep V1.1.
 *
 * These nodes represent the deterministic scene logic layer:
 *   quantifiers, boolean connectives, predicate calls, and terms.
 *
 * All nodes follow the unist-style shape with source spans.
 */

import type { AstNode } from './ast.js'
import type { Position } from './types.js'

// ---------------------------------------------------------------------------
// Formula Union
// ---------------------------------------------------------------------------

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

// ---------------------------------------------------------------------------
// Quantifier Formulas
// ---------------------------------------------------------------------------

export interface ForAllFormula extends AstNode {
  type: 'FormulaNode'
  kind: 'forall'
  bindings: TupleBinding[]
  body: FormulaNode
}

export interface ExistsFormula extends AstNode {
  type: 'FormulaNode'
  kind: 'exists'
  bindings: TupleBinding[]
  body: FormulaNode
}

// ---------------------------------------------------------------------------
// Boolean Connective Formulas
// ---------------------------------------------------------------------------

export interface AndFormula extends AstNode {
  type: 'FormulaNode'
  kind: 'and'
  left: FormulaNode
  right: FormulaNode
}

export interface OrFormula extends AstNode {
  type: 'FormulaNode'
  kind: 'or'
  left: FormulaNode
  right: FormulaNode
}

export interface NotFormula extends AstNode {
  type: 'FormulaNode'
  kind: 'not'
  operand: FormulaNode
}

export interface ImpliesFormula extends AstNode {
  type: 'FormulaNode'
  kind: 'implies'
  antecedent: FormulaNode
  consequent: FormulaNode
}

// ---------------------------------------------------------------------------
// Atomic Formula: Predicate Call
// ---------------------------------------------------------------------------

export interface PredicateCall extends AstNode {
  type: 'FormulaNode'
  kind: 'predicate'
  predicate: string
  args: TermNode[]
  options?: Record<string, unknown>
}

// ---------------------------------------------------------------------------
// Terms
// ---------------------------------------------------------------------------

export type TermNode = VariableRef | DomainRef | AccessorTerm

export interface VariableRef extends AstNode {
  type: 'VariableRef'
  name: string
}

export interface DomainRef extends AstNode {
  type: 'DomainRef'
  domain: string
  selector?: string
  parentVar?: string
}

export interface AccessorTerm extends AstNode {
  type: 'AccessorTerm'
  variable: string
  property: string
}

// ---------------------------------------------------------------------------
// Tuple Binding (for multi-variable quantification)
// ---------------------------------------------------------------------------

export interface TupleBinding extends AstNode {
  type: 'TupleBinding'
  variables: string[]
  domain: DomainRef
}

// ---------------------------------------------------------------------------
// Property Run Blocks
// ---------------------------------------------------------------------------

export interface PropertyRunBlock extends AstNode {
  type: 'PropertyRunBlock'
  mode: 'sampled' | 'enumerated'
  inputDomain: unknown
  body: AstNode[]
}

export interface SampledRunBlock extends AstNode {
  type: 'SampledRunBlock'
  arbitrary: unknown
  numRuns?: number
  seed?: number
  body: AstNode[]
}

// ---------------------------------------------------------------------------
// Type Guards
// ---------------------------------------------------------------------------

export function isForAllFormula(node: FormulaNode): node is ForAllFormula {
  return node.kind === 'forall'
}

export function isExistsFormula(node: FormulaNode): node is ExistsFormula {
  return node.kind === 'exists'
}

export function isAndFormula(node: FormulaNode): node is AndFormula {
  return node.kind === 'and'
}

export function isOrFormula(node: FormulaNode): node is OrFormula {
  return node.kind === 'or'
}

export function isNotFormula(node: FormulaNode): node is NotFormula {
  return node.kind === 'not'
}

export function isImpliesFormula(node: FormulaNode): node is ImpliesFormula {
  return node.kind === 'implies'
}

export function isPredicateCall(node: FormulaNode): node is PredicateCall {
  return node.kind === 'predicate'
}

export function isVariableRef(node: AstNode): node is VariableRef {
  return node.type === 'VariableRef'
}

export function isDomainRef(node: AstNode): node is DomainRef {
  return node.type === 'DomainRef'
}

export function isAccessorTerm(node: AstNode): node is AccessorTerm {
  return node.type === 'AccessorTerm'
}

export function isTupleBinding(node: AstNode): node is TupleBinding {
  return node.type === 'TupleBinding'
}