Format

3 files changed, 209 insertions, 382 deletions

diff --git a/lib/prelude/catalog.ml b/lib/prelude/catalog.ml
index 01721b2..26fe30c 100644
--- a/lib/prelude/catalog.ml
+++ b/lib/prelude/catalog.ml
@@ -7,7 +7,7 @@
    written to by any executor. They appear to be stubs for trigger/timing
    metadata that was never implemented. *)
 
-(** Dedicated multigroup hosting the system catalog.  The catalog's relation
+(** Dedicated multigroup hosting the system catalog. The catalog's relation
     names keep the [public:] prefix — that prefix is part of the relation name
     inside this mg, not a separate namespace. *)
 let prelude_mg = "sakura"
@@ -28,8 +28,7 @@ let loaded_library_rel_name = catalog_prefix ^ "loaded_library"
 
 (** Relations present in every multigroup's catalog. *)
 let catalog_relation_names =
-  [
-    relation_rel_name;
+  [ relation_rel_name;
     domain_rel_name;
     attribute_rel_name;
     constraint_rel_name;
@@ -37,15 +36,12 @@ let catalog_relation_names =
     timing_rel_name;
     schema_rel_name;
     function_predicate_rel_name;
-    loaded_library_rel_name;
-  ]
+    loaded_library_rel_name ]
 
 (** Relations exclusive to the sakura meta-multigroup. *)
-let sakura_only_relation_names = [ multigroup_rel_name ]
-
-let all_catalog_relation_names =
-  catalog_relation_names @ sakura_only_relation_names
+let sakura_only_relation_names = [multigroup_rel_name]
 
+let all_catalog_relation_names = catalog_relation_names @ sakura_only_relation_names
 let is_catalog_relation name = List.mem name all_catalog_relation_names
 let relation_schema : Schema.t = Schema.empty |> Schema.add "name" "string"
 let domain_schema : Schema.t = Schema.empty |> Schema.add "name" "string"
@@ -57,8 +53,7 @@ let attribute_schema : Schema.t =
   |> Schema.add "domain_name" "string"
 
 let constraint_schema : Schema.t =
-  Schema.empty |> Schema.add "name" "string"
-  |> Schema.add "relation_name" "string"
+  Schema.empty |> Schema.add "name" "string" |> Schema.add "relation_name" "string"
 
 let on_schema : Schema.t = Schema.empty |> Schema.add "event" "string"
 let timing_schema : Schema.t = Schema.empty |> Schema.add "timing" "string"
@@ -66,108 +61,74 @@ let multigroup_schema : Schema.t = Schema.empty |> Schema.add "name" "string"
 let schema_schema : Schema.t = Schema.empty |> Schema.add "name" "string"
 
 let function_predicate_schema : Schema.t =
-  Schema.empty |> Schema.add "name" "string"
+  Schema.empty
+  |> Schema.add "name" "string"
   |> Schema.add "symbol" "string"
   |> Schema.add "cardinality" "string"
   |> Schema.add "purity" "string"
 
-let loaded_library_schema : Schema.t =
-  Schema.empty |> Schema.add "path" "string"
+let loaded_library_schema : Schema.t = Schema.empty |> Schema.add "path" "string"
 
 (** Definitions seeded into every multigroup. *)
 let catalog_definitions =
-  [
-    (relation_rel_name, relation_schema);
-    (domain_rel_name, domain_schema);
-    (attribute_rel_name, attribute_schema);
-    (constraint_rel_name, constraint_schema);
-    (on_rel_name, on_schema);
-    (timing_rel_name, timing_schema);
-    (schema_rel_name, schema_schema);
-    (function_predicate_rel_name, function_predicate_schema);
-    (loaded_library_rel_name, loaded_library_schema);
-  ]
+  [ relation_rel_name, relation_schema;
+    domain_rel_name, domain_schema;
+    attribute_rel_name, attribute_schema;
+    constraint_rel_name, constraint_schema;
+    on_rel_name, on_schema;
+    timing_rel_name, timing_schema;
+    schema_rel_name, schema_schema;
+    function_predicate_rel_name, function_predicate_schema;
+    loaded_library_rel_name, loaded_library_schema ]
 
 (** Extra definitions seeded only into the sakura meta-multigroup. *)
-let sakura_only_definitions = [ (multigroup_rel_name, multigroup_schema) ]
+let sakura_only_definitions = [multigroup_rel_name, multigroup_schema]
 
 (* TODO: all tuple builders use Obj.magic to coerce string values into
    Attribute.value (Obj.t). This is the same UB pattern fixed in standard.ml;
    should use Obj.repr instead. *)
 
 let build_relation_tuple rel_name : Tuple.materialized =
-  {
-    Tuple.relation = relation_rel_name;
-    attributes =
-      Tuple.AttributeMap.singleton "name"
-        { Attribute.value = Obj.magic rel_name };
-  }
+  { Tuple.relation= relation_rel_name;
+    attributes= Tuple.AttributeMap.singleton "name" {Attribute.value= Obj.magic rel_name} }
 
 let build_domain_tuple dom_name : Tuple.materialized =
-  {
-    Tuple.relation = domain_rel_name;
-    attributes =
-      Tuple.AttributeMap.singleton "name"
-        { Attribute.value = Obj.magic dom_name };
-  }
-
-let build_attribute_tuples ~relation_name (schema : Schema.t) :
-    Tuple.materialized list =
+  { Tuple.relation= domain_rel_name;
+    attributes= Tuple.AttributeMap.singleton "name" {Attribute.value= Obj.magic dom_name} }
+
+let build_attribute_tuples ~relation_name (schema : Schema.t) : Tuple.materialized list =
   List.map
     (fun (attr_n, dom_n) ->
-      {
-        Tuple.relation = attribute_rel_name;
-        attributes =
+      { Tuple.relation= attribute_rel_name;
+        attributes=
           Tuple.AttributeMap.of_list
-            [
-              ("relation_name", { Attribute.value = Obj.magic relation_name });
-              ("attr_name", { Attribute.value = Obj.magic attr_n });
-              ("domain_name", { Attribute.value = Obj.magic dom_n });
-            ];
-      })
+            [ "relation_name", {Attribute.value= Obj.magic relation_name};
+              "attr_name", {Attribute.value= Obj.magic attr_n};
+              "domain_name", {Attribute.value= Obj.magic dom_n} ] } )
     schema
 
 let build_constraint_tuple cname rel_name : Tuple.materialized =
-  {
-    Tuple.relation = constraint_rel_name;
-    attributes =
+  { Tuple.relation= constraint_rel_name;
+    attributes=
       Tuple.AttributeMap.of_list
-        [
-          ("name", { Attribute.value = Obj.magic cname });
-          ("relation_name", { Attribute.value = Obj.magic rel_name });
-        ];
-  }
+        [ "name", {Attribute.value= Obj.magic cname};
+          "relation_name", {Attribute.value= Obj.magic rel_name} ] }
 
 let build_on_tuple event : Tuple.materialized =
-  {
-    Tuple.relation = on_rel_name;
-    attributes =
-      Tuple.AttributeMap.singleton "event" { Attribute.value = Obj.magic event };
-  }
+  { Tuple.relation= on_rel_name;
+    attributes= Tuple.AttributeMap.singleton "event" {Attribute.value= Obj.magic event} }
 
 let build_timing_tuple timing : Tuple.materialized =
-  {
-    Tuple.relation = timing_rel_name;
-    attributes =
-      Tuple.AttributeMap.singleton "timing"
-        { Attribute.value = Obj.magic timing };
-  }
+  { Tuple.relation= timing_rel_name;
+    attributes= Tuple.AttributeMap.singleton "timing" {Attribute.value= Obj.magic timing} }
 
 let build_multigroup_tuple mg_name : Tuple.materialized =
-  {
-    Tuple.relation = multigroup_rel_name;
-    attributes =
-      Tuple.AttributeMap.singleton "name"
-        { Attribute.value = Obj.magic mg_name };
-  }
+  { Tuple.relation= multigroup_rel_name;
+    attributes= Tuple.AttributeMap.singleton "name" {Attribute.value= Obj.magic mg_name} }
 
 let build_schema_tuple schema_name : Tuple.materialized =
-  {
-    Tuple.relation = schema_rel_name;
-    attributes =
-      Tuple.AttributeMap.singleton "name"
-        { Attribute.value = Obj.magic schema_name };
-  }
+  { Tuple.relation= schema_rel_name;
+    attributes= Tuple.AttributeMap.singleton "name" {Attribute.value= Obj.magic schema_name} }
 
 let purity_to_string p = Sexplib.Sexp.to_string (Conventions.Purity.sexp_of_t p)
 
@@ -176,33 +137,22 @@ let purity_of_string s =
   | p -> Some p
   | exception _ -> None
 
-let cardinality_to_string c =
-  Sexplib.Sexp.to_string (Conventions.Cardinality.sexp_of_t c)
+let cardinality_to_string c = Sexplib.Sexp.to_string (Conventions.Cardinality.sexp_of_t c)
 
 let cardinality_of_string s =
   match Conventions.Cardinality.t_of_sexp (Sexplib.Sexp.of_string s) with
   | c -> Some c
   | exception _ -> None
 
-let build_function_predicate_tuple ~name ~symbol ~cardinality ~purity :
-    Tuple.materialized =
-  {
-    Tuple.relation = function_predicate_rel_name;
-    attributes =
+let build_function_predicate_tuple ~name ~symbol ~cardinality ~purity : Tuple.materialized =
+  { Tuple.relation= function_predicate_rel_name;
+    attributes=
       Tuple.AttributeMap.of_list
-        [
-          ("name", { Attribute.value = Obj.magic name });
-          ("symbol", { Attribute.value = Obj.magic symbol });
-          ( "cardinality",
-            { Attribute.value = Obj.magic (cardinality_to_string cardinality) }
-          );
-          ("purity", { Attribute.value = Obj.magic (purity_to_string purity) });
-        ];
-  }
+        [ "name", {Attribute.value= Obj.magic name};
+          "symbol", {Attribute.value= Obj.magic symbol};
+          "cardinality", {Attribute.value= Obj.magic (cardinality_to_string cardinality)};
+          "purity", {Attribute.value= Obj.magic (purity_to_string purity)} ] }
 
 let build_loaded_library_tuple path : Tuple.materialized =
-  {
-    Tuple.relation = loaded_library_rel_name;
-    attributes =
-      Tuple.AttributeMap.singleton "path" { Attribute.value = Obj.magic path };
-  }
+  { Tuple.relation= loaded_library_rel_name;
+    attributes= Tuple.AttributeMap.singleton "path" {Attribute.value= Obj.magic path} }
diff --git a/lib/prelude/domains.ml b/lib/prelude/domains.ml
index 9dc9c86..264bf03 100644
--- a/lib/prelude/domains.ml
+++ b/lib/prelude/domains.ml
@@ -1,22 +1,20 @@
-(** Predefined fundamental domains. Each domain carries a generator
-    (for enumeration) and membership criteria (for validation). Values
-    are stored as {!Conventions.AbstractValue.t} via [Obj.magic],
-    following the same convention as {!Standard}. *)
+(** Predefined fundamental domains. Each domain carries a generator (for
+    enumeration) and membership criteria (for validation). Values are stored as
+    {!Conventions.AbstractValue.t} via [Obj.magic], following the same
+    convention as {!Standard}. *)
 
-(** Bijection from natural number to integer: 0->0, 1->1, 2->-1, 3->2, 4->-2, ... *)
-let nat_to_int n =
-  if n = 0 then 0 else if n mod 2 = 1 then (n + 1) / 2 else -(n / 2)
+(** Bijection from natural number to integer: 0->0, 1->1, 2->-1, 3->2, 4->-2,
+    ... *)
+let nat_to_int n = if n = 0 then 0 else if n mod 2 = 1 then (n + 1) / 2 else -(n / 2)
 
 (** Cantor pairing inverse: given position [n], returns a pair [(a, b)] of
     natural numbers such that [a + b] lies on the [n]-th diagonal. *)
 let cantor_unpair n =
-  let w =
-    int_of_float (floor ((sqrt (float_of_int ((8 * n) + 1)) -. 1.) /. 2.))
-  in
+  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)
+  a, b
 
 (** Integer domain: all integers, enumerated via a bijection from the naturals.
     Schema: [value: integer]. *)
@@ -25,32 +23,18 @@ let integer : Relation.domain =
     match position with
     | Some n ->
         let v = nat_to_int n in
-        let attributes =
-          Tuple.AttributeMap.of_list [ ("value", Obj.magic v) ]
-        in
-        Generator.Value
-          (Tuple.make_materialized ~relation:"integer" ~attributes, generator)
-    | None ->
-        Generator.Error
-          "Cannot produce a randomly enumerated value for the integer domain."
+        let attributes = Tuple.AttributeMap.of_list ["value", Obj.magic v] in
+        Generator.Value (Tuple.make_materialized ~relation:"integer" ~attributes, generator)
+    | None -> Generator.Error "Cannot produce a randomly enumerated value for the integer domain."
   in
   let membership_criteria : Tuple.t -> bool = function
     | Tuple.Materialized _ -> true
     | Tuple.NonMaterialized _ -> false
   in
-  let schema =
-    Schema.empty
-    |> Schema.add "value" "integer"
-  in
+  let schema = Schema.empty |> Schema.add "value" "integer" in
   new Relation.domain
-    ~name:"integer"
-    ~generator
-    ~membership_criteria
-    ~schema
-    ~constraints:None
-    ~cardinality:Conventions.Cardinality.AlephZero
-    ~lineage:None
-    ~provenance:None
+    ~name:"integer" ~generator ~membership_criteria ~schema ~constraints:None
+    ~cardinality:Conventions.Cardinality.AlephZero ~lineage:None ~provenance:None
 
 (** Natural number domain: non-negative integers (0, 1, 2, …). Schema:
     [value: natural]. *)
@@ -58,35 +42,21 @@ let natural : Relation.domain =
   let rec generator (position : int option) : Generator.result =
     match position with
     | Some n ->
-        let attributes =
-          Tuple.AttributeMap.of_list [ ("value", Obj.magic n) ]
-        in
-        Generator.Value
-          (Tuple.make_materialized ~relation:"natural" ~attributes, generator)
-    | None ->
-        Generator.Error
-          "Cannot produce a randomly enumerated value for the natural domain."
+        let attributes = Tuple.AttributeMap.of_list ["value", Obj.magic n] in
+        Generator.Value (Tuple.make_materialized ~relation:"natural" ~attributes, generator)
+    | None -> Generator.Error "Cannot produce a randomly enumerated value for the natural domain."
   in
   let membership_criteria : Tuple.t -> bool = function
     | Tuple.Materialized m -> (
-        match Tuple.AttributeMap.find_opt "value" m.attributes with
-        | Some attr -> (Obj.magic attr : int) >= 0
-        | None -> false)
+      match Tuple.AttributeMap.find_opt "value" m.attributes with
+      | Some attr -> (Obj.magic attr : int) >= 0
+      | None -> false )
     | Tuple.NonMaterialized _ -> false
   in
-  let schema =
-    Schema.empty
-    |> Schema.add "value" "natural"
-  in
+  let schema = Schema.empty |> Schema.add "value" "natural" in
   new Relation.domain
-    ~name:"natural"
-    ~generator
-    ~membership_criteria
-    ~schema
-    ~constraints:None
-    ~cardinality:Conventions.Cardinality.AlephZero
-    ~lineage:None
-    ~provenance:None
+    ~name:"natural" ~generator ~membership_criteria ~schema ~constraints:None
+    ~cardinality:Conventions.Cardinality.AlephZero ~lineage:None ~provenance:None
 
 (** Rational number domain: pairs [(numerator, denominator)] where the
     denominator is never zero. The generator enumerates all such pairs via
@@ -101,50 +71,35 @@ let rational : Relation.domain =
         (* Map b -> non-zero integer: 0->1, 1->-1, 2->2, 3->-2, … *)
         let den = if b mod 2 = 0 then (b / 2) + 1 else -((b + 1) / 2) in
         let attributes =
-          Tuple.AttributeMap.of_list
-            [ ("numerator", Obj.magic num); ("denominator", Obj.magic den) ]
+          Tuple.AttributeMap.of_list ["numerator", Obj.magic num; "denominator", Obj.magic den]
         in
-        Generator.Value
-          (Tuple.make_materialized ~relation:"rational" ~attributes, generator)
-    | None ->
-        Generator.Error
-          "Cannot produce a randomly enumerated value for the rational domain."
+        Generator.Value (Tuple.make_materialized ~relation:"rational" ~attributes, generator)
+    | None -> Generator.Error "Cannot produce a randomly enumerated value for the rational domain."
   in
   let membership_criteria : Tuple.t -> bool = function
     | Tuple.Materialized m -> (
-        match Tuple.AttributeMap.find_opt "denominator" m.attributes with
-        | Some attr -> (Obj.magic attr : int) <> 0
-        | None -> false)
+      match Tuple.AttributeMap.find_opt "denominator" m.attributes with
+      | Some attr -> (Obj.magic attr : int) <> 0
+      | None -> false )
     | Tuple.NonMaterialized _ -> false
   in
   (* Note: Additionally to the membership criteria, we add the constraint here as this relation
      can be further dismembered, rendering the denominator into a lone integer, that should
      propagate the constraint `integer <> 0`. If we declared a domain `integer_without_zero`,
      then this constraint would not be needed as the domain would not be dissociated from the value. *)
-  let constraints: Relation.RelationConstraint.t option =
+  let constraints : Relation.RelationConstraint.t option =
     let denominator_not_zero =
       let open Constraint in
-      Not
-        { body = Eq {left = Var "denominator"; right = Const (Obj.magic 0)}
-        ; universe = "integer" }
+      Not {body= Eq {left= Var "denominator"; right= Const (Obj.magic 0)}; universe= "integer"}
     in
-    Some (("DENOMINATOR_DIFFERENT_FROM_ZERO", denominator_not_zero)
-          |> List.singleton)
+    Some (("DENOMINATOR_DIFFERENT_FROM_ZERO", denominator_not_zero) |> List.singleton)
   in
   let schema =
-    Schema.empty
-    |> Schema.add "numerator" "integer"
-    |> Schema.add "denominator" "integer"
+    Schema.empty |> Schema.add "numerator" "integer" |> Schema.add "denominator" "integer"
   in
   new Relation.domain
-    ~name:"rational"
-    ~generator
-    ~membership_criteria
-    ~schema
-    ~constraints
-    ~cardinality:Conventions.Cardinality.AlephZero
-    ~lineage:None
-    ~provenance:None
+    ~name:"rational" ~generator ~membership_criteria ~schema ~constraints
+    ~cardinality:Conventions.Cardinality.AlephZero ~lineage:None ~provenance:None
 
 (** String domain: any string value. Not enumerable. Schema: [value: string]. *)
 let string : Relation.domain =
@@ -155,17 +110,9 @@ let string : Relation.domain =
     | Tuple.Materialized _ -> true
     | Tuple.NonMaterialized _ -> false
   in
-  let schema =
-    Schema.empty
-    |> Schema.add "value" "string"
-  in
+  let schema = Schema.empty |> Schema.add "value" "string" in
   new Relation.domain
-    ~name:"string"
-    ~generator
-    ~membership_criteria
-    ~schema
+    ~name:"string" ~generator ~membership_criteria ~schema
     ~constraints:None
-    (* TODO: Implement some form of enumeration for strings with a bijection on naturals. *)
-    ~cardinality:Conventions.Cardinality.Continuum
-    ~lineage:None
-    ~provenance:None
+      (* TODO: Implement some form of enumeration for strings with a bijection on naturals. *)
+    ~cardinality:Conventions.Cardinality.Continuum ~lineage:None ~provenance:None
diff --git a/lib/prelude/standard.ml b/lib/prelude/standard.ml
index f38ee40..3822700 100644
--- a/lib/prelude/standard.ml
+++ b/lib/prelude/standard.ml
@@ -5,37 +5,26 @@
    Stdlib.compare on Obj.t, which only works correctly for unboxed integers.
    Extending to other domains requires a proper typed comparison dispatch. *)
 
-let mk v = { Attribute.value = Obj.repr v }
+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]. *)
 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 schema = Schema.empty |> Schema.add "left" domain_name |> Schema.add "right" domain_name in
   let membership_criteria : (*(string -> Merkle.t option) ->*) Tuple.t -> bool =
-   (* fun _tree_of -> function *)
-   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
+    (* fun _tree_of -> function *)
+    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
   new Relation.ephemeral
-    ~name
-    ~schema
-    ~constraints:None
-    ~cardinality
-    ~generator
-    ~membership_criteria
-    ~provenance:None
+    ~name ~schema ~constraints:None ~cardinality ~generator ~membership_criteria ~provenance:None
     ~lineage:None
 
 (** Enumerate pairs (a, b) where a < b using triangular indexing. *)
@@ -44,17 +33,15 @@ let pair_of_nat_lt n =
   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)
+  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.))
-  in
+  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)
+  a, b
 
 let less_than_natural : Relation.ephemeral =
   let rec generator (position : int option) : Generator.result =
@@ -62,14 +49,10 @@ let less_than_natural : Relation.ephemeral =
     | 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) ]
+          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."
+        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)
@@ -83,16 +66,12 @@ let less_than_or_equal_natural : Relation.ephemeral =
         (* 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
+        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 )
+          (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"
+  make_comparison ~name:"natural_natural_less_than_or_equal" ~domain_name:"natural"
     ~pred:(fun c -> c <= 0)
     ~cardinality:Conventions.Cardinality.AlephZero ~generator
 
@@ -102,12 +81,8 @@ let greater_than_natural : Relation.ephemeral =
     | 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 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"
@@ -121,16 +96,12 @@ let greater_than_or_equal_natural : Relation.ephemeral =
         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
+        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 )
+          (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"
+  make_comparison ~name:"natural_natural_greater_than_or_equal" ~domain_name:"natural"
     ~pred:(fun c -> c >= 0)
     ~cardinality:Conventions.Cardinality.AlephZero ~generator
 
@@ -138,11 +109,8 @@ let equal_natural : Relation.ephemeral =
   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"
@@ -154,12 +122,9 @@ let not_equal_natural : Relation.ephemeral =
     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 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"
@@ -168,7 +133,9 @@ let not_equal_natural : Relation.ephemeral =
 
 let plus_natural : Relation.ephemeral =
   let schema =
-    Schema.empty |> Schema.add "a" "natural" |> Schema.add "b" "natural"
+    Schema.empty
+    |> Schema.add "a" "natural"
+    |> Schema.add "b" "natural"
     |> Schema.add "sum" "natural"
   in
   let rec generator (position : int option) : Generator.result =
@@ -176,42 +143,34 @@ let plus_natural : Relation.ephemeral =
     | 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 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 =
-   (* fun _tree_of ->  *)
+    (* fun _tree_of ->  *)
     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
+    | 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
   new Relation.ephemeral
-    ~name:"natural_plus"
-    ~schema
-    ~constraints:None
-    ~cardinality:Conventions.Cardinality.AlephZero
-    ~generator
-    ~membership_criteria
-    ~provenance:None
-    ~lineage:None
+    ~name:"natural_plus" ~schema ~constraints:None ~cardinality:Conventions.Cardinality.AlephZero
+    ~generator ~membership_criteria ~provenance:None ~lineage:None
 
 let times_natural : Relation.ephemeral =
   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 =
@@ -219,43 +178,34 @@ let times_natural : Relation.ephemeral =
     | 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 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 =
-   (* fun _tree_of -> *) 
+    (* fun _tree_of -> *)
     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
+    | 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
   new Relation.ephemeral
-    ~name:"natural_times"
-    ~schema
-    ~constraints:None
-    ~cardinality:Conventions.Cardinality.AlephZero
-    ~generator
-    ~membership_criteria
-    ~provenance:None
-    ~lineage:None
+    ~name:"natural_times" ~schema ~constraints:None ~cardinality:Conventions.Cardinality.AlephZero
+    ~generator ~membership_criteria ~provenance:None ~lineage:None
 
 let minus_natural : Relation.ephemeral =
   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 =
@@ -264,45 +214,37 @@ let minus_natural : Relation.ephemeral =
         (* 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)
+        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 =
-   (* fun _tree_of ->  *)
+    (* fun _tree_of ->  *)
     function
-     | Tuple.Materialized m ->
-         begin 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
-         end
-     | Tuple.NonMaterialized _ -> false
+    | Tuple.Materialized m ->
+      begin 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
+      end
+    | Tuple.NonMaterialized _ -> false
   in
   new Relation.ephemeral
-    ~name:"natural_minus"
-    ~schema
-    ~constraints:None
-    ~cardinality:Conventions.Cardinality.AlephZero
-    ~generator
-    ~membership_criteria
-    ~provenance:None
-    ~lineage:None
+    ~name:"natural_minus" ~schema ~constraints:None ~cardinality:Conventions.Cardinality.AlephZero
+    ~generator ~membership_criteria ~provenance:None ~lineage:None
 
 let divide_natural : Relation.ephemeral =
   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
@@ -318,47 +260,36 @@ let divide_natural : Relation.ephemeral =
         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);
-            ]
+          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)
+        Generator.Value (Tuple.make_materialized ~relation:"divide" ~attributes, generator)
     | None -> Error "Cannot enumerate divide randomly."
   in
   let membership_criteria : Tuple.t -> bool =
-   (* fun _tree_of ->  *)
+    (* fun _tree_of ->  *)
     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
+    | 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
   new Relation.ephemeral
-    ~name:"natural_divide"
-    ~schema
-    ~constraints:None
-    ~cardinality:Conventions.Cardinality.AlephZero
-    ~generator
-    ~membership_criteria
-    ~provenance:None
-    ~lineage:None
+    ~name:"natural_divide" ~schema ~constraints:None ~cardinality:Conventions.Cardinality.AlephZero
+    ~generator ~membership_criteria ~provenance:None ~lineage:None
 
 let prelude_relations =
-  [
-    less_than_natural;
+  [ less_than_natural;
     less_than_or_equal_natural;
     greater_than_natural;
     greater_than_or_equal_natural;
@@ -367,5 +298,4 @@ let prelude_relations =
     plus_natural;
     times_natural;
     minus_natural;
-    divide_natural;
-  ]
+    divide_natural ]