From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- tactics/autorewrite.ml | 159 +++++++++++++++++++++++-------------------------- 1 file changed, 74 insertions(+), 85 deletions(-) (limited to 'tactics/autorewrite.ml') diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 93441a93..ee8e1855 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -1,39 +1,37 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* - errorlabstrm "AutoRewrite" - (str ("Rewriting base "^(bas)^" does not exist.")) + try raw_find_base bas + with Not_found -> + errorlabstrm "AutoRewrite" + (str ("Rewriting base "^(bas)^" does not exist.")) let find_rewrites bas = List.rev_map snd (HintDN.find_all (find_base bas)) @@ -86,45 +74,55 @@ let find_rewrites bas = let find_matches bas pat = let base = find_base bas in let res = HintDN.search_pattern base pat in - List.map (fun ((_,rew), esubst, subst) -> rew) res + List.map snd res let print_rewrite_hintdb bas = - ppnl (str "Database " ++ str bas ++ (Pp.cut ()) ++ - prlist_with_sep Pp.cut + (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 ++ - str " then use tactic " ++ - Pptactic.pr_glob_tactic (Global.env()) h.rew_tac) + Option.cata (fun tac -> str " then use tactic " ++ + Pptactic.pr_glob_tactic (Global.env()) tac) (mt ()) h.rew_tac) (find_rewrites bas)) -type raw_rew_rule = loc * constr * bool * raw_tactic_expr +type raw_rew_rule = Loc.t * constr Univ.in_universe_context_set * bool * raw_tactic_expr option (* Applies all the rules of one base *) let one_base general_rewrite_maybe_in tac_main bas = let lrul = find_rewrites bas in - let lrul = List.map (fun h -> (h.rew_lemma,h.rew_l2r,Tacinterp.eval_tactic h.rew_tac)) lrul in - tclREPEAT_MAIN (tclPROGRESS (List.fold_left (fun tac (csr,dir,tc) -> - tclTHEN tac - (tclREPEAT_MAIN - (tclTHENFIRST (general_rewrite_maybe_in dir csr tc) tac_main))) - tclIDTAC lrul)) + let try_rewrite dir ctx c tc = Proofview.Goal.nf_enter (fun gl -> + let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in + let c' = Vars.subst_univs_level_constr subst c in + let sigma = Proofview.Goal.sigma gl in + let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx' in + Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (general_rewrite_maybe_in dir c' tc) + ) in + let lrul = List.map (fun h -> + let tac = match h.rew_tac with None -> Proofview.tclUNIT () | Some t -> Tacinterp.eval_tactic t in + (h.rew_ctx,h.rew_lemma,h.rew_l2r,tac)) lrul in + Tacticals.New.tclREPEAT_MAIN (Proofview.tclPROGRESS (List.fold_left (fun tac (ctx,csr,dir,tc) -> + Tacticals.New.tclTHEN tac + (Tacticals.New.tclREPEAT_MAIN + (Tacticals.New.tclTHENFIRST (try_rewrite dir ctx csr tc) tac_main))) + (Proofview.tclUNIT()) lrul)) (* The AutoRewrite tactic *) let autorewrite ?(conds=Naive) tac_main lbas = - tclREPEAT_MAIN (tclPROGRESS + Tacticals.New.tclREPEAT_MAIN (Proofview.tclPROGRESS (List.fold_left (fun tac bas -> - tclTHEN tac + Tacticals.New.tclTHEN tac (one_base (fun dir c tac -> - let tac = tac, conds in - general_rewrite dir all_occurrences true false ~tac c) + let tac = (tac, conds) in + general_rewrite dir AllOccurrences true false ~tac c) tac_main bas)) - tclIDTAC lbas)) + (Proofview.tclUNIT()) lbas)) -let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas : tactic = - fun gl -> +let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas = + Proofview.Goal.nf_enter begin fun gl -> (* let's check at once if id exists (to raise the appropriate error) *) - let _ = List.map (Tacmach.pf_get_hyp gl) idl in + 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 @@ -133,15 +131,15 @@ let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas : tactic = match Tacmach.pf_hyps gl with (last_hyp_id,_,_)::_ -> last_hyp_id | _ -> (* even the hypothesis id is missing *) - error ("No such hypothesis: " ^ (string_of_id !id) ^".") + raise (Logic.RefinerError (Logic.NoSuchHyp !id)) in - let gl' = general_rewrite_in dir all_occurrences true ~tac:(tac, conds) false !id cstr false gl 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 (lastid,_,_)::_ -> - if last_hyp_id <> lastid then + if not (Id.equal last_hyp_id lastid) then begin let gl'' = if !to_be_cleared then @@ -159,11 +157,13 @@ let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas : tactic = | _ -> assert false) (* there must be at least an hypothesis *) | _ -> assert false (* rewriting cannot complete a proof *) in - tclMAP (fun id -> - tclREPEAT_MAIN (tclPROGRESS + let general_rewrite_in x y z w = Proofview.V82.tactic (general_rewrite_in x y z w) in + Tacticals.New.tclMAP (fun id -> + Tacticals.New.tclREPEAT_MAIN (Proofview.tclPROGRESS (List.fold_left (fun tac bas -> - tclTHEN tac (one_base (general_rewrite_in id) tac_main bas)) tclIDTAC lbas))) - idl gl + Tacticals.New.tclTHEN tac (one_base (general_rewrite_in id) tac_main bas)) (Proofview.tclUNIT()) lbas))) + idl + end let autorewrite_in ?(conds=Naive) id = autorewrite_multi_in ~conds [id] @@ -171,53 +171,48 @@ let gen_auto_multi_rewrite conds tac_main lbas cl = let try_do_hyps treat_id l = autorewrite_multi_in ~conds (List.map treat_id l) tac_main lbas in - if cl.concl_occs <> all_occurrences_expr & - cl.concl_occs <> no_occurrences_expr + if cl.concl_occs != AllOccurrences && + cl.concl_occs != NoOccurrences then - error "The \"at\" syntax isn't available yet for the autorewrite tactic." + Proofview.tclZERO (UserError("" , str"The \"at\" syntax isn't available yet for the autorewrite tactic.")) else let compose_tac t1 t2 = match cl.onhyps with | Some [] -> t1 - | _ -> tclTHENFIRST t1 t2 + | _ -> Tacticals.New.tclTHENFIRST t1 t2 in compose_tac - (if cl.concl_occs <> no_occurrences_expr then autorewrite ~conds tac_main lbas else tclIDTAC) + (if cl.concl_occs != NoOccurrences then autorewrite ~conds tac_main lbas else Proofview.tclUNIT ()) (match cl.onhyps with | Some l -> try_do_hyps (fun ((_,id),_) -> id) l | None -> - fun gl -> (* try to rewrite in all hypothesis (except maybe the rewritten one) *) - let ids = Tacmach.pf_ids_of_hyps gl - in try_do_hyps (fun id -> id) ids 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) -let auto_multi_rewrite ?(conds=Naive) = gen_auto_multi_rewrite conds Refiner.tclIDTAC +let auto_multi_rewrite ?(conds=Naive) = gen_auto_multi_rewrite conds (Proofview.tclUNIT()) -let auto_multi_rewrite_with ?(conds=Naive) tac_main lbas cl gl = - let onconcl = cl.Tacexpr.concl_occs <> no_occurrences_expr in - match onconcl,cl.Tacexpr.onhyps with +let auto_multi_rewrite_with ?(conds=Naive) tac_main lbas cl = + let onconcl = match cl.Locus.concl_occs with NoOccurrences -> false | _ -> true in + match onconcl,cl.Locus.onhyps with | false,Some [_] | true,Some [] | false,Some [] -> (* autorewrite with .... in clause using tac n'est sur que si clause represente soit le but soit UNE hypothese *) - gen_auto_multi_rewrite conds tac_main lbas cl gl + gen_auto_multi_rewrite conds tac_main lbas cl | _ -> - Util.errorlabstrm "autorewrite" - (strbrk "autorewrite .. in .. using can only be used either with a unique hypothesis or on the conclusion.") + Proofview.tclZERO (UserError ("autorewrite",strbrk "autorewrite .. in .. using can only be used either with a unique hypothesis or on the conclusion.")) (* Functions necessary to the library object declaration *) let cache_hintrewrite (_,(rbase,lrl)) = - let base = - try find_base rbase - with e when Errors.noncritical e -> HintDN.empty - in - let max = - try fst (Util.list_last (HintDN.find_all base)) - with e when Errors.noncritical e -> 0 + let base = try raw_find_base rbase with Not_found -> HintDN.empty in + let max = try fst (Util.List.last (HintDN.find_all base)) with Failure _ -> 0 in let lrl = HintDN.map (fun (i,h) -> (i + max, h)) lrl in - rewtab:=Stringmap.add rbase (HintDN.union lrl base) !rewtab + rewtab:=String.Map.add rbase (HintDN.union lrl base) !rewtab let subst_hintrewrite (subst,(rbase,list as node)) = @@ -250,12 +245,6 @@ type hypinfo = { hyp_right : constr; } -let evd_convertible env evd x y = - try - ignore(Unification.w_unify ~flags:Unification.elim_flags env evd Reduction.CONV x y); true - (* try ignore(Evarconv.the_conv_x env x y evd); true *) - with e when Errors.noncritical e -> false - 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 @@ -296,7 +285,7 @@ let find_applied_relation metas loc env sigma c left2right = | Some c -> c | None -> user_err_loc (loc, "decompose_applied_relation", - str"The type" ++ spc () ++ Printer.pr_constr_env env ctype ++ + str"The type" ++ spc () ++ Printer.pr_constr_env env sigma ctype ++ spc () ++ str"of this term does not end with an applied relation.") (* To add rewriting rules to a base *) @@ -304,12 +293,12 @@ let add_rew_rules base lrul = let counter = ref 0 in let lrul = List.fold_left - (fun dn (loc,c,b,t) -> + (fun dn (loc,(c,ctx),b,t) -> let info = find_applied_relation false loc (Global.env ()) Evd.empty 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_l2r = b; - rew_tac = Tacinterp.glob_tactic t} + rew_pat = pat; rew_ctx = ctx; rew_l2r = b; + rew_tac = Option.map Tacintern.glob_tactic t} in incr counter; HintDN.add pat (!counter, rul) dn) HintDN.empty lrul in Lib.add_anonymous_leaf (inHintRewrite (base,lrul)) -- cgit v1.2.3