Adding a Ftactic module for potentially focussing tactics.

The code for the module was moved from Tacinterp. We still expose partially
the implementation of the Ftactic.t type, for the sake of simplicity. It may
be dangerous if used improperly though.

2 files changed, 35 insertions, 24 deletions

diff --git a/lib/monad.ml b/lib/monad.ml
index 7636b1630c..d4641194ee 100644
--- a/lib/monad.ml
+++ b/lib/monad.ml
@@ -24,6 +24,13 @@ module type Def = sig
 
 end
 
+module type ListS = sig
+  type 'a t
+  val map : ('a -> 'b t) -> 'a list -> 'b list t
+  val map_right : ('a -> 'b t) -> 'a list -> 'b list t
+  val fold_right : ('a -> 'b -> 'b t) -> 'a list -> 'b -> 'b t
+  val fold_left : ('a -> 'b -> 'a t) -> 'a -> 'b list -> 'a t
+end
 
 module type S = sig
 
diff --git a/lib/monad.mli b/lib/monad.mli
index 39d4056384..768fb739d3 100644
--- a/lib/monad.mli
+++ b/lib/monad.mli
@@ -25,38 +25,42 @@ module type Def = sig
 end
 
 
-module type S = sig
+(** List combinators *)
+module type ListS = sig
 
-  include Def
+  type 'a t
 
-  (** List combinators *)
-  module List : sig
+  (** [List.map f l] maps [f] on the elements of [l] in left to right
+      order. *)
+  val map : ('a -> 'b t) -> 'a list -> 'b list t
 
-    (** [List.map f l] maps [f] on the elements of [l] in left to right
-        order. *)
-    val map : ('a -> 'b t) -> 'a list -> 'b list t
+  (** [List.map f l] maps [f] on the elements of [l] in right to left
+      order. *)
+  val map_right : ('a -> 'b t) -> 'a list -> 'b list t
 
-    (** [List.map f l] maps [f] on the elements of [l] in right to left
-        order. *)
-    val map_right : ('a -> 'b t) -> 'a list -> 'b list t
+  (** Like the regular [List.fold_right]. The monadic effects are
+      threaded right to left.
 
-    (** Like the regular [List.fold_right]. The monadic effects are
-        threaded right to left.
+      Note: many monads behave poorly with right-to-left order. For
+      instance a failure monad would still have to traverse the
+      whole list in order to fail and failure needs to be propagated
+      through the rest of the list in binds which are now
+      spurious. It is also the worst case for substitution monads
+      (aka free monads), exposing the quadratic behaviour.*)
+  val fold_right : ('a -> 'b -> 'b t) -> 'a list -> 'b -> 'b t
 
-        Note: many monads behave poorly with right-to-left order. For
-        instance a failure monad would still have to traverse the
-        whole list in order to fail and failure needs to be propagated
-        through the rest of the list in binds which are now
-        spurious. It is also the worst case for substitution monads
-        (aka free monads), exposing the quadratic behaviour.*)
-    val fold_right : ('a -> 'b -> 'b t) -> 'a list -> 'b -> 'b t
+  (** Like the regular [List.fold_left]. The monadic effects are
+      threaded left to right. It is tail-recursive if the [(>>=)]
+      operator calls its second argument in a tail position. *)
+  val fold_left : ('a -> 'b -> 'a t) -> 'a -> 'b list -> 'a t
+
+end
 
-    (** Like the regular [List.fold_left]. The monadic effects are
-        threaded left to right. It is tail-recursive if the [(>>=)]
-        operator calls its second argument in a tail position. *)
-    val fold_left : ('a -> 'b -> 'a t) -> 'a -> 'b list -> 'a t
+module type S = sig
+
+  include Def
 
-  end
+  module List : ListS with type 'a t := 'a t
 
 end