Remove unsafe code (Obj.magic) in Tacinterp.

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

5 files changed, 127 insertions, 0 deletions

diff --git a/lib/clib.mllib b/lib/clib.mllib
index 2bd36cde26..d6d017c722 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 58dfbc91a1..306cdbed8b 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 6eea3ac926..45f0dddf2c 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 0000000000..773f952def
--- /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 0000000000..1f04cf5e0c
--- /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