diff options
Diffstat (limited to 'lib/prelude/domains.ml')
| -rw-r--r-- | lib/prelude/domains.ml | 118 |
1 files changed, 0 insertions, 118 deletions
diff --git a/lib/prelude/domains.ml b/lib/prelude/domains.ml deleted file mode 100644 index 264bf03..0000000 --- a/lib/prelude/domains.ml +++ /dev/null @@ -1,118 +0,0 @@ -(** Predefined fundamental domains. Each domain carries a generator (for - enumeration) and membership criteria (for validation). Values are stored as - {!Conventions.AbstractValue.t} via [Obj.magic], following the same - convention as {!Standard}. *) - -(** Bijection from natural number to integer: 0->0, 1->1, 2->-1, 3->2, 4->-2, - ... *) -let nat_to_int n = if n = 0 then 0 else if n mod 2 = 1 then (n + 1) / 2 else -(n / 2) - -(** Cantor pairing inverse: given position [n], returns a pair [(a, b)] of - natural numbers such that [a + b] lies on the [n]-th diagonal. *) -let cantor_unpair 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 - -(** Integer domain: all integers, enumerated via a bijection from the naturals. - Schema: [value: integer]. *) -let integer : Relation.domain = - let rec generator (position : int option) : Generator.result = - match position with - | Some n -> - let v = nat_to_int n in - let attributes = Tuple.AttributeMap.of_list ["value", Obj.magic v] in - Generator.Value (Tuple.make_materialized ~relation:"integer" ~attributes, generator) - | None -> Generator.Error "Cannot produce a randomly enumerated value for the integer domain." - in - let membership_criteria : Tuple.t -> bool = function - | Tuple.Materialized _ -> true - | Tuple.NonMaterialized _ -> false - in - let schema = Schema.empty |> Schema.add "value" "integer" in - new Relation.domain - ~name:"integer" ~generator ~membership_criteria ~schema ~constraints:None - ~cardinality:Conventions.Cardinality.AlephZero ~lineage:None ~provenance:None - -(** Natural number domain: non-negative integers (0, 1, 2, …). Schema: - [value: natural]. *) -let natural : Relation.domain = - let rec generator (position : int option) : Generator.result = - match position with - | Some n -> - let attributes = Tuple.AttributeMap.of_list ["value", Obj.magic n] in - Generator.Value (Tuple.make_materialized ~relation:"natural" ~attributes, generator) - | None -> Generator.Error "Cannot produce a randomly enumerated value for the natural domain." - in - let membership_criteria : Tuple.t -> bool = function - | Tuple.Materialized m -> ( - match Tuple.AttributeMap.find_opt "value" m.attributes with - | Some attr -> (Obj.magic attr : int) >= 0 - | None -> false ) - | Tuple.NonMaterialized _ -> false - in - let schema = Schema.empty |> Schema.add "value" "natural" in - new Relation.domain - ~name:"natural" ~generator ~membership_criteria ~schema ~constraints:None - ~cardinality:Conventions.Cardinality.AlephZero ~lineage:None ~provenance:None - -(** Rational number domain: pairs [(numerator, denominator)] where the - denominator is never zero. The generator enumerates all such pairs via - Cantor pairing on the integers. Schema: - [numerator: integer, denominator: integer]. *) -let rational : Relation.domain = - let rec generator (position : int option) : Generator.result = - match position with - | Some n -> - let a, b = cantor_unpair n in - let num = nat_to_int a in - (* Map b -> non-zero integer: 0->1, 1->-1, 2->2, 3->-2, … *) - let den = if b mod 2 = 0 then (b / 2) + 1 else -((b + 1) / 2) in - let attributes = - Tuple.AttributeMap.of_list ["numerator", Obj.magic num; "denominator", Obj.magic den] - in - Generator.Value (Tuple.make_materialized ~relation:"rational" ~attributes, generator) - | None -> Generator.Error "Cannot produce a randomly enumerated value for the rational domain." - in - let membership_criteria : Tuple.t -> bool = function - | Tuple.Materialized m -> ( - match Tuple.AttributeMap.find_opt "denominator" m.attributes with - | Some attr -> (Obj.magic attr : int) <> 0 - | None -> false ) - | Tuple.NonMaterialized _ -> false - in - (* Note: Additionally to the membership criteria, we add the constraint here as this relation - can be further dismembered, rendering the denominator into a lone integer, that should - propagate the constraint `integer <> 0`. If we declared a domain `integer_without_zero`, - then this constraint would not be needed as the domain would not be dissociated from the value. *) - let constraints : Relation.RelationConstraint.t option = - let denominator_not_zero = - let open Constraint in - Not {body= Eq {left= Var "denominator"; right= Const (Obj.magic 0)}; universe= "integer"} - in - Some (("DENOMINATOR_DIFFERENT_FROM_ZERO", denominator_not_zero) |> List.singleton) - in - let schema = - Schema.empty |> Schema.add "numerator" "integer" |> Schema.add "denominator" "integer" - in - new Relation.domain - ~name:"rational" ~generator ~membership_criteria ~schema ~constraints - ~cardinality:Conventions.Cardinality.AlephZero ~lineage:None ~provenance:None - -(** String domain: any string value. Not enumerable. Schema: [value: string]. *) -let string : Relation.domain = - let generator (_ : int option) : Generator.result = - Generator.Error "Strings are not enumerable." - in - let membership_criteria : Tuple.t -> bool = function - | Tuple.Materialized _ -> true - | Tuple.NonMaterialized _ -> false - in - let schema = Schema.empty |> Schema.add "value" "string" in - new Relation.domain - ~name:"string" ~generator ~membership_criteria ~schema - ~constraints:None - (* TODO: Implement some form of enumeration for strings with a bijection on naturals. *) - ~cardinality:Conventions.Cardinality.Continuum ~lineage:None ~provenance:None |