cardinality concept for relations

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