Remove unsafe code (Obj.magic) in Tacinterp.

This commit also introduces a module Monad to generate monadic combinators (currently, only List.map).

9 files changed, 137 insertions, 12 deletions

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 6415a1a78..746460421 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -154,6 +154,7 @@ Smartlocate
 Constrintern
 Modintern
 Constrextern
+Monad
 Proof_type
 Goal
 Logic
diff --git a/lib/clib.mllib b/lib/clib.mllib
index 2bd36cde2..d6d017c72 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -27,3 +27,4 @@ Serialize
 CUnix
 Envars
 Aux_file
+Monad
diff --git a/lib/genarg.ml b/lib/genarg.ml
index 58dfbc91a..306cdbed8 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -134,6 +134,22 @@ let app_pair f1 f2 = function
       (u, Obj.repr (o1,o2))
   | _ -> failwith "Genarg: not a pair"
 
+module Monadic (M:Monad.S) = struct
+
+  let app_list f = function
+  | (ListArgType t as u, l) ->
+      let o = Obj.magic l in
+      let open M in
+      let apply x =
+        f (in_gen t x) >>= fun y ->
+        return (out_gen t y)
+      in
+      M.List.map apply o >>= fun r ->
+      return (u, Obj.repr r)
+  | _ -> failwith "Genarg: not a list0"
+
+end
+
 let has_type (t, v) u = argument_type_eq t u
 
 let unquote x = x
diff --git a/lib/genarg.mli b/lib/genarg.mli
index 6eea3ac92..45f0dddf2 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -186,6 +186,16 @@ val app_pair :
       ('a generic_argument -> 'b generic_argument)
    -> 'a generic_argument -> 'b generic_argument
 
+module Monadic (M:Monad.S) : sig
+
+  (** [Monadic.app_list f x] maps the monadic computation [f] on
+      elements of [x], provided [x] has the tag [List0 t] for some [t]. It
+      fails otherwise. *)
+  val app_list : ('a generic_argument -> 'b generic_argument M.t) ->
+    'a generic_argument -> 'b generic_argument M.t
+
+end
+
 (** {6 Type reification} *)
 
 type argument_type =
diff --git a/lib/monad.ml b/lib/monad.ml
new file mode 100644
index 000000000..773f952de
--- /dev/null
+++ b/lib/monad.ml
@@ -0,0 +1,58 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+
+(** Combinators on monadic computations. *)
+
+
+(** A minimal definition necessary for the definition to go through. *)
+module type Def = sig
+
+  type +'a t
+  val return : 'a -> 'a t
+  val (>>=) : 'a t -> ('a -> 'b t) -> 'b t
+
+  (** The monadic laws must hold:
+      - [(x>>=f)>>=g] = [x>>=fun x' -> (f x'>>=g)]
+      - [return a >>= f] = [f a]
+      - [x>>=return] = [x]  *)
+
+end
+
+
+module type S = sig
+
+  include Def
+
+  (** List combinators *)
+  module List : sig
+
+    (** [map f l] applies the monadic effect left to right. *)
+    val map : ('a -> 'b t) -> 'a list -> 'b list t
+
+  end
+
+end
+
+
+module Make (M:Def) : S with type +'a t = 'a M.t = struct
+
+  include M
+
+  module List = struct
+
+    let rec map f = function
+      | [] -> return []
+      | a::l ->
+          f a >>= fun a' ->
+          map f l >>= fun l' ->
+          return (a'::l')
+
+  end
+
+end
diff --git a/lib/monad.mli b/lib/monad.mli
new file mode 100644
index 000000000..1f04cf5e0
--- /dev/null
+++ b/lib/monad.mli
@@ -0,0 +1,42 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+
+(** Combinators on monadic computations. *)
+
+
+(** A minimal definition necessary for the definition to go through. *)
+module type Def = sig
+
+  type +'a t
+  val return : 'a -> 'a t
+  val (>>=) : 'a t -> ('a -> 'b t) -> 'b t
+
+  (** The monadic laws must hold:
+      - [(x>>=f)>>=g] = [x>>=fun x' -> (f x'>>=g)]
+      - [return a >>= f] = [f a]
+      - [x>>=return] = [x]  *)
+
+end
+
+
+module type S = sig
+
+  include Def
+
+  (** List combinators *)
+  module List : sig
+
+    val map : ('a -> 'b t) -> 'a list -> 'b list t
+
+  end
+
+end
+
+(** Expands the monadic definition to extra combinators. *)
+module Make (M:Def) : S with type +'a t = 'a M.t
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 0dbbdca7c..338a8eede 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -647,6 +647,10 @@ module Notations = struct
 end
 
 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 ->
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 60a6c558c..eba673439 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -260,6 +260,8 @@ val tclTIMEOUT : int -> 'a tactic -> 'a tactic
 (** [mark_as_unsafe] signals that the current tactic is unsafe. *)
 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 ***)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 3d0c65862..1876651cb 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -949,6 +949,8 @@ let val_interp_glob ist (tac:glob_tactic_expr) : typed_generic_argument =
       let v = VFun (extract_trace ist,ist.lfun,[],t) in
       of_tacvalue v
 
+module GenargTac = Genarg.Monadic(Proofview.Monad)
+
 (* Interprets an l-tac expression into a value *)
 let rec val_interp ist (tac:glob_tactic_expr) (gl:Proofview.Goal.t) : typed_generic_argument Proofview.tactic =
   let value_interp ist =
@@ -2033,18 +2035,7 @@ and interp_atomic ist tac =
 	      let ans = List.map mk_ident (out_gen wit x) in
               Proofview.tclUNIT (in_gen (topwit (wit_list wit_genarg)) ans)
           | ListArgType t  ->
-              (* spiwack: unsafe, we should introduce relevant combinators.
-                 Before new tactical it simply read: [Genarg.app_list f x] *)
-              fold_list begin fun a l ->
-                f a gl >>= fun a' ->
-                l >>= fun l ->
-                Proofview.tclUNIT (a'::l)
-              end x (Proofview.tclUNIT []) >>= fun l ->
-		let wit_t = Obj.magic t in
-		let l = List.map (fun arg -> out_gen wit_t arg) l in
-              Proofview.tclUNIT (in_gen
-                                       (topwit (wit_list wit_t))
-				       l)
+              GenargTac.app_list (fun y -> f y gl) x
           | ExtraArgType _ ->
               (** Special treatment of tactics *)
               if has_type x (glbwit wit_tactic) then