diff options
author | Stephane Glondu <steph@glondu.net> | 2012-09-20 09:41:14 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-09-20 09:41:14 +0200 |
commit | 7ebd874126a513c29a8b10e7e6ea2c7e745ab33c (patch) | |
tree | dd3c16609149d401052607cc734538cec1fc913e /search_monad.mli | |
parent | 967ef647c79fa0409671b819a1ab5477419eb762 (diff) | |
parent | 8917ab003a9b7f2abf8e399b5e7ad013b31a2e0e (diff) |
Merge tag 'upstream/0.3'
Upstream version 0.3
Diffstat (limited to 'search_monad.mli')
-rw-r--r-- | search_monad.mli | 42 |
1 files changed, 42 insertions, 0 deletions
diff --git a/search_monad.mli b/search_monad.mli new file mode 100644 index 0000000..7e2a910 --- /dev/null +++ b/search_monad.mli @@ -0,0 +1,42 @@ +(***************************************************************************) +(* This is part of aac_tactics, it is distributed under the terms of the *) +(* GNU Lesser General Public License version 3 *) +(* (see file LICENSE for more details) *) +(* *) +(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) +(***************************************************************************) + +(** Search monad that allows to express non-deterministic algorithms + in a legible maner, or programs that solve combinatorial problems. + + @see <http://spivey.oriel.ox.ac.uk/mike/search-jfp.pdf> the + inspiration of this module +*) + +(** A data type that represent a collection of ['a] *) +type 'a m + + (** {2 Monadic operations} *) + +(** bind and return *) +val ( >> ) : 'a m -> ('a -> 'b m) -> 'b m +val return : 'a -> 'a m + +(** non-deterministic choice *) +val ( >>| ) : 'a m -> 'a m -> 'a m + +(** failure *) +val fail : unit -> 'a m + +(** folding through the collection *) +val fold : ('a -> 'b -> 'b) -> 'a m -> 'b -> 'b + +(** {2 Derived facilities } *) + +val sprint : ('a -> string) -> 'a m -> string +val count : 'a m -> int +val choose : 'a m -> 'a option +val to_list : 'a m -> 'a list +val sort : ('a -> 'a -> int) -> 'a m -> 'a m +val is_empty: 'a m -> bool +val filter : ('a -> bool) -> 'a m -> 'a m |