Code refactoring thanks to the new Monad module.

9 files changed, 29 insertions, 56 deletions

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 746460421..0138f7034 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -42,6 +42,7 @@ Stateid
 Ephemeron
 Future
 RemoteCounter
+Monad
 
 Names
 Univ
@@ -154,7 +155,6 @@ Smartlocate
 Constrintern
 Modintern
 Constrextern
-Monad
 Proof_type
 Goal
 Logic
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 0e53ff131..c93ec3b23 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -826,6 +826,22 @@ type 'a sigma = {
 let sig_it x = x.it
 let sig_sig x = x.sigma
 
+(*******************************************************************)
+(* The state monad with state an evar map. *)
+
+module Monad =
+  Monad.Make (struct
+
+    type +'a t = evar_map -> 'a * evar_map
+
+    let return a = fun s -> (a,s)
+
+    let (>>=) x f = fun s ->
+      let (a,s') = x s in
+      f a s'
+
+  end)
+
 (**********************************************************)
 (* Failure explanation *)
 
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 58e4cd630..0e65b151c 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -274,6 +274,10 @@ type 'a sigma = {
 val sig_it  : 'a sigma -> 'a
 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
+
 (** {5 Meta machinery}
 
     These functions are almost deprecated. They were used before the
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 4d1aa4124..07bdbda00 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -450,31 +450,6 @@ let rename_hyp id1 id2 = (); fun env rdefs gl info ->
   rdefs := Evd.define gl.content new_subproof !rdefs;
   { subgoals = [new_goal] }
 
-(*** Additional functions ***)
-
-(* emulates List.map for functions of type
-   [Evd.evar_map -> 'a -> 'b * Evd.evar_map] on lists of type 'a, by propagating
-   new evar_map to next definition. *)
-(*This sort of construction actually works with any monad (here the State monade
-   in Haskell). There is a generic construction in Haskell called mapM.
-*)
-let rec list_map f l s =
-  match l with
-  | [] -> ([],s)
-  | a::l -> let (a,s) = f s a in
-               let (l,s) = list_map f l s in
-	       (a::l,s)
-
-(* Another instance of the generic monadic map *)
-let rec sensitive_list_map f = function
-  | [] -> return []
-  | a::l ->
-      bind (f a) begin fun a' ->
-      bind (sensitive_list_map f l) begin fun l' ->
-      return (a'::l')
-      end
-      end
-
 
 (* Layer to implement v8.2 tactic engine ontop of the new architecture.
    Types are different from what they used to be due to a change of the
diff --git a/proofs/goal.mli b/proofs/goal.mli
index db864b273..87793878c 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -157,19 +157,6 @@ val defs : Evd.evar_map sensitive
    primitive. *)
 val enter : (Environ.env -> Evd.evar_map -> Environ.named_context_val -> Term.constr -> goal -> 'a) -> 'a sensitive
 
-(*** Additional functions ***)
-
-(* emulates List.map for functions of type 
-   [Evd.evar_map -> 'a -> 'b * Evd.evar_map] on lists of type 'a, by propagating
-   new evar_map to next definition *)
-val list_map : 
-  (Evd.evar_map -> 'a -> 'b * Evd.evar_map) ->
-  'a list -> Evd.evar_map ->
-    'b list * Evd.evar_map
-
-(* emulates List.map for [sensitive] Kleisli functions. *)
-val sensitive_list_map : ('a -> 'b sensitive) -> 'a list -> 'b list sensitive
-
 (* Layer to implement v8.2 tactic engine ontop of the new architecture. 
    Types are different from what they used to be due to a change of the
    internal types. *)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 0b9aa9907..68be51d9c 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -583,7 +583,7 @@ let prim_refiner r sigma goal =
 		  ("Name "^Id.to_string f^" already used in the environment");
 	      mk_sign (push_named_context_val (f,None,ar) sign) oth
 	  | [] ->
-	      Goal.list_map (fun sigma (_,_,c) ->
+	      Evd.Monad.List.map (fun (_,_,c) sigma ->
                 let gl,ev,sig' =
                   Goal.V82.mk_goal sigma sign c (Goal.V82.extra sigma goal) in
                 (gl,ev),sig')
@@ -625,7 +625,7 @@ let prim_refiner r sigma goal =
               |	Not_found ->
                   mk_sign (push_named_context_val (f,None,ar) sign) oth)
 	  | [] -> 
-              Goal.list_map (fun sigma(_,c) ->
+              Evd.Monad.List.map (fun (_,c) sigma ->
                 let gl,ev,sigma =
                   Goal.V82.mk_goal sigma sign c (Goal.V82.extra sigma goal) in
                 (gl,ev),sigma)
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 338a8eede..76af0c1e0 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -651,13 +651,6 @@ open Notations
 module Monad =
   Monad.Make(struct type +'a t = 'a tactic let return=tclUNIT let (>>=)=(>>=) end)
 
-let rec list_map f = function
-  | [] -> tclUNIT []
-  | a::l ->
-      f a >>= fun a' ->
-      list_map f l >>= fun l' ->
-      tclUNIT (a'::l')
-
 
 (*** Compatibility layer with <= 8.2 tactics ***)
 module V82 = struct
@@ -670,7 +663,7 @@ module V82 = struct
     let (>>=) = Proof.bind in
     Proof.get >>= fun ps ->
     try
-      let tac evd gl = 
+      let tac gl evd = 
         let glsigma  =
           tac { Evd.it = gl ; sigma = evd; }  in
         let sigma = glsigma.Evd.sigma in
@@ -679,9 +672,9 @@ module V82 = struct
       in
         (* Old style tactics expect the goals normalized with respect to evars. *)
       let (initgoals,initevd) =
-        Goal.list_map Goal.V82.nf_evar ps.comb ps.solution
+        Evd.Monad.List.map (fun g s -> Goal.V82.nf_evar s g) ps.comb ps.solution
       in
-      let (goalss,evd) = Goal.list_map tac initgoals initevd in
+      let (goalss,evd) = Evd.Monad.List.map tac initgoals initevd in
       let sgs = List.flatten goalss in
       Proof.set { ps with solution=evd ; comb=sgs; }
     with e when catchable_exception e ->
@@ -696,7 +689,7 @@ module V82 = struct
     let (>>=) = Proof.bind in
     Proof.get >>= fun ps ->
     let (goals,evd) =
-      Goal.list_map Goal.V82.nf_evar ps.comb ps.solution
+      Evd.Monad.List.map (fun g s -> Goal.V82.nf_evar s g) ps.comb ps.solution
     in
     Proof.set { ps with solution=evd ; comb=goals }
 
@@ -796,7 +789,7 @@ module Goal = struct
     Proof.get >>= fun step ->
     try
       let (ks,sigma) =
-        Goal.list_map begin fun sigma g ->
+        Evd.Monad.List.map begin fun g sigma ->
           Util.on_fst k (Goal.eval s env sigma g)
         end step.comb step.solution
       in
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index eba673439..7e2d374d5 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -262,8 +262,6 @@ val mark_as_unsafe : unit tactic
 
 module Monad : Monad.S with type +'a t = 'a tactic
 
-val list_map : ('a -> 'b tactic) -> 'a list -> 'b list tactic
-
 (*** Commands ***)
 
 val in_proofview : proofview -> (Evd.evar_map -> 'a) -> 'a
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 098e45a4a..d6139f529 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1196,7 +1196,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
     Proofview.tclZERO (Errors.UserError ("Equality.inj" , str "Failed to decompose the equality."))
   else
     Proofview.tclBIND
-      (Proofview.list_map
+      (Proofview.Monad.List.map
          (fun (pf,ty) -> Tacticals.New.tclTHENS (cut ty) [Proofview.tclUNIT (); Proofview.V82.tactic (refine pf)])
          (if l2r then List.rev injectors else injectors))
       (fun _ -> tac (List.length injectors))