diff options
Diffstat (limited to 'lib/prelude')
| -rw-r--r-- | lib/prelude/catalog.ml | 135 | ||||
| -rw-r--r-- | lib/prelude/domains.ml | 105 | ||||
| -rw-r--r-- | lib/prelude/standard.ml | 332 |
3 files changed, 273 insertions, 299 deletions
diff --git a/lib/prelude/catalog.ml b/lib/prelude/catalog.ml index 4a7241a..ce36f1e 100644 --- a/lib/prelude/catalog.ml +++ b/lib/prelude/catalog.ml @@ -1,39 +1,35 @@ -(** System catalog helpers. - Pure definitions — no storage access, no manipulation dependency. - Consumed by {!Manipulation.Make} to bootstrap and maintain the six - catalog relations that make the database self-describing. *) +(** System catalog helpers. Pure definitions — no storage access, no + manipulation dependency. Consumed by {!Manipulation.Make} to bootstrap and + maintain the six catalog relations that make the database self-describing. +*) (* TODO: on_rel_name and timing_rel_name are defined and seeded but never written to by any executor. They appear to be stubs for trigger/timing metadata that was never implemented. *) let catalog_prefix = "sakura:" - -let relation_rel_name = catalog_prefix ^ "relation" -let domain_rel_name = catalog_prefix ^ "domain" -let attribute_rel_name = catalog_prefix ^ "attribute" +let relation_rel_name = catalog_prefix ^ "relation" +let domain_rel_name = catalog_prefix ^ "domain" +let attribute_rel_name = catalog_prefix ^ "attribute" let constraint_rel_name = catalog_prefix ^ "constraint" -let on_rel_name = catalog_prefix ^ "on" -let timing_rel_name = catalog_prefix ^ "timing" -let branch_rel_name = catalog_prefix ^ "branch" -let head_rel_name = catalog_prefix ^ "head" +let on_rel_name = catalog_prefix ^ "on" +let timing_rel_name = catalog_prefix ^ "timing" +let branch_rel_name = catalog_prefix ^ "branch" +let head_rel_name = catalog_prefix ^ "head" let catalog_relation_names = - [ relation_rel_name - ; domain_rel_name - ; attribute_rel_name - ; constraint_rel_name - ; on_rel_name - ; timing_rel_name + [ + relation_rel_name; + domain_rel_name; + attribute_rel_name; + constraint_rel_name; + on_rel_name; + timing_rel_name; ] let is_catalog_relation name = List.mem name 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" +let relation_schema : Schema.t = Schema.empty |> Schema.add "name" "string" +let domain_schema : Schema.t = Schema.empty |> Schema.add "name" "string" let attribute_schema : Schema.t = Schema.empty @@ -42,23 +38,20 @@ let attribute_schema : Schema.t = |> Schema.add "domain_name" "string" let constraint_schema : Schema.t = - Schema.empty - |> Schema.add "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" +let on_schema : Schema.t = Schema.empty |> Schema.add "event" "string" +let timing_schema : Schema.t = Schema.empty |> Schema.add "timing" "string" 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) + [ + (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); ] (* TODO: all tuple builders use Obj.magic to coerce string values into @@ -66,51 +59,59 @@ let catalog_definitions = should use Obj.repr instead. *) let build_relation_tuple rel_name : Tuple.materialized = - { Tuple.relation = relation_rel_name - ; attributes = + { + Tuple.relation = relation_rel_name; + attributes = Tuple.AttributeMap.singleton "name" - { Attribute.value = Obj.magic rel_name } + { Attribute.value = Obj.magic rel_name }; } let build_domain_tuple dom_name : Tuple.materialized = - { Tuple.relation = domain_rel_name - ; attributes = + { + Tuple.relation = domain_rel_name; + attributes = Tuple.AttributeMap.singleton "name" - { Attribute.value = Obj.magic dom_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.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 }) - ] - } - ) schema +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.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 }); + ]; + }) + 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.relation = timing_rel_name; + attributes = Tuple.AttributeMap.singleton "timing" - { Attribute.value = Obj.magic timing } + { Attribute.value = Obj.magic timing }; } - diff --git a/lib/prelude/domains.ml b/lib/prelude/domains.ml index 29104bb..d892696 100644 --- a/lib/prelude/domains.ml +++ b/lib/prelude/domains.ml @@ -1,21 +1,19 @@ -(** Predefined fundamental domains, ported from the Erlang implementation. - Each domain carries a generator (for enumeration) and membership criteria - (for validation). Values are stored as {!Conventions.AbstractValue.t} via +(** Predefined fundamental domains, ported from the Erlang implementation. 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) + 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.)) + 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) @@ -26,84 +24,84 @@ let integer : Domain.t = let rec generator (position : int option) : Generator.result = 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) + 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." + 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 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)) + ~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]. *) +(** Natural number domain: non-negative integers (0, 1, 2, …). Schema: + [value: natural]. *) let natural : Domain.t = 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) + 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." + 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 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)) + ~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 - Cantor pairing on the integers. - Schema: [numerator: integer, denominator: integer]. *) + denominator is never zero. The generator enumerates all such pairs via + Cantor pairing on the integers. Schema: + [numerator: integer, denominator: integer]. *) let rational : Domain.t = let rec generator (position : int option) : Generator.result = match position with | Some n -> - let a, b = cantor_unpair n in - let num = nat_to_int a in - (* 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) ] - in - Generator.Value - (Tuple.make_materialized ~relation:"rational" ~attributes, generator) + let a, b = cantor_unpair n in + let num = nat_to_int a in + (* 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) ] + in + Generator.Value + (Tuple.make_materialized ~relation:"rational" ~attributes, generator) | None -> - Generator.Error - "Cannot produce a randomly enumerated value for the rational domain." + 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 Domain.make ~name:"rational" ~generator ~membership_criteria - ~cardinality:Conventions.Cardinality.AlephZero - ~compare:(fun a b -> + ~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]. *) +(** String domain: any string value. Not enumerable. Schema: [value: string]. *) let string : Domain.t = let generator (_ : int option) : Generator.result = Generator.Error "Strings are not enumerable." @@ -113,6 +111,5 @@ let string : Domain.t = | Tuple.NonMaterialized _ -> false in Domain.make ~name:"string" ~generator ~membership_criteria - ~cardinality:Conventions.Cardinality.AlephZero - ~compare:(fun a b -> + ~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 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") |