constraints

2 files changed, 368 insertions, 34 deletions

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")