format

1 files changed, 154 insertions, 178 deletions

diff --git a/lib/prelude/standard.ml b/lib/prelude/standard.ml
index 68012fc..6bdab0c 100644
--- a/lib/prelude/standard.ml
+++ b/lib/prelude/standard.ml
@@ -7,22 +7,23 @@
 
 let mk v = { Attribute.value = Obj.repr v }
 
-(** Build a comparison relation over a single domain.
-    [pred] receives the result of [Stdlib.compare left right]. *)
+(** Build a comparison relation over a single domain. [pred] receives the result
+    of [Stdlib.compare left right]. *)
 let make_comparison ~name ~domain_name ~pred ~cardinality ~generator =
   let schema =
-    Schema.empty |> Schema.add "left" domain_name
+    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)
+        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
@@ -33,38 +34,35 @@ let make_comparison ~name ~domain_name ~pred ~cardinality ~generator =
 (** Enumerate pairs (a, b) where a < b using triangular indexing. *)
 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 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) via Cantor pairing. *)
 let cantor_pair_of_nat n =
   let w =
-    int_of_float (floor ((sqrt (float_of_int (8 * n + 1)) -. 1.) /. 2.))
+    int_of_float (floor ((sqrt (float_of_int ((8 * n) + 1)) -. 1.) /. 2.))
   in
-  let t = (w * (w + 1)) / 2 in
+  let t = w * (w + 1) / 2 in
   let b = n - t in
   let a = w - b in
   (a, b)
 
-
 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", mk left); ("right", mk right) ]
-      in
-      Generator.Value
-        ( Tuple.make_materialized ~relation:"less_than" ~attributes,
-          generator )
+        let left, right = pair_of_nat_lt position in
+        let attributes : Attribute.materialized Tuple.AttributeMap.t =
+          Tuple.AttributeMap.of_list [ ("left", mk left); ("right", mk 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."
+        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)
@@ -74,17 +72,16 @@ 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", mk left); ("right", mk right) ]
-      in
-      Generator.Value
-        ( Tuple.make_materialized ~relation:"less_than_or_equal" ~attributes,
-          generator )
+        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", mk left); ("right", mk 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"
@@ -96,15 +93,14 @@ 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", mk right); ("right", mk left) ]
-      in
-      Generator.Value
-        ( Tuple.make_materialized ~relation:"greater_than" ~attributes,
-          generator )
+        let left, right = pair_of_nat_lt n in
+        (* Swap: right > left *)
+        let attributes =
+          Tuple.AttributeMap.of_list [ ("left", mk right); ("right", mk 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"
@@ -115,16 +111,15 @@ 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", mk left); ("right", mk right) ]
-      in
-      Generator.Value
-        ( Tuple.make_materialized ~relation:"greater_than_or_equal" ~attributes,
-          generator )
+        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", mk left); ("right", mk 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"
@@ -136,12 +131,11 @@ 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", mk n); ("right", mk n) ]
-      in
-      Generator.Value
-        ( Tuple.make_materialized ~relation:"equal" ~attributes, generator )
+        let attributes =
+          Tuple.AttributeMap.of_list [ ("left", mk n); ("right", mk 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"
@@ -152,21 +146,19 @@ 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", mk left); ("right", mk right) ]
-      in
-      Generator.Value
-        ( Tuple.make_materialized ~relation:"not_equal" ~attributes, generator )
+        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", mk left); ("right", mk 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
 
-
 let plus_natural : Relation.t =
   let schema =
     Schema.empty |> Schema.add "a" "natural" |> Schema.add "b" "natural"
@@ -175,175 +167,159 @@ let plus_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 s = a + b in
-      let attributes =
-        Tuple.AttributeMap.of_list
-          [ ("a", mk a); ("b", mk b); ("sum", mk s) ]
-      in
-      Generator.Value
-        ( Tuple.make_materialized ~relation:"plus" ~attributes, generator )
+        let a, b = cantor_pair_of_nat n in
+        let s = a + b in
+        let attributes =
+          Tuple.AttributeMap.of_list [ ("a", mk a); ("b", mk b); ("sum", mk 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)
+        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
+    ~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.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", mk a); ("b", mk b); ("product", mk p);
-          ]
-      in
-      Generator.Value
-        ( Tuple.make_materialized ~relation:"times" ~attributes, generator )
+        let a, b = cantor_pair_of_nat n in
+        let p = a * b in
+        let attributes =
+          Tuple.AttributeMap.of_list
+            [ ("a", mk a); ("b", mk b); ("product", mk 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)
+        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
+    ~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.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", mk a);
-            ("b", mk b);
-            ("difference", mk diff);
-          ]
-      in
-      Generator.Value
-        ( Tuple.make_materialized ~relation:"minus" ~attributes, generator )
+        (* 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", mk a); ("b", mk b); ("difference", mk 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)
+        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
+    ~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.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", mk a);
-            ("b", mk b);
-            ("quotient", mk q);
-            ("remainder", mk r);
-          ]
-      in
-      Generator.Value
-        ( Tuple.make_materialized ~relation:"divide" ~attributes, generator )
+        (* 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", mk a); ("b", mk b); ("quotient", mk q); ("remainder", mk 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)
+        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
+    ~constraints:None ~cardinality:Conventions.Cardinality.AlephZero
     ~generator:(Some generator) ~membership_criteria
     ~provenance:(Relation.Provenance.Base "divide")
     ~lineage:(Relation.Lineage.Base "divide")