Sublanguages improvement & Coq experiment (#53)

* separation and functor for sublanguages

* add coq experiment for termination

* fix tests with envelopes

* add timestamp and print responses to server on terminal

* remove coq experiment for trivial cases and rework gate

* refactor nesting with let*

* remove non-envelope sublang support and tests on server

* manip_err duplication purge and better format as s-expr

* abstract storage with dispatch for sublanguages

* dead code and minor refactor due to old non-envelope parsing on subl

* refactor server to use proper dml alg error and wire ephem relations

* remove (schema)

* change .gitignore to blacklist folders

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