diff options
Diffstat (limited to 'clib')
-rw-r--r-- | clib/clib.mllib | 1 | ||||
-rw-r--r-- | clib/orderedType.ml | 35 | ||||
-rw-r--r-- | clib/orderedType.mli | 19 |
3 files changed, 55 insertions, 0 deletions
diff --git a/clib/clib.mllib b/clib/clib.mllib index 0b5d9826f..c9b4d72fc 100644 --- a/clib/clib.mllib +++ b/clib/clib.mllib @@ -5,6 +5,7 @@ CEphemeron Hashset Hashcons +OrderedType CSet CMap CList diff --git a/clib/orderedType.ml b/clib/orderedType.ml new file mode 100644 index 000000000..922eb76ab --- /dev/null +++ b/clib/orderedType.ml @@ -0,0 +1,35 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +module type S = +sig + type t + val compare : t -> t -> int +end + +module Pair (M:S) (N:S) = struct + type t = M.t * N.t + + let compare (a,b) (a',b') = + let i = M.compare a a' in + if Int.equal i 0 then N.compare b b' + else i +end + +module UnorderedPair (M:S) = struct + type t = M.t * M.t + + let reorder (a,b as p) = + if M.compare a b <= 0 then p else (b,a) + + let compare p p' = + let p = reorder p and p' = reorder p' in + let module P = Pair(M)(M) in P.compare p p' +end diff --git a/clib/orderedType.mli b/clib/orderedType.mli new file mode 100644 index 000000000..3578ea0d8 --- /dev/null +++ b/clib/orderedType.mli @@ -0,0 +1,19 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +module type S = +sig + type t + val compare : t -> t -> int +end + +module Pair (M:S) (N:S) : S with type t = M.t * N.t + +module UnorderedPair (M:S) : S with type t = M.t * M.t |