From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- tactics/autorewrite.ml | 112 ++++++++++++++++++------------------------------- 1 file changed, 40 insertions(+), 72 deletions(-) (limited to 'tactics/autorewrite.ml') diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 47500564..c3857e6b 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -1,29 +1,28 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - errorlabstrm "AutoRewrite" + user_err ~hdr:"AutoRewrite" (str "Rewriting base " ++ str bas ++ str " does not exist.") let find_rewrites bas = @@ -76,31 +75,30 @@ let find_matches bas pat = let res = HintDN.search_pattern base pat in List.map snd res -let print_rewrite_hintdb bas = +let print_rewrite_hintdb env sigma bas = (str "Database " ++ str bas ++ fnl () ++ prlist_with_sep fnl (fun h -> str (if h.rew_l2r then "rewrite -> " else "rewrite <- ") ++ - Printer.pr_lconstr h.rew_lemma ++ str " of type " ++ Printer.pr_lconstr h.rew_type ++ + Printer.pr_lconstr_env env sigma h.rew_lemma ++ str " of type " ++ Printer.pr_lconstr_env env sigma h.rew_type ++ Option.cata (fun tac -> str " then use tactic " ++ - Pptactic.pr_glb_generic (Global.env()) tac) (mt ()) h.rew_tac) + Pputils.pr_glb_generic (Global.env()) tac) (mt ()) h.rew_tac) (find_rewrites bas)) -type raw_rew_rule = Loc.t * constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option +type raw_rew_rule = (constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option) CAst.t (* Applies all the rules of one base *) let one_base general_rewrite_maybe_in tac_main bas = let lrul = find_rewrites bas in let try_rewrite dir ctx c tc = - Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in let c' = Vars.subst_univs_level_constr subst c in - let sigma = Sigma.to_evar_map sigma in let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx' in - let tac = general_rewrite_maybe_in dir c' tc in - Sigma.Unsafe.of_pair (tac, sigma) - end } in + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (general_rewrite_maybe_in dir c' tc) + end in let lrul = List.map (fun h -> let tac = match h.rew_tac with | None -> Proofview.tclUNIT () @@ -122,56 +120,24 @@ let autorewrite ?(conds=Naive) tac_main lbas = Tacticals.New.tclTHEN tac (one_base (fun dir c tac -> let tac = (tac, conds) in - general_rewrite dir AllOccurrences true false ~tac c) + general_rewrite dir AllOccurrences true false ~tac (EConstr.of_constr c)) tac_main bas)) (Proofview.tclUNIT()) lbas)) let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> (* let's check at once if id exists (to raise the appropriate error) *) - let _ = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) idl in - let general_rewrite_in id = - let id = ref id in - let to_be_cleared = ref false in - fun dir cstr tac gl -> - let last_hyp_id = - match Tacmach.pf_hyps gl with - d :: _ -> Context.Named.Declaration.get_id d - | _ -> (* even the hypothesis id is missing *) - raise (Logic.RefinerError (Logic.NoSuchHyp !id)) - in - let gl' = Proofview.V82.of_tactic (general_rewrite_in dir AllOccurrences true ~tac:(tac, conds) false !id cstr false) gl in - let gls = gl'.Evd.it in - match gls with - g::_ -> - (match Environ.named_context_of_val (Goal.V82.hyps gl'.Evd.sigma g) with - d ::_ -> - let lastid = Context.Named.Declaration.get_id d in - if not (Id.equal last_hyp_id lastid) then - begin - let gl'' = - if !to_be_cleared then - tclTHEN (fun _ -> gl') (tclTRY (Proofview.V82.of_tactic (clear [!id]))) gl - else gl' in - id := lastid ; - to_be_cleared := true ; - gl'' - end - else - begin - to_be_cleared := false ; - gl' - end - | _ -> assert false) (* there must be at least an hypothesis *) - | _ -> assert false (* rewriting cannot complete a proof *) - in - let general_rewrite_in x y z w = Proofview.V82.tactic (general_rewrite_in x y z w) in + let _ = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) idl in + let general_rewrite_in id dir cstr tac = + let cstr = EConstr.of_constr cstr in + general_rewrite_in dir AllOccurrences true ~tac:(tac, conds) false id cstr false + in Tacticals.New.tclMAP (fun id -> Tacticals.New.tclREPEAT_MAIN (Proofview.tclPROGRESS (List.fold_left (fun tac bas -> Tacticals.New.tclTHEN tac (one_base (general_rewrite_in id) tac_main bas)) (Proofview.tclUNIT()) lbas))) idl - end } + end let autorewrite_in ?(conds=Naive) id = autorewrite_multi_in ~conds [id] @@ -196,10 +162,10 @@ let gen_auto_multi_rewrite conds tac_main lbas cl = | None -> (* try to rewrite in all hypothesis (except maybe the rewritten one) *) - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> let ids = Tacmach.New.pf_ids_of_hyps gl in try_do_hyps (fun id -> id) ids - end }) + end) let auto_multi_rewrite ?(conds=Naive) lems cl = Proofview.V82.wrap_exceptions (fun () -> gen_auto_multi_rewrite conds (Proofview.tclUNIT()) lems cl) @@ -257,12 +223,12 @@ type hypinfo = { let decompose_applied_relation metas env sigma c ctype left2right = let find_rel ty = - let eqclause = Clenv.mk_clenv_from_env env sigma None (c,ty) in + let eqclause = Clenv.mk_clenv_from_env env sigma None (EConstr.of_constr c,ty) in let eqclause = if metas then eqclause else clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd) in - let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in + let (equiv, args) = decompose_app (EConstr.Unsafe.to_constr (Clenv.clenv_type eqclause)) in let rec split_last_two = function | [c1;c2] -> [],(c1, c2) | x::y::z -> @@ -272,11 +238,13 @@ let decompose_applied_relation metas env sigma c ctype left2right = try let others,(c1,c2) = split_last_two args in let ty1, ty2 = - Typing.unsafe_type_of env eqclause.evd c1, Typing.unsafe_type_of env eqclause.evd c2 + Typing.unsafe_type_of env eqclause.evd (EConstr.of_constr c1), Typing.unsafe_type_of env eqclause.evd (EConstr.of_constr c2) in + let ty = EConstr.Unsafe.to_constr ty in + let ty1 = EConstr.Unsafe.to_constr ty1 in (* if not (evd_convertible env eqclause.evd ty1 ty2) then None *) (* else *) - Some { hyp_cl=eqclause; hyp_prf=(Clenv.clenv_value eqclause); hyp_ty = ty; + Some { hyp_cl=eqclause; hyp_prf=EConstr.Unsafe.to_constr (Clenv.clenv_value eqclause); hyp_ty = ty; hyp_car=ty1; hyp_rel=mkApp (equiv, Array.of_list others); hyp_l2r=left2right; hyp_left=c1; hyp_right=c2; } with Not_found -> None @@ -289,13 +257,13 @@ let decompose_applied_relation metas env sigma c ctype left2right = | Some c -> Some c | None -> None -let find_applied_relation metas loc env sigma c left2right = - let ctype = Typing.unsafe_type_of env sigma c in +let find_applied_relation ?loc metas env sigma c left2right = + let ctype = Typing.unsafe_type_of env sigma (EConstr.of_constr c) in match decompose_applied_relation metas env sigma c ctype left2right with | Some c -> c | None -> - user_err_loc (loc, "decompose_applied_relation", - str"The type" ++ spc () ++ Printer.pr_constr_env env sigma ctype ++ + user_err ?loc ~hdr:"decompose_applied_relation" + (str"The type" ++ spc () ++ Printer.pr_econstr_env env sigma ctype ++ spc () ++ str"of this term does not end with an applied relation.") (* To add rewriting rules to a base *) @@ -303,13 +271,13 @@ let add_rew_rules base lrul = let counter = ref 0 in let env = Global.env () in let sigma = Evd.from_env env in - let ist = { Genintern.ltacvars = Id.Set.empty; genv = Global.env () } in + let ist = Genintern.empty_glob_sign (Global.env ()) in let intern tac = snd (Genintern.generic_intern ist tac) in let lrul = List.fold_left - (fun dn (loc,(c,ctx),b,t) -> + (fun dn {CAst.loc;v=((c,ctx),b,t)} -> let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in - let info = find_applied_relation false loc env sigma c b in + let info = find_applied_relation ?loc false env sigma c b in let pat = if b then info.hyp_left else info.hyp_right in let rul = { rew_lemma = c; rew_type = info.hyp_ty; rew_pat = pat; rew_ctx = ctx; rew_l2r = b; -- cgit v1.2.3