CompletedNatWitness.mli 837 Bytes
Newer Older
1
(* This is an enriched version of [CompletedNat], where we compute not just
2
   numbers, but also sequences of matching length. *)
3 4

(* A property is either [Finite (n, xs)], where [n] is a natural number and
5
   [xs] is a sequence of length [n]; or [Infinity]. *)
6 7

type 'a t =
8
| Finite of int * 'a Seq.seq
9 10 11 12 13 14
| Infinity

val bottom: 'a t
val equal: 'a t -> 'b t -> bool
val is_maximal: 'a t -> bool

15 16
val compare: 'a t -> 'b t -> int

POTTIER Francois's avatar
POTTIER Francois committed
17 18 19
val epsilon: 'a t
val singleton: 'a -> 'a t

20 21 22
val min: 'a t -> 'a t -> 'a t
val add: 'a t -> 'a t -> 'a t

23 24
val min_lazy: 'a t -> (unit -> 'a t) -> 'a t
val add_lazy: 'a t -> (unit -> 'a t) -> 'a t
25

POTTIER Francois's avatar
POTTIER Francois committed
26
val min_cutoff: 'a t -> (int -> 'a t) -> 'a t
POTTIER Francois's avatar
POTTIER Francois committed
27
val add_cutoff: (* cutoff: *) int -> 'a t -> (int -> 'a t) -> 'a t
POTTIER Francois's avatar
POTTIER Francois committed
28

29
val print: ('a -> string) -> 'a t -> string
30
val to_int: 'a t -> int
31
val extract: 'a t -> 'a list