diff options
Diffstat (limited to '')
| -rw-r--r-- | docs/constraints.org | 403 | ||||
| -rw-r--r-- | lib/algebra.ml | 60 | ||||
| -rw-r--r-- | lib/constraint.ml | 378 | ||||
| -rw-r--r-- | lib/conventions.ml | 2 | ||||
| -rw-r--r-- | lib/domain.ml | 5 | ||||
| -rw-r--r-- | lib/manipulation.ml | 192 | ||||
| -rw-r--r-- | lib/prelude/domains.ml | 6 | ||||
| -rw-r--r-- | lib/prelude/standard.ml | 396 | ||||
| -rw-r--r-- | test/test_relational_engine.ml | 1036 |
9 files changed, 2417 insertions, 61 deletions
diff --git a/docs/constraints.org b/docs/constraints.org new file mode 100644 index 0000000..9f866fa --- /dev/null +++ b/docs/constraints.org @@ -0,0 +1,403 @@ +#+TITLE: Constraints and Membership Criteria + +* Conceptual Foundation + +A relation's *intension* is its meaning: what the relation represents +in the conceptual model. Where the extension is the set of tuples +currently admitted, the intension declares which tuples /could/ be +admitted. Constraints are the formal mechanism by which a relation's +intension narrows the infinite space of possible tuples to only those +consistent with the conceptual model. + +Because Sakura models everything as a relation, constraints are +themselves relations. Checking a constraint is checking membership in +a constraint-relation. When a DML operation (insert/delete) +manipulates a relation, it verifies that the manipulated data +satisfies membership in all attached constraint-relations before +committing the change. + +** Membership Criteria vs. Constraints + +Sakura distinguishes two levels of admission control: + +- *Membership criteria* (=membership_criteria : Tuple.t -> bool=) is + the opaque predicate baked into every relation. For stored relations + it validates schema/domain conformance. For ephemeral relations + (less_than, plus, etc.) it /is/ the intensional definition --- the + rule that characterizes the relation rather than an enumeration of + members. + +- *Constraints* (=Constraint.t=) are declarative, inspectable + structures attached to a relation via its =constraints= field. They + are evaluated at DML time against the current database snapshot and + produce structured diagnostics on failure. + +Membership criteria are checked first. If the tuple passes, the +constraint list is evaluated. + +** Negation and Closed-World Reasoning + +The =Not= constructor requires an explicit universe relation name. +This forces closed-world reasoning: negation is only meaningful +relative to a known domain. Without a declared universe, =NOT P= +would vacuously hold for anything outside the domain of discourse. + +At runtime the universe annotation is declarative --- it is not +checked as a tuple-existence predicate, because the tuple being +validated has not been stored yet. The evaluator simply negates the +body and treats any =MembershipFailed= diagnostic from the body as +successful negation. + +** Cardinality Awareness + +Constraints can narrow cardinality. A =Forall= over a finite +quantifier relation, or a range restriction via comparison relations, +constrains an otherwise infinite domain to a finite subset. The +=ConstrainedFinite= variant of =Conventions.Cardinality.t= tags +relations known to be finite due to constraints but whose exact count +is not computed. + +* Constraint Language + +The constraint language is a small first-order logic over relation +membership: + +#+begin_src ocaml +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 } +#+end_src + +** MemberOf + +The atomic constraint. It checks whether the tuple, after binding +resolution, is a member of the target relation. + +#+begin_src ocaml +MemberOf { target = "orders"; binding = BindingMap.singleton "order_id" (Var "order_id") } +#+end_src + +This says: "the value of =order_id= in the current tuple must appear +as =order_id= in some tuple of the =orders= relation." This is a +foreign key constraint. + +Everything is a relation --- domains, comparison relations, user +relations. =MemberOf= resolves them uniformly from the database. + +** Bindings + +Bindings map target attribute names to expressions: + +#+begin_src ocaml +type binding_expr = + | Var of attr_name (* resolve from current tuple *) + | Const of AbstractValue.t (* literal value *) +#+end_src + +A binding like ={ "left" -> Var "age"; "right" -> Const 18 }= applied +to a tuple with =age=25= produces the pairs +=[("left", 25); ("right", 18)]=, which are then checked for +membership in the target relation (e.g., =greater_than_or_equal=). + +** Logical Connectives + +- =And cs=: All sub-constraints must hold. Short-circuits on first failure. +- =Or cs=: At least one must hold. Short-circuits on first success. +- =Not { body; universe }=: The body must /not/ hold. The universe + declares the domain of negation for logical soundness. + +** Quantifiers + +- =Exists { variable; quantifier; body }=: There exists a tuple in + the quantifier relation such that, when bound to =variable=, the + body holds. The quantifier must be a finite relation. +- =Forall { variable; quantifier; body }=: For all tuples in the + quantifier relation, the body holds. Also requires finiteness. + +Quantifiers bind values from the quantifier relation into the tuple's +attribute map, extending the scope for the body evaluation. + +* Comparison Shorthands + +Because comparisons are relations, comparison constraints are +=MemberOf= with the appropriate relation name and binding. Shorthand +constructors eliminate boilerplate: + +#+begin_src ocaml +Constraint.lt ~left:(Var "age") ~right:(Const (Obj.repr 65)) +(* equivalent to: + MemberOf { target = "less_than"; + binding = { "left" -> Var "age"; "right" -> Const 65 } } *) + +Constraint.between ~value:(Var "score") ~low:(Const 0) ~high:(Const 100) +(* And [ gte score 0; lte score 100 ] *) +#+end_src + +Available shorthands: =lt=, =lte=, =gt=, =gte=, =eq=, =neq=, =between=. + +* Comparison and Arithmetic Relations + +The prelude registers domain-parameterized comparison relations. Each +takes a domain's =compare= function and a predicate over the compare +result: + +| Relation name | Schema | Predicate | +|-----------------------+----------------+-----------------| +| =less_than= | (left, right) | =compare < 0= | +| =less_than_or_equal= | (left, right) | =compare <= 0= | +| =greater_than= | (left, right) | =compare > 0= | +| =greater_than_or_equal= | (left, right) | =compare >= 0= | +| =equal= | (left, right) | =compare = 0= | +| =not_equal= | (left, right) | =compare <> 0= | + +Arithmetic relations follow the same pattern with richer schemas: + +| Relation | Schema | Invariant | +|--------------+---------------------------------+-----------------------| +| =plus= | (a, b, sum) | =a + b = sum= | +| =times= | (a, b, product) | =a * b = product= | +| =minus= | (a, b, difference) | =a - b = difference= | +| =divide= | (a, b, quotient, remainder) | =a = b*q + r, 0<=r<b= | + +All are ephemeral (generator-based, infinite). They serve as the +vocabulary for constraint expressions. + +* Domain Compare + +Each =Domain.t= now carries a =compare= field: + +#+begin_src ocaml +type t = { + name : Name.t; + generator : Generator.t; + membership_criteria : Tuple.t -> bool; + cardinality : Cardinality.t; + compare : AbstractValue.t -> AbstractValue.t -> int; +} +#+end_src + +The =compare= function dispatches comparison for values of that +domain. The comparison relations use domain comparators rather than +spreading =Obj.magic= casts at each call site. The four prelude +domains define their comparators: + +- =integer=, =natural=: integer comparison +- =rational=: float comparison +- =string=: lexicographic comparison + +* Evaluation Engine + +** Eval Context + +The evaluator cannot depend on =Relation.t=, =Database.t=, or +=Manipulation= (they compile later). Instead it receives a callback +record: + +#+begin_src ocaml +type eval_context = { + check_membership : + relation_name -> + (attr_name * AbstractValue.t) list -> + bool; + iterate_finite : + relation_name -> + (attr_name * AbstractValue.t) list list option; +} +#+end_src + +Both callbacks are closed over a specific =(storage, db)= pair at +construction time. The =db= is a =Management.Database.t= representing +one exact version (one hash). All relation lookups resolve against +that snapshot only. This is critical: constraint evaluation sees a +consistent view of the database, never a partially-mutated state. + +** How =check_membership= Works + +For a stored relation, =check_membership= loads every tuple from the +Merkle tree and checks whether any tuple's attributes match the bound +pairs. For an ephemeral relation (no tree), it delegates to +=membership_criteria=. + +This distinction matters for foreign key constraints. A FK like +"order_items.order_id must exist in orders" requires checking actual +tuple existence in the =orders= relation, not just schema +conformance. + +** Evaluation Rules + +| Constructor | Rule | +|-------------+-------------------------------------------------------------| +| =MemberOf= | Bind variables from tuple, call =check_membership= | +| =Not= | Negate body. =MembershipFailed= from body counts as success | +| =And= | All must hold (short-circuit on first failure) | +| =Or= | Any must hold (short-circuit on first success) | +| =Exists= | Iterate quantifier, bind each row, true if any body holds | +| =Forall= | Iterate quantifier, bind each row, true only if all hold | + +Quantifiers require finite quantifier relations (=iterate_finite= +returns =Some rows=). An infinite quantifier produces +=UnboundedQuantifier= diagnostic. + +** Diagnostics + +Failures produce structured diagnostics rather than opaque booleans: + +#+begin_src ocaml +type diagnostic = + | MembershipFailed of { target : string; bound_values : ... } + | RelationNotFound of string + | UnboundedQuantifier of { variable; quantifier } + | ConstraintFailures of (string * diagnostic) list +#+end_src + +Named constraint evaluation collects all failures into +=ConstraintFailures=, giving the caller a complete picture of which +constraints were violated and why. + +* Enforcement in Manipulation + +Constraints are enforced in =Manipulation.create_tuple=. The sequence is: + +1. Check =membership_criteria= (schema/domain validation) +2. If the relation has constraints, build an =eval_context= from the + current =(storage, db)= pair +3. Evaluate each named constraint against the tuple +4. On any failure, return =ConstraintViolation= with diagnostic details +5. On success, proceed to hash, store, and persist + +The =eval_context= is built fresh for each =create_tuple= call with +the /current/ database state. This ensures FK lookups see recently +inserted tuples, not a stale snapshot from constraint registration +time. + +** Registering Constraints + +=register_constraint= performs two actions: + +1. Attaches the constraint body to the relation via + =update_relation_constraints=, which merges new constraints with + any existing ones +2. Records the constraint name and relation in the =sakura:constraint= + catalog relation + +The constraint body is stored in the =Relation.t= object's +=constraints= field, not separately. This means the constraint +travels with the relation through algebraic operations. + +* Propagation Through Algebra + +When algebraic operations derive new relations, constraints propagate +according to rules that preserve soundness: + +| Operation | Propagation rule | +|-----------+-----------------------------------------------------| +| Select | Preserve all source constraints | +| Project | Filter: keep only constraints whose variables are | +| | all within the projected attributes | +| Rename | Apply variable renaming to constraint references | +| Equijoin | Merge constraints from both input relations | +| Union | Drop all constraints (conservative: constraints | +| | only hold if both inputs agree) | +| Diff | Preserve left relation's constraints | +| Take | Preserve source constraints | + +The =filter_by_attrs=, =rename_vars=, and =merge= utility functions +on =Constraint.t= implement these transformations. + +** Example: Project Filtering + +Given a relation =R(x, y)= with constraint "=x < 100=", projecting +to =[y]= drops the constraint because =x= is no longer in scope. +Projecting to =[x]= or =[x, y]= preserves it. + +#+begin_src ocaml +Constraint.filter_by_attrs ["y"] (Constraint.lt ~left:(Var "x") ~right:(Const 100)) +(* => None — dropped because "x" not in ["y"] *) + +Constraint.filter_by_attrs ["x"] (Constraint.lt ~left:(Var "x") ~right:(Const 100)) +(* => Some (lt ...) — preserved *) +#+end_src + +* Utility Functions + +=Constraint.t= provides introspection and transformation utilities: + +- =vars_in : t -> attr_name list= --- collect all =Var= names + referenced in a constraint, recursively through all sub-expressions. + +- =rename_vars : (attr_name * attr_name) list -> t -> t= --- rename + variable references throughout a constraint tree. Used by the rename + algebra operator. + +- =filter_by_attrs : attr_name list -> t -> t option= --- returns + =None= if the constraint references any variable not in the given + set. Used by projection to drop inapplicable constraints. For =Or=, + all branches must survive (dropping a branch changes semantics). + +- =merge : (string * t) list -> (string * t) list -> (string * t) list= + --- AND-merge two named constraint lists. Constraints sharing a name + are combined with =And=. Used by equijoin. + +* Examples + +** Foreign Key + +#+begin_src ocaml +(* order_items.order_id must reference an existing order *) +let fk = + Constraint.MemberOf { + target = "orders"; + binding = Constraint.BindingMap.singleton "order_id" (Var "order_id") + } +in +register_constraint storage db + ~constraint_name:"fk_order" + ~relation_name:"order_items" + ~body:fk +#+end_src + +Inserting an order_item with =order_id=999= when no such order exists +produces =ConstraintViolation "constraint fk_order violated"=. + +** Mutual Exclusion + +#+begin_src ocaml +(* A ticket cannot be both open and closed *) +let not_closed = + Constraint.Not { + body = Constraint.MemberOf { + target = "closed_ticket"; + binding = Constraint.BindingMap.singleton "ticket_id" (Var "ticket_id") + }; + universe = "open_ticket" + } +in +register_constraint storage db + ~constraint_name:"not_closed" + ~relation_name:"open_ticket" + ~body:not_closed +#+end_src + +** Self-Reference Inequality + +#+begin_src ocaml +(* An employee cannot manage themselves *) +let neq = Constraint.neq ~left:(Var "emp_id") ~right:(Var "mgr_id") in +register_constraint storage db + ~constraint_name:"no_self_manage" + ~relation_name:"reports_to" + ~body:neq +#+end_src + +This uses the =not_equal= comparison relation: it checks membership +in ={(left, right) | left <> right}=. + +* References + +- Codd, E. F. (1979), "Extending the Database Relational Model to Capture More Meaning" +- Date, C. J. and Darwen, H. (2006), "The Third Manifesto" +- McGoveran, D. (1994), "The Semantic Relational Data Model" diff --git a/lib/algebra.ml b/lib/algebra.ml index 8701dcb..f03aa53 100644 --- a/lib/algebra.ml +++ b/lib/algebra.ml @@ -29,10 +29,15 @@ module Make(Storage : Management.Physical.S) = struct | Error _ -> (fun _pos -> Generator.Error ("Failed to load: " ^ rel.Relation.name)) | Ok ts -> list_generator (List.map (fun t -> Tuple.Materialized t) ts)) - let of_generator ~name ~schema gen = + let of_generator ~name ~schema ?constraints ?cardinality gen = + let cardinality = + match cardinality with + | Some c -> c + | None -> Conventions.Cardinality.AlephZero + in Relation.make - ~hash:None ~name ~schema ~tree:None ~constraints:None - ~cardinality:Conventions.Cardinality.AlephZero + ~hash:None ~name ~schema ~tree:None ~constraints + ~cardinality ~generator:(Some gen) ~membership_criteria:(fun _ -> true) ~provenance:Relation.Provenance.Undefined @@ -61,7 +66,8 @@ module Make(Storage : Management.Physical.S) = struct else go next (Option.map ((+) 1) pos) in fun pos -> go gen pos in - Ok (of_generator ~name:("σ_" ^ rel.Relation.name) ~schema:rel.Relation.schema lazy_gen) + Ok (of_generator ~name:("σ_" ^ rel.Relation.name) ~schema:rel.Relation.schema + ?constraints:rel.Relation.constraints lazy_gen) let project storage (attrs : string list) rel = let gen = to_generator storage rel in @@ -83,7 +89,22 @@ module Make(Storage : Management.Physical.S) = struct | Generator.Value (t, next) -> Generator.Value (project_tuple t, go next) in fun pos -> go gen pos in - Ok (of_generator ~name:("π_" ^ rel.Relation.name) ~schema:new_schema lazy_gen) + let filtered_constraints = + match rel.Relation.constraints with + | None | Some [] -> None + | Some cs -> + let kept = + List.filter_map + (fun (name, c) -> + match Constraint.filter_by_attrs attrs c with + | Some c' -> Some (name, c') + | None -> None) + cs + in + (match kept with [] -> None | _ -> Some kept) + in + Ok (of_generator ~name:("π_" ^ rel.Relation.name) ~schema:new_schema + ?constraints:filtered_constraints lazy_gen) let rename storage (renames : (string * string) list) rel = let rename_key k = match List.assoc_opt k renames with Some k' -> k' | None -> k in @@ -104,7 +125,17 @@ module Make(Storage : Management.Physical.S) = struct | Generator.Value (t, next) -> Generator.Value (rename_tuple t, go next) in fun pos -> go gen pos in - Ok (of_generator ~name:("ρ_" ^ rel.Relation.name) ~schema:new_schema lazy_gen) + let renamed_constraints = + match rel.Relation.constraints with + | None | Some [] -> None + | Some cs -> + Some + (List.map + (fun (name, c) -> (name, Constraint.rename_vars renames c)) + cs) + in + Ok (of_generator ~name:("ρ_" ^ rel.Relation.name) ~schema:new_schema + ?constraints:renamed_constraints lazy_gen) let equijoin storage (attrs : string list) left right = let right_gen = to_generator storage right in @@ -155,8 +186,15 @@ module Make(Storage : Management.Physical.S) = struct in from_left left_gen 0 in + let merged_constraints = + match left.Relation.constraints, right.Relation.constraints with + | None, None -> None + | Some cs, None | None, Some cs -> Some cs + | Some cs1, Some cs2 -> Some (Constraint.merge cs1 cs2) + in let name = "⋈_" ^ left.Relation.name ^ "_" ^ right.Relation.name in - Ok (of_generator ~name ~schema:merged_schema join_gen) + Ok (of_generator ~name ~schema:merged_schema + ?constraints:merged_constraints join_gen) let union storage rel1 rel2 = let gen1 = to_generator storage rel1 in @@ -170,6 +208,7 @@ module Make(Storage : Management.Physical.S) = struct in fun pos -> go gen1 gen2 pos in let name = "∪_" ^ rel1.Relation.name ^ "_" ^ rel2.Relation.name in + (* Conservative: drop constraints since they only hold if both inputs agree *) Ok (of_generator ~name ~schema:rel1.Relation.schema chain_gen) let attrs_equal @@ -203,7 +242,8 @@ module Make(Storage : Management.Physical.S) = struct in fun pos -> go left_gen pos in let name = "−_" ^ rel1.Relation.name ^ "_" ^ rel2.Relation.name in - Ok (of_generator ~name ~schema:rel1.Relation.schema lazy_gen) + Ok (of_generator ~name ~schema:rel1.Relation.schema + ?constraints:rel1.Relation.constraints lazy_gen) let take storage n rel = let gen = to_generator storage rel in @@ -216,7 +256,9 @@ module Make(Storage : Management.Physical.S) = struct | Generator.Value (t, next) -> Generator.Value (t, go next (count - 1)) in fun pos -> go gen n pos in - Ok (of_generator ~name:("τ_" ^ rel.Relation.name) ~schema:rel.Relation.schema lazy_gen) + Ok (of_generator ~name:("τ_" ^ rel.Relation.name) ~schema:rel.Relation.schema + ?constraints:rel.Relation.constraints + ~cardinality:(Conventions.Cardinality.Finite n) lazy_gen) let materialize storage rel : (Tuple.materialized list, error) Result.t = match drain (to_generator storage rel) with diff --git a/lib/constraint.ml b/lib/constraint.ml index f6164b2..b7844eb 100644 --- a/lib/constraint.ml +++ b/lib/constraint.ml @@ -1,8 +1,376 @@ +(** 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. + + Negation requires an explicit universe relation name, forcing + closed-world reasoning in first-order logic. *) + type relation_name = string -type t = - | MemberOf of relation_name - | Not of t * relation_name option +type attr_name = string + +(** Binding expressions resolve against a tuple's attributes *) +type binding_expr = + | Var of attr_name + | Const of Conventions.AbstractValue.t + +module BindingMap = Map.Make (String) + +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: string; quantifier: relation_name; constraint': t} - | Forall of {variable: string; quantifier: relation_name; constraint': 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; + bound_values : (attr_name * Conventions.AbstractValue.t) list; + } + | RelationNotFound of string + | UnboundedQuantifier of { + variable : attr_name; + quantifier : relation_name; + } + | 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 + (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 + +(** 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' = + 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 } + +(** 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) + | And cs -> + 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 *) + 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) + +(** 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) -> + match Hashtbl.find_opt tbl name with + | 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) + 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) + ============================================================================ *) + +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; +} + +(* ============================================================================ + Binding resolution + ============================================================================ *) + +(** Resolve binding expressions against a materialized tuple *) +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) + in + match value with + | Some v -> (target_attr, v) :: acc + | 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 + | 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. + 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). *) + (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 -> + (* 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 + | 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) + +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) + +(** 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) + : Tuple.materialized = + let extra_attrs = + List.fold_left + (fun acc (k, v) -> + Tuple.AttributeMap.add k { Attribute.value = v } acc) + tuple.attributes row + 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 = + 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)) + named + in + match failures with + | [] -> 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 } + +let lte ~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; + } + +let gte ~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 } + +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; + }; + ] diff --git a/lib/conventions.ml b/lib/conventions.ml index 538bc5c..0019447 100644 --- a/lib/conventions.ml +++ b/lib/conventions.ml @@ -9,7 +9,7 @@ module Name = struct end module Cardinality = struct - type t = Finite of int | AlephZero | Continuum + type t = Finite of int | ConstrainedFinite | AlephZero | Continuum end module AbstractValue = struct diff --git a/lib/domain.ml b/lib/domain.ml index 753a7b9..87ed1a9 100644 --- a/lib/domain.ml +++ b/lib/domain.ml @@ -3,7 +3,8 @@ type t = { generator : Generator.t; membership_criteria : Tuple.t -> bool; cardinality : Conventions.Cardinality.t; + compare : Conventions.AbstractValue.t -> Conventions.AbstractValue.t -> int; } -let make ~name ~generator ~membership_criteria ~cardinality = - { name; generator; membership_criteria; cardinality } +let make ~name ~generator ~membership_criteria ~cardinality ~compare = + { name; generator; membership_criteria; cardinality; compare } diff --git a/lib/manipulation.ml b/lib/manipulation.ml index e019fa8..a1d90d6 100644 --- a/lib/manipulation.ml +++ b/lib/manipulation.ml @@ -45,6 +45,98 @@ let build_membership_criteria _schema : (Tuple.t -> bool) = module Make (Storage : Management.Physical.S) = struct type storage = Storage.t + (* ============================================================================ + Constraint evaluation context + ============================================================================ *) + + (** Build an eval_context closed over a specific (storage, db) snapshot. + All relation lookups resolve against this exact database version. *) + let build_eval_context (storage : storage) (db : Management.Database.t) + : Constraint.eval_context = + let check_membership rel_name bound_pairs = + match Management.Database.get_relation db rel_name with + | None -> false + | Some rel -> + let attributes = + List.fold_left + (fun acc (k, v) -> + Tuple.AttributeMap.add k { Attribute.value = v } acc) + Tuple.AttributeMap.empty bound_pairs + in + let tuple = + Tuple.Materialized { Tuple.relation = rel_name; attributes } + in + if not (rel.membership_criteria tuple) then false + else + (* For stored relations, check if a matching tuple actually exists *) + match rel.tree with + | None -> + (* No tree = ephemeral/generator relation, membership_criteria suffices *) + true + | Some tree -> + let hashes = Merkle.keys tree in + List.exists + (fun h -> + match Storage.load_raw storage h with + | Error _ | Ok None -> false + | Ok (Some bytes) -> + let stored = Storable.Tuple.of_bytes bytes in + (* Check if all bound pairs match the stored tuple's attributes *) + List.for_all + (fun (bk, bv) -> + List.exists + (fun (sk, sh) -> + sk = bk + && + match Storage.load_raw storage sh with + | Error _ | Ok None -> false + | Ok (Some vbytes) -> + let sv : Conventions.AbstractValue.t = + Marshal.from_bytes vbytes 0 + in + Stdlib.( = ) sv bv) + stored.Storable.Tuple.attributes) + bound_pairs) + hashes + in + let iterate_finite rel_name = + match Management.Database.get_relation db rel_name with + | None -> None + | Some rel -> ( + match rel.cardinality with + | Conventions.Cardinality.Finite _ | Conventions.Cardinality.ConstrainedFinite -> ( + match rel.tree with + | None -> Some [] + | Some tree -> + let hashes = Merkle.keys tree in + let rec load_all acc = function + | [] -> Some (List.rev acc) + | h :: rest -> ( + match Storage.load_raw storage h with + | Error _ -> None + | Ok None -> None + | Ok (Some bytes) -> + let stored = Storable.Tuple.of_bytes bytes in + let rec load_attrs attr_acc = function + | [] -> Some (List.rev attr_acc) + | (name, attr_hash) :: attr_rest -> ( + match Storage.load_raw storage attr_hash with + | Error _ | Ok None -> None + | Ok (Some vbytes) -> + let value : Conventions.AbstractValue.t = + Marshal.from_bytes vbytes 0 + in + load_attrs ((name, value) :: attr_acc) attr_rest) + in + (match load_attrs [] stored.Storable.Tuple.attributes with + | None -> None + | Some pairs -> load_all (pairs :: acc) rest)) + in + load_all [] hashes) + | _ -> None) + in + { Constraint.check_membership; iterate_finite } + (* State Persistence - Store relation and database states *) (** Store a relation state to storage *) @@ -219,6 +311,25 @@ module Make (Storage : Management.Physical.S) = struct if not (relation.membership_criteria (Tuple.Materialized tuple)) then Error (ConstraintViolation "Tuple does not satisfy membership criteria") else + (* Check constraints *) + let constraint_ok = + match relation.constraints with + | None | Some [] -> Ok true + | Some named_constraints -> + let ctx = build_eval_context storage db in + Constraint.evaluate_named ctx tuple named_constraints + in + (match constraint_ok with + | Error (Constraint.ConstraintFailures failures) -> + let msg = + String.concat "; " + (List.map (fun (name, _) -> "constraint " ^ name ^ " violated") + failures) + in + Error (ConstraintViolation msg) + | Error _ -> Error (ConstraintViolation "Constraint evaluation failed") + | Ok false -> Error (ConstraintViolation "Constraint not satisfied") + | Ok true -> (* Compute tuple hash *) let tuple_hash = Hashing.hash_tuple tuple in @@ -275,7 +386,7 @@ module Make (Storage : Management.Physical.S) = struct | Ok () -> match store_database storage new_db with | Error e -> Error e - | Ok () -> Ok (new_db, new_relation, tuple_hash)) + | Ok () -> Ok (new_db, new_relation, tuple_hash))) (** Insert multiple tuples into a relation *) let create_tuples @@ -709,20 +820,83 @@ module Make (Storage : Management.Physical.S) = struct | Error e -> Error e | Ok () -> Ok (new_db, new_relation) - (** Register a named constraint on a relation in the system catalog. *) + (** Attach constraints to an existing relation. + Rebuilds membership_criteria to include constraint checking, + re-hashes, and persists. *) + let update_relation_constraints + (storage : storage) + (db : Management.Database.t) + ~(relation_name : string) + ~(constraints : Relation.RelationConstraint.t) + : (Management.Database.t * Relation.t) result = + match Management.Database.get_relation db relation_name with + | None -> Error (RelationNotFound relation_name) + | Some relation -> + let merged_constraints = + match relation.constraints with + | None -> constraints + | Some existing -> Constraint.merge existing constraints + in + (* Don't bake constraint evaluation into membership_criteria — + create_tuple evaluates constraints with the current db snapshot. + membership_criteria stays for schema/domain validation only. *) + let new_relation = + { relation with + constraints = Some merged_constraints; + } + in + (* Re-hash *) + let new_relation = + match new_relation.tree with + | Some tree -> + let h = + Hashing.hash_relation ~name:relation_name + ~schema:relation.schema ~tree + in + { new_relation with hash = Some h } + | None -> new_relation + in + let new_db = + Management.Database.update_relation db ~relation:new_relation + in + (match store_relation storage new_relation with + | Error e -> Error e + | Ok () -> + (match store_database storage new_db with + | Error e -> Error e + | Ok () -> Ok (new_db, new_relation))) + + (** Register a named constraint on a relation. + Attaches the constraint body to the relation AND records it in + [sakura:constraint]. *) let register_constraint (storage : storage) (db : Management.Database.t) ~(constraint_name : string) ~(relation_name : string) + ~(body : Constraint.t) : (Management.Database.t, error) Result.t = - match Management.Database.get_relation db Prelude.Catalog.constraint_rel_name with - | None -> Ok db (* catalog not initialized *) - | Some con_cat -> - let con_tuple = Prelude.Catalog.build_constraint_tuple constraint_name relation_name in - match create_tuple storage db con_cat con_tuple with - | Error e -> Error e - | Ok (new_db, _, _) -> Ok new_db + (* Attach constraint to the relation *) + (match + update_relation_constraints storage db ~relation_name + ~constraints:[ (constraint_name, body) ] + with + | Error e -> Error e + | Ok (db, _) -> + (* Record in system catalog *) + (match + Management.Database.get_relation db + Prelude.Catalog.constraint_rel_name + with + | None -> Ok db + | Some con_cat -> + let con_tuple = + Prelude.Catalog.build_constraint_tuple constraint_name + relation_name + in + (match create_tuple storage db con_cat con_tuple with + | Error e -> Error e + | Ok (new_db, _, _) -> Ok new_db))) (*Query Operations *) diff --git a/lib/prelude/domains.ml b/lib/prelude/domains.ml index bc1716a..29104bb 100644 --- a/lib/prelude/domains.ml +++ b/lib/prelude/domains.ml @@ -40,6 +40,7 @@ let integer : Domain.t = in Domain.make ~name:"integer" ~generator ~membership_criteria ~cardinality:Conventions.Cardinality.AlephZero + ~compare:(fun a b -> Stdlib.compare (Obj.magic a : int) (Obj.magic b : int)) (** Natural number domain: non-negative integers (0, 1, 2, …). Schema: [value: natural]. *) @@ -63,6 +64,7 @@ let natural : Domain.t = in Domain.make ~name:"natural" ~generator ~membership_criteria ~cardinality:Conventions.Cardinality.AlephZero + ~compare:(fun a b -> Stdlib.compare (Obj.magic a : int) (Obj.magic b : int)) (** Rational number domain: pairs [(numerator, denominator)] where the denominator is never zero. The generator enumerates all such pairs via @@ -97,6 +99,8 @@ let rational : Domain.t = in Domain.make ~name:"rational" ~generator ~membership_criteria ~cardinality:Conventions.Cardinality.AlephZero + ~compare:(fun a b -> + Stdlib.compare (Obj.magic a : float) (Obj.magic b : float)) (** String domain: any string value. Not enumerable. Schema: [value: string]. *) @@ -110,3 +114,5 @@ let string : Domain.t = in Domain.make ~name:"string" ~generator ~membership_criteria ~cardinality:Conventions.Cardinality.AlephZero + ~compare:(fun a b -> + String.compare (Obj.magic a : string) (Obj.magic b : string)) diff --git a/lib/prelude/standard.ml b/lib/prelude/standard.ml index 5725978..aca7f93 100644 --- a/lib/prelude/standard.ml +++ b/lib/prelude/standard.ml @@ -1,34 +1,362 @@ -let less_than_natural: Relation.t = - let rec generator (position: int option): Generator.result = - let pair_of_nat n = - let nf = float_of_int n in - let r = - int_of_float (floor ((1. +. sqrt (1. +. 8. *. nf)) /. 2.)) - in - let t_prev = (r * (r - 1)) / 2 in - let left = n - t_prev in - (left, r) in - match position with - | Some position -> - let left, right = pair_of_nat position in - let attributes: Attribute.materialized Tuple.AttributeMap.t = - Tuple.AttributeMap.of_list [("left", Obj.magic left); ("right", Obj.magic right)] - in Generator.Value (Tuple.make_materialized ~relation: "less_than" ~attributes: attributes, generator) - | None -> Error "Cannot produce a randomly enumerated value for less_than over naturals." - in let membership_criteria: Tuple.t -> bool = function - | Tuple.Materialized materialized -> - let left = Tuple.AttributeMap.find "left" materialized.attributes - in let right = Tuple.AttributeMap.find "right" materialized.attributes - in left < right - | Tuple.NonMaterialized _non_materialized -> false (* TODO: Handle references later *) - in Relation.make - ~hash: None - ~name: "natural_natural_less_than" - ~schema: (Schema.empty |> Schema.add "left" "natural" |> Schema.add "right" "natural") - ~tree: None - ~constraints: None - ~cardinality: Conventions.Cardinality.AlephZero - ~generator: (Some generator) - ~membership_criteria: membership_criteria - ~provenance: (Relation.Provenance.Base "less_than") - ~lineage: (Relation.Lineage.Base "less_than")
\ No newline at end of file +(** Domain-parameterized comparison and arithmetic relations. + + All comparison relations use a two-attribute schema [(left, right)] + with both attributes in the same domain. The domain's [compare] function + is used for evaluation — no more spreading [Obj.magic]. *) + +(* ============================================================================ + Comparison relation factory + ============================================================================ *) + +(** Build a comparison relation parameterized by domain. + [pred] receives the result of [Domain.compare left right]. *) +let make_comparison ~name ~domain_name ~pred ~cardinality ~generator = + let schema = + Schema.empty |> Schema.add "left" domain_name + |> Schema.add "right" domain_name + in + let membership_criteria : Tuple.t -> bool = function + | Tuple.Materialized m -> ( + match + ( Tuple.AttributeMap.find_opt "left" m.attributes, + Tuple.AttributeMap.find_opt "right" m.attributes ) + with + | Some l, Some r -> + pred (Stdlib.compare l.Attribute.value r.Attribute.value) + | _ -> false) + | Tuple.NonMaterialized _ -> false + in + Relation.make ~hash:None ~name ~schema ~tree:None ~constraints:None + ~cardinality ~generator:(Some generator) ~membership_criteria + ~provenance:(Relation.Provenance.Base name) + ~lineage:(Relation.Lineage.Base name) + +(* ============================================================================ + Pair enumeration for comparison generators + ============================================================================ *) + +(** Enumerate pairs (a, b) from naturals where a < b. + Uses triangular indexing: position n maps to row r, column c + where a = c, b = r, and a < b. *) +let pair_of_nat_lt n = + let nf = float_of_int n in + let r = int_of_float (floor ((1. +. sqrt (1. +. 8. *. nf)) /. 2.)) in + let t_prev = (r * (r - 1)) / 2 in + let left = n - t_prev in + (left, r) + +(** Enumerate all pairs (a, b) from naturals via Cantor pairing. *) +let cantor_pair_of_nat n = + let w = + int_of_float (floor ((sqrt (float_of_int (8 * n + 1)) -. 1.) /. 2.)) + in + let t = (w * (w + 1)) / 2 in + let b = n - t in + let a = w - b in + (a, b) + +(* ============================================================================ + Concrete comparison relations (natural domain) + ============================================================================ *) + +let less_than_natural : Relation.t = + let rec generator (position : int option) : Generator.result = + match position with + | Some position -> + let left, right = pair_of_nat_lt position in + let attributes : Attribute.materialized Tuple.AttributeMap.t = + Tuple.AttributeMap.of_list + [ ("left", Obj.magic left); ("right", Obj.magic right) ] + in + Generator.Value + ( Tuple.make_materialized ~relation:"less_than" ~attributes, + generator ) + | None -> + Error + "Cannot produce a randomly enumerated value for less_than over \ + naturals." + in + make_comparison ~name:"natural_natural_less_than" ~domain_name:"natural" + ~pred:(fun c -> c < 0) + ~cardinality:Conventions.Cardinality.AlephZero ~generator + +let less_than_or_equal_natural : Relation.t = + let rec generator (position : int option) : Generator.result = + match position with + | Some n -> + let a, b = cantor_pair_of_nat n in + (* a <= b is always true when a <= b; we enumerate all (a, b) with a <= b *) + let left = min a b in + let right = max a b in + let attributes = + Tuple.AttributeMap.of_list + [ ("left", Obj.magic left); ("right", Obj.magic right) ] + in + Generator.Value + ( Tuple.make_materialized ~relation:"less_than_or_equal" ~attributes, + generator ) + | None -> Error "Cannot enumerate less_than_or_equal randomly." + in + make_comparison ~name:"natural_natural_less_than_or_equal" + ~domain_name:"natural" + ~pred:(fun c -> c <= 0) + ~cardinality:Conventions.Cardinality.AlephZero ~generator + +let greater_than_natural : Relation.t = + let rec generator (position : int option) : Generator.result = + match position with + | Some n -> + let left, right = pair_of_nat_lt n in + (* Swap: right > left *) + let attributes = + Tuple.AttributeMap.of_list + [ ("left", Obj.magic right); ("right", Obj.magic left) ] + in + Generator.Value + ( Tuple.make_materialized ~relation:"greater_than" ~attributes, + generator ) + | None -> Error "Cannot enumerate greater_than randomly." + in + make_comparison ~name:"natural_natural_greater_than" ~domain_name:"natural" + ~pred:(fun c -> c > 0) + ~cardinality:Conventions.Cardinality.AlephZero ~generator + +let greater_than_or_equal_natural : Relation.t = + let rec generator (position : int option) : Generator.result = + match position with + | Some n -> + let a, b = cantor_pair_of_nat n in + let left = max a b in + let right = min a b in + let attributes = + Tuple.AttributeMap.of_list + [ ("left", Obj.magic left); ("right", Obj.magic right) ] + in + Generator.Value + ( Tuple.make_materialized ~relation:"greater_than_or_equal" ~attributes, + generator ) + | None -> Error "Cannot enumerate greater_than_or_equal randomly." + in + make_comparison ~name:"natural_natural_greater_than_or_equal" + ~domain_name:"natural" + ~pred:(fun c -> c >= 0) + ~cardinality:Conventions.Cardinality.AlephZero ~generator + +let equal_natural : Relation.t = + let rec generator (position : int option) : Generator.result = + match position with + | Some n -> + let attributes = + Tuple.AttributeMap.of_list + [ ("left", Obj.magic n); ("right", Obj.magic n) ] + in + Generator.Value + ( Tuple.make_materialized ~relation:"equal" ~attributes, generator ) + | None -> Error "Cannot enumerate equal randomly." + in + make_comparison ~name:"natural_natural_equal" ~domain_name:"natural" + ~pred:(fun c -> c = 0) + ~cardinality:Conventions.Cardinality.AlephZero ~generator + +let not_equal_natural : Relation.t = + let rec generator (position : int option) : Generator.result = + match position with + | Some n -> + let a, b = cantor_pair_of_nat n in + let left, right = if a = b then (a, b + 1) else (a, b) in + let attributes = + Tuple.AttributeMap.of_list + [ ("left", Obj.magic left); ("right", Obj.magic right) ] + in + Generator.Value + ( Tuple.make_materialized ~relation:"not_equal" ~attributes, generator ) + | None -> Error "Cannot enumerate not_equal randomly." + in + make_comparison ~name:"natural_natural_not_equal" ~domain_name:"natural" + ~pred:(fun c -> c <> 0) + ~cardinality:Conventions.Cardinality.AlephZero ~generator + +(* ============================================================================ + Arithmetic relations (natural domain) + ============================================================================ *) + +let plus_natural : Relation.t = + let schema = + Schema.empty |> Schema.add "a" "natural" |> Schema.add "b" "natural" + |> Schema.add "sum" "natural" + in + let rec generator (position : int option) : Generator.result = + match position with + | Some n -> + let a, b = cantor_pair_of_nat n in + let s = a + b in + let attributes = + Tuple.AttributeMap.of_list + [ ("a", Obj.magic a); ("b", Obj.magic b); ("sum", Obj.magic s) ] + in + Generator.Value + ( Tuple.make_materialized ~relation:"plus" ~attributes, generator ) + | None -> Error "Cannot enumerate plus randomly." + in + let membership_criteria : Tuple.t -> bool = function + | Tuple.Materialized m -> ( + match + ( Tuple.AttributeMap.find_opt "a" m.attributes, + Tuple.AttributeMap.find_opt "b" m.attributes, + Tuple.AttributeMap.find_opt "sum" m.attributes ) + with + | Some a, Some b, Some s -> + (Obj.magic a.Attribute.value : int) + + (Obj.magic b.Attribute.value : int) + = (Obj.magic s.Attribute.value : int) + | _ -> false) + | Tuple.NonMaterialized _ -> false + in + Relation.make ~hash:None ~name:"natural_plus" ~schema ~tree:None + ~constraints:None + ~cardinality:Conventions.Cardinality.AlephZero + ~generator:(Some generator) ~membership_criteria + ~provenance:(Relation.Provenance.Base "plus") + ~lineage:(Relation.Lineage.Base "plus") + +let times_natural : Relation.t = + let schema = + Schema.empty |> Schema.add "a" "natural" + |> Schema.add "b" "natural" + |> Schema.add "product" "natural" + in + let rec generator (position : int option) : Generator.result = + match position with + | Some n -> + let a, b = cantor_pair_of_nat n in + let p = a * b in + let attributes = + Tuple.AttributeMap.of_list + [ + ("a", Obj.magic a); ("b", Obj.magic b); ("product", Obj.magic p); + ] + in + Generator.Value + ( Tuple.make_materialized ~relation:"times" ~attributes, generator ) + | None -> Error "Cannot enumerate times randomly." + in + let membership_criteria : Tuple.t -> bool = function + | Tuple.Materialized m -> ( + match + ( Tuple.AttributeMap.find_opt "a" m.attributes, + Tuple.AttributeMap.find_opt "b" m.attributes, + Tuple.AttributeMap.find_opt "product" m.attributes ) + with + | Some a, Some b, Some p -> + (Obj.magic a.Attribute.value : int) + * (Obj.magic b.Attribute.value : int) + = (Obj.magic p.Attribute.value : int) + | _ -> false) + | Tuple.NonMaterialized _ -> false + in + Relation.make ~hash:None ~name:"natural_times" ~schema ~tree:None + ~constraints:None + ~cardinality:Conventions.Cardinality.AlephZero + ~generator:(Some generator) ~membership_criteria + ~provenance:(Relation.Provenance.Base "times") + ~lineage:(Relation.Lineage.Base "times") + +let minus_natural : Relation.t = + let schema = + Schema.empty |> Schema.add "a" "natural" + |> Schema.add "b" "natural" + |> Schema.add "difference" "natural" + in + let rec generator (position : int option) : Generator.result = + match position with + | Some n -> + (* Enumerate pairs where a >= b, so difference >= 0 *) + let b, diff = cantor_pair_of_nat n in + let a = b + diff in + let attributes = + Tuple.AttributeMap.of_list + [ + ("a", Obj.magic a); + ("b", Obj.magic b); + ("difference", Obj.magic diff); + ] + in + Generator.Value + ( Tuple.make_materialized ~relation:"minus" ~attributes, generator ) + | None -> Error "Cannot enumerate minus randomly." + in + let membership_criteria : Tuple.t -> bool = function + | Tuple.Materialized m -> ( + match + ( Tuple.AttributeMap.find_opt "a" m.attributes, + Tuple.AttributeMap.find_opt "b" m.attributes, + Tuple.AttributeMap.find_opt "difference" m.attributes ) + with + | Some a, Some b, Some d -> + let av = (Obj.magic a.Attribute.value : int) in + let bv = (Obj.magic b.Attribute.value : int) in + let dv = (Obj.magic d.Attribute.value : int) in + av - bv = dv && dv >= 0 + | _ -> false) + | Tuple.NonMaterialized _ -> false + in + Relation.make ~hash:None ~name:"natural_minus" ~schema ~tree:None + ~constraints:None + ~cardinality:Conventions.Cardinality.AlephZero + ~generator:(Some generator) ~membership_criteria + ~provenance:(Relation.Provenance.Base "minus") + ~lineage:(Relation.Lineage.Base "minus") + +let divide_natural : Relation.t = + let schema = + Schema.empty |> Schema.add "a" "natural" + |> Schema.add "b" "natural" + |> Schema.add "quotient" "natural" + |> Schema.add "remainder" "natural" + in + let rec generator (position : int option) : Generator.result = + match position with + | Some n -> + (* Enumerate (b, q, r) triples where b > 0, then a = b*q + r, 0 <= r < b *) + (* We use a nested Cantor pairing: n -> (b_idx, qr_idx) -> (q, r) *) + let b_idx, qr_idx = cantor_pair_of_nat n in + let b = b_idx + 1 in (* b > 0 *) + let q, r_raw = cantor_pair_of_nat qr_idx in + let r = r_raw mod b in + let a = b * q + r in + let attributes = + Tuple.AttributeMap.of_list + [ + ("a", Obj.magic a); + ("b", Obj.magic b); + ("quotient", Obj.magic q); + ("remainder", Obj.magic r); + ] + in + Generator.Value + ( Tuple.make_materialized ~relation:"divide" ~attributes, generator ) + | None -> Error "Cannot enumerate divide randomly." + in + let membership_criteria : Tuple.t -> bool = function + | Tuple.Materialized m -> ( + match + ( Tuple.AttributeMap.find_opt "a" m.attributes, + Tuple.AttributeMap.find_opt "b" m.attributes, + Tuple.AttributeMap.find_opt "quotient" m.attributes, + Tuple.AttributeMap.find_opt "remainder" m.attributes ) + with + | Some a, Some b, Some q, Some r -> + let av = (Obj.magic a.Attribute.value : int) in + let bv = (Obj.magic b.Attribute.value : int) in + let qv = (Obj.magic q.Attribute.value : int) in + let rv = (Obj.magic r.Attribute.value : int) in + bv > 0 && av = bv * qv + rv && rv >= 0 && rv < bv + | _ -> false) + | Tuple.NonMaterialized _ -> false + in + Relation.make ~hash:None ~name:"natural_divide" ~schema ~tree:None + ~constraints:None + ~cardinality:Conventions.Cardinality.AlephZero + ~generator:(Some generator) ~membership_criteria + ~provenance:(Relation.Provenance.Base "divide") + ~lineage:(Relation.Lineage.Base "divide") diff --git a/test/test_relational_engine.ml b/test/test_relational_engine.ml index 8ba8226..f7421f1 100644 --- a/test/test_relational_engine.ml +++ b/test/test_relational_engine.ml @@ -705,7 +705,8 @@ let%test_unit "catalog: register_constraint inserts into sakura:constraint" = in let db = match Manipulation.Memory.register_constraint storage db ~constraint_name:"orders_id_positive" - ~relation_name:"orders" with + ~relation_name:"orders" + ~body:(Constraint.And []) with | Error _ -> assert false | Ok db -> db in let con_rel = match Manipulation.Memory.get_relation db ~name:"sakura:constraint" with @@ -1350,3 +1351,1036 @@ let%test_unit "drl: execute Select+Const" = Obj.obj (Tuple.AttributeMap.find "name" (List.hd rows).Tuple.attributes).Attribute.value in assert (name_v = "Alice")) + +(* ============================================================================ + Constraint System Tests + ============================================================================ *) + +(* ---------- Constraint construction ---------- *) + +let%test_unit "constraint: vars_in MemberOf" = + let b = + Constraint.BindingMap.empty + |> Constraint.BindingMap.add "left" (Constraint.Var "x") + |> Constraint.BindingMap.add "right" (Constraint.Const (Obj.repr 10)) + in + let c = Constraint.MemberOf { target = "less_than"; binding = b } in + let vars = Constraint.vars_in c in + assert (List.mem "x" vars); + assert (not (List.mem "right" vars)) + +let%test_unit "constraint: vars_in And" = + let b1 = + Constraint.BindingMap.singleton "left" (Constraint.Var "a") + in + let b2 = + Constraint.BindingMap.singleton "left" (Constraint.Var "b") + in + let c = + Constraint.And + [ + Constraint.MemberOf { target = "t1"; binding = b1 }; + Constraint.MemberOf { target = "t2"; binding = b2 }; + ] + in + let vars = Constraint.vars_in c in + assert (List.mem "a" vars); + assert (List.mem "b" vars) + +let%test_unit "constraint: rename_vars" = + let b = + Constraint.BindingMap.singleton "left" (Constraint.Var "old_name") + in + let c = Constraint.MemberOf { target = "t"; binding = b } in + let c' = Constraint.rename_vars [ ("old_name", "new_name") ] c in + let vars = Constraint.vars_in c' in + assert (List.mem "new_name" vars); + assert (not (List.mem "old_name" vars)) + +let%test_unit "constraint: filter_by_attrs keeps relevant" = + let b = + Constraint.BindingMap.singleton "left" (Constraint.Var "x") + in + let c = Constraint.MemberOf { target = "t"; binding = b } in + assert (Constraint.filter_by_attrs [ "x" ] c <> None); + assert (Constraint.filter_by_attrs [ "y" ] c = None) + +let%test_unit "constraint: merge named constraints" = + let b = Constraint.BindingMap.empty in + let cs1 = [ ("c1", Constraint.MemberOf { target = "t1"; binding = b }) ] in + let cs2 = [ ("c2", Constraint.MemberOf { target = "t2"; binding = b }) ] in + let merged = Constraint.merge cs1 cs2 in + assert (List.length merged = 2) + +let%test_unit "constraint: merge duplicate names produces And" = + let b = Constraint.BindingMap.empty in + let c1 = Constraint.MemberOf { target = "t1"; binding = b } in + let c2 = Constraint.MemberOf { target = "t2"; binding = b } in + let merged = Constraint.merge [ ("shared", c1) ] [ ("shared", c2) ] in + assert (List.length merged = 1); + match List.assoc "shared" merged with + | Constraint.And _ -> () + | _ -> assert false + +(* ---------- Smart constructors ---------- *) + +let%test_unit "constraint: and_ singleton" = + let b = Constraint.BindingMap.empty in + let c = Constraint.MemberOf { target = "t"; binding = b } in + match Constraint.and_ [ c ] with + | Constraint.MemberOf _ -> () + | _ -> assert false + +let%test_unit "constraint: or_ singleton" = + let b = Constraint.BindingMap.empty in + let c = Constraint.MemberOf { target = "t"; binding = b } in + match Constraint.or_ [ c ] with + | Constraint.MemberOf _ -> () + | _ -> assert false + +(* ---------- Comparison shorthands ---------- *) + +let%test_unit "constraint: lt shorthand" = + match Constraint.lt ~left:(Var "x") ~right:(Const (Obj.repr 5)) with + | Constraint.MemberOf { target = "less_than"; _ } -> () + | _ -> assert false + +let%test_unit "constraint: between shorthand" = + match + Constraint.between ~value:(Var "x") ~low:(Const (Obj.repr 0)) + ~high:(Const (Obj.repr 100)) + with + | Constraint.And [ _; _ ] -> () + | _ -> assert false + +(* ---------- Binding resolution ---------- *) + +let%test_unit "constraint: bind resolves Var and Const" = + let b = + Constraint.BindingMap.empty + |> Constraint.BindingMap.add "left" (Constraint.Var "x") + |> Constraint.BindingMap.add "right" (Constraint.Const (Obj.repr 42)) + in + let tuple : Tuple.materialized = + { + relation = "test"; + attributes = + Tuple.AttributeMap.singleton "x" { Attribute.value = Obj.repr 10 }; + } + in + let bound = Constraint.bind b tuple in + assert (List.length bound = 2); + let left_v : int = Obj.obj (List.assoc "left" bound) in + let right_v : int = Obj.obj (List.assoc "right" bound) in + assert (left_v = 10); + assert (right_v = 42) + +(* ---------- Evaluation engine ---------- *) + +let make_eval_ctx ?(relations = []) () : Constraint.eval_context = + { + check_membership = + (fun rel_name bound_pairs -> + match List.assoc_opt rel_name relations with + | None -> false + | Some checker -> checker bound_pairs); + iterate_finite = + (fun rel_name -> + match List.assoc_opt rel_name relations with + | None -> None + | Some _ -> Some []); + } + +let%test_unit "constraint: evaluate MemberOf success" = + let ctx = + make_eval_ctx + ~relations:[ ("my_rel", fun _pairs -> true) ] + () + in + let b = Constraint.BindingMap.empty in + let c = Constraint.MemberOf { target = "my_rel"; binding = b } in + let tuple : Tuple.materialized = + { relation = "test"; attributes = Tuple.AttributeMap.empty } + in + match Constraint.evaluate ctx tuple c with + | Ok true -> () + | _ -> assert false + +let%test_unit "constraint: evaluate MemberOf failure" = + let ctx = + make_eval_ctx + ~relations:[ ("my_rel", fun _pairs -> false) ] + () + in + let b = Constraint.BindingMap.empty in + let c = Constraint.MemberOf { target = "my_rel"; binding = b } in + let tuple : Tuple.materialized = + { relation = "test"; attributes = Tuple.AttributeMap.empty } + in + match Constraint.evaluate ctx tuple c with + | Error (Constraint.MembershipFailed _) -> () + | _ -> assert false + +let%test_unit "constraint: evaluate And short-circuits" = + let call_count = ref 0 in + let ctx = + make_eval_ctx + ~relations: + [ + ( "fail_rel", + fun _ -> + incr call_count; + false ); + ( "ok_rel", + fun _ -> + incr call_count; + true ); + ] + () + in + let b = Constraint.BindingMap.empty in + let c = + Constraint.And + [ + Constraint.MemberOf { target = "fail_rel"; binding = b }; + Constraint.MemberOf { target = "ok_rel"; binding = b }; + ] + in + let tuple : Tuple.materialized = + { relation = "test"; attributes = Tuple.AttributeMap.empty } + in + (match Constraint.evaluate ctx tuple c with + | Error _ -> () + | _ -> assert false); + (* Second branch should not have been called *) + assert (!call_count = 1) + +let%test_unit "constraint: evaluate Or succeeds on first match" = + let ctx = + make_eval_ctx + ~relations: + [ + ("a", fun _ -> false); + ("b", fun _ -> true); + ] + () + in + let b = Constraint.BindingMap.empty in + let c = + Constraint.Or + [ + Constraint.MemberOf { target = "a"; binding = b }; + Constraint.MemberOf { target = "b"; binding = b }; + ] + in + let tuple : Tuple.materialized = + { relation = "test"; attributes = Tuple.AttributeMap.empty } + in + match Constraint.evaluate ctx tuple c with + | Ok true -> () + | _ -> assert false + +let%test_unit "constraint: evaluate Not negates" = + let ctx : Constraint.eval_context = + { + check_membership = + (fun rel_name _pairs -> + match rel_name with + | "universe" -> true + | "body_rel" -> false + | _ -> false); + iterate_finite = (fun _ -> None); + } + in + let b = Constraint.BindingMap.empty in + let c = + Constraint.Not + { + body = Constraint.MemberOf { target = "body_rel"; binding = b }; + universe = "universe"; + } + in + let tuple : Tuple.materialized = + { relation = "test"; attributes = Tuple.AttributeMap.empty } + in + match Constraint.evaluate ctx tuple c with + | Ok true -> () + | _ -> assert false + +let%test_unit "constraint: evaluate Exists over finite relation" = + let ctx : Constraint.eval_context = + { + check_membership = + (fun _rel_name pairs -> + match List.assoc_opt "left" pairs, List.assoc_opt "right" pairs with + | Some l, Some r -> (Obj.obj l : int) < (Obj.obj r : int) + | _ -> false); + iterate_finite = + (fun rel_name -> + if rel_name = "small_set" then + Some + [ + [ ("value", Obj.repr 1) ]; + [ ("value", Obj.repr 5) ]; + [ ("value", Obj.repr 10) ]; + ] + else None); + } + in + let b = + Constraint.BindingMap.empty + |> Constraint.BindingMap.add "left" (Constraint.Var "x") + |> Constraint.BindingMap.add "right" (Constraint.Var "value") + in + let c = + Constraint.Exists + { + variable = "value"; + quantifier = "small_set"; + body = Constraint.MemberOf { target = "less_than"; binding = b }; + } + in + (* x=3, exists value in {1,5,10} where 3 < value => true (5 or 10 work) *) + let tuple : Tuple.materialized = + { + relation = "test"; + attributes = + Tuple.AttributeMap.singleton "x" { Attribute.value = Obj.repr 3 }; + } + in + match Constraint.evaluate ctx tuple c with + | Ok true -> () + | _ -> assert false + +let%test_unit "constraint: evaluate Forall fails when not all match" = + let ctx : Constraint.eval_context = + { + check_membership = + (fun _rel_name pairs -> + match List.assoc_opt "left" pairs, List.assoc_opt "right" pairs with + | Some l, Some r -> (Obj.obj l : int) < (Obj.obj r : int) + | _ -> false); + iterate_finite = + (fun rel_name -> + if rel_name = "small_set" then + Some + [ + [ ("value", Obj.repr 1) ]; + [ ("value", Obj.repr 5) ]; + ] + else None); + } + in + let b = + Constraint.BindingMap.empty + |> Constraint.BindingMap.add "left" (Constraint.Var "x") + |> Constraint.BindingMap.add "right" (Constraint.Var "value") + in + let c = + Constraint.Forall + { + variable = "value"; + quantifier = "small_set"; + body = Constraint.MemberOf { target = "less_than"; binding = b }; + } + in + (* x=3, forall value in {1,5} where 3 < value => false (3 is not < 1) *) + let tuple : Tuple.materialized = + { + relation = "test"; + attributes = + Tuple.AttributeMap.singleton "x" { Attribute.value = Obj.repr 3 }; + } + in + match Constraint.evaluate ctx tuple c with + | Ok false -> () + | _ -> assert false + +let%test_unit "constraint: Forall unbounded quantifier errors" = + let ctx : Constraint.eval_context = + { + check_membership = (fun _ _ -> true); + iterate_finite = (fun _ -> None); + } + in + let b = Constraint.BindingMap.empty in + let c = + Constraint.Forall + { + variable = "v"; + quantifier = "infinite_rel"; + body = Constraint.MemberOf { target = "t"; binding = b }; + } + in + let tuple : Tuple.materialized = + { relation = "test"; attributes = Tuple.AttributeMap.empty } + in + match Constraint.evaluate ctx tuple c with + | Error (Constraint.UnboundedQuantifier _) -> () + | _ -> assert false + +(* ---------- Integrated constraint enforcement in manipulation ---------- *) + +let%test_unit "constraint: create_tuple with passing constraint" = + with_storage (fun storage -> + let db = + match Manipulation.Memory.create_database storage ~name:"test" with + | Error _ -> assert false + | Ok db -> db + in + let schema = Schema.empty |> Schema.add "value" "natural" in + let db, _rel = + match + Manipulation.Memory.create_relation storage db ~name:"positives" + ~schema + with + | Error _ -> assert false + | Ok x -> x + in + (* Register a constraint: value must be member of natural (always true for naturals) *) + let db = + match + Manipulation.Memory.register_constraint storage db + ~constraint_name:"is_natural" ~relation_name:"positives" + ~body:(Constraint.And []) + with + | Error _ -> assert false + | Ok db -> db + in + let rel = + match Manipulation.Memory.get_relation db ~name:"positives" with + | None -> assert false + | Some r -> r + in + let tuple : Tuple.materialized = + { + relation = "positives"; + attributes = + Tuple.AttributeMap.singleton "value" + { Attribute.value = Obj.repr 5 }; + } + in + match Manipulation.Memory.create_tuple storage db rel tuple with + | Ok _ -> () + | Error _ -> assert false) + +let%test_unit "constraint: create_tuple with failing constraint" = + with_storage (fun storage -> + let db = + match Manipulation.Memory.create_database storage ~name:"test" with + | Error _ -> assert false + | Ok db -> db + in + let schema = Schema.empty |> Schema.add "value" "natural" in + let db, _rel = + match + Manipulation.Memory.create_relation storage db ~name:"checked" + ~schema + with + | Error _ -> assert false + | Ok x -> x + in + (* Register a constraint that always fails: MemberOf a nonexistent relation *) + let db = + match + Manipulation.Memory.register_constraint storage db + ~constraint_name:"impossible" ~relation_name:"checked" + ~body: + (Constraint.MemberOf + { + target = "nonexistent_relation"; + binding = + Constraint.BindingMap.singleton "x" (Constraint.Var "value"); + }) + with + | Error _ -> assert false + | Ok db -> db + in + let rel = + match Manipulation.Memory.get_relation db ~name:"checked" with + | None -> assert false + | Some r -> r + in + let tuple : Tuple.materialized = + { + relation = "checked"; + attributes = + Tuple.AttributeMap.singleton "value" + { Attribute.value = Obj.repr 5 }; + } + in + match Manipulation.Memory.create_tuple storage db rel tuple with + | Error (Manipulation.ConstraintViolation _) -> () + | _ -> assert false) + +(* ---------- Scenario tests ported from Erlang ---------- *) + +(* Scenario 1: Mutual exclusion between subtypes *) +let%test_unit "constraint scenario: mutual exclusion subtypes" = + with_storage (fun storage -> + let db = + match Manipulation.Memory.create_database storage ~name:"test" with + | Error _ -> assert false + | Ok db -> db + in + let schema = Schema.empty |> Schema.add "id" "natural" in + let db, _employee = + match + Manipulation.Memory.create_relation storage db ~name:"employee" + ~schema + with + | Error _ -> assert false + | Ok x -> x + in + let db, _manager = + match + Manipulation.Memory.create_relation storage db ~name:"manager" + ~schema + with + | Error _ -> assert false + | Ok x -> x + in + (* manager must NOT be in employee (mutual exclusion) *) + let body = + Constraint.Not + { + body = + Constraint.MemberOf + { + target = "employee"; + binding = + Constraint.BindingMap.singleton "id" (Constraint.Var "id"); + }; + universe = "manager"; + } + in + let db = + match + Manipulation.Memory.register_constraint storage db + ~constraint_name:"not_employee" ~relation_name:"manager" ~body + with + | Error _ -> assert false + | Ok db -> db + in + (* Insert into employee first *) + let employee = + match Manipulation.Memory.get_relation db ~name:"employee" with + | None -> assert false + | Some r -> r + in + let emp_tuple : Tuple.materialized = + { + relation = "employee"; + attributes = + Tuple.AttributeMap.singleton "id" + { Attribute.value = Obj.repr 1 }; + } + in + let db, _employee, _ = + match + Manipulation.Memory.create_tuple storage db employee emp_tuple + with + | Error _ -> assert false + | Ok x -> x + in + (* Now try to insert same id into manager — should fail *) + let manager = + match Manipulation.Memory.get_relation db ~name:"manager" with + | None -> assert false + | Some r -> r + in + let mgr_tuple : Tuple.materialized = + { + relation = "manager"; + attributes = + Tuple.AttributeMap.singleton "id" + { Attribute.value = Obj.repr 1 }; + } + in + match Manipulation.Memory.create_tuple storage db manager mgr_tuple with + | Error (Manipulation.ConstraintViolation _) -> () + | _ -> assert false) + +(* Scenario 2: Foreign key constraint *) +let%test_unit "constraint scenario: foreign key" = + with_storage (fun storage -> + let db = + match Manipulation.Memory.create_database storage ~name:"test" with + | Error _ -> assert false + | Ok db -> db + in + let order_schema = Schema.empty |> Schema.add "order_id" "natural" in + let db, _orders = + match + Manipulation.Memory.create_relation storage db ~name:"orders" + ~schema:order_schema + with + | Error _ -> assert false + | Ok x -> x + in + let item_schema = + Schema.empty |> Schema.add "item_id" "natural" + |> Schema.add "order_id" "natural" + in + let db, _items = + match + Manipulation.Memory.create_relation storage db ~name:"order_items" + ~schema:item_schema + with + | Error _ -> assert false + | Ok x -> x + in + (* FK: order_items.order_id must exist in orders *) + let fk_body = + Constraint.MemberOf + { + target = "orders"; + binding = + Constraint.BindingMap.singleton "order_id" + (Constraint.Var "order_id"); + } + in + let db = + match + Manipulation.Memory.register_constraint storage db + ~constraint_name:"fk_order" ~relation_name:"order_items" + ~body:fk_body + with + | Error _ -> assert false + | Ok db -> db + in + (* Insert an order *) + let orders = + match Manipulation.Memory.get_relation db ~name:"orders" with + | None -> assert false + | Some r -> r + in + let order_tuple : Tuple.materialized = + { + relation = "orders"; + attributes = + Tuple.AttributeMap.singleton "order_id" + { Attribute.value = Obj.repr 100 }; + } + in + let db, _orders, _ = + match + Manipulation.Memory.create_tuple storage db orders order_tuple + with + | Error _ -> assert false + | Ok x -> x + in + (* Insert item referencing valid order — should succeed *) + let items = + match Manipulation.Memory.get_relation db ~name:"order_items" with + | None -> assert false + | Some r -> r + in + let valid_item : Tuple.materialized = + { + relation = "order_items"; + attributes = + Tuple.AttributeMap.of_list + [ + ("item_id", { Attribute.value = Obj.repr 1 }); + ("order_id", { Attribute.value = Obj.repr 100 }); + ]; + } + in + let db, items, _ = + match + Manipulation.Memory.create_tuple storage db items valid_item + with + | Error _ -> assert false + | Ok x -> x + in + (* Insert item referencing nonexistent order — should fail *) + let invalid_item : Tuple.materialized = + { + relation = "order_items"; + attributes = + Tuple.AttributeMap.of_list + [ + ("item_id", { Attribute.value = Obj.repr 2 }); + ("order_id", { Attribute.value = Obj.repr 999 }); + ]; + } + in + match Manipulation.Memory.create_tuple storage db items invalid_item with + | Error (Manipulation.ConstraintViolation _) -> () + | _ -> assert false) + +(* Scenario 3: Self-reference (emp_id != mgr_id via not_equal comparison) *) +let%test_unit "constraint scenario: self-reference neq" = + with_storage (fun storage -> + let db = + match Manipulation.Memory.create_database storage ~name:"test" with + | Error _ -> assert false + | Ok db -> db + in + let schema = + Schema.empty |> Schema.add "emp_id" "natural" + |> Schema.add "mgr_id" "natural" + in + let db, _rel = + match + Manipulation.Memory.create_relation storage db ~name:"reports_to" + ~schema + with + | Error _ -> assert false + | Ok x -> x + in + (* Register the not_equal comparison relation *) + let db, _ = + match + Manipulation.Memory.create_immutable_relation storage db + ~name:"not_equal" + ~schema: + (Schema.empty |> Schema.add "left" "natural" + |> Schema.add "right" "natural") + ~generator:(fun _ -> Generator.Error "not enumerable") + ~membership_criteria:(fun t -> + match t with + | Tuple.Materialized m -> ( + match + ( Tuple.AttributeMap.find_opt "left" m.attributes, + Tuple.AttributeMap.find_opt "right" m.attributes ) + with + | Some l, Some r -> + (Obj.obj l.Attribute.value : int) + <> (Obj.obj r.Attribute.value : int) + | _ -> false) + | _ -> false) + ~cardinality:Conventions.Cardinality.AlephZero + with + | Error _ -> assert false + | Ok x -> x + in + (* Constraint: emp_id != mgr_id via not_equal relation *) + let neq_body = + Constraint.neq ~left:(Var "emp_id") ~right:(Var "mgr_id") + in + let db = + match + Manipulation.Memory.register_constraint storage db + ~constraint_name:"no_self_manage" ~relation_name:"reports_to" + ~body:neq_body + with + | Error _ -> assert false + | Ok db -> db + in + let rel = + match Manipulation.Memory.get_relation db ~name:"reports_to" with + | None -> assert false + | Some r -> r + in + (* Insert (emp_id=1, mgr_id=2) — should succeed *) + let valid : Tuple.materialized = + { + relation = "reports_to"; + attributes = + Tuple.AttributeMap.of_list + [ + ("emp_id", { Attribute.value = Obj.repr 1 }); + ("mgr_id", { Attribute.value = Obj.repr 2 }); + ]; + } + in + let db, rel, _ = + match Manipulation.Memory.create_tuple storage db rel valid with + | Error _ -> assert false + | Ok x -> x + in + (* Insert (emp_id=3, mgr_id=3) — same person, should fail *) + let invalid : Tuple.materialized = + { + relation = "reports_to"; + attributes = + Tuple.AttributeMap.of_list + [ + ("emp_id", { Attribute.value = Obj.repr 3 }); + ("mgr_id", { Attribute.value = Obj.repr 3 }); + ]; + } + in + match Manipulation.Memory.create_tuple storage db rel invalid with + | Error (Manipulation.ConstraintViolation _) -> () + | _ -> assert false) + +(* Scenario 4: Mutual exclusion between open_ticket and closed_ticket *) +let%test_unit "constraint scenario: open vs closed ticket" = + with_storage (fun storage -> + let db = + match Manipulation.Memory.create_database storage ~name:"test" with + | Error _ -> assert false + | Ok db -> db + in + let schema = Schema.empty |> Schema.add "ticket_id" "natural" in + let db, _ = + match + Manipulation.Memory.create_relation storage db ~name:"open_ticket" + ~schema + with + | Error _ -> assert false + | Ok x -> x + in + let db, _ = + match + Manipulation.Memory.create_relation storage db ~name:"closed_ticket" + ~schema + with + | Error _ -> assert false + | Ok x -> x + in + (* open_ticket must not be in closed_ticket *) + let db = + match + Manipulation.Memory.register_constraint storage db + ~constraint_name:"not_closed" ~relation_name:"open_ticket" + ~body: + (Constraint.Not + { + body = + Constraint.MemberOf + { + target = "closed_ticket"; + binding = + Constraint.BindingMap.singleton "ticket_id" + (Constraint.Var "ticket_id"); + }; + universe = "open_ticket"; + }) + with + | Error _ -> assert false + | Ok db -> db + in + (* Insert ticket 1 as closed *) + let closed = + match Manipulation.Memory.get_relation db ~name:"closed_ticket" with + | None -> assert false + | Some r -> r + in + let t1 : Tuple.materialized = + { + relation = "closed_ticket"; + attributes = + Tuple.AttributeMap.singleton "ticket_id" + { Attribute.value = Obj.repr 1 }; + } + in + let db, _, _ = + match Manipulation.Memory.create_tuple storage db closed t1 with + | Error _ -> assert false + | Ok x -> x + in + (* Try to open same ticket — should fail *) + let open_ = + match Manipulation.Memory.get_relation db ~name:"open_ticket" with + | None -> assert false + | Some r -> r + in + let t1_open : Tuple.materialized = + { + relation = "open_ticket"; + attributes = + Tuple.AttributeMap.singleton "ticket_id" + { Attribute.value = Obj.repr 1 }; + } + in + match Manipulation.Memory.create_tuple storage db open_ t1_open with + | Error (Manipulation.ConstraintViolation _) -> () + | _ -> assert false) + +(* Scenario 5: Weak entity dependency *) +let%test_unit "constraint scenario: weak entity dependency" = + with_storage (fun storage -> + let db = + match Manipulation.Memory.create_database storage ~name:"test" with + | Error _ -> assert false + | Ok db -> db + in + let parent_schema = Schema.empty |> Schema.add "parent_id" "natural" in + let db, _ = + match + Manipulation.Memory.create_relation storage db ~name:"parent" + ~schema:parent_schema + with + | Error _ -> assert false + | Ok x -> x + in + let dep_schema = + Schema.empty |> Schema.add "dep_id" "natural" + |> Schema.add "parent_id" "natural" + in + let db, _ = + match + Manipulation.Memory.create_relation storage db ~name:"dependent" + ~schema:dep_schema + with + | Error _ -> assert false + | Ok x -> x + in + (* dependent.parent_id must exist in parent *) + let db = + match + Manipulation.Memory.register_constraint storage db + ~constraint_name:"parent_exists" ~relation_name:"dependent" + ~body: + (Constraint.MemberOf + { + target = "parent"; + binding = + Constraint.BindingMap.singleton "parent_id" + (Constraint.Var "parent_id"); + }) + with + | Error _ -> assert false + | Ok db -> db + in + (* Insert parent *) + let parent = + match Manipulation.Memory.get_relation db ~name:"parent" with + | None -> assert false + | Some r -> r + in + let pt : Tuple.materialized = + { + relation = "parent"; + attributes = + Tuple.AttributeMap.singleton "parent_id" + { Attribute.value = Obj.repr 10 }; + } + in + let db, _, _ = + match Manipulation.Memory.create_tuple storage db parent pt with + | Error _ -> assert false + | Ok x -> x + in + (* Insert dependent with valid parent — succeeds *) + let dep = + match Manipulation.Memory.get_relation db ~name:"dependent" with + | None -> assert false + | Some r -> r + in + let valid_dep : Tuple.materialized = + { + relation = "dependent"; + attributes = + Tuple.AttributeMap.of_list + [ + ("dep_id", { Attribute.value = Obj.repr 1 }); + ("parent_id", { Attribute.value = Obj.repr 10 }); + ]; + } + in + let db, dep, _ = + match + Manipulation.Memory.create_tuple storage db dep valid_dep + with + | Error _ -> assert false + | Ok x -> x + in + (* Insert dependent with nonexistent parent — fails *) + let invalid_dep : Tuple.materialized = + { + relation = "dependent"; + attributes = + Tuple.AttributeMap.of_list + [ + ("dep_id", { Attribute.value = Obj.repr 2 }); + ("parent_id", { Attribute.value = Obj.repr 999 }); + ]; + } + in + match + Manipulation.Memory.create_tuple storage db dep invalid_dep + with + | Error (Manipulation.ConstraintViolation _) -> () + | _ -> assert false) + +(* Scenario 6: Algebra propagation — select preserves constraints *) +let%test_unit "constraint propagation: select preserves constraints" = + with_storage (fun storage -> + let db = + match Manipulation.Memory.create_database storage ~name:"test" with + | Error _ -> assert false + | Ok db -> db + in + let schema = Schema.empty |> Schema.add "x" "natural" in + let db, _rel = + match + Manipulation.Memory.create_relation storage db ~name:"constrained" + ~schema + with + | Error _ -> assert false + | Ok x -> x + in + let db = + match + Manipulation.Memory.register_constraint storage db + ~constraint_name:"c1" ~relation_name:"constrained" + ~body:(Constraint.And []) + with + | Error _ -> assert false + | Ok db -> db + in + let rel = + match Manipulation.Memory.get_relation db ~name:"constrained" with + | None -> assert false + | Some r -> r + in + match + Algebra.Memory.select_fn storage (fun _ -> true) rel + with + | Error _ -> assert false + | Ok result -> + assert (result.Relation.constraints <> None)) + +(* Scenario 7: Algebra propagation — project filters constraints *) +let%test_unit "constraint propagation: project filters constraints" = + with_storage (fun storage -> + let db = + match Manipulation.Memory.create_database storage ~name:"test" with + | Error _ -> assert false + | Ok db -> db + in + let schema = + Schema.empty |> Schema.add "x" "natural" |> Schema.add "y" "natural" + in + let db, _rel = + match + Manipulation.Memory.create_relation storage db ~name:"xy" ~schema + with + | Error _ -> assert false + | Ok x -> x + in + (* Constraint on x only *) + let c_on_x = + Constraint.MemberOf + { + target = "some_rel"; + binding = + Constraint.BindingMap.singleton "left" (Constraint.Var "x"); + } + in + let db = + match + Manipulation.Memory.register_constraint storage db + ~constraint_name:"x_only" ~relation_name:"xy" ~body:c_on_x + with + | Error _ -> assert false + | Ok db -> db + in + let rel = + match Manipulation.Memory.get_relation db ~name:"xy" with + | None -> assert false + | Some r -> r + in + (* Project to only "x" — constraint should survive *) + (match Algebra.Memory.project storage [ "x" ] rel with + | Error _ -> assert false + | Ok result -> assert (result.Relation.constraints <> None)); + (* Project to only "y" — constraint referencing "x" should be dropped *) + match Algebra.Memory.project storage [ "y" ] rel with + | Error _ -> assert false + | Ok result -> assert (result.Relation.constraints = None)) |