From 4d6b938e90ecd9dbfb29a0af28a7d8b6a657ae17 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack <arnaud@spiwack.net>
Date: Thu, 27 Feb 2014 13:50:57 +0100
Subject: Remove unsafe code (Obj.magic) in Tacinterp.

This commit also introduces a module Monad to generate monadic combinators (currently, only List.map).
---
 lib/monad.mli | 42 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 42 insertions(+)
 create mode 100644 lib/monad.mli

(limited to 'lib/monad.mli')

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
-- 
cgit v1.2.3