blob: a87f9c84b69fcb1fae7fe27b4cd0e48657b752de (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
|
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"
|
