Source file gospelstdlib.ml
1
let contents = "(**************************************************************************)\n(* *)\n(* GOSPEL -- A Specification Language for OCaml *)\n(* *)\n(* Copyright (c) 2018- The VOCaL Project *)\n(* *)\n(* This software is free software, distributed under the MIT license *)\n(* (as described in file LICENSE enclosed). *)\n(**************************************************************************)\n\n(* This file contains the GOSPEL standard library.\n It is automatically opened.\n\n The following are built-in in GOSPEL:\n\n type unit\n type string\n type char\n type float\n type bool\n type integer\n\n type 'a option\n function None: 'a option\n function Some (x: 'a) : 'a option\n\n type 'a list\n function ([]): 'a list\n function (::) (x: 'a) (l: 'a list) : 'a list\n\n predicate (=) (x y: 'a)\n*)\n\n(*@ type 'a seq *)\n(** The type for finite sequences. *)\n\n(*@ type 'a bag *)\n(** The type for finite unordered multisets. *)\n\n(*@ type 'a ref *)\n(** The type for references. *)\n\n(*@ type 'a array *)\n(** The type for arrays. *)\n\n(*@ type 'a set *)\n(** The type for finite unordered sets. *)\n\n(** {1 Arithmetic}\n\n The type [integer] is built-in. This is the type of arbitrary precision\n integers, not to be confused with OCaml's type [int] (machine, bounded\n integers). *)\n\n(*@ function succ (x: integer) : integer *)\n(*@ function pred (x: integer) : integer *)\n\n(*@ function (-_) (x: integer) : integer *)\n(*@ function (+) (x y: integer) : integer *)\n(*@ function (-) (x y: integer) : integer *)\n(*@ function ( * ) (x y: integer) : integer *)\n(*@ function (/) (x y: integer) : integer *)\n(*@ function mod (x y: integer) : integer *)\n\n(*@ function pow (x y: integer) : integer *)\n(*@ function abs (x:integer) : integer *)\n\n(*@ function min (x y : integer) : integer *)\n(*@ function max (x y : integer) : integer *)\n\n(** {2 Comparisons} *)\n\n(*@ predicate (>) (x y: integer) *)\n(*@ predicate (>=) (x y: integer) *)\n(*@ predicate (<) (x y: integer) *)\n(*@ predicate (<=) (x y: integer) *)\n\n(** {2 Bitwise operations} *)\n\n(*@ function logand (x y: integer) : integer *)\n(*@ function logor (x y: integer) : integer *)\n(*@ function logxor (x y: integer) : integer *)\n(*@ function lognot (x: integer) : integer *)\n\n(*@ function shift_left (x y: integer) : integer *)\n(** Shifts to the left, equivalent to a multiplication by a power of two *)\n\n(*@ function shift_right (x y: integer) : integer *)\n(** Shifts to the right, equivalent to a multiplication by a power of two with\n rounding toward -oo *)\n\n(*@ function shift_right_trunc (x y: integer) : integer *)\n(** Shift to the right with truncation, equivalent to a multiplication by a\n power of two with rounding toward 0 *)\n\n(** {2 Machine integers}\n\n There is a coercion from type [int] to type [integer], so that Gospel\n specifications can be written using type [integer] only, and yet use OCaml's\n variables of type [int]. The Gospel typechecker will automatically apply\n [integer_of_int] whenever necessary. *)\n\ntype int\n\n(*@ function integer_of_int (x: int) : integer *)\n(*@ coercion *)\n\n(*@ function max_int : integer *)\n(*@ function min_int : integer *)\n\n(** {1 Couples} *)\n\n(*@ function fst (p: 'a * 'b) : 'a *)\n(** [fst (x, y)] is [x]. *)\n\n(*@ function snd (p: 'a * 'b) : 'b *)\n(** [snd (x, y)] is [y]. *)\n\n(** {1 References} *)\n\n(*@ function (!_) (r: 'a ref) : 'a *)\n(** Reference content access operator. *)\n\n(*@ function ref (x: 'a) : 'a ref *)\n(** Reference creation. *)\n\n(** {1 Sequences} *)\n\n(*@ function (++) (s s': 'a seq) : 'a seq *)\n(** [s ++ s'] is the sequence [s] followed by the sequence [s']. *)\n\n(*@ function ([_]) (s: 'a seq) (i: integer): 'a *)\n(** [s\\[i\\]] is the [i]th element of the sequence [s]. *)\n\n(*@ function ([_.._]) (s: 'a seq) (i1: integer) (i2: integer): 'a seq *)\n(*@ function ([_..]) (s: 'a seq) (i: integer): 'a seq *)\n(*@ function ([.._]) (s: 'a seq) (i: integer): 'a seq *)\n\nmodule Seq : sig\n (*@ type 'a t = 'a seq *)\n (** An alias for {!'a seq} *)\n\n (*@ function length (s: 'a t): integer *)\n (** [length s] is the length of the sequence [s]. *)\n\n (*@ function empty : 'a t *)\n (** [empty] is the empty sequence. *)\n\n (*@ function singleton (x: 'a) : 'a t *)\n (** [singleton] is an alias for {!return}. *)\n\n (*@ function init (n: integer) (f: integer -> 'a) : 'a seq *)\n (** [init n f] is the sequence containing [f 0], [f 1], [...] , [f n]. *)\n\n (*@ function cons (x: 'a) (s: 'a t): 'a t *)\n (** [cons x s] is the sequence containing [x] followed by the elements of [s]. *)\n\n (*@ function snoc (s: 'a seq) (x: 'a): 'a seq *)\n (** [snoc s x] is the sequence containing the elements of [s] followed by [x]. *)\n\n (*@ function hd (s: 'a t) : 'a *)\n (** When [s] contains one or more elements, [hd s] is the first element of\n [s]. *)\n\n (*@ function tl (s: 'a t) : 'a t *)\n (** When [s] contains one or more elements, [tl s] is the sequence of the\n elements of [s], starting at position 2. *)\n\n (*@ function append (s s': 'a t) : 'a t *)\n (** [append s s'] is [s ++ s']. *)\n\n (*@ predicate mem (s: 'a seq) (x: 'a) *)\n (** [mem s x] holds iff [x] is in [s]. *)\n\n (*@ function map (f: 'a -> 'b) (s: 'a t) : 'b t *)\n (** [map f s] is a sequence whose elements are the elements of [s],\n transformed by [f]. *)\n\n (*@ function filter (f: 'a -> bool) (s: 'a t) : 'a t *)\n (** [filter f s] is a sequence whose elements are the elements of [s], that\n satisfy [f]. *)\n\n (*@ function filter_map (f: 'a -> 'b option) (s: 'a t) : 'b t *)\n (** [filter_map f s] is a sequence whose elements are the elements of [s],\n transformed by [f]. An element [x] is dropped whenever [f x] is [None]. *)\n\n (*@ function get (s: 'a t) (i: integer) : 'a *)\n (** [get s i] is [s\\[i\\]]. *)\n\n (*@ function set (s: 'a t) (i: integer) (x: 'a): 'a t *)\n (** [set s i x] is the sequence [s] where the [i]th element is [x]. *)\n\n (*@ function rev (s: 'a seq) : 'a seq *)\n (** [rev s] is the sequence containing the same elements as [s], in reverse\n order. *)\n\n (*@ function rec fold_left (f: 'a -> 'b -> 'a) (acc: 'a) (s: 'b seq) : 'a *)\n (** [fold_left f acc s] is [f (... (f (f acc s\\[0\\]) s\\[1\\]) ...) s\\[n-1\\]],\n where [n] is the length of [s]. *)\n\n (*@ function rec fold_right (f: 'a -> 'b -> 'b) (s: 'a seq) (acc: 'b) : 'b *)\n (** [fold_right f s acc] is [f s\\[1\\] (f s\\[2\\] (... (f s\\[n\\] acc) ...))]\n where [n] is the length of [s]. *)\nend\n\n(** Lists\n\n The type ['a list] and the constructors [\\[\\]] and [(::)] are built-in. *)\n\nmodule List : sig\n (*@ type 'a t = 'a list *)\n (** An alias for ['a list]. *)\n\n (*@ function length (l: 'a t) : integer *)\n (** [length l] is the number of elements of [l]. *)\n\n (*@ function hd (l: 'a t) : 'a *)\n (** When [l] contains one or more elements, [hd s] is the first element of\n [l]. *)\n\n (*@ function tl (l: 'a t) : 'a t *)\n (** When [l] contains one or more elements, [tl l] is the list of the elements\n of [l], starting at position 2. *)\n\n (*@ function nth (l: 'a t) (i: integer) : 'a *)\n (** [nth l i] is the [i]th element of [l]. *)\n\n (*@ function nth_opt (l: 'a t) (i: integer) : 'a option *)\n (** [nth l i] is the [i]th element of [l] if [i] is within the bounds of [l],\n and [None] otherwise. *)\n\n (*@ function rev (l: 'a t) : 'a t *)\n (** [rev l] contains the same elements as [l] in a reverse order. *)\n\n (*@ function init (n: integer) (f: integer -> 'a) : 'a t *)\n (** [init n f] is a list of length [n], with element number [i] initialized\n with [f i]. *)\n\n (*@ function map (f: 'a -> 'b) (l: 'a t) : 'b t *)\n (** [map f l] applies function [f] to all the elements of [l], and builds a\n list with the results returned by [f] *)\n\n (*@ function mapi (f: integer -> 'a -> 'b) (l: 'a t) : 'b t *)\n (** Same as {!map}, but the function is applied to the index of the element as\n first argument, and the element itself as second argument. *)\n\n (*@ function fold_left (f: 'a -> 'b -> 'a) (init: 'a) (l: 'b t) : 'a *)\n (** [fold_left f init t] is [f (... (f (f init a\\[0\\]) a\\[1\\]) ...) a\\[n-1\\]],\n where [n] is the length of [t]. *)\n\n (*@ function fold_right (f: 'b -> 'a -> 'a) (l: 'b t) (init: 'a) : 'a *)\n (** [fold_right f t init] is\n [f a\\[0\\] (f a\\[1\\] ( ... (f a\\[n-1\\] init) ...))], where [n] is the\n length of [t]. *)\n\n (*@ function map2 (f: 'a -> 'b -> 'c) (l: 'a t) (l': 'b t) : 'c t *)\n (** [map2 f l l'] applies function [f] to all the elements of [l] and [l'],\n and builds a list with the results returned by [f]. *)\n\n (*@ predicate for_all (f: 'a -> bool) (l: 'a t) *)\n (** [for_all f l] holds iff all elements of [l] satisfy the predicate [f]. *)\n\n (*@ predicate _exists (f: 'a -> bool) (l: 'a t) *)\n (** [_exists f l] holds iff at least one element of [l] satisfies [f]. *)\n\n (*@ predicate for_all2 (f: 'a -> 'b -> bool) (l: 'a t) (l': 'b t) *)\n (** Same as {!for_all}, but for a two-argument predicate. *)\n\n (*@ predicate _exists2 (f: 'a -> 'b -> bool) (l: 'a t) (l': 'b t) *)\n (** Same as {!_exists}, but for a two-argument predicate. *)\n\n (*@ predicate mem (x: 'a) (l: 'a t) *)\n (** [mem x l] holds iff [x] is equal to an element of [l] *)\n\n (*@ function to_seq (s: 'a t) : 'a Seq.t *)\n (*@ coercion *)\n\n (*@ function of_seq (s: 'a Seq.t) : 'a t *)\nend\n\n(** {1 Arrays} *)\n\nmodule Array : sig\n (*@ type 'a t = 'a array *)\n (** An alias for the type of arrays. *)\n\n (*@ function length (a: 'a t) : integer *)\n (** [length a] is the number of elements of [a]. *)\n\n (*@ function get (a: 'a t) (i: integer) : 'a *)\n (** [get a i] is the element number [i] of array [a]. *)\n\n (*@ function make (n: integer) (x: 'a) : 'a t *)\n (** [make n x] is an array of length [n], initialized with [x]. *)\n\n (*@ function init (n: integer) (f: integer -> 'a) : 'a t *)\n (** [init n f] is an array of length [n], with element number [i] initialized\n to the result of [f i]. *)\n\n (*@ function append (a b: 'a t) : 'a t *)\n (** [append v1 v2] returns an array containing the concatenation of [v1] and\n [v2]. *)\n\n (*@ function concat (a: 'a t list) : 'a t *)\n (** Same as {!append}, but concatenates a list of arrays. *)\n\n (*@ function sub (a: 'a t) (i len: integer) : 'a t *)\n (** [sub a pos len] is the array of length [len], containing the elements\n number [pos] to [pos + len - 1] of array [a]. *)\n\n (*@ function map (f: 'a -> 'b) (a: 'a t) : 'b t *)\n (** [map f a] applies function [f] to all the elements of [a], and builds an\n array with the results returned by [f] *)\n\n (*@ function mapi (f: integer -> 'a -> 'b) (a: 'a t) : 'b t *)\n (** Same as {!map}, but the function is applied to the index of the element as\n first argument, and the element itself as second argument. *)\n\n (*@ function fold_left (f: 'a -> 'b -> 'a) (init: 'a) (a: 'b t) : 'a *)\n (** [fold_left f init a] is [f (... (f (f init a\\[0\\]) a\\[1\\]) ...) a\\[n-1\\]],\n where [n] is the length of [a]. *)\n\n (*@ function fold_right (f: 'b -> 'a -> 'a) (a: 'b t) (init: 'a) : 'a *)\n (** [fold_right f a init] is\n [f a\\[0\\] (f a\\[1\\] ( ... (f a\\[n-1\\] init) ...))], where [n] is the\n length of [a]. *)\n\n (*@ function map2 (f: 'a -> 'b -> 'c) (a: 'a t) (b: 'b t) : 'c t *)\n (** [map2 f a b] applies function [f] to all the elements of [a] and [b], and\n builds an array with the results returned by [f]. *)\n\n (*@ predicate for_all (f: 'a -> bool) (a: 'a t) *)\n (** [for_all f a] holds iff all elements of [a] satisfy the predicate [f]. *)\n\n (*@ predicate _exists (f: 'a -> bool) (a: 'a t) *)\n (** [_exists f a] holds iff at least one element of [a] satisfies [f]. *)\n\n (*@ predicate for_all2 (f: 'a -> 'b -> bool) (a: 'a t) (b: 'b t) *)\n (** Same as {!for_all}, but for a two-argument predicate. *)\n\n (*@ predicate _exists2 (f: 'a -> 'b -> bool) (a: 'a t) (b: 'b t) *)\n (** Same as {!_exists}, but for a two-argument predicate. *)\n\n (*@ predicate mem (x: 'a) (a: 'a t) *)\n (** [mem x a] holds iff [x] is equal to an element of [a] *)\n\n (*@ function to_list (a: 'a t) : 'a list *)\n (*@ function of_list (l: 'a list) : 'a t *)\n\n (*@ function to_seq (a: 'a t) : 'a Seq.t *)\n (*@ coercion *)\n (*@ function of_seq (s: 'a Seq.t) : 'a t *)\n\n (*@ function to_bag (a: 'a t) : 'a bag *)\n\n (*@ predicate permut (a b: 'a array) *)\n (** [permut a b] is true iff [a] and [b] contain the same elements with the\n same number of occurrences *)\n\n (*@ predicate permut_sub (a b: 'a array) (lo hi: integer) *)\n (** [permut_sub a b lo hi] is true iff the segment `a1.(lo..hi-1)` is a\n permutation of the segment `a2.(lo..hi-1)` and values outside of the\n interval are equal. *)\nend\n\n(** {1 Bags} *)\n\nmodule Bag : sig\n (*@ type 'a t = 'a bag *)\n (** An alias for ['a bag]. *)\n\n (*@ function occurrences (x: 'a) (b: 'a t): integer *)\n (** [occurrences x b] is the number of occurrences of [x] in [s]. *)\n\n (*@ function compare (b b': 'a t) : int *)\n (** A comparison function over bags. *)\n\n (*@ function empty : 'a t *)\n (** [empty] is the empty bag. *)\n\n (*@ predicate is_empty (b: 'a t) *)\n (** [is_empty b] is [b = empty]. *)\n\n (*@ predicate mem (x: 'a) (b: 'a t) *)\n (** [mem x b] holds iff [b] contains [x] at least once. *)\n\n (*@ function add (x: 'a) (b: 'a t) : 'a t *)\n (** [add x b] is [b] when an occurence of [x] was added. *)\n\n (*@ function singleton (x: 'a) : 'a t *)\n (** [singleton x] is a bag containing one occurence of [x]. *)\n\n (*@ function remove (x: 'a) (b: 'a t) : 'a t *)\n (** [remove x b] is [b] where an occurence of [x] was removed. *)\n\n (*@ function union (b b': 'a t) : 'a t *)\n (** [union b b'] is a bag [br] where for all element [x],\n [occurences x br = max\n (occurences x b) (occurences x b')]. *)\n\n (*@ function sum (b b': 'a t) : 'a t *)\n (** [sum b b'] is a bag [br] where for all element [x],\n [occurences x br =\n (occurences x b) + (occurences x b')]. *)\n\n (*@ function inter (b b': 'a t) : 'a t *)\n (** [inter b b'] is a bag [br] where for all element [x],\n [occurences x br =\n min (occurences x b) (occurences x b')]. *)\n\n (*@ predicate disjoint (b b': 'a t) *)\n (** [disjoint b b'] holds iff [b] and [b'] have no element in common. *)\n\n (*@ function diff (b b': 'a t) : 'a t *)\n (** [diff b b'] is a bag [br] where for all element [x],\n [occurences x br =\n max 0 (occurences x b - occurences x b')]. *)\n\n (*@ predicate subset (b b': 'a t) *)\n (** [subset b b'] holds iff for all element [x],\n [occurences x b <= occurences x b']. *)\n\n (*@ function choose (b: 'a t) : 'a *)\n (** [choose b] is an arbitrary element of [b]. *)\n\n (*@ function choose_opt (b: 'a t) : 'a option *)\n (** [choose_opt b] is an arbitrary element of [b] or [None] if [b] is empty. *)\n\n (*@ function map (f: 'a -> 'b) (b: 'a t) : 'b t *)\n (** [map f b] is a fresh bag which elements are [f x1 ... f xN], where\n [x1 ... xN] are the elements of [b]. *)\n\n (*@ function fold (f: 'a -> 'b -> 'b) (b: 'a t) (a: 'b) : 'b *)\n (** [fold f b a] is [(f xN ... (f x2 (f x1 a))...)], where [x1 ... xN] are the\n elements of [b]. *)\n\n (*@ predicate for_all (f: 'a -> bool) (b: 'a t) *)\n (** [for_all f b] holds iff [f x] is [true] for all elements in [b]. *)\n\n (*@ predicate _exists (f: 'a -> bool) (b: 'a t) *)\n (** [for_all f b] holds iff [f x] is [true] for at least one element in [b]. *)\n\n (*@ function filter (f: 'a -> bool) (b: 'a t) : 'a t *)\n (** [filter f b] is the bag of all elements in [b] that satisfy [f]. *)\n\n (*@ function filter_map (f: 'a -> 'a option) (b: 'a t) : 'a t *)\n (** [filter_map f b] is the bag of all [v] such that [f x = Some v] for some\n element [x] of [b]. *)\n\n (*@ function partition (f: 'a -> bool) (b: 'a t) : ('a t * 'a t) *)\n (** [partition f b] is the pair of bags [(b1, b2)], where [b1] is the bag of\n all the elements of [b] that satisfy [f], and [b2] is the bag of all the\n elements of [b] that do not satisfy [f]. *)\n\n (*@ function cardinal (b: 'a t) : int *)\n (** [cardinal b] is the number of distinct elements in [b]. *)\n\n (*@ function elements (b: 'a t) : 'a list *)\n (** [elements b] is the list of all elements in [b]. *)\n\n (*@ function to_list (b: 'a t) : 'a list *)\n (*@ function of_list (l: 'a list) : 'a t *)\n\n (*@ function to_seq (b: 'a t) : 'a Seq.t *)\n (*@ function of_seq (s: 'a Seq.t) : 'a t *)\n\n (*@ function of_array (a: 'a array) : 'a t *)\nend\n\n(** {1 Sets} *)\n\n(*@ function ({}) : 'a set *)\n(** [\\{\\}] is the empty set. *)\n\nmodule Set : sig\n (*@ type 'a t = 'a set *)\n (** An alias for ['a set]. *)\n\n (*@ function compare (s s': 'a t) : int *)\n (** A comparison function over sets. *)\n\n (*@ function empty : 'a t *)\n (** [empty] is [\226\136\133]. *)\n\n (*@ predicate is_empty (s: 'a t) *)\n (** [is_empty s] is [s = \226\136\133]. *)\n\n (*@ predicate mem (x: 'a) (s: 'a t) *)\n (** [mem x s] is [x \226\136\136 s]. *)\n\n (*@ function add (x: 'a) (s: 'a t) : 'a t *)\n (** [add x s] is [s \226\136\170 {x}]. *)\n\n (*@ function singleton (x: 'a) : 'a t *)\n (** [singleton x] is [{x}]. *)\n\n (*@ function remove (x: 'a) (s: 'a t) : 'a t *)\n (** [remove x s] is [s \226\136\150 {x}]. *)\n\n (*@ function union (s s': 'a t) : 'a t *)\n (** [union s s'] is [s \226\136\170 s']. *)\n\n (*@ function inter (s s': 'a t) : 'a t *)\n (** [inter s s'] is [s \226\136\169 s']. *)\n\n (*@ predicate disjoint (s s': 'a t) *)\n (** [disjoint s s'] is [s \226\136\169 s' = \226\136\133]. *)\n\n (*@ function diff (s s': 'a t) : 'a t *)\n (** [diff s s'] is [s \226\136\150 s']. *)\n\n (*@ predicate subset (s s': 'a t) *)\n (** [subset s s'] is [s \226\138\130 s']. *)\n\n (*@ function cardinal (s: 'a t) : integer *)\n (** [cardinal s] is the number of elements in [s]. *)\n\n (*@ function choose (s: 'a t) : integer *)\n (** [choose s] is an arbitrary element of [s]. *)\n\n (*@ function choose_opt: 'a t -> 'a option *)\n (** [choose_opt s] is an arbitrary element of [s] or [None] if [s] is empty. *)\n\n (*@ function map (f: 'a -> 'b) (s: 'a t) : 'b t *)\n (** [map f s] is a fresh set which elements are [f x1 ... f xN], where\n [x1 ...\n xN] are the elements of [s]. *)\n\n (*@ function fold (f: 'a -> 'b -> 'b) (s: 'a t) (a: 'b) : 'b *)\n (** [fold f s a] is [(f xN ... (f x2 (f x1 a))...)], where [x1 ... xN] are the\n elements of [s]. *)\n\n (*@ predicate for_all (f: 'a -> bool) (s: 'a t) *)\n (** [for_all f s] holds iff [f x] is [true] for all elements in [s]. *)\n\n (*@ predicate _exists (f: 'a -> bool) (s: 'a t) *)\n (** [_exists f s] holds iff [f x] is [true] for at least one element in [s]. *)\n\n (*@ function filter (f: 'a -> bool) (s: 'a t) : 'a t *)\n (** [filter f s] is the set of all elements in [s] that satisfy [f]. *)\n\n (*@ function filter_map (f: 'a -> 'a option) (s: 'a t) : 'a t *)\n (** [filter_map f s] is the set of all [v] such that [f x = Some v] for some\n element [x] of [s]. *)\n\n (*@ function partition (f: 'a -> bool) (s: 'a t) : ('a t * 'a t) *)\n (** [partition f s] is the pair of sets [(s1, s2)], where [s1] is the set of\n all the elements of [s] that satisfy the predicate [f], and [s2] is the\n set of all the elements of [s] that do not satisfy [f]. *)\n\n (*@ function elements (s: 'a t) : 'a list *)\n (** [elements s] is the list of all elements in [s]. *)\n\n (*@ function to_list (s: 'a t) : 'a list *)\n (*@ function of_list (l: 'a list) : 'a t *)\n\n (*@ function to_seq (s: 'a t) : 'a Seq.t *)\n (*@ function of_seq (s: 'a Seq.t) : 'a t *)\nend\n\n(*@ function ( [->] ) (f: 'a -> 'b) (x:'a) (y: 'b) : 'a -> 'b *)\n\nmodule Map : sig\n (* the type ('a, 'b) map is defined internally in GOSPEL and can be\n written as 'a -> 'b *)\nend\n\nmodule Order : sig\n (*@ predicate is_pre_order (cmp: 'a -> 'a -> int) =\n (forall x. cmp x x = 0) /\\\n (forall x y. cmp x y <= 0 <-> cmp y x >= 0) /\\\n (forall x y z.\n (cmp x y <= 0 -> cmp y z <= 0 -> cmp x z <= 0) /\\\n (cmp x y <= 0 -> cmp y z < 0 -> cmp x z < 0) /\\\n (cmp x y < 0 -> cmp y z <= 0 -> cmp x z < 0) /\\\n (cmp x y < 0 -> cmp y z < 0 -> cmp x z < 0)) *)\nend\n\n(** Other OCaml built-in stuff *)\n\nexception Not_found\nexception Invalid_argument of string\n\nmodule Sys : sig\n (*@ function word_size : integer *)\n\n (*@ function int_size : integer *)\n\n (*@ function big_endian : bool *)\n\n (*@ function max_string_length : integer *)\n\n (*@ function max_array_length : integer *)\nend\n"