4 files changed, 123 insertions, 1 deletions

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)