Adding a new folder corresponding to the low-level part of the pretyper

together with the tactic monad.

The move is not complete yet, because some file candidates for this directory
have almost useless dependencies in other ones that should not be moved.

3 files changed, 0 insertions, 484 deletions

diff --git a/proofs/logic_monad.ml b/proofs/logic_monad.ml
deleted file mode 100644
index d509670ec..000000000
--- a/proofs/logic_monad.ml
+++ /dev/null
@@ -1,326 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
-(*   \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
-
-  (** {!Pp.pp}. The buffer is also flushed. *)
-  let print = fun s -> (); fun () -> try Pp.msg_info s; Pp.pp_flush () with e ->
-    let (e, info) = Errors.push e in raise ~info e ()
-
-  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)
-
-  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 rational 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. (rich_exn -> 'r NonLogical.t) ->
-                     ('a -> (rich_exn -> 'r NonLogical.t) -> 'r NonLogical.t) ->
-                     'r NonLogical.t }
-
-  include Monad.Make(struct
-    type 'a t = state -> ('a * state) iolist
-
-    let return x : 'a t = (); fun s ->
-      { iolist = fun nil cons -> cons (x, s) nil }
-
-    let (>>=) (m : 'a t) (f : 'a -> 'b t) : 'b t = (); fun s ->
-      let m = m s in
-      { iolist = fun nil cons ->
-        m.iolist nil (fun (x, s) next -> (f x s).iolist next cons) }
-
-    let (>>) (m : unit t) (f : 'a t) : 'a t = (); fun s ->
-      let m = m s in
-      { iolist = fun nil cons ->
-        m.iolist nil (fun ((), s) next -> (f s).iolist next cons) }
-
-    let map (f : 'a -> 'b) (m : 'a t) : 'b t = (); fun s ->
-      let m = m s in
-      { iolist = fun nil cons -> m.iolist nil (fun (x, s) next -> cons (f x, s) next) }
-
-  end)
-
-  let zero e : 'a t = (); fun s ->
-    { iolist = fun nil cons -> nil e }
-
-  let plus m1 m2 : 'a t = (); fun s ->
-    let m1 = m1 s in
-    { iolist = fun nil cons -> m1.iolist (fun e -> (m2 e s).iolist nil cons) cons }
-
-  let ignore (m : 'a t) : unit t = (); fun s ->
-    let m = m s in
-    { iolist = fun nil cons -> m.iolist nil (fun (_, s) next -> cons ((), s) next) }
-
-  let lift (m : 'a NonLogical.t) : 'a t = (); fun s ->
-    { iolist = fun nil cons -> NonLogical.(m >>= fun x -> cons (x, s) nil) }
-
-  (** State related *)
-
-  let get : P.s t = (); fun s ->
-    { iolist = fun nil cons -> cons (s.sstate, s) nil }
-
-  let set (sstate : P.s) : unit t = (); fun s ->
-    { iolist = fun nil cons -> cons ((), { s with sstate }) nil }
-
-  let modify (f : P.s -> P.s) : unit t = (); fun s ->
-    { iolist = fun nil cons -> cons ((), { s with sstate = f s.sstate }) nil }
-
-  let current : P.e t = (); fun s ->
-    { iolist = fun nil cons -> cons (s.rstate, s) nil }
-
-  let local (type a) (e:P.e) (m:a t) : a t = (); fun s ->
-    let m = m { s with rstate = e } in
-    { iolist = fun nil cons ->
-      m.iolist nil (fun (x,s') next -> cons (x,{s' with rstate=s.rstate}) next) }
-
-  let put (w : P.w) : unit t = (); fun s ->
-    { iolist = fun nil cons -> cons ((), { s with wstate = P.wprod s.wstate w }) nil }
-
-  let update (f : P.u -> P.u) : unit t = (); fun s ->
-    { iolist = fun nil cons -> cons ((), { s with ustate = f s.ustate }) nil }
-
-  (** List observation *)
-
-  let once (m : 'a t) : 'a t = (); fun s ->
-    let m = m s in
-    { iolist = fun nil cons -> m.iolist nil (fun x _ -> cons x nil) }
-
-  let break (f : rich_exn -> rich_exn option) (m : 'a t) : 'a t = (); fun s ->
-    let m = m s in
-    { iolist = fun nil cons ->
-      m.iolist nil (fun x next -> cons x (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 reified) : 'a iolist =
-    { iolist = fun nil cons ->
-      let next = function
-      | Nil e -> nil e
-      | Cons (x, l) -> cons x (fun e -> (reflect (l e)).iolist nil cons)
-      in
-      NonLogical.(m >>= next)
-    }
-
-  let split (m : 'a t) : ('a, rich_exn -> 'a t) list_view t = (); fun s ->
-    let m = m s in
-    let rnil e = NonLogical.return (Nil e) in
-    let rcons p l = NonLogical.return (Cons (p, l)) in
-    { iolist = fun nil cons ->
-      let open NonLogical in
-      m.iolist rnil rcons >>= begin function
-      | Nil e -> cons (Nil e, s) nil
-      | Cons ((x, s), l) ->
-        let l e = (); fun _ -> 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 m = m 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 rnil rcons
-
-  let repr x = x
-
- end
diff --git a/proofs/logic_monad.mli b/proofs/logic_monad.mli
deleted file mode 100644
index ab729aff7..000000000
--- a/proofs/logic_monad.mli
+++ /dev/null
@@ -1,157 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
-(*   \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
-
-
-(** {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 : sig
-
-  include Monad.S
-
-  val ignore : 'a t -> unit t
-
-  type 'a ref
-
-  val ref : 'a -> 'a ref t
-  (** [Pervasives.(:=)] *)
-  val (:=) : 'a ref -> 'a -> unit t
-  (** [Pervasives.(!)] *)
-  val (!) : 'a ref -> 'a t
-
-  val read_line : string t
-  val print_char : char -> unit t
-  (** {!Pp.pp}. The buffer is also flushed. *)
-  val print : Pp.std_ppcmds -> unit t
-
-  (** [Pervasives.raise]. Except that exceptions are wrapped with
-      {!Exception}. *)
-  val raise : ?info:Exninfo.info -> exn -> 'a t
-  (** [try ... with ...] but restricted to {!Exception}. *)
-  val catch : 'a t -> (Exninfo.iexn -> 'a t) -> 'a t
-  val timeout : int -> 'a t -> 'a t
-
-  (** Construct a monadified side-effect. Exceptions raised by the argument are
-      wrapped with {!Exception}. *)
-  val make : (unit -> 'a) -> 'a t
-
-  (** [run] performs effects. *)
-  val run : 'a t -> 'a
-
-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
-
-(** The monad is parametrised in the types of state, environment and
-    writer. *)
-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) : sig
-
-  include Monad.S
-
-  val ignore : 'a t -> unit t
-
-  val set : P.s -> unit t
-  val get : P.s t
-  val modify : (P.s -> P.s) -> unit t
-  val put : P.w -> unit t
-  val current : P.e t
-  val local : P.e -> 'a t -> 'a t
-  val update : (P.u -> P.u) -> unit t
-
-  val zero : Exninfo.iexn -> 'a t
-  val plus : 'a t -> (Exninfo.iexn -> 'a t) -> 'a t
-  val split : 'a t -> (('a,(Exninfo.iexn->'a t)) list_view) t
-  val once : 'a t -> 'a t
-  val break : (Exninfo.iexn -> Exninfo.iexn option) -> 'a t -> 'a t
-
-  val lift : 'a NonLogical.t -> 'a t
-
-  type 'a reified
-
-  val repr : 'a reified -> ('a, Exninfo.iexn -> 'a reified) list_view NonLogical.t
-
-  val run : 'a t -> P.e -> P.s -> ('a * P.s * P.w * P.u) reified
-
-end
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 32bf5576f..de0879127 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -4,7 +4,6 @@ Evar_refiner
 Proof_using
 Proof_type
 Proof_errors
-Logic_monad
 Proofview_monad
 Logic
 Proofview