Multigroup unified reference for hierarchical access

5 files changed, 9 insertions, 181 deletions

diff --git a/lib/drl/executor.ml b/lib/drl/executor.ml
index 1172553..41bdde5 100644
--- a/lib/drl/executor.ml
+++ b/lib/drl/executor.ml
@@ -24,22 +24,22 @@ module Make (Storage : Management.Physical.S) = struct
     let common =
       List.filter_map
         (fun (n, _) ->
-          if List.exists (fun (m, _) -> m = n) filter.Relation.schema then
+          if List.exists (fun (m, _) -> m = n) filter#schema then
             Some n
           else None)
-        source.Relation.schema
+        source#schema
     in
-    let source_attrs = List.map fst source.Relation.schema in
+    let source_attrs = List.map fst source#schema in
     Result.bind
       (wrap (Alg.equijoin storage common source filter))
       (fun joined -> wrap (Alg.project storage source_attrs joined))
 
-  let rec execute (storage : Storage.t) (db : Management.Database.t)
-      (q : Ast.query) : (Relation.t, error) Result.t =
+  let rec execute (storage : Storage.t) (db : Management.Multigroup.multigroup)
+      (q : Ast.query) : (Relation.ephemeral, error) Result.t =
     let ( >>= ) = Result.bind in
     match q with
     | Ast.Base name -> (
-        match Ops.get_relation db ~name with
+        match Ops.get_relation db name with
         | None -> Error (RelationNotFound name)
         | Some rel -> Ok rel)
     | Ast.Const pairs ->
diff --git a/lib/drl/gate.ml b/lib/drl/gate.ml
deleted file mode 100644
index a314bce..0000000
--- a/lib/drl/gate.ml
+++ /dev/null
@@ -1,79 +0,0 @@
-(** 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/sublanguage.ml b/lib/drl/sublanguage.ml
index 29047c3..f47129f 100644
--- a/lib/drl/sublanguage.ml
+++ b/lib/drl/sublanguage.ml
@@ -15,12 +15,9 @@ module Make (Storage : Management.Physical.S) = struct
     | 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_types.Query rel)
-        | Error e -> Error e)
+    match Exec.execute storage db ast with
+    | Ok rel -> Ok (Sublanguage_types.Query (rel :> Relation.relation))
+    | Error e -> Error e
 
   let sexp_of_error = Exec.sexp_of_error
 end
diff --git a/lib/drl_verified/drl_verified.ml b/lib/drl_verified/drl_verified.ml
deleted file mode 100644
index 868af2a..0000000
--- a/lib/drl_verified/drl_verified.ml
+++ /dev/null
@@ -1,67 +0,0 @@
-(** 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
deleted file mode 100644
index dac930e..0000000
--- a/lib/drl_verified/drl_verified.mli
+++ /dev/null
@@ -1,23 +0,0 @@
-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