aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--bootstrap/Monads.v60
-rw-r--r--proofs/proofview_gen.ml552
2 files changed, 387 insertions, 225 deletions
diff --git a/bootstrap/Monads.v b/bootstrap/Monads.v
index b8036b8787..ddfdaecbf3 100644
--- a/bootstrap/Monads.v
+++ b/bootstrap/Monads.v
@@ -379,52 +379,48 @@ End Common.
End Environment.
Module Writer.
-(** A "Writer" monad transformer, that is the canonical monad associated
- to a monoid. Adaptated from Haskell's WriterT *)
+(** 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) := T₀ (A*C)%type.
+ Definition T (A:Set) := forall (R:Set), (A->C->T₀ R) -> T₀ R.
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')
+ 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')))
|}.
Definition Writer : Writer C T := {|
- put := fun (x:C) => ret _ M ((),x) : T unit
+ put c := ((fun R (k:unit->C->T₀ R) => k tt c):T unit)
|}.
- Definition lift {A} (x:T₀ A) : T A :=
+ Definition lift {A} (x:T₀ A) : T A := fun R k =>
do M x := x in
- ret _ M (x, Monoid.zero _ m)
+ k x (Monoid.zero _ m)
.
- Definition run {A} (x:T A) : T₀ (A*C)%type := x.
- Definition reflect {A:Set} (x:T₀ (A*C)) := x.
+ 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 := plus _ L x y
+ plus A x y := fun R k => plus _ L (x _ k) (fun exc => y exc _ k)
|}.
End Common.
@@ -564,13 +560,13 @@ 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 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 _ (Logic.F NonLogicalType).
+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 _))).
@@ -582,16 +578,16 @@ Definition LogicalLogic : Logic LogicalType := State.Logic _ _ LogicalMonadEnv (
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 _ _ (
+ Writer.reflect _ _ LogicalMonadBase (
do LogicalMonadBase x' :=
- Logic.split _ NonLogicalMonad (Writer.run _ _ (Environment.run _ _ LogicalMonadWriter (State.run _ _ LogicalMonadEnv x s) e)) in
+ 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 _ _ (y exc)))
+ Writer.reflect _ _ LogicalMonadBase (y exc)))
in
ret _ LogicalMonadBase (Cons _ _ a' y',s',m')
end
@@ -683,7 +679,7 @@ split _ LogicalLogic 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 _ _ LogicalMonadWriter (State.run _ _ LogicalMonadEnv x s) e))
+ Logic.run _ NonLogicalMonad _ NonLogicalIO (Writer.run _ _ LogicalMonadBase (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 1609df5280..0f9d38775b 100644
--- a/proofs/proofview_gen.ml
+++ b/proofs/proofview_gen.ml
@@ -187,60 +187,99 @@ module Logical =
struct
type 'a t =
__ -> ('a -> proofview -> __ -> (__ -> __
- -> ((__*bool) -> (exn -> __ IOBase.coq_T)
+ -> (__ -> bool -> __ -> (__ -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn
+ -> __ IOBase.coq_T) -> __ IOBase.coq_T)
+ -> __ -> (__ -> (exn -> __ IOBase.coq_T)
-> __ IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
- Environ.env -> __ -> ((__*bool) -> (exn
+ Environ.env -> __ -> (__ -> bool -> __ ->
+ (__ -> (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> (exn -> __ IOBase.coq_T)
+ -> __ IOBase.coq_T) -> __ -> (__ -> (exn
-> __ IOBase.coq_T) -> __ IOBase.coq_T)
-> (exn -> __ IOBase.coq_T) -> __
IOBase.coq_T) -> proofview -> __ -> (__
- -> __ -> ((__*bool) -> (exn -> __
+ -> __ -> (__ -> bool -> __ -> (__ -> (exn
+ -> __ IOBase.coq_T) -> __ IOBase.coq_T)
+ -> (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> __ -> (__ -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) -> (exn
-> __ IOBase.coq_T) -> __ IOBase.coq_T)
- -> Environ.env -> __ -> ((__*bool) ->
- (exn -> __ IOBase.coq_T) -> __
+ -> Environ.env -> __ -> (__ -> bool -> __
+ -> (__ -> (exn -> __ IOBase.coq_T) -> __
IOBase.coq_T) -> (exn -> __ IOBase.coq_T)
- -> __ IOBase.coq_T
+ -> __ IOBase.coq_T) -> __ -> (__ -> (exn
+ -> __ IOBase.coq_T) -> __ IOBase.coq_T)
+ -> (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T
(** val ret :
'a1 -> __ -> ('a1 -> proofview -> __ ->
- ('a2 -> __ -> ((__*bool) -> (exn -> __
+ ('a2 -> __ -> (__ -> bool -> __ -> (__
+ -> (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) -> __
+ -> (__ -> (exn -> __ IOBase.coq_T) ->
+ __ IOBase.coq_T) -> (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 -> __
+ Environ.env -> __ -> (__ -> bool -> __
+ -> (__ -> (exn -> __ IOBase.coq_T) ->
+ __ IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) -> __
+ -> (__ -> (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 -> __
+ proofview -> __ -> ('a2 -> __ -> ('a3
+ -> bool -> __ -> (__ -> (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 **)
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> __ -> (__ -> (exn ->
+ __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> Environ.env -> __ ->
+ ('a3 -> bool -> __ -> ('a4 -> (exn ->
+ __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> __ -> ('a4 -> (exn ->
+ 'a5 IOBase.coq_T) -> 'a5 IOBase.coq_T)
+ -> (exn -> 'a5 IOBase.coq_T) -> 'a5
+ IOBase.coq_T **)
let ret x =
(); (fun _ k s -> Obj.magic k x s)
(** val bind :
'a1 t -> ('a1 -> 'a2 t) -> __ -> ('a2
- -> proofview -> __ -> ('a3 -> __ ->
- ((__*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 -> __ ->
- ('a3 -> __ -> (('a4*bool) -> (exn -> __
+ -> proofview -> __ -> ('a3 -> __ -> (__
+ -> bool -> __ -> (__ -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
(exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> __ -> (__ -> (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 **)
+ (__ -> bool -> __ -> (__ -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> __ -> (__ -> (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) -> __
+ -> (__ -> (exn -> __ IOBase.coq_T) ->
+ __ IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ Environ.env -> __ -> ('a4 -> bool -> __
+ -> ('a5 -> (exn -> __ IOBase.coq_T) ->
+ __ IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) -> __
+ -> ('a5 -> (exn -> 'a6 IOBase.coq_T) ->
+ 'a6 IOBase.coq_T) -> (exn -> 'a6
+ IOBase.coq_T) -> 'a6 IOBase.coq_T **)
let bind x k =
(); (fun _ k0 s ->
@@ -249,21 +288,35 @@ module Logical =
(** val ignore :
'a1 t -> __ -> (unit -> proofview -> __
- -> ('a2 -> __ -> ((__*bool) -> (exn ->
+ -> ('a2 -> __ -> (__ -> bool -> __ ->
+ (__ -> (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) -> __
+ -> (__ -> (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) -> __
+ -> (__ -> (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) -> __ -> (__ -> (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 -> __ -> ('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 **)
+ ('a3 -> bool -> __ -> ('a4 -> (exn ->
+ __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> __ -> ('a4 -> (exn ->
+ 'a5 IOBase.coq_T) -> 'a5 IOBase.coq_T)
+ -> (exn -> 'a5 IOBase.coq_T) -> 'a5
+ IOBase.coq_T **)
let ignore x =
(); (fun _ k s ->
@@ -271,22 +324,35 @@ module Logical =
(** val seq :
unit t -> 'a1 t -> __ -> ('a1 ->
- proofview -> __ -> ('a2 -> __ ->
- ((__*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 -> __ ->
- ('a2 -> __ -> (('a3*bool) -> (exn -> __
+ proofview -> __ -> ('a2 -> __ -> (__ ->
+ bool -> __ -> (__ -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
(exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> __ -> (__ -> (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 **)
+ (__ -> bool -> __ -> (__ -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> __ -> (__ -> (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) -> __
+ -> (__ -> (exn -> __ IOBase.coq_T) ->
+ __ IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ Environ.env -> __ -> ('a3 -> bool -> __
+ -> ('a4 -> (exn -> __ IOBase.coq_T) ->
+ __ IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) -> __
+ -> ('a4 -> (exn -> 'a5 IOBase.coq_T) ->
+ 'a5 IOBase.coq_T) -> (exn -> 'a5
+ IOBase.coq_T) -> 'a5 IOBase.coq_T **)
let seq x k =
(); (fun _ k0 s ->
@@ -295,91 +361,142 @@ module Logical =
(** val set :
logicalState -> __ -> (unit ->
- proofview -> __ -> ('a1 -> __ ->
- ((__*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 -> __ ->
- ('a1 -> __ -> (('a2*bool) -> (exn -> __
+ proofview -> __ -> ('a1 -> __ -> (__ ->
+ bool -> __ -> (__ -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
(exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> __ -> (__ -> (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 **)
+ (__ -> bool -> __ -> (__ -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> __ -> (__ -> (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) -> __
+ -> (__ -> (exn -> __ IOBase.coq_T) ->
+ __ IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ Environ.env -> __ -> ('a2 -> bool -> __
+ -> ('a3 -> (exn -> __ IOBase.coq_T) ->
+ __ IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) -> __
+ -> ('a3 -> (exn -> 'a4 IOBase.coq_T) ->
+ 'a4 IOBase.coq_T) -> (exn -> 'a4
+ IOBase.coq_T) -> 'a4 IOBase.coq_T **)
let set s =
(); (fun _ k x -> Obj.magic k () s)
(** val get :
__ -> (logicalState -> proofview -> __
- -> ('a1 -> __ -> ((__*bool) -> (exn ->
+ -> ('a1 -> __ -> (__ -> bool -> __ ->
+ (__ -> (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) -> __
+ -> (__ -> (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) -> __
+ -> (__ -> (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) -> __ -> (__ -> (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 -> __ -> ('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 **)
+ ('a2 -> bool -> __ -> ('a3 -> (exn ->
+ __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> __ -> ('a3 -> (exn ->
+ 'a4 IOBase.coq_T) -> 'a4 IOBase.coq_T)
+ -> (exn -> 'a4 IOBase.coq_T) -> 'a4
+ IOBase.coq_T **)
let get r k s =
Obj.magic k s s
(** val put :
logicalMessageType -> __ -> (unit ->
- proofview -> __ -> ('a1 -> __ ->
- ((__*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 -> __ ->
- ('a1 -> __ -> (('a2*bool) -> (exn -> __
+ proofview -> __ -> ('a1 -> __ -> (__ ->
+ bool -> __ -> (__ -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
(exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> __ -> (__ -> (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 **)
+ (__ -> bool -> __ -> (__ -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> __ -> (__ -> (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) -> __
+ -> (__ -> (exn -> __ IOBase.coq_T) ->
+ __ IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ Environ.env -> __ -> ('a2 -> bool -> __
+ -> ('a3 -> (exn -> __ IOBase.coq_T) ->
+ __ IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) -> __
+ -> ('a3 -> (exn -> 'a4 IOBase.coq_T) ->
+ 'a4 IOBase.coq_T) -> (exn -> 'a4
+ IOBase.coq_T) -> 'a4 IOBase.coq_T **)
let put m =
- (); (fun _ k s _ k0 e _ sk fk ->
+ (); (fun _ k s _ k0 e _ k1 ->
Obj.magic k () s __ k0 e __
- (fun a fk0 ->
- let y,c' = a in
- sk (y,(if m then c' else false)) fk0)
- fk)
+ (fun b c' ->
+ k1 b (if m then c' else false)))
(** val current :
__ -> (logicalEnvironment -> proofview
- -> __ -> ('a1 -> __ -> ((__*bool) ->
- (exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> (exn -> __
+ -> __ -> ('a1 -> __ -> (__ -> bool ->
+ __ -> (__ -> (exn -> __ IOBase.coq_T)
+ -> __ IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) -> __
+ -> (__ -> (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 -> __ ->
- ('a1 -> __ -> (('a2*bool) -> (exn -> __
+ Environ.env -> __ -> (__ -> bool -> __
+ -> (__ -> (exn -> __ IOBase.coq_T) ->
+ __ IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) -> __
+ -> (__ -> (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) -> __ -> (__ -> (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
+ ('a2 -> bool -> __ -> ('a3 -> (exn ->
+ __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> __ -> ('a3 -> (exn ->
+ 'a4 IOBase.coq_T) -> 'a4 IOBase.coq_T)
+ -> (exn -> 'a4 IOBase.coq_T) -> 'a4
IOBase.coq_T **)
let current r k s r0 k0 e =
@@ -387,77 +504,119 @@ module Logical =
(** val zero :
exn -> __ -> ('a1 -> proofview -> __ ->
- ('a2 -> __ -> ((__*bool) -> (exn -> __
+ ('a2 -> __ -> (__ -> bool -> __ -> (__
+ -> (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) -> __
+ -> (__ -> (exn -> __ IOBase.coq_T) ->
+ __ IOBase.coq_T) -> (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 -> __
+ Environ.env -> __ -> (__ -> bool -> __
+ -> (__ -> (exn -> __ IOBase.coq_T) ->
+ __ IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) -> __
+ -> (__ -> (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 -> __
+ proofview -> __ -> ('a2 -> __ -> ('a3
+ -> bool -> __ -> (__ -> (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 **)
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> __ -> (__ -> (exn ->
+ __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> Environ.env -> __ ->
+ ('a3 -> bool -> __ -> ('a4 -> (exn ->
+ __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> __ -> ('a4 -> (exn ->
+ 'a5 IOBase.coq_T) -> 'a5 IOBase.coq_T)
+ -> (exn -> 'a5 IOBase.coq_T) -> 'a5
+ IOBase.coq_T **)
let zero e =
- (); (fun _ k s _ k0 e0 _ sk fk -> fk e)
+ (); (fun _ k s _ k0 e0 _ k1 _ sk fk ->
+ fk e)
(** val plus :
'a1 t -> (exn -> 'a1 t) -> __ -> ('a1
- -> proofview -> __ -> ('a2 -> __ ->
- ((__*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 -> __ ->
- ('a2 -> __ -> (('a3*bool) -> (exn -> __
+ -> proofview -> __ -> ('a2 -> __ -> (__
+ -> bool -> __ -> (__ -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
(exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> __ -> (__ -> (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 **)
+ (__ -> bool -> __ -> (__ -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> __ -> (__ -> (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) -> __
+ -> (__ -> (exn -> __ IOBase.coq_T) ->
+ __ IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ Environ.env -> __ -> ('a3 -> bool -> __
+ -> ('a4 -> (exn -> __ IOBase.coq_T) ->
+ __ IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) -> __
+ -> ('a4 -> (exn -> 'a5 IOBase.coq_T) ->
+ 'a5 IOBase.coq_T) -> (exn -> 'a5
+ IOBase.coq_T) -> 'a5 IOBase.coq_T **)
let plus x y =
- (); (fun _ k s _ k0 e _ sk fk ->
- Obj.magic x __ k s __ k0 e __ sk
+ (); (fun _ k s _ k0 e _ k1 _ sk fk ->
+ Obj.magic x __ k s __ k0 e __ k1 __ sk
(fun e0 ->
- Obj.magic y e0 __ k s __ k0 e __ sk
- fk))
+ Obj.magic y e0 __ k s __ k0 e __ k1
+ __ sk fk))
(** val split :
'a1 t -> __ -> (('a1, exn -> 'a1 t)
list_view -> proofview -> __ -> ('a2 ->
- __ -> ((__*bool) -> (exn -> __
- IOBase.coq_T) -> __ IOBase.coq_T) ->
+ __ -> (__ -> bool -> __ -> (__ -> (exn
+ -> __ IOBase.coq_T) -> __ IOBase.coq_T)
+ -> (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> __ -> (__ -> (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 -> __
+ (__ -> bool -> __ -> (__ -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
- proofview -> __ -> ('a2 -> __ ->
- (('a3*bool) -> (exn -> __ IOBase.coq_T)
- -> __ IOBase.coq_T) -> (exn -> __
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> __ -> (__ -> (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) -> __
+ -> (__ -> (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 **)
+ Environ.env -> __ -> ('a3 -> bool -> __
+ -> ('a4 -> (exn -> __ IOBase.coq_T) ->
+ __ IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) -> __
+ -> ('a4 -> (exn -> 'a5 IOBase.coq_T) ->
+ 'a5 IOBase.coq_T) -> (exn -> 'a5
+ IOBase.coq_T) -> 'a5 IOBase.coq_T **)
let split x =
- (); (fun _ k s _ k0 e _ sk fk ->
+ (); (fun _ k s _ k0 e _ k1 _ sk fk ->
IOBase.bind
- (Obj.magic x __ (fun a s' _ k1 e0 ->
- k1 (a,s')) s __ (fun a _ sk0 fk0 ->
- sk0 (a,true) fk0) e __
- (fun a fk0 ->
+ (Obj.magic x __ (fun a s' _ k2 e0 ->
+ k2 (a,s')) s __ (fun a _ k2 ->
+ k2 a true) e __
+ (fun a c _ sk0 fk0 ->
+ sk0 (a,c) fk0) __ (fun a fk0 ->
IOBase.ret (Cons (a,
(fun e0 _ sk0 fk1 ->
IOBase.bind (fk0 e0) (fun x0 ->
@@ -471,55 +630,61 @@ module Logical =
match x0 with
| Nil exc ->
Obj.magic k (Nil exc) s __ k0 e __
- (fun a fk0 ->
- let y,c' = a in sk (y,c') fk0) fk
+ (fun b c' -> k1 b c') __ sk fk
| Cons (p, y) ->
let p0,m' = p in
let a',s' = p0 in
Obj.magic k (Cons (a',
- (fun exc _ k1 s0 _ k2 e0 _ sk0 fk0 ->
+ (fun exc _ k2 s0 _ k3 e0 _ k4 _ sk0 fk0 ->
y exc __ (fun a fk1 ->
- let x1,c = a in
- let a0,s'0 = x1 in
- 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' __ k0 e __
- (fun a fk0 ->
- let y0,c' = a in
- sk
- (y0,(if m' then c' else false))
- fk0) fk))
+ let a0,c = a in
+ let a1,s'0 = a0 in
+ k2 a1 s'0 __ k3 e0 __
+ (fun b c' ->
+ k4 b
+ (if c then c' else false))
+ __ sk0 fk1) fk0))) s' __ k0 e
+ __ (fun b c' ->
+ k1 b (if m' then c' else false))
+ __ sk fk))
(** val lift :
'a1 NonLogical.t -> __ -> ('a1 ->
- proofview -> __ -> ('a2 -> __ ->
- ((__*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 -> __ ->
- ('a2 -> __ -> (('a3*bool) -> (exn -> __
+ proofview -> __ -> ('a2 -> __ -> (__ ->
+ bool -> __ -> (__ -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
(exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> __ -> (__ -> (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 **)
+ (__ -> bool -> __ -> (__ -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> __ -> (__ -> (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) -> __
+ -> (__ -> (exn -> __ IOBase.coq_T) ->
+ __ IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ Environ.env -> __ -> ('a3 -> bool -> __
+ -> ('a4 -> (exn -> __ IOBase.coq_T) ->
+ __ IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) -> __
+ -> ('a4 -> (exn -> 'a5 IOBase.coq_T) ->
+ 'a5 IOBase.coq_T) -> (exn -> 'a5
+ IOBase.coq_T) -> 'a5 IOBase.coq_T **)
let lift x =
- (); (fun _ k s _ k0 e _ sk fk ->
+ (); (fun _ k s _ k0 e _ k1 _ sk fk ->
IOBase.bind x (fun x0 ->
Obj.magic k x0 s __ k0 e __
- (fun a fk0 ->
- let y,c' = a in sk (y,c') fk0) fk))
+ (fun b c' -> k1 b c') __ sk fk))
(** val run :
'a1 t -> logicalEnvironment ->
@@ -529,9 +694,10 @@ module Logical =
let run x e s =
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 ->
+ k (a,s')) s __ (fun a _ k -> k a true)
+ e __ (fun a c _ sk fk -> sk (a,c) fk)
+ __ (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 21:23:12 +0000