@@ -211,6 +211,22 @@ def generateIR_Insert
211211 typesMatch := stmt.typesMatch
212212 }
213213
214+ /-- Convert AST.Condition to a simplified WhereClause predicate.
215+
216+ The AST uses a rich Condition type with dependent TypedValue constructors,
217+ but WhereClause uses a simplified (column, op, value) triple for the parser
218+ tier. We extract the first leaf comparison as the predicate representation.
219+ -/
220+ private def conditionToWhereClause : Condition → Option WhereClause
221+ | .eq (t := .string) (.string col) (.string val) =>
222+ some { predicate := (col, "=" , .string val), proof := fun _ => trivial }
223+ | .eq (t := .nat) (.nat col) (.nat val) =>
224+ some { predicate := (toString col, "=" , .nat val), proof := fun _ => trivial }
225+ | .lt (t := .nat) (.nat col) (.nat val) =>
226+ some { predicate := (toString col, "<" , .nat val), proof := fun _ => trivial }
227+ | .and c _ => conditionToWhereClause c -- Use left side of AND as representative
228+ | _ => none -- Complex conditions fall back to no WHERE in IR (runtime eval handles them)
229+
214230/-- Generate IR from SELECT AST -/
215231def generateIR_Select
216232 {α : Type }
@@ -220,10 +236,10 @@ def generateIR_Select
220236 .select {
221237 selectList := stmt.selectList,
222238 from_ := stmt.from_,
223- where_ := none, -- TODO: Convert Condition to WhereClause
224- orderBy := none, -- TODO: Parse ORDER BY
225- limit := none, -- TODO: Parse LIMIT
226- returning := none, -- TODO: Convert TypeRefinement
239+ where_ := stmt.where_.bind conditionToWhereClause,
240+ orderBy := none, -- AST.SelectStmt does not carry ORDER BY (Pipeline uses ParsedSelect)
241+ limit := none, -- AST.SelectStmt does not carry LIMIT (Pipeline uses ParsedSelect)
242+ returning := none, -- TODO: Convert TypeRefinement (requires runtime type erasure)
227243 permissions := permissions
228244 }
229245
@@ -495,6 +511,207 @@ def requiresProofs (ir : IR) : Bool :=
495511 | .normalize stmt => !stmt.proofs.isEmpty
496512 | _ => false
497513
514+ -- ============================================================================
515+ -- IR Evaluation (In-Memory)
516+ -- ============================================================================
517+
518+ /-- In-memory row: column name to string value mapping -/
519+ structure EvalRow where
520+ values : List (String × String)
521+ deriving Repr
522+
523+ /-- In-memory table: list of rows -/
524+ structure EvalTable where
525+ name : String
526+ columns : List String
527+ rows : List EvalRow
528+ deriving Repr
529+
530+ /-- In-memory database: list of tables -/
531+ structure EvalDatabase where
532+ tables : List EvalTable
533+ deriving Repr
534+
535+ namespace EvalDatabase
536+
537+ /-- Find a table by name -/
538+ def findTable (db : EvalDatabase) (name : String) : Option EvalTable :=
539+ db.tables.find? (·.name == name)
540+
541+ /-- Replace a table by name -/
542+ def updateTable (db : EvalDatabase) (name : String) (f : EvalTable → EvalTable) : EvalDatabase :=
543+ { tables := db.tables.map fun t => if t.name == name then f t else t }
544+
545+ /-- Create empty database -/
546+ def empty : EvalDatabase := { tables := [] }
547+
548+ end EvalDatabase
549+
550+ /-- Convert a TypedValue to its string representation for in-memory storage -/
551+ def typedValueToString : {t : TypeExpr} → TypedValue t → String
552+ | _, .nat n => toString n
553+ | _, .int i => toString i
554+ | _, .string s => s
555+ | _, .bool b => toString b
556+ | _, .float f => toString f
557+ | _, .boundedNat _ _ bn => toString bn.val
558+ | _, .nonEmptyString nes => nes.val
559+ | _, .promptScores ps => toString ps.overall.val
560+
561+ /-- Evaluate WHERE clause predicate against a row -/
562+ def evalWhereClause (row : EvalRow) (wc : WhereClause) : Bool :=
563+ let (col, op, val) := wc.predicate
564+ let rowVal := row.values.find? (·.1 == col) |>.map (·.2 )
565+ match rowVal with
566+ | none => false
567+ | some rv =>
568+ let valStr := match val with
569+ | .nat n => toString n
570+ | .int i => toString i
571+ | .string s => s
572+ | .bool b => toString b
573+ | .float f => toString f
574+ match op with
575+ | "=" => rv == valStr
576+ | "!=" => rv != valStr
577+ | "<" =>
578+ match rv.toNat?, valStr.toNat? with
579+ | some a, some b => a < b
580+ | _, _ => rv < valStr
581+ | ">" =>
582+ match rv.toNat?, valStr.toNat? with
583+ | some a, some b => a > b
584+ | _, _ => rv > valStr
585+ | "<=" =>
586+ match rv.toNat?, valStr.toNat? with
587+ | some a, some b => a ≤ b
588+ | _, _ => rv ≤ valStr
589+ | ">=" =>
590+ match rv.toNat?, valStr.toNat? with
591+ | some a, some b => a ≥ b
592+ | _, _ => rv ≥ valStr
593+ | _ => false
594+
595+ /-- Apply ORDER BY to rows -/
596+ def applyOrderBy (rows : List EvalRow) (ob : OrderByClause) : List EvalRow :=
597+ match ob.columns.head? with
598+ | none => rows
599+ | some (colName, direction) =>
600+ let isAsc := direction == "ASC"
601+ rows.toArray.qsort (fun r1 r2 =>
602+ let v1 := r1.values.find? (·.1 == colName) |>.map (·.2 ) |>.getD ""
603+ let v2 := r2.values.find? (·.1 == colName) |>.map (·.2 ) |>.getD ""
604+ -- Try numeric comparison first, fall back to string
605+ match v1.toNat?, v2.toNat? with
606+ | some n1, some n2 => if isAsc then n1 < n2 else n1 > n2
607+ | _, _ => if isAsc then v1 < v2 else v1 > v2
608+ ) |>.toList
609+
610+ /-- Result of evaluating an IR statement -/
611+ inductive EvalIRResult where
612+ | rows : List String → List (List String) → EvalIRResult -- columns, row values
613+ | mutation : Nat → EvalIRResult -- affected rows
614+ | error : String → EvalIRResult
615+ deriving Repr
616+
617+ /-- Format an EvalIRResult for display -/
618+ def EvalIRResult.toString : EvalIRResult → String
619+ | .rows cols rowData =>
620+ if rowData.isEmpty then "(0 rows)"
621+ else
622+ let header := String.intercalate " | " cols
623+ let separator := String.mk (List.replicate header.length '-' )
624+ let rowStrs := rowData.map fun row =>
625+ String.intercalate " | " row
626+ s! "{ header} \n { separator} \n { String.intercalate "\n " rowStrs} \n ({ rowData.length} rows)"
627+ | .mutation n => s! "OK, { n} row(s) affected"
628+ | .error msg => s! "Error: { msg} "
629+
630+ /-- Evaluate an IR statement against an in-memory database.
631+
632+ Returns the updated database and the result.
633+ -/
634+ def evalIR (db : EvalDatabase) (ir : IR) : EvalDatabase × EvalIRResult :=
635+ match ir with
636+ | .select stmt =>
637+ let tableName := match stmt.from_.tables.head? with
638+ | some t => t.name
639+ | none => ""
640+ match db.findTable tableName with
641+ | none => (db, .error s! "Table not found: { tableName} "
642+ | some table =>
643+ -- Filter rows by WHERE clause
644+ let filtered := match stmt.where_ with
645+ | none => table.rows
646+ | some wc => table.rows.filter (evalWhereClause · wc)
647+ -- Apply ORDER BY
648+ let sorted := match stmt.orderBy with
649+ | none => filtered
650+ | some ob => applyOrderBy filtered ob
651+ -- Apply LIMIT
652+ let limited := match stmt.limit with
653+ | none => sorted
654+ | some n => sorted.take n
655+ -- Project columns
656+ let cols := match stmt.selectList with
657+ | .star => table.columns
658+ | .columns cs => cs
659+ | .typed _ _ => table.columns
660+ let rowData := limited.map fun row =>
661+ cols.map fun c =>
662+ row.values.find? (·.1 == c) |>.map (·.2 ) |>.getD "NULL"
663+ (db, .rows cols rowData)
664+
665+ | .insert stmt =>
666+ let row : EvalRow := {
667+ values := stmt.columns.zip (stmt.values.map fun ⟨_, v⟩ => typedValueToString v)
668+ }
669+ match db.findTable stmt.table with
670+ | none =>
671+ -- Create table if it doesn't exist
672+ let newTable : EvalTable := {
673+ name := stmt.table,
674+ columns := stmt.columns,
675+ rows := [row]
676+ }
677+ ({ tables := db.tables ++ [newTable] }, .mutation 1 )
678+ | some table =>
679+ let newTable := { table with rows := table.rows ++ [row] }
680+ (db.updateTable stmt.table (fun _ => newTable), .mutation 1 )
681+
682+ | .update stmt =>
683+ match db.findTable stmt.table with
684+ | none => (db, .error s! "Table not found: { stmt.table} "
685+ | some table =>
686+ -- Find rows matching WHERE clause
687+ let (matching, nonMatching) := match stmt.where_ with
688+ | none => (table.rows, [])
689+ | some wc =>
690+ let m := table.rows.filter (evalWhereClause · wc)
691+ let nm := table.rows.filter (fun r => !evalWhereClause r wc)
692+ (m, nm)
693+ -- Apply assignments to matching rows
694+ let updated := matching.map fun row =>
695+ stmt.assignments.foldl (fun r a =>
696+ let newVal := typedValueToString a.value.2
697+ { values := r.values.map fun (c, v) =>
698+ if c == a.column then (c, newVal) else (c, v) }
699+ ) row
700+ let newTable := { table with rows := nonMatching ++ updated }
701+ (db.updateTable stmt.table (fun _ => newTable), .mutation matching.length)
702+
703+ | .delete stmt =>
704+ match db.findTable stmt.table with
705+ | none => (db, .error s! "Table not found: { stmt.table} "
706+ | some table =>
707+ let matching := table.rows.filter (evalWhereClause · stmt.where_)
708+ let remaining := table.rows.filter (fun r => !evalWhereClause r stmt.where_)
709+ let newTable := { table with rows := remaining }
710+ (db.updateTable stmt.table (fun _ => newTable), .mutation matching.length)
711+
712+ | .normalize _ =>
713+ (db, .error "NORMALIZE not yet supported in evaluation" )
714+
498715-- ============================================================================
499716-- Example: IR Construction
500717-- ============================================================================
0 commit comments