diff options
| -rw-r--r-- | lib/concepts/Cardinality.ml | 27 | ||||
| -rw-r--r-- | lib/concepts/Cardinality.mli | 14 |
2 files changed, 41 insertions, 0 deletions
diff --git a/lib/concepts/Cardinality.ml b/lib/concepts/Cardinality.ml new file mode 100644 index 0000000..ac80a15 --- /dev/null +++ b/lib/concepts/Cardinality.ml @@ -0,0 +1,27 @@ +type t = Empty | Bounded of int | Finite | Countable + +let bounded n = if n <= 0 then Empty else Bounded n +let rank = function Empty -> 0 | Bounded _ -> 1 | Finite -> 2 | Countable -> 3 + +let compare a b = + match (a, b) with + | Bounded n, Bounded m -> Utilities.Ordering.of_int (Int.compare n m) + | _ -> Utilities.Ordering.of_int (Int.compare (rank a) (rank b)) + +let equal a b = compare a b = Utilities.Ordering.Equal +let leq a b = compare a b <> Utilities.Ordering.Greater +let join a b = if leq a b then b else a +let meet a b = if leq a b then a else b +let product a b = + match (a, b) with + | Empty, _ | _, Empty -> Empty + | Countable, _ | _, Countable -> Countable + | Finite, _ | _, Finite -> Finite + | Bounded n, Bounded m -> if n > max_int / m then Finite else bounded (n * m) + +let exhaustible = function Countable -> false | Empty | Bounded _ | Finite -> true +let to_string = function + | Empty -> "empty" + | Bounded n -> Printf.sprintf "bounded(%d)" n + | Finite -> "finite" + | Countable -> "countable" diff --git a/lib/concepts/Cardinality.mli b/lib/concepts/Cardinality.mli new file mode 100644 index 0000000..e4df62b --- /dev/null +++ b/lib/concepts/Cardinality.mli @@ -0,0 +1,14 @@ +type t = Empty | Bounded of int | Finite | Countable + +val bounded : int -> t +val compare : t -> t -> Utilities.Ordering.t +val equal : t -> t -> bool +val leq : t -> t -> bool +val join : t -> t -> t +val meet : t -> t -> t +(** the class of a generator run under every binding produced by + another, which is how the classes of the generators chosen by an + analysis combine. *) +val product : t -> t -> t +val exhaustible : t -> bool +val to_string : t -> string |