Tacinterp: more refactoring.

Introducing List.fold_right and List.fold_left in Monad.

3 files changed, 51 insertions, 19 deletions

diff --git a/lib/monad.ml b/lib/monad.ml
index a1508ae01c..7636b1630c 100644
--- a/lib/monad.ml
+++ b/lib/monad.ml
@@ -32,14 +32,30 @@ module type S = sig
   (** List combinators *)
   module List : sig
 
-    (** [map f l] maps [f] on the elements of [l] in left to right
+    (** [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
 
-    (** [map f l] maps [f] on the elements of [l] in right to left
+    (** [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.
+
+        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
 
 end
@@ -65,16 +81,18 @@ module Make (M:Def) : S with type +'a t = 'a M.t = struct
           f a >>= fun a' ->
           return (a'::l')
 
+    let rec fold_right f l x =
+      match l with
+      | [] -> return x
+      | a::l ->
+          fold_right f l x >>= fun acc ->
+          f a acc
+
+    let rec fold_left f x = function
+      | [] -> return x
+      | a::l ->
+          f x a >>= fun x' ->
+          fold_left f x' l
   end
 
 end
-
-
-
-
-
-
-
-
-
-
diff --git a/lib/monad.mli b/lib/monad.mli
index 5c4f74e51d..39d4056384 100644
--- a/lib/monad.mli
+++ b/lib/monad.mli
@@ -32,14 +32,30 @@ module type S = sig
   (** List combinators *)
   module List : sig
 
-    (** [map f l] maps [f] on the elements of [l] in left to right
+    (** [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
 
-    (** [map f l] maps [f] on the elements of [l] in right to left
+    (** [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.
+
+        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
 
 end
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 7d9720614e..ca2c914853 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1201,12 +1201,11 @@ and interp_letrec ist llc u gl =
 
 (* Interprets the clauses of a LetIn *)
 and interp_letin ist llc u gl =
-  let fold ((_, id), body) acc =
+  let fold acc ((_, id), body) =
     interp_tacarg ist body gl >>= fun v ->
-    acc >>= fun acc ->
     Proofview.tclUNIT (Id.Map.add id v acc)
   in
-  List.fold_right fold llc (Proofview.tclUNIT ist.lfun) >>= fun lfun ->
+  Proofview.Monad.List.fold_left fold ist.lfun llc >>= fun lfun ->
   let ist = { ist with lfun } in
   val_interp ist u gl
 
@@ -2033,11 +2032,10 @@ and interp_atomic ist tac =
       in
       Proofview.Goal.enter begin fun gl ->
         let addvar (x, v) accu =
-          accu >>= fun accu ->
           f v gl >>= fun v ->
           Proofview.tclUNIT (Id.Map.add x v accu)
         in
-        List.fold_right addvar l (Proofview.tclUNIT ist.lfun) >>= fun lfun ->
+        Proofview.Monad.List.fold_right addvar l ist.lfun >>= fun lfun ->
           let trace = push_trace (loc,LtacNotationCall s) ist in
           let ist = {
             lfun = lfun;