diff options
Diffstat (limited to 'plugins/ssr/ssrbwd.ml')
| -rw-r--r-- | plugins/ssr/ssrbwd.ml | 65 |
1 files changed, 49 insertions, 16 deletions
diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml index c29a1fe7c..23da1eb69 100644 --- a/plugins/ssr/ssrbwd.ml +++ b/plugins/ssr/ssrbwd.ml @@ -51,6 +51,24 @@ let interp_agen ist gl ((goclr, _), (k, gc as c)) (clr, rcs) = let pf_pr_glob_constr gl = pr_glob_constr_env (pf_env gl) +let interp_nbargs ist gl rc = + try + let rc6 = mkRApp rc (mkRHoles 6) in + let sigma, t = interp_open_constr ist gl (rc6, None) in + let si = sig_it gl in + let gl = re_sig si sigma in + 6 + Ssrcommon.nbargs_open_constr gl t + with _ -> 5 + +let interp_view_nbimps ist gl rc = + try + let sigma, t = interp_open_constr ist gl (rc, None) in + let si = sig_it gl in + let gl = re_sig si sigma in + let pl, c = splay_open_constr gl t in + if Ssrcommon.isAppInd (pf_env gl) (project gl) c then List.length pl else (-(List.length pl)) + with _ -> 0 + let interp_agens ist gl gagens = match List.fold_right (interp_agen ist gl) gagens ([], []) with | clr, rlemma :: args -> @@ -86,40 +104,55 @@ let mkRAppView ist gl rv gv = let prof_apply_interp_with = mk_profiler "ssrapplytac.interp_with";; -let refine_interp_apply_view i ist gl gv = +let refine_interp_apply_view dbl ist gl gv = let pair i = List.map (fun x -> i, x) in let rv = pf_intern_term ist gl gv in let v = mkRAppView ist gl rv gv in - let interp_with (i, hint) = + let interp_with (dbl, hint) = + let i = if dbl = Ssrview.AdaptorDb.Equivalence then 2 else 1 in interp_refine ist gl (mkRApp hint (v :: mkRHoles i)) in let interp_with x = prof_apply_interp_with.profile interp_with x in let rec loop = function | [] -> (try apply_rconstr ~ist rv gl with _ -> view_error "apply" gv) | h :: hs -> (try refine_with (snd (interp_with h)) gl with _ -> loop hs) in - loop (pair i Ssrview.viewtab.(i) @ - if i = 2 then pair 1 Ssrview.viewtab.(1) else []) - -let apply_top_tac gl = - Tacticals.tclTHENLIST [introid top_id; apply_rconstr (mkRVar top_id); Proofview.V82.of_tactic (Tactics.clear [top_id])] gl - -let inner_ssrapplytac gviews ggenl gclr ist gl = + loop (pair dbl (Ssrview.AdaptorDb.get dbl) @ + if dbl = Ssrview.AdaptorDb.Equivalence + then pair Ssrview.AdaptorDb.Backward (Ssrview.AdaptorDb.(get Backward)) + else []) + +let apply_top_tac = + Tacticals.tclTHENLIST [ + introid top_id; + apply_rconstr (mkRVar top_id); + old_cleartac [SsrHyp(None,top_id)] + ] + +let inner_ssrapplytac gviews (ggenl, gclr) ist = Proofview.V82.tactic ~nf_evars:false (fun gl -> let _, clr = interp_hyps ist gl gclr in let vtac gv i gl' = refine_interp_apply_view i ist gl' gv in let ggenl, tclGENTAC = if gviews <> [] && ggenl <> [] then - let ggenl= List.map (fun (x,g) -> x, cpattern_of_term g) (List.hd ggenl) in - [], Tacticals.tclTHEN (genstac (ggenl,[]) ist) + let ggenl= List.map (fun (x,g) -> x, cpattern_of_term g ist) (List.hd ggenl) in + [], Tacticals.tclTHEN (genstac (ggenl,[])) else ggenl, Tacticals.tclTHEN Tacticals.tclIDTAC in tclGENTAC (fun gl -> match gviews, ggenl with | v :: tl, [] -> - let dbl = if List.length tl = 1 then 2 else 1 in + let dbl = + if List.length tl = 1 + then Ssrview.AdaptorDb.Equivalence + else Ssrview.AdaptorDb.Backward in Tacticals.tclTHEN - (List.fold_left (fun acc v -> Tacticals.tclTHENLAST acc (vtac v dbl)) (vtac v 1) tl) - (cleartac clr) gl + (List.fold_left (fun acc v -> + Tacticals.tclTHENLAST acc (vtac v dbl)) + (vtac v Ssrview.AdaptorDb.Backward) tl) + (old_cleartac clr) gl | [], [agens] -> let clr', (sigma, lemma) = interp_agens ist gl agens in let gl = pf_merge_uc_of sigma gl in - Tacticals.tclTHENLIST [cleartac clr; refine_with ~beta:true lemma; cleartac clr'] gl - | _, _ -> Tacticals.tclTHEN apply_top_tac (cleartac clr) gl) gl + Tacticals.tclTHENLIST [old_cleartac clr; refine_with ~beta:true lemma; old_cleartac clr'] gl + | _, _ -> + Tacticals.tclTHENLIST [apply_top_tac; old_cleartac clr] gl) gl +) +let apply_top_tac = Proofview.V82.tactic ~nf_evars:false apply_top_tac |