CompletedNatWitness.mli 1.99 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13
(******************************************************************************)
(*                                                                            *)
(*                                   Menhir                                   *)
(*                                                                            *)
(*                       François Pottier, Inria Paris                        *)
(*              Yann Régis-Gianas, PPS, Université Paris Diderot              *)
(*                                                                            *)
(*  Copyright Inria. All rights reserved. This file is distributed under the  *)
(*  terms of the GNU General Public License version 2, as described in the    *)
(*  file LICENSE.                                                             *)
(*                                                                            *)
(******************************************************************************)

14 15
(* This is the lattice of the natural numbers, completed with [Infinity], and
   ordered towards zero (i.e. [Infinity] is [bottom], [Finite 0] is [top]). *)
16

17 18 19 20 21 22
(* These numbers are further enriched with sequences of matching length. Thus,
   a lattice element is either [Finite (n, xs)], where [n] is a natural number
   and [xs] is a sequence of length [n]; or [Infinity]. The sequences [xs] are
   ignored by the ordering (e.g., [compare] ignores them) but are nevertheless
   constructed (e.g., [add] concatenates two sequences). They should be thought
   of as witnesses, or proofs, that explain why the number [n] was obtained. *)
23 24

type 'a t =
25
| Finite of int * 'a Seq.seq
26 27 28 29 30 31
| Infinity

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

POTTIER Francois's avatar
POTTIER Francois committed
32 33 34
val epsilon: 'a t
val singleton: 'a -> 'a t

35 36 37
val min: 'a t -> 'a t -> 'a t
val add: 'a t -> 'a t -> 'a t

38 39
val min_lazy: 'a t -> (unit -> 'a t) -> 'a t
val add_lazy: 'a t -> (unit -> 'a t) -> 'a t
40 41

val print: ('a -> string) -> 'a t -> string
42
val to_int: 'a t -> int
43
val extract: 'a t -> 'a list