Cleaning of the new implementation of the tactic monad.

* Add comments in the code (mostly imported from Monad.v)
* Inline duplicated module
* Clean up some artifacts due to the extracted code.
* [NonLogical.new_ref] -> [NonLogical.ref] (I don't even remember why I chose this name originally)
* Remove the now superfluous [Proof_errors] module (which was used to define exceptions to be used in the extracted code).
* Remove Monad.v

1 files changed, 0 insertions, 714 deletions

diff --git a/bootstrap/Monads.v b/bootstrap/Monads.v
deleted file mode 100644
index d0412827b1..0000000000
--- a/bootstrap/Monads.v
+++ /dev/null
@@ -1,714 +0,0 @@
-(* -*- coq-prog-args: ("-emacs-U" "-impredicative-set") -*- *)
-
-Reserved Notation "'do' M x ':=' e 'in' u" (at level 200, M at level 0, x ident, e at level 200, u at level 200).
-(*Reserved Notation "'do' e ; u" (at level 200, e at level 200, u at level 200).*)
-
-(*** Unit ***)
-
-Extract Inductive unit => unit [
-  "()"
-].
-Notation "()" := tt.
-
-(*** Bool ***)
-Extract Inductive bool => bool [
-  "true"
-  "false"
-].
-
-(*** List ***)
-Extract Inductive list => list [
-  "[]"
-  "(::)"
-].
-Opaque app.
-Extraction Implicit app [A].
-Extract Inlined Constant app => "List.append".
-
-(*** Prod ***)
-Extract Inductive prod => "(*)" [
-  "(,)"
-].
-Opaque fst.
-Extraction Implicit fst [A B].
-Extract Inlined Constant fst => "fst".
-Extraction Implicit snd [A B].
-Opaque snd.
-Extract Inlined Constant snd => "snd".
-
-
-(*** Closure elimination **)
-
-(* [freeze] is used to help OCaml figure where partial applications
-   are usually made. This way, the compiler will output code optimised
-   for partial applications to happen at this point. It happens to
-   make the monadic code substantially faster.
-
-   Documentation on that particular behaviour can be found at:
-   https://ocaml.janestreet.com/?q=node/30
-*)
-
-Parameter freeze : forall (A : Set), A -> A.
-Extraction Implicit freeze [A].
-Extract Inlined Constant freeze => "();".
-
-(*** Exceptions ***)
-
-Parameter Exception : Set.
-Extract Inlined Constant Exception => exn.
-
-Parameter tactic_failure : Exception -> Exception.
-Extract Inlined Constant tactic_failure => "(fun e -> Proof_errors.TacticFailure e)".
-
-(*** Basic integers ***)
-
-Parameter Int : Set.
-Extract Inlined Constant Int => int.
-
-(*** Char ***)
-
-Parameter Char : Set.
-Extract Inlined Constant Char => char.
-
-(*** Primitive strings ***)
-
-Parameter String : Set.
-Extract Inlined Constant String => string.
-
-(*** Pretty printer ***)
-
-Parameter Ppcmds : Set.
-Extract Inlined Constant Ppcmds => "Pp.std_ppcmds".
-
-(*** A view datatype for the [split] primitive ***)
-
-Inductive list_view (A B:Set) : Set :=
-| Nil : Exception -> list_view A B
-| Cons : A -> B -> list_view A B
-.
-
-(*** Monoids ***)
-
-Module Monoid.
-
-Record T (M:Set) := {
-  zero : M;
-  prod : M -> M -> M
-}.
-
-(** Cartesian product of monoids *)
-Definition cart {M₁} (Mon₁:T M₁) {M₂} (Mon₂:T M₂) : T (M₁*M₂) := {|
-  zero := (Mon₁.(zero _),Mon₂.(zero _));
-  prod x y := (Mon₁.(prod _) (fst x) (fst y), Mon₂.(prod _) (snd x) (snd y))
-|}.
-
-Definition BoolAnd : T bool := {|
-  zero := true;
-  prod := andb
-|}.
-
-Definition List {A:Set} : T (list A) := {|
-  zero := nil ;
-  prod := @app _
-|}.
-
-End Monoid.
-
-(*** Monads and related interfaces ***)
-(* spiwack: the interfaces are presented in a mixin style.
-   I haven't tested other presentation, it just felt
-   convenient when I started *)
-
-Record Monad (T:Set->Set) := {
-  ret : forall{A:Set}, A->T A;
-  bind : forall{A B:Set}, T A -> (A -> T B) -> T B;
-  ignore : forall{A:Set}, T A -> T unit;
-  seq : forall{A:Set}, T unit -> T A -> T A;
-  map : forall {A B : Set}, (A -> B) -> T A -> T B
-}.
-
-Notation "'do' M x ':=' e 'in' u" := (bind _ M e (fun x => u)).
-
-Record State (S:Set) (T:Set->Set) := {
-  set : S -> T unit;
-  get : T S ;
-  modify : (S -> S) -> T unit
-}.
-
-(* spiwack: Environment and Writer are given distinct interfaces from
-   State (rather than state beeing the composition of these) because I
-   don't really know how to combine the three together. However, we
-   might want to be able to arrange things so that we can say "I have a
-   number of things I can get, and a number of things I can set, some
-   of which can be got, and the other being monoids, then I have a
-   monad". I have yet to find how to do that though.*)
-Record Environment (E:Set) (T:Set->Set) := { current : T E }.
-
-Record Writer (M:Set) (T:Set->Set) := {
-  put : M -> T unit
-}.
-
-Record Logic (T:Set -> Set) := {
-  (* [zero] is usually argument free, but Coq likes to explain errors,
-     hence error messages should be carried around. *)
-  zero : forall {A}, Exception -> T A;
-  plus : forall {A}, T A -> (Exception -> T A) -> T A
-}.
-(** Writing (+) for plus and (>>=) for bind, we shall require that
-
-    x+(y+z) = (x+y)+z
-
-    zero+x = x
-
-    x+zero = x
-
-    (x+y)>>=k = (x>>=k)+(y>>=k) *)
-(* The [T] argument represents the "global" effect: it is not
-   backtracked when backtracking occurs at a [plus]. *)
-(* spiwack: hence, [T] will not be instanciated with a state monad
-   representing the proofs, we will use a surrounding state transformer
-   to that effect. [T] is meant to be instantiated with [IO]. *)
-
-
-Module Id.
-
- Definition M : Monad (fun A => A) := {|
-   ret := fun _ x => x;
-   bind := fun _ _ x k => k x;
-   ignore := fun _ x => ();
-   seq := fun _ x k => k;
-   map := fun _ _ f x => f x
- |}.
-
-End Id.
-
-Module IOBase.
-
- Parameter T : Set -> Set.
- Extract Constant T "'a" => "unit -> 'a".
- Parameter Ref : Set -> Set.
- Extract Constant Ref "'a" => "'a Pervasives.ref".
-
- Parameter ret : forall (A:Set), A -> T A.
- Extract Constant ret => "fun a -> (); fun () -> a".
- Extraction Implicit ret [A].
- Parameter bind : forall A B, T A -> (A->T B) -> T B.
- Extract Constant bind => "fun a k -> (); fun () -> k (a ()) ()".
- Extraction Implicit bind [A B].
- Parameter ignore : forall A, T A -> T unit.
- Extract Constant ignore => "fun a -> (); fun () -> ignore (a ())".
- Extraction Implicit ignore [A].
- Parameter seq : forall A, T unit -> T A -> T A.
- Extract Constant seq => "fun a k -> (); fun () -> a (); k ()".
- Extraction Implicit seq [A].
- Parameter map : forall (A B : Set), (A -> B) -> T A -> T B.
- Extract Constant map => "fun f a -> (); fun () -> f (a ())".
- Extraction Implicit map [A B].
-
- Parameter ref : forall (A:Set), A -> T (Ref A).
- Extract Constant ref => "fun a -> (); fun () -> Pervasives.ref a".
- Extraction Implicit ref [A].
- Parameter set : forall A, Ref A -> A -> T unit.
- Extract Constant set => "fun r a -> (); fun () -> Pervasives.(:=) r a".
- Extraction Implicit set [A].
- Parameter get : forall A, Ref A -> T A.
- Extract Constant get => "fun r -> (); fun () -> Pervasives.(!) r".
- Extraction Implicit get [A].
-
- Parameter raise : forall A, Exception -> T A.
- Extract Constant raise => "fun e -> (); fun () -> raise (Proof_errors.Exception e)".
- Extraction Implicit raise [A].
- Parameter catch : forall A, T A -> (Exception -> T A) -> T A.
- Extract Constant catch => "fun s h -> ();
-  fun () -> try s ()
-  with Proof_errors.Exception e as src ->
-    let src = Errors.push src in
-    let e = Backtrace.app_backtrace ~src ~dst:e in
-    h e ()".
- Extraction Implicit catch [A].
-
- Parameter read_line : T String.
- Extract Constant read_line => "fun () -> try Pervasives.read_line () with e -> let e = Errors.push e in raise e ()".
- Parameter print_char : Char -> T unit.
- Extract Constant print_char => "fun c -> (); fun () -> print_char c".
- Parameter print : Ppcmds -> T unit.
- Extract Constant print => "fun s -> (); fun () -> try Pp.pp s; Pp.pp_flush () with e -> let e = Errors.push e in raise e ()".
-
- Parameter timeout: forall A, Int -> T A -> T A.
- Extract Constant timeout => "fun n t -> (); fun () -> Control.timeout n t (Proof_errors.Exception Proof_errors.Timeout)".
- Extraction Implicit timeout [A].
-
-End IOBase.
-
-(* spiwack: IO is split in two modules to avoid moot dependencies and
-   useless extracted code. *)
-Module IO.
-
- Record S (Ref:Set->Set) (T:Set->Set) : Set := {
-   ref : forall {A:Set}, A -> T (Ref A);
-   set : forall {A:Set}, Ref A -> A -> T unit;
-   get : forall {A:Set}, Ref A -> T A;
-
-   read_line : T String;
-   print_char : Char -> T unit;
-   print : Ppcmds -> T unit;
-
-   raise : forall {A:Set}, Exception -> T A;
-   catch : forall {A:Set}, T A -> (Exception -> T A) -> T A;
-   timeout : forall {A:Set}, Int -> T A -> T A
- }.
-
- Definition T : Set -> Set := IOBase.T.
- Definition Ref : Set -> Set := IOBase.Ref.
-
- Definition M : Monad T := {|
-   ret := IOBase.ret;
-   bind := IOBase.bind;
-   ignore := IOBase.ignore;
-   seq := IOBase.seq;
-   map := IOBase.map
- |}.
-
- Definition IO : S Ref T := {|
-   ref := IOBase.ref;
-   set := IOBase.set;
-   get := IOBase.get;
-
-   read_line := IOBase.read_line;
-   print_char := IOBase.print_char;
-   print := IOBase.print;
-
-   raise := IOBase.raise;
-   catch := IOBase.catch;
-   timeout := IOBase.timeout
- |}.
-
-End IO.
-
-Module State.
-(** The impredicative encoding of the usual State monad transformer
-    (StateT in Haskell). The impredicative encoding allows to avoid
-    creating blocks (val,state) at each bind. *)
-
-Section Common.
-
- Variables (S:Set) (T₀:Set->Set) (M:Monad T₀).
-
- Definition T (A:Set):= forall R:Set, (A -> S -> T₀ R) -> S -> T₀ R.
-
- Definition F : Monad T := {|
-   ret A x := fun R k s => k x s ;
-   bind A B x f := fun R k s =>
-            x R (fun a s' => f a R k s') s ;
-   ignore A x := fun R k s =>
-            x R (fun _ s' => k tt s') s ;
-   seq A x y := fun R k s =>
-           x R (fun _ s' => y R k s') s;
-   map A B f x := fun R k s => x R (fun a s => k (f a) s) s
- |}.
-
- Definition State : State S T := {|
-   set s := (fun R k _ => k () s) : T unit  ;
-   get := fun R k s => k s s ;
-   modify := fun f R k s => k () (f s)
- |}.
-
- Definition lift {A} (x:T₀ A) : T A := fun R k s =>
-   do M x := x in
-   k x s
- .
-
- Definition run {A} (x:T A) (s:S) : T₀ (A*S) := x _ (fun a s' => ret _ M (a,s')) s.
- Definition reflect {A:Set} (x:S -> T₀ (A*S)) : T A := fun R k s =>
-   do M x' := x s in
-   let '(a,s') := x' in
-   k a s'
- .
-
-
- Variable (L:Logic T₀).
-
- Definition Logic : Logic T := {|
-   zero A e := lift (zero _ L e);
-   plus A x y := fun R k s => plus _ L (x R k s) (fun e => y e R k s)
- |}.
-
- Variable (Env:Set) (E:Environment Env T₀).
-
- Definition Environment : Environment Env T := {|
-   current := lift (current _ _ E)
- |}.
-
- Variable (C:Set) (W:Writer C T₀).
-
- Definition Writer : Writer C T := {|
-   put x := lift (put _ _ W x)
- |}.
-
-End Common.
-
-End State.
-
-
-Module Environment.
-(** The impredicative encoding of the usual environment monad
-    transformer (ReaderT in Haskell). The impredicative encoding
-    allows to avoid using the binding operations of the underlying
-    monad when it isn't explicitly needed. *)
-
-Section Common.
-
- Variable (E:Set) (T₀:Set->Set) (M:Monad T₀).
-
- Definition T (A:Set) := forall (R:Set), (A -> T₀ R)-> E-> T₀ R.
-
- Definition F : Monad T := {|
-   ret A x := fun R k e => k x;
-   bind A B x f := fun R k e => x _ (fun a => f a _ k e) e;
-   ignore A x := fun R k e => x _ (fun _ => k tt) e;
-   seq A x y := fun R k e => x _ (fun _ => y _ k e) e;
-   map A B f x := fun R k e => x _ (fun a => k (f a)) e
- |}.
-
- Definition Environment : Environment E T := {|
-   current := fun R k e => k e 
- |}.
-
-
- Definition lift {A:Set} (x:T₀ A) : T A := fun R k _ =>
-   do M x := x in
-   k x
- .
-
- Definition run {A:Set} (x:T A) (e:E) : T₀ A := x _ (fun a => ret _ M a) e.
- Definition reflect {A:Set} (m:E->T₀ A) : T A := fun R k e =>
-   do M m' := m e in
-   k m'
- .
-
-
- Variable (L:Logic T₀).
-
- Definition Logic : Logic T := {|
-   zero A e := lift (zero _ L e);
-   plus A x y := fun R k e => plus _ L (x _ k e) (fun exc => y exc _ k e)
- |}.
-
- Variable (C:Set) (W:Writer C T₀).
-
- Definition Writer : Writer C T := {|
-   put x := lift (put _ _ W x)
- |}.
-
-End Common.
-
-End Environment.
-
-Module Writer.
-(** The impredicative encoding of the usual "writer" monad
-    transformer (WriterT in Haskell). The impredicative encoding
-    allows to avoid using the binding operations of the underlying
-    monad when it isn't explicitly needed and to avoid constructing
-    and deconstructing values of the form (val,c). *)
-
-Section Common.
-
- Variables (C:Set) (m:Monoid.T C) (T₀:Set->Set) (M:Monad T₀).
-
- Definition T (A:Set) := forall (R:Set), (A->C->T₀ R) -> T₀ R.
-
- Definition F : Monad T := {|
-   ret A x := fun R k => k x (Monoid.zero _ m);
-   bind A B x f := fun R k =>
-     x _ (fun a c => f a _ (fun b c' => k b (Monoid.prod _ m c c')));
-   ignore A x := fun R k => x _ (fun _ c => k tt c);
-   seq A x y := fun R k =>
-     x _ (fun _ c => y _ (fun b c' => k b (Monoid.prod _ m c c')));
-   map A B f x := fun R k => x _ (fun a c => k (f a) c)
- |}.
-
- Definition Writer : Writer C T := {|
-   put c := ((fun R (k:unit->C->T₀ R) => k tt c):T unit)
- |}.
-
- Definition lift {A} (x:T₀ A) : T A := fun R k =>
-   do M x := x in
-   k x (Monoid.zero _ m)
- .
-
- Definition run {A} (x:T A) : T₀ (A*C)%type := x _ (fun a c => ret _ M (a,c)).
- Definition reflect {A:Set} (x:T₀ (A*C)) :T A := fun R k =>
-   do M x := x in
-   let '(a,c) := x in
-   k a c
- .
-
- Variable (L:Logic T₀).
-
- Definition Logic : Logic T := {|
-   zero A e := lift (zero _ L e);
-   plus A x y := fun R k => plus _ L (x _ k) (fun exc => y exc _ k)
- |}.
-
-End Common.
-
-End Writer.
-
-
-Module Logic.
-
-(* Double-continuation backtracking monads are reasonable folklore for
-   "search" implementations (including 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.
-
-   One way to think of the [Logic] functor is to imagine ['a
-   Logic(X).t] to represent list of ['a] with an exception at the
-   bottom (leaving the monad-transforming issues aside, as they don't
-   really work well with lists). Each of the element is a valid
-   result, sequentialising with a [f:'a -> 'b t] is done by applying
-   [f] to each element and then flatten the list, [plus] is
-   concatenation, and [split] is pattern-matching. *)
-
-Section Common.
-
- Variables (T₀:Set->Set) (M:Monad T₀).
-
- Definition FK (R:Set) : Set := Exception -> R.
- Definition SK (A R:Set) : Set := A -> FK R -> R.
- Definition T (A:Set) : Set := forall (R:Set), SK A (T₀ R) -> FK (T₀ R) -> T₀ R.
- (* spiwack: the implementation is an adaptation of the aforementionned
-    "Backtracking, Interleaving, and Terminating Monad Transformers"
-    paper *)
- (* spiwack: [fk] stands for failure continuation, and [sk] for success
-    continuation. *)
-
- Definition F : Monad T := {|
-   ret A x R sk fk := sk x fk;
-   bind A B x k R sk fk :=
-      x _ (fun a fk => k a _ sk fk) fk;
-   ignore A x R sk fk :=
-      x _ (fun _ fk => sk () fk) fk;
-   seq A x k R sk fk :=
-      x _ (fun _ fk => k _ sk fk) fk;
-   map A B f x R sk fk := x _ (fun a fk => sk (f a) fk) fk
- |}.
-
- Definition lift {A} (x:T₀ A) : T A := fun _ sk fk =>
-   do M x := x in
-   sk x fk
- .
-
- Definition _zero {A:Set} (e:Exception) : T A := fun _ _ fk => fk e.
- Definition _plus {A:Set} (x:T A) (y:Exception -> T A) : T A := fun _ sk fk =>
-   x _ sk (fun e => y e _ sk fk)
- .
-
- (* For [reflect] and [split] see the "Backtracking, Interleaving, and
-    Terminating Monad Transformers" paper.  *)
- Definition reflect {A:Set} (x:list_view A (Exception -> T A)) : T A :=
-   match x with
-   | Nil _ _ e => _zero e
-   | Cons _ _ a x => _plus (ret _ F a) x
-   end
- .
- Definition reify {A:Set} (x:T A) : T₀ (list_view A (Exception -> T A)) :=
-   let fk e := ret _ M (Nil _ _ e) in
-   let lift_fk fk e := do F y := lift (fk e) in reflect y in
-   let sk a fk := ret _ M (Cons _ _ a (lift_fk fk)) in
-   x _ sk fk
- .
-
- Definition split {A:Set} (x:T A) : T (list_view A (Exception -> T A)) :=
-   lift (reify x)
- .
-
- Definition Logic : Logic T := {|
-   zero := @_zero;
-   plus := @_plus
- |}.
-
- Variable (Ref:Set->Set) (IO:IO.S Ref T₀).
-
- Definition run {A:Set} (x:T A) : T₀ A :=
-   let sk (a:A) _ : T₀ A := ret _ M a in
-   let fk e : T₀ A := IO.raise _ _ IO (tactic_failure e) in
-   x _ sk fk
- .
-
-End Common.
-
-End Logic.
-
-
-(*** Extraction **)
-
-Parameters (constr types evar_map goal env seffs:Set).
-Extract Inlined Constant constr => "Term.constr".
-Extract Inlined Constant types => "Term.types".
-Extract Inlined Constant evar_map => "Evd.evar_map".
-Extract Inlined Constant goal => "Goal.goal".
-Extract Inlined Constant env => "Environ.env".
-
-Record proofview := {
-  solution : evar_map;
-  comb : list goal
-}.
-
-Definition LogicalState := proofview.
-(** Logical Message: status (safe/unsafe) * ( shelved goals * given up ) *)
-Definition LogicalMessageType := ( bool * ( list goal * list goal ))%type.
-Definition LogicalEnvironment := env.
-Definition LogicalMessage : Monoid.T LogicalMessageType :=
-  Monoid.cart Monoid.BoolAnd (Monoid.cart Monoid.List Monoid.List)
-.
-
-Definition NonLogicalType := IO.T.
-Definition NonLogicalMonad : Monad NonLogicalType := IO.M.
-Definition NonLogicalIO : IO.S IO.Ref NonLogicalType := IO.IO.
-
-Definition LogicType := Logic.T NonLogicalType.
-Definition WriterType := Writer.T LogicalMessageType LogicType.
-Definition EnvironmentType := Environment.T LogicalEnvironment WriterType.
-Definition LogicalType := State.T LogicalState EnvironmentType.
-Definition LogicalMonadBase := Logic.F NonLogicalType.
-Definition LogicalMonadWriter := Writer.F _ LogicalMessage LogicType.
-Definition LogicalMonadEnv := Environment.F LogicalEnvironment WriterType.
-Definition LogicalMonad : Monad LogicalType := State.F LogicalState _.
-Definition LogicalStateM : State LogicalState LogicalType := State.State LogicalState _.
-Definition LogicalReaderE : Environment LogicalEnvironment _ := Environment.Environment LogicalEnvironment WriterType.
-Definition LogicalReader : Environment LogicalEnvironment LogicalType := State.Environment _ _ LogicalMonadEnv _ LogicalReaderE.
-Definition LogicalWriterW : Writer LogicalMessageType  _ := Writer.Writer LogicalMessageType LogicType.
-Definition LogicalWriterE : Writer LogicalMessageType _ := Environment.Writer LogicalEnvironment _ LogicalMonadWriter LogicalMessageType LogicalWriterW.
-Definition LogicalWriter : Writer LogicalMessageType LogicalType := State.Writer _ _ LogicalMonadEnv _ LogicalWriterE.
-Definition LogicalLogic : Logic LogicalType := State.Logic _ _ LogicalMonadEnv (Environment.Logic _ _ LogicalMonadWriter (Writer.Logic _ LogicalMessage _ LogicalMonadBase (Logic.Logic _))).
-
-
-(* The function [split] will be define as the normal form of
-   [split0]. It reifies the monad transformer stack until we can read
-   back a more syntactic form, then reflects the result back. *)
-Definition split0 {a:Set} (x:LogicalType a) : LogicalType (list_view a (Exception -> LogicalType a)) :=
-  State.reflect _ _ LogicalMonadEnv (fun s =>
-  Environment.reflect _ _ LogicalMonadWriter (fun e =>
-  Writer.reflect _ _ LogicalMonadBase (
-    do LogicalMonadBase x' :=
-        Logic.split _ NonLogicalMonad (Writer.run _ _ LogicalMonadBase (Environment.run _ _ LogicalMonadWriter (State.run _ _ LogicalMonadEnv x s) e)) in
-    match x' with
-    | Nil _ _ exc => ret _ LogicalMonadBase ((Nil _ _ exc),s, Monoid.zero _ LogicalMessage)
-    | Cons _ _ (a',s',m') y =>
-      let y' exc :=
-          State.reflect _ _ LogicalMonadEnv (fun _ =>
-          Environment.reflect _ _ LogicalMonadWriter (fun _ =>
-          Writer.reflect _ _ LogicalMonadBase (y exc)))
-      in
-      ret _ LogicalMonadBase (Cons _ _ a' y',s',m')
-    end
-  )))
-.
-
-
-Module NonLogical.
-
- Definition t (a:Set) := Eval compute in NonLogicalType a.
- Definition ref (a:Set) := Eval compute in IO.Ref a.
-
- Definition ret {a:Set} (x:a) : t a := Eval compute in ret _ NonLogicalMonad x.
- Extraction Implicit ret [a].
- Definition bind {a b:Set} (x:t a) (k:a-> t b) : t b := Eval compute in bind _ NonLogicalMonad x k.
- Extraction Implicit bind [a b].
-
- Definition ignore {a:Set} (x:t a) : t unit := Eval compute in ignore _ NonLogicalMonad x.
- Extraction Implicit ignore [a].
- Definition seq {a:Set} (x:t unit) (k:t a) : t a := Eval compute in seq _ NonLogicalMonad x k.
- Extraction Implicit seq [a].
- Definition map {a b:Set} (f:a -> b) (x:t a) : t b := Eval compute in freeze _ (map _ NonLogicalMonad f x).
- Extraction Implicit map [a b].
-
- Definition new_ref {a:Set} (x:a) : t (ref a) := Eval compute in IO.ref _ _ NonLogicalIO x.
- Extraction Implicit new_ref [a].
- Definition set {a:Set} (r:ref a) (x:a) : t unit := Eval compute in IO.set _ _ NonLogicalIO r x.
- Extraction Implicit set [a].
- Definition get {a:Set} (r:ref a) : t a := Eval compute in IO.get _ _ NonLogicalIO r.
- Extraction Implicit get [a].
-
- Definition raise {a:Set} (e:Exception) : t a := Eval compute in IO.raise _ _ NonLogicalIO e.
- Extraction Implicit raise [a].
- Definition catch {a:Set} (s:t a) (h:Exception -> t a) : t a := Eval compute in IO.catch _ _ NonLogicalIO s h.
- Extraction Implicit catch [a].
- Definition timeout {a:Set} n (x:t a) : t a := Eval compute in IO.timeout _ _ NonLogicalIO n x.
- Extraction Implicit timeout [a].
-
- Definition read_line : t String := Eval compute in IO.read_line _ _ NonLogicalIO.
- Definition print_char (c:Char) : t unit := Eval compute in IO.print_char _ _ NonLogicalIO c.
- Definition print (s:Ppcmds) : t unit := Eval compute in IO.print _ _ NonLogicalIO s.
-
- (* /!\ The extracted code for [run] performs effects. /!\ *)
- Parameter run : forall a:Set, t a -> a.
- Extract Constant run => "fun x ->
-  try x () with Proof_errors.Exception e as src ->
-    let src = Errors.push src in
-    let e = Backtrace.app_backtrace ~src ~dst:e in
-    Pervasives.raise e".
- Extraction Implicit run [a].
-
-End NonLogical.
-
-Module Logical.
-
- Definition t (a:Set) := Eval compute in LogicalType a.
-
- Definition ret {a:Set} (x:a) : t a := Eval compute in freeze _ (ret _ LogicalMonad x).
- Extraction Implicit ret [a].
- Definition bind {a b:Set} (x:t a) (k:a-> t b) : t b := Eval compute in freeze _ (bind _ LogicalMonad x k).
- Extraction Implicit bind [a b].
- Definition ignore {a:Set} (x:t a) : t unit := Eval compute in freeze _ (ignore _ LogicalMonad x).
- Extraction Implicit ignore [a].
- Definition seq {a:Set} (x:t unit) (k:t a) : t a := Eval compute in freeze _ (seq _ LogicalMonad x k).
- Extraction Implicit seq [a].
- Definition map {a b:Set} (f:a -> b) (x:t a) : t b := Eval compute in freeze _ (map _ LogicalMonad f x).
- Extraction Implicit map [a b].
-
- Definition set (s:LogicalState) : t unit := Eval compute in freeze _ (set _ _ LogicalStateM s).
- Definition get : t LogicalState := Eval compute in get _ _ LogicalStateM.
- Definition modify (f : LogicalState -> LogicalState) : t unit := Eval compute in freeze _ (modify _ _ LogicalStateM f).
- Definition put (m:LogicalMessageType) : t unit := Eval compute in freeze _ (put _ _ LogicalWriter m).
- Definition current : t LogicalEnvironment := Eval compute in current _ _ LogicalReader.
-
- Definition zero {a:Set} (e:Exception) : t a := Eval compute in freeze _ (zero _ LogicalLogic e).
- Extraction Implicit zero [a].
- Definition plus {a:Set} (x:t a) (y:Exception -> t a) : t a := Eval compute in freeze _ (plus _ LogicalLogic x y).
- Extraction Implicit plus [a].
-
- Definition split {a:Set} (x:t a) : t (list_view a (Exception -> t a)) :=
-   Eval compute in freeze _ (split0 x).
- Extraction Implicit split [a].
- Definition lift {a:Set} (x:NonLogical.t a) : t a := Eval compute in
-  freeze _ (State.lift _ _ LogicalMonadEnv (Environment.lift _ _ LogicalMonadWriter (Writer.lift _ LogicalMessage _ LogicalMonadBase (Logic.lift _ NonLogicalMonad x)))).
- Extraction Implicit lift [a].
-
- Definition run {a:Set} (x:t a) (e:LogicalEnvironment) (s:LogicalState) : NonLogical.t ((a*LogicalState)*LogicalMessageType) := Eval compute in
-  Logic.run _ NonLogicalMonad _ NonLogicalIO (Writer.run _ _ LogicalMonadBase (Environment.run _ _ LogicalMonadWriter (State.run _ _ LogicalMonadEnv x s) e))
- .
- Extraction Implicit run [a].
-
-End Logical.
-
-Set Extraction Flag 1007.
-Set Extraction Conservative Types.
-Set Extraction File Comment "
-This file has been generated by extraction of bootstrap/Monads.v.
-It shouldn't be modified directly. To regenerate it run
-coqtop -batch -impredicative-set -l bootstrap/Monads.v in Coq's source
-directory.
-".
-
-Extraction "proofs/proofview_gen.ml" NonLogical Logical.