5 files changed, 116 insertions, 124 deletions

diff --git a/lib/drl/ast.ml b/lib/drl/ast.ml
index 2beb010..6b191bb 100644
--- a/lib/drl/ast.ml
+++ b/lib/drl/ast.ml
@@ -1,32 +1,28 @@
 open Sexplib.Std
 
 (** Literal values for Const nodes *)
-type value =
-  | Int   of int
-  | Float of float
-  | Str   of string
-  | Bool  of bool
+type value = Int of int | Float of float | Str of string | Bool of bool
 [@@deriving sexp]
 
 (** Convert an AST value to an AbstractValue.t (Obj.t) via Obj.repr *)
 let value_to_abstract : value -> Conventions.AbstractValue.t = function
-  | Int n   -> Obj.repr n
+  | Int n -> Obj.repr n
   | Float f -> Obj.repr f
-  | Str s   -> Obj.repr s
-  | Bool b  -> Obj.repr b
+  | Str s -> Obj.repr s
+  | Bool b -> Obj.repr b
 
-type direction = Asc | Desc
-[@@deriving sexp]
+type direction = Asc | Desc [@@deriving sexp]
 
 type query =
-  | Base    of string                          (** base relation by name *)
-  | Const   of (string * value) list           (** constant single-tuple relation *)
-  | Select  of query * query                   (** σ semijoin: (filter, source) *)
-  | Join    of string list * query * query     (** ⋈ natural equijoin on named attrs *)
-  | Cartesian of query * query                 (** × Cartesian product *)
-  | Project of string list * query             (** π restrict columns *)
-  | Rename  of (string * string) list * query  (** ρ rename (old,new) pairs *)
-  | Union   of query * query                   (** ∪ — compatible schemas assumed *)
-  | Diff    of query * query                   (** − *)
-  | Take    of int * query                     (** τ *)
+  | Base of string  (** base relation by name *)
+  | Const of (string * value) list  (** constant single-tuple relation *)
+  | Select of query * query  (** σ semijoin: (filter, source) *)
+  | Join of string list * query * query
+      (** ⋈ natural equijoin on named attrs *)
+  | Cartesian of query * query  (** × Cartesian product *)
+  | Project of string list * query  (** π restrict columns *)
+  | Rename of (string * string) list * query  (** ρ rename (old,new) pairs *)
+  | Union of query * query  (** ∪ — compatible schemas assumed *)
+  | Diff of query * query  (** − *)
+  | Take of int * query  (** τ *)
 [@@deriving sexp]
diff --git a/lib/drl/executor.ml b/lib/drl/executor.ml
index 322fada..f1732eb 100644
--- a/lib/drl/executor.ml
+++ b/lib/drl/executor.ml
@@ -1,74 +1,74 @@
-module Make(Storage : Management.Physical.S) = struct
-  module Alg = Algebra.Make(Storage)
-  module Ops = Manipulation.Make(Storage)
+module Make (Storage : Management.Physical.S) = struct
+  module Alg = Algebra.Make (Storage)
+  module Ops = Manipulation.Make (Storage)
 
   type error =
-    | ParseError       of string
+    | 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]
+    | 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)
-
   let ast_value_to_abstract = Ast.value_to_abstract
 
-  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.Database.t)
+      (q : Ast.query) : (Relation.t, error) Result.t =
     let ( >>= ) = Result.bind in
     match q with
-    | Ast.Base name ->
-      (match Ops.get_relation db ~name with
-       | None     -> Error (RelationNotFound name)
-       | Some rel -> Ok rel)
+    | Ast.Base name -> (
+        match Ops.get_relation db ~name with
+        | None -> Error (RelationNotFound name)
+        | Some rel -> Ok rel)
     | Ast.Const pairs ->
-      Ok (Alg.const_relation
-            (List.map (fun (k, v) -> (k, ast_value_to_abstract v)) pairs))
+        Ok
+          (Alg.const_relation
+             (List.map (fun (k, v) -> (k, ast_value_to_abstract v)) pairs))
     | Ast.Select (filter_q, source_q) ->
-      execute storage db filter_q >>= fun filter ->
-      execute storage db source_q >>= fun source ->
-      (* semijoin = project(source attrs, equijoin on common attrs) *)
-      let common = List.filter_map (fun (n, _) ->
-        if List.exists (fun (m, _) -> m = n) filter.Relation.schema
-        then Some n else None) source.Relation.schema in
-      let source_attrs = List.map fst source.Relation.schema in
-      wrap (Alg.equijoin storage common source filter) >>= fun joined ->
-      wrap (Alg.project storage source_attrs joined)
+        execute storage db filter_q >>= fun filter ->
+        execute storage db source_q >>= fun source ->
+        (* semijoin = project(source attrs, equijoin on common attrs) *)
+        let common =
+          List.filter_map
+            (fun (n, _) ->
+              if List.exists (fun (m, _) -> m = n) filter.Relation.schema then
+                Some n
+              else None)
+            source.Relation.schema
+        in
+        let source_attrs = List.map fst source.Relation.schema in
+        wrap (Alg.equijoin storage common source filter) >>= fun joined ->
+        wrap (Alg.project storage source_attrs joined)
     | Ast.Join (attrs, q1, q2) ->
-      execute storage db q1 >>= fun r1 ->
-      execute storage db q2 >>= fun r2 ->
-      wrap (Alg.equijoin storage attrs r1 r2)
+        execute storage db q1 >>= fun r1 ->
+        execute storage db q2 >>= fun r2 ->
+        wrap (Alg.equijoin storage attrs r1 r2)
     | Ast.Project (attrs, q) ->
-      execute storage db q >>= fun rel ->
-      wrap (Alg.project storage attrs rel)
+        execute storage db q >>= fun rel -> wrap (Alg.project storage attrs rel)
     | Ast.Rename (renames, q) ->
-      execute storage db q >>= fun rel ->
-      wrap (Alg.rename storage renames rel)
+        execute storage db q >>= fun rel ->
+        wrap (Alg.rename storage renames rel)
     | Ast.Cartesian (q1, q2) ->
-      execute storage db q1 >>= fun r1 ->
-      execute storage db q2 >>= fun r2 ->
-      (* Cartesian product = join on no attrs *)
-      wrap (Alg.equijoin storage [] r1 r2)
+        execute storage db q1 >>= fun r1 ->
+        execute storage db q2 >>= fun r2 ->
+        (* Cartesian product = join on no attrs *)
+        wrap (Alg.equijoin storage [] r1 r2)
     | Ast.Union (q1, q2) ->
-      execute storage db q1 >>= fun r1 ->
-      execute storage db q2 >>= fun r2 ->
-      wrap (Alg.union storage r1 r2)
+        execute storage db q1 >>= fun r1 ->
+        execute storage db q2 >>= fun r2 -> wrap (Alg.union storage r1 r2)
     | Ast.Diff (q1, q2) ->
-      execute storage db q1 >>= fun r1 ->
-      execute storage db q2 >>= fun r2 ->
-      wrap (Alg.diff storage r1 r2)
+        execute storage db q1 >>= fun r1 ->
+        execute storage db q2 >>= fun r2 -> wrap (Alg.diff storage r1 r2)
     | Ast.Take (n, q) ->
-      execute storage db q >>= fun rel ->
-      wrap (Alg.take storage n rel)
+        execute storage db q >>= fun rel -> wrap (Alg.take storage n rel)
 end
 
-module Memory = Make(Management.Physical.Memory)
+module Memory = Make (Management.Physical.Memory)
diff --git a/lib/drl/gate.ml b/lib/drl/gate.ml
index 222e935..a314bce 100644
--- a/lib/drl/gate.ml
+++ b/lib/drl/gate.ml
@@ -1,8 +1,8 @@
 (** 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. *)
+    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 --------------------------------- *)
 
@@ -12,71 +12,68 @@ let string_to_chars (s : string) : char list =
 (* -- 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.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)
+      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)
+      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)
+      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)
+      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)
+      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)
+      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
+  | 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
+  | 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
+  | 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
-    []
+      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 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"
+      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 36ce15a..76d4b4e 100644
--- a/lib/drl/parser.ml
+++ b/lib/drl/parser.ml
@@ -2,13 +2,12 @@ type error = ParseError of string
 
 let of_sexp sexp =
   match Ast.query_of_sexp sexp with
-  | q             -> Ok q
+  | 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
+  | q -> Ok q
   | exception exn -> Error (ParseError (Printexc.to_string exn))
 
-let to_string q =
-  Ast.sexp_of_query q |> Sexplib.Sexp.to_string_hum
+let to_string q = Ast.sexp_of_query q |> Sexplib.Sexp.to_string_hum
diff --git a/lib/drl/sublanguage.ml b/lib/drl/sublanguage.ml
index f57af95..ce69b56 100644
--- a/lib/drl/sublanguage.ml
+++ b/lib/drl/sublanguage.ml
@@ -1,9 +1,9 @@
 module Make (Storage : Management.Physical.S) = struct
-  module Exec = Executor.Make(Storage)
+  module Exec = Executor.Make (Storage)
 
   type storage = Storage.t
-  type ast     = Ast.query
-  type error   = Exec.error
+  type ast = Ast.query
+  type error = Exec.error
 
   let name = "drl"
 
@@ -15,12 +15,12 @@ module Make (Storage : Management.Physical.S) = struct
   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
+    | 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)
+module Memory = Make (Management.Physical.Memory)