Remove unsafe code (Obj.magic) in Tacinterp.

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

1 files changed, 42 insertions, 0 deletions

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