diff options
| -rw-r--r-- | proofs/proofview.ml | 37 | ||||
| -rw-r--r-- | proofs/proofview.mli | 21 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 7 | ||||
| -rw-r--r-- | tactics/rewrite.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 13 |
5 files changed, 19 insertions, 61 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 49615a5f8..d42ea8b80 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -639,22 +639,9 @@ let in_proofview p k = k p.solution -(* spiwack: to help using `bind' like construct consistently. A glist - is promissed to have exactly one element per goal when it is - produced. *) -type 'a glist = 'a list module Notations = struct let (>=) = tclBIND - let (>>=) t k = - t >= fun l -> - tclDISPATCHGEN k ignore l - let (>>==) t k = - begin - t >= fun l -> - tclDISPATCHGEN k List.rev l - end >= fun l' -> - tclUNIT (List.flatten l') let (<*>) = tclTHEN let (<+>) t1 t2 = tclOR t1 (fun _ -> t2) end @@ -797,26 +784,24 @@ module Goal = struct let hyps { hyps=hyps } = Environ.named_context_of_val hyps let concl { concl=concl } = concl - let lift s = + let lift s k = (* spiwack: convenience notations, waiting for ocaml 3.12 *) let (>>=) = Proof.bind in let (>>) = Proof.seq in Proof.current >>= fun env -> Proof.get >>= fun step -> try - let (res,sigma) = + let (ks,sigma) = Goal.list_map begin fun sigma g -> - Goal.eval s env sigma g + Util.on_fst k (Goal.eval s env sigma g) end step.comb step.solution in Proof.set { step with solution=sigma } >> - Proof.ret res + tclDISPATCH ks with e when catchable_exception e -> let e = Errors.push e in tclZERO e - let return x = lift (Goal.return x) - let enter_t f = Goal.enter begin fun env sigma hyps concl self -> f {env=env;sigma=sigma;hyps=hyps;concl=concl;self=self} end @@ -832,20 +817,6 @@ module Goal = struct let e = Errors.push e in tclZERO e end - let enterl f = - list_iter_goal [] begin fun goal acc -> - Proof.current >= fun env -> - tclEVARMAP >= fun sigma -> - try - (* enter_t cannot modify the sigma. *) - let (t,_) = Goal.eval (enter_t f) env sigma goal in - t >= fun r -> - tclUNIT (r::acc) - with e when catchable_exception e -> - let e = Errors.push e in - tclZERO e - end >= fun res -> - tclUNIT (List.flatten (List.rev res)) (* compatibility *) diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 021155c42..c608bc841 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -266,11 +266,6 @@ val list_map : ('a -> 'b tactic) -> 'a list -> 'b list tactic val in_proofview : proofview -> (Evd.evar_map -> 'a) -> 'a -(* spiwack: to help using `bind' like construct consistently. A glist - is promissed to have exactly one element per goal when it is - produced. *) -type 'a glist = private 'a list - (* Notations for building tactics. *) module Notations : sig @@ -280,10 +275,6 @@ module Notations : sig The [t] is supposed to return a list of values of the size of the list of goals. [k] is then applied to each of this value in the corresponding goal. *) - val (>>=) : 'a glist tactic -> ('a -> unit tactic) -> unit tactic - (* [t >>== k] acts as [t] except that [k] returns a list of value - corresponding to its produced subgoals. *) - val (>>==) : 'a glist tactic -> ('a -> 'b glist tactic) -> 'b glist tactic (* tclTHEN *) val (<*>) : unit tactic -> 'a tactic -> 'a tactic @@ -356,20 +347,14 @@ module Goal : sig val env : t -> Environ.env val sigma : t -> Evd.evar_map - (* [lift_sensitive s] returns the list corresponding to the evaluation - of [s] on each of the focused goals *) - val lift : 'a Goal.sensitive -> 'a glist tactic - - (* [return x] returns a copy of [x] per focused goal. *) - val return : 'a -> 'a glist tactic + (* [lift_sensitive s k] applies [s] in each goal independently + raising result [a] then continues with [k a]. *) + val lift : 'a Goal.sensitive -> ('a->unit tactic) -> unit tactic (* [enter t] execute the goal-dependent tactic [t] in each goal independently. In particular [t] need not backtrack the same way in each goal. *) val enter : (t -> unit tactic) -> unit tactic - (* [enterl t] works like [enter t] except that [t] returns a value - in each of the produced subgoals. *) - val enterl : (t -> 'a glist tactic) -> 'a glist tactic (* compatibility: avoid if possible *) diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index a1e57fd3c..033a4dc1b 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -344,9 +344,10 @@ let refine_tac (ist, c) = let tycon = Pretyping.OfType concl in Goal.Refinable.constr_of_raw h tycon flags vars c) end in - Proofview.Goal.lift c >>= fun c -> - Proofview.tclSENSITIVE (Goal.refine c) <*> - Proofview.V82.tactic (reduce refine_red_flags refine_locs)) + Proofview.Goal.lift c begin fun c -> + Proofview.tclSENSITIVE (Goal.refine c) <*> + Proofview.V82.tactic (reduce refine_red_flags refine_locs) + end) TACTIC EXTEND refine [ "refine" glob(c) ] -> [ refine_tac c ] diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index a10b62162..853215a5a 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1305,7 +1305,7 @@ let cl_rewrite_clause_newtac ?abs strat clause = | TypeClassError (env, (UnsatisfiableConstraints _ as e)) -> raise (RewriteFailure (str"Unable to satisfy the rewriting constraints." ++ fnl () ++ Himsg.explain_typeclass_error env e))) - in Proofview.Notations.(>>=) (Proofview.Goal.lift info) (fun i -> treat i) + in Proofview.Goal.lift info (fun i -> treat i) let newtactic_init_setoid () = try init_setoid (); Proofview.tclUNIT () diff --git a/tactics/tactics.ml b/tactics/tactics.ml index b4fb6b900..b4b6934f2 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3937,11 +3937,12 @@ module New = struct let c = Goal.Refinable.make begin fun h -> Goal.Refinable.constr_of_open_constr h true c end in - Proofview.Goal.lift c >>= fun c -> - Proofview.tclSENSITIVE (Goal.refine c) <*> - Proofview.V82.tactic (reduce - (Lazy {rBeta=true;rIota=true;rZeta=false;rDelta=false;rConst=[]}) - {onhyps=None; concl_occs=AllOccurrences } - ) + Proofview.Goal.lift c begin fun c -> + Proofview.tclSENSITIVE (Goal.refine c) <*> + Proofview.V82.tactic (reduce + (Lazy {rBeta=true;rIota=true;rZeta=false;rDelta=false;rConst=[]}) + {onhyps=None; concl_occs=AllOccurrences } + ) + end end |