/**
 * World extraction pipeline for Imhotep Playwright.
 *
 * Handles collecting geometry from the browser (fast path via page.evaluate
 * or CDP protocol), building the solver-ready world, and evaluating FOL
 * assertions against it.  Also includes compatibility reporting.
 */

import path from 'path'
import fs from 'fs'
import { createRequire } from 'module'
import type { Page } from 'playwright'
import {
  FluentRelation,
  FluentQuantifier,
  parseSpec,
  lowerToCanonical,
} from 'imhotep-dsl'
import type { FluentAssertion, CanonicalClauseDescriptor } from 'imhotep-dsl'
import type {
  ImhotepResult,
  ClauseResult,
  ImhotepDiagnostic,
  DiagnosticCode,
  NormalizedContract,
  DomainValue,
  SourceReference,
} from 'imhotep-core'
import { adaptCanonicalWorldToSolver } from 'imhotep-core'
import type { DomainRef, FormulaNode } from 'imhotep-core'
import {
  isForAllFormula,
  isExistsFormula,
  isAndFormula,
  isOrFormula,
  isNotFormula,
  isImpliesFormula,
  isPredicateCall,
} from 'imhotep-core'
import {
  computeGeometryCacheKey,
  readCachedExtractionResult,
  writeCachedExtractionResult,
  getDefaultCacheDir,
} from 'imhotep-core'
import type { GeometryWorld } from 'imhotep-solver'
import {
  evaluateLogic,
  registerDefaultPredicates,
  getPredicateEvaluator,
  type DomainResolver,
  BindingEnv,
} from 'imhotep-solver'
import {
  getPredicateRequiredFacts,
  getPredicateDiagnosticCode,
  getPredicateDecomposition,
  isUnaryPredicate,
  isVariableArityPredicate,
  getPredicateSpec,
} from 'imhotep-core'
import { buildGeometryWorld } from './world-builder.js'
import {
  materializeSemanticSelector,
  type SelectorPlan,
} from './semantic-subjects.js'
import {
  CDPExtractor,
  createSessionManager,
  resolveSelector,
  adaptSnapshotToCanonical,
} from 'imhotep-cdp'
import { lookupCode } from 'imhotep-reporter'
import type { ImhotepUi, CompatibilityReport, CompatibilityCheck } from './public-types.js'

const cjsRequire = createRequire(import.meta.url)

const assertionStore = new WeakMap<ImhotepUi, (FluentRelation | FluentAssertion | FluentQuantifier)[]>()
const specStore = new WeakMap<ImhotepUi, string[]>()

const extractionPathStats = {
  fastPathHits: 0,
  cdpFallbacks: 0,
}

const pageCacheNamespace = new WeakMap<Page, string>()
let pageCacheNamespaceCounter = 0

function getPageCacheNamespace(page: Page): string {
  const existing = pageCacheNamespace.get(page)
  if (existing) return existing
  const ns = `page-${++pageCacheNamespaceCounter}`
  pageCacheNamespace.set(page, ns)
  return ns
}

let extractionStatsHookInstalled = false
let compatibilityWarningEmitted = false

function maybeInstallExtractionStatsHook(): void {
  if (extractionStatsHookInstalled) return
  if (process.env.IMHOTEP_EXTRACT_STATS !== '1') return
  extractionStatsHookInstalled = true
  process.on('exit', () => {
    const total = extractionPathStats.fastPathHits + extractionPathStats.cdpFallbacks
    const fastPct = total > 0 ? ((extractionPathStats.fastPathHits / total) * 100).toFixed(1) : '0.0'
    const cdpPct = total > 0 ? ((extractionPathStats.cdpFallbacks / total) * 100).toFixed(1) : '0.0'
    console.log(
      `[imhotep] extraction path stats: fast=${extractionPathStats.fastPathHits} (${fastPct}%), cdp=${extractionPathStats.cdpFallbacks} (${cdpPct}%), total=${total}`,
    )
  })
}

export {
  assertionStore,
  specStore,
  extractionPathStats,
  getPageCacheNamespace,
  maybeInstallExtractionStatsHook,
}

// ---------------------------------------------------------------------------
// Formula AST walkers
// ---------------------------------------------------------------------------

/**
 * Walk a formula AST and collect all predicate names.
 */
export function collectPredicates(formula: FormulaNode): string[] {
  const predicates: string[] = []
  function walk(node: FormulaNode) {
    if (isPredicateCall(node)) {
      predicates.push(node.predicate)
    } else if (isForAllFormula(node) || isExistsFormula(node)) {
      walk(node.body)
    } else if (isAndFormula(node) || isOrFormula(node)) {
      walk(node.left)
      walk(node.right)
    } else if (isNotFormula(node)) {
      walk(node.operand)
    } else if (isImpliesFormula(node)) {
      walk(node.antecedent)
      walk(node.consequent)
    }
  }
  walk(formula)
  return predicates
}

export function formulaNeedsCssLengthMetrics(formula: FormulaNode): boolean {
  let needs = false
  const scanValue = (value: unknown): void => {
    if (needs || value == null) return
    if (Array.isArray(value)) {
      for (const item of value) scanValue(item)
      return
    }
    if (typeof value !== 'object') return
    const obj = value as Record<string, unknown>
    if (typeof obj.unit === 'string') {
      const unit = obj.unit.toLowerCase()
      if (unit === 'ch' || unit === 'em' || unit === 'rem') {
        needs = true
        return
      }
    }
    for (const child of Object.values(obj)) scanValue(child)
  }
  const walk = (node: FormulaNode): void => {
    if (needs) return
    if (isPredicateCall(node)) {
      scanValue(node.options)
      return
    }
    if (isForAllFormula(node) || isExistsFormula(node)) {
      walk(node.body)
      return
    }
    if (isAndFormula(node) || isOrFormula(node)) {
      walk(node.left)
      walk(node.right)
      return
    }
    if (isNotFormula(node)) {
      walk(node.operand)
      return
    }
    if (isImpliesFormula(node)) {
      walk(node.antecedent)
      walk(node.consequent)
    }
  }
  walk(formula)
  return needs
}

/**
 * Compute the minimal set of facts required by a collection of formulas.
 */
export function computeRequiredFacts(formulas: FormulaNode[]): {
  geometry: boolean
  topology: boolean
  styles: boolean
  fragments: boolean
  domAncestry: boolean
} {
  const facts = new Set<string>()
  for (const formula of formulas) {
    const predicates = collectPredicates(formula)
    for (const p of predicates) {
      const required = getPredicateRequiredFacts(p)
      for (const f of required) {
        facts.add(f)
      }
    }
  }

  const needsCssLengthMetrics = formulas.some((formula) => formulaNeedsCssLengthMetrics(formula))

  const needsDomAncestry = formulas.some((formula) => {
    let found = false
    const scan = (node: FormulaNode) => {
      if (found) return
      if (isForAllFormula(node) || isExistsFormula(node)) {
        for (const b of node.bindings) {
          if (b.domain.parentVar) { found = true; return }
        }
        scan(node.body)
      } else if (isAndFormula(node) || isOrFormula(node)) {
        scan(node.left); scan(node.right)
      } else if (isNotFormula(node)) {
        scan(node.operand)
      } else if (isImpliesFormula(node)) {
        scan(node.antecedent); scan(node.consequent)
      }
    }
    scan(formula)
    return found
  })

  const needsTopology = Array.from(facts).some((f) => f.startsWith('topology.') || f.endsWith('.clipChain'))

  return {
    geometry: true, // Always required for subject resolution
    topology: needsTopology,
    styles: facts.has('styles') || facts.has('computedStyle') || needsCssLengthMetrics,
    fragments: facts.has('subject.fragmentCount') || facts.has('subject.firstFragmentId'),
    domAncestry: needsDomAncestry,
  }
}

export function usesLayoutSpace(formula: FormulaNode): boolean {
  let found = false
  function walk(node: FormulaNode) {
    if (found) return
    if (isPredicateCall(node)) {
      if (node.options?.space === 'layout') {
        found = true
      }
    } else if (isForAllFormula(node) || isExistsFormula(node)) {
      walk(node.body)
    } else if (isAndFormula(node) || isOrFormula(node)) {
      walk(node.left)
      walk(node.right)
    } else if (isNotFormula(node)) {
      walk(node.operand)
    } else if (isImpliesFormula(node)) {
      walk(node.antecedent)
      walk(node.consequent)
    }
  }
  walk(formula)
  return found
}

// ---------------------------------------------------------------------------
// ch Width Measurement
// ---------------------------------------------------------------------------

export async function measureChWidthsByPlan(
  playwrightPage: Page,
  plans: SelectorPlan[],
): Promise<Map<string, number[]>> {
  const measured = await playwrightPage.evaluate((inputPlans: Array<{ key: string; queries: string[] }>) => {
    const out: Array<[string, number[]]> = []
    const canvas = document.createElement('canvas')
    const ctx = canvas.getContext('2d')
    const fallbackMeasure = (el: HTMLElement): number => {
      const probe = document.createElement('span')
      probe.textContent = '0'
      probe.style.position = 'absolute'
      probe.style.visibility = 'hidden'
      probe.style.left = '-99999px'
      probe.style.top = '0'
      const cs = window.getComputedStyle(el)
      probe.style.font = cs.font
      probe.style.letterSpacing = cs.letterSpacing
      probe.style.fontKerning = cs.fontKerning as any
      probe.style.fontVariant = cs.fontVariant
      document.body.appendChild(probe)
      const w = probe.getBoundingClientRect().width
      probe.remove()
      return w
    }

    const measure = (el: HTMLElement): number => {
      const cs = window.getComputedStyle(el)
      if (ctx) {
        ctx.font = cs.font
        const w = ctx.measureText('0').width
        if (Number.isFinite(w) && w > 0) return w
      }
      const fallback = fallbackMeasure(el)
      if (Number.isFinite(fallback) && fallback > 0) return fallback
      const fontSize = Number.parseFloat(cs.fontSize)
      return Number.isFinite(fontSize) && fontSize > 0 ? fontSize * 0.5 : 8
    }

    for (const plan of inputPlans) {
      const widths: number[] = []
      for (const query of plan.queries) {
        const nodes = document.querySelectorAll(query)
        for (let i = 0; i < nodes.length; i++) {
          widths.push(measure(nodes[i] as HTMLElement))
        }
      }
      out.push([plan.key, widths])
    }
    return out
  }, plans)
  return new Map<string, number[]>(measured)
}

export function attachMeasuredChWidths(
  world: GeometryWorld,
  selectorToIds: Map<string, number[]>,
  chWidthsBySelector: Map<string, number[]>,
): void {
  const worldAny = world as any
  const styles = worldAny.styles as {
    subjectId?: number[]
    fontSize?: number[]
    chWidth?: number[]
  } | undefined
  if (!styles) return
  const bySubject = new Map<number, number>()
  for (const [key, ids] of selectorToIds) {
    const widths = chWidthsBySelector.get(key)
    if (!widths || widths.length === 0) continue
    const n = Math.min(ids.length, widths.length)
    for (let i = 0; i < n; i++) {
      const subjectId = ids[i]
      const width = Number(widths[i])
      if (!Number.isFinite(subjectId) || !Number.isFinite(width) || width <= 0) continue
      if (!bySubject.has(subjectId)) bySubject.set(subjectId, width)
    }
  }
  if (bySubject.size === 0) return

  const styleSubjectIds = styles.subjectId
  if (styleSubjectIds && styleSubjectIds.length > 0) {
    const chWidth = new Array(styleSubjectIds.length)
    for (let i = 0; i < styleSubjectIds.length; i++) {
      const subjectId = Number(styleSubjectIds[i])
      const measured = bySubject.get(subjectId)
      if (measured !== undefined) {
        chWidth[i] = measured
        continue
      }
      const fs = Number(styles.fontSize?.[i])
      chWidth[i] = Number.isFinite(fs) && fs > 0 ? fs * 0.5 : 8
    }
    styles.chWidth = chWidth
    return
  }

  const subjectIds = world.subjects?.ids ?? []
  const chWidth = new Array(subjectIds.length)
  for (let i = 0; i < subjectIds.length; i++) {
    const measured = bySubject.get(subjectIds[i])
    if (measured !== undefined) {
      chWidth[i] = measured
      continue
    }
    const fs = Number(styles.fontSize?.[i])
    chWidth[i] = Number.isFinite(fs) && fs > 0 ? fs * 0.5 : 8
  }
  styles.chWidth = chWidth
}

// ---------------------------------------------------------------------------
// Fast Geometry Extraction
// ---------------------------------------------------------------------------

export async function extractWorldFastGeometry(
  playwrightPage: Page,
  selectors: string[],
  requiredFacts?: { geometry: boolean; topology: boolean; styles: boolean; fragments: boolean; domAncestry: boolean },
): Promise<{ world: GeometryWorld; selectorToIds: Map<string, number[]>; errors: ImhotepDiagnostic[] }> {
  interface FastExtractedElement {
    tagName: string
    rect: { x: number; y: number; width: number; height: number }
    fragments?: Array<{ left: number; top: number; right: number; bottom: number }>
    transform?: { matrix: number[]; originX: number; originY: number }
    style?: {
      display: string
      position: string
      overflowX: string
      overflowY: string
      visibility: string
      pointerEvents: string
      opacity: number
      zIndex: string
      lineHeight: number
      fontFamily: string
      fontSize: number
      fontWeight: number
      chWidth: number
    }
  }
  interface FastExtractedPayload {
    elements: FastExtractedElement[]
    selectorToIds: Array<[string, number[]]>
  }

  const selectorPlans: SelectorPlan[] = []
  for (let i = 0; i < selectors.length; i++) {
    const queries = await materializeSemanticSelector(playwrightPage, selectors[i], i)
    selectorPlans.push({ key: selectors[i], queries })
  }

  try {
    const extracted = await playwrightPage.evaluate(({ plans, needs }: any) => {
      const elements: FastExtractedElement[] = []
      const selectorToIds: Array<[string, number[]]> = []

      for (const plan of plans) {
        const ids: number[] = []
        for (const query of plan.queries) {
          const matches = document.querySelectorAll(query)
          for (let i = 0; i < matches.length; i++) {
            const el = matches[i] as HTMLElement
            const rect = el.getBoundingClientRect()
            const subjectId = elements.length + 1
            elements.push({
              tagName: el.tagName.toLowerCase(),
              rect: {
                x: rect.left,
                y: rect.top,
                width: rect.width,
                height: rect.height,
              },
              ...(needs.fragments
                ? {
                    fragments: Array.from(el.getClientRects()).map((r) => ({
                      left: r.left,
                      top: r.top,
                      right: r.right,
                      bottom: r.bottom,
                    })),
                  }
                : {}),
              ...(needs.styles || needs.geometry
                ? {
                    transform: (() => {
                      const cs = window.getComputedStyle(el)
                      const t = cs.transform
                      let matrix = [1, 0, 0, 1, 0, 0]
                      if (t && t !== 'none') {
                        const m = t.match(/matrix\(([^)]+)\)/)
                        if (m) matrix = m[1].split(',').map(Number)
                      }
                      const origin = cs.transformOrigin.split(' ').map(parseFloat)
                      return { matrix, originX: origin[0] || 0, originY: origin[1] || 0 }
                    })(),
                  }
                : {}),
              ...(needs.styles
                ? {
                    style: (() => {
                      const cs = window.getComputedStyle(el)
                      const canvas = document.createElement('canvas')
                      const ctx = canvas.getContext('2d')
                      let chWidth = 0
                      if (ctx) {
                        ctx.font = cs.font
                        chWidth = ctx.measureText('0').width
                      }
                      if (!(Number.isFinite(chWidth) && chWidth > 0)) {
                        const probe = document.createElement('span')
                        probe.textContent = '0'
                        probe.style.position = 'absolute'
                        probe.style.visibility = 'hidden'
                        probe.style.left = '-99999px'
                        probe.style.top = '0'
                        probe.style.font = cs.font
                        document.body.appendChild(probe)
                        chWidth = probe.getBoundingClientRect().width
                        probe.remove()
                      }
                      return {
                        display: cs.display,
                        position: cs.position,
                        overflowX: cs.overflowX,
                        overflowY: cs.overflowY,
                        visibility: cs.visibility,
                        pointerEvents: cs.pointerEvents,
                        contain: cs.contain,
                        opacity: Number.parseFloat(cs.opacity) || 1,
                        zIndex: cs.zIndex,
                        lineHeight: Number.parseFloat(cs.lineHeight) || 0,
                        fontFamily: cs.fontFamily || '',
                        fontSize: Number.parseFloat(cs.fontSize) || 0,
                        fontWeight: Number.parseInt(cs.fontWeight, 10) || 400,
                        chWidth: Number.isFinite(chWidth) && chWidth > 0
                          ? chWidth
                          : (Number.parseFloat(cs.fontSize) || 16) * 0.5,
                      }
                    })(),
                  }
                : {}),
            })
            ids.push(subjectId)
          }
        }
        selectorToIds.push([plan.key, ids])
      }

      return { elements, selectorToIds }
    }, {
      plans: selectorPlans,
      needs: {
        fragments: requiredFacts?.fragments === true,
        styles: requiredFacts?.styles === true,
        geometry: requiredFacts?.geometry !== false,
      },
    }) as FastExtractedPayload

    const world = buildGeometryWorld(extracted.elements) as GeometryWorld
    const worldAny = world as any

    if (requiredFacts?.fragments) {
      const fragmentId: number[] = []
      const subjectId: number[] = []
      const fragmentKind: number[] = []
      const boxLeft: number[] = []
      const boxTop: number[] = []
      const boxRight: number[] = []
      const boxBottom: number[] = []
      const lineIndex: number[] = []
      const flowIndex: number[] = []
      const parentFragmentId: number[] = []

      const firstFragmentIds: number[] = Array.from({ length: extracted.elements.length }, () => 0)
      const fragmentCounts: number[] = Array.from({ length: extracted.elements.length }, () => 0)

      for (let i = 0; i < extracted.elements.length; i++) {
        const frags = extracted.elements[i].fragments ?? []
        if (frags.length > 0) {
          firstFragmentIds[i] = fragmentId.length
          fragmentCounts[i] = frags.length
        }
        for (let j = 0; j < frags.length; j++) {
          const f = frags[j]
          fragmentId.push(fragmentId.length)
          subjectId.push(i + 1)
          fragmentKind.push(1)
          boxLeft.push(f.left)
          boxTop.push(f.top)
          boxRight.push(f.right)
          boxBottom.push(f.bottom)
          lineIndex.push(j)
          flowIndex.push(0)
          parentFragmentId.push(0)
        }
      }

      worldAny.fragments = {
        fragmentId,
        subjectId,
        fragmentKind,
        boxLeft,
        boxTop,
        boxRight,
        boxBottom,
        lineIndex,
        flowIndex,
        parentFragmentId,
      }
      worldAny.subjects.firstFragmentId = firstFragmentIds
      worldAny.subjects.fragmentCount = fragmentCounts
    }

    if (requiredFacts?.geometry) {
      const transformId: number[] = []
      const transformSubjectId: number[] = []
      const matrixStart: number[] = []
      const matrixLength: number[] = []
      const originX: number[] = []
      const originY: number[] = []
      const matrices: number[] = []

      for (let i = 0; i < extracted.elements.length; i++) {
        const t = extracted.elements[i].transform
        if (!t) continue
        const start = matrices.length
        matrices.push(...t.matrix)
        transformId.push(transformId.length)
        transformSubjectId.push(i + 1)
        matrixStart.push(start)
        matrixLength.push(t.matrix.length)
        originX.push(t.originX)
        originY.push(t.originY)
      }

      worldAny.transforms = {
        transformId,
        subjectId: transformSubjectId,
        matrixStart,
        matrixLength,
        originX,
        originY,
      }
      worldAny.matrices = { values: matrices }
    }

    if (requiredFacts?.styles) {
      const strings = worldAny.strings?.values ?? []
      const stringToId = new Map<string, number>()
      for (let i = 0; i < strings.length; i++) stringToId.set(strings[i], i)
      const intern = (value: string): number => {
        const existing = stringToId.get(value)
        if (existing !== undefined) return existing
        const id = strings.length
        strings.push(value)
        stringToId.set(value, id)
        return id
      }

      const styleSubjectId: number[] = []
      const display: number[] = []
      const position: number[] = []
      const zIndexKind: number[] = []
      const zIndexValue: number[] = []
      const overflowX: number[] = []
      const overflowY: number[] = []
      const opacity: number[] = []
      const visibility: number[] = []
      const containFlags: number[] = []
      const pointerEvents: number[] = []
      const lineHeight: number[] = []
      const fontFamilyStringId: number[] = []
      const fontSize: number[] = []
      const fontWeight: number[] = []
      const chWidth: number[] = []

      for (let i = 0; i < extracted.elements.length; i++) {
        const s = extracted.elements[i].style
        if (!s) continue
        styleSubjectId.push(i + 1)
        display.push(intern(s.display))
        position.push(intern(s.position))
        overflowX.push(intern(s.overflowX))
        overflowY.push(intern(s.overflowY))
        visibility.push(intern(s.visibility))
        pointerEvents.push(intern(s.pointerEvents))
        zIndexKind.push(s.zIndex === 'auto' ? 0 : 1)
        zIndexValue.push(s.zIndex === 'auto' ? 0 : Number.parseInt(s.zIndex, 10) || 0)
        opacity.push(s.opacity)
        const csContain = (s as any).contain
        let flags = 0
        if (typeof csContain === 'string') {
          for (const part of csContain.split(/\s+/)) {
            switch (part) {
              case 'layout': flags |= 1; break
              case 'paint': flags |= 2; break
              case 'size': flags |= 4; break
              case 'style': flags |= 8; break
              case 'strict': flags |= 15; break
              case 'content': flags |= 7; break
              case 'inline-size': flags |= 16; break
            }
          }
        }
        containFlags.push(flags)
        lineHeight.push(s.lineHeight)
        fontFamilyStringId.push(intern(s.fontFamily))
        fontSize.push(s.fontSize)
        fontWeight.push(s.fontWeight)
        chWidth.push(s.chWidth)
      }

      worldAny.strings = { values: strings }
      worldAny.styles = {
        subjectId: styleSubjectId,
        display,
        position,
        zIndexKind,
        zIndexValue,
        overflowX,
        overflowY,
        opacity,
        visibility,
        containFlags,
        pointerEvents,
        lineHeight,
        fontFamilyStringId,
        fontSize,
        fontWeight,
        chWidth,
      }
    }

    const selectorToIds = new Map<string, number[]>(extracted.selectorToIds)
    const errors: ImhotepDiagnostic[] = []

    for (const [selector, ids] of selectorToIds) {
      if (ids.length === 0 && !selector.startsWith('$')) {
        errors.push({
          code: 'IMH_SELECTOR_ZERO_MATCHES',
          severity: 'error',
          category: 'extraction-error',
          message: `Selector "${selector}" resolved to 0 elements.`,
          source: 'imhotep-playwright',
          related: [],
          fixHints: [
            `Check that "${selector}" is a valid CSS selector or semantic reference.`,
            `Use ui.extract('${selector}') to verify the selector resolves to at least one element.`,
          ],
          metrics: {},
          sourceRef: { selector },
        })
      }
    }

    return { world, selectorToIds, errors }
  } finally {
    await playwrightPage.evaluate(() => {
      const nodes = Array.from(document.querySelectorAll('[data-imhotep-runtime-id]'))
      for (const el of nodes) {
        el.removeAttribute('data-imhotep-runtime-id')
      }
    }).catch((err) => {
      console.debug('[imhotep-playwright] fast-geometry cleanup evaluate failed:', err instanceof Error ? err.message : err)
    })
  }
}

// ---------------------------------------------------------------------------
// CDP Extraction
// ---------------------------------------------------------------------------

function remapTopologyIds(world: GeometryWorld): void {
  const nSubjects = world.subjects.ids.length
  if (nSubjects === 0) return

  const backendToSolver = new Map<number, number>()
  for (let i = 0; i < nSubjects; i++) {
    backendToSolver.set(world.subjects.domNodeId[i], world.subjects.ids[i])
  }

  const rawSubjectIds = (world as any)._topologySubjectIds as number[] | undefined

  function reorderAndRemap(rawValues: ArrayLike<number>, targetLength: number): number[] {
    if (!rawSubjectIds || rawSubjectIds.length === 0) {
      return remapSimple(rawValues)
    }

    const rawToValue = new Map<number, number>()
    for (let j = 0; j < rawSubjectIds.length; j++) {
      rawToValue.set(rawSubjectIds[j], rawValues[j] ?? 0)
    }

    const out = new Array<number>(targetLength)
    for (let i = 0; i < targetLength; i++) {
      const backendId = world.subjects.domNodeId[i]
      const rawVal = rawToValue.get(backendId) ?? 0
      out[i] = rawVal > 0 ? (backendToSolver.get(rawVal) ?? 0) : 0
    }
    return out
  }

  function remapSimple(src: ArrayLike<number>): number[] {
    const out = new Array<number>(src.length)
    for (let i = 0; i < src.length; i++) {
      const backendId = src[i]
      out[i] = backendId > 0 ? (backendToSolver.get(backendId) ?? 0) : 0
    }
    return out
  }

  const t = world.topology
  t.containingBlockOf = reorderAndRemap(t.containingBlockOf, nSubjects)
  t.nearestPositionedAncestorOf = reorderAndRemap(t.nearestPositionedAncestorOf, nSubjects)
  t.scrollContainerOf = reorderAndRemap(t.scrollContainerOf, nSubjects)
  t.stackingContextOf = reorderAndRemap(t.stackingContextOf, nSubjects)
  t.formattingContextOf = reorderAndRemap(t.formattingContextOf, nSubjects)
  t.clippingRootOf = reorderAndRemap(t.clippingRootOf, nSubjects)

  if (world.clipping) {
    world.clipping.subjectId = remapSimple(world.clipping.subjectId)
  }
  if (world.scroll) {
    world.scroll.containerId = remapSimple(world.scroll.containerId)
  }

  delete (world as any)._topologySubjectIds
}

export async function extractWorldCdp(
  playwrightPage: Page,
  selectors: string[],
  requiredFacts?: { geometry: boolean; topology: boolean; styles: boolean; fragments: boolean; domAncestry: boolean },
): Promise<{ world: GeometryWorld; selectorToIds: Map<string, number[]>; errors: ImhotepDiagnostic[] }> {
  const errors: ImhotepDiagnostic[] = []
  const selectorToNodeIds = new Map<string, number[]>()

  const selectorPlans: SelectorPlan[] = []
  for (let i = 0; i < selectors.length; i++) {
    const queries = await materializeSemanticSelector(playwrightPage, selectors[i], i)
    selectorPlans.push({ key: selectors[i], queries })
  }

  const sessionManager = createSessionManager(playwrightPage)
  try {
    await sessionManager.enableDomain('DOM')

    const allQueries = selectorPlans.flatMap((plan) =>
      plan.queries.map((query) => ({ key: plan.key, query })),
    )
    const allMatches: Awaited<ReturnType<typeof resolveSelector>>[] = []
    for (const { query } of allQueries) {
      allMatches.push(await resolveSelector(sessionManager, query))
    }
    const resolvedSubjects: Array<{ id: string; selector: string; nodeId: number; backendNodeId: number }> = []
    for (let i = 0; i < allQueries.length; i++) {
      const { key, query } = allQueries[i]
      const matches = allMatches[i]
      const ids = selectorToNodeIds.get(key) ?? []
      for (const m of matches) {
        ids.push(m.backendNodeId)
        resolvedSubjects.push({
          id: `sel_${resolvedSubjects.length}`,
          selector: query,
          nodeId: m.nodeId,
          backendNodeId: m.backendNodeId,
        })
      }
      selectorToNodeIds.set(key, ids)
    }
    for (const plan of selectorPlans) {
      const ids = selectorToNodeIds.get(plan.key) ?? []
      if (ids.length === 0) {
        errors.push({
          code: 'IMH_SELECTOR_ZERO_MATCHES',
          severity: 'error',
          category: 'extraction-error',
          message: `Selector "${plan.key}" resolved to 0 elements.`,
          source: 'imhotep-cdp',
          related: [],
          fixHints: [
            `Check that "${plan.key}" is a valid CSS selector or semantic reference.`,
            `Use ui.extract('${plan.key}') to verify the selector resolves to at least one element.`,
          ],
          metrics: {},
          sourceRef: { selector: plan.key },
        })
      }
    }

    const extractor = new CDPExtractor(sessionManager)
    const cdpRequest = {
      requestId: `req_${Date.now()}`,
      sceneTarget: { pageRef: playwrightPage as unknown, url: playwrightPage.url?.() ?? '' },
      env: {
        viewportWidth: 0,
        viewportHeight: 0,
        colorScheme: 'light',
        pointer: 'fine',
      },
      subjects: resolvedSubjects,
      requiredFacts: requiredFacts ?? {
        geometry: true,
        fragments: true,
        styles: true,
        topology: true,
      },
    }
    const cdpResponse = await extractor.extract(cdpRequest)
    if (cdpResponse.status === 'error') {
      throw new Error('CDP extraction failed for relational evaluation')
    }

    const snapshot = cdpResponse.snapshots[0]
    const canonical = adaptSnapshotToCanonical(snapshot)
    const world = adaptCanonicalWorldToSolver(canonical as any) as GeometryWorld
    ;(world as any).styles = {
      subjectId: Array.from(canonical.styles.subjectId),
      lineHeight: Array.from(canonical.styles.lineHeight),
      fontFamilyStringId: Array.from(canonical.styles.fontFamilyStringId),
      fontSize: Array.from(canonical.styles.fontSize),
      fontWeight: Array.from(canonical.styles.fontWeight),
    }

    ;(world as any)._topologySubjectIds = (canonical as any).topology?.subjectIds

    remapTopologyIds(world)

    const selectorToIds = new Map<string, number[]>()
    for (const [selectorKey, nodeIds] of selectorToNodeIds) {
      const idSet = new Set(nodeIds)
      const matches: number[] = []
      for (let i = 0; i < world.subjects.ids.length; i++) {
        const domNodeId = world.subjects.domNodeId[i]
        if (idSet.has(domNodeId)) {
          matches.push(world.subjects.ids[i])
        }
      }
      selectorToIds.set(selectorKey, matches)
    }

    return { world, selectorToIds, errors }
  } finally {
    await playwrightPage.evaluate(() => {
      const nodes = Array.from(document.querySelectorAll('[data-imhotep-runtime-id]'))
      for (const el of nodes) {
        el.removeAttribute('data-imhotep-runtime-id')
      }
    }).catch((err) => {
      console.debug('[imhotep-playwright] CDP cleanup evaluate failed:', err instanceof Error ? err.message : err)
    })
    await sessionManager.detach()
  }
}

// ---------------------------------------------------------------------------
// Orchestrator
// ---------------------------------------------------------------------------

export async function extractWorld(
  playwrightPage: Page,
  selectors: string[],
  cacheDir?: string | null,
  requiredFacts?: { geometry: boolean; topology: boolean; styles: boolean; fragments: boolean; domAncestry: boolean },
  allowFastGeometry = false,
): Promise<{ world: GeometryWorld; selectorToIds: Map<string, number[]>; errors: ImhotepDiagnostic[] }> {
  async function resolveViewport(): Promise<{ width: number; height: number }> {
    const direct = typeof playwrightPage.viewportSize === 'function' ? playwrightPage.viewportSize() : null
    if (direct && direct.width > 0 && direct.height > 0) {
      return { width: direct.width, height: direct.height }
    }
    try {
      const measured = await playwrightPage.evaluate(() => ({
        width: window.innerWidth || document.documentElement?.clientWidth || 0,
        height: window.innerHeight || document.documentElement?.clientHeight || 0,
      }))
      return {
        width: Number.isFinite(measured?.width) ? Number(measured.width) : 0,
        height: Number.isFinite(measured?.height) ? Number(measured.height) : 0,
      }
    } catch (err) {
      console.warn(`[imhotep-playwright] resolveViewport: page.evaluate failed (${err instanceof Error ? err.message : err}), falling back to 0x0 viewport`)
      return { width: 0, height: 0 }
    }
  }

  maybeInstallExtractionStatsHook()
  const filteredSelectors = selectors.filter((s) => typeof s === 'string' && s.length > 0)
  const pageUrl = playwrightPage.url?.() ?? ''
  const viewport = await resolveViewport()
  const env = {
    viewportWidth: viewport.width,
    viewportHeight: viewport.height,
    colorScheme: 'light',
    pointer: 'fine',
  }

  const resolvedCacheDir = cacheDir === null ? null : (cacheDir ?? getDefaultCacheDir())
  const cacheNamespace = getPageCacheNamespace(playwrightPage)
  const cacheSelectors = requiredFacts
    ? [...filteredSelectors, `__imhotep_facts:${requiredFacts.geometry ? 'g' : ''}${requiredFacts.topology ? 't' : ''}${requiredFacts.styles ? 's' : ''}${requiredFacts.fragments ? 'f' : ''}${requiredFacts.domAncestry ? 'a' : ''}:${allowFastGeometry ? 'fast' : 'cdp'}`, `__imhotep_page_ns:${cacheNamespace}`]
    : [...filteredSelectors, `__imhotep_page_ns:${cacheNamespace}`]

  if (resolvedCacheDir !== null) {
    const cacheKey = computeGeometryCacheKey(pageUrl, cacheSelectors, env)
    const cached = await readCachedExtractionResult(resolvedCacheDir, cacheKey)
    if (cached) {
      return {
        world: cached.world as unknown as GeometryWorld,
        selectorToIds: cached.selectorToIds,
        errors: cached.errors as unknown as ImhotepDiagnostic[],
      }
    }
  }

  const useFastGeometry = allowFastGeometry
    && requiredFacts?.geometry === true
    && requiredFacts.topology === false
    && requiredFacts.domAncestry === false

  const result = useFastGeometry
    ? await extractWorldFastGeometry(playwrightPage, filteredSelectors, requiredFacts)
    : await extractWorldCdp(playwrightPage, filteredSelectors, requiredFacts)

  ;(result.world as any).env = {
    ...(result.world as any).env,
    viewportWidth: env.viewportWidth,
    viewportHeight: env.viewportHeight,
  }

  if (requiredFacts?.styles) {
    try {
      const plans: SelectorPlan[] = []
      for (let i = 0; i < filteredSelectors.length; i++) {
        const queries = await materializeSemanticSelector(playwrightPage, filteredSelectors[i], i)
        plans.push({ key: filteredSelectors[i], queries })
      }
      const chWidthsBySelector = await measureChWidthsByPlan(playwrightPage, plans)
      attachMeasuredChWidths(result.world, result.selectorToIds, chWidthsBySelector)
    } catch {
      // Best effort only; solver falls back to font-size heuristic.
    }
  }

  if (useFastGeometry) {
    extractionPathStats.fastPathHits += 1
  } else {
    extractionPathStats.cdpFallbacks += 1
  }

  if (resolvedCacheDir !== null) {
    const cacheKey = computeGeometryCacheKey(pageUrl, cacheSelectors, env)
    await writeCachedExtractionResult(
      resolvedCacheDir,
      cacheKey,
      result.world as unknown as import('imhotep-core').GeometryWorld,
      result.selectorToIds,
      result.errors as any,
    )
  }

  return result
}

// ---------------------------------------------------------------------------
// Domain Resolver
// ---------------------------------------------------------------------------

export function buildAncestorIndex(world: GeometryWorld): Map<number, Set<number>> {
  const ancestors = new Map<number, Set<number>>()
  const nodeIdToSubjectId = new Map<number, number>()

  for (let i = 0; i < world.subjects.ids.length; i++) {
    const sid = world.subjects.ids[i]
    const nodeId = world.subjects.domNodeId[i]
    if (nodeId > 0) {
      nodeIdToSubjectId.set(nodeId, sid)
    }
  }

  if (nodeIdToSubjectId.size === 0) return ancestors

  for (const [cid, sid] of nodeIdToSubjectId) {
    const chain = new Set<number>()
    let current = cid
    while (current > 0) {
      const pos = world.dom.nodeId.indexOf(current)
      if (pos === -1) break
      const parent = world.dom.parentNodeId[pos]
      if (parent <= 0) break
      const parentSid = nodeIdToSubjectId.get(parent)
      if (parentSid !== undefined) {
        chain.add(parentSid)
      }
      current = parent
    }
    if (chain.size > 0) {
      ancestors.set(sid, chain)
    }
  }

  return ancestors
}

export class SelectorDomainResolver implements DomainResolver {
  private domains = new Map<string, DomainValue>()
  private ancestorIndex?: Map<number, Set<number>>

  setAncestorIndex(ancestors: Map<number, Set<number>>) {
    this.ancestorIndex = ancestors
  }

  register(selector: string, subjectIds: number[]) {
    this.domains.set(selector, {
      domainId: `dom_${selector}`,
      subjectIds: new Uint32Array(subjectIds),
      provenance: `elements(${selector})`,
      closed: true,
    })
  }

  private allRegisteredSubjectIds(): number[] {
    const seen = new Set<number>()
    for (const d of this.domains.values()) {
      for (const id of d.subjectIds) {
        seen.add(id)
      }
    }
    return Array.from(seen)
  }

  resolve(domain: DomainRef, env?: BindingEnv): DomainValue | undefined {
    if (domain.parentVar) {
      if (!env || !this.ancestorIndex) return undefined
      const parentId = env.lookup(domain.parentVar)
      if (parentId === undefined) return undefined
      const selector = domain.selector
      const candidateIds = selector
        ? this.domains.get(selector)?.subjectIds
        : this.allRegisteredSubjectIds()
      if (!candidateIds || candidateIds.length === 0) return undefined
      const filtered: number[] = []
      for (const id of candidateIds) {
        const ancestors = this.ancestorIndex.get(id)
        if (ancestors?.has(parentId)) {
          filtered.push(id)
        }
      }
      const key = `descendants_p${parentId}_${selector ?? '*'}`
      return {
        domainId: `dom_${key}`,
        subjectIds: new Uint32Array(filtered),
        provenance: `descendants(parentId=${parentId}, ${selector ?? '*'})`,
        closed: true,
      }
    }
    return this.domains.get(domain.selector ?? domain.domain)
  }
}

// ---------------------------------------------------------------------------
// Canonical Clause → Formula Compilation
// ---------------------------------------------------------------------------

export function compileCanonicalClauseToFormula(clause: CanonicalClauseDescriptor): FormulaNode {
  const extended = clause as CanonicalClauseDescriptor & {
    space?: 'layout' | 'visual'
    options?: Record<string, unknown>
  }
  const subjectVar = { type: 'VariableRef' as const, name: '$subject' }
  const referenceVar = { type: 'VariableRef' as const, name: '$reference' }

  const options: Record<string, unknown> = {}
  if (clause.bounds?.minGap !== undefined) options.minGap = clause.bounds.minGap
  if (clause.bounds?.maxGap !== undefined) options.maxGap = clause.bounds.maxGap
  if (clause.tolerance?.value !== undefined) options.tolerance = clause.tolerance.value
  if (extended.space) options.space = extended.space
  if (extended.options) {
    for (const [k, v] of Object.entries(extended.options)) {
      options[k] = v
    }
  }

  let body: FormulaNode

  const decomp = getPredicateDecomposition(clause.relation)
  const hasInStackingFlag = (clause.flags & 8) !== 0

  if (decomp?.kind === 'between') {
    const minVal = extended.options?.min as number | undefined
    const maxVal = extended.options?.max as number | undefined
    const atLeastOpts: Record<string, unknown> = {}
    const atMostOpts: Record<string, unknown> = {}
    if (extended.options?.dimension !== undefined) {
      atLeastOpts.dimension = extended.options.dimension
      atMostOpts.dimension = extended.options.dimension
    }
    body = {
      type: 'FormulaNode',
      kind: 'and',
      left: {
        type: 'FormulaNode',
        kind: 'predicate',
        predicate: 'atLeast',
        args: [subjectVar],
        ...(minVal !== undefined ? { options: { ...atLeastOpts, value: minVal } } : { options: atLeastOpts }),
      } as FormulaNode,
      right: {
        type: 'FormulaNode',
        kind: 'predicate',
        predicate: 'atMost',
        args: [subjectVar],
        ...(maxVal !== undefined ? { options: { ...atMostOpts, value: maxVal } } : { options: atMostOpts }),
      } as FormulaNode,
    }
  } else if (decomp?.kind === 'negate' && decomp.inner) {
    const innerOpts: Record<string, unknown> = { ...options }
    body = {
      type: 'FormulaNode',
      kind: 'not',
      operand: {
        type: 'FormulaNode',
        kind: 'predicate',
        predicate: decomp.inner,
        args: [subjectVar, referenceVar],
        ...(Object.keys(innerOpts).length > 0 ? { options: innerOpts } : {}),
      } as FormulaNode,
    }
  } else {
    const unaryPredicate = isUnaryPredicate(clause.relation)
      && !(isVariableArityPredicate(clause.relation) && clause.reference)

    body = {
      type: 'FormulaNode',
      kind: 'predicate',
      predicate: clause.relation,
      args: unaryPredicate ? [subjectVar] : [subjectVar, referenceVar],
      ...(Object.keys(options).length > 0 ? { options } : {}),
    } as FormulaNode

    if (hasInStackingFlag && !unaryPredicate) {
      body = {
        type: 'FormulaNode',
        kind: 'and',
        left: body,
        right: {
          type: 'FormulaNode',
          kind: 'predicate',
          predicate: 'inStackingContext',
          args: [subjectVar, referenceVar],
        },
      }
    }
  }

  if (clause.negated) {
    body = {
      type: 'FormulaNode',
      kind: 'not',
      operand: body,
    }
  }

  const subjectBinding = {
    type: 'TupleBinding' as const,
    variables: ['$subject'],
    domain: { type: 'DomainRef' as const, domain: 'elements', selector: clause.subject },
  }
  const referenceBinding = {
    type: 'TupleBinding' as const,
    variables: ['$reference'],
    domain: { type: 'DomainRef' as const, domain: 'elements', selector: clause.reference },
  }

  const isUnary = isUnaryPredicate(clause.relation)
    && !(isVariableArityPredicate(clause.relation) && clause.reference)

  if (isUnary) {
    return {
      type: 'FormulaNode',
      kind: 'forall',
      bindings: [subjectBinding],
      body,
    }
  }

  if (clause.quantifier === 'any') {
    return {
      type: 'FormulaNode',
      kind: 'exists',
      bindings: [subjectBinding],
      body: {
        type: 'FormulaNode',
        kind: 'forall',
        bindings: [referenceBinding],
        body,
      },
    }
  }

  if (clause.quantifier === 'none') {
    return {
      type: 'FormulaNode',
      kind: 'forall',
      bindings: [subjectBinding],
      body: {
        type: 'FormulaNode',
        kind: 'not',
        operand: {
          type: 'FormulaNode',
          kind: 'exists',
          bindings: [referenceBinding],
          body,
        },
      },
    }
  }

  return {
    type: 'FormulaNode',
    kind: 'forall',
    bindings: [subjectBinding, referenceBinding],
    body,
  }
}

// ---------------------------------------------------------------------------
// Selector Extraction from Assertions / Formulas
// ---------------------------------------------------------------------------

export function getSelectorsFromAssertion(assertion: FluentRelation | FluentAssertion | FluentQuantifier): string[] {
  const selectors = new Set<string>()
  const rel = assertion as any
  if (rel.assertion?.getSubject) {
    selectors.add(rel.assertion.getSubject())
  }
  if (rel.referenceSelector) {
    selectors.add(rel.referenceSelector)
  }
  // Extract selectors from compound relation parts (.and / .or chaining)
  const compoundRel = assertion as FluentRelation
  if (compoundRel.isCompound) {
    for (const part of compoundRel.compoundParts) {
      if (part.referenceSelector) {
        selectors.add(part.referenceSelector)
      }
    }
  }
  if (Array.isArray(rel.bindings)) {
    for (const b of rel.bindings) {
      if (b?.selector) selectors.add(b.selector)
      // Extract reference selectors from assertions inside FluentQuantifier bindings
      if (typeof b?.getAssertions === 'function') {
        for (const assertion of b.getAssertions()) {
          if (assertion?.reference?.value) {
            selectors.add(assertion.reference.value)
          }
        }
      }
    }
  }
  return Array.from(selectors)
}

export function getSelectorsFromFormula(formula: FormulaNode): string[] {
  const selectors = new Set<string>()
  const visit = (node: FormulaNode) => {
    if (isForAllFormula(node) || isExistsFormula(node)) {
      for (const b of node.bindings) {
        if (b.domain.selector && !b.domain.selector.startsWith('$')) {
          selectors.add(b.domain.selector)
        }
      }
      visit(node.body)
      return
    }
    if (isAndFormula(node) || isOrFormula(node)) {
      visit(node.left)
      visit(node.right)
      return
    }
    if (isNotFormula(node)) {
      visit(node.operand)
      return
    }
    if (isImpliesFormula(node)) {
      visit(node.antecedent)
      visit(node.consequent)
    }
  }
  visit(formula)
  return Array.from(selectors)
}

// ---------------------------------------------------------------------------
// Clause Label Builders
// ---------------------------------------------------------------------------

export function buildFluentLabel(assertion: FluentRelation | FluentAssertion | FluentQuantifier): string {
  const rel = assertion as any

  // FluentQuantifier
  if (rel.bindings && Array.isArray(rel.bindings)) {
    const firstBinding = rel.bindings[0]
    const selector = firstBinding?.selector || 'unknown'
    return `quantified assertion over '${selector}'`
  }

  // FluentRelation
  if (rel.relation && rel.assertion?.getSubject) {
    const subject = rel.assertion.getSubject()
    const ref = rel.referenceSelector || ''
    const opts = rel.options || {}
    const parts: string[] = [`'${subject}' ${rel.relation}`]
    if (ref) parts.push(`'${ref}'`)
    if (opts.minGap !== undefined) parts.push(`gap ${opts.minGap}px`)
    if (opts.maxGap !== undefined) parts.push(`maxGap ${opts.maxGap}px`)
    if (opts.tolerance !== undefined) parts.push(`tolerance ${opts.tolerance}px`)
    if (opts.axis) parts.push(`axis ${opts.axis}`)
    return parts.join(' ')
  }

  return 'fluent assertion'
}

export function buildDenseLabel(clause: CanonicalClauseDescriptor): string {
  const parts: string[] = [`'${clause.subject}' ${clause.relation}`]
  if (clause.reference) parts.push(`'${clause.reference}'`)
  if (clause.bounds?.minGap !== undefined) parts.push(`gap ${clause.bounds.minGap}px`)
  if (clause.bounds?.maxGap !== undefined) parts.push(`maxGap ${clause.bounds.maxGap}px`)
  if (clause.tolerance) parts.push(`tolerance ${clause.tolerance.value}${clause.tolerance.unit}`)
  if (clause.quantifier && clause.quantifier !== 'all') parts.unshift(clause.quantifier)
  return parts.join(' ')
}

export function buildFOLLabel(folAst: any): string {
  switch (folAst.type) {
    case 'ForAll':
      return `forall ${folAst.variable?.name} in ${folAst.domain?.kind}(${folAst.domain?.selector ?? ''})`
    case 'Exists':
      return `exists ${folAst.variable?.name} in ${folAst.domain?.kind}(${folAst.domain?.selector ?? ''})`
    case 'And':
      return `${buildFOLLabel(folAst.left)} and ${buildFOLLabel(folAst.right)}`
    case 'Or':
      return `${buildFOLLabel(folAst.left)} or ${buildFOLLabel(folAst.right)}`
    case 'Not':
      return `not ${buildFOLLabel(folAst.operand)}`
    case 'Implies':
      return `${buildFOLLabel(folAst.left)} implies ${buildFOLLabel(folAst.right)}`
    case 'PredicateCall':
      return `${folAst.name}(${folAst.args.map((a: any) => a.name ?? a).join(', ')})`
    default:
      return 'FOL formula'
  }
}

// ---------------------------------------------------------------------------
// Normalized Contract Builder
// ---------------------------------------------------------------------------

export function extractCanonicalFromAssertion(
  assertion: FluentRelation | FluentAssertion | FluentQuantifier,
): CanonicalClauseDescriptor[] {
  if (assertion instanceof FluentRelation) {
    const ast = assertion.toAst()
    return lowerToCanonical(ast)
  }
  if (assertion instanceof FluentQuantifier) {
    const descriptors: CanonicalClauseDescriptor[] = []
    for (const binding of assertion.bindings) {
      for (const a of binding.getAssertions()) {
        descriptors.push(...lowerToCanonical(a))
      }
    }
    return descriptors
  }
  return []
}

export function buildNormalizedContracts(
  assertions: (FluentRelation | FluentAssertion | FluentQuantifier)[],
  specs: string[],
): NormalizedContract[] {
  const contracts: NormalizedContract[] = []
  let index = 0

  for (const assertion of assertions) {
    const descriptors = extractCanonicalFromAssertion(assertion)
    for (const desc of descriptors) {
      contracts.push(descriptorToContract(desc, index++))
    }
  }

  for (const source of specs) {
    if (source.trim().length === 0) continue
    const parsed = parseSpec(source)
    if (parsed.diagnostics.some((d) => d.severity === 'error')) continue
    const descriptors = lowerToCanonical(parsed.ast)
    for (const desc of descriptors) {
      contracts.push(descriptorToContract(desc, index++))
    }
  }

  return contracts
}

export function descriptorToContract(
  desc: CanonicalClauseDescriptor,
  index: number,
): NormalizedContract {
  const options: Record<string, unknown> = {}
  if (desc.bounds) {
    if (desc.bounds.minGap !== undefined) options.minGap = desc.bounds.minGap
    if (desc.bounds.maxGap !== undefined) options.maxGap = desc.bounds.maxGap
  }
  if (desc.tolerance) {
    options.tolerance = desc.tolerance.value
    options.toleranceUnit = desc.tolerance.unit
  }
  if (desc.options) {
    for (const [k, v] of Object.entries(desc.options)) {
      if (options[k] === undefined) options[k] = v
    }
  }
  if (desc.quantifier) {
    options.quantifier = desc.quantifier
  }
  if (desc.space) {
    options.space = desc.space
  }

  const labelParts: string[] = []
  labelParts.push(`'${desc.subject}'`)
  labelParts.push(desc.relation)
  if (desc.reference) {
    labelParts.push(`'${desc.reference}'`)
  }

  const optionEntries = Object.entries(options)
  if (optionEntries.length > 0) {
    const optionStr = optionEntries
      .map(([k, v]) => `${k}: ${JSON.stringify(v)}`)
      .join(', ')
    labelParts.push(`with ${optionStr}`)
  }

  return {
    clauseId: `contract_${index}`,
    clauseLabel: labelParts.join(' '),
    relation: desc.relation,
    subject: desc.subject,
    reference: desc.reference || '',
    options,
  }
}

// ---------------------------------------------------------------------------
// Cardinality Assertion Evaluation
// ---------------------------------------------------------------------------

export interface CardinalityResult {
  clauseId: string
  status: ClauseResult['status']
  truth: ClauseResult['truth']
  diagnostics: ImhotepDiagnostic[]
  selector: string
  expectedCount: number
  label: string
}

export function buildCardinalityLabel(kind: 'exactlyOne' | 'atLeastN' | 'atMostN', selector: string, expectedCount: number): string {
  if (kind === 'exactlyOne') return `'${selector}' exactlyOne`
  if (kind === 'atLeastN') return `'${selector}' atLeastN ${expectedCount}`
  return `'${selector}' atMostN ${expectedCount}`
}

export function evaluateCardinalityAssertion(
  assertion: any,
  clauseId: string,
  selectorToIds: Map<string, number[]>,
): CardinalityResult {
  const selector = assertion.assertion?.getSubject?.() ?? assertion.selector ?? ''
  const kind = assertion.kind as 'exactlyOne' | 'atLeastN' | 'atMostN'
  const expectedCount = assertion.expectedCount as number
  const ids = selectorToIds.get(selector) ?? []
  const observedCount = ids.length
  const label = buildCardinalityLabel(kind, selector, expectedCount)

  let pass = false
  let expectedDescription = ''

  switch (kind) {
    case 'exactlyOne':
      pass = observedCount === 1
      expectedDescription = 'exactly 1'
      break
    case 'atLeastN':
      pass = observedCount >= expectedCount
      expectedDescription = `at least ${expectedCount}`
      break
    case 'atMostN':
      pass = observedCount <= expectedCount
      expectedDescription = `at most ${expectedCount}`
      break
  }

  const diagnostics: ImhotepDiagnostic[] = []
  if (!pass) {
    diagnostics.push({
      code: `IMH_CARDINALITY_${kind.toUpperCase()}_FAILED` as DiagnosticCode,
      severity: 'error',
      category: 'contract-failure',
      message: `Selector "${selector}" resolved to ${observedCount} element(s), but expected ${expectedDescription}.`,
      source: 'imhotep-playwright',
      related: [],
      fixHints: [
        `Check that "${selector}" matches the intended number of elements.`,
        `Use ui.extract('${selector}') to verify the selector resolves to the expected count.`,
      ],
      metrics: { observedCount, expectedCount },
      sourceRef: { selector },
      clauseLabel: label,
    })
  }

  return {
    clauseId,
    status: pass ? 'pass' : 'fail',
    truth: 'determinate',
    diagnostics,
    selector,
    expectedCount,
    label,
  }
}

// ---------------------------------------------------------------------------
// Result Adapter: FOL → Public API shape
// ---------------------------------------------------------------------------

export function mapFolDiagnostic(
  d: { code: string; severity: 'error' | 'warning' | 'info'; category?: string; message: string; clauseId?: string },
  metrics?: Record<string, number>,
): ImhotepDiagnostic {
  let code = d.code as DiagnosticCode
  let message = d.message
  const fixHints: string[] = []

  if ((code as string) === 'IMH_LOGIC_PREDICATE_MISSING') {
    code = 'IMH_INTERNAL_UNKNOWN_CLAUSE_KIND'
    fixHints.push('The assertion uses an unsupported relation or predicate.')
    fixHints.push('Supported relations: leftOf, rightOf, above, below, alignedWith, centeredWithin, inside, contains, overlaps.')
  }

  if ((code as string) === 'IMH_PREDICATE_FAILED') {
    const match = message.match(/Predicate "([^"]+)" failed/)
    const predicateName = match?.[1]
    if (predicateName && getPredicateDiagnosticCode(predicateName)) {
      code = getPredicateDiagnosticCode(predicateName) as DiagnosticCode
      const gapMatch = message.match(/gap=([\d.-]+)/)
      const observedGap = gapMatch ? parseFloat(gapMatch[1]) : undefined
      const minGapMatch = message.match(/minGap=([\d.-]+)/)
      const minGap = minGapMatch ? parseFloat(minGapMatch[1]) : undefined
      const maxGapMatch = message.match(/maxGap=([\d.-]+)/)
      const maxGap = maxGapMatch ? parseFloat(maxGapMatch[1]) : undefined
      const gapKind = observedGap !== undefined && maxGap !== undefined && minGap !== undefined
        ? (observedGap < minGap ? 'min' : observedGap > maxGap ? 'max' : 'min')
        : 'min'
      const expectedGap = gapKind === 'min' ? (minGap ?? 0) : (maxGap ?? 0)
      const boundDescription = gapKind === 'min' ? 'minimum required gap' : 'maximum required gap'
      const spec = predicateName ? getPredicateSpec(predicateName) : undefined
      const isDirectional = spec?.validOptions.includes('minGap') ?? false
      if (isDirectional && observedGap !== undefined) {
        message = `${predicateName} assertion failed: measured gap is ${observedGap.toFixed(0)}px, but ${boundDescription} is ${expectedGap}px.`
        fixHints.push(`The measured gap is ${observedGap.toFixed(0)}px. Consider ${gapKind === 'min' ? 'lowering minGap' : 'increasing maxGap'} or checking element positions.`)
      } else if (spec?.isSize) {
        fixHints.push(`Check the expected size threshold and the actual element dimensions using ui.extract(selector).`)
      } else {
        fixHints.push(`Verify the expected layout and consider adjusting thresholds.`)
      }
    } else {
      fixHints.push(`Verify the expected layout and consider adjusting thresholds.`)
    }
  }

  if (code === 'IMH_SELECTOR_ZERO_MATCHES') {
    fixHints.push('Check that the selector is valid and matches an element in the DOM.')
    fixHints.push('Use ui.extract(selector) to verify the selector resolves to at least one element.')
  }

  if (code === 'IMH_EXTRACT_PROTOCOL_ERROR') {
    fixHints.push('Verify the page is fully loaded before running assertions.')
    fixHints.push('Check that selectors are valid CSS selectors or semantic references.')
    fixHints.push('Use ui.extract(selector) to debug selector resolution.')
  }

  if ((code as string) === 'IMH_FEATURE_NOT_YET_IMPLEMENTED') {
    fixHints.push('This assertion uses a relation that is documented but not yet implemented.')
    fixHints.push('Use a supported relation such as leftOf, rightOf, above, below, inside, overlaps, alignedWith, or centeredWithin.')
  }

  const codeStr = code as string
  if (codeStr === 'IMH_PARSE_ERROR' || codeStr === 'IMH_PARSE_INVALID_SYNTAX' || codeStr === 'IMH_PARSE_UNEXPECTED_TOKEN') {
    fixHints.push('Selectors must be single-quoted strings, e.g. \'[data-testid="x"]\'.')
    fixHints.push('Use relation keywords directly without "is": e.g. \'a\' leftOf \'b\'.')
    fixHints.push('Gap values require units: e.g. gap 8px.')
  }

  if (fixHints.length === 0) {
    const entry = lookupCode(code)
    if (entry?.fixHints && entry.fixHints.length > 0) {
      fixHints.push(...entry.fixHints)
    }
  }

  return {
    code,
    severity: d.severity,
    category: (d.category ?? 'internal-error') as ImhotepDiagnostic['category'],
    message,
    clauseId: d.clauseId,
    source: 'imhotep-solver',
    related: [],
    fixHints,
    metrics: metrics ?? {},
    sourceRef: {},
  }
}

interface TraceMetadata {
  sourceRef?: SourceReference
  clauseLabel?: string
}

export function isDuckTypedFluentQuantifier(value: unknown): boolean {
  return !!value
    && typeof value === 'object'
    && Array.isArray((value as any).bindings)
    && typeof (value as any).toFormula === 'function'
}

export function hasSubjectQuantifier(value: unknown): boolean {
  if (!value || typeof value !== 'object') return false
  const assertion = (value as any).assertion
  return !!assertion && typeof assertion.getQuantifier === 'function' && assertion.getQuantifier() !== undefined
}

// ---------------------------------------------------------------------------
// Package Fingerprint & Compatibility
// ---------------------------------------------------------------------------

export function findNearestPackageJson(startPath: string): string | null {
  let current = path.dirname(startPath)
  for (let i = 0; i < 16; i++) {
    const candidate = path.join(current, 'package.json')
    if (fs.existsSync(candidate)) return candidate
    const parent = path.dirname(current)
    if (parent === current) break
    current = parent
  }
  return null
}

export function resolvePackageFingerprint(name: string): { name: string; version: string; resolvedFrom: string } {
  try {
    const resolvedEntry = cjsRequire.resolve(name)
    const pkgJson = findNearestPackageJson(resolvedEntry)
    if (!pkgJson) {
      return {
        name,
        version: 'unknown',
        resolvedFrom: resolvedEntry,
      }
    }
    const content = fs.readFileSync(pkgJson, 'utf8')
    const parsed = JSON.parse(content) as { version?: string }
    return {
      name,
      version: typeof parsed.version === 'string' ? parsed.version : 'unknown',
      resolvedFrom: pkgJson,
    }
  } catch (err) {
    return {
      name,
      version: 'unresolved',
      resolvedFrom: err instanceof Error ? err.message : String(err),
    }
  }
}

export function collectPackageFingerprints(): Array<{ name: string; version: string; resolvedFrom: string }> {
  return [
    resolvePackageFingerprint('imhotep-playwright'),
    resolvePackageFingerprint('imhotep-dsl'),
    resolvePackageFingerprint('imhotep-solver'),
  ]
}

export function buildCompatibilityReport(ui: ImhotepUi): CompatibilityReport {
  const checks: CompatibilityCheck[] = []
  const packageFingerprints = collectPackageFingerprints()

  const packageResolutionOk = packageFingerprints.every((p) => p.version !== 'unresolved')
  checks.push({
    id: 'package-fingerprints-resolved',
    ok: packageResolutionOk,
    details: packageFingerprints.map((p) => `${p.name}@${p.version}`).join(', '),
  })

  const unitsSource = "in viewport:\n  '.probe' atMost 85vw wide\n  '.probe' atMost 60ch wide"
  const parsedUnits = parseSpec(unitsSource)
  const hasUnitsParseError = parsedUnits.diagnostics.some((d) => d.severity === 'error')
  const unitsClauses = hasUnitsParseError ? 0 : lowerToCanonical(parsedUnits.ast).length
  checks.push({
    id: 'dsl-units-vw-ch',
    ok: !hasUnitsParseError && unitsClauses === 2,
    details: hasUnitsParseError
      ? `parse errors: ${parsedUnits.diagnostics.map((d) => String(d.code)).join(', ')}`
      : `parsed clauses=${unitsClauses}`,
  })

  const loweredUnits = hasUnitsParseError ? [] : lowerToCanonical(parsedUnits.ast)
  const firstMax = loweredUnits[0]?.options?.max as any
  const secondMax = loweredUnits[1]?.options?.max as any
  const loweredUnitsOk =
    !!firstMax
    && typeof firstMax === 'object'
    && firstMax.value === 85
    && firstMax.unit === 'vw'
    && !!secondMax
    && typeof secondMax === 'object'
    && secondMax.value === 60
    && secondMax.unit === 'ch'
  checks.push({
    id: 'dsl-size-unit-lowering',
    ok: loweredUnitsOk,
    details: `first=${JSON.stringify(firstMax ?? null)}, second=${JSON.stringify(secondMax ?? null)}`,
  })

  const hasQuantifierHelpers = typeof ui.expect.all === 'function' && typeof ui.expect.any === 'function' && typeof ui.expect.none === 'function'
  checks.push({
    id: 'expect-quantifier-helpers',
    ok: hasQuantifierHelpers,
    details: `all=${typeof ui.expect.all}, any=${typeof ui.expect.any}, none=${typeof ui.expect.none}`,
  })

  const priorAssertions = [...(assertionStore.get(ui) || [])]
  const priorSpecs = [...(specStore.get(ui) || [])]
  let expectAllInvocationOk = false
  let expectAllInvocationDetails = 'not executed'
  try {
    const chain = ui.expect.all('.__imhotep_compat_none__').to.be.atLeast(1, 'height') as any
    expectAllInvocationOk = !!chain && typeof chain === 'object' && !!chain.assertion && chain.assertion.getQuantifier?.() === 'all'
    expectAllInvocationDetails = `chain=${typeof chain}, quantifier=${chain?.assertion?.getQuantifier?.()}`
  } catch (err) {
    expectAllInvocationDetails = err instanceof Error ? err.message : String(err)
  } finally {
    assertionStore.set(ui, priorAssertions)
    specStore.set(ui, priorSpecs)
  }
  checks.push({
    id: 'expect-all-chain-invocation',
    ok: expectAllInvocationOk,
    details: expectAllInvocationDetails,
  })

  const emptyResolver: DomainResolver = {
    resolve(domain, _env?) {
      if (domain.selector === '.none') {
        return {
          domainId: 'dom_none',
          subjectIds: new Uint32Array([]),
          provenance: 'elements(.none)',
          closed: true,
        }
      }
      return undefined
    },
  }

  const emptyWorld = buildGeometryWorld([]) as unknown as GeometryWorld
  const forallEmpty = evaluateLogic({
    formula: {
      type: 'FormulaNode',
      kind: 'forall',
      bindings: [{
        type: 'TupleBinding',
        variables: ['$x'],
        domain: { type: 'DomainRef', domain: 'elements', selector: '.none' },
      }],
      body: {
        type: 'FormulaNode',
        kind: 'predicate',
        predicate: 'atLeast',
        args: [{ type: 'VariableRef', name: '$x' }],
        options: { value: 1, dimension: 'height' },
      },
    } as FormulaNode,
    world: emptyWorld,
    resolver: emptyResolver,
    options: { trace: false },
  })
  const existsEmpty = evaluateLogic({
    formula: {
      type: 'FormulaNode',
      kind: 'exists',
      bindings: [{
        type: 'TupleBinding',
        variables: ['$x'],
        domain: { type: 'DomainRef', domain: 'elements', selector: '.none' },
      }],
      body: {
        type: 'FormulaNode',
        kind: 'predicate',
        predicate: 'atLeast',
        args: [{ type: 'VariableRef', name: '$x' }],
        options: { value: 1, dimension: 'height' },
      },
    } as FormulaNode,
    world: emptyWorld,
    resolver: emptyResolver,
    options: { trace: false },
  })
  const quantifierEmptyDomainOk =
    forallEmpty.passed
    && existsEmpty.passed === false
    && existsEmpty.diagnostics.some((d) => d.code === 'IMH_LOGIC_EMPTY_DOMAIN_EXISTS')
  checks.push({
    id: 'quantifier-empty-domain-semantics',
    ok: quantifierEmptyDomainOk,
    details: `forallPassed=${forallEmpty.passed}, existsPassed=${existsEmpty.passed}`,
  })

  const insideWorld = buildGeometryWorld([
    { tagName: 'div', rect: { x: 47, y: 537, width: 231, height: 47 } },
    { tagName: 'div', rect: { x: 47, y: 482, width: 619, height: 518 } },
  ]) as unknown as GeometryWorld
  registerDefaultPredicates()
  const insideEvaluator = getPredicateEvaluator('inside')
  const insideEval = insideEvaluator?.evaluateTuple(insideWorld, [1, 2], {})
  const insideMetrics = ((insideEval?.metrics ?? {}) as Record<string, number>)
  const hasOverflowMetrics =
    typeof insideMetrics.overflowTop === 'number'
    || typeof insideMetrics.overflowBottom === 'number'
    || typeof insideMetrics.overflowLeft === 'number'
    || typeof insideMetrics.overflowRight === 'number'
  const insideMetricsOk =
    insideEval?.truth === 'true'
    && (
      !hasOverflowMetrics
      || (
        (insideMetrics.overflowTop ?? 0) === 0
        && (insideMetrics.overflowBottom ?? 0) === 0
        && (insideMetrics.overflowLeft ?? 0) === 0
        && (insideMetrics.overflowRight ?? 0) === 0
      )
    )
  checks.push({
    id: 'inside-overflow-orientation',
    ok: insideMetricsOk,
    details: hasOverflowMetrics
      ? `top=${insideMetrics.overflowTop ?? 'na'}, bottom=${insideMetrics.overflowBottom ?? 'na'}, left=${insideMetrics.overflowLeft ?? 'na'}, right=${insideMetrics.overflowRight ?? 'na'}`
      : 'overflow metrics unavailable in solver output',
  })

  const sizeWorld = buildGeometryWorld([
    { tagName: 'div', rect: { x: 0, y: 0, width: 527, height: 100 } },
  ]) as unknown as GeometryWorld
  ;(sizeWorld as any).env = {
    ...((sizeWorld as any).env || {}),
    viewportWidth: 1280,
    viewportHeight: 720,
  }
  ;(sizeWorld as any).styles = {
    subjectId: [1],
    fontSize: [16],
    chWidth: [9],
  }
  registerDefaultPredicates()
  const atMostEvaluator = getPredicateEvaluator('atMost')
  const vwResult = atMostEvaluator?.evaluateTuple(sizeWorld, [1], { dimension: 'width', max: { value: 85, unit: 'vw' } })
  const chResult = atMostEvaluator?.evaluateTuple(sizeWorld, [1], { dimension: 'width', max: { value: 60, unit: 'ch' } })
  const solverUnitsOk =
    vwResult?.truth === 'true'
    && (vwResult.metrics?.max ?? 0) > 1000
    && chResult?.truth === 'true'
    && Math.abs((chResult.metrics?.max ?? 0) - 540) < 0.0001
  checks.push({
    id: 'solver-size-unit-conversion',
    ok: !!solverUnitsOk,
    details: `vwTruth=${vwResult?.truth ?? 'na'}, vwMax=${vwResult?.metrics?.max ?? 'na'}, chTruth=${chResult?.truth ?? 'na'}, chMax=${chResult?.metrics?.max ?? 'na'}`,
  })

  return {
    ok: checks.every((c) => c.ok),
    generatedAt: new Date().toISOString(),
    checks,
    packageFingerprints,
  }
}

export function maybeEmitCompatibilityWarning(ui: ImhotepUi): void {
  if (compatibilityWarningEmitted) return
  const report = buildCompatibilityReport(ui)
  if (report.ok) return
  compatibilityWarningEmitted = true
  const failed = report.checks.filter((c) => !c.ok)
  const detail = failed.map((c) => `${c.id}: ${c.details}`).join(' | ')
  const fingerprints = report.packageFingerprints
    .map((p) => `${p.name}@${p.version} (${p.resolvedFrom})`)
    .join(' | ')
  // eslint-disable-next-line no-console
  console.warn(`[imhotep-playwright] compatibility warning: ${detail}; fingerprints=${fingerprints}`)
}

export function buildCompatibilityDiagnostic(report: CompatibilityReport): ImhotepDiagnostic | null {
  if (report.ok) return null
  const failed = report.checks.filter((c) => !c.ok)
  const detail = failed.map((c) => `${c.id}: ${c.details}`).join(' | ')
  const fingerprints = report.packageFingerprints
    .map((p) => `${p.name}@${p.version}`)
    .join(', ')
  return {
    code: 'IMH_INTERNAL_COMPAT_WARNING' as DiagnosticCode,
    severity: 'warning',
    category: 'internal-error',
    message: `Runtime compatibility checks reported issues: ${detail}`,
    source: 'imhotep-playwright',
    related: [],
    fixHints: [
      `Resolved packages: ${fingerprints}`,
      'Reinstall imhotep-playwright, imhotep-dsl, and imhotep-solver together from the same build.',
    ],
    metrics: {},
    sourceRef: { file: 'public.ts' },
    clauseLabel: 'compatibility',
  }
}

// ---------------------------------------------------------------------------
// FOL Result Adapter
// ---------------------------------------------------------------------------

export function adaptFOLResultToImhotepResult(
  folResult: ReturnType<typeof evaluateLogic>,
  assertionCount: number,
  clauseId?: string,
  traceMeta?: TraceMetadata,
): ImhotepResult {
  const formulaMetricsById = new Map<string, Record<string, number> | undefined>()
  for (const fr of folResult.formulaResults) {
    formulaMetricsById.set(fr.formulaId, fr.metrics)
  }

  const diagnostics: ImhotepDiagnostic[] = folResult.diagnostics.map((d) => {
    const metrics = d.clauseId ? formulaMetricsById.get(d.clauseId) : undefined
    const mapped = mapFolDiagnostic(d, metrics)
    if (traceMeta?.sourceRef) mapped.sourceRef = traceMeta.sourceRef
    if (traceMeta?.clauseLabel) mapped.clauseLabel = traceMeta.clauseLabel
    return mapped
  })

  const clauseResults: ClauseResult[] = folResult.formulaResults.map((fr, idx) => {
    const status: ClauseResult['status'] =
      fr.outcome === 'indeterminate' ? 'error' : fr.outcome

    const normalizedMetrics = (() => {
      const raw = (fr.metrics || {}) as Record<string, unknown>
      const hasInsideGeometry =
        typeof raw.subjectTop === 'number'
        && typeof raw.subjectBottom === 'number'
        && typeof raw.subjectLeft === 'number'
        && typeof raw.subjectRight === 'number'
        && typeof raw.refTop === 'number'
        && typeof raw.refBottom === 'number'
        && typeof raw.refLeft === 'number'
        && typeof raw.refRight === 'number'
      if (!hasInsideGeometry) {
        const hasOverflowOnly =
          typeof raw.overflowTop === 'number'
          || typeof raw.overflowBottom === 'number'
          || typeof raw.overflowLeft === 'number'
          || typeof raw.overflowRight === 'number'
        if (hasOverflowOnly && fr.outcome === 'pass') {
          return {
            ...raw,
            overflowTop: 0,
            overflowBottom: 0,
            overflowLeft: 0,
            overflowRight: 0,
          }
        }
        return raw
      }

      const subjectTop = raw.subjectTop as number
      const subjectBottom = raw.subjectBottom as number
      const subjectLeft = raw.subjectLeft as number
      const subjectRight = raw.subjectRight as number
      const refTop = raw.refTop as number
      const refBottom = raw.refBottom as number
      const refLeft = raw.refLeft as number
      const refRight = raw.refRight as number

      return {
        ...raw,
        overflowTop: Math.max(0, refTop - subjectTop),
        overflowBottom: Math.max(0, subjectBottom - refBottom),
        overflowLeft: Math.max(0, refLeft - subjectLeft),
        overflowRight: Math.max(0, subjectRight - refRight),
      }
    })()

    return {
      clauseId: clauseId ?? (fr.formulaId ?? `clause_${idx}`),
      status,
      truth: fr.truth,
      metrics: normalizedMetrics as any,
      witness: fr.witness
        ? { subjectId: fr.witness[0] ?? 0, frameId: 0 }
        : { subjectId: 0, frameId: 0 },
      diagnostics: [fr.outcome === 'fail' ? 'IMH_PREDICATE_FAILED' : ''].filter(Boolean),
      sourceRef: traceMeta?.sourceRef,
      clauseLabel: traceMeta?.clauseLabel,
    }
  })

  const passed = folResult.passed && clauseResults.every((r) => r.status === 'pass')

  return {
    schemaVersion: '1.0',
    passed,
    summary: `${assertionCount} assertion(s), ${diagnostics.length} diagnostic(s)`,
    clauseResults,
    diagnostics,
  }
}