From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 lib/monad.ml | 168 -----------------------------------------------------------
 1 file changed, 168 deletions(-)
 delete mode 100644 lib/monad.ml

(limited to 'lib/monad.ml')

diff --git a/lib/monad.ml b/lib/monad.ml
deleted file mode 100644
index 2e55e969..00000000
--- a/lib/monad.ml
+++ /dev/null
@@ -1,168 +0,0 @@
-(***********************************************************************)
-(*  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 definition of monads, each of the combinators is used in the
-    [Make] functor. *)
-module type Def = sig
-
-  type +'a t
-  val return : 'a -> 'a t
-  val (>>=) : 'a t -> ('a -> 'b t) -> 'b t
-  val (>>) : unit t -> 'a t -> 'a t
-  val map : ('a -> 'b) -> 'a 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]
-
-      As well as the following identities:
-      - [x >> y] = [x >>= fun () -> y]
-      - [map f x] = [x >>= fun x' -> f x'] *)
-
-end
-
-module type ListS = sig
-
-  type 'a t
-
-  (** [List.map f l] maps [f] on the elements of [l] in left to right
-      order. *)
-  val map : ('a -> 'b t) -> 'a list -> 'b list t
-
-  (** [List.map f l] maps [f] on the elements of [l] in right to left
-      order. *)
-  val map_right : ('a -> 'b t) -> 'a list -> 'b list t
-
-  (** Like the regular [List.fold_right]. The monadic effects are
-      threaded right to left.
-
-      Note: many monads behave poorly with right-to-left order. For
-      instance a failure monad would still have to traverse the
-      whole list in order to fail and failure needs to be propagated
-      through the rest of the list in binds which are now
-      spurious. It is also the worst case for substitution monads
-      (aka free monads), exposing the quadratic behaviour.*)
-  val fold_right : ('a -> 'b -> 'b t) -> 'a list -> 'b -> 'b t
-
-  (** Like the regular [List.fold_left]. The monadic effects are
-      threaded left to right. It is tail-recursive if the [(>>=)]
-      operator calls its second argument in a tail position. *)
-  val fold_left : ('a -> 'b -> 'a t) -> 'a -> 'b list -> 'a t
-
-  (** Like the regular [List.iter]. The monadic effects are threaded
-      left to right. It is tail-recurisve if the [>>] operator calls
-      its second argument in a tail position. *)
-  val iter : ('a -> unit t) -> 'a list -> unit t
-
-  (** Like the regular {!CList.map_filter}. The monadic effects are threaded left*)
-  val map_filter : ('a -> 'b option t) -> 'a list -> 'b list t
-
-
-  (** {6 Two-list iterators} *)
-
-  (** [fold_left2 r f s l1 l2] behaves like {!fold_left} but acts
-      simultaneously on two lists. Runs [r] (presumably an
-      exception-raising computation) if both lists do not have the
-      same length. *)
-  val fold_left2 : 'a t ->
-    ('a -> 'b -> 'c -> 'a t) -> 'a -> 'b list -> 'c list -> 'a t
-
-end
-
-module type S = sig
-
-  include Def
-
-  (** List combinators *)
-  module List : ListS with type 'a t := 'a t
-
-end
-
-
-module Make (M:Def) : S with type +'a t = 'a M.t = struct
-
-  include M
-
-  module List = struct
-
-    (* The combinators are loop-unrolled to spare a some monadic binds
-       (it is a common optimisation to treat the last of a list of
-       bind specially) and hopefully gain some efficiency using fewer
-       jump. *)
-
-    let rec map f = function
-      | [] -> return []
-      | [a] ->
-          M.map (fun a' -> [a']) (f a)
-      | a::b::l ->
-          f a >>= fun a' ->
-          f b >>= fun b' ->
-          M.map (fun l' -> a'::b'::l') (map f l)
-
-    let rec map_right f = function
-      | [] -> return []
-      | [a] ->
-          M.map (fun a' -> [a']) (f a)
-      | a::b::l ->
-          map_right f l >>= fun l' ->
-          f b >>= fun b' ->
-          M.map (fun a' -> a'::b'::l') (f a)
-
-    let rec fold_right f l x =
-      match l with
-      | [] -> return x
-      | [a] -> f a x
-      | a::b::l ->
-          fold_right f l x >>= fun acc ->
-          f b acc >>= fun acc ->
-          f a acc
-
-    let rec fold_left f x = function
-      | [] -> return x
-      | [a] -> f x a
-      | a::b::l ->
-          f x a >>= fun x' ->
-          f x' b >>= fun x'' ->
-          fold_left f x'' l
-
-    let rec iter f = function
-      | [] -> return ()
-      | [a] -> f a
-      | a::b::l -> f a >> f b >> iter f l
-
-
-    let rec map_filter f = function
-      | [] -> return []
-      | a::l ->
-        f a >>= function
-        | None -> map_filter f l
-        | Some b ->
-          map_filter f l >>= fun filtered ->
-          return (b::filtered)
-
-    let rec fold_left2 r f x l1 l2 =
-      match l1,l2 with
-      | [] , [] -> return x
-      | [a] , [b] -> f x a b
-      | a1::a2::l1 , b1::b2::l2 ->
-          f x a1 b1 >>= fun x' ->
-          f x' a2 b2 >>= fun x'' ->
-          fold_left2 r f x'' l1 l2
-      | _ , _ -> r
-
-  end
-
-end
-
-
-
-- 
cgit v1.2.3