// SQLOptimizer.speckdl — A cost-based SQL query optimizer
// Models the full optimization pipeline: parse → rewrite → plan → execute
// Exercises: state-dependent transforms, cost models, map-based catalog,
// collection guards, conditional emits, and rollback semantics.

speck SQLOptimizer {
  version: "0.1.0"
  author:  "sscoble"
  license: "MIT"

  // ─── State ────────────────────────────────────────────────
  state: {
    phase:          OptimizerPhase,
    queryText:      String,
    logicalPlan:    PlanNode,
    physicalPlan:   PlanNode,
    estimatedCost:  CostModel,
    catalog:        SchemaCatalog,
    stats:          TableStats,
    rewriteRules:   RuleSet,
    planCache:      PlanCache
  }

  init: {
    phase := Idle,
    queryText := "",
    logicalPlan := {},
    physicalPlan := {},
    estimatedCost := {},
    catalog := {},
    stats := {},
    rewriteRules := {},
    planCache := {}
  }

  // ─── Events ───────────────────────────────────────────────
  event OptimizationStarted {
    query: String,
    at: String
  }

  event PlanRewritten {
    rule: String,
    before: String,
    after: String,
    costBefore: Nat,
    costAfter: Nat,
    at: String
  }

  event PlanGenerated {
    planType: PlanType,
    estimatedRows: Nat,
    estimatedCost: Nat,
    at: String
  }

  event OptimizationCompleted {
    totalRulesApplied: Nat,
    finalCost: Nat,
    at: String
  }

  event OptimizationFailed {
    phase: OptimizerPhase,
    message: String,
    at: String
  }

  // ─── Actions ──────────────────────────────────────────────
  action optimize(query: String) {
    require phase === Idle
    require len(query) > 0

    this.phase := Parsing
    this.queryText := query
    this.logicalPlan := {}

    emit OptimizationStarted { query: query, at: now() }
  }

  action parse() {
    require phase === Parsing
    require len(queryText) > 0

    // Lexical + syntactic analysis → raw AST
    // Semantic validation: table/column existence, type checking
    this.logicalPlan := parseSQL(queryText)

    // Fail fast on syntax errors
    if logicalPlan == {} {
      this.phase := Failed
      emit OptimizationFailed { phase: Parsing, message: "Syntax error in query", at: now() }
      return
    }

    this.phase := Rewriting
    emit PlanRewritten { rule: "parse", before: queryText, after: stringOf(logicalPlan), costBefore: 0, costAfter: estimatedCostOf(logicalPlan), at: now() }
  }

  action rewrite() {
    require phase === Rewriting

    // Apply logical rewrites: predicate pushdown, column pruning,
    // subquery flattening, join reordering (logical), constant folding
    let rulesApplied := 0
    let plan := logicalPlan
    let prevCost := estimatedCostOf(plan)

    // Predicate pushdown: move filters closer to scans
    let pushed := pushDownPredicates(plan, catalog)
    if estimatedCostOf(pushed) < prevCost {
      plan := pushed
      prevCost := estimatedCostOf(pushed)
      rulesApplied := rulesApplied + 1
      emit PlanRewritten { rule: "predicate_pushdown", before: stringOf(logicalPlan), after: stringOf(pushed), costBefore: prevCost, costAfter: estimatedCostOf(pushed), at: now() }
    }

    // Column pruning: remove unused projections
    let pruned := pruneColumns(plan, catalog)
    if estimatedCostOf(pruned) < prevCost {
      plan := pruned
      prevCost := estimatedCostOf(pruned)
      rulesApplied := rulesApplied + 1
      emit PlanRewritten { rule: "column_pruning", before: stringOf(logicalPlan), after: stringOf(pruned), costBefore: prevCost, costAfter: estimatedCostOf(pruned), at: now() }
    }

    // Subquery flattening: convert subqueries to joins where possible
    let flattened := flattenSubqueries(plan, catalog)
    if estimatedCostOf(flattened) < prevCost {
      plan := flattened
      prevCost := estimatedCostOf(flattened)
      rulesApplied := rulesApplied + 1
      emit PlanRewritten { rule: "subquery_flatten", before: stringOf(logicalPlan), after: stringOf(flattened), costBefore: prevCost, costAfter: estimatedCostOf(flattened), at: now() }
    }

    // Constant folding: evaluate compile-time expressions
    let folded := foldConstants(plan)
    if estimatedCostOf(folded) < prevCost {
      plan := folded
      rulesApplied := rulesApplied + 1
      emit PlanRewritten { rule: "constant_folding", before: stringOf(logicalPlan), after: stringOf(folded), costBefore: prevCost, costAfter: estimatedCostOf(folded), at: now() }
    }

    this.logicalPlan := plan
    this.phase := Planning
  }

  action plan() {
    require phase === Planning

    // Cost-based join enumeration: consider join orderings
    // Choose physical operators: hash join vs merge join vs nested loop
    // Use catalog stats (row counts, cardinality, histograms) for cost estimation

    let bestPlan := choosePhysicalPlan(logicalPlan, catalog, stats)
    let cost := estimatedCostOf(bestPlan)

    this.physicalPlan := bestPlan
    this.estimatedCost := cost

    // Check plan cache for identical query shape
    let cached := lookupPlan(planCache, logicalPlan)
    if cached != {} and estimatedCostOf(cached) < cost {
      this.physicalPlan := cached
      this.estimatedCost := estimatedCostOf(cached)
    }

    emit PlanGenerated {
      planType: Physical,
      estimatedRows: estimatedRowsOf(physicalPlan),
      estimatedCost: cost.estimatedCost,
      at: now()
    }

    this.phase := Ready
  }

  action execute() {
    require phase === Ready

    // Execute the physical plan against the storage engine
    // Stream results, track actual vs estimated cardinalities
    this.phase := Executing
  }

  action complete() {
    require phase === Executing

    // Collect execution statistics
    // Update plan cache if actual cost diverges significantly from estimate
    let rulesApplied := countRewrites(planCache)

    this.phase := Done
    emit OptimizationCompleted { totalRulesApplied: rulesApplied, finalCost: estimatedCost.estimatedCost, at: now() }
  }

  action fail(message: String) {
    // Any phase can transition to Failed
    this.phase := Failed
    emit OptimizationFailed { phase: phase, message: message, at: now() }
  }

  action reset() {
    this.phase := Idle
    this.queryText := ""
    this.logicalPlan := {}
    this.physicalPlan := {}
    this.estimatedCost := {}
    this.catalog := {}
    this.stats := {}
    this.rewriteRules := defaultRules()
    this.planCache := {}
  }

  // ─── Constraints ──────────────────────────────────────────
  constraint C1: phase === Idle || len(queryText) > 0
  // Non-idle phases require a query

  constraint C2: estimatedCost > 0 implies phase >= Planning
  // A cost estimate implies planning has occurred

  constraint C3: phase === Ready implies physicalPlan != {}
  // Ready phase requires a physical plan

  constraint C4: phase === Done implies estimatedCost > 0
  // Completion requires a cost estimate

  constraint C5: phase === Failed implies len(queryText) > 0
  // Failure requires a query was submitted

  // ─── Temporal Verifications ───────────────────────────────
  verify V1: always(implies(phase === Parsing, eventually(phase === Rewriting || phase === Failed)))
  // Parsing must complete or fail

  verify V2: always(implies(phase === Rewriting, eventually(phase === Planning || phase === Failed)))
  // Rewriting must reach planning or fail

  verify V3: always(implies(phase === Planning, eventually(phase === Ready || phase === Failed)))
  // Planning must produce a plan or fail

  verify V4: always(implies(phase === Ready, eventually(phase === Done || phase === Failed)))
  // A ready plan must execute or fail

  // ─── Provenance ───────────────────────────────────────────
  provenance {
    wasGeneratedBy(sql-optimizer, SQLOptimizer, "2026-05-13T00:00:00Z")
    used(SQLOptimizer, cascades-volcano, "framework")
    used(SQLOptimizer, postgres-planner, "reference")
    used(SQLOptimizer, z3, "verification")
  }

  // ─── BOM ──────────────────────────────────────────────────
  bom {
    optimizer: "sql-optimizer@0.1.0"
    runtime:   "node@22.0.0"
    solver:    "z3@4.13.0"
  }

  // ─── Supporting Types ─────────────────────────────────────
  interface OptimizerPhase {
    Idle, Parsing, Rewriting, Planning, Ready, Executing, Done, Failed
  }

  interface PlanType {
    Logical, Physical, Cached
  }

  interface PlanNode {
    // Opaque — represents a query plan tree (scan, join, filter, project, aggregate, sort)
  }

  interface CostModel {
    // Captures: estimated IO, CPU, memory, network cost
    // Plus cardinality estimates per operator
  }

  interface SchemaCatalog {
    // Table definitions, column types, indexes, constraints
  }

  interface TableStats {
    // Row counts, column histograms, NDV, null fractions
  }

  interface RuleSet {
    // Ordered list of rewrite rules with enable/disable flags
  }

  interface PlanCache {
    // Maps query fingerprints to cached physical plans
  }
}