(******************************************************************************)
(*                                                                            *)
(*                                   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.                                                             *)
(*                                                                            *)
(******************************************************************************)

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

(* 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. *)

type 'a t =
| Finite of int * 'a Sequence.seq
| Infinity

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

val epsilon: 'a t
val singleton: 'a -> 'a t

val min: 'a t -> 'a t -> 'a t
val add: 'a t -> 'a t -> 'a t

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

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