aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--bootstrap/Monads.v58
-rw-r--r--proofs/proofview_gen.ml309
2 files changed, 235 insertions, 132 deletions
diff --git a/bootstrap/Monads.v b/bootstrap/Monads.v
index 2b09497914..b8036b8787 100644
--- a/bootstrap/Monads.v
+++ b/bootstrap/Monads.v
@@ -326,39 +326,46 @@ End State.
Module Environment.
-(** An environment monad transformer, like Haskell's ReaderT *)
+(** 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) := E -> T₀ A.
+ Definition T (A:Set) := forall (R:Set), (A -> T₀ R)-> E-> T₀ R.
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)
+ 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
|}.
Definition Environment : Environment E T := {|
- current e := ret _ M e
+ current := fun R k e => k e
|}.
- Definition lift {A:Set} (x:T₀ A) : T A := fun _ => x.
+ 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 e.
- Definition reflect {A:Set} (m:E->T₀ A) : T A := m.
+ 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 env := zero _ L e;
- plus A x y env := plus _ L (x env) (fun e => y e env)
+ 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₀).
@@ -552,18 +559,21 @@ Definition NonLogicalType := IO.T.
Definition NonLogicalMonad : Monad NonLogicalType := IO.M.
Definition NonLogicalIO : IO.S IO.Ref NonLogicalType := IO.IO.
-Definition LogicalType := State.T LogicalState (Environment.T LogicalEnvironment (Writer.T LogicalMessageType (Logic.T NonLogicalType))).
+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 _ LogicalMonadBase.
-Definition LogicalMonadEnv := Environment.F LogicalEnvironment _ LogicalMonadWriter.
+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 _ LogicalMonadWriter.
+Definition LogicalReaderE : Environment LogicalEnvironment _ := Environment.Environment LogicalEnvironment WriterType.
Definition LogicalReader : Environment LogicalEnvironment LogicalType := State.Environment _ _ LogicalMonadEnv _ LogicalReaderE.
Definition LogicalWriterW : Writer LogicalMessageType _ := Writer.Writer LogicalMessageType _ (Logic.F NonLogicalType).
-Definition LogicalWriterE : Writer LogicalMessageType _ := Environment.Writer LogicalEnvironment _ LogicalMessageType LogicalWriterW.
+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 _ _ (Writer.Logic _ LogicalMessage _ LogicalMonadBase (Logic.Logic _))).
+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
@@ -571,16 +581,16 @@ Definition LogicalLogic : Logic LogicalType := State.Logic _ _ LogicalMonadEnv (
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 _ _ (fun e =>
+ Environment.reflect _ _ LogicalMonadWriter (fun e =>
Writer.reflect _ _ (
do LogicalMonadBase x' :=
- Logic.split _ NonLogicalMonad (Writer.run _ _ (Environment.run _ _ (State.run _ _ LogicalMonadEnv x s) e)) in
+ Logic.split _ NonLogicalMonad (Writer.run _ _ (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 _ _ (fun _ =>
+ Environment.reflect _ _ LogicalMonadWriter (fun _ =>
Writer.reflect _ _ (y exc)))
in
ret _ LogicalMonadBase (Cons _ _ a' y',s',m')
@@ -669,11 +679,11 @@ split _ LogicalLogic x).
*)
Extraction Implicit split [a].
Definition lift {a:Set} (x:NonLogical.t a) : t a := Eval compute in
- freeze _ (State.lift _ _ LogicalMonadEnv (Environment.lift _ _ (Writer.lift _ LogicalMessage _ LogicalMonadBase (Logic.lift _ NonLogicalMonad x)))).
+ 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 _ _ (Environment.run _ _ (State.run _ _ LogicalMonadEnv x s) e))
+ Logic.run _ NonLogicalMonad _ NonLogicalIO (Writer.run _ _ (Environment.run _ _ LogicalMonadWriter (State.run _ _ LogicalMonadEnv x s) e))
.
Extraction Implicit run [a].
diff --git a/proofs/proofview_gen.ml b/proofs/proofview_gen.ml
index d168188de7..1609df5280 100644
--- a/proofs/proofview_gen.ml
+++ b/proofs/proofview_gen.ml
@@ -186,40 +186,60 @@ module NonLogical =
module Logical =
struct
type 'a t =
- __ -> ('a -> proofview -> Environ.env ->
- __ -> ((__*bool) -> (exn -> __
+ __ -> ('a -> proofview -> __ -> (__ -> __
+ -> ((__*bool) -> (exn -> __ IOBase.coq_T)
+ -> __ IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ Environ.env -> __ -> ((__*bool) -> (exn
+ -> __ IOBase.coq_T) -> __ IOBase.coq_T)
+ -> (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> proofview -> __ -> (__
+ -> __ -> ((__*bool) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) -> (exn
-> __ IOBase.coq_T) -> __ IOBase.coq_T)
- -> proofview -> Environ.env -> __ ->
- ((__*bool) -> (exn -> __ IOBase.coq_T) ->
- __ IOBase.coq_T) -> (exn -> __
- IOBase.coq_T) -> __ IOBase.coq_T
+ -> Environ.env -> __ -> ((__*bool) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> (exn -> __ IOBase.coq_T)
+ -> __ IOBase.coq_T
(** val ret :
- 'a1 -> __ -> ('a1 -> proofview ->
- Environ.env -> __ -> (('a2*bool) ->
+ 'a1 -> __ -> ('a1 -> proofview -> __ ->
+ ('a2 -> __ -> ((__*bool) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
(exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> Environ.env -> __ ->
+ ((__*bool) -> (exn -> __ IOBase.coq_T)
+ -> __ IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
- proofview -> Environ.env -> __ ->
- (('a2*bool) -> (exn -> 'a3
- IOBase.coq_T) -> 'a3 IOBase.coq_T) ->
- (exn -> 'a3 IOBase.coq_T) -> 'a3
- IOBase.coq_T **)
+ proofview -> __ -> ('a2 -> __ ->
+ (('a3*bool) -> (exn -> __ IOBase.coq_T)
+ -> __ IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ Environ.env -> __ -> (('a3*bool) ->
+ (exn -> 'a4 IOBase.coq_T) -> 'a4
+ IOBase.coq_T) -> (exn -> 'a4
+ IOBase.coq_T) -> 'a4 IOBase.coq_T **)
let ret x =
(); (fun _ k s -> Obj.magic k x s)
(** val bind :
'a1 t -> ('a1 -> 'a2 t) -> __ -> ('a2
- -> proofview -> Environ.env -> __ ->
- (('a3*bool) -> (exn -> __ IOBase.coq_T)
+ -> proofview -> __ -> ('a3 -> __ ->
+ ((__*bool) -> (exn -> __ IOBase.coq_T)
-> __ IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
- proofview -> Environ.env -> __ ->
- (('a3*bool) -> (exn -> 'a4
- IOBase.coq_T) -> 'a4 IOBase.coq_T) ->
- (exn -> 'a4 IOBase.coq_T) -> 'a4
+ Environ.env -> __ -> ((__*bool) -> (exn
+ -> __ IOBase.coq_T) -> __ IOBase.coq_T)
+ -> (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> proofview -> __ ->
+ ('a3 -> __ -> (('a4*bool) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> Environ.env -> __ ->
+ (('a4*bool) -> (exn -> 'a5
+ IOBase.coq_T) -> 'a5 IOBase.coq_T) ->
+ (exn -> 'a5 IOBase.coq_T) -> 'a5
IOBase.coq_T **)
let bind x k =
@@ -228,16 +248,22 @@ module Logical =
Obj.magic k a __ k0 s') s)
(** val ignore :
- 'a1 t -> __ -> (unit -> proofview ->
- Environ.env -> __ -> (('a2*bool) ->
+ 'a1 t -> __ -> (unit -> proofview -> __
+ -> ('a2 -> __ -> ((__*bool) -> (exn ->
+ __ IOBase.coq_T) -> __ IOBase.coq_T) ->
(exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> Environ.env -> __ ->
+ ((__*bool) -> (exn -> __ IOBase.coq_T)
+ -> __ IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
- proofview -> Environ.env -> __ ->
- (('a2*bool) -> (exn -> 'a3
- IOBase.coq_T) -> 'a3 IOBase.coq_T) ->
- (exn -> 'a3 IOBase.coq_T) -> 'a3
- IOBase.coq_T **)
+ proofview -> __ -> ('a2 -> __ ->
+ (('a3*bool) -> (exn -> __ IOBase.coq_T)
+ -> __ IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ Environ.env -> __ -> (('a3*bool) ->
+ (exn -> 'a4 IOBase.coq_T) -> 'a4
+ IOBase.coq_T) -> (exn -> 'a4
+ IOBase.coq_T) -> 'a4 IOBase.coq_T **)
let ignore x =
(); (fun _ k s ->
@@ -245,14 +271,21 @@ module Logical =
(** val seq :
unit t -> 'a1 t -> __ -> ('a1 ->
- proofview -> Environ.env -> __ ->
- (('a2*bool) -> (exn -> __ IOBase.coq_T)
+ proofview -> __ -> ('a2 -> __ ->
+ ((__*bool) -> (exn -> __ IOBase.coq_T)
-> __ IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
- proofview -> Environ.env -> __ ->
- (('a2*bool) -> (exn -> 'a3
- IOBase.coq_T) -> 'a3 IOBase.coq_T) ->
- (exn -> 'a3 IOBase.coq_T) -> 'a3
+ Environ.env -> __ -> ((__*bool) -> (exn
+ -> __ IOBase.coq_T) -> __ IOBase.coq_T)
+ -> (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> proofview -> __ ->
+ ('a2 -> __ -> (('a3*bool) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> Environ.env -> __ ->
+ (('a3*bool) -> (exn -> 'a4
+ IOBase.coq_T) -> 'a4 IOBase.coq_T) ->
+ (exn -> 'a4 IOBase.coq_T) -> 'a4
IOBase.coq_T **)
let seq x k =
@@ -262,119 +295,168 @@ module Logical =
(** val set :
logicalState -> __ -> (unit ->
- proofview -> Environ.env -> __ ->
- (('a1*bool) -> (exn -> __ IOBase.coq_T)
+ proofview -> __ -> ('a1 -> __ ->
+ ((__*bool) -> (exn -> __ IOBase.coq_T)
-> __ IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
- proofview -> Environ.env -> __ ->
- (('a1*bool) -> (exn -> 'a2
- IOBase.coq_T) -> 'a2 IOBase.coq_T) ->
- (exn -> 'a2 IOBase.coq_T) -> 'a2
+ Environ.env -> __ -> ((__*bool) -> (exn
+ -> __ IOBase.coq_T) -> __ IOBase.coq_T)
+ -> (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> proofview -> __ ->
+ ('a1 -> __ -> (('a2*bool) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> Environ.env -> __ ->
+ (('a2*bool) -> (exn -> 'a3
+ IOBase.coq_T) -> 'a3 IOBase.coq_T) ->
+ (exn -> 'a3 IOBase.coq_T) -> 'a3
IOBase.coq_T **)
let set s =
(); (fun _ k x -> Obj.magic k () s)
(** val get :
- __ -> (logicalState -> proofview ->
- Environ.env -> __ -> (('a1*bool) ->
+ __ -> (logicalState -> proofview -> __
+ -> ('a1 -> __ -> ((__*bool) -> (exn ->
+ __ IOBase.coq_T) -> __ IOBase.coq_T) ->
(exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> Environ.env -> __ ->
+ ((__*bool) -> (exn -> __ IOBase.coq_T)
+ -> __ IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
- proofview -> Environ.env -> __ ->
- (('a1*bool) -> (exn -> 'a2
- IOBase.coq_T) -> 'a2 IOBase.coq_T) ->
- (exn -> 'a2 IOBase.coq_T) -> 'a2
- IOBase.coq_T **)
+ proofview -> __ -> ('a1 -> __ ->
+ (('a2*bool) -> (exn -> __ IOBase.coq_T)
+ -> __ IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ Environ.env -> __ -> (('a2*bool) ->
+ (exn -> 'a3 IOBase.coq_T) -> 'a3
+ IOBase.coq_T) -> (exn -> 'a3
+ IOBase.coq_T) -> 'a3 IOBase.coq_T **)
let get r k s =
Obj.magic k s s
(** val put :
logicalMessageType -> __ -> (unit ->
- proofview -> Environ.env -> __ ->
- (('a1*bool) -> (exn -> __ IOBase.coq_T)
+ proofview -> __ -> ('a1 -> __ ->
+ ((__*bool) -> (exn -> __ IOBase.coq_T)
-> __ IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
- proofview -> Environ.env -> __ ->
- (('a1*bool) -> (exn -> 'a2
- IOBase.coq_T) -> 'a2 IOBase.coq_T) ->
- (exn -> 'a2 IOBase.coq_T) -> 'a2
+ Environ.env -> __ -> ((__*bool) -> (exn
+ -> __ IOBase.coq_T) -> __ IOBase.coq_T)
+ -> (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> proofview -> __ ->
+ ('a1 -> __ -> (('a2*bool) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> Environ.env -> __ ->
+ (('a2*bool) -> (exn -> 'a3
+ IOBase.coq_T) -> 'a3 IOBase.coq_T) ->
+ (exn -> 'a3 IOBase.coq_T) -> 'a3
IOBase.coq_T **)
let put m =
- (); (fun _ k s e _ sk fk ->
- Obj.magic k () s e __ (fun a fk0 ->
+ (); (fun _ k s _ k0 e _ sk fk ->
+ Obj.magic k () s __ k0 e __
+ (fun a fk0 ->
let y,c' = a in
sk (y,(if m then c' else false)) fk0)
fk)
(** val current :
__ -> (logicalEnvironment -> proofview
- -> Environ.env -> __ -> (('a1*bool) ->
+ -> __ -> ('a1 -> __ -> ((__*bool) ->
(exn -> __ IOBase.coq_T) -> __
IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
- proofview -> Environ.env -> __ ->
- (('a1*bool) -> (exn -> 'a2
- IOBase.coq_T) -> 'a2 IOBase.coq_T) ->
- (exn -> 'a2 IOBase.coq_T) -> 'a2
+ Environ.env -> __ -> ((__*bool) -> (exn
+ -> __ IOBase.coq_T) -> __ IOBase.coq_T)
+ -> (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> proofview -> __ ->
+ ('a1 -> __ -> (('a2*bool) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> Environ.env -> __ ->
+ (('a2*bool) -> (exn -> 'a3
+ IOBase.coq_T) -> 'a3 IOBase.coq_T) ->
+ (exn -> 'a3 IOBase.coq_T) -> 'a3
IOBase.coq_T **)
- let current r k s e r0 sk fk =
- Obj.magic k e s e __ (fun a fk0 ->
- let y,c' = a in sk (y,c') fk0) fk
+ let current r k s r0 k0 e =
+ Obj.magic k e s __ k0 e
(** val zero :
- exn -> __ -> ('a1 -> proofview ->
- Environ.env -> __ -> (('a2*bool) ->
+ exn -> __ -> ('a1 -> proofview -> __ ->
+ ('a2 -> __ -> ((__*bool) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
(exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> Environ.env -> __ ->
+ ((__*bool) -> (exn -> __ IOBase.coq_T)
+ -> __ IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
- proofview -> Environ.env -> __ ->
- (('a2*bool) -> (exn -> 'a3
- IOBase.coq_T) -> 'a3 IOBase.coq_T) ->
- (exn -> 'a3 IOBase.coq_T) -> 'a3
- IOBase.coq_T **)
+ proofview -> __ -> ('a2 -> __ ->
+ (('a3*bool) -> (exn -> __ IOBase.coq_T)
+ -> __ IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ Environ.env -> __ -> (('a3*bool) ->
+ (exn -> 'a4 IOBase.coq_T) -> 'a4
+ IOBase.coq_T) -> (exn -> 'a4
+ IOBase.coq_T) -> 'a4 IOBase.coq_T **)
let zero e =
- (); (fun _ k s e0 _ sk fk -> fk e)
+ (); (fun _ k s _ k0 e0 _ sk fk -> fk e)
(** val plus :
'a1 t -> (exn -> 'a1 t) -> __ -> ('a1
- -> proofview -> Environ.env -> __ ->
- (('a2*bool) -> (exn -> __ IOBase.coq_T)
+ -> proofview -> __ -> ('a2 -> __ ->
+ ((__*bool) -> (exn -> __ IOBase.coq_T)
-> __ IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
- proofview -> Environ.env -> __ ->
- (('a2*bool) -> (exn -> 'a3
- IOBase.coq_T) -> 'a3 IOBase.coq_T) ->
- (exn -> 'a3 IOBase.coq_T) -> 'a3
+ Environ.env -> __ -> ((__*bool) -> (exn
+ -> __ IOBase.coq_T) -> __ IOBase.coq_T)
+ -> (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> proofview -> __ ->
+ ('a2 -> __ -> (('a3*bool) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> Environ.env -> __ ->
+ (('a3*bool) -> (exn -> 'a4
+ IOBase.coq_T) -> 'a4 IOBase.coq_T) ->
+ (exn -> 'a4 IOBase.coq_T) -> 'a4
IOBase.coq_T **)
let plus x y =
- (); (fun _ k s env _ sk fk ->
- Obj.magic x __ k s env __ sk (fun e ->
- Obj.magic y e __ k s env __ sk fk))
+ (); (fun _ k s _ k0 e _ sk fk ->
+ Obj.magic x __ k s __ k0 e __ sk
+ (fun e0 ->
+ Obj.magic y e0 __ k s __ k0 e __ sk
+ fk))
(** val split :
'a1 t -> __ -> (('a1, exn -> 'a1 t)
- list_view -> proofview -> Environ.env
- -> __ -> (('a2*bool) -> (exn -> __
+ list_view -> proofview -> __ -> ('a2 ->
+ __ -> ((__*bool) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
(exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> proofview ->
- Environ.env -> __ -> (('a2*bool) ->
- (exn -> 'a3 IOBase.coq_T) -> 'a3
- IOBase.coq_T) -> (exn -> 'a3
- IOBase.coq_T) -> 'a3 IOBase.coq_T **)
+ IOBase.coq_T) -> Environ.env -> __ ->
+ ((__*bool) -> (exn -> __ IOBase.coq_T)
+ -> __ IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ proofview -> __ -> ('a2 -> __ ->
+ (('a3*bool) -> (exn -> __ IOBase.coq_T)
+ -> __ IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ Environ.env -> __ -> (('a3*bool) ->
+ (exn -> 'a4 IOBase.coq_T) -> 'a4
+ IOBase.coq_T) -> (exn -> 'a4
+ IOBase.coq_T) -> 'a4 IOBase.coq_T **)
let split x =
- (); (fun _ k s e _ sk fk ->
+ (); (fun _ k s _ k0 e _ sk fk ->
IOBase.bind
- (Obj.magic x __
- (fun a s' e0 _ sk0 fk0 ->
- sk0 ((a,s'),true) fk0) s e __
+ (Obj.magic x __ (fun a s' _ k1 e0 ->
+ k1 (a,s')) s __ (fun a _ sk0 fk0 ->
+ sk0 (a,true) fk0) e __
(fun a fk0 ->
IOBase.ret (Cons (a,
(fun e0 _ sk0 fk1 ->
@@ -388,24 +470,26 @@ module Logical =
(fun x0 ->
match x0 with
| Nil exc ->
- Obj.magic k (Nil exc) s e __
+ Obj.magic k (Nil exc) s __ k0 e __
(fun a fk0 ->
let y,c' = a in sk (y,c') fk0) fk
| Cons (p, y) ->
let p0,m' = p in
let a',s' = p0 in
Obj.magic k (Cons (a',
- (fun exc _ k0 s0 e0 _ sk0 fk0 ->
+ (fun exc _ k1 s0 _ k2 e0 _ sk0 fk0 ->
y exc __ (fun a fk1 ->
let x1,c = a in
let a0,s'0 = x1 in
- k0 a0 s'0 e0 __ (fun a1 fk2 ->
+ k1 a0 s'0 __ k2 e0 __
+ (fun a1 fk2 ->
let y0,c' = a1 in
sk0
(y0,(if c
then c'
else false)) fk2) fk1)
- fk0))) s' e __ (fun a fk0 ->
+ fk0))) s' __ k0 e __
+ (fun a fk0 ->
let y0,c' = a in
sk
(y0,(if m' then c' else false))
@@ -413,20 +497,28 @@ module Logical =
(** val lift :
'a1 NonLogical.t -> __ -> ('a1 ->
- proofview -> Environ.env -> __ ->
- (('a2*bool) -> (exn -> __ IOBase.coq_T)
+ proofview -> __ -> ('a2 -> __ ->
+ ((__*bool) -> (exn -> __ IOBase.coq_T)
-> __ IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
- proofview -> Environ.env -> __ ->
- (('a2*bool) -> (exn -> 'a3
- IOBase.coq_T) -> 'a3 IOBase.coq_T) ->
- (exn -> 'a3 IOBase.coq_T) -> 'a3
+ Environ.env -> __ -> ((__*bool) -> (exn
+ -> __ IOBase.coq_T) -> __ IOBase.coq_T)
+ -> (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> proofview -> __ ->
+ ('a2 -> __ -> (('a3*bool) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> Environ.env -> __ ->
+ (('a3*bool) -> (exn -> 'a4
+ IOBase.coq_T) -> 'a4 IOBase.coq_T) ->
+ (exn -> 'a4 IOBase.coq_T) -> 'a4
IOBase.coq_T **)
let lift x =
- (); (fun _ k s e _ sk fk ->
+ (); (fun _ k s _ k0 e _ sk fk ->
IOBase.bind x (fun x0 ->
- Obj.magic k x0 s e __ (fun a fk0 ->
+ Obj.magic k x0 s __ k0 e __
+ (fun a fk0 ->
let y,c' = a in sk (y,c') fk0) fk))
(** val run :
@@ -436,9 +528,10 @@ module Logical =
NonLogical.t **)
let run x e s =
- Obj.magic x __ (fun a s' e0 _ sk fk ->
- sk ((a,s'),true) fk) s e __
- (fun a x0 -> IOBase.ret a) (fun e0 ->
+ Obj.magic x __ (fun a s' _ k e0 ->
+ k (a,s')) s __ (fun a _ sk fk ->
+ sk (a,true) fk) e __ (fun a x0 ->
+ IOBase.ret a) (fun e0 ->
IOBase.raise
((fun e -> Proof_errors.TacticFailure e)
e0))
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:11:50 +0000