Replaced monads.ml by an essentially equivalent proofview_gen.ml generated by extraction.

The goal was to use Coq's partial evaluation capabilities to do manually some
inlining that Ocaml couldn't do. It may be critical as we are defining higher
order combinators in term of others and no inlining means a lot of
unnecessary, short-lived closures built.

With this modification we get back some (but not all) of the loss of performance introduced by threading the monadic type all over the place.
I still have an estimated 15% longer compilation time for Coq.

Makes use of Set Extraction Conservative Types and Set Extraction File Comment
to maintain the relationship between the functions and their types.

Uses an intermediate layer Proofview_monad between Proofview_gen and
Proofview in order to use a hand-written mli to catch potential errors in the
generated file (it uses Extract Constant a lot).

A bug in the extraction of signatures forces to remove the generated
proofview_gen.mli which does not have the correct types.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16981 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 605 insertions, 0 deletions

diff --git a/bootstrap/Monads.v b/bootstrap/Monads.v
new file mode 100644
index 0000000000..26583b0be5
--- /dev/null
+++ b/bootstrap/Monads.v
@@ -0,0 +1,605 @@
+(* -*- coq-prog-args: ("-emacs-U" "-impredicative-set") -*- *)
+
+(* arnaud: on ne doit pas en avoir besoin normalement. *)
+
+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 [
+  "[]"
+  "(::)"
+].
+
+(*** Prod ***)
+Extract Inductive prod => "(*)" [
+  "(,)"
+].
+
+(*** Sum ***)
+Print sum.
+Extract Inductive sum => "Util.union" [
+  "Util.Inl"
+  "Util.Inr"
+].
+
+(*** 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)".
+
+(*** Monoids ***)
+
+Module Monoid.
+
+Record T (M:Set) := {
+  zero : M;
+  prod : M -> M -> M
+}.
+
+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
+}.
+
+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
+}.
+
+(* 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;
+  (** [split x] runs [x] until it either fails with [zero e] or finds
+      a result [a].  In the former case it returns [Inr e], otherwise
+      it returns [Inl (a,y)] where [y] can be run to get more results
+      from [x]. It is a variant of prolog's cut. *)
+  split : forall {A}, T A -> T ((A * (Exception -> T A)) + Exception)%type
+}.
+(** 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
+ |}.
+
+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 () -> a".
+ Extraction Implicit ret [A].
+ Parameter bind : forall A B, T A -> (A->T B) -> T B.
+ Extract Constant bind => "fun a k () -> k (a ()) ()".
+ Extraction Implicit bind [A B].
+ Parameter ignore : forall A, T A -> T unit.
+ Extract Constant ignore => "fun a () -> ignore (a ())".
+ Extraction Implicit ignore [A].
+ Parameter seq : forall A, T unit -> T A -> T A.
+ Extract Constant seq => "fun a k () -> a (); k ()".
+ Extraction Implicit seq [A].
+
+ Parameter ref : forall (A:Set), A -> T (Ref A).
+ Extract Constant ref => "fun a () -> Pervasives.ref a".
+ Extraction Implicit ref [A].
+ Parameter set : forall A, Ref A -> A -> T unit.
+ Extract Constant set => "fun r a () -> Pervasives.(:=) r a".
+ Extraction Implicit set [A].
+ Parameter get : forall A, Ref A -> T A.
+ Extract Constant get => "fun r () -> Pervasives.(!) r".
+ Extraction Implicit get [A].
+
+ Parameter raise : forall A, Exception -> T A.
+ Extract Constant raise => "fun e () -> 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 () -> try s () with Proof_errors.Exception e -> h e ()".
+ Extraction Implicit catch [A].
+
+ Parameter Int : Set.
+ Extract Constant Int => int.
+ Parameter timeout: forall A, Int -> T A -> T A.
+ Extract Constant timeout => "fun n t () ->
+    let timeout_handler _ = Pervasives.raise (Proof_errors.Exception Proof_errors.Timeout) in
+    let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in
+    Pervasives.ignore (Unix.alarm n);
+    let restore_timeout () =
+      Pervasives.ignore (Unix.alarm 0);
+      Sys.set_signal Sys.sigalrm psh
+    in
+    try
+      let res = t () in
+      restore_timeout ();
+      res
+    with
+    | e -> restore_timeout (); Pervasives.raise e
+ ".
+ 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;
+
+   raise : forall {A:Set}, Exception -> T A;
+   catch : forall {A:Set}, T A -> (Exception -> T A) -> T A;
+   timeout : forall {A:Set}, IOBase.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
+ |}.
+
+ Definition IO : S Ref T := {|
+   ref := IOBase.ref;
+   set := IOBase.set;
+   get := IOBase.get;
+
+   raise := IOBase.raise;
+   catch := IOBase.catch;
+   timeout := IOBase.timeout
+ |}.
+
+End IO.
+
+Module State.
+(** State monad transformer, adapted from Haskell' StateT *)
+
+Section Common.
+
+ Variables (S:Set) (T₀:Set->Set) (M:Monad T₀).
+
+ Definition T (A:Set):= S -> T₀ (A*S)%type.
+
+ Definition F : Monad T := {|
+   ret A x s := ret _ M (x,s);
+   bind A B x k s :=
+            do M x := x s in
+            let '(x,s) := x in
+            k x s;
+   ignore A x s :=
+              do M x := x s in
+              let '(_,s) := x in
+              ret _ M ((),s);
+   seq A x k s :=
+           do M x := x s in
+           let '((),s) := x in
+           k s
+ |}.
+
+ Definition State : State S T := {|
+   set := (fun (x s:S) => ret _ M ((),x)) : S -> T unit ;
+   get := fun (s:S) => ret _ M (s,s)
+ |}.
+
+ Definition lift : forall {A}, T₀ A -> T A :=  fun _ x s =>
+   do M x := x in
+   ret _ M (x,s)
+ .
+
+ Definition run : forall {A}, T A -> S -> T₀ (A*S) := fun _ x => x.
+
+ Variable (L:Logic T₀).
+
+
+ Definition Logic : Logic T := {|
+   zero A e := lift (zero _ L e);
+   plus A x y s := plus _ L (x s) (fun e => y e s);
+   split A x s :=
+     do M x := split _ L (x s) in
+     match x return T₀ (((A*(Exception->T A))+Exception)*S) with
+     | inr e => ret _ M (inr e,s)
+     | inl ((a,s),y) =>
+        let y e (_:S) := y e in
+        ret _ M (inl (a,y) , s)
+     end
+ |}.
+
+End Common.
+
+End State.
+
+
+Module Environment.
+(** An environment monad transformer, like Haskell's ReaderT *)
+
+Section Common.
+
+ Variable (E:Set) (T₀:Set->Set) (M:Monad T₀).
+
+ Definition T (A:Set) := E -> T₀ A.
+
+ Definition F : Monad T := {|
+   ret A x e := ret _ M x;
+   bind A B x k e :=
+      do M x := x e in
+      k x e;
+   ignore A x e := ignore _ M (x e);
+   seq A x k e := seq _ M (x e) (k e)
+ |}.
+
+ Definition Environment : Environment E T := {|
+   current e := ret _ M e 
+ |}.
+
+
+ Variable (L:Logic T₀).
+
+
+ Definition Logic : Logic T := {|
+   zero A e env := zero _ L e;
+   plus A x y env := plus _ L (x env) (fun e => y e env);
+   split A x env :=
+     do M x := split _ L (x env) in
+     match x return T₀ ((A*(Exception->T A))+Exception) with
+     | inr e => ret _ M (inr e)
+     | inl (a,y) =>
+        let y e (_:E) := y e in
+        ret _ M (inl (a,y))
+     end
+ |}.
+
+
+ Definition lift {A:Set} (x:T₀ A) : T A := fun _ => x.
+
+ Definition run {A:Set} (x:T A) (e:E) : T₀ A := x e.
+
+End Common.
+
+End Environment.
+
+Module Writer.
+(** A "Writer" monad transformer, that is the canonical monad associated
+    to a monoid. Adaptated from Haskell's WriterT *)
+
+Section Common.
+
+ Variables (C:Set) (m:Monoid.T C) (T₀:Set->Set) (M:Monad T₀).
+
+ Definition T (A:Set) := T₀ (A*C)%type.
+
+ Definition F : Monad T := {|
+   ret A x := ret _ M (x,Monoid.zero _ m);
+   bind A B x k :=
+      do M x := x in
+      let '(x,c) := x in
+      do M y := k x in
+      let '(y,c') := y in
+      ret _ M (y,Monoid.prod _ m c c');
+   ignore A x :=
+      do M x := x in
+      let '(_,c) := x in
+      ret _ M ((),c);
+   seq A x k :=
+      do M x := x in
+      let '((),c) := x in
+      do M y := k  in
+      let '(y,c') := y in
+      ret _ M (y,Monoid.prod _ m c c')
+ |}.
+
+ Definition Writer : Writer C T := {|
+   put := fun (x:C) => ret _ M ((),x) : T unit
+ |}.
+
+ Definition lift {A} (x:T₀ A) : T A :=
+   do M x := x in
+   ret _ M (x, Monoid.zero _ m)
+ .
+
+ Definition run {A} (x:T A) : T₀ (A*C)%type := x.
+
+ Variable (L:Logic T₀).
+
+ Definition Logic : Logic T := {|
+   zero A e := lift (zero _ L e);
+   plus A x y := plus _ L x y;
+   split A x :=
+     do M x := split _ L x in
+     match x return T ((A*(Exception -> T A)) + Exception) with
+     | inr e => ret _ M (inr e, Monoid.zero _ m)
+     | inl ((a,c),y) =>
+         ret _ M (inl (a,y), c)
+    end
+ |}.
+
+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. Chen,
+   D. Fridman.  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. *)
+(* spiwack: I added the primitives from [IO] directly in the [Logic]
+   signature for convenience. It doesn't really make sense, strictly
+   speaking, as they are somewhat deconnected from the semantics of
+   [Logic], but without an appropriate language for composition (some
+   kind of mixins?) I would be going nowhere with a gazillion
+   functors. *)
+
+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
+ |}.
+
+ 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:(A*(Exception -> T A)) + Exception) : T A :=
+   match x with
+   | inr e => _zero e
+   | inl (a,x) => _plus (ret _ F a) x
+   end
+ .
+
+ Definition lower {A:Set} (x:T A) : T₀ ((A*(Exception -> T A)) + Exception) :=
+   let fk e := ret _ M (inr e) in
+   let lift_fk fk e := do F y := lift (fk e) in reflect y in
+   let sk a fk := ret _ M (inl (a, lift_fk fk)) in
+   x _ sk fk
+ .
+
+ Definition Logic : Logic T := {|
+   zero := @_zero;
+   plus := @_plus;
+   split A x := lift (lower x)
+ |}.
+
+ 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 := {
+  initial : list (constr*types);
+  solution : evar_map;
+  comb : list goal
+}.
+
+Definition LogicalState := proofview.
+Definition LogicalMessageType := bool.
+Definition LogicalEnvironment := env.
+Definition LogicalMessage : Monoid.T LogicalMessageType := {|
+  Monoid.zero := true;
+  Monoid.prod x y := andb x y
+|}.
+
+Definition NonLogicalType := IO.T.
+Definition NonLogicalMonad : Monad NonLogicalType := IO.M.
+Definition NonLogicalIO : IO.S IO.Ref NonLogicalType := IO.IO.
+
+Definition LogicalType := Eval compute in State.T LogicalState (Environment.T LogicalEnvironment (Writer.T LogicalMessageType (Logic.T NonLogicalType))).
+Definition LogicalMonadBase := Logic.F NonLogicalType.
+Definition LogicalMonadWriter := Writer.F _ LogicalMessage _ LogicalMonadBase.
+Definition LogicalMonadEnv := Environment.F LogicalEnvironment _ LogicalMonadWriter.
+Definition LogicalMonad : Monad LogicalType := State.F LogicalState _ LogicalMonadEnv.
+Definition LogicalStateM : State LogicalState LogicalType := State.State LogicalState _ LogicalMonadEnv.
+Definition LogicalReader : Environment LogicalEnvironment _ := Environment.Environment LogicalEnvironment _ LogicalMonadWriter.
+Definition LogicalWriter : Writer LogicalMessageType  _ := Writer.Writer LogicalMessageType _ (Logic.F NonLogicalType).
+Definition LogicalLogic : Logic LogicalType := State.Logic _ _ LogicalMonadEnv (Environment.Logic _ _ LogicalMonadWriter (Writer.Logic _ LogicalMessage _ LogicalMonadBase (Logic.Logic _ NonLogicalMonad))).
+
+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 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].
+
+ (* /!\ 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 -> 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 ret _ LogicalMonad x.
+ Extraction Implicit ret [a].
+ Definition bind {a b:Set} (x:t a) (k:a-> t b) : t b := Eval compute in bind _ LogicalMonad x k.
+ Extraction Implicit bind [a b].
+ Definition ignore {a:Set} (x:t a) : t unit := Eval compute in ignore _ LogicalMonad x.
+ Extraction Implicit ignore [a].
+ Definition seq {a:Set} (x:t unit) (k:t a) : t a := Eval compute in seq _ LogicalMonad x k.
+ Extraction Implicit seq [a].
+
+ Definition set (s:LogicalState) : t unit := Eval compute in set _ _ LogicalStateM s.
+ Definition get : t LogicalState := Eval compute in get _ _ LogicalStateM.
+ Print Environment.lift.
+ Definition put (m:LogicalMessageType) : t unit := Eval compute in State.lift _ _ LogicalMonadEnv (Environment.lift _ _ (put _ _ LogicalWriter m)).
+ Definition current : t LogicalEnvironment := Eval compute in State.lift _ _ LogicalMonadEnv (current _ _ LogicalReader).
+
+ Definition zero {a:Set} (e:Exception) : t a := Eval compute in zero _ LogicalLogic e.
+ Extraction Implicit zero [a].
+ Definition plus {a:Set} (x:t a) (y:Exception -> t a) : t a := Eval compute in plus _ LogicalLogic x y.
+ Extraction Implicit plus [a].
+ Definition split {a:Set} (x:t a) : t ((a*(Exception -> t a))+Exception) := Eval compute in split _ LogicalLogic x.
+ Extraction Implicit split [a].
+ Definition lift {a:Set} (x:NonLogical.t a) : t a := Eval compute in
+  State.lift _ _ LogicalMonadEnv (Environment.lift _ _ (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 _ _ (Environment.run _ _ (State.run _ _ x s) e))
+ .
+ Extraction Implicit run [a].
+
+End Logical.
+
+
+Set Extraction Conservative Types.
+Set Extraction File Comment "
+This file has been generated by extraction of bootstrap/Monad.v.
+It shouldn't be modified directly. To regenerate it run
+coqtop -batch -impredicative-set bootstrap/Monad.v in Coq's source
+directory.
+".
+
+Extraction "proofs/proofview_gen.ml" NonLogical Logical.