/**
 * checkAll() implementation — the assertion evaluation pipeline.
 *
 * Extracted from public.ts to reduce the imhotep() factory function size.
 * Takes all state captured from the imhotep() closure as explicit parameters.
 */

import type { Page } from 'playwright'
import {
  FluentRelation,
  parseSpec,
  lowerToCanonical,
  extractFOLFormulas,
  compileDenseFOLToFormula,
  validateRelation,
} from 'imhotep-dsl'
import type { ImhotepPage } from './page.js'
import type { ImhotepUi } from './public-types.js'
import type { ImhotepResult, ClauseResult, ImhotepDiagnostic, DiagnosticCode } from 'imhotep-core'
import type { SourceReference } from 'imhotep-core'
import type { FormulaNode } from 'imhotep-core'
import {
  evaluateLogic,
  registerDefaultPredicates,
  type LogicEngineInput,
} from 'imhotep-solver'
import { compileAssertionsToFOL } from './fol-compiler.js'
import { attachFailureAnalysis } from 'imhotep-reporter'
import {
  assertionStore,
  specStore,
  extractWorld,
  SelectorDomainResolver,
  buildAncestorIndex,
  compileCanonicalClauseToFormula,
  getSelectorsFromAssertion,
  getSelectorsFromFormula,
  buildFluentLabel,
  buildDenseLabel,
  buildFOLLabel,
  buildNormalizedContracts,
  evaluateCardinalityAssertion,
  isDuckTypedFluentQuantifier,
  hasSubjectQuantifier,
  buildCompatibilityReport,
  maybeEmitCompatibilityWarning,
  buildCompatibilityDiagnostic,
  adaptFOLResultToImhotepResult,
  computeRequiredFacts,
  usesLayoutSpace,
} from './extraction.js'
import { formatAsLLM } from './llm-output.js'

// ---------------------------------------------------------------------------
// Internal type for the check-all compile phase
// ---------------------------------------------------------------------------

interface CheckItem {
  clauseId: string
  formula: FormulaNode
  selectors: string[]
  sourceRef: SourceReference
  clauseLabel: string
  state?: { selector: string; kind: string }
  allowEmptyDomains?: boolean
}

export interface CheckAllDeps {
  /** Getter for the UI handle (lazily resolved to avoid temporal dead zone). */
  getUi: () => ImhotepUi
  /** The raw Playwright page for extraction. */
  page: Page
  /** The wrapped ImhotepPage for state materialization. */
  wrapped: ImhotepPage
  /** Resolved cache directory (null to disable). */
  resolvedCacheDir: string | null
}

/**
 * Create the checkAll function bound to the given dependencies.
 */
export function makeCheckAll(deps: CheckAllDeps): ImhotepUi['checkAll'] {
  const { getUi, page, wrapped, resolvedCacheDir } = deps

  return (async (options?: { format?: 'default' | 'llm'; includeNormalized?: boolean }) => {
    const ui = getUi()
    const compatibilityReport = buildCompatibilityReport(ui)
    maybeEmitCompatibilityWarning(ui)
    const compatibilityDiagnostic = process.env.IMHOTEP_INCLUDE_COMPAT_DIAGNOSTICS === '1'
      ? buildCompatibilityDiagnostic(compatibilityReport)
      : null
    const format = options?.format ?? 'default'
    const assertions = assertionStore.get(ui) || []
    const specs = specStore.get(ui) || []
    assertionStore.set(ui, [])
    specStore.set(ui, [])

    // Build normalized contracts before we mutate the collections.
    const normalizedContracts = options?.includeNormalized
      ? buildNormalizedContracts(assertions, specs)
      : undefined

    if (assertions.length === 0 && specs.length === 0) {
      const emptyResult: ImhotepResult = {
        schemaVersion: '1.0',
        passed: true,
        summary: '0 assertions',
        clauseResults: [],
        diagnostics: compatibilityDiagnostic ? [compatibilityDiagnostic] : [],
        ...(normalizedContracts !== undefined ? { normalizedContracts } : {}),
      }
      return format === 'llm' ? formatAsLLM(emptyResult) : emptyResult
    }

    // Ensure predicates are registered before evaluation.
    registerDefaultPredicates()

    // Compile all check items into formulas first.
    const checks: CheckItem[] = []
    const cardinalityChecks: Array<{ clauseId: string; assertion: any }> = []
    const preflightDiagnostics: ImhotepDiagnostic[] = []
    const validationClauseResults: ClauseResult[] = []

    for (let i = 0; i < assertions.length; i++) {
      // eslint-disable-next-line @typescript-eslint/no-explicit-any
      const assertion = assertions[i] as any
      // Cardinality assertions are evaluated outside the FOL engine.
      if (assertion && ['exactlyOne', 'atLeastN', 'atMostN'].includes(assertion.kind)) {
        cardinalityChecks.push({ clauseId: `clause_${i}`, assertion })
        continue
      }
      // Validate fluent relation options before compilation.
      if (assertion instanceof FluentRelation) {
        const validation = validateRelation(assertion.toAst())
        if (!validation.valid) {
          for (const d of validation.diagnostics) {
            preflightDiagnostics.push({
              code: d.code as DiagnosticCode,
              severity: d.severity as 'error' | 'warning' | 'info',
              category: (d.category as ImhotepDiagnostic['category']) ?? 'validation-error',
              message: d.message,
              source: 'imhotep-dsl',
              related: [],
              fixHints: d.fixHints ?? [],
              metrics: d.metrics ?? {},
              sourceRef: { fluentIndex: i },
              clauseLabel: buildFluentLabel(assertions[i]),
            })
          }
          validationClauseResults.push({
            clauseId: `clause_${i}`,
            status: 'error' as const,
            truth: 'indeterminate' as const,
            metrics: {},
            witness: { subjectId: 0, frameId: 0 },
            diagnostics: validation.diagnostics.map((d) => d.code as string),
            sourceRef: { fluentIndex: i },
            clauseLabel: buildFluentLabel(assertions[i]),
          })
          continue
        }
      }
      const formula = compileAssertionsToFOL([assertions[i]])
      if (!formula) {
        preflightDiagnostics.push({
          code: 'IMH_INTERNAL_UNKNOWN_CLAUSE_KIND',
          severity: 'error',
          category: 'internal-error',
          message: 'Assertion compilation produced no FOL formula.',
          source: 'imhotep-playwright',
          related: [],
          fixHints: [
            'Check that the assertion uses a supported relation or predicate.',
            'Supported relations: leftOf, rightOf, above, below, alignedWith, centeredWithin, inside, contains, overlaps.',
          ],
          metrics: {},
          sourceRef: { file: 'public.ts' },
          clauseLabel: buildFluentLabel(assertions[i]),
        })
        continue
      }
      checks.push({
        clauseId: `clause_${i}`,
        formula,
        selectors: getSelectorsFromAssertion(assertions[i]),
        sourceRef: { fluentIndex: i },
        clauseLabel: buildFluentLabel(assertions[i]),
        allowEmptyDomains:
          isDuckTypedFluentQuantifier(assertion) || hasSubjectQuantifier(assertion),
        state: (() => {
          const state = assertion?.assertion?.getState?.()
          const subject = assertion?.assertion?.getSubject?.()
          if (state?.kind && subject) {
            return { selector: subject, kind: state.kind }
          }
          return undefined
        })(),
      })
    }

    let specBase = assertions.length
    for (const source of specs) {
      const parsed = parseSpec(source)
      if (parsed.diagnostics.some((d) => d.severity === 'error')) {
        for (const d of parsed.diagnostics) {
          const hints: string[] = [
            'Selectors must be single-quoted strings, e.g. \'[data-testid="x"]\'.',
            'Use relation keywords directly without "is": e.g. \'a\' leftOf \'b\'.',
            'Gap values require units: e.g. gap 8px.',
          ]
          const sourceRef: SourceReference = d.position?.start
            ? { specLine: d.position.start.line, specColumn: d.position.start.column }
            : {}
          preflightDiagnostics.push({
            code: (d.code as DiagnosticCode) || 'IMH_PARSE_INVALID_SYNTAX',
            severity: 'error',
            category: 'parse-error',
            message: d.message,
            source: 'imhotep-dsl',
            related: [],
            fixHints: hints,
            metrics: {},
            sourceRef,
            clauseLabel: 'parse error',
          })
          validationClauseResults.push({
            clauseId: `clause_${specBase++}`,
            status: 'error',
            truth: 'indeterminate',
            metrics: {},
            witness: { subjectId: 0, frameId: 0 },
            diagnostics: [(d.code as string) || 'IMH_PARSE_INVALID_SYNTAX'],
            sourceRef,
            clauseLabel: 'parse error',
          })
        }
        continue
      }

      // FOL formula path: dense DSL forall/exists bypass canonical lowering
      const folFormulas = extractFOLFormulas(parsed.ast)
      for (const folAst of folFormulas) {
        const solverFormula = compileDenseFOLToFormula(folAst)
        const selectors = getSelectorsFromFormula(solverFormula)
        const sourceRef: SourceReference = folAst.position?.start
          ? { specLine: folAst.position.start.line, specColumn: folAst.position.start.column }
          : {}
        checks.push({
          clauseId: `clause_${specBase++}`,
          formula: solverFormula,
          selectors,
          sourceRef,
          clauseLabel: buildFOLLabel(folAst),
          allowEmptyDomains: true,
        })
      }

      const canonicalClauses = lowerToCanonical(parsed.ast)

      // Group compound assertions so 'and'/'or' clauses are evaluated as one FOL formula
      const clauseGroups: Array<{
        clauses: typeof canonicalClauses
        operator?: 'and' | 'or'
      }> = []
      let currentGroup: (typeof clauseGroups)[0] | null = null

      for (const clause of canonicalClauses) {
        if (clause.compoundGroupId !== undefined && clause.compoundOperator) {
          if (!currentGroup || currentGroup.operator !== clause.compoundOperator) {
            currentGroup = { clauses: [], operator: clause.compoundOperator }
            clauseGroups.push(currentGroup)
          }
          currentGroup.clauses.push(clause)
        } else {
          clauseGroups.push({ clauses: [clause] })
          currentGroup = null
        }
      }

      for (const group of clauseGroups) {
        if (group.operator && group.clauses.length > 1) {
          const formulas = group.clauses.map((c) => compileCanonicalClauseToFormula(c))
          let combinedFormula: FormulaNode = formulas[0]
          for (let i = 1; i < formulas.length; i++) {
            combinedFormula = {
              type: 'FormulaNode',
              kind: group.operator,
              left: combinedFormula,
              right: formulas[i],
            } as FormulaNode
          }

          const selectors = Array.from(
            new Set(
              group.clauses.flatMap((c) =>
                [c.subject, c.reference].filter((s): s is string => typeof s === 'string' && s.length > 0),
              ),
            ),
          )
          const firstClause = group.clauses[0]
          const sourceRef: SourceReference = firstClause.position?.start
            ? { specLine: firstClause.position.start.line, specColumn: firstClause.position.start.column }
            : {}

          checks.push({
            clauseId: `clause_${specBase++}`,
            formula: combinedFormula,
            selectors,
            sourceRef,
            clauseLabel: group.clauses.map(buildDenseLabel).join(` ${group.operator} `),
            allowEmptyDomains: false,
            state: (() => {
              const firstState = group.clauses[0]?.state
              const firstSubject = group.clauses[0]?.subject
              if (!firstState?.kind || !firstSubject) return undefined
              const uniform = group.clauses.every((c) => c.state?.kind === firstState.kind && c.subject === firstSubject)
              return uniform ? { selector: firstSubject, kind: firstState.kind } : undefined
            })(),
          })
        } else {
          for (const clause of group.clauses) {
            const formula = compileCanonicalClauseToFormula(clause)
            const sourceRef: SourceReference = clause.position?.start
              ? { specLine: clause.position.start.line, specColumn: clause.position.start.column }
              : {}
            checks.push({
              clauseId: `clause_${specBase++}`,
              formula,
              selectors: [clause.subject, clause.reference].filter((s): s is string => typeof s === 'string' && s.length > 0),
              sourceRef,
              clauseLabel: buildDenseLabel(clause),
              allowEmptyDomains: false,
              state: clause.state?.kind ? { selector: clause.subject, kind: clause.state.kind } : undefined,
            })
          }
        }
      }

      // Guard: non-empty spec with no diagnostics and no clauses = parser/version mismatch
      const parsedAnyClauses = folFormulas.length > 0 || canonicalClauses.length > 0
      if (!parsedAnyClauses && source.trim().length > 0) {
        const sourceRef: SourceReference = { specLine: 1, specColumn: 1 }
        preflightDiagnostics.push({
          code: 'IMH_PARSE_ERROR',
          severity: 'error',
          category: 'parse-error',
          message: 'Spec produced no clauses. This may indicate parser/version mismatch in imhotep-dsl.',
          source: 'imhotep-playwright',
          related: [],
          fixHints: [
            'Ensure imhotep-playwright and imhotep-dsl are installed from the same source build.',
            'If using local packages, reinstall both packages together.',
          ],
          metrics: {},
          sourceRef,
          clauseLabel: 'parse error',
        })
        validationClauseResults.push({
          clauseId: `clause_${specBase++}`,
          status: 'error',
          truth: 'indeterminate',
          metrics: {},
          witness: { subjectId: 0, frameId: 0 },
          diagnostics: ['IMH_PARSE_ERROR'],
          sourceRef,
          clauseLabel: 'parse error',
        })
      }
    }

    // Collect selectors from both spatial and cardinality assertions.
    const cardinalitySelectors = cardinalityChecks.map((c) => c.assertion.selector as string)
    const statelessChecks = checks.filter((c) => !c.state)
    const statefulChecks = checks.filter((c) => !!c.state)
    const allSelectors = Array.from(new Set([...statelessChecks.flatMap((c) => c.selectors), ...cardinalitySelectors]))

    // 1. Extract world and collect selector domains.
    const requiredFacts = computeRequiredFacts(statelessChecks.map((c) => c.formula))
    const allowFastGeometry = !statelessChecks.some((c) => usesLayoutSpace(c.formula))
    let world: import('imhotep-solver').GeometryWorld | null = null
    let selectorToIds = new Map<string, number[]>()
    let errors: ImhotepDiagnostic[] = []
    try {
      if (allSelectors.length > 0 || cardinalityChecks.length > 0) {
        const extracted = await extractWorld(page, allSelectors, resolvedCacheDir, requiredFacts, allowFastGeometry)
        world = extracted.world
        selectorToIds = extracted.selectorToIds
        errors = extracted.errors
      }
    } catch (err) {
      const message = err instanceof Error ? err.message : String(err)
      const firstCheck = checks[0]
      const extractDiagnostic: ImhotepDiagnostic = {
        code: 'IMH_EXTRACT_PROTOCOL_ERROR',
        severity: 'error',
        category: 'extraction-error',
        message,
        source: 'imhotep-playwright',
        related: [],
        fixHints: [
          'Verify the page is fully loaded before running assertions.',
          'Check that selectors are valid CSS selectors or semantic references.',
          'Use ui.extract(selector) to debug selector resolution.',
        ],
        metrics: {},
        sourceRef: firstCheck?.sourceRef,
        clauseLabel: firstCheck?.clauseLabel ?? 'extraction',
      }
      const emptySelectorToIds = new Map<string, number[]>()
      const cardClauseResults: ClauseResult[] = []
      const cardDiagnostics: ImhotepDiagnostic[] = []
      for (const cardCheck of cardinalityChecks) {
        const cardResult = evaluateCardinalityAssertion(
          cardCheck.assertion,
          cardCheck.clauseId,
          emptySelectorToIds,
        )
        cardClauseResults.push({
          clauseId: cardResult.clauseId,
          status: cardResult.status,
          truth: cardResult.truth,
          metrics: {
            observedCount: 0,
            expectedCount: cardResult.expectedCount,
          },
          witness: { subjectId: 0, frameId: 0 },
          diagnostics: cardResult.diagnostics.map((d) => d.code),
          sourceRef: { selector: cardResult.selector },
          clauseLabel: cardResult.label,
        })
        cardDiagnostics.push(...cardResult.diagnostics)
      }
      const extractDiagnostics = [
        ...(compatibilityDiagnostic ? [compatibilityDiagnostic] : []),
        extractDiagnostic,
        ...preflightDiagnostics,
        ...cardDiagnostics,
      ].map((d) =>
        attachFailureAnalysis(d),
      )
      const extractResult: ImhotepResult = {
        schemaVersion: '1.0',
        passed: false,
        summary: `${checks.length + cardinalityChecks.length} assertion(s), ${extractDiagnostics.length} diagnostic(s)`,
        clauseResults: [
          ...validationClauseResults,
          ...cardClauseResults,
          ...checks.map((c) => ({
            clauseId: c.clauseId,
            status: 'error' as const,
            truth: 'indeterminate' as const,
            metrics: {},
            witness: { subjectId: 0, frameId: 0 },
            diagnostics: ['IMH_EXTRACT_PROTOCOL_ERROR'],
            sourceRef: c.sourceRef,
            clauseLabel: c.clauseLabel,
          })),
        ],
        diagnostics: extractDiagnostics,
        ...(normalizedContracts !== undefined ? { normalizedContracts } : {}),
      }
      return format === 'llm' ? formatAsLLM(extractResult) : extractResult
    }

    // 2. Evaluate cardinality assertions using extracted selector counts.
    const allClauseResults: ClauseResult[] = [...validationClauseResults]
    const allDiagnostics: ImhotepDiagnostic[] = [
      ...(compatibilityDiagnostic ? [compatibilityDiagnostic] : []),
      ...preflightDiagnostics,
    ]

    for (const cardCheck of cardinalityChecks) {
      const cardResult = evaluateCardinalityAssertion(
        cardCheck.assertion,
        cardCheck.clauseId,
        selectorToIds,
      )
      allClauseResults.push({
        clauseId: cardResult.clauseId,
        status: cardResult.status,
        truth: cardResult.truth,
        metrics: {
          observedCount: selectorToIds.get(cardResult.selector)?.length ?? 0,
          expectedCount: cardResult.expectedCount,
        },
        witness: { subjectId: 0, frameId: 0 },
        diagnostics: cardResult.diagnostics.map((d) => d.code),
        sourceRef: { selector: cardResult.selector },
        clauseLabel: cardResult.label,
      })
      allDiagnostics.push(...cardResult.diagnostics)
    }

    // Build a set of selectors that failed to resolve (zero matches).
    const failedSelectors = new Set<string>()
    const selectorErrorsBySelector = new Map<string, ImhotepDiagnostic[]>()
    const emittedSelectorErrorKeys = new Set<string>()
    for (const err of errors) {
      const sel = (err.sourceRef as { selector?: string })?.selector
      if (typeof sel === 'string') {
        failedSelectors.add(sel)
        const list = selectorErrorsBySelector.get(sel) ?? []
        list.push(err)
        selectorErrorsBySelector.set(sel, list)
      }
    }

    // Partition stateless checks: those referencing a failed selector vs. clean.
    const failedChecks: CheckItem[] = []
    const validChecks: CheckItem[] = []
    for (const check of statelessChecks) {
      const hasMissingSelector = check.selectors.some((s) => failedSelectors.has(s))
      if (hasMissingSelector && !check.allowEmptyDomains) {
        failedChecks.push(check)
      } else {
        validChecks.push(check)
      }
    }

    for (const check of failedChecks) {
      allClauseResults.push({
        clauseId: check.clauseId,
        status: 'error' as const,
        truth: 'indeterminate' as const,
        metrics: {},
        witness: { subjectId: 0, frameId: 0 },
        diagnostics: ['IMH_SELECTOR_ZERO_MATCHES'],
        sourceRef: check.sourceRef,
        clauseLabel: check.clauseLabel,
      })
      for (const selector of check.selectors) {
        const selectorErrors = selectorErrorsBySelector.get(selector)
        if (selectorErrors) {
          for (const d of selectorErrors) {
            const key = `${selector}:${d.code}:${d.message}`
            if (!emittedSelectorErrorKeys.has(key)) {
              emittedSelectorErrorKeys.add(key)
              allDiagnostics.push(d)
            }
          }
        }
      }
    }

    // 3. Build domain resolver and evaluate clean stateless assertions through FOL.
    if (validChecks.length > 0 && world) {
      const resolver = new SelectorDomainResolver()
      for (const [selector, ids] of selectorToIds) {
        resolver.register(selector, ids)
      }
      for (const selector of failedSelectors) {
        if (!selectorToIds.has(selector)) {
          resolver.register(selector, [])
        }
      }
      const ancestorIndex = buildAncestorIndex(world)
      if (ancestorIndex.size > 0) {
        resolver.setAncestorIndex(ancestorIndex)
      }

      for (let i = 0; i < validChecks.length; i++) {
        const check = validChecks[i]
        const input: LogicEngineInput = {
          formula: check.formula,
          world,
          resolver,
          options: { trace: false },
        }
        const folResult = evaluateLogic(input)
        const adapted = adaptFOLResultToImhotepResult(folResult, 1, check.clauseId, {
          sourceRef: check.sourceRef,
          clauseLabel: check.clauseLabel,
        })
        allClauseResults.push(...adapted.clauseResults)
        const checkFailed = adapted.clauseResults.some((r) => r.status !== 'pass')
        if (checkFailed) {
          allDiagnostics.push(...adapted.diagnostics)
        }
      }
    }

    // 4. Evaluate stateful assertions one-by-one with explicit state materialization.
    for (const check of statefulChecks) {
      const stateInfo = check.state
      if (!stateInfo) continue

      try {
        await wrapped.materializeState(stateInfo.selector, stateInfo.kind as import('./page.js').StateSnapshot)
      } catch (err) {
        allClauseResults.push({
          clauseId: check.clauseId,
          status: 'error' as const,
          truth: 'indeterminate' as const,
          metrics: {},
          witness: { subjectId: 0, frameId: 0 },
          diagnostics: ['IMH_EXTRACT_PROTOCOL_ERROR'],
          sourceRef: check.sourceRef,
          clauseLabel: check.clauseLabel,
        })
        allDiagnostics.push({
          code: 'IMH_EXTRACT_PROTOCOL_ERROR',
          severity: 'error',
          category: 'extraction-error',
          message: err instanceof Error ? err.message : String(err),
          source: 'imhotep-playwright',
          related: [],
          fixHints: [
            `Verify selector "${stateInfo.selector}" exists before applying state "${stateInfo.kind}".`,
            'Use ui.materializeState(selector, state) directly to debug state setup.',
          ],
          metrics: {},
          sourceRef: check.sourceRef,
          clauseLabel: check.clauseLabel,
        })
        continue
      }

      const perCheckFacts = computeRequiredFacts([check.formula])
      const perCheckFast = !usesLayoutSpace(check.formula)
      const extracted = await extractWorld(page, check.selectors, resolvedCacheDir, perCheckFacts, perCheckFast)

      const perCheckFailedSelectors = new Set<string>()
      for (const err of extracted.errors) {
        const sel = (err.sourceRef as { selector?: string })?.selector
        if (typeof sel === 'string') {
          perCheckFailedSelectors.add(sel)
        }
      }

      const hasMissingSelector = check.selectors.some((s) => perCheckFailedSelectors.has(s))
      if (hasMissingSelector) {
        allClauseResults.push({
          clauseId: check.clauseId,
          status: 'error' as const,
          truth: 'indeterminate' as const,
          metrics: {},
          witness: { subjectId: 0, frameId: 0 },
          diagnostics: ['IMH_SELECTOR_ZERO_MATCHES'],
          sourceRef: check.sourceRef,
          clauseLabel: check.clauseLabel,
        })
        allDiagnostics.push(...extracted.errors)
        continue
      }

      const resolver = new SelectorDomainResolver()
      for (const [selector, ids] of extracted.selectorToIds) {
        resolver.register(selector, ids)
      }
      const stateAncestorIndex = buildAncestorIndex(extracted.world)
      if (stateAncestorIndex.size > 0) {
        resolver.setAncestorIndex(stateAncestorIndex)
      }

      const folResult = evaluateLogic({
        formula: check.formula,
        world: extracted.world,
        resolver,
        options: { trace: false },
      })
      const adapted = adaptFOLResultToImhotepResult(folResult, 1, check.clauseId, {
        sourceRef: check.sourceRef,
        clauseLabel: check.clauseLabel,
      })
      allClauseResults.push(...adapted.clauseResults)
      const checkFailed = adapted.clauseResults.some((r) => r.status !== 'pass')
      if (checkFailed) {
        allDiagnostics.push(...adapted.diagnostics)
      }
    }

    const hasPreflightErrors = preflightDiagnostics.some((d) => d.severity === 'error')
    const passed = allClauseResults.every((r) => r.status === 'pass') && !allDiagnostics.some((d) => d.severity === 'error') && !hasPreflightErrors
    const totalAssertions = checks.length + cardinalityChecks.length

    const analyzedDiagnostics = allDiagnostics.map((d) =>
      attachFailureAnalysis(d),
    )

    const result: ImhotepResult = {
      schemaVersion: '1.0',
      passed,
      summary: `${totalAssertions} assertion(s), ${analyzedDiagnostics.length} diagnostic(s)`,
      clauseResults: allClauseResults,
      diagnostics: analyzedDiagnostics,
      ...(normalizedContracts !== undefined ? { normalizedContracts } : {}),
    }
    return format === 'llm' ? formatAsLLM(result) : result
  }) as ImhotepUi['checkAll']
}