Imported Upstream version 8.6

1 files changed, 0 insertions, 321 deletions

diff --git a/proofs/logic_monad.ml b/proofs/logic_monad.ml
deleted file mode 100644
index 68efa71e..00000000
--- a/proofs/logic_monad.ml
+++ /dev/null
@@ -1,321 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** This file defines the low-level monadic operations used by the
-    tactic monad. The monad is divided into two layers: a non-logical
-    layer which consists in operations which will not (or cannot) be
-    backtracked in case of failure (input/output or persistent state)
-    and a logical layer which handles backtracking, proof
-    manipulation, and any other effect which needs to backtrack. *)
-
-
-(** {6 Exceptions} *)
-
-
-(** To help distinguish between exceptions raised by the IO monad from
-    the one used natively by Coq, the former are wrapped in
-    [Exception].  It is only used internally so that [catch] blocks of
-    the IO monad would only catch exceptions raised by the [raise]
-    function of the IO monad, and not for instance, by system
-    interrupts. Also used in [Proofview] to avoid capturing exception
-    from the IO monad ([Proofview] catches errors in its compatibility
-    layer, and when lifting goal-level expressions). *)
-exception Exception of exn
-(** This exception is used to signal abortion in [timeout] functions. *)
-exception Timeout
-(** This exception is used by the tactics to signal failure by lack of
-    successes, rather than some other exceptions (like system
-    interrupts). *)
-exception TacticFailure of exn
-
-let _ = Errors.register_handler begin function
-  | Timeout -> Errors.errorlabstrm "Some timeout function" (Pp.str"Timeout!")
-  | Exception e -> Errors.print e
-  | TacticFailure e -> Errors.print e
-  | _ -> Pervasives.raise Errors.Unhandled
-end
-
-(** {6 Non-logical layer} *)
-
-(** The non-logical monad is a simple [unit -> 'a] (i/o) monad. The
-    operations are simple wrappers around corresponding usual
-    operations and require little documentation. *)
-module NonLogical =
-struct
-
-  (* The functions in this module follow the pattern that they are
-     defined with the form [(); fun ()->...]. This is an optimisation
-     which signals to the compiler that the function is usually partially
-     applied up to the [();]. Without this annotation, partial
-     applications can be significantly slower.
-
-     Documentation of this behaviour can be found at:
-     https://ocaml.janestreet.com/?q=node/30 *)
-
-  include Monad.Make(struct
-    type 'a t = unit -> 'a
-
-    let return a = (); fun () -> a
-    let (>>=) a k = (); fun () -> k (a ()) ()
-    let (>>) a k = (); fun () -> a (); k ()
-    let map f a = (); fun () -> f (a ())
-  end)
-
-  type 'a ref = 'a Pervasives.ref
-
-  let ignore a = (); fun () -> ignore (a ())
-
-  let ref a = (); fun () -> Pervasives.ref a
-
-  (** [Pervasives.(:=)] *)
-  let (:=) r a = (); fun () -> r := a
-
-  (** [Pervasives.(!)] *)
-  let (!) = fun r -> (); fun () -> ! r
-
-  (** [Pervasives.raise]. Except that exceptions are wrapped with
-      {!Exception}. *)
-  let raise ?info = fun e -> (); fun () -> Exninfo.raise ?info (Exception e)
-
-  (** [try ... with ...] but restricted to {!Exception}. *)
-  let catch = fun s h -> ();
-    fun () -> try s ()
-      with Exception e as src ->
-        let (src, info) = Errors.push src in
-        h (e, info) ()
-
-  let read_line = fun () -> try Pervasives.read_line () with e ->
-    let (e, info) = Errors.push e in raise ~info e ()
-
-  let print_char = fun c -> (); fun () -> print_char c
-
-  let timeout = fun n t -> (); fun () ->
-    Control.timeout n t (Exception Timeout)
-
-  let make f = (); fun () ->
-    try f ()
-    with e when Errors.noncritical e ->
-      let (e, info) = Errors.push e in
-      Util.iraise (Exception e, info)
-
-  (** Use the current logger. The buffer is also flushed. *)
-  let print_debug s = make (fun _ -> Pp.msg_info s;Pp.pp_flush ())
-  let print_info s =  make (fun _ -> Pp.msg_info s;Pp.pp_flush ())
-  let print_warning s =  make (fun _ -> Pp.msg_warning s;Pp.pp_flush ())
-  let print_error s =  make (fun _ -> Pp.msg_error s;Pp.pp_flush ())
-  let print_notice s = make (fun _ -> Pp.msg_notice s;Pp.pp_flush ())
-
-  let run = fun x ->
-    try x () with Exception e as src ->
-      let (src, info) = Errors.push src in
-      Util.iraise (e, info)
-end
-
-(** {6 Logical layer} *)
-
-(** The logical monad is a backtracking monad on top of which is
-    layered a state monad (which is used to implement all of read/write,
-    read only, and write only effects). The state monad being layered on
-    top of the backtracking monad makes it so that the state is
-    backtracked on failure.
-
-    Backtracking differs from regular exception in that, writing (+)
-    for exception catching and (>>=) for bind, we require the
-    following extra distributivity laws:
-
-    x+(y+z) = (x+y)+z
-
-    zero+x = x
-
-    x+zero = x
-
-    (x+y)>>=k = (x>>=k)+(y>>=k) *)
-
-(** A view type for the logical monad, which is a form of list, hence
-    we can decompose it with as a list. *)
-type ('a, 'b) list_view =
-  | Nil of Exninfo.iexn
-  | Cons of 'a * 'b
-
-module type Param = sig
-
-  (** Read only *)
-  type e
-
-  (** Write only *)
-  type w
-
-  (** [w] must be a monoid *)
-  val wunit : w
-  val wprod : w -> w -> w
-
-  (** Read-write *)
-  type s
-
-  (** Update-only. Essentially a writer on [u->u]. *)
-  type u
-
-  (** [u] must be pointed. *)
-  val uunit : u
-
-end
-
-
-module Logical (P:Param) =
-struct
-
-  (** All three of environment, writer and state are coded as a single
-      state-passing-style monad.*)
-  type state = {
-    rstate : P.e;
-    ustate : P.u;
-    wstate : P.w;
-    sstate : P.s;
-  }
-
-  (** Double-continuation backtracking monads are reasonable folklore
-      for "search" implementations (including the Tac interactive
-      prover's tactics). Yet it's quite hard to wrap your head around
-      these.  I recommand reading a few times the "Backtracking,
-      Interleaving, and Terminating Monad Transformers" paper by
-      O. Kiselyov, C. Shan, D. Friedman, and A. Sabry.  The peculiar
-      shape of the monadic type is reminiscent of that of the
-      continuation monad transformer.
-
-      The paper also contains the rationale for the [split] abstraction.
-
-      An explanation of how to derive such a monad from mathematical
-      principles can be found in "Kan Extensions for Program
-      Optimisation" by Ralf Hinze.
-
-      A somewhat concrete view is that the type ['a iolist] is, in fact
-      the impredicative encoding of the following stream type:
-
-      [type 'a _iolist' = Nil of exn | Cons of 'a*'a iolist'
-      and 'a iolist = 'a _iolist NonLogical.t]
-
-      Using impredicative encoding avoids intermediate allocation and
-      is, empirically, very efficient in Ocaml. It also has the
-      practical benefit that the monadic operation are independent of
-      the underlying monad, which simplifies the code and side-steps
-      the limited inlining of Ocaml.
-
-      In that vision, [bind] is simply [concat_map] (though the cps
-      version is significantly simpler), [plus] is concatenation, and
-      [split] is pattern-matching. *)
-  type rich_exn = Exninfo.iexn
-
-  type 'a iolist =
-    { iolist : 'r. state -> (rich_exn -> 'r NonLogical.t) ->
-      ('a -> state -> (rich_exn -> 'r NonLogical.t) -> 'r NonLogical.t) ->
-      'r NonLogical.t }
-
-  include Monad.Make(struct
-
-    type 'a t = 'a iolist
-
-    let return x =
-      { iolist = fun s nil cons -> cons x s nil }
-
-    let (>>=) m f =
-      { iolist = fun s nil cons ->
-        m.iolist s nil (fun x s next -> (f x).iolist s next cons) }
-
-    let (>>) m f =
-      { iolist = fun s nil cons ->
-        m.iolist s nil (fun () s next -> f.iolist s next cons) }
-
-    let map f m =
-      { iolist = fun s nil cons -> m.iolist s nil (fun x s next -> cons (f x) s next) }
-
-  end)
-
-  let zero e =
-    { iolist = fun _ nil cons -> nil e }
-
-  let plus m1 m2 =
-    { iolist = fun s nil cons -> m1.iolist s (fun e -> (m2 e).iolist s nil cons) cons }
-
-  let ignore m =
-    { iolist = fun s nil cons -> m.iolist s nil (fun _ s next -> cons () s next) }
-
-  let lift m =
-    { iolist = fun s nil cons -> NonLogical.(m >>= fun x -> cons x s nil) }
-
-  (** State related *)
-
-  let get =
-    { iolist = fun s nil cons -> cons s.sstate s nil }
-
-  let set (sstate : P.s) =
-    { iolist = fun s nil cons -> cons () { s with sstate } nil }
-
-  let modify (f : P.s -> P.s) =
-    { iolist = fun s nil cons -> cons () { s with sstate = f s.sstate } nil }
-
-  let current =
-    { iolist = fun s nil cons -> cons s.rstate s nil }
-
-  let local e m =
-    { iolist = fun s nil cons ->
-      m.iolist { s with rstate = e } nil
-        (fun x s' next -> cons x {s' with rstate = s.rstate} next) }
-
-  let put w =
-    { iolist = fun s nil cons -> cons () { s with wstate = P.wprod s.wstate w } nil }
-
-  let update (f : P.u -> P.u) =
-    { iolist = fun s nil cons -> cons () { s with ustate = f s.ustate } nil }
-
-  (** List observation *)
-
-  let once m =
-    { iolist = fun s nil cons -> m.iolist s nil (fun x s _ -> cons x s nil) }
-
-  let break f m =
-    { iolist = fun s nil cons ->
-      m.iolist s nil (fun x s next -> cons x s (fun e -> match f e with None -> next e | Some e -> nil e))
-    }
-
-  (** For [reflect] and [split] see the "Backtracking, Interleaving,
-      and Terminating Monad Transformers" paper.  *)
-  type 'a reified = ('a, rich_exn -> 'a reified) list_view NonLogical.t
-
-  let rec reflect (m : ('a * state) reified) : 'a iolist =
-    { iolist = fun s0 nil cons ->
-      let next = function
-      | Nil e -> nil e
-      | Cons ((x, s), l) -> cons x s (fun e -> (reflect (l e)).iolist s0 nil cons)
-      in
-      NonLogical.(m >>= next)
-    }
-
-  let split m : ('a, rich_exn -> 'a t) list_view t =
-    let rnil e = NonLogical.return (Nil e) in
-    let rcons p s l = NonLogical.return (Cons ((p, s), l)) in
-    { iolist = fun s nil cons ->
-      let open NonLogical in
-      m.iolist s rnil rcons >>= begin function
-      | Nil e -> cons (Nil e) s nil
-      | Cons ((x, s), l) ->
-        let l e = reflect (l e) in
-        cons (Cons (x, l)) s nil
-      end }
-
-  let run m r s =
-    let s = { wstate = P.wunit; ustate = P.uunit; rstate = r; sstate = s } in
-    let rnil e = NonLogical.return (Nil e) in
-    let rcons x s l =
-      let p = (x, s.sstate, s.wstate, s.ustate) in
-      NonLogical.return (Cons (p, l))
-    in
-    m.iolist s rnil rcons
-
-  let repr x = x
-
- end