1 files changed, 45 insertions, 54 deletions

diff --git a/lib/drl_verified/drl_verified.ml b/lib/drl_verified/drl_verified.ml
index b5aeaa7..868af2a 100644
--- a/lib/drl_verified/drl_verified.ml
+++ b/lib/drl_verified/drl_verified.ml
@@ -1,76 +1,67 @@
-
 (** 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)
+  | [] -> ( 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
+  | [] -> 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 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
+  | 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)
+  | 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)
-   | None -> None)
-| Cartesian (q1, q2) ->
-  (match predicted_finite db q1 with
-   | Some f1 ->
-     (match predicted_finite db q2 with
-      | Some f2 -> Some ((&&) f1 f2)
+  | 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)
-   | 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)
+  | 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)
-   | None -> None)
-| Diff (q1, _) -> predicted_finite db q1
-| _ -> Some true
+  | Diff (q1, _) -> predicted_finite db q1
+  | _ -> Some true