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
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
module F = Lang.F
let iter f e =
let q = Queue.create () in
Queue.add e q ;
while not (Queue.is_empty q) do
let e = Queue.pop q in
if F.lc_closed e then f e ;
F.lc_iter (fun e -> Queue.push e q) e
done
let once f e =
let q = Queue.create () in
let m = ref F.Tset.empty in
let once m e =
if F.Tset.mem e !m then false else (m := F.Tset.add e !m ; true) in
Queue.add e q ;
while not (Queue.is_empty q) do
let e = Queue.pop q in
if F.lc_closed e then f e ;
F.lc_iter (fun e -> if once m e then Queue.push e q) e
done
let head_fields = function
| [] -> ""
| (Lang.Mfield(mdt,_,_,_),_)::_ -> mdt.Lang.ext_debug
| (Lang.Cfield(fd, _),_):: _ -> let open Cil_types in fd.fcomp.cname
let head e =
let open Qed.Logic in
match F.repr e with
| Kint z -> Z.to_string z
| Kreal r -> Q.to_string r
| Fvar x -> Printf.sprintf "$%s" (F.Var.basename x)
| Bvar(k,_) -> Printf.sprintf "#%d" k
| True -> "T"
| False -> "F"
| And _ -> "&"
| Or _ -> "|"
| Not _ -> "!"
| Imply _ -> ">"
| Eq _ -> "="
| Lt _ -> "<"
| Leq _ -> "<="
| Neq _ -> "~"
| Add _ -> "+"
| Mul _ -> "*"
| Times(k,_) -> Printf.sprintf ".%s" (Z.to_string k)
| Div _ -> "/"
| Mod _ -> "%"
| If _ -> "?"
| Aget _ -> "[]"
| Acst _ -> "[.]"
| Aset _ -> "[=]"
| Rget(_,fd) -> Format.asprintf ".%a" Lang.Field.pretty fd
| Rdef fds -> Format.asprintf "{%s}" (head_fields fds)
| Fun(f,_) -> Pretty_utils.to_string Lang.Fun.pretty f
| Apply _ -> "()"
| Bind(Forall,_,_) -> "\\F"
| Bind(Exists,_,_) -> "\\E"
| Bind(Lambda,_,_) -> "\\L"
let pattern e =
let buffer = Buffer.create 32 in
(try
iter (fun e ->
Buffer.add_string buffer (head e) ;
if Buffer.length buffer >= 32 then raise Exit)
e
with Exit -> ()) ;
Buffer.contents buffer
let _prefix m k m' =
let n = String.length m in
let n' = String.length m' in
k+n' <= n &&
(try for i = 0 to n'-1 do
if m.[k+i] != m'.[i] then raise Exit
done ; true
with Exit -> false)
let matches fp e =
let fe = pattern e in
fp = fe
type occurrence = int * string
exception Located of occurrence
exception Found of F.term
let locate ~select ~inside =
let k = ref 0 in
let m = pattern select in
try
once
(fun e ->
if e == select then raise (Located(!k,m)) ;
if matches m e then incr k ;
) inside ;
raise Not_found
with Located fp -> fp
let lookup ~occur ~inside =
let k = ref (succ (fst occur)) in
let m = snd occur in
try
once
(fun e ->
if matches m e then decr k ;
if !k = 0 then raise (Found e) ;
) inside ;
raise Not_found
with Found e -> e