diff options
Diffstat (limited to '')
| -rw-r--r-- | lib/constraint.ml | 103 | ||||
| -rw-r--r-- | lib/constraint.mli | 91 |
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 |