aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--bin/server.ml70
-rw-r--r--lib/constraint.ml129
-rw-r--r--lib/management/database.ml67
-rw-r--r--lib/manipulation.ml4
-rw-r--r--lib/prelude/catalog.ml23
-rw-r--r--lib/prelude/standard.ml34
6 files changed, 89 insertions, 238 deletions
diff --git a/bin/server.ml b/bin/server.ml
index a7b5fa3..b476631 100644
--- a/bin/server.ml
+++ b/bin/server.ml
@@ -3,9 +3,8 @@ open Relational_engine
let default_port = 7777
let default_limit = 50
-(* ============================================================================
- Minimal JSON serialisation — no external deps
- ============================================================================ *)
+(* TODO: move JSON serialisation into its own module; it's grown enough to
+ warrant separation and the server shouldn't own the wire format. *)
let js_str s =
let buf = Buffer.create (String.length s + 2) in
@@ -30,12 +29,10 @@ let js_arr elems = "[" ^ String.concat "," elems ^ "]"
let js_bool b = if b then "true" else "false"
let js_int n = string_of_int n
-(* ============================================================================
- Value serialisation
- ============================================================================ *)
-
-(** Convert an AbstractValue (Obj.t) to a JSON fragment.
- Uses Obj tag inspection to recover Int / String / Float. *)
+(* TODO: AbstractValue carries no type tag of its own; we recover the OCaml
+ runtime tag here via Obj introspection. This is fragile — it breaks the
+ moment a domain stores a boxed integer or a custom block. The right fix is
+ a typed value representation in Conventions. *)
let abstract_to_json (v : Conventions.AbstractValue.t) =
if Obj.is_int v then js_int (Obj.obj v : int)
else
@@ -51,11 +48,8 @@ let tuple_to_json (t : Tuple.materialized) =
let pairs = Tuple.AttributeMap.bindings t.Tuple.attributes in
js_obj (List.map (fun (k, attr) -> (k, abstract_to_json attr.Attribute.value)) pairs)
-(* ============================================================================
- Relation materialisation
- ============================================================================ *)
-
-(** Iterate a generator up to [limit] tuples; returns (rows, truncated). *)
+(* TODO: Generator.Error is silently treated as end-of-stream here, hiding
+ real failures from the client. *)
let materialize_generator gen limit =
let rec go gen pos acc count =
if count >= limit then (List.rev acc, true)
@@ -74,15 +68,10 @@ let materialize_generator gen limit =
in
go gen 0 [] 0
-(** Materialise either a stored or generator-backed relation. *)
let materialize_relation storage (rel : Relation.t) limit =
let gen = Algebra.Memory.to_generator storage rel in
materialize_generator gen limit
-(* ============================================================================
- JSON response builders
- ============================================================================ *)
-
let short_hash (h : string) = String.sub h 0 (min 8 (String.length h))
let relation_to_json storage (db_hash : string) (rel : Relation.t) limit =
@@ -117,31 +106,27 @@ let error_response db_hash msg =
("db_hash", js_str (short_hash db_hash));
]
-(* ============================================================================
- Error formatting
- ============================================================================ *)
-
let manip_err = function
- | Manipulation.RelationNotFound s -> "RelationNotFound: " ^ s
+ | Manipulation.RelationNotFound s -> "RelationNotFound: " ^ s
| Manipulation.RelationAlreadyExists s -> "RelationAlreadyExists: " ^ s
- | Manipulation.TupleNotFound h -> "TupleNotFound: " ^ h
- | Manipulation.DuplicateTuple h -> "DuplicateTuple: " ^ h
- | Manipulation.ConstraintViolation s -> "ConstraintViolation: " ^ s
- | Manipulation.StorageError s -> "StorageError: " ^ s
-
-(* ============================================================================
- Command execution
- ============================================================================ *)
-
+ | Manipulation.TupleNotFound h -> "TupleNotFound: " ^ h
+ | Manipulation.DuplicateTuple h -> "DuplicateTuple: " ^ h
+ | Manipulation.ConstraintViolation s -> "ConstraintViolation: " ^ s
+ | Manipulation.StorageError s -> "StorageError: " ^ s
+
+(* TODO: language dispatch by trying parsers in sequence is a code smell —
+ a valid DRL expression that happens to also parse as DML would silently
+ be treated as DRL. The three sublanguages should share a common envelope,
+ e.g. a top-level tag distinguishing (Query ...) from (Exec ...). *)
let execute_command storage db_ref cmd =
let db = !db_ref in
let h = db.Management.Database.hash in
- (* 0. Special commands *)
+ (* TODO: (schema) is a stopgap. Introspection should be expressible in
+ DRL itself via the catalog relations, not special-cased here. *)
let cmd = match String.trim cmd with
| "(schema)" -> {|(Base sakura:attribute)|}
| s -> s
in
- (* 1. Try DRL *)
match Drl.Parser.of_string cmd with
| Ok query ->
(match Drl.Executor.Memory.execute storage db query with
@@ -153,7 +138,6 @@ let execute_command storage db_ref cmd =
| Error (Drl.Executor.Memory.AlgebraError (Algebra.GeneratorError s)) ->
error_response h ("GeneratorError: " ^ s))
| Error _ ->
- (* 2. Try DML *)
match Dml.Parser.of_string cmd with
| Ok stmt ->
(match Dml.Executor.Memory.execute storage db stmt with
@@ -167,7 +151,6 @@ let execute_command storage db_ref cmd =
| Error (Dml.Executor.Memory.ParseError s) ->
error_response h ("ParseError: " ^ s))
| Error _ ->
- (* 3. Try DCL *)
match Dcl.Parser.of_string cmd with
| Ok stmt ->
(match Dcl.Executor.Memory.execute storage db stmt with
@@ -181,10 +164,9 @@ let execute_command storage db_ref cmd =
| Error _ ->
error_response h "Parse error: not valid DRL, DML, or DCL"
-(* ============================================================================
- Prelude registration
- ============================================================================ *)
-
+(* TODO: registration failures are silently ignored; a broken prelude
+ relation leaves the catalog in a partially-seeded state with no
+ indication to the user. *)
let register_prelude_relations storage db =
let open Prelude.Standard in
List.fold_left
@@ -211,10 +193,8 @@ let register_prelude_relations storage db =
; divide_natural
]
-(* ============================================================================
- TCP server
- ============================================================================ *)
-
+(* TODO: single-threaded accept loop — one slow or hung client blocks all
+ others. Should use threads or non-blocking I/O. *)
let handle_client storage db_ref fd =
let ic = Unix.in_channel_of_descr fd in
let oc = Unix.out_channel_of_descr fd in
diff --git a/lib/constraint.ml b/lib/constraint.ml
index b7844eb..42f8f88 100644
--- a/lib/constraint.ml
+++ b/lib/constraint.ml
@@ -7,10 +7,14 @@
Negation requires an explicit universe relation name, forcing
closed-world reasoning in first-order logic. *)
+(* TODO: lt/lte/gt/gte/eq/neq/between at the bottom reference target names
+ like "less_than" that don't match the prelude relation names
+ (e.g. "natural_natural_less_than"). These constructors are currently dead
+ code and will fail at runtime if used. *)
+
type relation_name = string
type attr_name = string
-(** Binding expressions resolve against a tuple's attributes *)
type binding_expr =
| Var of attr_name
| Const of Conventions.AbstractValue.t
@@ -27,10 +31,6 @@ type t =
| Exists of { variable : attr_name; quantifier : relation_name; body : t }
| Forall of { variable : attr_name; quantifier : relation_name; body : t }
-(* ============================================================================
- Diagnostics
- ============================================================================ *)
-
type diagnostic =
| MembershipFailed of {
target : string;
@@ -43,11 +43,6 @@ type diagnostic =
}
| ConstraintFailures of (string * diagnostic) list
-(* ============================================================================
- Utility functions
- ============================================================================ *)
-
-(** Collect all [Var] names referenced in a constraint *)
let rec vars_in : t -> attr_name list = function
| MemberOf { binding; _ } ->
BindingMap.fold
@@ -63,7 +58,6 @@ let rec vars_in : t -> attr_name list = function
if List.mem variable inner then inner
else variable :: inner
-(** Rename [Var] references according to a rename list *)
let rec rename_vars (renames : (attr_name * attr_name) list) : t -> t = function
| MemberOf { target; binding } ->
let binding' =
@@ -94,16 +88,14 @@ let rec rename_vars (renames : (attr_name * attr_name) list) : t -> t = function
| Some n -> n
| None -> variable
in
- Exists
- { variable = variable'; quantifier; body = rename_vars renames body }
+ Exists { variable = variable'; quantifier; body = rename_vars renames body }
| Forall { variable; quantifier; body } ->
let variable' =
match List.assoc_opt variable renames with
| Some n -> n
| None -> variable
in
- Forall
- { variable = variable'; quantifier; body = rename_vars renames body }
+ Forall { variable = variable'; quantifier; body = rename_vars renames body }
(** Drop constraints referencing attributes not in the given set.
Returns [None] if the constraint cannot be kept. *)
@@ -121,7 +113,7 @@ let rec filter_by_attrs (attrs : attr_name list) (c : t) : t option =
let kept = List.filter_map (filter_by_attrs attrs) cs in
if kept = [] then None else Some (And kept)
| Or cs ->
- (* For Or, all branches must survive *)
+ (* All branches must survive for Or to remain sound *)
let kept = List.filter_map (filter_by_attrs attrs) cs in
if List.length kept = List.length cs then Some (Or kept) else None
| Exists { variable; quantifier; body } -> (
@@ -133,11 +125,9 @@ let rec filter_by_attrs (attrs : attr_name list) (c : t) : t option =
| Some body' -> Some (Forall { variable; quantifier; body = body' })
| None -> None)
-(** AND-merge two named constraint lists *)
let merge (cs1 : (string * t) list) (cs2 : (string * t) list)
: (string * t) list =
let combined = cs1 @ cs2 in
- (* Group by name and AND-merge duplicates *)
let tbl = Hashtbl.create 16 in
List.iter
(fun (name, c) ->
@@ -151,33 +141,12 @@ let merge (cs1 : (string * t) list) (cs2 : (string * t) list)
(name, merged) :: acc)
tbl []
-(* ============================================================================
- Smart constructors
- ============================================================================ *)
-
let member_of ~target ~binding = MemberOf { target; binding }
-
let not_ ~universe body = Not { body; universe }
-
-let and_ cs =
- match cs with
- | [ c ] -> c
- | _ -> And cs
-
-let or_ cs =
- match cs with
- | [ c ] -> c
- | _ -> Or cs
-
-let exists ~variable ~quantifier body =
- Exists { variable; quantifier; body }
-
-let forall ~variable ~quantifier body =
- Forall { variable; quantifier; body }
-
-(* ============================================================================
- Evaluation context (no dependency on Relation/Database/Manipulation)
- ============================================================================ *)
+let and_ cs = match cs with [ c ] -> c | _ -> And cs
+let or_ cs = match cs with [ c ] -> c | _ -> Or cs
+let exists ~variable ~quantifier body = Exists { variable; quantifier; body }
+let forall ~variable ~quantifier body = Forall { variable; quantifier; body }
type eval_context = {
check_membership :
@@ -189,11 +158,6 @@ type eval_context = {
(attr_name * Conventions.AbstractValue.t) list list option;
}
-(* ============================================================================
- Binding resolution
- ============================================================================ *)
-
-(** Resolve binding expressions against a materialized tuple *)
let bind (b : binding) (tuple : Tuple.materialized)
: (attr_name * Conventions.AbstractValue.t) list =
BindingMap.fold
@@ -211,13 +175,6 @@ let bind (b : binding) (tuple : Tuple.materialized)
| None -> acc)
b []
-(* ============================================================================
- Constraint evaluation
- ============================================================================ *)
-
-(** Evaluate a constraint against a tuple in the given context.
- Returns [Ok true] if satisfied, [Ok false] should not occur —
- failures return [Error diagnostic]. *)
let rec evaluate (ctx : eval_context) (tuple : Tuple.materialized) (c : t)
: (bool, diagnostic) result =
match c with
@@ -227,9 +184,8 @@ let rec evaluate (ctx : eval_context) (tuple : Tuple.materialized) (c : t)
else Error (MembershipFailed { target; bound_values })
| Not { body; universe = _ } ->
(* The universe is a declarative annotation for closed-world reasoning.
- At runtime, we simply negate the body. The universe ensures logical
- soundness at the schema level, not as a runtime tuple-existence check
- (the tuple being validated hasn't been stored yet). *)
+ At runtime we negate the body; the universe enforces logical soundness
+ at the schema level, not as a runtime tuple-existence check. *)
(match evaluate ctx tuple body with
| Ok true -> Ok false
| Ok false -> Ok true
@@ -239,13 +195,11 @@ let rec evaluate (ctx : eval_context) (tuple : Tuple.materialized) (c : t)
| Or cs -> evaluate_or ctx tuple cs
| Exists { variable; quantifier; body } -> (
match ctx.iterate_finite quantifier with
- | None ->
- Error (UnboundedQuantifier { variable; quantifier })
+ | None -> Error (UnboundedQuantifier { variable; quantifier })
| Some rows ->
let rec check = function
| [] -> Ok false
| row :: rest ->
- (* Bind the quantifier variable into scope *)
let extended_tuple = extend_tuple tuple variable row in
(match evaluate ctx extended_tuple body with
| Ok true -> Ok true
@@ -255,8 +209,7 @@ let rec evaluate (ctx : eval_context) (tuple : Tuple.materialized) (c : t)
check rows)
| Forall { variable; quantifier; body } -> (
match ctx.iterate_finite quantifier with
- | None ->
- Error (UnboundedQuantifier { variable; quantifier })
+ | None -> Error (UnboundedQuantifier { variable; quantifier })
| Some rows ->
let rec check = function
| [] -> Ok true
@@ -286,9 +239,6 @@ and evaluate_or ctx tuple = function
| Ok false -> evaluate_or ctx tuple rest
| Error _ -> evaluate_or ctx tuple rest)
-(** Extend a tuple with bindings from a quantifier row.
- Each row entry [(attr, value)] gets added with [variable] as prefix
- if the attr name doesn't match an existing attribute. *)
and extend_tuple (tuple : Tuple.materialized)
(_variable : attr_name)
(row : (attr_name * Conventions.AbstractValue.t) list)
@@ -301,7 +251,6 @@ and extend_tuple (tuple : Tuple.materialized)
in
{ tuple with attributes = extra_attrs }
-(** Evaluate a list of named constraints, collecting all failures *)
let evaluate_named (ctx : eval_context) (tuple : Tuple.materialized)
(named : (string * t) list) : (bool, diagnostic) result =
let failures =
@@ -318,59 +267,33 @@ let evaluate_named (ctx : eval_context) (tuple : Tuple.materialized)
| [] -> Ok true
| fs -> Error (ConstraintFailures fs)
-(* ============================================================================
- Comparison shorthand constructors
- ============================================================================ *)
-
let make_comparison_binding ~left ~right =
BindingMap.empty
|> BindingMap.add "left" left
|> BindingMap.add "right" right
let lt ~left ~right =
- MemberOf
- { target = "less_than"; binding = make_comparison_binding ~left ~right }
+ MemberOf { target = "less_than"; binding = make_comparison_binding ~left ~right }
let lte ~left ~right =
- MemberOf
- {
- target = "less_than_or_equal";
- binding = make_comparison_binding ~left ~right;
- }
+ MemberOf { target = "less_than_or_equal"; binding = make_comparison_binding ~left ~right }
let gt ~left ~right =
- MemberOf
- {
- target = "greater_than";
- binding = make_comparison_binding ~left ~right;
- }
+ MemberOf { target = "greater_than"; binding = make_comparison_binding ~left ~right }
let gte ~left ~right =
- MemberOf
- {
- target = "greater_than_or_equal";
- binding = make_comparison_binding ~left ~right;
- }
+ MemberOf { target = "greater_than_or_equal"; binding = make_comparison_binding ~left ~right }
let eq ~left ~right =
- MemberOf
- { target = "equal"; binding = make_comparison_binding ~left ~right }
+ MemberOf { target = "equal"; binding = make_comparison_binding ~left ~right }
let neq ~left ~right =
- MemberOf
- { target = "not_equal"; binding = make_comparison_binding ~left ~right }
+ MemberOf { target = "not_equal"; binding = make_comparison_binding ~left ~right }
let between ~value ~low ~high =
And
- [
- MemberOf
- {
- target = "greater_than_or_equal";
- binding = make_comparison_binding ~left:value ~right:low;
- };
- MemberOf
- {
- target = "less_than_or_equal";
- binding = make_comparison_binding ~left:value ~right:high;
- };
+ [ MemberOf { target = "greater_than_or_equal";
+ binding = make_comparison_binding ~left:value ~right:low }
+ ; MemberOf { target = "less_than_or_equal";
+ binding = make_comparison_binding ~left:value ~right:high }
]
diff --git a/lib/management/database.ml b/lib/management/database.ml
index 08e03b8..2dc0ae6 100644
--- a/lib/management/database.ml
+++ b/lib/management/database.ml
@@ -1,12 +1,10 @@
-(** Database state management.
+(** Database state: a named collection of relations with a Merkle tree over
+ their hashes, a domain registry, and a history chain of prior hashes.
+ All mutations produce a new value; no in-place update. *)
- A database is a collection of relations with:
- - A merkle tree of relation hashes (for integrity verification)
- - A map of relation names to their actual Relation.t objects (integrated cache)
- - A history of previous database hashes (for time-travel queries)
-
- All mutations produce a new database state with a new hash.
- The history chain allows reconstruction of any past state. *)
+(* TODO: history is an unbounded list of hashes; there is no way to
+ reconstruct a past state from a hash alone without a separate snapshot
+ store. Either cap the history or make it actually useful. *)
module RelationMap = Map.Make(String)
@@ -14,8 +12,8 @@ type t = {
hash : Conventions.Hash.t;
name : Conventions.Name.t;
tree : Merkle.t;
- relations : Relation.t RelationMap.t; (* Stores actual relations, not just hashes *)
- domains : Domain.t RelationMap.t; (* Domain registry: prelude + user-defined *)
+ relations : Relation.t RelationMap.t;
+ domains : Domain.t RelationMap.t;
history : Conventions.Hash.t list;
timestamp : float;
}
@@ -30,13 +28,11 @@ let empty ~name = {
timestamp = Unix.gettimeofday ();
}
-(** Compute database hash from the merkle tree root *)
let compute_hash db =
match Merkle.root_hash db.tree with
| Some root -> root
| None -> Conventions.Hash.hash_text db.name
-(** Update database with new relations map and tree *)
let update_state db ~relations ~tree =
let new_hash =
match Merkle.root_hash tree with
@@ -44,21 +40,11 @@ let update_state db ~relations ~tree =
| None -> Conventions.Hash.hash_text db.name
in
let history = if db.hash = "" then db.history else db.hash :: db.history in
- {
- hash = new_hash;
- name = db.name;
- tree;
- relations;
- domains = db.domains;
- history;
- timestamp = Unix.gettimeofday ();
- }
-
-(** Get a relation by name *)
-let get_relation db name =
- RelationMap.find_opt name db.relations
-
-(** Get a relation's hash by name *)
+ { hash = new_hash; name = db.name; tree; relations;
+ domains = db.domains; history; timestamp = Unix.gettimeofday () }
+
+let get_relation db name = RelationMap.find_opt name db.relations
+
let get_relation_hash db name =
match RelationMap.find_opt name db.relations with
| None -> None
@@ -67,10 +53,11 @@ let get_relation_hash db name =
let get_relation_names db =
RelationMap.fold (fun name _ acc -> name :: acc) db.relations []
-let has_relation db name =
- RelationMap.mem name db.relations
+let has_relation db name = RelationMap.mem name db.relations
-(** Add a relation to the database *)
+(* TODO: computing the hash here for hash:None relations (ephemeral/prelude)
+ is a layering violation — callers should assign the hash before calling
+ add_relation, not rely on this fallback. *)
let add_relation db ~(relation : Relation.t) =
let relation_hash = match relation.hash with
| Some h -> h
@@ -83,7 +70,6 @@ let add_relation db ~(relation : Relation.t) =
let relations = RelationMap.add relation.name relation db.relations in
update_state db ~relations ~tree
-(** Remove a relation from the database *)
let remove_relation db ~name =
match RelationMap.find_opt name db.relations with
| None -> db
@@ -93,11 +79,10 @@ let remove_relation db ~name =
let relations = RelationMap.remove name db.relations in
update_state db ~relations ~tree
-(** Update a relation in the database (after tuple insert/delete) *)
let update_relation db ~(relation : Relation.t) =
let name = relation.name in
match RelationMap.find_opt name db.relations with
- | None -> db (* Relation doesn't exist, no-op *)
+ | None -> db
| Some old_relation ->
let old_hash = Option.get old_relation.hash in
let new_hash = Option.get relation.hash in
@@ -105,27 +90,15 @@ let update_relation db ~(relation : Relation.t) =
let relations = RelationMap.add name relation db.relations in
update_state db ~relations ~tree
-(* ============================================================================
- Domain Registry - prelude and user-defined domains
- ============================================================================ *)
-
-(** Register a domain in the database. Overwrites any existing domain with
- the same name, allowing user-defined domains to shadow prelude ones. *)
let add_domain db (domain : Domain.t) =
{ db with domains = RelationMap.add domain.name domain db.domains }
-(** Look up a domain by name *)
-let get_domain db name =
- RelationMap.find_opt name db.domains
+let get_domain db name = RelationMap.find_opt name db.domains
-(** List all registered domain names *)
let get_domain_names db =
RelationMap.fold (fun name _ acc -> name :: acc) db.domains []
-(** Check whether a domain is registered *)
-let has_domain db name =
- RelationMap.mem name db.domains
+let has_domain db name = RelationMap.mem name db.domains
-(** Remove a domain from the registry *)
let remove_domain db name =
{ db with domains = RelationMap.remove name db.domains }
diff --git a/lib/manipulation.ml b/lib/manipulation.ml
index 5f7cfb9..2a43b6c 100644
--- a/lib/manipulation.ml
+++ b/lib/manipulation.ml
@@ -45,9 +45,7 @@ let build_membership_criteria _schema : (Tuple.t -> bool) =
module Make (Storage : Management.Physical.S) = struct
type storage = Storage.t
- (* ============================================================================
- Constraint evaluation context
- ============================================================================ *)
+ (* Constraint evaluation context *)
(** Build an eval_context closed over a specific (storage, db) snapshot.
All relation lookups resolve against this exact database version. *)
diff --git a/lib/prelude/catalog.ml b/lib/prelude/catalog.ml
index ae43c4d..a277066 100644
--- a/lib/prelude/catalog.ml
+++ b/lib/prelude/catalog.ml
@@ -1,14 +1,13 @@
(** 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. *)
-let catalog_prefix = "sakura:"
+(* 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. *)
-(*
- Catalog relation names
- *)
+let catalog_prefix = "sakura:"
let relation_rel_name = catalog_prefix ^ "relation"
let domain_rel_name = catalog_prefix ^ "domain"
@@ -26,12 +25,7 @@ let catalog_relation_names =
; timing_rel_name
]
-let is_catalog_relation name =
- List.mem name catalog_relation_names
-
-(*
- Schema definitions
- *)
+let is_catalog_relation name = List.mem name catalog_relation_names
let relation_schema : Schema.t =
Schema.empty |> Schema.add "name" "string"
@@ -56,7 +50,6 @@ let on_schema : Schema.t =
let timing_schema : Schema.t =
Schema.empty |> Schema.add "timing" "string"
-(** All (name, schema) pairs for the 6 catalog relations, in bootstrap order. *)
let catalog_definitions =
[ (relation_rel_name, relation_schema)
; (domain_rel_name, domain_schema)
@@ -66,9 +59,9 @@ let catalog_definitions =
; (timing_rel_name, timing_schema)
]
-(*
- Tuple builders
- *)
+(* 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
diff --git a/lib/prelude/standard.ml b/lib/prelude/standard.ml
index efcb7ae..68012fc 100644
--- a/lib/prelude/standard.ml
+++ b/lib/prelude/standard.ml
@@ -1,18 +1,14 @@
-(** Domain-parameterized comparison and arithmetic relations.
+(** Comparison and arithmetic relations over the natural domain. *)
- All comparison relations use a two-attribute schema [(left, right)]
- with both attributes in the same domain. The domain's [compare] function
- is used for evaluation — no more spreading [Obj.magic]. *)
+(* 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. *)
-(* Helper: wrap a native value in the Attribute.materialized record *)
let mk v = { Attribute.value = Obj.repr v }
-(* ============================================================================
- Comparison relation factory
- ============================================================================ *)
-
-(** Build a comparison relation parameterized by domain.
- [pred] receives the result of [Domain.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
@@ -34,13 +30,7 @@ let make_comparison ~name ~domain_name ~pred ~cardinality ~generator =
~provenance:(Relation.Provenance.Base name)
~lineage:(Relation.Lineage.Base name)
-(* ============================================================================
- Pair enumeration for comparison generators
- ============================================================================ *)
-
-(** Enumerate pairs (a, b) from naturals where a < b.
- Uses triangular indexing: position n maps to row r, column c
- where a = c, b = r, and a < b. *)
+(** 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
@@ -48,7 +38,7 @@ let pair_of_nat_lt n =
let left = n - t_prev in
(left, r)
-(** Enumerate all pairs (a, b) from naturals via Cantor pairing. *)
+(** 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.))
@@ -58,9 +48,6 @@ let cantor_pair_of_nat n =
let a = w - b in
(a, b)
-(* ============================================================================
- Concrete comparison relations (natural domain)
- ============================================================================ *)
let less_than_natural : Relation.t =
let rec generator (position : int option) : Generator.result =
@@ -179,9 +166,6 @@ let not_equal_natural : Relation.t =
~pred:(fun c -> c <> 0)
~cardinality:Conventions.Cardinality.AlephZero ~generator
-(* ============================================================================
- Arithmetic relations (natural domain)
- ============================================================================ *)
let plus_natural : Relation.t =
let schema =
generated by cgit v1.2.3 (git 2.25.1) at 2026-11-04 23:54:13 +0000