// SQLOptimizer.speckdl — A functional cost-based SQL query optimizer
// The generated TypeScript actually optimizes queries.
// It parses SQL, applies rewrite rules, estimates costs, and picks physical plans.

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

  // ─── State ────────────────────────────────────────────────
  state: {
    phase:          OptimizerPhase,
    originalSQL:    String,
    planNodes:      PlanNodeMap,
    planEdges:      PlanEdgeMap,
    rootPlanId:     String,
    catalog:        CatalogMap,
    stats:          StatsMap,
    rulesApplied:   Nat,
    bestCost:       Nat,
    resultSQL:      String,
    errors:         StringList
  }

  init: {
    phase := Idle,
    originalSQL := "",
    planNodes := {},
    planEdges := {},
    rootPlanId := "",
    catalog := {},
    stats := {},
    rulesApplied := 0,
    bestCost := 0,
    resultSQL := "",
    errors := []
  }

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

  event RuleApplied {
    ruleName: String,
    planBefore: String,
    planAfter: String,
    costDelta: Nat,
    at: String
  }

  event PlanOptimized {
    originalSQL: String,
    optimizedSQL: String,
    originalCost: Nat,
    optimizedCost: Nat,
    rulesApplied: Nat,
    at: String
  }

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

  // ─── Actions ──────────────────────────────────────────────

  // Accept a SQL query string and begin optimization
  action submit(sql: String) {
    require phase === Idle
    require len(sql) > 0

    this.phase := Parsing
    this.originalSQL := sql
    this.errors := []

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

  // Parse SQL into a logical plan tree
  // Builds PlanNode objects representing Scan, Filter, Join, Project, Aggregate, Sort
  action parse() {
    require phase === Parsing
    require len(originalSQL) > 0

    // Parse SELECT ... FROM ... WHERE ... GROUP BY ... ORDER BY ...
    let sql := originalSQL

    // Extract FROM clause — identify table names
    let fromClause := extractFrom(sql)
    if len(fromClause) == 0 {
      this.phase := Failed
      this.errors := ["No FROM clause found"]
      emit OptimizationFailed { phase: Parsing, message: "No FROM clause found", at: now() }
      return
    }

    // Extract WHERE clause — identify predicates
    let whereClause := extractWhere(sql)
    let groupByClause := extractGroupBy(sql)
    let orderByClause := extractOrderBy(sql)
    let selectClause := extractSelect(sql)

    // Build initial plan: Scan → Filter → Join → Project
    let scanId := "scan_0"
    this.planNodes := {}
    this.planNodes := setPlanNode(planNodes, scanId, { op: "Scan", table: fromClause, estimatedRows: lookupRowCount(stats, fromClause), children: [], filter: "" })

    let currentRoot := scanId

    // Add filter if WHERE exists
    if len(whereClause) > 0 {
      let filterId := "filter_0"
      let filterRows := estimateFilterSelectivity(stats, fromClause, whereClause, lookupRowCount(stats, fromClause))
      this.planNodes := setPlanNode(planNodes, filterId, { op: "Filter", predicate: whereClause, estimatedRows: filterRows, children: [currentRoot] })
      currentRoot := filterId
    }

    // Add GROUP BY if present
    if len(groupByClause) > 0 {
      let aggId := "aggregate_0"
      this.planNodes := setPlanNode(planNodes, aggId, { op: "Aggregate", groupBy: groupByClause, estimatedRows: 1, children: [currentRoot] })
      currentRoot := aggId
    }

    // Add ORDER BY if present
    if len(orderByClause) > 0 {
      let sortId := "sort_0"
      this.planNodes := setPlanNode(planNodes, sortId, { op: "Sort", orderBy: orderByClause, estimatedRows: 1, children: [currentRoot] })
      currentRoot := sortId
    }

    // Add projection
    let projectId := "project_0"
    this.planNodes := setPlanNode(planNodes, projectId, { op: "Project", columns: selectClause, estimatedRows: 1, children: [currentRoot] })
    currentRoot := projectId

    this.rootPlanId := currentRoot
    this.bestCost := estimateCost(planNodes, rootPlanId)
    this.phase := Rewriting
  }

  // Apply logical rewrite rules
  action rewrite() {
    require phase === Rewriting

    let costBefore := bestCost
    let rulesThisRound := 0

    // Rule 1: Predicate pushdown — move filters closer to scans
    let pushed := pushDownFilters(planNodes, rootPlanId)
    let pushedCost := estimateCost(pushed.nodes, pushed.root)
    if pushedCost < bestCost {
      this.planNodes := pushed.nodes
      this.rootPlanId := pushed.root
      this.bestCost := pushedCost
      this.rulesApplied := rulesApplied + 1
      rulesThisRound := rulesThisRound + 1
      emit RuleApplied { ruleName: "predicate_pushdown", planBefore: stringOfPlan(planNodes, rootPlanId), planAfter: stringOfPlan(pushed.nodes, pushed.root), costDelta: costBefore - pushedCost, at: now() }
      costBefore := pushedCost
    }

    // Rule 2: Column pruning — remove unused columns from projections
    let pruned := pruneUnusedColumns(planNodes, rootPlanId)
    let prunedCost := estimateCost(pruned.nodes, pruned.root)
    if prunedCost < bestCost {
      this.planNodes := pruned.nodes
      this.rootPlanId := pruned.root
      this.bestCost := prunedCost
      this.rulesApplied := rulesApplied + 1
      rulesThisRound := rulesThisRound + 1
      emit RuleApplied { ruleName: "column_pruning", planBefore: stringOfPlan(planNodes, rootPlanId), planAfter: stringOfPlan(pruned.nodes, pruned.root), costDelta: costBefore - prunedCost, at: now() }
      costBefore := prunedCost
    }

    // Rule 3: Constant folding — evaluate compile-time expressions
    let folded := foldConstants(planNodes, rootPlanId)
    let foldedCost := estimateCost(folded.nodes, folded.root)
    if foldedCost < bestCost {
      this.planNodes := folded.nodes
      this.rootPlanId := folded.root
      this.bestCost := foldedCost
      this.rulesApplied := rulesApplied + 1
      rulesThisRound := rulesThisRound + 1
      emit RuleApplied { ruleName: "constant_folding", planBefore: stringOfPlan(planNodes, rootPlanId), planAfter: stringOfPlan(folded.nodes, folded.root), costDelta: costBefore - foldedCost, at: now() }
    }

    this.phase := Planning
  }

  // Choose physical operators and join order
  action planPhysical() {
    require phase === Planning

    // Choose join algorithm based on table sizes
    let physical := choosePhysicalOperators(planNodes, rootPlanId, stats)
    let physicalCost := estimateCost(physical.nodes, physical.root)

    if physicalCost < bestCost {
      this.planNodes := physical.nodes
      this.rootPlanId := physical.root
      this.bestCost := physicalCost
    }

    this.phase := Generating
  }

  // Generate optimized SQL from the physical plan
  action generate() {
    require phase === Generating

    let optimized := generateSQL(planNodes, rootPlanId)

    this.resultSQL := optimized
    this.phase := Done

    emit PlanOptimized {
      originalSQL: originalSQL,
      optimizedSQL: optimized,
      originalCost: estimateCost(planNodes, rootPlanId),
      optimizedCost: bestCost,
      rulesApplied: rulesApplied,
      at: now()
    }
  }

  // Reset for next query
  action reset() {
    this.phase := Idle
    this.originalSQL := ""
    this.planNodes := {}
    this.planEdges := {}
    this.rootPlanId := ""
    this.catalog := {}
    this.stats := {}
    this.rulesApplied := 0
    this.bestCost := 0
    this.resultSQL := ""
    this.errors := []
  }

  // ─── Constraints ──────────────────────────────────────────
  constraint C1: phase === Idle || len(originalSQL) > 0
  // Non-idle implies a query is loaded

  constraint C2: phase === Done implies len(resultSQL) > 0
  // Done implies we produced output

  constraint C3: phase === Failed implies len(errors) > 0
  // Failure implies error messages exist

  constraint C4: rulesApplied > 0 implies bestCost < estimateCost(planNodes, rootPlanId) + bestCost
  // Rules only fire when they reduce cost (loose — cost can't increase from applying rules)

  // ─── Temporal Verifications ───────────────────────────────
  verify V1: always(implies(phase === Parsing, eventually(phase === Rewriting || phase === Failed)))
  verify V2: always(implies(phase === Rewriting, eventually(phase === Planning || phase === Failed)))
  verify V3: always(implies(phase === Generating, eventually(phase === Done)))

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

  // ─── BOM ──────────────────────────────────────────────────
  bom {
    optimizer: "sql-optimizer@0.2.0"
    runtime:   "node@22.0.0"
  }

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

  interface PlanNodeMap {
    // Map from plan node ID to PlanNode object
  }

  interface PlanEdgeMap {
    // Map from parent ID to child IDs
  }

  interface CatalogMap {
    // Map from table name to schema info
  }

  interface StatsMap {
    // Map from table name to row count and column statistics
  }

  interface StringList {
    // List of strings
  }
}