diff options
Diffstat (limited to '')
| -rw-r--r-- | lib/prelude/standard.ml | 36 |
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 |