Source file TacRewrite.ml
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
open Tactical
open Repr
let rewrite ~select ~replaced ~value =
Applicable
(Tactical.rewrite
?at:(Tactical.at select)
[ "Rewrite" , Lang.F.p_true , replaced , value ])
let hypothesis s =
let open Conditions in
match s.condition with
| When p | Have p | Core p | Init p -> p
| _ -> raise Not_found
let clause = function
| Clause(Step s) -> hypothesis s
| Inside(Step s,e) ->
begin
match Repr.pred (hypothesis s) with
| And es when List.memq e es -> Lang.F.p_bool e
| _ -> raise Not_found
end
| _ -> raise Not_found
class rewrite dir =
let id = if dir then "Wp.TacRewrite.Left" else "Wp.TacRewrite.Right" in
let title = if dir then "Rewrite (<-)" else "Rewrite (->)" in
object
inherit Tactical.make
~id ~title ~descr:"Rewrite from equality." ~params:[]
method select _feedback select =
try
let p = clause select in
match Repr.pred p with
| Eq(a,b) ->
let replaced,value = if dir then a,b else b,a in
rewrite ~select ~replaced ~value
| _ -> Not_applicable
with Not_found -> Not_applicable
end
let tacl = Tactical.export (new rewrite true :> Tactical.tactical)
let tacr = Tactical.export (new rewrite false :> Tactical.tactical)
let mem a b =
let rec walk m e =
if a==e then raise Exit ;
if not (Lang.F.Tset.mem e !m) then
begin
m := Lang.F.Tset.add e !m ;
Lang.F.lc_iter (walk m) e
end
in try walk (ref Lang.F.Tset.empty) b ; false with Exit -> true
let direct a goal =
match Repr.term goal with
| Eq(u,v) when a == u || a == v -> true
| _ -> false
let submit push select e goal rw =
if direct e goal then
push (Strategy.make ~priority:1.5 rw select)
else
if mem e goal then
push (Strategy.make ~priority:0.5 rw select)
let rec lookup step push goal e =
match Repr.term e with
| And ps -> List.iter (lookup step push goal) ps
| Eq(a,b) ->
begin
let select = Inside(Step step,e) in
submit push select a goal tacl ;
submit push select b goal tacr ;
end
| _ -> ()
class auto_rewrite =
object
method id = "wp:replace"
method title = "Auto Replace"
method descr = "Lookup for equalities to rewrite with."
method search (push : Strategy.strategy -> unit) (hyps,goal) =
Conditions.iter
(fun s ->
let open Conditions in
match s.condition with
| Have p | When p | Core p | Init p ->
lookup s push (Lang.F.e_prop goal) (Lang.F.e_prop p)
| _ -> ())
hyps
end
let () = Strategy.register (new auto_rewrite)
type dir = [ `Left | `Right ]
let tactical = function
| `Left -> tacl
| `Right -> tacr
let strategy ?priority dir selection =
Strategy.make ?priority (tactical dir) selection