Source file records.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
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
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
open Format
open Options
open Sig
module Hs = Hstring
module E = Expr
type 'a abstract =
| Record of (Hs.t * 'a abstract) list * Ty.t
| Access of Hs.t * 'a abstract * Ty.t
| Other of 'a * Ty.t
module type ALIEN = sig
include Sig.X
val embed : r abstract -> r
end
module Shostak (X : ALIEN) = struct
module XS = Set.Make(struct type t = X.r let compare = X.hash_cmp end)
let name = "records"
type t = X.r abstract
type r = X.r
module Debug = struct
let rec print fmt = function
| Record (lbs, _) ->
fprintf fmt "{";
let _ = List.fold_left
(fun first (lb, e) ->
fprintf fmt "%s%s = %a"
(if first then "" else "; ") (Hs.view lb) print e;
false
) true lbs in
fprintf fmt "}"
| Access(a, e, _) ->
fprintf fmt "%a.%s" print e (Hs.view a)
| Other(t, _) -> X.print fmt t
end
let print = Debug.print
let rec raw_compare r1 r2 =
match r1, r2 with
| Other (u1, ty1), Other (u2, ty2) ->
let c = Ty.compare ty1 ty2 in
if c <> 0 then c else X.str_cmp u1 u2
| Other _, _ -> -1
| _, Other _ -> 1
| Access (s1, u1, ty1), Access (s2, u2, ty2) ->
let c = Ty.compare ty1 ty2 in
if c <> 0 then c
else
let c = Hs.compare s1 s2 in
if c <> 0 then c
else raw_compare u1 u2
| Access _, _ -> -1
| _, Access _ -> 1
| Record (lbs1, ty1), Record (lbs2, ty2) ->
let c = Ty.compare ty1 ty2 in
if c <> 0 then c else raw_compare_list lbs1 lbs2
and raw_compare_list l1 l2 =
match l1, l2 with
| [], [] -> 0
| [], _ -> 1
| _, [] -> -1
| (_, x1)::l1, (_, x2)::l2 ->
let c = raw_compare x1 x2 in
if c<>0 then c else raw_compare_list l1 l2
let rec normalize v =
match v with
| Record (lbs, ty) ->
begin
let lbs_n = List.map (fun (lb, x) -> lb, normalize x) lbs in
match lbs_n with
| (lb1, Access(lb2, x, _)) :: l when Hs.equal lb1 lb2 ->
if List.for_all
(function
| (lb1, Access(lb2, y, _)) ->
Hs.equal lb1 lb2 && raw_compare x y = 0
| _ -> false) l
then x
else Record (lbs_n, ty)
| _ -> Record (lbs_n, ty)
end
| Access (a, x, ty) ->
begin
match normalize x with
| Record (lbs, _) -> Hs.list_assoc a lbs
| x_n -> Access (a, x_n, ty)
end
| Other _ -> v
let embed r =
match X.extract r with
| Some p -> p
| None -> Other(r, X.type_info r)
let compare_mine t u = raw_compare (normalize t) (normalize u)
let compare x y = compare_mine (embed x) (embed y)
let rec equal r1 r2 =
match r1, r2 with
| Other (u1, ty1), Other (u2, ty2) ->
Ty.equal ty1 ty2 && X.equal u1 u2
| Access (s1, u1, ty1), Access (s2, u2, ty2) ->
Hs.equal s1 s2 && Ty.equal ty1 ty2 && equal u1 u2
| Record (lbs1, ty1), Record (lbs2, ty2) ->
Ty.equal ty1 ty2 && equal_list lbs1 lbs2
| Other _, _ | _, Other _ | Access _, _ | _, Access _ -> false
and equal_list l1 l2 =
try List.for_all2 (fun (_,r1) (_,r2) -> equal r1 r2) l1 l2
with Invalid_argument _ -> false
let is_mine t =
match normalize t with
| Other(r, _) -> r
| x -> X.embed x
let type_info = function
| Record (_, ty) | Access (_, _, ty) | Other (_, ty) -> ty
let make t =
let rec make_rec t ctx =
let { E.f; xs; ty; _ } =
match E.term_view t with
| E.Not_a_term _ -> assert false
| E.Term tt -> tt
in
match f, ty with
| Symbols.Op (Symbols.Record), Ty.Trecord { Ty.lbs; _ } ->
assert (List.length xs = List.length lbs);
let l, ctx =
List.fold_right2
(fun x (lb, _) (l, ctx) ->
let r, ctx = make_rec x ctx in
let tyr = type_info r in
let dlb = E.mk_term (Symbols.Op (Symbols.Access lb)) [t] tyr in
let c = E.mk_eq ~iff:false dlb x in
(lb, r)::l, c::ctx
)
xs lbs ([], ctx)
in
Record (l, ty), ctx
| Symbols.Op (Symbols.Access a), _ ->
begin
match xs with
| [x] ->
let r, ctx = make_rec x ctx in
Access (a, r, ty), ctx
| _ -> assert false
end
| _, _ ->
let r, ctx' = X.make t in
Other (r, ty), ctx'@ctx
in
let r, ctx = make_rec t [] in
let is_m = is_mine r in
is_m, ctx
let color _ = assert false
let embed r =
match X.extract r with
| Some p -> p
| None -> Other(r, X.type_info r)
let xs_of_list = List.fold_left (fun s x -> XS.add x s) XS.empty
let leaves t =
let rec leaves t =
match normalize t with
| Record (lbs, _) ->
List.fold_left (fun s (_, x) -> XS.union (leaves x) s) XS.empty lbs
| Access (_, x, _) -> leaves x
| Other (x, _) -> xs_of_list (X.leaves x)
in
XS.elements (leaves t)
let rec hash = function
| Record (lbs, ty) ->
List.fold_left
(fun h (lb, x) -> 17 * hash x + 13 * Hs.hash lb + h)
(Ty.hash ty) lbs
| Access (a, x, ty) ->
19 * hash x + 17 * Hs.hash a + Ty.hash ty
| Other (x, ty) ->
Ty.hash ty + 23 * X.hash x
let rec subst_rec p v r =
match r with
| Other (t, _) ->
embed (if X.equal p t then v else X.subst p v t)
| Access (a, t, ty) ->
Access (a, subst_rec p v t, ty)
| Record (lbs, ty) ->
let lbs = List.map (fun (lb, t) -> lb, subst_rec p v t) lbs in
Record (lbs, ty)
let subst p v r = is_mine (subst_rec p v r)
let is_mine_symb_aux sy = match sy with
| Symbols.Op (Symbols.Record | Symbols.Access _) -> true
| _ -> false
let is_mine_symb sy _ty = is_mine_symb_aux sy
let abstract_access field e ty acc =
let xe = is_mine e in
let abs_right_xe, acc =
try List.assoc xe acc, acc
with Not_found ->
let left_abs_xe2, acc = X.abstract_selectors xe acc in
match X.type_info left_abs_xe2 with
| (Ty.Trecord { Ty.lbs; _ }) as tyr ->
let flds =
List.map
(fun (lb,ty) -> lb, embed (X.term_embed (E.fresh_name ty))) lbs
in
let record = is_mine (Record (flds, tyr)) in
record, (left_abs_xe2, record) :: acc
| _ -> assert false
in
let abs_access = normalize (Access (field, embed abs_right_xe, ty)) in
is_mine abs_access, acc
let abstract_selectors v acc =
match v with
| Other _ -> assert false
| Record (fields,ty) ->
let flds, acc =
List.fold_left
(fun (flds,acc) (lbl,e) ->
let e, acc = X.abstract_selectors (is_mine e) acc in
(lbl, embed e)::flds, acc
)([], acc) fields
[@ocaml.ppwarning "TODO: should not rebuild if not changed !"]
in
is_mine (Record (List.rev flds, ty)), acc
| Access (field, e, ty) -> abstract_access field e ty acc
let fully_interpreted = is_mine_symb_aux
let rec r =
match X.extract r with
| Some v -> begin match v with
| Record (lbs, ty) ->
begin
try
let lbs =
List.map
(fun (_, r) ->
match term_extract (is_mine r) with
| None, _ -> raise Not_found
| Some t, _ -> t)
lbs
in
Some (E.mk_term (Symbols.Op Symbols.Record) lbs ty), false
with Not_found -> None, false
end
| Access (a, r, ty) ->
begin
match X.term_extract (is_mine r) with
| None, _ -> None, false
| Some t, _ ->
Some (E.mk_term (Symbols.Op (Symbols.Access a)) [t] ty), false
end
| Other (r, _) -> X.term_extract r
end
| None -> X.term_extract r
let orient_solved p v pb =
if List.mem p (X.leaves v) then raise Util.Unsolvable;
{ pb with sbt = (p,v) :: pb.sbt }
let solve r1 r2 pb =
match embed r1, embed r2 with
| Record (l1, _), Record (l2, _) ->
let eqs =
List.fold_left2
(fun eqs (a,b) (x,y) ->
assert (Hs.compare a x = 0);
(is_mine y, is_mine b) :: eqs
)pb.eqs l1 l2
in
{pb with eqs=eqs}
| Other _, Other _ ->
if X.str_cmp r1 r2 > 0 then { pb with sbt = (r1,r2)::pb.sbt }
else { pb with sbt = (r2,r1)::pb.sbt }
| Other _, Record _ -> orient_solved r1 r2 pb
| Record _, Other _ -> orient_solved r2 r1 pb
| Access _ , _ -> assert false
| _ , Access _ -> assert false
let make t =
if Options.get_timers() then
try
Timers.exec_timer_start Timers.M_Records Timers.F_make;
let res = make t in
Timers.exec_timer_pause Timers.M_Records Timers.F_make;
res
with e ->
Timers.exec_timer_pause Timers.M_Records Timers.F_make;
raise e
else make t
let solve r1 r2 pb =
if Options.get_timers() then
try
Timers.exec_timer_start Timers.M_Records Timers.F_solve;
let res = solve r1 r2 pb in
Timers.exec_timer_pause Timers.M_Records Timers.F_solve;
res
with e ->
Timers.exec_timer_pause Timers.M_Records Timers.F_solve;
raise e
else solve r1 r2 pb
let assign_value t _ eq =
match embed t with
| Access _ -> None
| Record (_, ty) ->
if List.exists (fun (t,_) -> Expr.const_term t) eq
then None
else Some (Expr.fresh_name ty, false)
| Other (_,ty) ->
match ty with
| Ty.Trecord { Ty.lbs; _ } ->
let rev_lbs = List.rev_map (fun (_, ty) -> Expr.fresh_name ty) lbs in
let s = E.mk_term (Symbols.Op Symbols.Record) (List.rev rev_lbs) ty in
Some (s, false)
| _ -> assert false
let choose_adequate_model _ _ l =
let acc =
List.fold_left
(fun acc (s, r) ->
if not (Expr.const_term s) then acc
else
match acc with
| Some(s', _) when Expr.compare s' s > 0 -> acc
| _ -> Some (s, r)
) None l
in
match acc with
| Some (_,r) ->
r, asprintf "%a" X.print r
| _ -> assert false
end