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