aboutsummaryrefslogtreecommitdiffstats
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/dbms_language.ml39
-rw-r--r--lib/dcl/executor.ml20
-rw-r--r--lib/dcl/parser.ml7
-rw-r--r--lib/dcl/sublanguage.ml23
-rw-r--r--lib/ddl/ast.ml16
-rw-r--r--lib/ddl/executor.ml68
-rw-r--r--lib/ddl/parser.ml14
-rw-r--r--lib/ddl/sublanguage.ml23
-rw-r--r--lib/dml/ast.ml15
-rw-r--r--lib/dml/executor.ml150
-rw-r--r--lib/dml/parser.ml5
-rw-r--r--lib/dml/sublanguage.ml23
-rw-r--r--lib/drl/executor.ml11
-rw-r--r--lib/drl/gate.ml82
-rw-r--r--lib/drl/parser.ml5
-rw-r--r--lib/drl/sublanguage.ml26
-rw-r--r--lib/drl_verified/drl_verified.ml76
-rw-r--r--lib/drl_verified/drl_verified.mli29
-rw-r--r--lib/envelope.ml18
-rw-r--r--lib/icl/executor.ml10
-rw-r--r--lib/icl/parser.ml5
-rw-r--r--lib/icl/sublanguage.ml23
-rw-r--r--lib/manipulation.ml18
-rw-r--r--lib/sublanguage.ml29
24 files changed, 640 insertions, 95 deletions
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-11-04 02:41:51 +0000