diff options
Diffstat (limited to 'lib/option.ml')
-rw-r--r-- | lib/option.ml | 50 |
1 files changed, 34 insertions, 16 deletions
diff --git a/lib/option.ml b/lib/option.ml index d6df7063..9ea1a769 100644 --- a/lib/option.ml +++ b/lib/option.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -19,6 +19,26 @@ let has_some = function | None -> false | _ -> true +let is_empty = function +| None -> true +| Some _ -> false + +(** Lifting equality onto option types. *) +let equal f x y = match x, y with +| None, None -> true +| Some x, Some y -> f x y +| _, _ -> false + +let compare f x y = match x, y with +| None, None -> 0 +| Some x, Some y -> f x y +| None, Some _ -> -1 +| Some _, None -> 1 + +let hash f = function +| None -> 0 +| Some x -> f x + exception IsNone (** [get x] returns [y] where [x] is [Some y]. It raises IsNone @@ -44,6 +64,14 @@ let flatten = function | _ -> None +(** [append x y] is the first element of the concatenation of [x] and + [y] seen as lists. *) +let append o1 o2 = + match o1 with + | Some _ -> o1 + | None -> o2 + + (** {6 "Iterators"} ***) (** [iter f x] executes [f y] if [x] equals [Some y]. It does nothing @@ -153,21 +181,11 @@ module List = let rec flatten = function | x::l -> cons x (flatten l) | [] -> [] -end - + let rec find f = function + |[] -> None + |h :: t -> match f h with + |None -> find f t + |x -> x -(** {6 Miscelaneous Primitives} *) - -module Misc = - struct - (** [Misc.compare f x y] lifts the equality predicate [f] to - option types. That is, if both [x] and [y] are [None] then - it returns [true], if they are bothe [Some _] then - [f] is called. Otherwise it returns [false]. *) - let compare f x y = - match x,y with - | None, None -> true - | Some z, Some w -> f z w - | _,_ -> false end |