diff options
Diffstat (limited to '')
36 files changed, 1330 insertions, 371 deletions
@@ -1,5 +1,5 @@ -_build/ -.direnv/ +_build +.direnv # Nix build/link artifacts result diff --git a/bin/server.ml b/bin/server.ml index 2c84468..80f392b 100644 --- a/bin/server.ml +++ b/bin/server.ml @@ -35,6 +35,7 @@ let materialize_relation storage (rel : Relation.t) limit = let short_hash (h : string) = String.sub h 0 (min 8 (String.length h)) module BranchOps = Management.Branch.Make(Management.Physical.Memory) +module Dispatch = Dbms_language.Memory let get_branch storage = match BranchOps.get_head storage with @@ -76,96 +77,45 @@ let ok_response storage db_name db_hash msg = List [Atom "branch"; Atom (get_branch storage)]; ] -let error_response storage db_name db_hash msg = +let error_response storage db_name db_hash err_sexp = let open Sexplib.Sexp in to_string @@ List [ Atom "error"; - List [Atom "message"; Atom msg]; + err_sexp; List [Atom "db_hash"; Atom (short_hash db_hash)]; List [Atom "db_name"; Atom db_name]; List [Atom "branch"; Atom (get_branch storage)]; ] -let manip_err = function - | Manipulation.RelationNotFound s -> "RelationNotFound: " ^ s - | Manipulation.RelationAlreadyExists s -> "RelationAlreadyExists: " ^ s - | Manipulation.TupleNotFound h -> "TupleNotFound: " ^ h - | Manipulation.DuplicateTuple h -> "DuplicateTuple: " ^ h - | Manipulation.ConstraintViolation s -> "ConstraintViolation: " ^ s - | Manipulation.StorageError s -> "StorageError: " ^ s - -(* TODO: language dispatch by trying parsers in sequence is a code smell — - a valid DRL expression that happens to also parse as DML would silently - be treated as DRL. The three sublanguages should share a common envelope, - e.g. a top-level tag distinguishing (Query ...) from (Exec ...). *) let advance_head_branch storage new_hash = match BranchOps.get_head storage with | Ok (Some branch_name) -> ignore (BranchOps.update_tip storage ~name:branch_name ~tip:new_hash) | _ -> () +let dbms_dispatch = Dispatch.create [ + (module Drl.Sublanguage.Memory : Dispatch.SubS); + (module Ddl.Sublanguage.Memory : Dispatch.SubS); + (module Dml.Sublanguage.Memory : Dispatch.SubS); + (module Icl.Sublanguage.Memory : Dispatch.SubS); + (module Dcl.Sublanguage.Memory : Dispatch.SubS); +] + let execute_command storage db_ref cmd = let db = !db_ref in let h = db.Management.Database.hash in let name = db.Management.Database.name in let ok = ok_response storage name in let err = error_response storage name in - (* TODO: (schema) is a stopgap. Introspection should be expressible in - DRL itself via the catalog relations, not special-cased here. *) - let cmd = match String.trim cmd with - | "(schema)" -> {|(Base sakura:attribute)|} - | s -> s - in - match Drl.Parser.of_string cmd with - | Ok query -> - (match Drl.Executor.Memory.execute storage db query with - | Ok rel -> relation_to_sexp storage name h rel default_limit - | Error (Drl.Executor.Memory.RelationNotFound s) -> - err h ("RelationNotFound: " ^ s) - | Error (Drl.Executor.Memory.AlgebraError (Algebra.StorageError s)) -> - err h ("StorageError: " ^ s) - | Error (Drl.Executor.Memory.AlgebraError (Algebra.GeneratorError s)) -> - err h ("GeneratorError: " ^ s)) - | Error _ -> - match Dml.Parser.of_string cmd with - | Ok stmt -> - (match Dml.Executor.Memory.execute storage db stmt with - | Ok new_db -> - db_ref := new_db; - advance_head_branch storage new_db.Management.Database.hash; - ok new_db.Management.Database.hash "updated" - | Error (Dml.Executor.Memory.ManipulationError me) -> - err h (manip_err me) - | Error (Dml.Executor.Memory.RelationNotFound s) -> - err h ("RelationNotFound: " ^ s) - | Error (Dml.Executor.Memory.ParseError s) -> - err h ("ParseError: " ^ s)) - | Error _ -> - match Icl.Parser.of_string cmd with - | Ok stmt -> - (match Icl.Executor.Memory.execute storage db stmt with - | Ok (new_db, msg) -> - db_ref := new_db; - advance_head_branch storage new_db.Management.Database.hash; - ok new_db.Management.Database.hash msg - | Error (Icl.Executor.Memory.ManipulationError me) -> - err h (manip_err me) - | Error (Icl.Executor.Memory.ConversionError s) -> - err h ("ConversionError: " ^ s)) - | Error _ -> - match Dcl.Parser.of_string cmd with - | Ok stmt -> - (match Dcl.Executor.Memory.execute storage db stmt with - | Ok (new_db, msg) -> - db_ref := new_db; - advance_head_branch storage new_db.Management.Database.hash; - ok new_db.Management.Database.hash msg - | Error (Dcl.Executor.Memory.BranchError s) -> - err h ("BranchError: " ^ s) - | Error (Dcl.Executor.Memory.MergeError s) -> - err h ("MergeError: " ^ s)) - | Error _ -> - err h "ParseError: not valid DRL, DML, ICL, or DCL" + match Dispatch.execute dbms_dispatch storage db cmd with + | Ok (Sublanguage.Query rel) -> + relation_to_sexp storage name h rel default_limit + | Ok (Sublanguage.Transition (new_db, msg)) -> + db_ref := new_db; + advance_head_branch storage new_db.Management.Database.hash; + ok new_db.Management.Database.hash msg + | Error e -> + err h (Dispatch.sexp_of_dispatch_error e) (* TODO: registration failures are silently ignored; a broken prelude relation leaves the catalog in a partially-seeded state with no @@ -184,7 +134,7 @@ let register_prelude_relations storage db = | Ok (new_db, _) -> new_db | Error e -> Printf.eprintf "Warning: failed to register prelude relation %s: %s\n%!" - rel.name (manip_err e); + rel.name (Manipulation.string_of_error e); db) db [ less_than_natural @@ -199,6 +149,18 @@ let register_prelude_relations storage db = ; divide_natural ] +let print_with_time str = + let now = Unix.gettimeofday () in + let tm = Unix.localtime now in + let orange = "\027[38;5;208m" in + let reset = "\027[0m" in + let formatted_time = + Printf.sprintf "%04d-%02d-%02d %02d:%02d:%02d" + (tm.Unix.tm_year + 1900) (tm.Unix.tm_mon + 1) tm.Unix.tm_mday + tm.Unix.tm_hour tm.Unix.tm_min tm.Unix.tm_sec + in + print_endline @@ Printf.sprintf "%s[%s]%s %s" orange formatted_time reset str + (* TODO: single-threaded accept loop — one slow or hung client blocks all others. Should use threads or non-blocking I/O. *) let handle_client storage db_ref fd = @@ -215,183 +177,75 @@ let handle_client storage db_ref fd = let db = !db_ref in error_response storage db.Management.Database.name db.Management.Database.hash - ("Uncaught error: " ^ Printexc.to_string e) + Sexplib.Sexp.(List [Atom "uncaught-error"; Atom (Printexc.to_string e)]) in + print_with_time response; output_string oc (response ^ "\n"); flush oc end done with End_of_file | Unix.Unix_error _ -> ()) -let depart_emp = [ - "(CreateRelation (name \"Department\") (schema ((dept_id \"integer\") (dept_name \"string\") (location \"string\"))))"; - "(CreateRelation (name \"Employee\") (schema ((emp_id \"integer\") (emp_name \"string\") (salary \"float\") (dept_id \"integer\") (hire_date \"string\"))))"; - "(RegisterConstraint(constraint_name \"salary_positive\")(relation_name \"Employee\")(body (MemberOf(target \"positive_reals\")(binding ((salary (Var \"salary\")))))))"; - "(RegisterConstraint - (constraint_name \"fk_employee_dept\") - (relation_name \"Employee\") - (body (MemberOf - (target \"Department\") - (binding ((dept_id (Var \"dept_id\")))))))"; - "(InsertTuple (relation \"Department\") (attributes ((dept_id (Int 1)) (location (Str \"Gifu\")) (dept_name (Str \"Nippon Ichi\")))))"; - "(InsertTuples (relation \"Employee\") (tuples (((emp_id (Int 101)) (emp_name (Str \"Alice Johnson\")) (salary (Float 95000.0)) (dept_id (Int 1)) (hire_date (Str \"2020-01-15\"))))))" - ] - -let _depart_emp () = - match Management.Physical.Memory.create () with - | Error _ -> failwith "Failed to create storage" - | Ok storage -> - match Manipulation.Memory.create_database storage ~name:"sakura" with - | Error _ -> failwith "Failed to create initial database" - | Ok db -> - let db = register_prelude_relations storage db in - let db_ref = ref db in - Printf.printf "Database hash: %s\n%!" (short_hash db.Management.Database.hash); - List.iter (fun cmd -> print_endline @@ execute_command storage db_ref cmd) - depart_emp; - () - -let n_way = [ - "(CreateRelation - (name \"Building\") - (schema - ((building_id \"integer\") - (building_name \"string\") - (floors \"integer\"))))"; - "(CreateRelation - (name \"Room\") - (schema - ((room_id \"integer\") - (building_id \"integer\") - (floor \"integer\") - (room_number \"string\"))))"; -"(CreateRelation - (name \"Suite\") - (schema - ((suite_id \"integer\") - (room_id \"integer\") - (suite_name \"string\") - (capacity \"integer\"))))"; -(* FK: every Room must belong to an existing Building *) -"(RegisterConstraint - (constraint_name \"fk_room_building\") - (relation_name \"Room\") - (body (MemberOf - (target \"Building\") - (binding ((building_id (Var \"building_id\")))))))"; -(* FK: every Suite must belong to an existing Room *) -"(RegisterConstraint - (constraint_name \"fk_suite_room\") - (relation_name \"Suite\") - (body (MemberOf - (target \"Room\") - (binding ((room_id (Var \"room_id\")))))))"; -(* A suite is only valid if its room belongs to a building with more than 3 floors *) -"(RegisterConstraint - (constraint_name \"suite_in_tall_building\") - (relation_name \"Suite\") - (body - (Exists (variable \"r\") (quantifier \"Room\") - (body - (Exists (variable \"b\") (quantifier \"Building\") - (body - (And - ((MemberOf (target \"Room\") - (binding ((room_id (Var \"room_id\"))))) - (MemberOf (target \"Building\") - (binding ((building_id (Var \"r.building_id\"))))) - (MemberOf (target \"greater_than_natural\") - (binding ((left (Var \"b.floors\")) (right (Const (Int 3))))))))))))))"; -"(InsertTuple - (relation \"Building\") - (attributes - ((building_id (Int 2)) - (building_name (Str \"Tower B\")) - (floors (Int 2)))))"; - "(InsertTuple - (relation \"Building\") - (attributes - ((building_id (Int 1)) - (building_name (Str \"Tower A\")) - (floors (Int 10)))))"; -"(InsertTuples - (relation \"Room\") - (tuples - (((room_id (Int 101)) (building_id (Int 1)) (floor (Int 1)) (room_number (Str \"1A\"))) - ((room_id (Int 102)) (building_id (Int 1)) (floor (Int 2)) (room_number (Str \"2A\"))) - ((room_id (Int 201)) (building_id (Int 2)) (floor (Int 1)) (room_number (Str \"1B\"))))))"; -"(InsertTuples - (relation \"Suite\") - (tuples - (((suite_id (Int 1001)) (room_id (Int 101)) (suite_name (Str \"Presidential\")) (capacity (Int 4))) - ((suite_id (Int 1002)) (room_id (Int 101)) (suite_name (Str \"Standard\")) (capacity (Int 2))) - ((suite_id (Int 1003)) (room_id (Int 102)) (suite_name (Str \"Deluxe\")) (capacity (Int 3))))))"; - ] +let setup () = + let ( let* ) = Result.bind in + let* storage = + Management.Physical.Memory.create () + |> Result.map_error (Fun.const "Failed to create storage") + in + let* db = + Manipulation.Memory.create_database storage ~name:"sakura" + |> Result.map_error (Fun.const "Failed to create initial database") + in + Ok (storage, db) + +let register_branch_relations storage db = + (* Register ephemeral sakura:branch and sakura:head relations backed by + the raw branch registry — no stored tuples, no circularity. *) + let register db rel = + match Manipulation.Memory.create_immutable_relation storage db + ~name:rel.Relation.name + ~schema:rel.Relation.schema + ~generator:(Option.get rel.Relation.generator) + ~membership_criteria:rel.Relation.membership_criteria + ~cardinality:rel.Relation.cardinality + with + | Ok (db, _) -> db + | Error e -> + Printf.eprintf "Warning: failed to register %s: %s\n%!" + rel.Relation.name (Manipulation.string_of_error e); + db + in + db + |> Fun.flip register (BranchOps.branch_relation storage) + |> Fun.flip register (BranchOps.head_relation storage) -let _n_way () = - match Management.Physical.Memory.create () with - | Error _ -> failwith "Failed to create storage" - | Ok storage -> - match Manipulation.Memory.create_database storage ~name:"sakura" with - | Error _ -> failwith "Failed to create initial database" - | Ok db -> - let db = register_prelude_relations storage db in - let db_ref = ref db in - Printf.printf "Database hash: %s\n%!" (short_hash db.Management.Database.hash); - List.iter (fun cmd -> print_endline @@ execute_command storage db_ref cmd) - n_way; - () +let warn_on_error fmt = function + | Ok () -> () + | Error e -> Printf.eprintf fmt e let () = - let port = default_port in - match Management.Physical.Memory.create () with - | Error _ -> failwith "Failed to create storage" - | Ok storage -> - match Manipulation.Memory.create_database storage ~name:"sakura" with - | Error _ -> failwith "Failed to create initial database" - | Ok db -> - let db = register_prelude_relations storage db in - (* Register ephemeral sakura:branch and sakura:head relations backed by - the raw branch registry — no stored tuples, no circularity. *) - let db = - let register db rel = - match Manipulation.Memory.create_immutable_relation storage db - ~name:rel.Relation.name - ~schema:rel.Relation.schema - ~generator:(Option.get rel.Relation.generator) - ~membership_criteria:rel.Relation.membership_criteria - ~cardinality:rel.Relation.cardinality - with - | Ok (db, _) -> db - | Error e -> - Printf.eprintf "Warning: failed to register %s: %s\n%!" - rel.Relation.name (match e with - | Manipulation.RelationAlreadyExists s -> "already exists: " ^ s - | Manipulation.StorageError s -> s | _ -> "error"); - db - in - let db = register db (BranchOps.branch_relation storage) in - let db = register db (BranchOps.head_relation storage) in - db - in - (* Create default master branch in raw registry and set HEAD *) - (match BranchOps.create storage ~name:"master" - ~tip:db.Management.Database.hash with - | Error e -> Printf.eprintf "Warning: failed to create master branch: %s\n%!" e - | Ok () -> ()); - (match BranchOps.checkout storage "master" with - | Error e -> Printf.eprintf "Warning: failed to checkout master: %s\n%!" e - | Ok () -> ()); - let db_ref = ref db in - let sock = Unix.socket Unix.PF_INET Unix.SOCK_STREAM 0 in - Unix.setsockopt sock Unix.SO_REUSEADDR true; - Unix.setsockopt sock Unix.SO_REUSEPORT true; - Unix.bind sock (Unix.ADDR_INET (Unix.inet_addr_loopback, port)); - Unix.listen sock 5; - Printf.printf "Sakura server listening on 127.0.0.1:%d\n" port; - Printf.printf "Database hash: %s\n%!" (short_hash db.Management.Database.hash); - while true do - let (client_fd, _addr) = Unix.accept sock in - handle_client storage db_ref client_fd; - (try Unix.close client_fd with _ -> ()) - done + match setup () with + | Error msg -> failwith msg + | Ok (storage, db) -> + let db = db + |> register_prelude_relations storage + |> register_branch_relations storage + in + (* Create default master branch in raw registry and set HEAD *) + BranchOps.create storage ~name:"master" ~tip:db.Management.Database.hash + |> warn_on_error "Warning: failed to create master branch: %s\n%!"; + BranchOps.checkout storage "master" + |> warn_on_error "Warning: failed to checkout master: %s\n%!"; + let db_ref = ref db in + let sock = Unix.socket Unix.PF_INET Unix.SOCK_STREAM 0 in + Unix.setsockopt sock Unix.SO_REUSEADDR true; + Unix.setsockopt sock Unix.SO_REUSEPORT true; + Unix.bind sock (Unix.ADDR_INET (Unix.inet_addr_loopback, default_port)); + Unix.listen sock 5; + Printf.printf "Sakura server listening on 127.0.0.1:%d\n" default_port; + Printf.printf "Database hash: %s\n%!" (short_hash db.Management.Database.hash); + while true do + let (client_fd, _addr) = Unix.accept sock in + handle_client storage db_ref client_fd; + (try Unix.close client_fd with _ -> ()) + done @@ -275,6 +275,10 @@ ppx_protocol_conv ppx_protocol_conv_xml_light ocamlPackages.earlybird + # Formal verification + legacyPackages.coq + legacyPackages.coqPackages.stdlib + legacyPackages.z3 ]; diff --git a/lib/dbms_language.ml b/lib/dbms_language.ml new file mode 100644 index 0000000..8d61aa3 --- /dev/null +++ b/lib/dbms_language.ml @@ -0,0 +1,39 @@ +(** Composable dispatch over sublanguages. + + All commands must use the tagged envelope format: (tag payload) + where [tag] is the sublanguage name (drl, dml, ddl, icl, dcl, ...). + Adding a new sublanguage is just extending the list passed to [create]. *) + +module Make (Storage : Management.Physical.S with type error = string) = struct + module type SubS = Sublanguage.S with type storage = Storage.t + + type dispatch_error = NoMatch of Sexplib.Sexp.t + + type dispatch = (module SubS) list + + let create (langs : (module SubS) list) : dispatch = langs + + let execute + (langs : dispatch) + (storage : Storage.t) + (db : Management.Database.t) + (input : string) + : (Sublanguage.result, dispatch_error) Result.t = + let no_match s = Error (NoMatch Sexplib.Sexp.(List [Atom "parse-error"; Atom s])) in + match Envelope.parse input with + | Error msg -> no_match msg + | Ok { tag; payload } -> + match List.find_opt (fun (module L : SubS) -> L.name = tag) langs with + | None -> no_match ("unknown sublanguage: " ^ tag) + | Some (module L) -> + match L.parse_sexp payload with + | Error e -> Error (NoMatch (L.sexp_of_error e)) + | Ok ast -> + match L.execute storage db ast with + | Ok result -> Ok result + | Error e -> Error (NoMatch (L.sexp_of_error e)) + + let sexp_of_dispatch_error (NoMatch sexp) = sexp +end + +module Memory = Make(Management.Physical.Memory) diff --git a/lib/dcl/executor.ml b/lib/dcl/executor.ml index bf549ec..cf2cfed 100644 --- a/lib/dcl/executor.ml +++ b/lib/dcl/executor.ml @@ -4,22 +4,22 @@ module Make (Storage : Management.Physical.S with type error = string) = struct module MergeOps = Management.Merge.Make(Storage)(Ops) type error = + | ParseError of string | BranchError of string | MergeError of string + let sexp_of_error e = + let open Sexplib.Sexp in + match e with + | ParseError s -> List [Atom "parse-error"; Atom s] + | BranchError s -> List [Atom "branch-error"; Atom s] + | MergeError s -> List [Atom "merge-error"; Atom s] + let convert_strategy : Ast.merge_strategy -> Management.Merge.strategy = function | Ast.PreferLeft -> Management.Merge.PreferLeft | Ast.PreferRight -> Management.Merge.PreferRight | Ast.RevertToAncestor -> Management.Merge.RevertToAncestor - let manip_err = function - | Manipulation.RelationNotFound s -> "RelationNotFound: " ^ s - | Manipulation.RelationAlreadyExists s -> "RelationAlreadyExists: " ^ s - | Manipulation.TupleNotFound h -> "TupleNotFound: " ^ h - | Manipulation.DuplicateTuple h -> "DuplicateTuple: " ^ h - | Manipulation.ConstraintViolation s -> "ConstraintViolation: " ^ s - | Manipulation.StorageError s -> "StorageError: " ^ s - let execute (storage : Storage.t) (db : Management.Database.t) @@ -45,7 +45,7 @@ module Make (Storage : Management.Physical.S with type error = string) = struct | Error e -> Error (BranchError e) | Ok () -> (match Ops.load_database storage tip with - | Error e -> Error (BranchError (manip_err e)) + | Error e -> Error (BranchError (Manipulation.string_of_error e)) | Ok None -> Error (BranchError ("No database at hash: " ^ tip)) | Ok (Some loaded_db) -> Ok (loaded_db, "HEAD:" ^ branch_name)))) @@ -75,7 +75,7 @@ module Make (Storage : Management.Physical.S with type error = string) = struct | Ok (Some left_tip), Ok (Some right_tip) -> let strat = convert_strategy strategy in (match MergeOps.merge ~storage ~strategy:strat ~left_tip ~right_tip with - | Error e -> Error (MergeError (manip_err e)) + | Error e -> Error (MergeError (Manipulation.string_of_error e)) | Ok (Management.Merge.Failed conflicts) -> let msgs = List.map (function | Management.Merge.TupleConflict { relation; hash } -> diff --git a/lib/dcl/parser.ml b/lib/dcl/parser.ml index 3caf748..ef64924 100644 --- a/lib/dcl/parser.ml +++ b/lib/dcl/parser.ml @@ -1,9 +1,9 @@ type error = ParseError of string -let of_string s = +let of_sexp sexp = (* ppx_sexp_conv encodes no-argument variants as bare atoms, so unwrap a single-element list (e.g. (GetHead)) → atom (GetHead). *) - let sexp = match Sexplib.Sexp.of_string s with + let sexp = match sexp with | Sexplib.Sexp.List [atom] -> atom | other -> other in @@ -11,5 +11,8 @@ let of_string s = | stmt -> Ok stmt | exception exn -> Error (ParseError (Printexc.to_string exn)) +let of_string s = + of_sexp (Sexplib.Sexp.of_string s) + let to_string stmt = Ast.sexp_of_statement stmt |> Sexplib.Sexp.to_string_hum diff --git a/lib/dcl/sublanguage.ml b/lib/dcl/sublanguage.ml new file mode 100644 index 0000000..112b6ed --- /dev/null +++ b/lib/dcl/sublanguage.ml @@ -0,0 +1,23 @@ +module Make (Storage : Management.Physical.S with type error = string) = struct + module Exec = Executor.Make(Storage) + + type storage = Storage.t + type ast = Ast.statement + type error = Exec.error + + let name = "dcl" + + let parse_sexp sexp = + match Parser.of_sexp sexp with + | Ok r -> Ok r + | Error (Parser.ParseError s) -> Error (Exec.ParseError s) + + let execute storage db ast = + match Exec.execute storage db ast with + | Ok (db, msg) -> Ok (Sublanguage.Transition (db, msg)) + | Error e -> Error e + + let sexp_of_error = Exec.sexp_of_error +end + +module Memory = Make(Management.Physical.Memory) diff --git a/lib/ddl/ast.ml b/lib/ddl/ast.ml new file mode 100644 index 0000000..7faee40 --- /dev/null +++ b/lib/ddl/ast.ml @@ -0,0 +1,16 @@ +open Sexplib.Std + +type cardinality_spec = + | Finite of int + | AlephZero + | Continuum + | ConstrainedFinite +[@@deriving sexp] + +type statement = + | CreateDatabase of string + | CreateRelation of { name: string; schema: (string * string) list } + | RetractRelation of string + | ClearRelation of string + | RegisterDomain of { name: string; cardinality: cardinality_spec } +[@@deriving sexp] diff --git a/lib/ddl/executor.ml b/lib/ddl/executor.ml new file mode 100644 index 0000000..fbb2f62 --- /dev/null +++ b/lib/ddl/executor.ml @@ -0,0 +1,68 @@ +module Make (Storage : Management.Physical.S) = struct + module Ops = Manipulation.Make(Storage) + + type error = + | ParseError of string + | ManipulationError of Manipulation.error + | RelationNotFound of string + + let sexp_of_error e = + let open Sexplib.Sexp in + match e with + | ParseError s -> List [Atom "parse-error"; Atom s] + | ManipulationError e -> Manipulation.sexp_of_error e + | RelationNotFound s -> List [Atom "relation-not-found"; Atom s] + + let ( let* ) = Result.bind + + let wrap_manip r = Result.map_error (fun e -> ManipulationError e) r + + let get_rel db name = + Ops.get_relation db ~name + |> Option.to_result ~none:(RelationNotFound name) + + let convert_cardinality : Ast.cardinality_spec -> Conventions.Cardinality.t = function + | Ast.Finite n -> Conventions.Cardinality.Finite n + | Ast.AlephZero -> Conventions.Cardinality.AlephZero + | Ast.Continuum -> Conventions.Cardinality.Continuum + | Ast.ConstrainedFinite -> Conventions.Cardinality.ConstrainedFinite + + let execute + (storage : Storage.t) + (db : Management.Database.t) + (stmt : Ast.statement) + : (Management.Database.t * string, error) result = + match stmt with + | Ast.CreateDatabase name -> + let* db = Ops.create_database storage ~name |> wrap_manip in + Ok (db, "Database created: " ^ name) + + | Ast.CreateRelation { name; schema = schema_pairs } -> + let schema = + List.fold_left (fun s (attr, dom) -> Schema.add attr dom s) Schema.empty schema_pairs + in + let* (db, _) = Ops.create_relation storage db ~name ~schema |> wrap_manip in + Ok (db, "Relation created: " ^ name) + + | Ast.RetractRelation name -> + let* db = Ops.retract_relation storage db ~name |> wrap_manip in + Ok (db, "Relation retracted: " ^ name) + + | Ast.ClearRelation name -> + let* rel = get_rel db name in + let* (db, _) = Ops.clear_relation storage db rel |> wrap_manip in + Ok (db, "Relation cleared: " ^ name) + + | Ast.RegisterDomain { name; cardinality } -> + let domain = Domain.make + ~name + ~generator:(fun _ -> Generator.Error "not enumerable via DDL") + ~membership_criteria:(fun _ -> true) + ~cardinality:(convert_cardinality cardinality) + ~compare:Stdlib.compare + in + let* db = Ops.register_domain storage db domain |> wrap_manip in + Ok (db, "Domain registered: " ^ name) +end + +module Memory = Make(Management.Physical.Memory) diff --git a/lib/ddl/parser.ml b/lib/ddl/parser.ml new file mode 100644 index 0000000..28f8b6c --- /dev/null +++ b/lib/ddl/parser.ml @@ -0,0 +1,14 @@ +type error = ParseError of string + +let of_sexp sexp = + match Ast.statement_of_sexp sexp with + | stmt -> Ok stmt + | exception exn -> Error (ParseError (Printexc.to_string exn)) + +let of_string s = + match Sexplib.Sexp.of_string s |> Ast.statement_of_sexp with + | stmt -> Ok stmt + | exception exn -> Error (ParseError (Printexc.to_string exn)) + +let to_string stmt = + Ast.sexp_of_statement stmt |> Sexplib.Sexp.to_string_hum diff --git a/lib/ddl/sublanguage.ml b/lib/ddl/sublanguage.ml new file mode 100644 index 0000000..26a012f --- /dev/null +++ b/lib/ddl/sublanguage.ml @@ -0,0 +1,23 @@ +module Make (Storage : Management.Physical.S) = struct + module Exec = Executor.Make(Storage) + + type storage = Storage.t + type ast = Ast.statement + type error = Exec.error + + let name = "ddl" + + let parse_sexp sexp = + match Parser.of_sexp sexp with + | Ok r -> Ok r + | Error (Parser.ParseError s) -> Error (Exec.ParseError s) + + let execute storage db ast = + match Exec.execute storage db ast with + | Ok (db, msg) -> Ok (Sublanguage.Transition (db, msg)) + | Error e -> Error e + + let sexp_of_error = Exec.sexp_of_error +end + +module Memory = Make(Management.Physical.Memory) diff --git a/lib/dml/ast.ml b/lib/dml/ast.ml index 4a903e7..479437a 100644 --- a/lib/dml/ast.ml +++ b/lib/dml/ast.ml @@ -3,20 +3,11 @@ open Sexplib.Std type attr_value = string * Drl.Ast.value [@@deriving sexp] -type cardinality_spec = - | Finite of int - | AlephZero - | Continuum - | ConstrainedFinite -[@@deriving sexp] - type statement = - | CreateDatabase of string - | CreateRelation of { name: string; schema: (string * string) list } - | RetractRelation of string - | ClearRelation of string - | RegisterDomain of { name: string; cardinality: cardinality_spec } | InsertTuple of { relation: string; attributes: attr_value list } | InsertTuples of { relation: string; tuples: attr_value list list } | DeleteTuple of { relation: string; attributes: attr_value list } + | Assign of { target: string; body: Drl.Ast.query } + | InsertFrom of { target: string; source: Drl.Ast.query } + | DeleteWhere of { target: string; predicate: Drl.Ast.query } [@@deriving sexp] diff --git a/lib/dml/executor.ml b/lib/dml/executor.ml index 3a8b05a..7c08a24 100644 --- a/lib/dml/executor.ml +++ b/lib/dml/executor.ml @@ -1,19 +1,35 @@ module Make (Storage : Management.Physical.S) = struct module Ops = Manipulation.Make(Storage) + module Alg = Algebra.Make(Storage) + module DrlExec = Drl.Executor.Make(Storage) type error = + | ParseError of string | ManipulationError of Manipulation.error - | RelationNotFound of string - | ParseError of string + | RelationNotFound of string + | AlgebraError of Algebra.error + + let sexp_of_error e = + let open Sexplib.Sexp in + match e with + | ParseError s -> List [Atom "parse-error"; Atom s] + | ManipulationError e -> Manipulation.sexp_of_error e + | RelationNotFound s -> List [Atom "relation-not-found"; Atom s] + | AlgebraError (Algebra.StorageError s) -> List [Atom "storage-error"; Atom s] + | AlgebraError (Algebra.GeneratorError s) -> List [Atom "generator-error"; Atom s] + + let ( let* ) = Result.bind let wrap_manip r = Result.map_error (fun e -> ManipulationError e) r - (** Convert a cardinality_spec AST node to a Conventions.Cardinality.t *) - let convert_cardinality : Ast.cardinality_spec -> Conventions.Cardinality.t = function - | Ast.Finite n -> Conventions.Cardinality.Finite n - | Ast.AlephZero -> Conventions.Cardinality.AlephZero - | Ast.Continuum -> Conventions.Cardinality.Continuum - | Ast.ConstrainedFinite -> Conventions.Cardinality.ConstrainedFinite + let wrap_alg e = AlgebraError e + + let get_rel db name = + match Ops.get_relation db ~name with + | Some r -> Ok r + | None -> Error (RelationNotFound name) + + let retarget target (t : Tuple.materialized) = { t with Tuple.relation = target } (** Build a materialized tuple from a list of (attr_name, ast_value) pairs *) let build_tuple ~relation (attributes : Ast.attr_value list) : Tuple.materialized = @@ -28,78 +44,74 @@ module Make (Storage : Management.Physical.S) = struct in { Tuple.relation; attributes = attr_map } + let eval_query storage db query = + match DrlExec.execute storage db query with + | Ok rel -> Ok rel + | Error (DrlExec.ParseError s) -> Error (ParseError s) + | Error (DrlExec.RelationNotFound s) -> Error (RelationNotFound s) + | Error (DrlExec.AlgebraError e) -> Error (AlgebraError e) + + let materialize_tuples storage rel = + Result.map_error wrap_alg (Alg.materialize storage rel) + let execute (storage : Storage.t) (db : Management.Database.t) (stmt : Ast.statement) : (Management.Database.t, error) result = match stmt with - | Ast.CreateDatabase name -> - Ops.create_database storage ~name |> wrap_manip - - | Ast.CreateRelation { name; schema = schema_pairs } -> - let schema = - List.fold_left - (fun s (attr, dom) -> Schema.add attr dom s) - Schema.empty - schema_pairs - in - (match Ops.create_relation storage db ~name ~schema |> wrap_manip with - | Ok (db, _rel) -> Ok db - | Error e -> Error e) - - | Ast.RetractRelation name -> - Ops.retract_relation storage db ~name |> wrap_manip - - | Ast.ClearRelation name -> - (match Ops.get_relation db ~name with - | None -> Error (RelationNotFound name) - | Some rel -> - match Ops.clear_relation storage db rel |> wrap_manip with - | Ok (db, _rel) -> Ok db - | Error e -> Error e) - - | Ast.RegisterDomain { name; cardinality } -> - (* TODO: Custom generators, membership_criteria, and comparators - are not supported via DML. Use the OCaml API for full-featured - domain definitions (e.g., custom enumeration, type-specific - comparison, or domain-specific validation). *) - let domain = Domain.make - ~name - ~generator:(fun _ -> Generator.Error "not enumerable via DML") - ~membership_criteria:(fun _ -> true) - ~cardinality:(convert_cardinality cardinality) - ~compare:Stdlib.compare - in - Ops.register_domain storage db domain |> wrap_manip - | Ast.InsertTuple { relation; attributes } -> - (match Ops.get_relation db ~name:relation with - | None -> Error (RelationNotFound relation) - | Some rel -> - let tuple = build_tuple ~relation attributes in - match Ops.create_tuple storage db rel tuple |> wrap_manip with - | Ok (db, _rel, _hash) -> Ok db - | Error e -> Error e) + let* rel = get_rel db relation in + let tuple = build_tuple ~relation attributes in + let* (db, _, _) = Ops.create_tuple storage db rel tuple |> wrap_manip in + Ok db | Ast.InsertTuples { relation; tuples } -> - (match Ops.get_relation db ~name:relation with - | None -> Error (RelationNotFound relation) - | Some rel -> - let tuple_list = List.map (build_tuple ~relation) tuples in - match Ops.create_tuples storage db rel tuple_list |> wrap_manip with - | Ok (db, _rel, _hashes) -> Ok db - | Error e -> Error e) + let* rel = get_rel db relation in + let tuple_list = List.map (build_tuple ~relation) tuples in + let* (db, _, _) = Ops.create_tuples storage db rel tuple_list |> wrap_manip in + Ok db | Ast.DeleteTuple { relation; attributes } -> - (match Ops.get_relation db ~name:relation with - | None -> Error (RelationNotFound relation) - | Some rel -> - let tuple = build_tuple ~relation attributes in - let tuple_hash = Hashing.hash_tuple tuple in - match Ops.retract_tuple storage db rel ~tuple_hash |> wrap_manip with - | Ok (db, _rel) -> Ok db - | Error e -> Error e) + let* rel = get_rel db relation in + let tuple = build_tuple ~relation attributes in + let tuple_hash = Hashing.hash_tuple tuple in + let* (db, _) = Ops.retract_tuple storage db rel ~tuple_hash |> wrap_manip in + Ok db + + | Ast.Assign { target; body } -> + let* rel = get_rel db target in + let* result_rel = eval_query storage db body in + let* tuples = materialize_tuples storage result_rel in + let* (db, rel) = Ops.clear_relation storage db rel |> wrap_manip in + let* (db, _, _) = Ops.create_tuples storage db rel (List.map (retarget target) tuples) |> wrap_manip in + Ok db + + | Ast.InsertFrom { target; source } -> + let* rel = get_rel db target in + let* result_rel = eval_query storage db source in + let* tuples = materialize_tuples storage result_rel in + let* (db, _, _) = Ops.create_tuples storage db rel (List.map (retarget target) tuples) |> wrap_manip in + Ok db + + | Ast.DeleteWhere { target; predicate } -> + let* rel = get_rel db target in + let* pred_rel = eval_query storage db predicate in + let common = List.filter_map + (fun (n, _) -> if List.exists (fun (m, _) -> m = n) pred_rel.Relation.schema + then Some n else None) + rel.Relation.schema in + let* joined = Alg.equijoin storage common rel pred_rel |> Result.map_error wrap_alg in + let* to_delete = Alg.project storage (List.map fst rel.Relation.schema) joined + |> Result.map_error wrap_alg in + let* tuples = materialize_tuples storage to_delete in + List.fold_left (fun acc t -> + let* db = acc in + let* rel = get_rel db target in + let tuple_hash = Hashing.hash_tuple (retarget target t) in + let* (db, _) = Ops.retract_tuple storage db rel ~tuple_hash |> wrap_manip in + Ok db) + (Ok db) tuples end module Memory = Make(Management.Physical.Memory) diff --git a/lib/dml/parser.ml b/lib/dml/parser.ml index a7981c0..28f8b6c 100644 --- a/lib/dml/parser.ml +++ b/lib/dml/parser.ml @@ -1,5 +1,10 @@ type error = ParseError of string +let of_sexp sexp = + match Ast.statement_of_sexp sexp with + | stmt -> Ok stmt + | exception exn -> Error (ParseError (Printexc.to_string exn)) + let of_string s = match Sexplib.Sexp.of_string s |> Ast.statement_of_sexp with | stmt -> Ok stmt diff --git a/lib/dml/sublanguage.ml b/lib/dml/sublanguage.ml new file mode 100644 index 0000000..29f951e --- /dev/null +++ b/lib/dml/sublanguage.ml @@ -0,0 +1,23 @@ +module Make (Storage : Management.Physical.S) = struct + module Exec = Executor.Make(Storage) + + type storage = Storage.t + type ast = Ast.statement + type error = Exec.error + + let name = "dml" + + let parse_sexp sexp = + match Parser.of_sexp sexp with + | Ok r -> Ok r + | Error (Parser.ParseError s) -> Error (Exec.ParseError s) + + let execute storage db ast = + match Exec.execute storage db ast with + | Ok db -> Ok (Sublanguage.Transition (db, "updated")) + | Error e -> Error e + + let sexp_of_error = Exec.sexp_of_error +end + +module Memory = Make(Management.Physical.Memory) diff --git a/lib/drl/executor.ml b/lib/drl/executor.ml index 27f52c2..322fada 100644 --- a/lib/drl/executor.ml +++ b/lib/drl/executor.ml @@ -3,8 +3,17 @@ module Make(Storage : Management.Physical.S) = struct module Ops = Manipulation.Make(Storage) type error = + | ParseError of string | RelationNotFound of string - | AlgebraError of Algebra.error + | AlgebraError of Algebra.error + + let sexp_of_error e = + let open Sexplib.Sexp in + match e with + | ParseError s -> List [Atom "parse-error"; Atom s] + | RelationNotFound s -> List [Atom "relation-not-found"; Atom s] + | AlgebraError (Algebra.StorageError s) -> List [Atom "storage-error"; Atom s] + | AlgebraError (Algebra.GeneratorError s) -> List [Atom "generator-error"; Atom s] let wrap = Result.map_error (fun e -> AlgebraError e) diff --git a/lib/drl/gate.ml b/lib/drl/gate.ml new file mode 100644 index 0000000..222e935 --- /dev/null +++ b/lib/drl/gate.ml @@ -0,0 +1,82 @@ +(** Finiteness gate for DRL queries. + + Converts Sakura types to Coq-extracted types and calls the + verified [predicted_finite] function. Rejects queries whose + result cannot be statically proven finite. *) + +(* -- string -> char list impedance --------------------------------- *) + +let string_to_chars (s : string) : char list = + List.init (String.length s) (String.get s) + +(* -- Sakura AST -> extracted AST ----------------------------------- *) + +let rec query_of_ast : Ast.query -> Drl_verified.query = function + | Ast.Base name -> + Drl_verified.Base (string_to_chars name) + | Ast.Const pairs -> + Drl_verified.Const + (List.map + (fun (k, v) -> + (string_to_chars k, value_of_ast_value v)) + pairs) + | Ast.Select (filter, source) -> + Drl_verified.Select (query_of_ast filter, query_of_ast source) + | Ast.Join (attrs, q1, q2) -> + Drl_verified.Join + (List.map string_to_chars attrs, query_of_ast q1, query_of_ast q2) + | Ast.Cartesian (q1, q2) -> + Drl_verified.Cartesian (query_of_ast q1, query_of_ast q2) + | Ast.Project (attrs, q) -> + Drl_verified.Project (List.map string_to_chars attrs, query_of_ast q) + | Ast.Rename (renames, q) -> + Drl_verified.Rename + (List.map + (fun (o, n) -> (string_to_chars o, string_to_chars n)) + renames, + query_of_ast q) + | Ast.Union (q1, q2) -> + Drl_verified.Union (query_of_ast q1, query_of_ast q2) + | Ast.Diff (q1, q2) -> + Drl_verified.Diff (query_of_ast q1, query_of_ast q2) + | Ast.Take (n, q) -> + Drl_verified.Take (n, query_of_ast q) + +and value_of_ast_value : Ast.value -> Drl_verified.literal = function + | Ast.Int n -> Drl_verified.LitInt n + (* The Coq model has no float literal. This truncation is harmless: + the finiteness gate inspects only relation names and query structure, + never literal values. *) + | Ast.Float f -> Drl_verified.LitInt (int_of_float f) + | Ast.Str s -> Drl_verified.LitStr (string_to_chars s) + | Ast.Bool b -> Drl_verified.LitBool b + +(* -- database snapshot --------------------------------------------- *) + +let is_finite (c : Conventions.Cardinality.t) : bool = + match c with + | Conventions.Cardinality.Finite _ | Conventions.Cardinality.ConstrainedFinite -> true + | Conventions.Cardinality.AlephZero | Conventions.Cardinality.Continuum -> false + +let database_snapshot (db : Management.Database.t) : Drl_verified.database = + Management.Database.RelationMap.fold + (fun name (rel : Relation.t) acc -> + let entry : Drl_verified.relation = + { rel_name = string_to_chars name; + rel_finite = is_finite rel.cardinality } + in + (string_to_chars name, entry) :: acc) + db.relations + [] + +(* -- public interface ---------------------------------------------- *) + +let admit (db : Management.Database.t) (ast : Ast.query) : (unit, string) result = + let vdb = database_snapshot db in + let vq = query_of_ast ast in + match Drl_verified.predicted_finite vdb vq with + | Some true -> Ok () + | Some false -> + Error "query produces potentially infinite result; use Take to bound it" + | None -> + Error "referenced relation not found in finiteness check" diff --git a/lib/drl/parser.ml b/lib/drl/parser.ml index 71d694b..36ce15a 100644 --- a/lib/drl/parser.ml +++ b/lib/drl/parser.ml @@ -1,5 +1,10 @@ type error = ParseError of string +let of_sexp sexp = + match Ast.query_of_sexp sexp with + | q -> Ok q + | exception exn -> Error (ParseError (Printexc.to_string exn)) + let of_string s = match Sexplib.Sexp.of_string s |> Ast.query_of_sexp with | q -> Ok q diff --git a/lib/drl/sublanguage.ml b/lib/drl/sublanguage.ml new file mode 100644 index 0000000..f57af95 --- /dev/null +++ b/lib/drl/sublanguage.ml @@ -0,0 +1,26 @@ +module Make (Storage : Management.Physical.S) = struct + module Exec = Executor.Make(Storage) + + type storage = Storage.t + type ast = Ast.query + type error = Exec.error + + let name = "drl" + + let parse_sexp sexp = + match Parser.of_sexp sexp with + | Ok r -> Ok r + | Error (Parser.ParseError s) -> Error (Exec.ParseError s) + + let execute storage db ast = + match Gate.admit db ast with + | Error msg -> Error (Exec.ParseError msg) + | Ok () -> + match Exec.execute storage db ast with + | Ok rel -> Ok (Sublanguage.Query rel) + | Error e -> Error e + + let sexp_of_error = Exec.sexp_of_error +end + +module Memory = Make(Management.Physical.Memory) diff --git a/lib/drl_verified/drl_verified.ml b/lib/drl_verified/drl_verified.ml new file mode 100644 index 0000000..b5aeaa7 --- /dev/null +++ b/lib/drl_verified/drl_verified.ml @@ -0,0 +1,76 @@ + +(** val eqb : char list -> char list -> bool **) + +let rec eqb s1 s2 = + match s1 with + | [] -> (match s2 with + | [] -> true + | _::_ -> false) + | c1::s1' -> + (match s2 with + | [] -> false + | c2::s2' -> if (=) c1 c2 then eqb s1' s2' else false) + +type attr_name = char list + +type relation = { rel_name : char list; rel_finite : bool } + +type database = (char list * relation) list + +(** val db_lookup : char list -> database -> relation option **) + +let rec db_lookup name = function +| [] -> None +| p :: rest -> + let (n, r) = p in if eqb name n then Some r else db_lookup name rest + +type literal = +| LitInt of int +| LitStr of char list +| LitBool of bool + +type query = +| Base of char list +| Const of (attr_name * literal) list +| Select of query * query +| Join of attr_name list * query * query +| Cartesian of query * query +| Project of attr_name list * query +| Rename of (attr_name * attr_name) list * query +| Union of query * query +| Diff of query * query +| Take of int * query + +(** val predicted_finite : database -> query -> bool option **) + +let rec predicted_finite db = function +| Base name -> + (match db_lookup name db with + | Some r -> Some r.rel_finite + | None -> None) +| Select (_, source) -> predicted_finite db source +| Join (_, q1, q2) -> + (match predicted_finite db q1 with + | Some f1 -> + (match predicted_finite db q2 with + | Some f2 -> Some ((&&) f1 f2) + | None -> None) + | None -> None) +| Cartesian (q1, q2) -> + (match predicted_finite db q1 with + | Some f1 -> + (match predicted_finite db q2 with + | Some f2 -> Some ((&&) f1 f2) + | None -> None) + | None -> None) +| Project (_, q0) -> predicted_finite db q0 +| Rename (_, q0) -> predicted_finite db q0 +| Union (q1, q2) -> + (match predicted_finite db q1 with + | Some f1 -> + (match predicted_finite db q2 with + | Some f2 -> Some ((&&) f1 f2) + | None -> None) + | None -> None) +| Diff (q1, _) -> predicted_finite db q1 +| _ -> Some true diff --git a/lib/drl_verified/drl_verified.mli b/lib/drl_verified/drl_verified.mli new file mode 100644 index 0000000..31acc7a --- /dev/null +++ b/lib/drl_verified/drl_verified.mli @@ -0,0 +1,29 @@ + +val eqb : char list -> char list -> bool + +type attr_name = char list + +type relation = { rel_name : char list; rel_finite : bool } + +type database = (char list * relation) list + +val db_lookup : char list -> database -> relation option + +type literal = +| LitInt of int +| LitStr of char list +| LitBool of bool + +type query = +| Base of char list +| Const of (attr_name * literal) list +| Select of query * query +| Join of attr_name list * query * query +| Cartesian of query * query +| Project of attr_name list * query +| Rename of (attr_name * attr_name) list * query +| Union of query * query +| Diff of query * query +| Take of int * query + +val predicted_finite : database -> query -> bool option diff --git a/lib/envelope.ml b/lib/envelope.ml new file mode 100644 index 0000000..d8404d9 --- /dev/null +++ b/lib/envelope.ml @@ -0,0 +1,18 @@ +(** Envelope parser for tagged S-expressions. + + Parses commands of the form (tag payload...) where the tag selects + which sublanguage handles the payload. The tag set is open — future + sublanguages (tcl, ppl, acl) just add new tags. *) + +type tagged = { tag : string; payload : Sexplib.Sexp.t } + +let parse (input : string) : (tagged, string) Result.t = + match Sexplib.Sexp.of_string input with + | Sexplib.Sexp.List (Sexplib.Sexp.Atom tag :: rest) -> + let payload = match rest with + | [single] -> single + | many -> Sexplib.Sexp.List many + in + Ok { tag; payload } + | _ -> Error "expected (tag payload...)" + | exception exn -> Error (Printexc.to_string exn) diff --git a/lib/icl/executor.ml b/lib/icl/executor.ml index a895135..591f839 100644 --- a/lib/icl/executor.ml +++ b/lib/icl/executor.ml @@ -2,8 +2,16 @@ module Make (Storage : Management.Physical.S) = struct module Ops = Manipulation.Make(Storage) type error = + | ParseError of string | ManipulationError of Manipulation.error - | ConversionError of string + | ConversionError of string + + let sexp_of_error e = + let open Sexplib.Sexp in + match e with + | ParseError s -> List [Atom "parse-error"; Atom s] + | ManipulationError e -> Manipulation.sexp_of_error e + | ConversionError s -> List [Atom "conversion-error"; Atom s] let wrap_manip = Result.map_error (fun e -> ManipulationError e) diff --git a/lib/icl/parser.ml b/lib/icl/parser.ml index a7981c0..28f8b6c 100644 --- a/lib/icl/parser.ml +++ b/lib/icl/parser.ml @@ -1,5 +1,10 @@ type error = ParseError of string +let of_sexp sexp = + match Ast.statement_of_sexp sexp with + | stmt -> Ok stmt + | exception exn -> Error (ParseError (Printexc.to_string exn)) + let of_string s = match Sexplib.Sexp.of_string s |> Ast.statement_of_sexp with | stmt -> Ok stmt diff --git a/lib/icl/sublanguage.ml b/lib/icl/sublanguage.ml new file mode 100644 index 0000000..4e74082 --- /dev/null +++ b/lib/icl/sublanguage.ml @@ -0,0 +1,23 @@ +module Make (Storage : Management.Physical.S) = struct + module Exec = Executor.Make(Storage) + + type storage = Storage.t + type ast = Ast.statement + type error = Exec.error + + let name = "icl" + + let parse_sexp sexp = + match Parser.of_sexp sexp with + | Ok r -> Ok r + | Error (Parser.ParseError s) -> Error (Exec.ParseError s) + + let execute storage db ast = + match Exec.execute storage db ast with + | Ok (db, msg) -> Ok (Sublanguage.Transition (db, msg)) + | Error e -> Error e + + let sexp_of_error = Exec.sexp_of_error +end + +module Memory = Make(Management.Physical.Memory) diff --git a/lib/manipulation.ml b/lib/manipulation.ml index 73607fa..be77c02 100644 --- a/lib/manipulation.ml +++ b/lib/manipulation.ml @@ -23,6 +23,24 @@ type error = | ConstraintViolation of string | StorageError of string +let string_of_error = function + | RelationNotFound s -> "RelationNotFound: " ^ s + | RelationAlreadyExists s -> "RelationAlreadyExists: " ^ s + | TupleNotFound h -> "TupleNotFound: " ^ h + | DuplicateTuple h -> "DuplicateTuple: " ^ h + | ConstraintViolation s -> "ConstraintViolation: " ^ s + | StorageError s -> "StorageError: " ^ s + +let sexp_of_error e = + let open Sexplib.Sexp in + match e with + | RelationNotFound s -> List [Atom "relation-not-found"; Atom s] + | RelationAlreadyExists s -> List [Atom "relation-already-exists"; Atom s] + | TupleNotFound h -> List [Atom "tuple-not-found"; Atom h] + | DuplicateTuple h -> List [Atom "duplicate-tuple"; Atom h] + | ConstraintViolation s -> List [Atom "constraint-violation"; Atom s] + | StorageError s -> List [Atom "storage-error"; Atom s] + (** Result type for operations *) type 'a result = ('a, error) Result.t diff --git a/lib/sublanguage.ml b/lib/sublanguage.ml new file mode 100644 index 0000000..3df91f1 --- /dev/null +++ b/lib/sublanguage.ml @@ -0,0 +1,29 @@ +(** Effect classification for sublanguage operations. + + Categorically: + - Query: a natural transformation between instance functors (DRL). + Side-effect-free; the database state is unchanged. + - Transition: a morphism in the category of database states (DDL, + DML, ICL, DCL, and future TCL). Produces a new state via + substitution (Harper, PFPL ch. 3-4). + + Future sublanguages: + - TCL -> Transition (transaction boundaries are state morphisms + with atomicity constraints) + - PPL -> new effect class: potentially non-terminating computation + (Turing-complete; breaks the termination guarantee of DRL) + - ACL -> a functor restriction: narrows the admissible natural + transformations based on authorization context *) +type result = + | Query of Relation.t + | Transition of Management.Database.t * string + +module type S = sig + type storage + type ast + type error + val name : string + val parse_sexp : Sexplib.Sexp.t -> (ast, error) Result.t + val execute : storage -> Management.Database.t -> ast -> (result, error) Result.t + val sexp_of_error : error -> Sexplib.Sexp.t +end diff --git a/proof/.gitignore b/proof/.gitignore new file mode 100644 index 0000000..5ff7fe7 --- /dev/null +++ b/proof/.gitignore @@ -0,0 +1,11 @@ +# Coq build artifacts +*.vo +*.vos +*.vok +*.glob +*.aux +.*.aux +Makefile.coq +Makefile.coq.conf +.Makefile.coq.d +.coqdeps.d diff --git a/proof/Drl.v b/proof/Drl.v new file mode 100644 index 0000000..fd179a1 --- /dev/null +++ b/proof/Drl.v @@ -0,0 +1,67 @@ +(** * DRL: Data Retrieval Language — Finiteness Gate + + This file defines: + - The DRL query AST (mirroring [lib/drl/ast.ml]) + - [predicted_finite]: statically decides whether a query can + produce an infinite result based on the cardinality flags of + the relations it references. + + [predicted_finite] is extracted to OCaml and called by + [lib/drl/gate.ml] before every query execution. Queries whose + result cannot be statically proven finite are rejected unless + wrapped in a [Take]. *) + +From Stdlib Require Import List. +From Stdlib Require Import String. +From Stdlib Require Import Bool. +Require Import Schema. +Require Import Relation. +Import ListNotations. + +(* ================================================================== *) +(** ** AST *) +(* ================================================================== *) + +Inductive literal := + | LitInt : nat -> literal + | LitStr : string -> literal + | LitBool : bool -> literal. + +Inductive query : Type := + | Base : string -> query + | Const : list (attr_name * literal) -> query + | Select : query -> query -> query + | Join : list attr_name -> query -> query -> query + | Cartesian : query -> query -> query + | Project : list attr_name -> query -> query + | Rename : list (attr_name * attr_name) -> query -> query + | Union : query -> query -> query + | Diff : query -> query -> query + | Take : nat -> query -> query. + +(* ================================================================== *) +(** ** Finiteness Prediction *) +(* ================================================================== *) + +(** Conservatively predict whether a query produces a finite result. + Returns [Some true] if guaranteed finite, [Some false] if not, + [None] if a referenced relation is not found in the database. *) +Fixpoint predicted_finite (db : database) (q : query) : option bool := + match q with + | Base name => + match db_lookup name db with + | Some r => Some (rel_finite r) + | None => None + end + | Const _ => Some true + | Take _ _ => Some true + | Select _ source => + predicted_finite db source + | Join _ q1 q2 | Cartesian q1 q2 | Union q1 q2 => + match predicted_finite db q1, predicted_finite db q2 with + | Some f1, Some f2 => Some (f1 && f2) + | _, _ => None + end + | Diff q1 _ => predicted_finite db q1 + | Project _ q' | Rename _ q' => predicted_finite db q' + end. diff --git a/proof/Extraction.v b/proof/Extraction.v new file mode 100644 index 0000000..dc93c21 --- /dev/null +++ b/proof/Extraction.v @@ -0,0 +1,17 @@ +(** * Extraction to OCaml — finiteness gate only + + Extracts [predicted_finite] to [lib/drl_verified/drl_verified.ml]. + To regenerate: cd proof && make *) + +From Stdlib Require Import Extraction. +From Stdlib Require Import ExtrOcamlBasic. +From Stdlib Require Import ExtrOcamlString. +From Stdlib Require Import ExtrOcamlNatInt. + +Require Import Schema. +Require Import Relation. +Require Import Drl. + +Set Extraction Output Directory "../lib/drl_verified". + +Extraction "drl_verified" predicted_finite. diff --git a/proof/Makefile b/proof/Makefile new file mode 100644 index 0000000..a9e1f72 --- /dev/null +++ b/proof/Makefile @@ -0,0 +1,14 @@ +COQMAKEFILE ?= Makefile.coq + +all: $(COQMAKEFILE) + mkdir -p ../lib/drl_verified + $(MAKE) -f $(COQMAKEFILE) + +$(COQMAKEFILE): _CoqProject + coq_makefile -f _CoqProject -o $(COQMAKEFILE) + +clean: $(COQMAKEFILE) + $(MAKE) -f $(COQMAKEFILE) clean + rm -f $(COQMAKEFILE) $(COQMAKEFILE).conf + +.PHONY: all clean diff --git a/proof/Relation.v b/proof/Relation.v new file mode 100644 index 0000000..f7c087d --- /dev/null +++ b/proof/Relation.v @@ -0,0 +1,26 @@ +(** * Relation: minimal model for finiteness checking + + A relation is reduced to the two fields that [predicted_finite] + actually inspects: its name (for database lookup) and its + finiteness flag (for the gate decision). *) + +From Stdlib Require Import List. +From Stdlib Require Import String. +Require Import Schema. +Import ListNotations. + +Record relation := mkRelation { + rel_name : string; + rel_finite : bool; +}. + +(** A database is a named collection of relations. *) +Definition database := list (string * relation). + +(** Look up a relation by name. *) +Fixpoint db_lookup (name : string) (db : database) : option relation := + match db with + | [] => None + | (n, r) :: rest => + if String.eqb name n then Some r else db_lookup name rest + end. diff --git a/proof/Schema.v b/proof/Schema.v new file mode 100644 index 0000000..eb8f4c5 --- /dev/null +++ b/proof/Schema.v @@ -0,0 +1,5 @@ +(** * Schema: attribute name type *) + +From Stdlib Require Import String. + +Definition attr_name := string. diff --git a/proof/_CoqProject b/proof/_CoqProject new file mode 100644 index 0000000..0e6123e --- /dev/null +++ b/proof/_CoqProject @@ -0,0 +1,6 @@ +-R . Sakura + +Schema.v +Relation.v +Drl.v +Extraction.v diff --git a/proof/drl_verified.ml b/proof/drl_verified.ml new file mode 100644 index 0000000..f4c282a --- /dev/null +++ b/proof/drl_verified.ml @@ -0,0 +1,410 @@ + +(** val negb : bool -> bool **) + +let negb = function +| true -> false +| false -> true + +(** val fst : ('a1 * 'a2) -> 'a1 **) + +let fst = function +| (x, _) -> x + +(** val snd : ('a1 * 'a2) -> 'a2 **) + +let snd = function +| (_, y) -> y + +(** val app : 'a1 list -> 'a1 list -> 'a1 list **) + +let rec app l m = + match l with + | [] -> m + | a :: l1 -> a :: (app l1 m) + +(** val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **) + +let rec map f = function +| [] -> [] +| a :: l0 -> (f a) :: (map f l0) + +(** val firstn : int -> 'a1 list -> 'a1 list **) + +let rec firstn n l = + (fun fO fS n -> if n=0 then fO () else fS (n-1)) + (fun _ -> []) + (fun n0 -> match l with + | [] -> [] + | a :: l0 -> a :: (firstn n0 l0)) + n + +(** val flat_map : ('a1 -> 'a2 list) -> 'a1 list -> 'a2 list **) + +let rec flat_map f = function +| [] -> [] +| x :: l0 -> app (f x) (flat_map f l0) + +(** val existsb : ('a1 -> bool) -> 'a1 list -> bool **) + +let rec existsb f = function +| [] -> false +| a :: l0 -> (||) (f a) (existsb f l0) + +(** val forallb : ('a1 -> bool) -> 'a1 list -> bool **) + +let rec forallb f = function +| [] -> true +| a :: l0 -> (&&) (f a) (forallb f l0) + +(** val filter : ('a1 -> bool) -> 'a1 list -> 'a1 list **) + +let rec filter f = function +| [] -> [] +| x :: l0 -> if f x then x :: (filter f l0) else filter f l0 + +(** val find : ('a1 -> bool) -> 'a1 list -> 'a1 option **) + +let rec find f = function +| [] -> None +| x :: tl -> if f x then Some x else find f tl + +(** val eqb : char list -> char list -> bool **) + +let rec eqb s1 s2 = + match s1 with + | [] -> (match s2 with + | [] -> true + | _::_ -> false) + | c1::s1' -> + (match s2 with + | [] -> false + | c2::s2' -> if (=) c1 c2 then eqb s1' s2' else false) + +(** val append : char list -> char list -> char list **) + +let rec append s1 s2 = + match s1 with + | [] -> s2 + | c::s1' -> c::(append s1' s2) + +type attr_name = char list + +type domain_name = char list + +type schema = (attr_name * domain_name) list + +(** val has_attr : attr_name -> schema -> bool **) + +let has_attr a s = + existsb (fun p -> eqb a (fst p)) s + +(** val attr_names : schema -> attr_name list **) + +let attr_names s = + map fst s + +(** val filter_schema : attr_name list -> schema -> schema **) + +let filter_schema attrs s = + filter (fun p -> existsb (eqb (fst p)) attrs) s + +(** val merge_schema : schema -> schema -> schema **) + +let merge_schema s1 s2 = + app s1 (filter (fun p -> negb (has_attr (fst p) s1)) s2) + +(** val remove_attrs : attr_name list -> schema -> schema **) + +let remove_attrs attrs s = + filter (fun p -> negb (existsb (eqb (fst p)) attrs)) s + +(** val rename_in_schema : + (attr_name * attr_name) list -> schema -> schema **) + +let rename_in_schema renames s = + map (fun p -> + let a = fst p in + let d = snd p in + (match find (fun r -> eqb a (fst r)) renames with + | Some p0 -> let (_, a') = p0 in (a', d) + | None -> (a, d))) + s + +type value (* AXIOM TO BE REALIZED *) + +(** val value_eqb : value -> value -> bool **) + +let value_eqb = + failwith "AXIOM TO BE REALIZED (Sakura.Relation.value_eqb)" + +type tuple = (attr_name * value) list + +(** val tuple_lookup : attr_name -> tuple -> value option **) + +let rec tuple_lookup a = function +| [] -> None +| p :: rest -> + let (a', v) = p in if eqb a a' then Some v else tuple_lookup a rest + +(** val project_tuple : attr_name list -> tuple -> tuple **) + +let project_tuple attrs t = + filter (fun p -> existsb (eqb (fst p)) attrs) t + +(** val rename_tuple : (attr_name * attr_name) list -> tuple -> tuple **) + +let rename_tuple renames t = + map (fun p -> + let a = fst p in + let v = snd p in + (match find (fun r -> eqb a (fst r)) renames with + | Some p0 -> let (_, a') = p0 in (a', v) + | None -> (a, v))) + t + +(** val merge_tuples : tuple -> tuple -> tuple **) + +let merge_tuples t1 t2 = + app t1 (filter (fun p -> negb (existsb (eqb (fst p)) (map fst t1))) t2) + +(** val tuples_agree_on : attr_name list -> tuple -> tuple -> bool **) + +let tuples_agree_on attrs t1 t2 = + forallb (fun a -> + match tuple_lookup a t1 with + | Some v1 -> + (match tuple_lookup a t2 with + | Some v2 -> value_eqb v1 v2 + | None -> false) + | None -> (match tuple_lookup a t2 with + | Some _ -> false + | None -> true)) + attrs + +type relation = { rel_name : char list; rel_schema : schema; + rel_tuples : tuple list } + +type database = (char list * relation) list + +(** val db_lookup : char list -> database -> relation option **) + +let rec db_lookup name = function +| [] -> None +| p :: rest -> + let (n, r) = p in if eqb name n then Some r else db_lookup name rest + +type literal = +| LitInt of int +| LitStr of char list +| LitBool of bool + +type query = +| Base of char list +| Const of (attr_name * literal) list +| Select of query * query +| Join of attr_name list * query * query +| Cartesian of query * query +| Project of attr_name list * query +| Rename of (attr_name * attr_name) list * query +| Union of query * query +| Diff of query * query +| Take of int * query + +(** val predicted_schema : database -> query -> schema option **) + +let rec predicted_schema db = function +| Base name -> + (match db_lookup name db with + | Some r -> Some r.rel_schema + | None -> None) +| Const pairs -> + Some + (map (fun p -> ((fst p), + ('a'::('b'::('s'::('t'::('r'::('a'::('c'::('t'::[])))))))))) pairs) +| Select (_, source) -> predicted_schema db source +| Join (attrs, q1, q2) -> + (match predicted_schema db q1 with + | Some s1 -> + (match predicted_schema db q2 with + | Some s2 -> + Some + (merge_schema s1 + (remove_attrs (attr_names s1) (remove_attrs attrs s2))) + | None -> None) + | None -> None) +| Cartesian (q1, q2) -> + (match predicted_schema db q1 with + | Some s1 -> + (match predicted_schema db q2 with + | Some s2 -> Some (merge_schema s1 s2) + | None -> None) + | None -> None) +| Project (attrs, q') -> + (match predicted_schema db q' with + | Some s -> Some (filter_schema attrs s) + | None -> None) +| Rename (renames, q') -> + (match predicted_schema db q' with + | Some s -> Some (rename_in_schema renames s) + | None -> None) +| Union (q1, _) -> predicted_schema db q1 +| Diff (q1, _) -> predicted_schema db q1 +| Take (_, q') -> predicted_schema db q' + +(** val literal_to_value : literal -> value **) + +let literal_to_value = + failwith "AXIOM TO BE REALIZED (Sakura.Drl.literal_to_value)" + +(** val eval_const : (attr_name * literal) list -> relation **) + +let eval_const pairs = + let tuple0 = map (fun p -> ((fst p), (literal_to_value (snd p)))) pairs in + let sch = + map (fun p -> ((fst p), + ('a'::('b'::('s'::('t'::('r'::('a'::('c'::('t'::[])))))))))) pairs + in + { rel_name = ('c'::('o'::('n'::('s'::('t'::[]))))); rel_schema = sch; + rel_tuples = (tuple0 :: []) } + +(** val semijoin : relation -> relation -> relation **) + +let semijoin filter_rel source = + let common = + filter (fun a -> has_attr a filter_rel.rel_schema) + (attr_names source.rel_schema) + in + let matches = fun t -> + existsb (fun ft -> tuples_agree_on common t ft) filter_rel.rel_tuples + in + { rel_name = source.rel_name; rel_schema = source.rel_schema; rel_tuples = + (filter matches source.rel_tuples) } + +(** val equijoin : attr_name list -> relation -> relation -> relation **) + +let equijoin attrs left right = + let joined = + flat_map (fun lt -> + flat_map (fun rt -> + if tuples_agree_on attrs lt rt then (merge_tuples lt rt) :: [] else []) + right.rel_tuples) + left.rel_tuples + in + let new_schema = + merge_schema left.rel_schema + (remove_attrs (attr_names left.rel_schema) + (remove_attrs attrs right.rel_schema)) + in + { rel_name = + (append ('j'::('o'::('i'::('n'::('_'::[]))))) + (append left.rel_name (append ('_'::[]) right.rel_name))); + rel_schema = new_schema; rel_tuples = joined } + +(** val cartesian : relation -> relation -> relation **) + +let cartesian left right = + let joined = + flat_map (fun lt -> map (fun rt -> merge_tuples lt rt) right.rel_tuples) + left.rel_tuples + in + { rel_name = + (append ('c'::('a'::('r'::('t'::('_'::[]))))) + (append left.rel_name (append ('_'::[]) right.rel_name))); + rel_schema = (merge_schema left.rel_schema right.rel_schema); rel_tuples = + joined } + +(** val project : attr_name list -> relation -> relation **) + +let project attrs r = + { rel_name = (append ('p'::('r'::('o'::('j'::('_'::[]))))) r.rel_name); + rel_schema = (filter_schema attrs r.rel_schema); rel_tuples = + (map (project_tuple attrs) r.rel_tuples) } + +(** val rename : (attr_name * attr_name) list -> relation -> relation **) + +let rename renames r = + { rel_name = + (append ('r'::('e'::('n'::('a'::('m'::('e'::('_'::[]))))))) r.rel_name); + rel_schema = (rename_in_schema renames r.rel_schema); rel_tuples = + (map (rename_tuple renames) r.rel_tuples) } + +(** val rel_union : relation -> relation -> relation **) + +let rel_union r1 r2 = + { rel_name = + (append ('u'::('n'::('i'::('o'::('n'::('_'::[])))))) + (append r1.rel_name (append ('_'::[]) r2.rel_name))); + rel_schema = r1.rel_schema; rel_tuples = + (app r1.rel_tuples r2.rel_tuples) } + +(** val rel_diff : relation -> relation -> relation **) + +let rel_diff r1 r2 = + let in_r2 = fun t -> + existsb (fun t2 -> tuples_agree_on (attr_names r1.rel_schema) t t2) + r2.rel_tuples + in + { rel_name = + (append ('d'::('i'::('f'::('f'::('_'::[]))))) + (append r1.rel_name (append ('_'::[]) r2.rel_name))); + rel_schema = r1.rel_schema; rel_tuples = + (filter (fun t -> negb (in_r2 t)) r1.rel_tuples) } + +(** val take : int -> relation -> relation **) + +let take n r = + { rel_name = (append ('t'::('a'::('k'::('e'::('_'::[]))))) r.rel_name); + rel_schema = r.rel_schema; rel_tuples = (firstn n r.rel_tuples) } + +(** val eval : database -> query -> relation option **) + +let rec eval db = function +| Base name -> db_lookup name db +| Const pairs -> Some (eval_const pairs) +| Select (filter_q, source_q) -> + (match eval db filter_q with + | Some filter_rel -> + (match eval db source_q with + | Some source_rel -> Some (semijoin filter_rel source_rel) + | None -> None) + | None -> None) +| Join (attrs, q1, q2) -> + (match eval db q1 with + | Some r1 -> + (match eval db q2 with + | Some r2 -> Some (equijoin attrs r1 r2) + | None -> None) + | None -> None) +| Cartesian (q1, q2) -> + (match eval db q1 with + | Some r1 -> + (match eval db q2 with + | Some r2 -> Some (cartesian r1 r2) + | None -> None) + | None -> None) +| Project (attrs, q') -> + (match eval db q' with + | Some r -> Some (project attrs r) + | None -> None) +| Rename (renames, q') -> + (match eval db q' with + | Some r -> Some (rename renames r) + | None -> None) +| Union (q1, q2) -> + (match eval db q1 with + | Some r1 -> + (match eval db q2 with + | Some r2 -> Some (rel_union r1 r2) + | None -> None) + | None -> None) +| Diff (q1, q2) -> + (match eval db q1 with + | Some r1 -> + (match eval db q2 with + | Some r2 -> Some (rel_diff r1 r2) + | None -> None) + | None -> None) +| Take (n, q') -> + (match eval db q' with + | Some r -> Some (take n r) + | None -> None) diff --git a/test/test_relational_engine.ml b/test/test_relational_engine.ml index 2b902e1..963337f 100644 --- a/test/test_relational_engine.ml +++ b/test/test_relational_engine.ml @@ -2391,20 +2391,20 @@ let%test_unit "constraint propagation: project filters constraints" = (* Parse tests use canonical flat sexp format: (Constructor (field val) ...) *) -let%test_unit "dml: parse CreateDatabase" = - match Dml.Parser.of_string {|(CreateDatabase "shop")|} with +let%test_unit "ddl: parse CreateDatabase" = + match Ddl.Parser.of_string {|(CreateDatabase "shop")|} with | Error _ -> assert false - | Ok stmt -> assert (stmt = Dml.Ast.CreateDatabase "shop") + | Ok stmt -> assert (stmt = Ddl.Ast.CreateDatabase "shop") -let%test_unit "dml: parse RetractRelation" = - match Dml.Parser.of_string {|(RetractRelation "users")|} with +let%test_unit "ddl: parse RetractRelation" = + match Ddl.Parser.of_string {|(RetractRelation "users")|} with | Error _ -> assert false - | Ok stmt -> assert (stmt = Dml.Ast.RetractRelation "users") + | Ok stmt -> assert (stmt = Ddl.Ast.RetractRelation "users") -let%test_unit "dml: parse ClearRelation" = - match Dml.Parser.of_string {|(ClearRelation "users")|} with +let%test_unit "ddl: parse ClearRelation" = + match Ddl.Parser.of_string {|(ClearRelation "users")|} with | Error _ -> assert false - | Ok stmt -> assert (stmt = Dml.Ast.ClearRelation "users") + | Ok stmt -> assert (stmt = Ddl.Ast.ClearRelation "users") let%test_unit "dml: round-trip InsertTuple" = let src = Dml.Ast.InsertTuple { @@ -2415,12 +2415,12 @@ let%test_unit "dml: round-trip InsertTuple" = | Error _ -> assert false | Ok parsed -> assert (parsed = src) -let%test_unit "dml: round-trip CreateRelation" = - let src = Dml.Ast.CreateRelation { +let%test_unit "ddl: round-trip CreateRelation" = + let src = Ddl.Ast.CreateRelation { name = "users"; schema = [("name", "string"); ("age", "natural")] } in - match Dml.Parser.of_string (Dml.Parser.to_string src) with + match Ddl.Parser.of_string (Ddl.Parser.to_string src) with | Error _ -> assert false | Ok parsed -> assert (parsed = src) @@ -2436,31 +2436,31 @@ let%test_unit "dml: round-trip InsertTuples" = | Error _ -> assert false | Ok parsed -> assert (parsed = src) -let%test_unit "dml: round-trip RegisterDomain" = - let src = Dml.Ast.RegisterDomain { name = "money"; cardinality = Dml.Ast.AlephZero } in - match Dml.Parser.of_string (Dml.Parser.to_string src) with +let%test_unit "ddl: round-trip RegisterDomain" = + let src = Ddl.Ast.RegisterDomain { name = "money"; cardinality = Ddl.Ast.AlephZero } in + match Ddl.Parser.of_string (Ddl.Parser.to_string src) with | Error _ -> assert false | Ok parsed -> assert (parsed = src) (* Executor tests construct AST directly — no dependency on sexp format *) -let%test_unit "dml: execute CreateDatabase" = +let%test_unit "ddl: execute CreateDatabase" = with_storage (fun storage -> let db = Management.Database.empty ~name:"" in - let stmt = Dml.Ast.CreateDatabase "shop" in - match Dml.Executor.Memory.execute storage db stmt with + let stmt = Ddl.Ast.CreateDatabase "shop" in + match Ddl.Executor.Memory.execute storage db stmt with | Error _ -> assert false - | Ok db -> assert (db.name = "shop")) + | Ok (db, _msg) -> assert (db.name = "shop")) -let%test_unit "dml: execute CreateRelation" = +let%test_unit "ddl: execute CreateRelation" = with_storage (fun storage -> let db = match Manipulation.Memory.create_database storage ~name:"shop" with | Error _ -> assert false | Ok db -> db in - let stmt = Dml.Ast.CreateRelation { name = "users"; schema = [("name", "string"); ("age", "natural")] } in - match Dml.Executor.Memory.execute storage db stmt with + let stmt = Ddl.Ast.CreateRelation { name = "users"; schema = [("name", "string"); ("age", "natural")] } in + match Ddl.Executor.Memory.execute storage db stmt with | Error _ -> assert false - | Ok db -> assert (Management.Database.has_relation db "users")) + | Ok (db, _msg) -> assert (Management.Database.has_relation db "users")) let%test_unit "dml: execute InsertTuple" = with_storage (fun storage -> @@ -2523,7 +2523,7 @@ let%test_unit "dml: execute DeleteTuple" = in assert (Manipulation.Memory.tuple_count rel = 0)) -let%test_unit "dml: execute RetractRelation" = +let%test_unit "ddl: execute RetractRelation" = with_storage (fun storage -> let db = match Manipulation.Memory.create_database storage ~name:"shop" with | Error _ -> assert false | Ok db -> db @@ -2532,11 +2532,11 @@ let%test_unit "dml: execute RetractRelation" = let db = match Manipulation.Memory.create_relation storage db ~name:"users" ~schema with | Error _ -> assert false | Ok (db, _) -> db in - match Dml.Executor.Memory.execute storage db (Dml.Ast.RetractRelation "users") with + match Ddl.Executor.Memory.execute storage db (Ddl.Ast.RetractRelation "users") with | Error _ -> assert false - | Ok db -> assert (not (Management.Database.has_relation db "users"))) + | Ok (db, _msg) -> assert (not (Management.Database.has_relation db "users"))) -let%test_unit "dml: execute ClearRelation" = +let%test_unit "ddl: execute ClearRelation" = with_storage (fun storage -> let db = match Manipulation.Memory.create_database storage ~name:"shop" with | Error _ -> assert false | Ok db -> db @@ -2550,23 +2550,23 @@ let%test_unit "dml: execute ClearRelation" = tuples = [[("name", Drl.Ast.Str "Alice")]; [("name", Drl.Ast.Str "Bob")]] }) with | Error _ -> assert false | Ok db -> db in - match Dml.Executor.Memory.execute storage db (Dml.Ast.ClearRelation "users") with + match Ddl.Executor.Memory.execute storage db (Ddl.Ast.ClearRelation "users") with | Error _ -> assert false - | Ok db -> + | Ok (db, _msg) -> let rel = match Management.Database.get_relation db "users" with | None -> assert false | Some r -> r in assert (Manipulation.Memory.tuple_count rel = 0)) -let%test_unit "dml: execute RegisterDomain" = +let%test_unit "ddl: execute RegisterDomain" = with_storage (fun storage -> let db = match Manipulation.Memory.create_database storage ~name:"shop" with | Error _ -> assert false | Ok db -> db in - let stmt = Dml.Ast.RegisterDomain { name = "money"; cardinality = Dml.Ast.AlephZero } in - match Dml.Executor.Memory.execute storage db stmt with + let stmt = Ddl.Ast.RegisterDomain { name = "money"; cardinality = Ddl.Ast.AlephZero } in + match Ddl.Executor.Memory.execute storage db stmt with | Error _ -> assert false - | Ok db -> assert (Management.Database.has_domain db "money")) + | Ok (db, _msg) -> assert (Management.Database.has_domain db "money")) let%test_unit "dml: insert into nonexistent relation returns error" = with_storage (fun storage -> |