Polarity walker, constraint and manipulation refactor with batteries

1 files changed, 408 insertions, 287 deletions

diff --git a/lib/constraint.ml b/lib/constraint.ml
index 527a7dc..05442ab 100644
--- a/lib/constraint.ml
+++ b/lib/constraint.ml
@@ -1,11 +1,11 @@
 (** Constraint system for relational membership criteria.
 
     A relation's intension includes constraints that refine the space of
-    admissible tuples. Since constraints are themselves relations, checking
-    a constraint = checking membership in that constraint-relation.
+    admissible tuples. Since constraints are themselves relations, checking a
+    constraint = checking membership in that constraint-relation.
 
-    Negation requires an explicit universe relation name, forcing
-    closed-world reasoning in first-order logic. *)
+    Negation requires an explicit universe relation name, forcing closed-world
+    reasoning in first-order logic. *)
 
 (* TODO: lt/lte/gt/gte/eq/neq/between at the bottom reference target names
    like "less_than" that don't match the prelude relation names
@@ -14,12 +14,12 @@
 
 type relation_name = string
 type attr_name = string
-
-type binding_expr =
-  | Var of attr_name
-  | Const of Conventions.AbstractValue.t
+type binding_expr = Var of attr_name | Const of Conventions.AbstractValue.t
 
 module BindingMap = Map.Make (String)
+module PolarityMap = Map.Make (String)
+module StringSet = Set.Make (String)
+module FingerTree = BatFingerTree
 
 type binding = binding_expr BindingMap.t
 
@@ -37,96 +37,89 @@ type diagnostic =
       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 rec vars_in : t -> attr_name list = function
-  | MemberOf { binding; _ } ->
+let vars_in (c : t) : attr_name list =
+  let add_from_binding set binding =
     BindingMap.fold
       (fun _ expr acc ->
-        match expr with
-        | Var v -> if List.mem v acc then acc else v :: acc
-        | Const _ -> acc)
-      binding []
-  | Not { body; _ } -> vars_in body
-  | And cs | Or cs -> List.concat_map vars_in cs |> List.sort_uniq String.compare
-  | Exists { variable; body; _ } | Forall { variable; body; _ } ->
-    let inner = vars_in body in
-    if List.mem variable inner then inner
-    else variable :: inner
-
-let rec rename_vars (renames : (attr_name * attr_name) list) : t -> t = function
-  | MemberOf { target; binding } ->
-    let binding' =
-      BindingMap.fold
-        (fun k expr acc ->
-          let k' =
-            match List.assoc_opt k renames with Some n -> n | None -> k
-          in
-          let expr' =
-            match expr with
-            | Var v -> (
-              match List.assoc_opt v renames with
-              | Some n -> Var n
-              | None -> expr)
-            | Const _ -> expr
-          in
-          BindingMap.add k' expr' acc)
-        binding BindingMap.empty
-    in
-    MemberOf { target; binding = binding' }
-  | Not { body; universe } ->
-    Not { body = rename_vars renames body; universe }
-  | And cs -> And (List.map (rename_vars renames) cs)
-  | Or cs -> Or (List.map (rename_vars renames) cs)
-  | Exists { variable; quantifier; body } ->
-    let variable' =
-      match List.assoc_opt variable renames with
-      | Some n -> n
-      | None -> variable
-    in
-    Exists { variable = variable'; quantifier; body = rename_vars renames body }
-  | Forall { variable; quantifier; body } ->
-    let variable' =
-      match List.assoc_opt variable renames with
-      | Some n -> n
-      | None -> variable
-    in
-    Forall { variable = variable'; quantifier; body = rename_vars renames body }
+        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))
+  in
+  loop StringSet.empty (FingerTree.singleton c) |> StringSet.elements
 
-(** Drop constraints referencing attributes not in the given set.
-    Returns [None] if the constraint cannot be kept. *)
-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)
+let rename_vars (renames : (attr_name * attr_name) list) : t -> t =
+  let rename_map = BindingMap.of_seq (List.to_seq renames) in
+  let rename_name name =
+    match BindingMap.find_opt name rename_map with Some n -> n | None -> name
+  in
+  let rec go = function
+    | 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)
+            binding BindingMap.empty
+        in
+        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 } ->
+        let variable' = rename_name variable in
+        Exists { variable = variable'; quantifier; body = go body }
+    | Forall { variable; quantifier; body } ->
+        let variable' = rename_name variable in
+        Forall { variable = variable'; quantifier; body = go body }
   in
+  go
+
+(** Drop constraints referencing attributes not in the given set. Returns [None]
+    if the constraint cannot be kept. *)
+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)
+      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)
+      let kept = List.filter_map (filter_by_attrs attrs) cs in
+      if kept = [] then None else Some (And kept)
   | Or cs ->
-    (* 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
+      (* 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)
+      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)
+      match filter_by_attrs (variable :: attrs) body with
+      | Some body' -> Some (Forall { variable; quantifier; body = body' })
+      | None -> 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
@@ -144,105 +137,99 @@ let merge (cs1 : (string * t) list) (cs2 : (string * 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 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;
+    relation_name -> (attr_name * Conventions.AbstractValue.t) list -> bool;
   iterate_finite :
-    relation_name ->
-    (attr_name * Conventions.AbstractValue.t) list list option;
+    relation_name -> (attr_name * Conventions.AbstractValue.t) list list option;
 }
 
-let bind (b : binding) (tuple : Tuple.materialized)
-    : (attr_name * Conventions.AbstractValue.t) list =
+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 =
+let rec evaluate (ctx : eval_context) (tuple : Tuple.materialized) (c : t) :
+    (bool, diagnostic) result =
   match c with
   | 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.
+      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.
        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
   | 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)
+      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 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)
-
-and extend_tuple (tuple : Tuple.materialized)
-    (variable : attr_name)
-    (row : (attr_name * Conventions.AbstractValue.t) list)
-    : Tuple.materialized =
+      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
+    =
   (* 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
@@ -272,113 +259,157 @@ let evaluate_named (ctx : eval_context) (tuple : Tuple.materialized)
         match evaluate ctx tuple c with
         | Ok true -> None
         | Ok false ->
-          Some (name, MembershipFailed { target = name; bound_values = [] })
+            Some (name, MembershipFailed { target = name; bound_values = [] })
         | Error d -> Some (name, d))
       named
   in
-  match failures with
-  | [] -> Ok true
-  | fs -> Error (ConstraintFailures fs)
+  match failures with [] -> Ok true | fs -> Error (ConstraintFailures fs)
+
+(** Fast-path evaluator: halts at the first non-passing constraint. Use in
+    cascade and deferred checking where a single violation suffices. *)
+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)
+  in
+  loop named
 
-(** Polarity analysis: determines whether each relation name appears in
-    a positive (must-exist) or negative (must-not-exist) position within
-    a constraint tree. Used for cascade checking: when a tuple is deleted,
-    only relations with Positive or Both polarity need re-validation. *)
+(** Polarity analysis: determines whether each relation name appears in a
+    positive (must-exist) or negative (must-not-exist) position within a
+    constraint tree. Used for cascade checking: when a tuple is deleted, only
+    relations with Positive or Both polarity need re-validation. *)
 
 type polarity = Positive | Negative | Both
+type polarity_index = polarity PolarityMap.t
 
 let merge_polarity a b =
-  match a, b with
+  match (a, b) with
   | Positive, Positive -> Positive
   | Negative, Negative -> Negative
-  | _                  -> Both
+  | _ -> Both
 
 let flip_polarity = function
   | Positive -> Negative
   | Negative -> Positive
-  | Both     -> Both
-
-let merge_polarity_maps m1 m2 =
-  List.fold_left (fun acc (name, pol) ->
-    match List.assoc_opt name acc with
-    | None      -> (name, pol) :: acc
-    | Some prev ->
-      (name, merge_polarity prev pol)
-      :: List.filter (fun (n, _) -> n <> name) acc)
-    m1 m2
-
-let rec polarity_of ?(neg = false) (c : t) : (relation_name * polarity) list =
-  let pos p = if neg then flip_polarity p else p in
-  match c with
-  | MemberOf { target; _ } ->
-    [(target, pos Positive)]
-  | Not { body; _ } ->
-    polarity_of ~neg:(not neg) body
-  | And cs | Or cs ->
-    List.fold_left (fun acc c ->
-      merge_polarity_maps acc (polarity_of ~neg c)) [] cs
-  | Exists { quantifier; body; _ } ->
-    merge_polarity_maps
-      [(quantifier, pos Positive)]
-      (polarity_of ~neg body)
-  | Forall { quantifier; body; _ } ->
-    merge_polarity_maps
-      [(quantifier, pos Negative)]
-      (polarity_of ~neg body)
+  | 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
+  let add_pol acc name pol =
+    match PolarityMap.find_opt name acc with
+    | None -> PolarityMap.add name pol acc
+    | Some prev -> PolarityMap.add name (merge_polarity prev pol) acc
+  in
+  let rec loop acc worklist =
+    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)))
+  in
+  loop PolarityMap.empty (FingerTree.singleton (neg, c))
+
+let polarity_find name (pols : polarity_index) = PolarityMap.find_opt name pols
 
 (** Constraint timing: immediate (checked on every mutation) or deferred
     (checked at transaction commit). *)
 type timing = Immediate | Deferred
 
+type substitute_mode =
+  | SubstituteGo
+  | SubstituteApply of Conventions.AbstractValue.t BindingMap.t
+
+type substitute_instr =
+  | Visit of substitute_mode * t
+  | BuildNot of relation_name
+  | BuildAnd of int
+  | BuildOr of int
+  | BuildExists of attr_name * relation_name
+  | BuildForall of attr_name * relation_name
+
 (** Given a constraint, a deleted relation name [dep_rel], and the deleted
-    tuple's attributes, return a filter: [(attr_name, value)] pairs that
-    narrow which constrained-relation tuples could be affected.
+    tuple's attributes, return a filter: [(attr_name, value)] pairs that narrow
+    which constrained-relation tuples could be affected.
 
-    For a Var binding like [dept_id = Var "dept_id"] targeting [dep_rel],
-    the deleted tuple's [dept_id] value becomes the filter: only constrained
-    tuples with that exact [dept_id] need re-checking.
+    For a Var binding like [dept_id = Var "dept_id"] targeting [dep_rel], the
+    deleted tuple's [dept_id] value becomes the filter: only constrained tuples
+    with that exact [dept_id] need re-checking.
 
     Returns [] if no narrowing is possible (Const bindings, unrelated rel). *)
-let rec focused_filter (c : t) (dep_rel : relation_name)
-    (deleted : (attr_name * Conventions.AbstractValue.t) list)
-  : (attr_name * Conventions.AbstractValue.t) list =
-  match c with
-  | MemberOf { target; binding } when target = dep_rel ->
-    BindingMap.fold (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)
-      binding []
-  | MemberOf _ -> []
-  | Not { body; _ } -> focused_filter body dep_rel deleted
-  | And cs | Or cs ->
-    List.concat_map (fun c -> focused_filter c dep_rel deleted) cs
-  | Exists { body; _ } | Forall { body; _ } ->
-    focused_filter body dep_rel deleted
+let focused_filter (c : t) (dep_rel : relation_name)
+    (deleted : (attr_name * Conventions.AbstractValue.t) list) :
+    (attr_name * Conventions.AbstractValue.t) list =
+  let add_from_binding acc binding =
+    BindingMap.fold
+      (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)
+      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)
+  in
+  loop [] (FingerTree.singleton c)
 
 (** Extract Const binding values from a constraint for a given [dep_rel].
 
-    These are fixed-value preconditions: if the deleted tuple doesn't have
-    these exact values, the constraint cannot be violated by the deletion.
-    The cascade checker uses this to bail out early. *)
-let rec trigger_constants (c : t) (dep_rel : relation_name)
-  : (attr_name * Conventions.AbstractValue.t) list =
-  match c with
-  | MemberOf { target; binding } when target = dep_rel ->
-    BindingMap.fold (fun target_attr expr acc ->
-      match expr with
-      | Const v -> (target_attr, v) :: acc
-      | Var _   -> acc)
-      binding []
-  | MemberOf _ -> []
-  | Not { body; _ } -> trigger_constants body dep_rel
-  | And cs | Or cs ->
-    List.concat_map (fun c -> trigger_constants c dep_rel) cs
-  | Exists { body; _ } | Forall { body; _ } ->
-    trigger_constants body dep_rel
+    These are fixed-value preconditions: if the deleted tuple doesn't have these
+    exact values, the constraint cannot be violated by the deletion. The cascade
+    checker uses this to bail out early. *)
+let trigger_constants (c : t) (dep_rel : relation_name) :
+    (attr_name * Conventions.AbstractValue.t) list =
+  let add_from_binding acc binding =
+    BindingMap.fold
+      (fun target_attr expr 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)
+  in
+  loop [] (FingerTree.singleton c)
 
 (** Substitute transition tuple values into a constraint for universal variable
     substitution. When [dep_rel] is being mutated (deleted from or inserted
@@ -388,85 +419,175 @@ let rec trigger_constants (c : t) (dep_rel : relation_name)
 
     The convention that quantifier attributes are namespaced as [variable.attr]
     (established by [extend_tuple]) means base tuple [Var] references like
-    [Var "dept_id"] are never substituted, only [Var "d.dept_id"] would match
-    a quantifier variable [d] over a deleted [Department] row.
+    [Var "dept_id"] are never substituted, only [Var "d.dept_id"] would match a
+    quantifier variable [d] over a deleted [Department] row.
 
     This transforms the recheck from a full relation evaluation into a targeted
-    expression that tests only the rows affected by the transition tuple.
-    See Technique 2 in docs/incremental_constraint_checking.org. *)
-let substitute_transition
-    (c : t)
-    (dep_rel : relation_name)
-    (transition : (attr_name * Conventions.AbstractValue.t) list)
-  : t =
+    expression that tests only the rows affected by the transition tuple. See
+    Technique 2 in docs/incremental_constraint_checking.org. *)
+let substitute_transition (c : t) (dep_rel : relation_name)
+    (transition : (attr_name * Conventions.AbstractValue.t) list) : t =
+  let namespaced_subs variable =
+    List.fold_left
+      (fun acc (a, v) -> BindingMap.add (variable ^ "." ^ a) v acc)
+      BindingMap.empty transition
+  in
+  let enqueue_visit_then_build visit build rest =
+    FingerTree.cons (FingerTree.cons rest build) visit
+  in
+  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))
+        (FingerTree.empty, 0) cs
+    in
+    let prefix = FingerTree.snoc prefix (build_of_count count) in
+    FingerTree.append prefix rest
+  in
   let apply_subs subs binding =
-    BindingMap.map (function
-      | Var v -> (match List.assoc_opt v subs with
-                  | Some value -> Const value
-                  | None -> Var v)
-      | Const _ as expr -> expr)
+    BindingMap.map
+      (function
+        | Var v -> (
+            match BindingMap.find_opt v subs with
+            | Some value -> Const value
+            | None -> Var v)
+        | Const _ as expr -> expr)
       binding
   in
-  let rec sub_body subs = function
-    | MemberOf { target; binding } ->
-      MemberOf { target; binding = apply_subs subs binding }
-    | Not { body; universe } -> Not { body = sub_body subs body; universe }
-    | And cs -> And (List.map (sub_body subs) cs)
-    | Or cs  -> Or  (List.map (sub_body subs) cs)
-    | Exists { variable; quantifier; body } ->
-      Exists { variable; quantifier; body = sub_body subs body }
-    | Forall { variable; quantifier; body } ->
-      Forall { variable; quantifier; body = sub_body subs body }
+  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)
   in
-  let rec go = function
-    | MemberOf _ as leaf -> leaf
-    | 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 } ->
-      let body' =
-        if quantifier = dep_rel then
-          sub_body (List.map (fun (a, v) -> (variable ^ "." ^ a, v)) transition) body
-        else go body
-      in
-      Exists { variable; quantifier; body = body' }
-    | Forall { variable; quantifier; body } ->
-      let body' =
-        if quantifier = dep_rel then
-          sub_body (List.map (fun (a, v) -> (variable ^ "." ^ a, v)) transition) body
-        else go body
-      in
-      Forall { variable; quantifier; body = body' }
+  let rec loop instrs vals =
+    match FingerTree.front instrs with
+    | 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)
+        | 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
-  go c
+  loop (FingerTree.singleton (Visit (SubstituteGo, c))) []
 
 let make_comparison_binding ~left ~right =
-  BindingMap.empty
-  |> BindingMap.add "left" left
-  |> BindingMap.add "right" 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 }
+  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 }
+  MemberOf
+    {
+      target = "greater_than_or_equal";
+      binding = make_comparison_binding ~left ~right;
+    }
 
 let eq ~left ~right =
   MemberOf { target = "equal"; binding = make_comparison_binding ~left ~right }
 
 let neq ~left ~right =
-  MemberOf { target = "not_equal"; binding = make_comparison_binding ~left ~right }
+  MemberOf
+    { target = "not_equal"; binding = make_comparison_binding ~left ~right }
 
 let between ~value ~low ~high =
   And
-    [ 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 }
+    [
+      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;
+        };
     ]