diff options
| author | msozeau | 2008-10-23 16:22:18 +0000 |
|---|---|---|
| committer | msozeau | 2008-10-23 16:22:18 +0000 |
| commit | 0b840f7aaece0c209850adb2a81904b54f410091 (patch) | |
| tree | 442e51c4aeea80184f77667f7abbd5a8d04e54b5 /lib | |
| parent | 57cb1648fcf7da18d74c28a4d63d59ea129ab136 (diff) | |
Open notation for declaring record instances.
It solves feature request 1852, makes me and Arnaud happy and
will permit to factor some more code in typeclasses.
- Records are introduced using the syntax "{| x := t; y := foo |}" and
"with" clauses are currently parsed but not yet supported in the
elaboration. You are invited to suggest other syntaxes :)
- Missing fields are turned into holes, extra fields cause an error
message. The current implementation finds the type of the record
at pretyping time, from the typing constraint alone (and just expects
an inductive with one constructor). It is then impossible to use
scope information to parse the bodies: that may be wrong. The other
solution I see is using the fields to detect the type earlier, before
internalisation of the bodies, but then we get in name clash hell.
- In funind/contrib/interface I mostly put [assert false] everywhere to
avoid warnings.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11496 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/option.ml | 6 | ||||
| -rw-r--r-- | lib/option.mli | 2 |
2 files changed, 7 insertions, 1 deletions
diff --git a/lib/option.ml b/lib/option.ml index 543c108ab9..3d98034256 100644 --- a/lib/option.ml +++ b/lib/option.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id:$ i*) +(*i $Id$ i*) (** Module implementing basic combinators for OCaml option type. It tries follow closely the style of OCaml standard library. @@ -97,6 +97,10 @@ let fold_right f x a = | Some y -> f y a | _ -> a +(** [cata f a x] is [a] if [x] is [None] and [f y] if [x] is [Some y]. *) +let cata f a = function + | Some c -> f c + | None -> a (** {6 More Specific operations} ***) diff --git a/lib/option.mli b/lib/option.mli index c1260d9acf..04f3ca37d0 100644 --- a/lib/option.mli +++ b/lib/option.mli @@ -66,6 +66,8 @@ val fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b option -> 'c option -> 'a (** [fold_right f x a] is [f y a] if [x] is [Some y], and [a] otherwise. *) val fold_right : ('a -> 'b -> 'b) -> 'a option -> 'b -> 'b +(** [cata e f x] is [e] if [x] is [None] and [f a] if [x] is [Some a] *) +val cata : ('a -> 'b) -> 'b -> 'a option -> 'b (** {6 More Specific Operations} ***) |