aboutsummaryrefslogtreecommitdiffstats
path: root/lib/prelude
diff options
context:
space:
mode:
Diffstat (limited to 'lib/prelude')
-rw-r--r--lib/prelude/standard.ml36
1 files changed, 36 insertions, 0 deletions
diff --git a/lib/prelude/standard.ml b/lib/prelude/standard.ml
new file mode 100644
index 0000000..43ffc44
--- /dev/null
+++ b/lib/prelude/standard.ml
@@ -0,0 +1,36 @@
+let less_than_natural: Relation.t =
+ let rec generator (position: int option): Generator.result =
+ let pair_of_nat 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) in
+ match position with
+ | Some position ->
+ let (left: Conventions.AbstractValue.t), (right: Conventions.AbstractValue.t) =
+ let (left_value, right_value) = pair_of_nat position in
+ ({ fields = Conventions.AbstractValue.StringMap.of_list [("value", string_of_int left_value)] },
+ { fields = Conventions.AbstractValue.StringMap.of_list [("value", string_of_int right_value)] })
+ in let attributes: Conventions.AbstractValue.t Tuple.AttributeMap.t =
+ Tuple.AttributeMap.of_list [("left", left); ("right", right)]
+ in Generator.Value (Tuple.make_materialized ~relation: "less_than" ~attributes: attributes, generator)
+ | None -> Error "Cannot produce a randomly enumerated value for less_than over naturals."
+ in let membership_criteria: Tuple.t -> bool = function
+ | Tuple.Materialized materialized ->
+ let left = Tuple.AttributeMap.find "left" materialized.attributes
+ in let right = Tuple.AttributeMap.find "right" materialized.attributes
+ in left < right
+ | Tuple.NonMaterialized _non_materialized -> false (* TODO: Handle references later *)
+ in Relation.make
+ ~hash: None
+ ~name: "natural_natural_less_than"
+ ~tree: None
+ ~constraints: None
+ ~cardinality: Conventions.Cardinality.AlephZero
+ ~generator: (Some generator)
+ ~membership_criteria: membership_criteria
+ ~provenance: (Relation.Provenance.Base "less_than")
+ ~lineage: (Relation.Lineage.Base "less_than") \ No newline at end of file