1 files changed, 39 insertions, 42 deletions

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"