1:- module(cil, [unify/2,
2 find_key/3,
3 role/3,
4 close_btree/1,
5 distribute_constr/2,
6 region_constr_of_leaves/4
7 ]). 8:- use_module([
9 library(lists),
10 library(sort),
11 library(ordsets)]). 12
16
17 21
24put_attr(X, Attr):- put_attr(X, cil, Attr).
25get_attr(X, Attr):- get_attr(X, cil, Attr).
26
28attr_unify_hook(V, Y):-
29 ( nonvar(Y)
30 -> attr_unify(V, Y)
31 ; ( get_attr(Y, A)
32 -> attr_unify(V, A, Y)
33 ; put_attr(Y, V)
34 )
35 ).
36
40attr_unify(btree(X), Y):- is_btree(Y), !, unify(X, Y).
41attr_unify(con(Rgn, _), Y):- is_btree(Y), !,
42 distribute_constr(Y, Rgn).
43attr_unify(_, _).
44
50
51attr_unify(btree(X), btree(Y), _):- unify(X, Y).
52attr_unify(btree(X), con(Rgn, D), Z):-
53 distribute_constr(X, Rgn),
54 put_attr(Z, con(Rgn, D), Z),
55 subsume(X, D).
56attr_unify(con(Rgn, Y), btree(D), Z):-
57 distribute_constr(D, Rgn),
58 put_attr(Z, con(Rgn, Y)),
59 subsume(D, Y).
60attr_unify(con(Rgn, Y), con(Rgn0, Y0), Z):-
61 meet_region(Rgn, Rgn0, Rgn1),
62 add_only_new(Y, Y0, Y1),
63 put_attr(Z, con(Rgn1, Y1)),
64 unify(Y, Y0).
65
66 69
89
90
91 94
106
107is_btree(t(_,_,_,_)).
108is_btree({}).
110apply_constr(X, con(I,_)):- distribute_constr(X, I).
111
115distribute_constr(X, Rgn):- var(X), !,
116 ( get_attr(X, A)
117 -> ( A = con(RgnA, D)
118 -> meet_region(RgnA, Rgn, RgnA0),
119 put_attr(X, con(RgnA0, D))
120 ; A = btree(A0),
121 distribute_constr(A0, Rgn)
122 )
123 ; put_attr(X, con(Rgn, []))
124 ).
125distribute_constr({}, _):-!.
126distribute_constr(t(K,_,L,R), Rgn):-
127 has_member(Rgn, K),
128 meet_region(Rgn, lower(K), LowK),
129 meet_region(Rgn, upper(K), UppK),
130 distribute_constr(L, LowK),
131 distribute_constr(R, UppK).
132
137
138region_constr_of_leaves(X, Rgn, P, Q):- odict_child(X, K, _, L, R), !,
139 meet_region(lower(K), Rgn, RgnL),
140 region_constr_of_leaves(L, RgnL, P, P0),
141 meet_region(upper(K), Rgn, RgnR),
142 region_constr_of_leaves(R, RgnR, P0, Q).
143region_constr_of_leaves(X, Rgn, [put_attr(X, con(Rgn, []))|P], P):- var(X), !.
144region_constr_of_leaves(_, _, P, P).
145
149
150unify(X, Y):- (attvar(X); attvar(Y)), !, X=Y.
151unify(X, Y):- (var(X); var(Y)), !, X=Y.
152unify(X, Y):- is_btree(X), is_btree(Y), !, subsume(X, Y).
153unify(X, X). 154
159subsume(X, Y):-attvar(X), !,
160 get_attr(X, A),
161 ( A=btree(T)
162 -> subsume(T, Y)
163 ; A=con(Rgn, S),
164 add_only_new([Y], S, S0), 165 put_attr(X, con(Rgn, S0))
166 ).
167subsume(X, Y):-var(X), !,
168 put_attr(X, con(total, [Y])).
169subsume(t(K,V,L,R), Y):-
170 find_key(Y, K, U),
171 unify(V, U),
172 subsume(L, Y),
173 subsume(R, Y).
174
178
179odict_child(X, K, V, L, R):- var(X), !,
180 get_attr(X, A),
181 A=btree(t(K, V, L, R)).
182odict_child(t(K, V, L, R), K, V, L, R).
183
186
192
193close_btree(X):- odict_child(X, _, _, L, R), !,
194 close_btree(L),
195 close_btree(R).
196close_btree([]):-!.
197close_btree(t(_, _, L, R)):-close_btree(L),
198 close_btree(R).
199
200
203
206
211
212odict_equal(X, Y):- odict_equal_stack([X],[Y]).
213
215odict_equal_stack(X, Y):- skip_leaves(X, X0),
216 skip_leaves(Y, Y0),
217 odict_equal_pair(X0, Y0).
219odict_equal_pair([],[]).
220odict_equal_pair([pair(K, V)|L],[pair(K, U)|M]):-
221 odict_equal_arg(V, U),
222 odict_equal_stack(L, M).
224odict_equal_arg(X, Y):- var(X), var(Y), X==Y, !.
225odict_equal_arg(X, Y):-
226 ( odict_child(X, K, V, L, R)
227 -> ( odict_child(Y, K0, V0, L0, R0)
228 -> odict_equal_stack( [L, pair(K, V), R],
229 [L0, pair(K0, V0), R0])
230 ; false
231 )
232 ; ( odict_child(Y, _, _, _, _)
233 -> false
234 ; odict_equal_non_bt(X, Y)
235 )
236 ).
238odict_equal_non_bt(X, Y):- (var(X); var(Y)), !, X==Y.
239odict_equal_non_bt(X, Y):- (atomic(X); atomic(Y)), !, X==Y.
240odict_equal_non_bt(X, Y):- X=..[F|Xs],
241 Y=..[F|Ys],
242 maplist(odict_equal_arg, Xs, Ys).
244skip_leaves([], []).
245skip_leaves([X|Xs], U):- odict_child(X, K, V, L, R),!,
246 skip_leaves([L, pair(K,V), R|Xs], U).
247skip_leaves([X|Xs], U):- (var(X); X==[]), !,
248 skip_leaves(Xs, U).
249skip_leaves(X, X).
250
254
255role(K, X, V):- when(ground(K), find_key(X, K, U)),
256 unify(V, U).
257
259min(X, Y, X):- X@<Y, !.
260min(_, Y, Y).
261
262max(X, Y, Y):- X@<Y, !.
263max(X, _, X).
264
268
272find_key(B, K, V):-
273 ( var(B)
274 -> ( get_attr(B, U)
275 -> ( U=btree(U0)
276 -> find_key(U0, K, V)
277 ; insert_key(U, K, V, B)
278 )
279 ; T = t(K, V, L, R),
280 put_attr(L, con(lower(K),[])),
281 put_attr(R, con(upper(K),[])),
282 put_attr(B, btree(T))
283 )
284 ; B=t(J,U,L,R),
285 ( J==K
286 -> V=U
287 ; ( J @< K
288 -> find_key(R, K, V)
289 ; find_key(L, K, V)
290 )
291 )
292 ).
293
295find_key_list([], _, _).
296find_key_list([Y|Ys], K, V):- find_key(Y, K, V),
297 find_key_list(Ys, K, V).
298
305
306insert_key(con(Rgn, Ys), K, V, N):-
307 has_member(Rgn, K),
308 meet_region(Rgn, lower(K), RgnL),
309 meet_region(Rgn, upper(K), RgnR),
310 put_attr(L, con(RgnL, Ys)),
311 put_attr(R, con(RgnR, Ys)),
312 put_attr(N, btree(t(K, V, L, R))),
313 find_key_list(Ys, K, V).
314
317has_member(total, _).
318has_member(seg(L,R), X):- L@<X, X@<R.
319has_member(lower(U), X):- X@<U.
320has_member(upper(U), X):- U@<X.
321
324
325meet_region(X, Y):- meet_region(X, Y, Z), Z\==[].
326
331
335meet_region(total, X, X).
336meet_region(X, total, X).
337meet_region([], _, []).
338meet_region(_, [], []).
339meet_region(lower(A), lower(B), lower(C)):- min(A, B, C).
340meet_region(lower(A), upper(B), R):-
341 ( B @< A -> R = seg(B, A)
342 ; R = []
343 ).
344meet_region(lower(C), seg(A,B), R):-
345 ( C @=< A -> R = []
346 ; R = seg(A, D),
347 min(B,C,D)
348 ).
349meet_region(upper(A), upper(B), upper(C)):- max(A, B, C).
350meet_region(upper(A), lower(B), R):-
351 ( A @< B -> R = seg(A, B)
352 ; R = []
353 ).
354meet_region(upper(C), seg(A, B), R):-
355 ( C @>= B
356 -> R = []
357 ; R = seg(D, B),
358 max(A, C, D)
359 ).
360meet_region(seg(A, B), lower(C), R):-
361 ( C @=< A -> R = []
362 ; R = seg(A, D),
363 min(B,C,D)
364 ).
365meet_region(seg(A, B), upper(C), R):-
366 ( C @>= B
367 -> R = []
368 ; R = seg(D, B),
369 max(A, C, D)
370 ).
371meet_region(seg(A, B), seg(C, D), M):-
372 max(A,C,L),
373 min(B,D,R),
374 ( L @>= R -> M = []
375 ; M = seg(L, R)
376 ).
377
382
383contain(total,_).
384contain(_, []).
385contain(lower(A), lower(B)) :- B@=<A.
386contain(lower(A), seg(_,B)) :- B@=<A.
387contain(upper(A), upper(B)) :- A@=<B.
388contain(upper(A), seg(B,_)) :- A@=<B.
389contain(seg(A,B), seg(A0, B0)) :- A@=<A0, B0@=<B.
390
392add_only_new([], X, X):- !.
393add_only_new([X|Y], Z, U):- memq(X, Z), !,
394 add_only_new(Y, Z, U).
395add_only_new([X|Y], Z, [X|U]):-
396 add_only_new(Y, Z, U).
398memq(X, [Y|_]):- X==Y, !.
399memq(X, [_|Y]):- memq(X, Y)