further deletions on drl and prelude

1 files changed, 0 insertions, 301 deletions

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 ]