diff options
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 19 | ||||
| -rw-r--r-- | plugins/ssr/ssrcommon.mli | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 29 | ||||
| -rw-r--r-- | plugins/ssr/ssrtacticals.ml | 2 |
4 files changed, 32 insertions, 20 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 64c4914054..238b94ae49 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -1105,16 +1105,17 @@ let interp_clr sigma = function let tclID tac = tac let tclDOTRY n tac = + let open Tacticals.New in if n <= 0 then tclIDTAC else - let rec loop i gl = - if i = n then tclTRY tac gl else - tclTRY (tclTHEN tac (loop (i + 1))) gl in + let rec loop i = + if i = n then tclTRY tac else + tclTRY (tclTHEN tac (loop (i + 1))) in loop 1 let tclDO n tac = let prefix i = str"At iteration " ++ int i ++ str": " in let tac_err_at i gl = - try tac gl + try Proofview.V82.of_tactic tac gl with | CErrors.UserError (l, s) as e -> let _, info = Exninfo.capture e in @@ -1125,11 +1126,15 @@ let tclDO n tac = let rec loop i gl = if i = n then tac_err_at i gl else (tclTHEN (tac_err_at i) (loop (i + 1))) gl in - loop 1 + Proofview.V82.tactic ~nf_evars:false (loop 1) + +let tclAT_LEAST_ONCE t = + let open Tacticals.New in + tclTHEN t (tclREPEAT t) let tclMULT = function - | 0, May -> tclREPEAT - | 1, May -> tclTRY + | 0, May -> Tacticals.New.tclREPEAT + | 1, May -> Tacticals.New.tclTRY | n, May -> tclDOTRY n | 0, Must -> tclAT_LEAST_ONCE | n, Must when n > 1 -> tclDO n diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index 00b2e56221..b82478a23a 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -410,7 +410,7 @@ val genclrtac : val old_cleartac : ssrhyps -> v82tac val cleartac : ssrhyps -> unit Proofview.tactic -val tclMULT : int * ssrmmod -> Tacmach.tactic -> Tacmach.tactic +val tclMULT : int * ssrmmod -> unit Proofview.tactic -> unit Proofview.tactic val unprotecttac : unit Proofview.tactic val is_protect : EConstr.t -> Environ.env -> Evd.evar_map -> bool diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 45426362fb..668395aa37 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -639,27 +639,34 @@ let ipat_rewrite occ dir c = Proofview.V82.tactic ~nf_evars:false begin fun gl - rwrxtac occ None dir (project gl, c) gl end -let rwargtac ?under ?map_redex ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) gl = +let rwargtac ?under ?map_redex ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) = + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in let fail = ref false in let interp_rpattern gl gc = try interp_rpattern (pf_env gl) (project gl) gc with _ when snd mult = May -> fail := true; project gl, T mkProp in - let interp gc gl = - try interp_term (pf_env gl) (project gl) ist gc - with _ when snd mult = May -> fail := true; (project gl, EConstr.mkProp) in - let rwtac gl = + let interp env sigma gc = + try interp_term env sigma ist gc + with _ when snd mult = May -> fail := true; (sigma, EConstr.mkProp) in + let rwtac = + Proofview.V82.tactic begin fun gl -> let rx = Option.map (interp_rpattern gl) grx in let gl = match rx with | None -> gl | Some (s,_) -> pf_merge_uc_of s gl in - let t = interp gt gl in + let t = interp (pf_env gl) (project gl) gt in let gl = pf_merge_uc_of (fst t) gl in (match kind with | RWred sim -> simplintac occ rx sim | RWdef -> if dir = R2L then foldtac occ rx t else unfoldintac occ rx t gt - | RWeq -> rwrxtac ?under ?map_redex occ rx dir t) gl in - let ctac = old_cleartac (interp_clr (project gl) (oclr, (fst gt, snd (interp gt gl)))) in - if !fail then ctac gl else tclTHEN (tclMULT mult rwtac) ctac gl + | RWeq -> rwrxtac ?under ?map_redex occ rx dir t) gl + end + in + let ctac = cleartac (interp_clr sigma (oclr, (fst gt, snd (interp env sigma gt)))) in + if !fail then ctac else Tacticals.New.tclTHEN (tclMULT mult rwtac) ctac + end (** Rewrite argument sequence *) @@ -668,8 +675,8 @@ let rwargtac ?under ?map_redex ist ((dir, mult), (((oclr, occ), grx), (kind, gt) (** The "rewrite" tactic *) let ssrrewritetac ?under ?map_redex ist rwargs = - Proofview.V82.tactic begin fun gl -> - tclTHENLIST (List.map (rwargtac ?under ?map_redex ist) rwargs) gl + Proofview.Goal.enter begin fun _ -> + Tacticals.New.tclTHENLIST (List.map (rwargtac ?under ?map_redex ist) rwargs) end (** The "unlock" tactic *) diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml index a379b2561a..26fd463124 100644 --- a/plugins/ssr/ssrtacticals.ml +++ b/plugins/ssr/ssrtacticals.ml @@ -164,4 +164,4 @@ let hinttac ist is_by (is_or, atacs) = let ssrdotac ist (((n, m), tac), clauses) = let mul = get_index n, m in - tclCLAUSES (Proofview.V82.tactic (tclMULT mul (Proofview.V82.of_tactic (hinttac ist false tac)))) clauses + tclCLAUSES (tclMULT mul (hinttac ist false tac)) clauses |