aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--bootstrap/Monads.v36
-rw-r--r--proofs/proofview.ml12
-rw-r--r--proofs/proofview_gen.ml56
-rw-r--r--proofs/proofview_monad.mli5
4 files changed, 57 insertions, 52 deletions
diff --git a/bootstrap/Monads.v b/bootstrap/Monads.v
index f3f2eb653..37eaf7d6a 100644
--- a/bootstrap/Monads.v
+++ b/bootstrap/Monads.v
@@ -27,11 +27,6 @@ Extract Inductive prod => "(*)" [
"(,)"
].
-(*** Sum ***)
-Extract Inductive sum => "Util.union" [
- "Util.Inl"
- "Util.Inr"
-].
(*** Closure elimination **)
@@ -76,6 +71,13 @@ Extract Inlined Constant String => string.
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.
@@ -471,20 +473,20 @@ Section Common.
(* 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 :=
+ Definition reflect {A:Set} (x:list_view A (Exception -> T A)) : T A :=
match x with
- | inr e => _zero e
- | inl (a,x) => _plus (ret _ F a) x
+ | Nil _ _ e => _zero e
+ | Cons _ _ a x => _plus (ret _ F a) x
end
.
- Definition reify {A:Set} (x:T A) : T₀ ((A*(Exception -> T A)) + Exception) :=
- let fk e := ret _ M (inr e) in
+ 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 (inl (a, lift_fk fk)) in
+ let sk a fk := ret _ M (Cons _ _ a (lift_fk fk)) in
x _ sk fk
.
- Definition split {A:Set} (x:T A) : T ((A*(Exception -> T A)) + Exception) :=
+ Definition split {A:Set} (x:T A) : T (list_view A (Exception -> T A)) :=
lift (reify x)
.
@@ -547,21 +549,21 @@ Definition LogicalLogic : Logic LogicalType := State.Logic _ _ LogicalMonadEnv (
(* 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 ((a*(Exception -> LogicalType a))+Exception) :=
+Definition split0 {a:Set} (x:LogicalType a) : LogicalType (list_view a (Exception -> LogicalType a)) :=
State.reflect _ _ LogicalMonadEnv (fun s =>
Environment.reflect _ _ (fun e =>
Writer.reflect _ _ (
do LogicalMonadBase x' :=
Logic.split _ NonLogicalMonad (Writer.run _ _ (Environment.run _ _ (State.run _ _ LogicalMonadEnv x s) e)) in
match x' with
- | inr exc => ret _ LogicalMonadBase ((inr exc),s, Monoid.zero _ LogicalMessage)
- | inl (a',s',m',y) =>
+ | 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 _ =>
Writer.reflect _ _ (y exc)))
in
- ret _ LogicalMonadBase (inl (a',y'),s',m')
+ ret _ LogicalMonadBase (Cons _ _ a' y',s',m')
end
)))
.
@@ -630,7 +632,7 @@ Module Logical.
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 ((a*(Exception -> t a))+Exception) :=
+ Definition split {a:Set} (x:t a) : t (list_view a (Exception -> t a)) :=
Eval compute in freeze _ (split0 x).
(*
Eval compute in
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 167fedf7b..bdddf310d 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -231,8 +231,8 @@ let tclORELSE t1 t2 =
(* spiwack: convenience notations, waiting for ocaml 3.12 *)
let (>>=) = Proof.bind in
Proof.split t1 >>= function
- | Util.Inr e -> t2 e
- | Util.Inl (a,t1') -> Proof.plus (Proof.ret a) t1'
+ | Nil e -> t2 e
+ | Cons (a,t1') -> Proof.plus (Proof.ret a) t1'
(* [tclIFCATCH a s f] is a generalisation of [tclORELSE]: if [a]
succeeds at least once then it behaves as [tclBIND a s] otherwise, if [a]
@@ -241,8 +241,8 @@ let tclIFCATCH a s f =
(* spiwack: convenience notations, waiting for ocaml 3.12 *)
let (>>=) = Proof.bind in
Proof.split a >>= function
- | Util.Inr e -> f e
- | Util.Inl (x,a') -> Proof.plus (s x) (fun e -> (a' e) >>= fun x' -> (s x'))
+ | Nil e -> f e
+ | Cons (x,a') -> Proof.plus (s x) (fun e -> (a' e) >>= fun x' -> (s x'))
(* [tclONCE t] fails if [t] fails, otherwise it has exactly one
success. *)
@@ -250,8 +250,8 @@ let tclONCE t =
(* spiwack: convenience notations, waiting for ocaml 3.12 *)
let (>>=) = Proof.bind in
Proof.split t >>= function
- | Util.Inr e -> tclZERO e
- | Util.Inl (x,_) -> tclUNIT x
+ | Nil e -> tclZERO e
+ | Cons (x,_) -> tclUNIT x
(* Focuses a tactic at a range of subgoals, found by their indices. *)
(* arnaud: bug if 0 goals ! *)
diff --git a/proofs/proofview_gen.ml b/proofs/proofview_gen.ml
index ad87b7328..d168188de 100644
--- a/proofs/proofview_gen.ml
+++ b/proofs/proofview_gen.ml
@@ -8,6 +8,10 @@
type __ = Obj.t
let __ = let rec f _ = Obj.repr f in Obj.repr f
+type ('a, 'b) list_view =
+| Nil of exn
+| Cons of 'a * 'b
+
module IOBase =
struct
type 'a coq_T = unit -> 'a
@@ -354,17 +358,16 @@ module Logical =
Obj.magic y e __ k s env __ sk fk))
(** val split :
- 'a1 t -> __ -> (('a1*(exn -> 'a1 t),
- exn) Util.union -> proofview ->
- Environ.env -> __ -> (('a2*bool) ->
- (exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> (exn -> __
+ 'a1 t -> __ -> (('a1, exn -> 'a1 t)
+ list_view -> proofview -> Environ.env
+ -> __ -> (('a2*bool) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
- proofview -> Environ.env -> __ ->
- (('a2*bool) -> (exn -> 'a3
- IOBase.coq_T) -> 'a3 IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> proofview ->
+ Environ.env -> __ -> (('a2*bool) ->
(exn -> 'a3 IOBase.coq_T) -> 'a3
- IOBase.coq_T **)
+ IOBase.coq_T) -> (exn -> 'a3
+ IOBase.coq_T) -> 'a3 IOBase.coq_T **)
let split x =
(); (fun _ k s e _ sk fk ->
@@ -373,25 +376,26 @@ module Logical =
(fun a s' e0 _ sk0 fk0 ->
sk0 ((a,s'),true) fk0) s e __
(fun a fk0 ->
- IOBase.ret (Util.Inl
- (a,(fun e0 _ sk0 fk1 ->
+ IOBase.ret (Cons (a,
+ (fun e0 _ sk0 fk1 ->
IOBase.bind (fk0 e0) (fun x0 ->
match x0 with
- | Util.Inl p ->
- let a0,x1 = p in
+ | Nil e1 -> fk1 e1
+ | Cons (a0, x1) ->
sk0 a0 (fun e1 ->
- x1 e1 __ sk0 fk1)
- | Util.Inr e1 -> fk1 e1)))))
- (fun e0 ->
- IOBase.ret (Util.Inr e0)))
+ x1 e1 __ sk0 fk1))))))
+ (fun e0 -> IOBase.ret (Nil e0)))
(fun x0 ->
match x0 with
- | Util.Inl p ->
- let p0,y = p in
- let p1,m' = p0 in
- let a',s' = p1 in
- Obj.magic k (Util.Inl
- (a',(fun exc _ k0 s0 e0 _ sk0 fk0 ->
+ | Nil exc ->
+ Obj.magic k (Nil exc) s 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 ->
y exc __ (fun a fk1 ->
let x1,c = a in
let a0,s'0 = x1 in
@@ -405,11 +409,7 @@ module Logical =
let y0,c' = a in
sk
(y0,(if m' then c' else false))
- fk0) fk
- | Util.Inr exc ->
- Obj.magic k (Util.Inr exc) s e __
- (fun a fk0 ->
- let y,c' = a in sk (y,c') fk0) fk))
+ fk0) fk))
(** val lift :
'a1 NonLogical.t -> __ -> ('a1 ->
diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli
index bdebe658c..f9854ae0c 100644
--- a/proofs/proofview_monad.mli
+++ b/proofs/proofview_monad.mli
@@ -1,6 +1,9 @@
(* This is an interface for the code extracted from bootstrap/Monad.v.
The relevant comments are overthere. *)
+type ('a, 'b) list_view =
+| Nil of exn
+| Cons of 'a * 'b
type proofview = { initial : (Term.constr * Term.types) list;
solution : Evd.evar_map; comb : Goal.goal list }
@@ -58,7 +61,7 @@ module Logical : sig
val zero : exn -> 'a t
val plus : 'a t -> (exn -> 'a t) -> 'a t
- val split : 'a t -> (('a*(exn->'a t),exn) Util.union) t
+ val split : 'a t -> (('a,(exn->'a t)) list_view) t
val lift : 'a NonLogical.t -> 'a t
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 01:12:23 +0000