summaryrefslogtreecommitdiff
path: root/tactics/autorewrite.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/autorewrite.ml')
-rw-r--r--tactics/autorewrite.ml112
1 files changed, 40 insertions, 72 deletions
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 *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Equality
open Names
open Pp
-open Tacticals
-open Tactics
-open Term
+open Constr
open Termops
open CErrors
open Util
open Mod_subst
open Locus
-open Proofview.Notations
(* Rewriting rules *)
type rew_rule = { rew_lemma: constr;
rew_type: types;
rew_pat: constr;
- rew_ctx: Univ.universe_context_set;
+ rew_ctx: Univ.ContextSet.t;
rew_l2r: bool;
rew_tac: Genarg.glob_generic_argument option }
@@ -65,7 +64,7 @@ let raw_find_base bas = String.Map.find bas !rewtab
let find_base bas =
try raw_find_base bas
with Not_found ->
- 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;
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-07 23:46:36 +0000