Format

1 files changed, 269 insertions, 346 deletions

diff --git a/lib/constraint.ml b/lib/constraint.ml
index 5e282c2..f657b00 100644
--- a/lib/constraint.ml
+++ b/lib/constraint.ml
@@ -24,45 +24,42 @@ module FingerTree = BatFingerTree
 type binding = binding_expr BindingMap.t
 
 type t =
-  | MemberOf of { target : relation_name; binding : binding }
-  | Not of { body : t; universe : relation_name }
+  | MemberOf of {target: relation_name; binding: binding}
+  | Not of {body: t; universe: relation_name}
   | And of t list
   | Or of t list
-  | Exists of { variable : attr_name; quantifier : relation_name; body : t }
-  | Forall of { variable : attr_name; quantifier : relation_name; body : t }
-  | Eq of { left : binding_expr; right : binding_expr }
+  | Exists of {variable: attr_name; quantifier: relation_name; body: t}
+  | Forall of {variable: attr_name; quantifier: relation_name; body: t}
+  | Eq of {left: binding_expr; right: binding_expr}
 
 type diagnostic =
-  | MembershipFailed of {
-      target : string;
-      bound_values : (attr_name * Conventions.AbstractValue.t) list;
-    }
+  | MembershipFailed of
+      {target: string; bound_values: (attr_name * Conventions.AbstractValue.t) list}
   | RelationNotFound of string
-  | UnboundedQuantifier of { variable : attr_name; quantifier : relation_name }
+  | UnboundedQuantifier of {variable: attr_name; quantifier: relation_name}
   | ConstraintFailures of (string * diagnostic) list
 
 let vars_in (c : t) : attr_name list =
   let add_from_binding set binding =
     BindingMap.fold
-      (fun _ expr acc ->
-        match expr with Var v -> StringSet.add v acc | Const _ -> acc)
+      (fun _ expr acc -> match expr with Var v -> StringSet.add v acc | Const _ -> acc)
       binding set
   in
   let rec loop set worklist =
     match FingerTree.front worklist with
     | None -> set
     | Some (rest, node) -> (
-        match node with
-        | MemberOf { binding; _ } -> loop (add_from_binding set binding) rest
-        | Not { body; _ } -> loop set (FingerTree.cons rest body)
-        | And cs | Or cs ->
-            let next = FingerTree.append (FingerTree.of_list cs) rest in
-            loop set next
-        | Exists { variable; body; _ } | Forall { variable; body; _ } ->
-            loop (StringSet.add variable set) (FingerTree.cons rest body)
-        | Eq { left; right } ->
-            let add_expr acc = function Var v -> StringSet.add v acc | Const _ -> acc in
-            loop (add_expr (add_expr set left) right) rest)
+      match node with
+      | MemberOf {binding; _} -> loop (add_from_binding set binding) rest
+      | Not {body; _} -> loop set (FingerTree.cons rest body)
+      | And cs | Or cs ->
+          let next = FingerTree.append (FingerTree.of_list cs) rest in
+          loop set next
+      | Exists {variable; body; _} | Forall {variable; body; _} ->
+          loop (StringSet.add variable set) (FingerTree.cons rest body)
+      | Eq {left; right} ->
+          let add_expr acc = function Var v -> StringSet.add v acc | Const _ -> acc in
+          loop (add_expr (add_expr set left) right) rest )
   in
   loop StringSet.empty (FingerTree.singleton c) |> StringSet.elements
 
@@ -72,30 +69,28 @@ let rename_vars (renames : (attr_name * attr_name) list) : t -> t =
     match BindingMap.find_opt name rename_map with Some n -> n | None -> name
   in
   let rec go = function
-    | MemberOf { target; binding } ->
+    | MemberOf {target; binding} ->
         let binding' =
           BindingMap.fold
             (fun k expr acc ->
               let k' = rename_name k in
-              let expr' =
-                match expr with Var v -> Var (rename_name v) | Const _ -> expr
-              in
-              BindingMap.add k' expr' acc)
+              let expr' = match expr with Var v -> Var (rename_name v) | Const _ -> expr in
+              BindingMap.add k' expr' acc )
             binding BindingMap.empty
         in
-        MemberOf { target; binding = binding' }
-    | Not { body; universe } -> Not { body = go body; universe }
+        MemberOf {target; binding= binding'}
+    | Not {body; universe} -> Not {body= go body; universe}
     | And cs -> And (List.map go cs)
     | Or cs -> Or (List.map go cs)
-    | Exists { variable; quantifier; body } ->
+    | Exists {variable; quantifier; body} ->
         let variable' = rename_name variable in
-        Exists { variable = variable'; quantifier; body = go body }
-    | Forall { variable; quantifier; body } ->
+        Exists {variable= variable'; quantifier; body= go body}
+    | Forall {variable; quantifier; body} ->
         let variable' = rename_name variable in
-        Forall { variable = variable'; quantifier; body = go body }
-    | Eq { left; right } ->
+        Forall {variable= variable'; quantifier; body= go body}
+    | Eq {left; right} ->
         let rename_expr = function Var v -> Var (rename_name v) | Const _ as e -> e in
-        Eq { left = rename_expr left; right = rename_expr right }
+        Eq {left= rename_expr left; right= rename_expr right}
   in
   go
 
@@ -105,10 +100,10 @@ let rec filter_by_attrs (attrs : attr_name list) (c : t) : t option =
   let all_present c = List.for_all (fun v -> List.mem v attrs) (vars_in c) in
   match c with
   | MemberOf _ -> if all_present c then Some c else None
-  | Not { body; universe } -> (
-      match filter_by_attrs attrs body with
-      | Some body' -> Some (Not { body = body'; universe })
-      | None -> None)
+  | Not {body; universe} -> (
+    match filter_by_attrs attrs body with
+    | Some body' -> Some (Not {body= body'; universe})
+    | None -> None )
   | And cs ->
       let kept = List.filter_map (filter_by_attrs attrs) cs in
       if kept = [] then None else Some (And kept)
@@ -116,139 +111,132 @@ let rec filter_by_attrs (attrs : attr_name list) (c : t) : t option =
       (* All branches must survive for Or to remain sound *)
       let kept = List.filter_map (filter_by_attrs attrs) cs in
       if List.length kept = List.length cs then Some (Or kept) else None
-  | Exists { variable; quantifier; body } -> (
-      match filter_by_attrs (variable :: attrs) body with
-      | Some body' -> Some (Exists { variable; quantifier; body = body' })
-      | None -> None)
-  | Forall { variable; quantifier; body } -> (
-      match filter_by_attrs (variable :: attrs) body with
-      | Some body' -> Some (Forall { variable; quantifier; body = body' })
-      | None -> None)
+  | Exists {variable; quantifier; body} -> (
+    match filter_by_attrs (variable :: attrs) body with
+    | Some body' -> Some (Exists {variable; quantifier; body= body'})
+    | None -> None )
+  | Forall {variable; quantifier; body} -> (
+    match filter_by_attrs (variable :: attrs) body with
+    | Some body' -> Some (Forall {variable; quantifier; body= body'})
+    | None -> None )
   | Eq _ -> if all_present c then Some c else None
 
-let merge (cs1 : (string * t) list) (cs2 : (string * t) list) :
-    (string * t) list =
+let merge (cs1 : (string * t) list) (cs2 : (string * t) list) : (string * t) list =
   let combined = cs1 @ cs2 in
   let tbl = Hashtbl.create 16 in
   List.iter
     (fun (name, c) ->
       match Hashtbl.find_opt tbl name with
-      | None -> Hashtbl.replace tbl name [ c ]
-      | Some cs -> Hashtbl.replace tbl name (c :: cs))
+      | None -> Hashtbl.replace tbl name [c]
+      | Some cs -> Hashtbl.replace tbl name (c :: cs) )
     combined;
   Hashtbl.fold
     (fun name cs acc ->
-      let merged = match cs with [ c ] -> c | _ -> And cs in
-      (name, merged) :: acc)
+      let merged = match cs with [c] -> c | _ -> And cs in
+      (name, merged) :: acc )
     tbl []
 
-let member_of ~target ~binding = MemberOf { target; binding }
-let not_ ~universe body = Not { body; universe }
-let and_ cs = match cs with [ c ] -> c | _ -> And cs
-let or_ cs = match cs with [ c ] -> c | _ -> Or cs
-let exists ~variable ~quantifier body = Exists { variable; quantifier; body }
-let forall ~variable ~quantifier body = Forall { variable; quantifier; body }
-
-type eval_context = {
-  check_membership :
-    relation_name -> (attr_name * Conventions.AbstractValue.t) list -> bool;
-  iterate_finite :
-    relation_name -> (attr_name * Conventions.AbstractValue.t) list list option;
-}
-
-let bind (b : binding) (tuple : Tuple.materialized) :
-    (attr_name * Conventions.AbstractValue.t) list =
+let member_of ~target ~binding = MemberOf {target; binding}
+let not_ ~universe body = Not {body; universe}
+let and_ cs = match cs with [c] -> c | _ -> And cs
+let or_ cs = match cs with [c] -> c | _ -> Or cs
+let exists ~variable ~quantifier body = Exists {variable; quantifier; body}
+let forall ~variable ~quantifier body = Forall {variable; quantifier; body}
+
+type eval_context =
+  { check_membership: relation_name -> (attr_name * Conventions.AbstractValue.t) list -> bool;
+    iterate_finite: relation_name -> (attr_name * Conventions.AbstractValue.t) list list option }
+
+let bind (b : binding) (tuple : Tuple.materialized) : (attr_name * Conventions.AbstractValue.t) list
+    =
   BindingMap.fold
     (fun target_attr expr acc ->
       let value =
         match expr with
         | Const v -> Some v
         | Var src_attr -> (
-            match Tuple.AttributeMap.find_opt src_attr tuple.attributes with
-            | Some attr -> Some attr.Attribute.value
-            | None -> None)
+          match Tuple.AttributeMap.find_opt src_attr tuple.attributes with
+          | Some attr -> Some attr.Attribute.value
+          | None -> None )
       in
-      match value with Some v -> (target_attr, v) :: acc | None -> acc)
+      match value with Some v -> (target_attr, v) :: acc | None -> acc )
     b []
 
 let rec evaluate (ctx : eval_context) (tuple : Tuple.materialized) (c : t) :
     (bool, diagnostic) result =
   match c with
-  | MemberOf { target; binding } ->
+  | MemberOf {target; binding} ->
       let bound_values = bind binding tuple in
       if ctx.check_membership target bound_values then Ok true
-      else Error (MembershipFailed { target; bound_values })
-  | Not { body; universe = _ } -> (
-      (* The universe is a declarative annotation for closed-world reasoning.
+      else Error (MembershipFailed {target; bound_values})
+  | Not {body; universe= _} -> (
+    (* The universe is a declarative annotation for closed-world reasoning.
        At runtime we negate the body; the universe enforces logical soundness
        at the schema level, not as a runtime tuple-existence check. *)
-      match evaluate ctx tuple body with
-      | Ok true -> Ok false
-      | Ok false -> Ok true
-      | Error (MembershipFailed _) -> Ok true
-      | Error d -> Error d)
+    match evaluate ctx tuple body with
+    | Ok true -> Ok false
+    | Ok false -> Ok true
+    | Error (MembershipFailed _) -> Ok true
+    | Error d -> Error d )
   | And cs -> evaluate_and ctx tuple cs
   | Or cs -> evaluate_or ctx tuple cs
-  | Eq { left; right } ->
+  | Eq {left; right} -> (
       let resolve = function
         | Const v -> Some v
         | Var a -> (
-            match Tuple.AttributeMap.find_opt a tuple.attributes with
-            | Some attr -> Some attr.Attribute.value
-            | None -> None)
+          match Tuple.AttributeMap.find_opt a tuple.attributes with
+          | Some attr -> Some attr.Attribute.value
+          | None -> None )
       in
-      (match (resolve left, resolve right) with
-      | Some l, Some r -> Ok (l = r)
-      | _ -> Ok false)
-  | Exists { variable; quantifier; body } -> (
-      match ctx.iterate_finite quantifier with
-      | None -> Error (UnboundedQuantifier { variable; quantifier })
-      | Some rows ->
-          let rec check = function
-            | [] -> Ok false
-            | row :: rest -> (
-                let extended_tuple = extend_tuple tuple variable row in
-                match evaluate ctx extended_tuple body with
-                | Ok true -> Ok true
-                | Ok false -> check rest
-                | Error _ -> check rest)
-          in
-          check rows)
-  | Forall { variable; quantifier; body } -> (
-      match ctx.iterate_finite quantifier with
-      | None -> Error (UnboundedQuantifier { variable; quantifier })
-      | Some rows ->
-          let rec check = function
-            | [] -> Ok true
-            | row :: rest -> (
-                let extended_tuple = extend_tuple tuple variable row in
-                match evaluate ctx extended_tuple body with
-                | Ok true -> check rest
-                | Ok false -> Ok false
-                | Error (MembershipFailed _) -> Ok false
-                | Error d -> Error d)
-          in
-          check rows)
+      match resolve left, resolve right with Some l, Some r -> Ok (l = r) | _ -> Ok false )
+  | Exists {variable; quantifier; body} -> (
+    match ctx.iterate_finite quantifier with
+    | None -> Error (UnboundedQuantifier {variable; quantifier})
+    | Some rows ->
+        let rec check = function
+          | [] -> Ok false
+          | row :: rest -> (
+              let extended_tuple = extend_tuple tuple variable row in
+              match evaluate ctx extended_tuple body with
+              | Ok true -> Ok true
+              | Ok false -> check rest
+              | Error _ -> check rest )
+        in
+        check rows )
+  | Forall {variable; quantifier; body} -> (
+    match ctx.iterate_finite quantifier with
+    | None -> Error (UnboundedQuantifier {variable; quantifier})
+    | Some rows ->
+        let rec check = function
+          | [] -> Ok true
+          | row :: rest -> (
+              let extended_tuple = extend_tuple tuple variable row in
+              match evaluate ctx extended_tuple body with
+              | Ok true -> check rest
+              | Ok false -> Ok false
+              | Error (MembershipFailed _) -> Ok false
+              | Error d -> Error d )
+        in
+        check rows )
 
 and evaluate_and ctx tuple = function
   | [] -> Ok true
   | c :: rest -> (
-      match evaluate ctx tuple c with
-      | Ok true -> evaluate_and ctx tuple rest
-      | Ok false -> Ok false
-      | Error d -> Error d)
+    match evaluate ctx tuple c with
+    | Ok true -> evaluate_and ctx tuple rest
+    | Ok false -> Ok false
+    | Error d -> Error d )
 
 and evaluate_or ctx tuple = function
   | [] -> Ok false
   | c :: rest -> (
-      match evaluate ctx tuple c with
-      | Ok true -> Ok true
-      | Ok false -> evaluate_or ctx tuple rest
-      | Error _ -> evaluate_or ctx tuple rest)
+    match evaluate ctx tuple c with
+    | Ok true -> Ok true
+    | Ok false -> evaluate_or ctx tuple rest
+    | Error _ -> evaluate_or ctx tuple rest )
 
 and extend_tuple (tuple : Tuple.materialized) (variable : attr_name)
-    (row : (attr_name * Conventions.AbstractValue.t) list) : Tuple.materialized
-    =
+    (row : (attr_name * Conventions.AbstractValue.t) list) : Tuple.materialized =
   (* Quantifier attributes are namespaced by the variable name (for example "d.dept_id")
      so they cannot silently overwrite same-named attributes from the base tuple
      or from other quantifiers. Without such namespacing, a constraint like
@@ -263,23 +251,21 @@ and extend_tuple (tuple : Tuple.materialized) (variable : attr_name)
      to each attribute rather than relying on name conventions, but we don't have that yet. *)
   let extra_attrs =
     List.fold_left
-      (fun acc (k, v) ->
-        Tuple.AttributeMap.add (variable ^ "." ^ k) { Attribute.value = v } acc)
+      (fun acc (k, v) -> Tuple.AttributeMap.add (variable ^ "." ^ k) {Attribute.value= v} acc)
       tuple.attributes row
   in
-  { tuple with attributes = extra_attrs }
+  {tuple with attributes= extra_attrs}
 
 (* TODO: Sometimes it's more efficient and sufficient to simply halt at the first constraint violated. However, it's also important to be able to adjudicate which constraints failed on the tuple materialization. For that reason, we should likely return a lazy stream that computes the constraints on demand. *)
-let evaluate_named (ctx : eval_context) (tuple : Tuple.materialized)
-    (named : (string * t) list) : (bool, diagnostic) result =
+let evaluate_named (ctx : eval_context) (tuple : Tuple.materialized) (named : (string * t) list) :
+    (bool, diagnostic) result =
   let failures =
     List.filter_map
       (fun (name, c) ->
         match evaluate ctx tuple c with
         | Ok true -> None
-        | Ok false ->
-            Some (name, MembershipFailed { target = name; bound_values = [] })
-        | Error d -> Some (name, d))
+        | Ok false -> Some (name, MembershipFailed {target= name; bound_values= []})
+        | Error d -> Some (name, d) )
       named
   in
   match failures with [] -> Ok true | fs -> Error (ConstraintFailures fs)
@@ -290,8 +276,7 @@ let evaluate_first_failure (ctx : eval_context) (tuple : Tuple.materialized)
     (named : (string * t) list) : (bool, diagnostic) result =
   let rec loop = function
     | [] -> Ok true
-    | (_name, c) :: rest -> (
-        match evaluate ctx tuple c with Ok true -> loop rest | r -> r)
+    | (_name, c) :: rest -> ( match evaluate ctx tuple c with Ok true -> loop rest | r -> r )
   in
   loop named
 
@@ -304,15 +289,9 @@ type polarity = Positive | Negative | Both
 type polarity_index = polarity PolarityMap.t
 
 let merge_polarity a b =
-  match (a, b) with
-  | Positive, Positive -> Positive
-  | Negative, Negative -> Negative
-  | _ -> Both
+  match a, b with Positive, Positive -> Positive | Negative, Negative -> Negative | _ -> Both
 
-let flip_polarity = function
-  | Positive -> Negative
-  | Negative -> Positive
-  | Both -> Both
+let flip_polarity = function Positive -> Negative | Negative -> Positive | Both -> Both
 
 let polarity_of ?(neg = false) (c : t) : polarity_index =
   let with_neg is_neg pol = if is_neg then flip_polarity pol else pol in
@@ -325,23 +304,20 @@ let polarity_of ?(neg = false) (c : t) : polarity_index =
     match FingerTree.front worklist with
     | None -> acc
     | Some (rest, (is_neg, node)) -> (
-        match node with
-        | MemberOf { target; _ } ->
-            loop (add_pol acc target (with_neg is_neg Positive)) rest
-        | Not { body; _ } -> loop acc (FingerTree.cons rest (not is_neg, body))
-        | And cs | Or cs ->
-            let children =
-              List.map (fun child -> (is_neg, child)) cs |> FingerTree.of_list
-            in
-            let next = FingerTree.append children rest in
-            loop acc next
-        | Exists { quantifier; body; _ } ->
-            let acc' = add_pol acc quantifier (with_neg is_neg Positive) in
-            loop acc' (FingerTree.cons rest (is_neg, body))
-        | Forall { quantifier; body; _ } ->
-            let acc' = add_pol acc quantifier (with_neg is_neg Negative) in
-            loop acc' (FingerTree.cons rest (is_neg, body))
-        | Eq _ -> loop acc rest)
+      match node with
+      | MemberOf {target; _} -> loop (add_pol acc target (with_neg is_neg Positive)) rest
+      | Not {body; _} -> loop acc (FingerTree.cons rest (not is_neg, body))
+      | And cs | Or cs ->
+          let children = List.map (fun child -> is_neg, child) cs |> FingerTree.of_list in
+          let next = FingerTree.append children rest in
+          loop acc next
+      | Exists {quantifier; body; _} ->
+          let acc' = add_pol acc quantifier (with_neg is_neg Positive) in
+          loop acc' (FingerTree.cons rest (is_neg, body))
+      | Forall {quantifier; body; _} ->
+          let acc' = add_pol acc quantifier (with_neg is_neg Negative) in
+          loop acc' (FingerTree.cons rest (is_neg, body))
+      | Eq _ -> loop acc rest )
   in
   loop PolarityMap.empty (FingerTree.singleton (neg, c))
 
@@ -351,9 +327,7 @@ let polarity_find name (pols : polarity_index) = PolarityMap.find_opt name pols
     (checked at transaction commit). *)
 type timing = Immediate | Deferred
 
-type substitute_mode =
-  | SubstituteGo
-  | SubstituteApply of Conventions.AbstractValue.t BindingMap.t
+type substitute_mode = SubstituteGo | SubstituteApply of Conventions.AbstractValue.t BindingMap.t
 
 type substitute_instr =
   | Visit of substitute_mode * t
@@ -380,26 +354,22 @@ let focused_filter (c : t) (dep_rel : relation_name)
       (fun _target_attr expr acc ->
         match expr with
         | Var src_attr -> (
-            match List.assoc_opt src_attr deleted with
-            | Some v -> (src_attr, v) :: acc
-            | None -> acc)
-        | Const _ -> acc)
+          match List.assoc_opt src_attr deleted with Some v -> (src_attr, v) :: acc | None -> acc )
+        | Const _ -> acc )
       binding acc
   in
   let rec loop acc worklist =
     match FingerTree.front worklist with
     | None -> acc
     | Some (rest, node) -> (
-        match node with
-        | MemberOf { target; binding } when target = dep_rel ->
-            loop (add_from_binding acc binding) rest
-        | MemberOf _ -> loop acc rest
-        | Not { body; _ } | Exists { body; _ } | Forall { body; _ } ->
-            loop acc (FingerTree.cons rest body)
-        | And cs | Or cs ->
-            let next = FingerTree.append (FingerTree.of_list cs) rest in
-            loop acc next
-        | Eq _ -> loop acc rest)
+      match node with
+      | MemberOf {target; binding} when target = dep_rel -> loop (add_from_binding acc binding) rest
+      | MemberOf _ -> loop acc rest
+      | Not {body; _} | Exists {body; _} | Forall {body; _} -> loop acc (FingerTree.cons rest body)
+      | And cs | Or cs ->
+          let next = FingerTree.append (FingerTree.of_list cs) rest in
+          loop acc next
+      | Eq _ -> loop acc rest )
   in
   loop [] (FingerTree.singleton c)
 
@@ -413,23 +383,21 @@ let trigger_constants (c : t) (dep_rel : relation_name) :
   let add_from_binding acc binding =
     BindingMap.fold
       (fun target_attr expr acc ->
-        match expr with Const v -> (target_attr, v) :: acc | Var _ -> acc)
+        match expr with Const v -> (target_attr, v) :: acc | Var _ -> acc )
       binding acc
   in
   let rec loop acc worklist =
     match FingerTree.front worklist with
     | None -> acc
     | Some (rest, node) -> (
-        match node with
-        | MemberOf { target; binding } when target = dep_rel ->
-            loop (add_from_binding acc binding) rest
-        | MemberOf _ -> loop acc rest
-        | Not { body; _ } | Exists { body; _ } | Forall { body; _ } ->
-            loop acc (FingerTree.cons rest body)
-        | And cs | Or cs ->
-            let next = FingerTree.append (FingerTree.of_list cs) rest in
-            loop acc next
-        | Eq _ -> loop acc rest)
+      match node with
+      | MemberOf {target; binding} when target = dep_rel -> loop (add_from_binding acc binding) rest
+      | MemberOf _ -> loop acc rest
+      | Not {body; _} | Exists {body; _} | Forall {body; _} -> loop acc (FingerTree.cons rest body)
+      | And cs | Or cs ->
+          let next = FingerTree.append (FingerTree.of_list cs) rest in
+          loop acc next
+      | Eq _ -> loop acc rest )
   in
   loop [] (FingerTree.singleton c)
 
@@ -460,8 +428,7 @@ let substitute_transition (c : t) (dep_rel : relation_name)
   let enqueue_children mode cs build_of_count rest =
     let prefix, count =
       List.fold_left
-        (fun (acc, n) child ->
-          (FingerTree.snoc acc (Visit (mode, child)), n + 1))
+        (fun (acc, n) child -> FingerTree.snoc acc (Visit (mode, child)), n + 1)
         (FingerTree.empty, 0) cs
     in
     let prefix = FingerTree.snoc prefix (build_of_count count) in
@@ -471,182 +438,142 @@ let substitute_transition (c : t) (dep_rel : relation_name)
     BindingMap.map
       (function
         | Var v -> (
-            match BindingMap.find_opt v subs with
-            | Some value -> Const value
-            | None -> Var v)
-        | Const _ as expr -> expr)
+          match BindingMap.find_opt v subs with Some value -> Const value | None -> Var v )
+        | Const _ as expr -> expr )
       binding
   in
   let rec pop_n n vals acc =
-    if n = 0 then (acc, vals)
-    else
-      match vals with
-      | [] -> (acc, [])
-      | v :: rest -> pop_n (n - 1) rest (v :: acc)
+    if n = 0 then acc, vals
+    else match vals with [] -> acc, [] | v :: rest -> pop_n (n - 1) rest (v :: acc)
   in
   let rec loop instrs vals =
     match FingerTree.front instrs with
-    | None -> ( match vals with [ result ] -> result | _ -> c)
+    | None -> ( match vals with [result] -> result | _ -> c )
     | Some (rest, instr) -> (
-        match instr with
-        | Visit (mode, node) -> (
-            match node with
-            | MemberOf { target; binding } ->
-                let binding' =
-                  match mode with
-                  | SubstituteGo -> binding
-                  | SubstituteApply subs -> apply_subs subs binding
-                in
-                loop rest (MemberOf { target; binding = binding' } :: vals)
-            | Not { body; universe } ->
-                loop
-                  (enqueue_visit_then_build
-                     (Visit (mode, body))
-                     (BuildNot universe) rest)
-                  vals
-            | And cs ->
-                let instrs' =
-                  enqueue_children mode cs (fun n -> BuildAnd n) rest
-                in
-                loop instrs' vals
-            | Or cs ->
-                let instrs' =
-                  enqueue_children mode cs (fun n -> BuildOr n) rest
-                in
-                loop instrs' vals
-            | Exists { variable; quantifier; body } ->
-                let body_mode =
-                  match mode with
-                  | SubstituteApply subs -> SubstituteApply subs
-                  | SubstituteGo ->
-                      if quantifier = dep_rel then
-                        SubstituteApply (namespaced_subs variable)
-                      else SubstituteGo
-                in
-                loop
-                  (enqueue_visit_then_build
-                     (Visit (body_mode, body))
-                     (BuildExists (variable, quantifier))
-                     rest)
-                  vals
-            | Forall { variable; quantifier; body } ->
-                let body_mode =
-                  match mode with
-                  | SubstituteApply subs -> SubstituteApply subs
-                  | SubstituteGo ->
-                      if quantifier = dep_rel then
-                        SubstituteApply (namespaced_subs variable)
-                      else SubstituteGo
-                in
-                loop
-                  (enqueue_visit_then_build
-                     (Visit (body_mode, body))
-                     (BuildForall (variable, quantifier))
-                     rest)
-                  vals
-            | Eq { left; right } ->
-                let subst_expr subs = function
-                  | Var v -> (match BindingMap.find_opt v subs with Some v' -> Const v' | None -> Var v)
-                  | Const _ as e -> e
-                in
-                let left', right' = match mode with
-                  | SubstituteGo -> (left, right)
-                  | SubstituteApply subs -> (subst_expr subs left, subst_expr subs right)
-                in
-                loop rest (Eq { left = left'; right = right' } :: vals))
-        | BuildNot universe -> (
-            match vals with
-            | body :: vals' -> loop rest (Not { body; universe } :: vals')
-            | [] -> loop rest vals)
-        | BuildAnd n ->
-            let children, vals' = pop_n n vals [] in
-            loop rest (And children :: vals')
-        | BuildOr n ->
-            let children, vals' = pop_n n vals [] in
-            loop rest (Or children :: vals')
-        | BuildExists (variable, quantifier) -> (
-            match vals with
-            | body :: vals' ->
-                loop rest (Exists { variable; quantifier; body } :: vals')
-            | [] -> loop rest vals)
-        | BuildForall (variable, quantifier) -> (
-            match vals with
-            | body :: vals' ->
-                loop rest (Forall { variable; quantifier; body } :: vals')
-            | [] -> loop rest vals))
+      match instr with
+      | Visit (mode, node) -> (
+        match node with
+        | MemberOf {target; binding} ->
+            let binding' =
+              match mode with
+              | SubstituteGo -> binding
+              | SubstituteApply subs -> apply_subs subs binding
+            in
+            loop rest (MemberOf {target; binding= binding'} :: vals)
+        | Not {body; universe} ->
+            loop (enqueue_visit_then_build (Visit (mode, body)) (BuildNot universe) rest) vals
+        | And cs ->
+            let instrs' = enqueue_children mode cs (fun n -> BuildAnd n) rest in
+            loop instrs' vals
+        | Or cs ->
+            let instrs' = enqueue_children mode cs (fun n -> BuildOr n) rest in
+            loop instrs' vals
+        | Exists {variable; quantifier; body} ->
+            let body_mode =
+              match mode with
+              | SubstituteApply subs -> SubstituteApply subs
+              | SubstituteGo ->
+                  if quantifier = dep_rel then SubstituteApply (namespaced_subs variable)
+                  else SubstituteGo
+            in
+            loop
+              (enqueue_visit_then_build
+                 (Visit (body_mode, body))
+                 (BuildExists (variable, quantifier))
+                 rest )
+              vals
+        | Forall {variable; quantifier; body} ->
+            let body_mode =
+              match mode with
+              | SubstituteApply subs -> SubstituteApply subs
+              | SubstituteGo ->
+                  if quantifier = dep_rel then SubstituteApply (namespaced_subs variable)
+                  else SubstituteGo
+            in
+            loop
+              (enqueue_visit_then_build
+                 (Visit (body_mode, body))
+                 (BuildForall (variable, quantifier))
+                 rest )
+              vals
+        | Eq {left; right} ->
+            let subst_expr subs = function
+              | Var v -> (
+                match BindingMap.find_opt v subs with Some v' -> Const v' | None -> Var v )
+              | Const _ as e -> e
+            in
+            let left', right' =
+              match mode with
+              | SubstituteGo -> left, right
+              | SubstituteApply subs -> subst_expr subs left, subst_expr subs right
+            in
+            loop rest (Eq {left= left'; right= right'} :: vals) )
+      | BuildNot universe -> (
+        match vals with
+        | body :: vals' -> loop rest (Not {body; universe} :: vals')
+        | [] -> loop rest vals )
+      | BuildAnd n ->
+          let children, vals' = pop_n n vals [] in
+          loop rest (And children :: vals')
+      | BuildOr n ->
+          let children, vals' = pop_n n vals [] in
+          loop rest (Or children :: vals')
+      | BuildExists (variable, quantifier) -> (
+        match vals with
+        | body :: vals' -> loop rest (Exists {variable; quantifier; body} :: vals')
+        | [] -> loop rest vals )
+      | BuildForall (variable, quantifier) -> (
+        match vals with
+        | body :: vals' -> loop rest (Forall {variable; quantifier; body} :: vals')
+        | [] -> loop rest vals ) )
   in
   loop (FingerTree.singleton (Visit (SubstituteGo, c))) []
 
 let make_comparison_binding ~left ~right =
   BindingMap.empty |> BindingMap.add "left" left |> BindingMap.add "right" right
 
-let lt ~left ~right =
-  MemberOf
-    { target = "less_than"; binding = make_comparison_binding ~left ~right }
+let lt ~left ~right = MemberOf {target= "less_than"; binding= make_comparison_binding ~left ~right}
 
 let lte ~left ~right =
-  MemberOf
-    {
-      target = "less_than_or_equal";
-      binding = make_comparison_binding ~left ~right;
-    }
+  MemberOf {target= "less_than_or_equal"; binding= make_comparison_binding ~left ~right}
 
 let gt ~left ~right =
-  MemberOf
-    { target = "greater_than"; binding = make_comparison_binding ~left ~right }
+  MemberOf {target= "greater_than"; binding= make_comparison_binding ~left ~right}
 
 let gte ~left ~right =
-  MemberOf
-    {
-      target = "greater_than_or_equal";
-      binding = make_comparison_binding ~left ~right;
-    }
-
-let eq ~left ~right = Eq { left; right }
+  MemberOf {target= "greater_than_or_equal"; binding= make_comparison_binding ~left ~right}
 
-let neq ~left ~right =
-  Not { body = Eq { left; right }; universe = "" }
+let eq ~left ~right = Eq {left; right}
+let neq ~left ~right = Not {body= Eq {left; right}; universe= ""}
 
 let between ~value ~low ~high =
   And
-    [
+    [ MemberOf
+        {target= "greater_than_or_equal"; binding= make_comparison_binding ~left:value ~right:low};
       MemberOf
-        {
-          target = "greater_than_or_equal";
-          binding = make_comparison_binding ~left:value ~right:low;
-        };
-      MemberOf
-        {
-          target = "less_than_or_equal";
-          binding = make_comparison_binding ~left:value ~right:high;
-        };
-    ]
+        {target= "less_than_or_equal"; binding= make_comparison_binding ~left:value ~right:high} ]
 
 (** Build membership criteria from schema (validates type membership). Returns a
     function that takes a tree-lookup function and a tuple, checking schema
     conformance and tree membership at call time. *)
-let build_membership_criteria 
-      ~_name
-      ~schema :
-      (*(string -> Merkle.t option) ->*) Tuple.t -> bool =
-  let value_conforms_to_domain domain_name (value : Conventions.AbstractValue.t)
-    =
+let build_membership_criteria ~_name ~schema : (*(string -> Merkle.t option) ->*) Tuple.t -> bool =
+  let value_conforms_to_domain domain_name (value : Conventions.AbstractValue.t) =
     match domain_name with
     | "integer" -> Obj.is_int value
     | "natural" -> Obj.is_int value && (Obj.obj value : int) >= 0
     | "string" -> Obj.tag value = Obj.string_tag
     | _ ->
-       (* Unknown domain: could be a relation-typed attribute (nested tuple)
+        (* Unknown domain: could be a relation-typed attribute (nested tuple)
           or a user-defined domain. Accept for now; full validation would
           require looking up the target relation's schema. *)
-       true
+        true
   in
   let n_expected = List.length schema in
   (* fun tree_of tuple -> *)
   fun tuple ->
-  match tuple with
-  | Tuple.NonMaterialized _nm ->
-     (* begin match tree_of name with
+    match tuple with
+    | Tuple.NonMaterialized _nm ->
+        (* begin match tree_of name with
         | None -> false
         | Some t ->
         Merkle.member nm.hash t
@@ -656,23 +583,19 @@ let build_membership_criteria
         Tuple.AttributeMap.mem attr_name nm.attributes)
         schema
         end *)
-     false
-  | Tuple.Materialized m ->
-     Tuple.AttributeMap.cardinal m.attributes = n_expected
-     && List.for_all
-          (fun (attr_name, domain_name) ->
-            match Tuple.AttributeMap.find_opt attr_name m.attributes with
-            | None -> false
-            | Some attr ->
-               value_conforms_to_domain domain_name attr.Attribute.value)
-          schema
+        false
+    | Tuple.Materialized m ->
+        Tuple.AttributeMap.cardinal m.attributes = n_expected
+        && List.for_all
+             (fun (attr_name, domain_name) ->
+               match Tuple.AttributeMap.find_opt attr_name m.attributes with
+               | None -> false
+               | Some attr -> value_conforms_to_domain domain_name attr.Attribute.value )
+             schema
 
 (** Mutation direction for cascade constraint checking *)
 type mutation = Insert | Delete
 
 (** Context for a single tuple mutation, used by cascade checking *)
-type mutation_context = {
-    target_relation : string;
-    transition : (string * Conventions.AbstractValue.t) list;
-    kind : mutation;
-  }
+type mutation_context =
+  {target_relation: string; transition: (string * Conventions.AbstractValue.t) list; kind: mutation}