summaryrefslogtreecommitdiff
path: root/AAC_search_monad.mli
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-12-01 13:33:59 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2010-12-01 13:33:59 +0100
commitaa51449cb692a9a1d183b2663679645aba16b036 (patch)
treef32b2fd38d3442e4d583009cb09cbac701c33bc0 /AAC_search_monad.mli
parenta3c2b799e0eceb0896af062887c762c654d2e2f6 (diff)
parent8ab748064ddeec8400859e210bf9963826cba631 (diff)
Merge commit 'upstream/0.2.1'
Diffstat (limited to 'AAC_search_monad.mli')
-rw-r--r--AAC_search_monad.mli41
1 files changed, 41 insertions, 0 deletions
diff --git a/AAC_search_monad.mli b/AAC_search_monad.mli
new file mode 100644
index 0000000..093f9d9
--- /dev/null
+++ b/AAC_search_monad.mli
@@ -0,0 +1,41 @@
+(***************************************************************************)
+(* 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