From cce3bfba31b32c13ea116a214306d96fe1eb27eb Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Sun, 8 Mar 2026 20:48:14 -0300 Subject: format todos and comment improvement --- bin/server.ml | 70 +++++++++--------------- lib/constraint.ml | 129 +++++++++------------------------------------ lib/management/database.ml | 67 +++++++---------------- lib/manipulation.ml | 4 +- lib/prelude/catalog.ml | 23 +++----- lib/prelude/standard.ml | 34 ++++-------- 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 = -- cgit v1.2.3