Tacinterp: refactoring using Monad.

Adds a combinator List.map_right which chains effects from right to left.

5 files changed, 59 insertions, 36 deletions

diff --git a/lib/monad.ml b/lib/monad.ml
index 773f952def..a1508ae01c 100644
--- a/lib/monad.ml
+++ b/lib/monad.ml
@@ -32,9 +32,14 @@ module type S = sig
   (** List combinators *)
   module List : sig
 
-    (** [map f l] applies the monadic effect left to right. *)
+    (** [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
+        order. *)
+    val map_right : ('a -> 'b t) -> 'a list -> 'b list t
+
   end
 
 end
@@ -53,6 +58,23 @@ module Make (M:Def) : S with type +'a t = 'a M.t = struct
           map f l >>= fun l' ->
           return (a'::l')
 
+    let rec map_right f = function
+      | [] -> return []
+      | a::l ->
+          map f l >>= fun l' ->
+          f a >>= fun a' ->
+          return (a'::l')
+
   end
 
 end
+
+
+
+
+
+
+
+
+
+
diff --git a/lib/monad.mli b/lib/monad.mli
index 1f04cf5e0c..5c4f74e51d 100644
--- a/lib/monad.mli
+++ b/lib/monad.mli
@@ -32,8 +32,14 @@ module type S = sig
   (** List combinators *)
   module List : sig
 
+    (** [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
+        order. *)
+    val map_right : ('a -> 'b t) -> 'a list -> 'b list t
+
   end
 
 end
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index c93ec3b234..d6c9a2097f 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -829,6 +829,19 @@ let sig_sig x = x.sigma
 (*******************************************************************)
 (* The state monad with state an evar map. *)
 
+module MonadR =
+  Monad.Make (struct
+
+    type +'a t = evar_map -> evar_map * 'a
+
+    let return a = fun s -> (s,a)
+
+    let (>>=) x f = fun s ->
+      let (s',a) = x s in
+      f a s'
+
+  end)
+
 module Monad =
   Monad.Make (struct
 
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 0e65b151c4..2b0e9ca684 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -276,7 +276,8 @@ val sig_sig : 'a sigma -> evar_map
 
 (** {5 The state monad with state an evar map} *)
 
-module Monad : Monad.S with type +'a t = evar_map -> 'a * evar_map
+module MonadR : Monad.S with type +'a t = evar_map -> evar_map * 'a
+module Monad  : Monad.S with type +'a t = evar_map -> 'a * evar_map
 
 (** {5 Meta machinery}
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 1876651cb2..7d9720614e 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -624,13 +624,11 @@ let interp_red_expr ist sigma env = function
   | Cbn f -> sigma , Cbn (interp_flag ist env f)
   | Lazy f -> sigma , Lazy (interp_flag ist env f)
   | Pattern l ->
-    let (sigma,l_interp) =
-      List.fold_right begin fun c (sigma,acc) ->
-	let (sigma,c_interp) = interp_constr_with_occurrences ist env sigma c in
-	sigma , c_interp :: acc
-      end l (sigma,[])
-    in
-    sigma , Pattern l_interp
+      let (sigma,l_interp) =
+        Evd.MonadR.List.map_right
+          (fun c sigma -> interp_constr_with_occurrences ist env sigma c) l sigma
+      in
+      sigma , Pattern l_interp
   | Simpl o ->
     sigma , Simpl (Option.map (interp_closed_typed_pattern_with_occurrences ist env sigma) o)
   | CbvVm o ->
@@ -1081,18 +1079,10 @@ and interp_tacarg ist arg gl =
       interp_ltac_reference loc true ist r gl
   | TacCall (loc,f,l) ->
       interp_ltac_reference loc true ist f gl >>= fun fv ->
-      List.fold_right begin fun a acc ->
-        interp_tacarg ist a gl >>= fun a_interp ->
-        acc >>= fun acc ->
-        Proofview.tclUNIT (a_interp::acc)
-      end l (Proofview.tclUNIT []) >>= fun largs ->
+      Proofview.Monad.List.map (fun a -> interp_tacarg ist a gl) l >>= fun largs ->
       interp_app loc ist fv largs gl
   | TacExternal (loc,com,req,la) ->
-      List.fold_right begin fun a acc ->
-        interp_tacarg ist a gl >>= fun a_interp ->
-        acc >>= fun acc ->
-        Proofview.tclUNIT (a_interp::acc)
-      end la (Proofview.tclUNIT []) >>= fun la_interp ->
+      Proofview.Monad.List.map (fun a -> interp_tacarg ist a gl) la >>= fun la_interp ->
       Proofview.V82.wrap_exceptions begin fun () ->
         interp_external loc ist gl com req la_interp
       end
@@ -1555,10 +1545,7 @@ and interp_atomic ist tac =
 	  let (sigma,c_interp) = pf_interp_type ist { gl with sigma=sigma } c in
 	  sigma , (interp_fresh_ident ist env id,n,c_interp) in
         let (sigma,l_interp) =
-	  List.fold_right begin fun c (sigma,acc) ->
-	    let (sigma,c_interp) = f sigma c in
-	    sigma , c_interp::acc
-	  end l (project gl,[])
+          Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl)
         in
         tclTHEN
 	  (tclEVARS sigma)
@@ -1577,10 +1564,7 @@ and interp_atomic ist tac =
 	  let (sigma,c_interp) = pf_interp_type ist { gl with sigma=sigma } c in
 	  sigma , (interp_fresh_ident ist env id,c_interp) in
         let (sigma,l_interp) =
-	  List.fold_right begin fun c (sigma,acc) ->
-	    let (sigma,c_interp) = f sigma c in
-	    sigma , c_interp::acc
-	  end l (project gl,[])
+          Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl)
         in
         tclTHEN
 	  (tclEVARS sigma)
@@ -1953,11 +1937,8 @@ and interp_atomic ist tac =
         let goal = Proofview.Goal.goal gl in
         let tac = Tacenv.interp_ml_tactic opn in
         let (sigma,args) =
-          (* spiwack: monadic List.map *)
-          List.fold_right begin fun a (sigma,acc) ->
-            let (sigma,a_interp) = interp_genarg ist env sigma concl goal a in
-	    sigma , a_interp::acc
-          end l (goal_sigma,[])
+          Evd.MonadR.List.map_right
+            (fun a sigma -> interp_genarg ist env sigma concl goal a) l goal_sigma
         in
         Proofview.V82.tclEVARS sigma <*>
         tac args ist
@@ -2012,10 +1993,10 @@ and interp_atomic ist tac =
           | ListArgType ConstrArgType ->
               let wit = glbwit (wit_list wit_constr) in
               let (sigma,l_interp) = Tacmach.New.of_old begin fun gl ->
-	        List.fold_right begin fun c (sigma,acc) ->
-	          let (sigma,c_interp) = mk_constr_value ist { gl with sigma=sigma } c in
-	          sigma , c_interp::acc
-	        end (out_gen wit x) (project gl,[])
+                Evd.MonadR.List.map_right
+                  (fun c sigma -> mk_constr_value ist { gl with sigma=sigma } c)
+                  (out_gen wit x)
+                  (project gl)
               end gl in
               Proofview.V82.tclEVARS sigma <*>
               Proofview.tclUNIT (in_gen (topwit (wit_list wit_genarg)) l_interp)