diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proofview.ml | 22 | ||||
| -rw-r--r-- | proofs/proofview_gen.ml | 33 | ||||
| -rw-r--r-- | proofs/proofview_monad.mli | 2 |
3 files changed, 42 insertions, 15 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index aac11ffc4c..055cd14b60 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -385,8 +385,7 @@ let list_iter_goal s i = ~adv: begin fun goal -> set_comb [goal] >> i goal r >>= fun r -> - Proof.get >>= fun step -> - Proof.ret ( r , step.comb::subgoals ) + Proof.map (fun step -> (r, step.comb :: subgoals)) Proof.get end end >>= fun (r,subgoals) -> set_comb (List.flatten (List.rev subgoals)) >> @@ -405,8 +404,7 @@ let list_iter_goal2 l s i = ~adv: begin fun goal -> set_comb [goal] >> i goal a r >>= fun r -> - Proof.get >>= fun step -> - Proof.ret ( r , step.comb::subgoals ) + Proof.map (fun step -> (r, step.comb :: subgoals)) Proof.get end end >>= fun (r,subgoals) -> set_comb (List.flatten (List.rev subgoals)) >> @@ -434,17 +432,14 @@ let tclDISPATCHGEN f join tacs = on_advance goal ~solved:( tclUNIT (join []) ) ~adv:begin fun _ -> - f tac >>= fun res -> - Proof.ret (join [res]) + Proof.map (fun res -> join [res]) (f tac) end | _ -> tclZERO SizeMismatch end | _ -> - list_iter_goal2 tacs [] begin fun _ t cur -> - f t >>= fun y -> - Proof.ret ( y :: cur ) - end >>= fun res -> - Proof.ret (join res) + let iter _ t cur = Proof.map (fun y -> y :: cur) (f t) in + let ans = list_iter_goal2 tacs [] iter in + Proof.map join ans let tclDISPATCH tacs = tclDISPATCHGEN Util.identity ignore tacs @@ -532,10 +527,7 @@ let tclPROGRESS t = tclZERO (Errors.UserError ("Proofview.tclPROGRESS" , Pp.str"Failed to progress.")) let tclEVARMAP = - (* spiwack: convenience notations, waiting for ocaml 3.12 *) - let (>>=) = Proof.bind in - Proof.get >>= fun initial -> - Proof.ret (initial.solution) + Proof.map (fun initial -> initial.solution) Proof.get let tclENV = Proof.current diff --git a/proofs/proofview_gen.ml b/proofs/proofview_gen.ml index 8008e108b3..a686c528c3 100644 --- a/proofs/proofview_gen.ml +++ b/proofs/proofview_gen.ml @@ -31,6 +31,10 @@ module IOBase = let seq = fun a k -> (); fun () -> a (); k () + (** val map : ('a1 -> 'a2) -> 'a1 coq_T -> 'a2 coq_T **) + + let map = fun f a -> (); fun () -> f (a ()) + (** val ref : 'a1 -> 'a1 coq_Ref coq_T **) let ref = fun a -> (); fun () -> Pervasives.ref a @@ -124,6 +128,11 @@ module NonLogical = let seq x k = IOBase.seq x k + (** val map : ('a1 -> 'a2) -> 'a1 t -> 'a2 t **) + + let map f x = + (); (IOBase.map f x) + (** val new_ref : 'a1 -> 'a1 ref t **) let new_ref x = @@ -296,6 +305,30 @@ module Logical = let seq x k = (); (fun _ k0 s -> Obj.magic x __ (fun x1 s' -> Obj.magic k __ k0 s') s) + (** val map : + ('a1 -> 'a2) -> 'a1 t -> __ -> ('a2 -> proofview -> __ -> ('a3 -> __ -> + (__ -> (bool*(Goal.goal list*Goal.goal list)) -> __ -> (__ -> (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*(Goal.goal list*Goal.goal list)) -> + __ -> (__ -> (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*(Goal.goal list*Goal.goal list)) -> __ -> (__ -> (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*(Goal.goal list*Goal.goal list)) -> + __ -> ('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 map f x = + (); (fun _ k s -> Obj.magic x __ (fun a s0 -> k (f a) s0) s) + (** val set : logicalState -> __ -> (unit -> proofview -> __ -> ('a1 -> __ -> (__ -> (bool*(Goal.goal list*Goal.goal list)) -> __ -> (__ -> (exn -> __ diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli index 6a832e40f5..4d4e4470c0 100644 --- a/proofs/proofview_monad.mli +++ b/proofs/proofview_monad.mli @@ -23,6 +23,7 @@ module NonLogical : sig val ret : 'a -> 'a t val bind : 'a t -> ('a -> 'b t) -> 'b t + val map : ('a -> 'b) -> 'a t -> 'b t val ignore : 'a t -> unit t val seq : unit t -> 'a t -> 'a t @@ -51,6 +52,7 @@ module Logical : sig val ret : 'a -> 'a t val bind : 'a t -> ('a -> 'b t) -> 'b t + val map : ('a -> 'b) -> 'a t -> 'b t val ignore : 'a t -> unit t val seq : unit t -> 'a t -> 'a t |