format todos and comment improvement

1 files changed, 26 insertions, 103 deletions

diff --git a/lib/constraint.ml b/lib/constraint.ml
index b7844eb..42f8f88 100644
--- a/lib/constraint.ml
+++ b/lib/constraint.ml
@@ -7,10 +7,14 @@
     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
+   (e.g. "natural_natural_less_than"). These constructors are currently dead
+   code and will fail at runtime if used. *)
+
 type relation_name = string
 type attr_name = string
 
-(** Binding expressions resolve against a tuple's attributes *)
 type binding_expr =
   | Var of attr_name
   | Const of Conventions.AbstractValue.t
@@ -27,10 +31,6 @@ type t =
   | Exists of { variable : attr_name; quantifier : relation_name; body : t }
   | Forall of { variable : attr_name; quantifier : relation_name; body : t }
 
-(* ============================================================================
-   Diagnostics
-   ============================================================================ *)
-
 type diagnostic =
   | MembershipFailed of {
       target : string;
@@ -43,11 +43,6 @@ type diagnostic =
     }
   | ConstraintFailures of (string * diagnostic) list
 
-(* ============================================================================
-   Utility functions
-   ============================================================================ *)
-
-(** Collect all [Var] names referenced in a constraint *)
 let rec vars_in : t -> attr_name list = function
   | MemberOf { binding; _ } ->
     BindingMap.fold
@@ -63,7 +58,6 @@ let rec vars_in : t -> attr_name list = function
     if List.mem variable inner then inner
     else variable :: inner
 
-(** Rename [Var] references according to a rename list *)
 let rec rename_vars (renames : (attr_name * attr_name) list) : t -> t = function
   | MemberOf { target; binding } ->
     let binding' =
@@ -94,16 +88,14 @@ let rec rename_vars (renames : (attr_name * attr_name) list) : t -> t = function
       | Some n -> n
       | None -> variable
     in
-    Exists
-      { variable = variable'; quantifier; body = rename_vars renames body }
+    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 }
+    Forall { variable = variable'; quantifier; body = rename_vars renames body }
 
 (** Drop constraints referencing attributes not in the given set.
     Returns [None] if the constraint cannot be kept. *)
@@ -121,7 +113,7 @@ let rec filter_by_attrs (attrs : attr_name list) (c : t) : t option =
     let kept = List.filter_map (filter_by_attrs attrs) cs in
     if kept = [] then None else Some (And kept)
   | Or cs ->
-    (* For Or, all branches must survive *)
+    (* 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 } -> (
@@ -133,11 +125,9 @@ let rec filter_by_attrs (attrs : attr_name list) (c : t) : t option =
     | Some body' -> Some (Forall { variable; quantifier; body = body' })
     | None -> None)
 
-(** AND-merge two named constraint lists *)
 let merge (cs1 : (string * t) list) (cs2 : (string * t) list)
     : (string * t) list =
   let combined = cs1 @ cs2 in
-  (* Group by name and AND-merge duplicates *)
   let tbl = Hashtbl.create 16 in
   List.iter
     (fun (name, c) ->
@@ -151,33 +141,12 @@ let merge (cs1 : (string * t) list) (cs2 : (string * t) list)
       (name, merged) :: acc)
     tbl []
 
-(* ============================================================================
-   Smart constructors
-   ============================================================================ *)
-
 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 }
-
-(* ============================================================================
-   Evaluation context (no dependency on Relation/Database/Manipulation)
-   ============================================================================ *)
+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 :
@@ -189,11 +158,6 @@ type eval_context = {
     (attr_name * Conventions.AbstractValue.t) list list option;
 }
 
-(* ============================================================================
-   Binding resolution
-   ============================================================================ *)
-
-(** Resolve binding expressions against a materialized tuple *)
 let bind (b : binding) (tuple : Tuple.materialized)
     : (attr_name * Conventions.AbstractValue.t) list =
   BindingMap.fold
@@ -211,13 +175,6 @@ let bind (b : binding) (tuple : Tuple.materialized)
       | None -> acc)
     b []
 
-(* ============================================================================
-   Constraint evaluation
-   ============================================================================ *)
-
-(** Evaluate a constraint against a tuple in the given context.
-    Returns [Ok true] if satisfied, [Ok false] should not occur —
-    failures return [Error diagnostic]. *)
 let rec evaluate (ctx : eval_context) (tuple : Tuple.materialized) (c : t)
     : (bool, diagnostic) result =
   match c with
@@ -227,9 +184,8 @@ let rec evaluate (ctx : eval_context) (tuple : Tuple.materialized) (c : t)
     else Error (MembershipFailed { target; bound_values })
   | Not { body; universe = _ } ->
     (* The universe is a declarative annotation for closed-world reasoning.
-       At runtime, we simply negate the body. The universe ensures logical
-       soundness at the schema level, not as a runtime tuple-existence check
-       (the tuple being validated hasn't been stored yet). *)
+       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
@@ -239,13 +195,11 @@ let rec evaluate (ctx : eval_context) (tuple : Tuple.materialized) (c : t)
   | Or cs -> evaluate_or ctx tuple cs
   | Exists { variable; quantifier; body } -> (
     match ctx.iterate_finite quantifier with
-    | None ->
-      Error (UnboundedQuantifier { variable; quantifier })
+    | None -> Error (UnboundedQuantifier { variable; quantifier })
     | Some rows ->
       let rec check = function
         | [] -> Ok false
         | row :: rest ->
-          (* Bind the quantifier variable into scope *)
           let extended_tuple = extend_tuple tuple variable row in
           (match evaluate ctx extended_tuple body with
            | Ok true -> Ok true
@@ -255,8 +209,7 @@ let rec evaluate (ctx : eval_context) (tuple : Tuple.materialized) (c : t)
       check rows)
   | Forall { variable; quantifier; body } -> (
     match ctx.iterate_finite quantifier with
-    | None ->
-      Error (UnboundedQuantifier { variable; quantifier })
+    | None -> Error (UnboundedQuantifier { variable; quantifier })
     | Some rows ->
       let rec check = function
         | [] -> Ok true
@@ -286,9 +239,6 @@ and evaluate_or ctx tuple = function
     | Ok false -> evaluate_or ctx tuple rest
     | Error _ -> evaluate_or ctx tuple rest)
 
-(** Extend a tuple with bindings from a quantifier row.
-    Each row entry [(attr, value)] gets added with [variable] as prefix
-    if the attr name doesn't match an existing attribute. *)
 and extend_tuple (tuple : Tuple.materialized)
     (_variable : attr_name)
     (row : (attr_name * Conventions.AbstractValue.t) list)
@@ -301,7 +251,6 @@ and extend_tuple (tuple : Tuple.materialized)
   in
   { tuple with attributes = extra_attrs }
 
-(** Evaluate a list of named constraints, collecting all failures *)
 let evaluate_named (ctx : eval_context) (tuple : Tuple.materialized)
     (named : (string * t) list) : (bool, diagnostic) result =
   let failures =
@@ -318,59 +267,33 @@ let evaluate_named (ctx : eval_context) (tuple : Tuple.materialized)
   | [] -> Ok true
   | fs -> Error (ConstraintFailures fs)
 
-(* ============================================================================
-   Comparison shorthand constructors
-   ============================================================================ *)
-
 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 }
+  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 }
+  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 }
     ]