From 99ac1e7d9b77d69f2a85a108468d4433953d8269 Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Sun, 8 Mar 2026 01:12:02 -0300 Subject: constraints --- lib/algebra.ml | 60 ++++++-- lib/constraint.ml | 378 ++++++++++++++++++++++++++++++++++++++++++++- lib/conventions.ml | 2 +- lib/domain.ml | 5 +- lib/manipulation.ml | 192 +++++++++++++++++++++-- lib/prelude/domains.ml | 6 + lib/prelude/standard.ml | 396 +++++++++++++++++++++++++++++++++++++++++++----- 7 files changed, 979 insertions(+), 60 deletions(-) (limited to 'lib') 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") -- cgit v1.2.3