diff options
| -rw-r--r-- | bin/dune | 1 | ||||
| -rw-r--r-- | lib/drl/ast.ml | 26 | ||||
| -rw-r--r-- | lib/drl/executor.ml | 62 | ||||
| -rw-r--r-- | lib/drl/parser.ml | 17 | ||||
| -rw-r--r-- | lib/drl/sublanguage.ml | 11 | ||||
| -rw-r--r-- | lib/dune | 4 | ||||
| -rw-r--r-- | lib/generator.ml | 2 | ||||
| -rw-r--r-- | lib/prelude/catalog.ml | 158 | ||||
| -rw-r--r-- | lib/prelude/domains.ml | 118 | ||||
| -rw-r--r-- | lib/prelude/standard.ml | 301 |
10 files changed, 1 insertions, 699 deletions
@@ -3,5 +3,4 @@ (public_name sakura-server) (modules server) (libraries relational_engine unix) - (link_deps ../shared/shabptree/sakura_shabptree.dll) (modes byte exe)) diff --git a/lib/drl/ast.ml b/lib/drl/ast.ml deleted file mode 100644 index 2fd56e6..0000000 --- a/lib/drl/ast.ml +++ /dev/null @@ -1,26 +0,0 @@ -open Sexplib.Std - -(** Literal values for Const nodes *) -type value = Int of int | Float of float | Str of string | Bool of bool [@@deriving sexp] - -(** Convert an AST value to an AbstractValue.t (Obj.t) via Obj.repr *) -let value_to_abstract : value -> Conventions.AbstractValue.t = function - | Int n -> Obj.repr n - | Float f -> Obj.repr f - | Str s -> Obj.repr s - | Bool b -> Obj.repr b - -type direction = Asc | Desc [@@deriving sexp] - -type query = - | Base of string (** base relation by name *) - | Const of (string * value) list (** constant single-tuple relation *) - | Select of query * query (** σ semijoin: (filter, source) *) - | Join of string list * query * query (** ⋈ natural equijoin on named attrs *) - | Cartesian of query * query (** × Cartesian product *) - | Project of string list * query (** π restrict columns *) - | Rename of (string * string) list * query (** ρ rename (old,new) pairs *) - | Union of query * query (** ∪ — compatible schemas assumed *) - | Diff of query * query (** − *) - | Take of int * query (** τ *) -[@@deriving sexp] diff --git a/lib/drl/executor.ml b/lib/drl/executor.ml deleted file mode 100644 index 6ff3551..0000000 --- a/lib/drl/executor.ml +++ /dev/null @@ -1,62 +0,0 @@ -module Make (NT : Nt.S) = struct - module Error = struct - open Condition - - let parse_error error = condition "parse-error" error empty - - let relation_not_found name = - condition "relation-not-found" "Relation not found" ("name" |=| of_string name) - - let unsupported_operator msg = condition "unsupported-operator" msg empty - end - - let ( let* ) = Result.bind - - (* Compile a DRL AST query to a Tarski VM plan node tree. - A qualified base reference ([<mg>:<rel>]) resolves through [ctx.resolve] - to its stored-relation path; an unqualified name resolves to the - session-scoped ephemeral binding created by DML [Define]. *) - let rec compile (ctx : Sublanguage_context.t) (q : Ast.query) : (Nt.plan_node, Condition.t) result - = - match q with - | Ast.Base name -> ( - match Qualified_name.try_parse name with - | Error _ -> Ok (Nt.Scan {path= Sublanguage_context.ephemeral_path ctx name; args= []}) - | Ok fqn -> Ok (Nt.Scan {path= ctx.resolve fqn; args= []}) ) - | Ast.Join (on_attrs, q1, q2) -> - let* p1 = compile ctx q1 in - let* p2 = compile ctx q2 in - Ok (Nt.Join {left= p1; right= p2; on_attrs}) - | Ast.Take (n, q) -> - let* p = compile ctx q in - Ok (Nt.Take {limit= n; source= p}) - | Ast.Project (attrs, q) -> - let* p = compile ctx q in - Ok (Nt.Project {attrs; source= p}) - | Ast.Const _ -> - Error - (Error.unsupported_operator "Const: literal relations not yet reachable by VM; use Base") - | _ -> - Error - (Error.unsupported_operator - "Select/Rename/Union/Diff/Cartesian require VM operators not yet implemented" ) - - let page_limit = 16 - - let execute (ctx : Sublanguage_context.t) (q : Ast.query) : - (Sublanguage_types.result, Condition.t) result = - let* plan = compile ctx q in - let rel_name = "query_result" in - let* stream = NT.execute_query plan ~rel_name in - let rec drain acc count = - if count >= page_limit then List.rev acc, true - else - match NT.stream_next stream with - | Error _ -> List.rev acc, false - | Ok None -> List.rev acc, false - | Ok (Some t) -> drain (t :: acc) (count + 1) - in - let rows, has_more = drain [] 0 in - ignore (NT.stream_close stream); - Ok (Sublanguage_types.Cursor {cursor_id= "0"; rows; has_more}) -end diff --git a/lib/drl/parser.ml b/lib/drl/parser.ml deleted file mode 100644 index abb3070..0000000 --- a/lib/drl/parser.ml +++ /dev/null @@ -1,17 +0,0 @@ -module Error = struct - open Condition - - let parse_error msg = condition "parse-error" msg empty -end - -let of_sexp sexp = - match Ast.query_of_sexp sexp with - | q -> Ok q - | exception exn -> Error (Error.parse_error (Printexc.to_string exn)) - -let of_string s = - match Sexplib.Sexp.of_string s |> Ast.query_of_sexp with - | q -> Ok q - | exception exn -> Error (Error.parse_error (Printexc.to_string exn)) - -let to_string q = Ast.sexp_of_query q |> Sexplib.Sexp.to_string_hum diff --git a/lib/drl/sublanguage.ml b/lib/drl/sublanguage.ml deleted file mode 100644 index d5c5977..0000000 --- a/lib/drl/sublanguage.ml +++ /dev/null @@ -1,11 +0,0 @@ -module Make (NT : Nt.S) = struct - module Exec = Executor.Make (NT) - - type configuration = unit - type ast = Ast.query - - let name = "drl" - let parse _ = Ok () - let parse_sexp sexp = Parser.of_sexp sexp - let execute ctx ast = Exec.execute ctx ast -end @@ -5,7 +5,6 @@ (public_name sakura.relational_engine) (libraries dynlink - sakura_prl_api sha data-encoding lwt @@ -17,5 +16,4 @@ ctypes ctypes.foreign) (preprocess - (pps ppx_deriving.show ppx_sexp_conv ppx_protocol_conv)) - (flags :standard -cclib -lRNT)) + (pps ppx_deriving.show ppx_sexp_conv ppx_protocol_conv))) diff --git a/lib/generator.ml b/lib/generator.ml deleted file mode 100644 index 5f0a50f..0000000 --- a/lib/generator.ml +++ /dev/null @@ -1,2 +0,0 @@ -type result = Done | Value of Tuple.t * (int option -> result) | Error of string -and t = int option -> result diff --git a/lib/prelude/catalog.ml b/lib/prelude/catalog.ml deleted file mode 100644 index 26fe30c..0000000 --- a/lib/prelude/catalog.ml +++ /dev/null @@ -1,158 +0,0 @@ -(** System catalog helpers. Pure definitions — no storage access, no - manipulation dependency. Consumed by {!Manipulation.Make} and - {!Catalog.Make} to bootstrap the catalog relations that make each multigroup - 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. *) - -(** 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" - -let catalog_prefix = "public:" -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 multigroup_rel_name = catalog_prefix ^ "multigroup" -let schema_rel_name = catalog_prefix ^ "schema" -let function_predicate_rel_name = catalog_prefix ^ "function_predicate" -let loaded_library_rel_name = catalog_prefix ^ "loaded_library" - -(** Relations present in every multigroup's catalog. *) -let catalog_relation_names = - [ relation_rel_name; - domain_rel_name; - attribute_rel_name; - constraint_rel_name; - on_rel_name; - timing_rel_name; - schema_rel_name; - function_predicate_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 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" - -let attribute_schema : Schema.t = - Schema.empty - |> Schema.add "relation_name" "string" - |> Schema.add "attr_name" "string" - |> Schema.add "domain_name" "string" - -let constraint_schema : Schema.t = - 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 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.add "symbol" "string" - |> Schema.add "cardinality" "string" - |> Schema.add "purity" "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 ] - -(** Extra definitions seeded only into the sakura meta-multigroup. *) -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} } - -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 = - 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.AttributeMap.of_list - [ "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} } - -let build_timing_tuple timing : Tuple.materialized = - { 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} } - -let build_schema_tuple schema_name : Tuple.materialized = - { 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) - -let purity_of_string s = - match Conventions.Purity.t_of_sexp (Sexplib.Sexp.of_string s) with - | p -> Some p - | exception _ -> None - -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= - 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)} ] } - -let build_loaded_library_tuple path : Tuple.materialized = - { 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 deleted file mode 100644 index 264bf03..0000000 --- a/lib/prelude/domains.ml +++ /dev/null @@ -1,118 +0,0 @@ -(** 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) - -(** 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 t = w * (w + 1) / 2 in - let b = n - t in - let a = w - b in - a, b - -(** Integer domain: all integers, enumerated via a bijection from the naturals. - Schema: [value: integer]. *) -let integer : Relation.domain = - 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) - | 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 - new Relation.domain - ~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]. *) -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." - 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 ) - | Tuple.NonMaterialized _ -> false - 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 - -(** 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]. *) -let rational : Relation.domain = - 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) - | 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 ) - | 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 denominator_not_zero = - let open Constraint in - Not {body= Eq {left= Var "denominator"; right= Const (Obj.magic 0)}; universe= "integer"} - in - Some (("DENOMINATOR_DIFFERENT_FROM_ZERO", denominator_not_zero) |> List.singleton) - in - let schema = - 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 - -(** String domain: any string value. Not enumerable. Schema: [value: string]. *) -let string : Relation.domain = - let generator (_ : int option) : Generator.result = - Generator.Error "Strings are not enumerable." - in - let membership_criteria : Tuple.t -> bool = function - | Tuple.Materialized _ -> true - | Tuple.NonMaterialized _ -> false - in - let schema = Schema.empty |> Schema.add "value" "string" in - new Relation.domain - ~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 diff --git a/lib/prelude/standard.ml b/lib/prelude/standard.ml deleted file mode 100644 index 3822700..0000000 --- a/lib/prelude/standard.ml +++ /dev/null @@ -1,301 +0,0 @@ -(** Comparison and arithmetic relations over the natural domain. *) - -(* TODO: all relations here are hardcoded to naturals. The make_comparison - factory accepts a domain_name string but membership_criteria always uses - 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} - -(** 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 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 - in - new Relation.ephemeral - ~name ~schema ~constraints:None ~cardinality ~generator ~membership_criteria ~provenance:None - ~lineage:None - -(** 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 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.)) 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.ephemeral = - 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) - | None -> Error "Cannot produce a randomly enumerated value for less_than over naturals." - in - make_comparison ~name:"natural_natural_less_than" ~domain_name:"natural" - ~pred:(fun c -> c < 0) - ~cardinality:Conventions.Cardinality.AlephZero ~generator - -let less_than_or_equal_natural : Relation.ephemeral = - 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) - | None -> Error "Cannot enumerate less_than_or_equal randomly." - in - make_comparison ~name:"natural_natural_less_than_or_equal" ~domain_name:"natural" - ~pred:(fun c -> c <= 0) - ~cardinality:Conventions.Cardinality.AlephZero ~generator - -let greater_than_natural : Relation.ephemeral = - 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) - | None -> Error "Cannot enumerate greater_than randomly." - in - make_comparison ~name:"natural_natural_greater_than" ~domain_name:"natural" - ~pred:(fun c -> c > 0) - ~cardinality:Conventions.Cardinality.AlephZero ~generator - -let greater_than_or_equal_natural : Relation.ephemeral = - 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) - | None -> Error "Cannot enumerate greater_than_or_equal randomly." - in - make_comparison ~name:"natural_natural_greater_than_or_equal" ~domain_name:"natural" - ~pred:(fun c -> c >= 0) - ~cardinality:Conventions.Cardinality.AlephZero ~generator - -let equal_natural : Relation.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) - | None -> Error "Cannot enumerate equal randomly." - in - make_comparison ~name:"natural_natural_equal" ~domain_name:"natural" - ~pred:(fun c -> c = 0) - ~cardinality:Conventions.Cardinality.AlephZero ~generator - -let not_equal_natural : Relation.ephemeral = - 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) - | 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.ephemeral = - let schema = - Schema.empty - |> Schema.add "a" "natural" - |> Schema.add "b" "natural" - |> Schema.add "sum" "natural" - in - let rec generator (position : int option) : Generator.result = - match position with - | Some n -> - let a, b = cantor_pair_of_nat n in - let s = a + b in - let attributes = Tuple.AttributeMap.of_list ["a", 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 -> *) - function - | Tuple.Materialized m -> ( - match - ( Tuple.AttributeMap.find_opt "a" m.attributes, - Tuple.AttributeMap.find_opt "b" m.attributes, - Tuple.AttributeMap.find_opt "sum" m.attributes ) - with - | Some a, Some b, Some s -> - (Obj.magic a.Attribute.value : int) + (Obj.magic b.Attribute.value : int) - = (Obj.magic s.Attribute.value : int) - | _ -> false ) - | Tuple.NonMaterialized _ -> false - in - new Relation.ephemeral - ~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.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) - | None -> Error "Cannot enumerate times randomly." - in - let membership_criteria : Tuple.t -> bool = - (* 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 - in - new Relation.ephemeral - ~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.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) - | None -> Error "Cannot enumerate minus randomly." - in - let membership_criteria : Tuple.t -> bool = - (* 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 - in - new Relation.ephemeral - ~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.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) - | None -> Error "Cannot enumerate divide randomly." - in - let membership_criteria : Tuple.t -> bool = - (* 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 - in - new Relation.ephemeral - ~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_or_equal_natural; - greater_than_natural; - greater_than_or_equal_natural; - equal_natural; - not_equal_natural; - plus_natural; - times_natural; - minus_natural; - divide_natural ] |