summaryrefslogtreecommitdiff
path: root/search_monad.mli
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@google.com>2019-02-13 20:40:51 -0500
committerGravatar Benjamin Barenblat <bbaren@google.com>2019-02-13 20:40:51 -0500
commit8018e923c75eb5504310864f821972f794b7d554 (patch)
tree88a55f7c23fcbbea0ff80e406555292049b48dec /search_monad.mli
parent76f9b4cdc5693a6313961e2f91b39ba311857e72 (diff)
New upstream version 8.8.0+1.gbp069dc3bupstream/8.8.0+1.gbp069dc3bupstream
Diffstat (limited to 'search_monad.mli')
-rw-r--r--search_monad.mli42
1 files changed, 0 insertions, 42 deletions
diff --git a/search_monad.mli b/search_monad.mli
deleted file mode 100644
index 7e2a910..0000000
--- a/search_monad.mli
+++ /dev/null
@@ -1,42 +0,0 @@
-(***************************************************************************)
-(* 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