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
open Lang
open Tactical
let access_update_pattern e =
let open Qed.Logic in
match F.repr e with
| Aget(u,j) ->
begin match F.repr u with
| Aset(a,i,e) -> Some(a,i,e,j)
| _ -> None
end
| _ -> None
class array =
object
inherit Tactical.make ~id:"Wp.array"
~title:"Array"
~descr:"Decompose access-update patterns"
~params:[]
method select feedback (s : Tactical.selection) =
let e = Tactical.selected s in
match access_update_pattern e with
| None -> Not_applicable
| Some(a,i,v,j) ->
ignore feedback ;
let at = Tactical.at s in
let cases = [
"Same Indices" , F.p_equal i j , e , v ;
"Diff Indices" , F.p_neq i j , e , F.e_get a j ;
] in
Applicable (Tactical.rewrite ?at cases)
end
let tactical = Tactical.export (new array)
let strategy = Strategy.make tactical ~arguments:[]