1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Ast
open Coqast
open Equality
open Hipattern
open Names
open Pp
open Proof_type
open Tacticals
open Tacinterp
open Tactics
open Term
open Util
open Vernacinterp
open Tacexpr
open Mod_subst
(* Rewriting rules *)
(* the type is the statement of the lemma constr. Used to elim duplicates. *)
type rew_rule = constr * types * bool * glob_tactic_expr
(* Summary and Object declaration *)
let rewtab =
ref (Stringmap.empty : rew_rule list Stringmap.t)
let _ =
let init () = rewtab := Stringmap.empty in
let freeze () = !rewtab in
let unfreeze fs = rewtab := fs in
Summary.declare_summary "autorewrite"
{ Summary.freeze_function = freeze;
Summary.unfreeze_function = unfreeze;
Summary.init_function = init;
Summary.survive_module = false;
Summary.survive_section = false }
type raw_rew_rule = constr * bool * raw_tactic_expr
(* Applies all the rules of one base *)
let one_base tac_main bas =
let lrul =
try
Stringmap.find bas !rewtab
with Not_found ->
errorlabstrm "AutoRewrite"
(str ("Rewriting base "^(bas)^" does not exist"))
in
let lrul = List.map (fun (c,_,b,t) -> (c,b,Tacinterp.eval_tactic t)) lrul in
tclREPEAT_MAIN (tclPROGRESS (List.fold_left (fun tac (csr,dir,tc) ->
tclTHEN tac
(tclREPEAT_MAIN
(tclTHENSFIRSTn (general_rewrite dir csr) [|tac_main|] tc)))
tclIDTAC lrul))
(* The AutoRewrite tactic *)
let autorewrite tac_main lbas =
tclREPEAT_MAIN (tclPROGRESS
(List.fold_left (fun tac bas ->
tclTHEN tac (one_base tac_main bas)) tclIDTAC lbas))
(* Functions necessary to the library object declaration *)
let cache_hintrewrite (_,(rbase,lrl)) =
let l =
try
let oldl = Stringmap.find rbase !rewtab in
let lrl =
List.map
(fun (c,dummy,b,t) ->
(* here we substitute the dummy value with the right one *)
c,Typing.type_of (Global.env ()) Evd.empty c,b,t) lrl in
List.rev_append
(List.filter
(fun (_,typ,_,_) ->
not (List.exists (fun (_,typ',_,_) -> Term.eq_constr typ typ') oldl)
) lrl) oldl
with
| Not_found -> List.rev lrl
in
rewtab:=Stringmap.add rbase l !rewtab
let export_hintrewrite x = Some x
let subst_hintrewrite (_,subst,(rbase,list as node)) =
let subst_first (cst,typ,b,t as pair) =
let cst' = subst_mps subst cst in
let typ' =
(* here we do not have the environment and Global.env () is not the
one where cst' lives in. Thus we can just put a dummy value and
override it in cache_hintrewrite *)
typ (* dummy value, it will be recomputed by cache_hintrewrite *) in
let t' = Tacinterp.subst_tactic subst t in
if cst == cst' && t == t' then pair else
(cst',typ',b,t)
in
let list' = list_smartmap subst_first list in
if list' == list then node else
(rbase,list')
let classify_hintrewrite (_,x) = Libobject.Substitute x
(* Declaration of the Hint Rewrite library object *)
let (in_hintrewrite,out_hintrewrite)=
Libobject.declare_object {(Libobject.default_object "HINT_REWRITE") with
Libobject.open_function = (fun i o -> if i=1 then cache_hintrewrite o);
Libobject.cache_function = cache_hintrewrite;
Libobject.subst_function = subst_hintrewrite;
Libobject.classify_function = classify_hintrewrite;
Libobject.export_function = export_hintrewrite }
(* To add rewriting rules to a base *)
let add_rew_rules base lrul =
let lrul =
List.rev_map
(fun (c,b,t) ->
(c,mkProp (* dummy value *), b,Tacinterp.glob_tactic t)
) lrul
in
Lib.add_anonymous_leaf (in_hintrewrite (base,lrul))
|
