From c284fcd570342c31bc21169960579a20a763e32e Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Tue, 23 Jun 2026 23:53:26 -0300 Subject: Format --- lib/prelude/catalog.ml | 154 +++++++++--------------- lib/prelude/domains.ml | 133 +++++++-------------- lib/prelude/standard.ml | 304 +++++++++++++++++++----------------------------- 3 files changed, 209 insertions(+), 382 deletions(-) (limited to 'lib/prelude') 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 ] -- cgit v1.2.3