CompletedNatWitness.mli 1.99 KB
 POTTIER Francois committed Mar 24, 2017 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. *) (* *) (******************************************************************************) `````` POTTIER Francois committed Sep 18, 2018 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]). *) `````` POTTIER Francois committed Jul 02, 2015 16 `````` `````` POTTIER Francois committed Sep 18, 2018 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. *) `````` POTTIER Francois committed Jul 02, 2015 23 24 `````` type 'a t = `````` POTTIER Francois committed Jul 03, 2015 25 ``````| Finite of int * 'a Seq.seq `````` POTTIER Francois committed Jul 02, 2015 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 committed Jul 02, 2015 32 33 34 ``````val epsilon: 'a t val singleton: 'a -> 'a t `````` POTTIER Francois committed Jul 02, 2015 35 36 37 ``````val min: 'a t -> 'a t -> 'a t val add: 'a t -> 'a t -> 'a t `````` POTTIER Francois committed Jul 03, 2015 38 39 ``````val min_lazy: 'a t -> (unit -> 'a t) -> 'a t val add_lazy: 'a t -> (unit -> 'a t) -> 'a t `````` POTTIER Francois committed Jul 02, 2015 40 41 `````` val print: ('a -> string) -> 'a t -> string `````` POTTIER Francois committed Jul 03, 2015 42 ``````val to_int: 'a t -> int `````` POTTIER Francois committed Jul 07, 2015 43 ``val extract: 'a t -> 'a list``