diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proofview.ml | 12 | ||||
| -rw-r--r-- | proofs/proofview_gen.ml | 56 | ||||
| -rw-r--r-- | proofs/proofview_monad.mli | 5 |
3 files changed, 38 insertions, 35 deletions
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 |