Multigroup unified reference for hierarchical access

2 files changed, 94 insertions, 100 deletions

diff --git a/lib/constraint.ml b/lib/constraint.ml
index 05442ab..5e282c2 100644
--- a/lib/constraint.ml
+++ b/lib/constraint.ml
@@ -30,6 +30,7 @@ type t =
   | 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 }
 
 type diagnostic =
   | MembershipFailed of {
@@ -58,7 +59,10 @@ let vars_in (c : t) : attr_name list =
             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))
+            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
 
@@ -89,6 +93,9 @@ let rename_vars (renames : (attr_name * attr_name) list) : t -> t =
     | Forall { variable; quantifier; body } ->
         let variable' = rename_name variable in
         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 }
   in
   go
 
@@ -117,6 +124,7 @@ let rec filter_by_attrs (attrs : attr_name list) (c : t) : t option =
       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 =
@@ -181,6 +189,17 @@ let rec evaluate (ctx : eval_context) (tuple : Tuple.materialized) (c : t) :
       | Error d -> Error d)
   | And cs -> evaluate_and ctx tuple cs
   | Or cs -> evaluate_or ctx tuple cs
+  | 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)
+      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 })
@@ -321,7 +340,8 @@ let polarity_of ?(neg = false) (c : t) : polarity_index =
             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)))
+            loop acc' (FingerTree.cons rest (is_neg, body))
+        | Eq _ -> loop acc rest)
   in
   loop PolarityMap.empty (FingerTree.singleton (neg, c))
 
@@ -378,7 +398,8 @@ let focused_filter (c : t) (dep_rel : relation_name)
             loop acc (FingerTree.cons rest body)
         | And cs | Or cs ->
             let next = FingerTree.append (FingerTree.of_list cs) rest in
-            loop acc next)
+            loop acc next
+        | Eq _ -> loop acc rest)
   in
   loop [] (FingerTree.singleton c)
 
@@ -407,7 +428,8 @@ let trigger_constants (c : t) (dep_rel : relation_name) :
             loop acc (FingerTree.cons rest body)
         | And cs | Or cs ->
             let next = FingerTree.append (FingerTree.of_list cs) rest in
-            loop acc next)
+            loop acc next
+        | Eq _ -> loop acc rest)
   in
   loop [] (FingerTree.singleton c)
 
@@ -521,7 +543,17 @@ let substitute_transition (c : t) (dep_rel : relation_name)
                      (Visit (body_mode, body))
                      (BuildForall (variable, quantifier))
                      rest)
-                  vals)
+                  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')
@@ -570,12 +602,10 @@ let gte ~left ~right =
       binding = make_comparison_binding ~left ~right;
     }
 
-let eq ~left ~right =
-  MemberOf { target = "equal"; binding = make_comparison_binding ~left ~right }
+let eq ~left ~right = Eq { left; right }
 
 let neq ~left ~right =
-  MemberOf
-    { target = "not_equal"; binding = make_comparison_binding ~left ~right }
+  Not { body = Eq { left; right }; universe = "" }
 
 let between ~value ~low ~high =
   And
@@ -591,3 +621,58 @@ let between ~value ~low ~high =
           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)
+    =
+    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)
+          or a user-defined domain. Accept for now; full validation would
+          require looking up the target relation's schema. *)
+       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
+        | None -> false
+        | Some t ->
+        Merkle.member nm.hash t
+        && Tuple.AttributeMap.cardinal nm.attributes = n_expected
+        && List.for_all
+        (fun (attr_name, _) ->
+        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
+
+(** 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;
+  }
diff --git a/lib/constraint.mli b/lib/constraint.mli
deleted file mode 100644
index c86ef89..0000000
--- a/lib/constraint.mli
+++ /dev/null
@@ -1,91 +0,0 @@
-type relation_name = string
-type attr_name = string
-type binding_expr = Var of attr_name | Const of Conventions.AbstractValue.t
-
-module BindingMap : Map.S with type key = String.t
-
-type binding = binding_expr BindingMap.t
-
-type t =
-  | 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 }
-
-type diagnostic =
-  | MembershipFailed of {
-      target : string;
-      bound_values : (attr_name * Conventions.AbstractValue.t) list;
-    }
-  | RelationNotFound of string
-  | UnboundedQuantifier of { variable : attr_name; quantifier : relation_name }
-  | ConstraintFailures of (string * diagnostic) list
-
-val vars_in : t -> attr_name list
-val rename_vars : (attr_name * attr_name) list -> t -> t
-val filter_by_attrs : attr_name list -> t -> t option
-val merge : (string * t) list -> (string * t) list -> (string * t) list
-val member_of : target:relation_name -> binding:binding -> t
-val not_ : universe:relation_name -> t -> t
-val and_ : t list -> t
-val or_ : t list -> t
-val exists : variable:attr_name -> quantifier:relation_name -> t -> t
-val forall : variable:attr_name -> quantifier:relation_name -> t -> t
-
-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;
-}
-
-val bind :
-  binding ->
-  Tuple.materialized ->
-  (attr_name * Conventions.AbstractValue.t) list
-
-val evaluate :
-  eval_context -> Tuple.materialized -> t -> (bool, diagnostic) result
-
-val evaluate_named :
-  eval_context ->
-  Tuple.materialized ->
-  (string * t) list ->
-  (bool, diagnostic) result
-
-val evaluate_first_failure :
-  eval_context ->
-  Tuple.materialized ->
-  (string * t) list ->
-  (bool, diagnostic) result
-
-type polarity = Positive | Negative | Both
-type polarity_index
-
-val polarity_of : ?neg:bool -> t -> polarity_index
-val polarity_find : relation_name -> polarity_index -> polarity option
-
-type timing = Immediate | Deferred
-
-val focused_filter :
-  t ->
-  relation_name ->
-  (attr_name * Conventions.AbstractValue.t) list ->
-  (attr_name * Conventions.AbstractValue.t) list
-
-val trigger_constants :
-  t -> relation_name -> (attr_name * Conventions.AbstractValue.t) list
-
-val substitute_transition :
-  t -> relation_name -> (attr_name * Conventions.AbstractValue.t) list -> t
-
-val make_comparison_binding : left:binding_expr -> right:binding_expr -> binding
-val lt : left:binding_expr -> right:binding_expr -> t
-val lte : left:binding_expr -> right:binding_expr -> t
-val gt : left:binding_expr -> right:binding_expr -> t
-val gte : left:binding_expr -> right:binding_expr -> t
-val eq : left:binding_expr -> right:binding_expr -> t
-val neq : left:binding_expr -> right:binding_expr -> t
-val between : value:binding_expr -> low:binding_expr -> high:binding_expr -> t