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
|
open Ast
open Coqast
open Equality
open Hipattern
open Names
open Pp
open Proof_type
open Tacmach
open Tacinterp
open Tactics
open Term
open Util
open Vernacinterp
(* Rewriting rules *)
type rew_rule = constr * bool * tactic
(* Summary and Object declaration *)
let rewtab =
ref ((Hashtbl.create 53) : (string,rew_rule) Hashtbl.t)
let lookup id = Hashtbl.find id !rewtab
let _ =
let init () = rewtab := (Hashtbl.create 53) 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_section = false }
(* Rewriting rules before tactic interpretation *)
type raw_rew_rule = constr * bool * t
(* Applies all the rules of one base *)
let one_base tac_main bas =
let lrul = Hashtbl.find_all !rewtab bas in
if lrul = [] then
errorlabstrm "AutoRewrite"
[<'sTR ("Rewriting base "^(bas)^" does not exist") >]
else
tclREPEAT_MAIN (tclPROGRESS (List.fold_left (fun tac (csr,dir,tc) ->
tclTHEN tac
(if dir then tclREPEAT_MAIN (tclTHENST (rewriteLR csr) [tac_main] tc)
else tclREPEAT_MAIN (tclTHENST (rewriteRL 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 load_hintrewrite _ = ()
let cache_hintrewrite (_,(rbase,lrl)) =
List.iter
(fun (c,b,t) -> Hashtbl.add !rewtab rbase (c,b,Tacinterp.interp t)) lrl
let export_hintrewrite x = Some x
(* Declaration of the Hint Rewrite library object *)
let (in_hintrewrite,out_hintrewrite)=
Libobject.declare_object
("HINT_REWRITE",
{ Libobject.load_function = load_hintrewrite;
Libobject.open_function = cache_hintrewrite;
Libobject.cache_function = cache_hintrewrite;
Libobject.export_function = export_hintrewrite })
(* To add rewriting rules to a base *)
let add_rew_rules base lrul =
Lib.add_anonymous_leaf (in_hintrewrite (base,lrul))
(* The vernac declaration of HintRewrite *)
let _ = vinterp_add "HintRewrite"
(function
| [VARG_STRING ort;VARG_CONSTRLIST lcom;VARG_IDENTIFIER id;VARG_TACTIC t]
when ort = "LR" || ort = "RL" ->
(fun () ->
let (evc,env) = Command.get_current_context () in
let lcsr =
List.map (function
| Node(loc,"CONSTR",l) ->
constr_of_Constr (interp_tacarg
(evc,env,[],[],None,Tactic_debug.DebugOff)
(Node(loc,"COMMAND",l)))
| _ -> bad_vernac_args "HintRewrite") lcom in
add_rew_rules (string_of_id id)
(List.map (fun csr -> (csr,ort = "LR",t)) lcsr))
| _ -> bad_vernac_args "HintRewrite")
(* To get back the tactic arguments and call AutoRewrite *)
let v_autorewrite = function
| (Tac (t,_))::l ->
let lbas =
List.map (function
| Identifier id -> string_of_id id
| _ -> Tacinterp.bad_tactic_args "AutoRewrite") l in
autorewrite t lbas
| l ->
let lbas =
List.map (function
| Identifier id -> string_of_id id
| _ -> Tacinterp.bad_tactic_args "AutoRewrite") l in
autorewrite tclIDTAC lbas
(* Declaration of AutoRewrite *)
let _ = hide_tactic "AutoRewrite" v_autorewrite
|
