1 | | % (c) 2009-2019 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, |
2 | | % Heinrich Heine Universitaet Duesseldorf |
3 | | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) |
4 | | |
5 | | :- module(store, [ %store_values_for_existing_ids/4, |
6 | | store_value_for_existing_id/4, |
7 | | variable_is_defined/2, |
8 | | store_value/4, |
9 | | store_updates_and_normalise/3, |
10 | | store_updates/3, |
11 | | store_intermediate_updates/4, |
12 | | save_updates_in_existing_store/2, |
13 | | %lazy_store_updates_and_normalise/3, |
14 | | merge_updates/3, |
15 | | get_id_value/3, |
16 | | lookup_value/3, |
17 | | lookup_value/4,lookup_value_with_span/5, |
18 | | lookup_value_without_check/4, |
19 | | lookup_value_for_existing_id/3, lookup_value_for_existing_id/4, |
20 | | lookup_and_delete_value/7, |
21 | | no_value_for_variable/2, |
22 | | empty_state/1, |
23 | | add_var_to_localstate/4, |
24 | | set_up_localstate/4, |
25 | | set_up_undefined_localstate/3, set_up_undefined_localstate_with_predefined/4, |
26 | | delete_variables_from_state/3, |
27 | | |
28 | | normalise_value_for_var/3, normalise_value_for_var/4, |
29 | | normalise_value/2, |
30 | | l_normalise_values/2, |
31 | | l_expand_and_normalise_values/2, l_expand_and_normalise_values/3, |
32 | | normalise_store/2, |
33 | | copy_variable_store/4, |
34 | | check_valid_store/2 |
35 | | ]). |
36 | | |
37 | | :- use_module(library(lists)). |
38 | | :- use_module(self_check). |
39 | | :- use_module(debug). |
40 | | |
41 | | :- use_module(typechecker). |
42 | | :- use_module(preferences). |
43 | | :- use_module(tools). |
44 | | |
45 | | :- use_module(bsyntaxtree). |
46 | | |
47 | | :- use_module(error_manager). |
48 | | |
49 | | :- use_module(bmachine, [b_is_constant/1]). |
50 | | |
51 | | :- type variable_id +--> (lambda_res(integer) ; atomic). |
52 | | :- type binding +--> bind(variable_id,any). |
53 | | :- type store +--> list(binding). |
54 | | |
55 | | :- use_module(tools). |
56 | | :- use_module(module_information). |
57 | | :- module_info(group,interpreter). |
58 | | :- module_info(description,'This module takes care of storing B values in an environment and normalising values.'). |
59 | | :- module_info(revision,'$Rev$'). |
60 | | :- module_info(lastchanged,'$LastChangedDate$'). |
61 | | |
62 | | /* --------------------------------------------------------- */ |
63 | | |
64 | | /* store and lookup of values */ |
65 | | |
66 | | |
67 | | :- load_files(library(system), [when(compile_time), imports([environ/2])]). |
68 | | :- if(environ(partially_evaluate, true)). |
69 | | :- use_module(partial_evaluator(pe)). |
70 | | :- unfold(normalise_value(V1,V2),(nonvar(V1);nonvar(V2))). |
71 | | :- unfold(l_expand_and_normalise_values(H,_),nonvar(H)). |
72 | | :- unfold(l_expand_and_normalise_values(H,_,_),nonvar(H)). |
73 | | :- unfold(store_value(_Var,_Value,_Old,_New)). |
74 | | :- unfold(store_value2(Old,Var,_Value,_New),(nonvar(Old),nonvar(Var))). % TO DO: also check whether we can perform the comparison with bind(V,_) in head of Old ! |
75 | | :- unfold(lookup_and_delete_value(_Var,_Value,_T,_UT,_ReportError,_WF,_Finished)). |
76 | | :- unfold(lookup_and_delete_value1(T,Var,_Value,_UT,_ReportError,_WF,_Finished),(nonvar(T),nonvar(Var))). |
77 | | :- unfold(lookup_and_delete_value2(Var2,_Value2,_T,_Var,_Value,_Res,_ReportError,_WF,_Finished), nonvar(Var2)). |
78 | | :- unfold(delete_variables_from_state(A,_,_),nonvar(A)). |
79 | | :- unfold(delete_variable(InState, _, _),nonvar(InState)). |
80 | | :- unfold(store_intermediate_updates(_InStore,_Update,_OutStore,_)). |
81 | | :- unfold(store_intermediate_updates2(A,B,_C,_),(nonvar(A),nonvar(B))). |
82 | | :- unfold(store_intermediate_updates3(Updates,_),nonvar(Updates)). |
83 | | :- unfold(search_and_delete_value(Var,_OldVal,_NewVal,_Updates,_NUpdates),nonvar(Var)). |
84 | | :- unfold(search_and_delete_value2(InStore,_Var,_OldVal,_Value,_OutStore),nonvar(InStore)). |
85 | | :- unfold(search_and_delete_value3(Var2,_Value2,_T,_Var,_OldVal,_Value,_Res),nonvar(Var2)). |
86 | | :- execute(normalise_value_for_var(Var,EXPAND,Val,_Res),(ground(Var),ground(EXPAND),simple_value_for_normalise(Val))). |
87 | | simple_value_for_normalise(V) :- var(V),!,fail. |
88 | | simple_value_for_normalise(fd(_,_)). |
89 | | simple_value_for_normalise(int(_)). |
90 | | simple_value_for_normalise([]). |
91 | | simple_value_for_normalise(string(_)). |
92 | | simple_value_for_normalise(pred_true). simple_value_for_normalise(pred_false). |
93 | | simple_value_for_normalise((A,B)) :- simple_value_for_normalise(A), simsimple_value_for_normaliseple_value(B). |
94 | | |
95 | | :- forward_block(lookup_and_delete_value1(?,?,?,?,?,?,?)) . |
96 | | :- forward_block(lookup_and_delete_value2(?,?,?,?,?,?,?,?,?)) . |
97 | | :- forward_block(search_and_delete_value(?,?,?,?,?)) . |
98 | | :- forward_block(search_and_delete_value2(?,?,?,?,?)) . |
99 | | :- forward_block(search_and_delete_value3(?,?,?,?,?,?,?)) . |
100 | | :- forward_block(store_intermediate_updates2(?,?,?,?)) . |
101 | | :- forward_block(store_intermediate_updates3(?,?)) . |
102 | | :- endif. |
103 | | |
104 | | variable_is_defined(Var,Store) :- safe_member(bind(Var,_),Store,variable_is_defined). |
105 | | |
106 | | store_value(Var,Value,Old,New) :- store_value2(Old,Var,Value,New). |
107 | | store_value2([],Var,Value,[bind(Var,Value)]). |
108 | | store_value2([bind(V,VV)|T],Var,Value,[bind(V,NValue)|UT]) :- |
109 | | ( Var=V -> |
110 | | NValue=Value, UT=T |
111 | | ; otherwise -> |
112 | | NValue=VV, store_value2(T,Var,Value,UT)). |
113 | | |
114 | | |
115 | | store_value_for_existing_id(L,ID,V,L2) :- var(ID),!, |
116 | | add_internal_error('VarID is var !!',store_value_for_existing_id(ID,V,L,L2)),fail. |
117 | | store_value_for_existing_id(L,ID,V,L2) :- store_value_for_existing_id_aux(L,ID,V,L2). |
118 | | store_value_for_existing_id_aux([],Var,Value,[bind(Var,Value)]) :- |
119 | | add_error(store_value_for_existing_id,'Variable does not exist in store: ',Var). |
120 | | store_value_for_existing_id_aux([bind(V,VV)|T],Var,Value,[bind(V,VV2)|UT]) :- |
121 | | (Var=V -> VV2=Value, UT=T |
122 | | ; VV2=VV,store_value_for_existing_id_aux(T,Var,Value,UT)). |
123 | | |
124 | | |
125 | | |
126 | | |
127 | | |
128 | | /* store_intermediate_updates(InState,Updates,OutStates) */ |
129 | | /* rewrote it so that it copies state skeleton even if updates are not yet known */ |
130 | | |
131 | | :- assert_must_succeed((store:store_intermediate_updates([bind(y,1),bind(x,2),bind(a,22)],[bind(x,33)],R,unit_test1),R==[bind(y,1),bind(x,33),bind(a,22)])). |
132 | | :- assert_must_succeed((store:store_intermediate_updates([bind(Y,1),bind(X,2),bind(A,22)],[bind(x,33)],R,unit_test2),X=x,A=a,Y=y,R==[bind(y,1),bind(x,33),bind(a,22)])). |
133 | | |
134 | | |
135 | | |
136 | | store_intermediate_updates(InStore,Update,OutStore,_PP) :- Update==[], !, |
137 | | OutStore=InStore. |
138 | | store_intermediate_updates(InStore,Update,OutStore,PP) :- |
139 | | %print(store_intermediate_updates(InStore,Update,OutStore,PP)),nl, |
140 | | store_intermediate_updates2(InStore,Update,OutStore,ctxt(PP,InStore,Update)). |
141 | | |
142 | | :- block store_intermediate_updates2(-,?,?,?), store_intermediate_updates2(?,-,?,?). |
143 | | store_intermediate_updates2([],Updates,[],PP) :- |
144 | ? | store_intermediate_updates3(Updates,PP). |
145 | | store_intermediate_updates2([bind(Var,OldVal)|InT],Updates,[bind(Var,NewVal)|OutT],PP) :- |
146 | | % TO DO: maybe it would be better to copy Update variables as they come in rather than forcing the order as in the store |
147 | ? | search_and_delete_value(Var,OldVal,NewVal,Updates,NUpdates), |
148 | ? | (NUpdates == [] -> OutT=InT |
149 | ? | ; store_intermediate_updates2(InT,NUpdates,OutT,PP)). |
150 | | |
151 | | :- use_module(library(ordsets),[ord_intersection/3]). |
152 | | :- block store_intermediate_updates3(-,?). |
153 | | store_intermediate_updates3(Updates,PP) :- |
154 | | ( Updates = [] -> true |
155 | | %; Updates = [bind(abort__flag__info,_)] -> true |
156 | | ; PP = ctxt(SpanInfo,InStore,FullUpdate), |
157 | | % TO DO: determine if illegal assignments, which do not occur in InStore |
158 | | get_ids_from_store(InStore,_,LegalIds), |
159 | | get_ids_from_store(FullUpdate,WrIDs,_WrittenIds), |
160 | | get_ids_from_store(Updates,_,IllegalIds), |
161 | | ord_intersection(IllegalIds,LegalIds,DoubleIds), |
162 | | (DoubleIds \= [] % at least some of the assignments are legal, hence must be double |
163 | | -> add_error(store_intermediate_updates,'Double assignments:', |
164 | | DoubleIds:(illegal_updates(Updates),written_ids(WrIDs)),SpanInfo) |
165 | | ; add_error(store_intermediate_updates,'Illegal assignments:', |
166 | | IllegalIds:(illegal_updates(Updates),legal_ids(LegalIds),written_ids(WrIDs)),SpanInfo) |
167 | | ) |
168 | | ). |
169 | | |
170 | | get_ids_from_store(Store,Ids,SIds) :- findall(Id,member(bind(Id,_),Store),Ids), sort(Ids,SIds). |
171 | | |
172 | | :- assert_pre(store:store_updates_and_normalise(A,B,_C),(type_check(A,store),type_check(B,store))). |
173 | | :- assert_post(store:store_updates_and_normalise(_A,_B,C),(type_check(C,store))). |
174 | | |
175 | | % TO DO: optimize; probably better to traverse InState once, rather than for each update binding |
176 | | %:- block store_updates_and_normalise(-,?,?). % block normally not necessary |
177 | | |
178 | | store_updates_and_normalise(Updates,InState,OutState) :- |
179 | | preferences:get_computed_preference(convert_closures_into_explicit_form_for_store,EXPAND), |
180 | | sort(Updates,SUpdates), % only necessary for checking for multiple variables; we could remove this call |
181 | | store_updates_and_normalise1(SUpdates,EXPAND,'$$NONE$$',InState,OutState). |
182 | | |
183 | | store_updates_and_normalise1([],_EXPAND,_Last,InState,InState). |
184 | | store_updates_and_normalise1([bind(Var,NewVal)|RestUpdates],EXPAND,LastVar,InState,OutState) :- |
185 | | store_updates_and_normalise2(Var,EXPAND,LastVar,NewVal,RestUpdates,InState,OutState). |
186 | | %:- block store_updates_and_normalise2(-,?,?,?,?). |
187 | | store_updates_and_normalise2(Var,EXPAND,LastVar,NewVal,RestUpdates,InState,OutState) :- |
188 | | var(Var),!, |
189 | | add_internal_error('Prolog variable for Var: ',store_updates_and_normalise2(Var,EXPAND,LastVar,NewVal,RestUpdates,InState,OutState)), |
190 | | when(nonvar(Var), |
191 | | store_updates_and_normalise2(Var,EXPAND,LastVar,NewVal,RestUpdates,InState,OutState)). |
192 | | store_updates_and_normalise2(Var,EXPAND,LastVar,NewVal,RestUpdates,InState,OutState) :- |
193 | | normalise_value_for_var(Var,EXPAND,NewVal,NormalisedNewVal), |
194 | | %NormalisedNewVal=NewVal, % comment in to avoid normalising values |
195 | | store_value_for_existing_id(InState,Var,NormalisedNewVal,InState2), |
196 | | % following is in principle no longer necessary: |
197 | | (Var==LastVar -> |
198 | | add_error(store_updates_and_normalise,'Variable has been assigned twice in parallel: ',Var:NewVal) |
199 | | ; true % no longer necessary; bmachine checks this: (b_is_constant(Var) -> add_error(store_updates_and_normalise,'Assigned value to constant: ',Var) ; true) |
200 | | ), |
201 | | store_updates_and_normalise1(RestUpdates,EXPAND,Var,InState2,OutState). |
202 | | |
203 | | |
204 | | % store already normalised updates, e.g., for operation_reuse |
205 | | % does not check for duplicate assignments in parallel |
206 | | store_updates([],S,S). |
207 | | store_updates([bind(Var,NewVal)|RestUpdates],InState,OutState) :- |
208 | | store_value_for_existing_id(InState,Var,NewVal,InState2), |
209 | | store_updates(RestUpdates,InState2,OutState). |
210 | | |
211 | | |
212 | | |
213 | | /* use to merge updates, e.g. for sequential composition LHS ; RHS */ |
214 | | :- assert_pre(store:merge_updates(_A,_B,_C),true). % (type_check(_A,store),type_check(_B,store))). |
215 | | :- assert_post(store:merge_updates(_A,_B,_C),true). %(type_check(_C,store))). |
216 | | |
217 | | :- assert_must_succeed((store:merge_updates([bind(x,1)],[bind(x,2)],R),R==[bind(x,2)])). |
218 | | :- assert_must_succeed((store:merge_updates([bind(x,1)],[bind(X,2),bind(y,3)],R),X=x,R==[bind(x,2),bind(y,3)])). |
219 | | :- assert_must_succeed((store:merge_updates([bind(x,1)],[bind(X,2),bind(y,3)],R),X=z,R==[bind(z,2),bind(y,3),bind(x,1)])). |
220 | | :- assert_must_succeed((store:merge_updates([bind(y,1),bind(x,1)],[bind(x,2)],R),R==[bind(x,2),bind(y,1)])). |
221 | | |
222 | | :- block merge_updates(-,?,?). |
223 | | merge_updates([],RHSUpdates,RHSUpdates). |
224 | | merge_updates([Bind|LHT],RHSUpdates,Rest) :- |
225 | ? | merge_updates2( Bind,LHT,RHSUpdates,Rest). |
226 | | :- block merge_updates2(?,?,-,?). |
227 | | merge_updates2(bind(Var,NewVal),LHT,RHSUpdates,Rest) :- |
228 | ? | merge_remove(RHSUpdates,Var,NewVal,RHSUpdates2), |
229 | ? | merge_updates(LHT,RHSUpdates2,Rest). |
230 | | |
231 | | :- block merge_remove(-,?,?,?). |
232 | | merge_remove([],Var,NewVal,[bind(Var,NewVal)]). |
233 | | merge_remove([bind(Var2,Val2)|T2],Var1,Val1,[bind(Var2,Val2)|NewT2]) :- |
234 | ? | merge_remove_aux(Var2,T2,Var1,Val1,NewT2). |
235 | | |
236 | | :- block merge_remove_aux(-,?,?,?,?). |
237 | | merge_remove_aux(Var2,T2,Var1,Val1,NewT2) :- |
238 | ? | (Var1=Var2 |
239 | | -> NewT2=T2 /* binding in second updates overrides first update */ |
240 | ? | ; merge_remove(T2,Var1,Val1,NewT2) |
241 | | ). |
242 | | /* ----------------------- */ |
243 | | |
244 | | :- block save_updates_in_existing_store(-,?). |
245 | | save_updates_in_existing_store([],_Store). |
246 | | save_updates_in_existing_store([bind(Var,Value)|Urest],Store) :- |
247 | | save_updates_in_existing_store2(Var,Value,Store), |
248 | | save_updates_in_existing_store(Urest,Store). |
249 | | :- block save_updates_in_existing_store2(-,?,?). |
250 | | save_updates_in_existing_store2(Var,Value,Store) :- |
251 | | lookup_value_for_existing_id(Var,Store,Value). |
252 | | |
253 | | |
254 | | :- assert_must_succeed(store:l_normalise_values([int(1)],[int(1)])). |
255 | | |
256 | | l_normalise_values([],[]). |
257 | | l_normalise_values([H|T],[NH|NT]) :- normalise_value(H,NH), l_normalise_values(T,NT). |
258 | | |
259 | | :- block l_expand_and_normalise_values(-,?). |
260 | | l_expand_and_normalise_values([],[]). |
261 | | l_expand_and_normalise_values([H|T],[NH|NT]) :- |
262 | | normalise_value_for_var(unkown,true,H,NH), |
263 | | l_expand_and_normalise_values(T,NT). |
264 | | :- block l_expand_and_normalise_values(-,?,?). |
265 | | l_expand_and_normalise_values([],[],_). |
266 | | l_expand_and_normalise_values([H|T],[NH|NT],[VarName|VT]) :- |
267 | | %% print(normalising(VarName)),nl, %% |
268 | | normalise_value_for_var(VarName,true,H,NH), |
269 | | l_expand_and_normalise_values(T,NT,VT). |
270 | | |
271 | | |
272 | | |
273 | | :- assert_must_succeed(store:normalise_value(int(1),int(1))). |
274 | | :- assert_must_succeed((store:normalise_value([int(1)],R), R==avl_set(node(int(1),true,0,empty,empty)))). |
275 | | :- assert_must_succeed((store:normalise_value([int(1),int(2)],R1), |
276 | | store:normalise_value([int(2),int(1)],R2),R1==R2)). |
277 | | %:- assert_must_succeed((store:normalise_value(X,[int(1),int(2)]),X=[int(2),int(1)])). |
278 | | :- assert_must_succeed((store:normalise_value(X,_R),X=[Y,Z], |
279 | | Y=[int(2),int(1)],Z=[int(1)])). |
280 | | :- assert_must_succeed(store:normalise_value(_X,[int(1),int(3)])). |
281 | | :- assert_must_succeed((store:normalise_value(X,[int(3),int(1)]), |
282 | | kernel_objects:equal_object(X,[int(1),int(3)]))). |
283 | | :- assert_must_fail(store:normalise_value(int(2),int(1))). |
284 | | |
285 | | |
286 | | normalise_value_for_var(Var,Val,NormVal) :- |
287 | | preferences:get_computed_preference(convert_closures_into_explicit_form_for_store,EXPAND), |
288 | | normalise_value_for_var(Var,EXPAND,Val,NormVal). |
289 | | |
290 | | :- block normalise_value_for_var(?,?,-,-). |
291 | | normalise_value_for_var(Var,EXPAND,Val,NormVal) :- % print(norm(Var,EXPAND,Val,NormVal)),nl, trace, |
292 | | ~~mnf(expand_closure_value(Val,EXPAND,Var,ENewVal)), % also normalises values inside closure if not expanded |
293 | | normalise_value(ENewVal,NormVal). % , tools_printing:print_term_summary(normalised(ENewVal,NormVal)). |
294 | | |
295 | | :- block normalise_value(-,-). |
296 | | normalise_value(V,Res) :- |
297 | | (nonvar(V),var(Res) -> ~~mnf(normalise2(V,ResR)),Res=ResR ; normalise3(V,Res)). |
298 | | % (nonvar(V),var(Res) -> normalise2(V,Res) ; normalise3(V,Res)). |
299 | | |
300 | | |
301 | | |
302 | | :- use_module(b_global_sets,[b_integer_or_string_set/1,all_elements_of_type/2]). |
303 | | :- use_module(library(avl)). |
304 | | |
305 | | %:- use_module(debug,[time/1]). |
306 | | |
307 | | % a normalise which does not need to call equal_object on the result argument: |
308 | | normalise2([H|T],Res) :- !, |
309 | | normalise_list([H|T],Res). |
310 | | normalise2((A,B),(NA,NB)) :- !, normalise_value(A,NA), normalise_value(B,NB). |
311 | | normalise2(global_set(GS),N) :- !, |
312 | ? | (b_integer_or_string_set(GS) |
313 | | -> N = global_set(GS) /* can be very large or infinite, so don't expand */ |
314 | | ; all_elements_of_type(GS,Res), |
315 | | normalise2(Res,N)). |
316 | | normalise2(avl_set(A),R) :- !, |
317 | | (%empty_avl(A) |
318 | | A=empty |
319 | | -> R=[] ; |
320 | | %A = node(_,_,_,empty,_) -> R = avl_set(A) ; % avoid normalising certain one and two element sets; does not seem to bring any improvement |
321 | | avl_to_list(A,L), ord_list_to_avl(L,B), R=avl_set(B)). |
322 | | normalise2(string(S),R) :- !, R=string(S). |
323 | | normalise2(int(S),R) :- !, R=int(S). |
324 | | normalise2(fd(N,T),R) :- !, R=fd(N,T). |
325 | | normalise2(rec(Fields),R) :- !, R=rec(NFields), normalise_fields(Fields,NFields). |
326 | | normalise2(V,V). |
327 | | |
328 | | :- block normalise_fields(-,-). |
329 | | normalise_fields([],[]). |
330 | | normalise_fields([field(Name,Val)|T], [field(Name,NVal)|NT]) :- normalise_value(Val,NVal), |
331 | | normalise_fields(T,NT). |
332 | | |
333 | | /* version to be called if for some reason second argument already instantiated; |
334 | | e.g. when operation arguments and results are already instantiated */ |
335 | | %%normalise3(X,R) :- var(R),var(X),!,R=X. /* just in case the when is unfrozen by hypercall */ |
336 | | :- use_module(kernel_objects,[equal_object/3]). |
337 | | %normalise3(R,[H|T]) :- !,kernel_objects:equal_object(R,[H|T]). |
338 | | /* don't insist on normalising if a set is already partially given*/ |
339 | | normalise3((A,B),(NA,NB)) :- !, normalise_value(A,NA), normalise_value(B,NB). |
340 | | normalise3(V,Res) :- equal_object(V,Res,normalise3). |
341 | | |
342 | | |
343 | | :- use_module(custom_explicit_sets,[construct_avl_from_lists/2]). |
344 | | :- use_module(kernel_tools,[ground_value_check/2]). |
345 | | normalise_list(List,Res) :- |
346 | | ground_value_check(List,ListGround), % this is slightly slower than ground() for long lists not containing avl_set values |
347 | | normalise_list_aux(ListGround,List,Res). |
348 | | :- block normalise_list_aux(-,?,?). |
349 | | normalise_list_aux(_,List,Res) :- |
350 | | construct_avl_from_lists(List,Avl), %print(done),nl, |
351 | | kernel_objects:equal_object(Res,Avl,normalise_list). |
352 | | |
353 | | |
354 | | expand_closure_value(Var,_,_,R) :- var(Var),!,R=Var. |
355 | | expand_closure_value(closure(P,T,B),EXPAND,VarName,ExpandedValue) :- !, %print(expand_closure_value(P,T,B)),nl, |
356 | | expand_closure_value2(P,T,B,EXPAND,VarName,ExpandedValue). |
357 | | %expand_closure_value(closure_x(P,T,B,Exp),EXPAND,VarName,ExpandedValue) :- !, |
358 | | % (ground(Exp) -> ExpandedValue=Exp ; expand_closure_value(closure(P,T,B),EXPAND,VarName,ExpandedValue)). |
359 | | expand_closure_value(Val,_Expand,_VarName,Val). |
360 | | |
361 | | :- use_module(custom_explicit_sets,[dont_expand_this_explicit_set/1,dont_expand_this_explicit_set/2, is_infinite_or_very_large_explicit_set/1]). |
362 | | :- use_module(clpfd_interface,[catch_clpfd_overflow_call2/2]). |
363 | | :- use_module(tools_timeout, [time_out_with_factor_call/3]). |
364 | | |
365 | | :- block expand_closure_value2(-,?,?,?,?,?), expand_closure_value2(?,-,?,?,?,?), expand_closure_value2(?,?,-,?,?,?). |
366 | | expand_closure_value2(P,T,B,EXPAND,VarName,ExpandedValue) :- !, |
367 | | % print(expand_closure_value(P,T,B)),nl, |
368 | ? | (dont_expand(EXPAND,closure(P,T,B)) |
369 | | -> construct_normalised_closure(P,T,B,ExpandedValue) %, print(not_expanding(closure(P,T,B))),nl |
370 | | ; %print(expanding(closure(P,T,B))),nl, |
371 | | catch_clpfd_overflow_call2( |
372 | | time_out_with_factor_call( |
373 | | call_with_enumeration_warning( /* ensure we generate enumeration_warning exceptions */ |
374 | | custom_explicit_sets:expand_closure_to_avl_or_list(P,T,B,ExpandedValue,no_check,no_wf_available) |
375 | | ), |
376 | | 0.3,store:time_out_expand_backup(VarName,P,T,B,ExpandedValue)) |
377 | | % , print(expanded_closure(ExpandedValue)),nl |
378 | | , (format('% CLP(FD) overflow during closure expansion: ~w~n',[VarName]), |
379 | | construct_normalised_closure(P,T,B,ExpandedValue))) |
380 | | ). |
381 | | |
382 | | dont_expand(false,_). |
383 | ? | dont_expand(true,C) :- dont_expand_this_explicit_set(C). |
384 | | dont_expand(limit(Limit),C) :- dont_expand_this_explicit_set(C,Limit). |
385 | | dont_expand(force,C) :- is_infinite_or_very_large_explicit_set(C). |
386 | | |
387 | | /* |
388 | | :- use_module(custom_explicit_sets,[dont_expand_this_explicit_set/1, is_interval_closure/5]). |
389 | | % maybe systematically expand small intervals and global_set's for normalization purposes ?? |
390 | | % (alternatively, we could re-convert certain avl-sets to symbolic form here) |
391 | | dont_expand_closure_value(_,_,_) :- |
392 | | preferences:get_computed_preference(convert_closures_into_explicit_form_for_store,false),!. |
393 | | %dont_expand_closure_value(P,T,B) :- |
394 | | % is_interval_closure(P,T,B,Low,Up), number(Low), number(Up),!, |
395 | | % % interval closures are quite efficient for certain manipulations |
396 | | % Size is Up+1-Low, Size>100. % another magic constant ; which value to choose ?? |
397 | | %dont_expand_closure_value(_,_,_) :- |
398 | | % preferences:get_preference(convert_comprehension_sets_into_closures,false),!. |
399 | | % % in the case above: we have already decided not to expand the closure earlier, dont repeat check !? TO DO: check that this is indeed ok; that no closures are constructed otherwise; maybe we should just check for small interval closures ? |
400 | | dont_expand_closure_value(P,T,B) :- dont_expand_this_explicit_set(closure(P,T,B)). |
401 | | */ |
402 | | |
403 | | time_out_expand_backup(VarName,P,T,B,ExpandedValue) :- |
404 | | add_message(expand_closure_value,'Time-out while trying to expand value of: ',VarName,B), |
405 | | construct_normalised_closure(P,T,B,ExpandedValue). |
406 | | |
407 | | construct_normalised_closure(P,T,B1,closure(P,T,NB)) :- |
408 | | %print(normalising(P)),nl, |
409 | | %b_compile(B1,P,[],[],B2,no_wf_available), % probably much more expensive than simple code with can_be_computed below |
410 | | normalise_closure_body(B1,NB). |
411 | | % print(norm),nl,print(B),nl,print(NB),nl,nl. |
412 | | |
413 | | % normalise values that are compiled inside closures |
414 | | normalise_closure_body(b(OP,T,I),b(NOP,T,FI)) :- |
415 | | (var(I) -> print(b(OP,T,I)),nl , when(nonvar(OP),(print(b(OP,T,I)),nl)) ; true), |
416 | | filter_info(I,FI), |
417 | | ncb(OP,OP2), |
418 | | (can_be_computed(OP2) % when compiling not all information was available for computation, now it is |
419 | | -> b_interpreter:b_compute_expression_nowf(b(OP,T,I),[],[],Val), |
420 | | %print(comp(Val)),nl, |
421 | | ncb(value(Val),NOP) % TO DO: better apply the can_be_computed check after ncb, if performance ok |
422 | | ; NOP=OP2). |
423 | | |
424 | | filter_info(V,R) :- var(V),!,R=V. |
425 | | filter_info([],[]). |
426 | | filter_info([H|T],Res) :- |
427 | | (important_info(H) -> Res=[H|TR] ; Res=TR), filter_info(T,TR). |
428 | | |
429 | | important_info(contains_wd_condition). |
430 | | important_info(prob_annotation(_)). |
431 | | important_info(used_ids(_)). |
432 | | important_info(was(_)). |
433 | | important_info(nodeid(_)). |
434 | | important_info(allow_to_lift_exists). |
435 | | |
436 | | :- use_module(kernel_mappings). |
437 | | % ncb stands for normalise closure body |
438 | | ncb(V,R) :- var(V),!, R=V. |
439 | | ncb(bool_set,R) :- !, R=bool_set. |
440 | | ncb(truth,R) :- !, R=truth. |
441 | | ncb(event_b_identity,R) :- !, R=event_b_identity. |
442 | | ncb(falsity,R) :- !, R=falsity. |
443 | | ncb(max_int,R) :- !, R=max_int. |
444 | | ncb(min_int,R) :- !, R=min_int. |
445 | | ncb(value(V),value(NV)) :- !,normalise_value_for_var(closure_body,V,NV). |
446 | | ncb(integer(X),integer(NX)) :- !, X=NX. |
447 | | ncb(identifier(X),identifier(NX)) :- !, X=NX. |
448 | | ncb(string(X),string(NX)) :- !, X=NX. |
449 | | ncb(string_set,R) :- !, R=string_set. |
450 | | ncb(integer_set(X),integer_set(NX)) :- !, X=NX. |
451 | | ncb(set_extension(X),set_extension(NX)) :- !, X=NX. |
452 | | ncb(partition(S,L),partition(NS,NL)) :- !, normalise_closure_body(S,NS), |
453 | | maplist(normalise_closure_body,L,NL). |
454 | | ncb(general_sum(Ids,Condition,Expression),general_sum(Ids,NC,NE)) :- !, |
455 | | normalise_closure_body(Condition,NC),normalise_closure_body(Expression,NE). |
456 | | ncb(general_product(Ids,Condition,Expression),general_product(Ids,NC,NE)) :- !, |
457 | | normalise_closure_body(Condition,NC),normalise_closure_body(Expression,NE). |
458 | | ncb(sequence_extension(X),sequence_extension(NX)) :- !, X=NX. |
459 | | ncb(external_function_call(F,L),external_function_call(F,LL)) :- !, L=LL. |
460 | | ncb(external_pred_call(F,L),external_pred_call(F,LL)) :- !, L=LL. |
461 | | ncb(equal(A,B),equal(NA,NB)) :- !, normalise_closure_body(A,NA), normalise_closure_body(B,NB). |
462 | | ncb(couple(A,B),couple(NA,NB)) :- !, normalise_closure_body(A,NA), normalise_closure_body(B,NB). |
463 | | ncb(interval(A,B),interval(NA,NB)) :- !, normalise_closure_body(A,NA), normalise_closure_body(B,NB). |
464 | | ncb(function(A,B),function(NA,NB)) :- !, normalise_closure_body(A,NA), normalise_closure_body(B,NB). |
465 | | ncb(operation_call_in_expr(A,B),operation_call_in_expr(NA,B)) :- !, |
466 | | normalise_closure_body(A,NA). |
467 | | ncb(relations(A,B),relations(NA,NB)) :- !, normalise_closure_body(A,NA), normalise_closure_body(B,NB). |
468 | | ncb(member(A,B),member(NA,NB)) :- !, normalise_closure_body(A,NA), normalise_closure_body(B,NB). |
469 | | ncb(not_member(A,B),not_member(NA,NB)) :- !, normalise_closure_body(A,NA), normalise_closure_body(B,NB). |
470 | | ncb(negation(B),negation(NB)) :- !, normalise_closure_body(B,NB). |
471 | | ncb(conjunct(A,B),conjunct(NA,NB)) :- !, normalise_closure_body(A,NA), normalise_closure_body(B,NB). |
472 | | ncb(disjunct(A,B),disjunct(NA,NB)) :- !, normalise_closure_body(A,NA), normalise_closure_body(B,NB). |
473 | | ncb(equivalence(A,B),equivalence(NA,NB)) :- !, normalise_closure_body(A,NA), normalise_closure_body(B,NB). |
474 | | ncb(if_then_else(A,B,C),if_then_else(NA,NB,NC)) :- !, |
475 | | normalise_closure_body(A,NA), normalise_closure_body(B,NB), normalise_closure_body(C,NC). |
476 | | ncb(implication(A,B),implication(NA,NB)) :- !, normalise_closure_body(A,NA), normalise_closure_body(B,NB). |
477 | | ncb(comprehension_set(V,B),comprehension_set(V,NB)) :- !, normalise_closure_body(B,NB). |
478 | | ncb(convert_bool(B),convert_bool(NB)) :- !, normalise_closure_body(B,NB). |
479 | | ncb(exists(IDs,B),exists(IDs,NB)) :- !, normalise_closure_body(B,NB). |
480 | | ncb(forall(IDs,A,B),forall(IDs,NA,NB)) :- !, normalise_closure_body(A,NA), normalise_closure_body(B,NB). |
481 | | ncb(assertion_expression(Cond,ErrMsg,Expr),assertion_expression(NA,ErrMsg,NB)) :- !, |
482 | | normalise_closure_body(Cond,NA), normalise_closure_body(Expr,NB). |
483 | | ncb(freetype_case(FT,IsCase,Expr),freetype_case(FT,IsCase,NB)) :- !, |
484 | | normalise_closure_body(Expr,NB). |
485 | | ncb(freetype_constructor(Id,Case,Expr),freetype_constructor(Id,Case,NB)) :- !, |
486 | | normalise_closure_body(Expr,NB). |
487 | | ncb(freetype_destructor(Id,Case,Expr),freetype_destructor(Id,Case,NB)) :- !, |
488 | | normalise_closure_body(Expr,NB). |
489 | | ncb(record_field(R,Name),record_field(NR,Name)) :- !, |
490 | | normalise_closure_body(R,NR). |
491 | | ncb(rec(Fields),rec(NFields)) :- !, |
492 | | ncb_fields(Fields,NFields). |
493 | | ncb(kodkod(Id,Ids),R) :- !, R=kodkod(Id,Ids). |
494 | | ncb(lazy_let_expr(Id,E,Expr),lazy_let_expr(Id,NE,NExpr)) :- !, normalise_closure_body(E,NE), |
495 | | normalise_closure_body(Expr,NExpr). |
496 | | ncb(lazy_let_pred(Id,E,Pred),lazy_let_pred(Id,NE,NPred)) :- !, normalise_closure_body(E,NE), |
497 | | normalise_closure_body(Pred,NPred). |
498 | | % lazy_let_subst should not occur in closure bodies |
499 | | ncb(lazy_lookup_expr(X),lazy_lookup_expr(NX)) :- !, X=NX. |
500 | | ncb(lazy_lookup_pred(X),lazy_lookup_pred(NX)) :- !, X=NX. |
501 | | ncb(let_predicate(Ids,AssignmentExprs,Pred),let_predicate(Ids,AssignmentExprs,NPred)) :- !, |
502 | | normalise_closure_body(Pred,NPred). |
503 | | ncb(let_expression(Ids,AssignmentExprs,Expr),let_expression(Ids,AssignmentExprs,NExpr)) :- !, |
504 | | normalise_closure_body(Expr,NExpr). |
505 | | ncb(let_expression_global(Ids,AssignmentExprs,Expr),let_expression_global(Ids,AssignmentExprs,NExpr)) :- !, |
506 | | normalise_closure_body(Expr,NExpr). |
507 | | ncb(F,NF) :- functor(F,Op,1), |
508 | ? | (unary_function(Op,_,_) ; unary_in_boolean_type(Op,_)), !, |
509 | | arg(1,F,Arg1), functor(NF,Op,1), arg(1,NF,NormArg1), |
510 | | normalise_closure_body(Arg1,NormArg1). |
511 | | ncb(F,NF) :- functor(F,Op,2), |
512 | ? | (binary_function(Op,_,_) ; kernel_mappings:binary_boolean_operator(Op,_,_) ; binary_in_boolean_type(Op,_)), !, |
513 | | arg(1,F,Arg1),arg(2,F,Arg2), functor(NF,Op,2), arg(1,NF,NormArg1), arg(2,NF,NormArg2), |
514 | | normalise_closure_body(Arg1,NormArg1), |
515 | | normalise_closure_body(Arg2,NormArg2). |
516 | | ncb(X,X) :- print(ncb(X)),nl. |
517 | | |
518 | | |
519 | | can_be_computed(domain(X)) :- is_known_set_or_int_value(X). |
520 | | can_be_computed(range(X)) :- is_known_set_or_int_value(X). |
521 | | can_be_computed(plus(X,Y)) :- is_known_set_or_int_value(X),is_known_set_or_int_value(Y). |
522 | | can_be_computed(minus(X,Y)) :- is_known_set_or_int_value(X),is_known_set_or_int_value(Y). |
523 | | can_be_computed(times(X,Y)) :- is_known_set_or_int_value(X),is_known_set_or_int_value(Y). |
524 | | % check for more possible partial evaluations; check for common code with b_compiler, CSE or other parts of ProB |
525 | | |
526 | | is_known_set_or_int_value(b(value(V),_,_)) :- is_known_aux(V). |
527 | | is_known_aux(X) :- var(X),!,fail. |
528 | | is_known_aux([]). |
529 | | is_known_aux(avl_set(_)). |
530 | | is_known_aux(int(Nr)) :- number(Nr). |
531 | | |
532 | | ncb_fields([],[]). |
533 | | ncb_fields([field(Name,Expr)|T], [field(Name,NExpr)|NT]) :- |
534 | | normalise_closure_body(Expr,NExpr), |
535 | | ncb_fields(T,NT). |
536 | | |
537 | | %ncb(set_extension([b(couple(b(add(b(identifier(idx),integer,[nodeid(pos(53,1,11,91,11,93))]),b(integer(1),integer,[nodeid(pos(54,1,11,95,11,95))])),integer,[nodeid(pos(52,1,11,91,11,95))]),b(identifier(bit),integer,[nodeid(pos(55,1,11,101,11,103))])),couple(integer,integer),[nodeid(pos(51,1,11,91,11,103))])])) |
538 | | |
539 | | normalise_store(T,NT) :- |
540 | | preferences:get_computed_preference(convert_closures_into_explicit_form_for_store,EXPAND), |
541 | | normalise_store1(T,EXPAND,NT). |
542 | | :- block normalise_store1(-,?,?). |
543 | | normalise_store1([],_Expand,[]). |
544 | | normalise_store1([bind(Var,Val)|T],EXPAND,[bind(Var,NVal)|NT]) :- |
545 | | %print(normalise(Val)),nl,print(Var),nl, |
546 | | normalise_value_for_var(Var,EXPAND,Val,NVal), |
547 | | normalise_store1(T,EXPAND,NT). |
548 | | |
549 | | /* ----------------------- */ |
550 | | |
551 | | :- assert_pre(store:lookup_value_for_existing_id(Id,State,_Val), |
552 | | (type_check(Id,variable_id),list_skeleton(State),type_check(State,store))). |
553 | | :- assert_post(store:lookup_value_for_existing_id(_Id,_State,_Val), true). |
554 | | |
555 | | lookup_value_for_existing_id(Id,State,Res) :- |
556 | | (member_bind(Id,Val,State) % safe_member(bind(Id,Val),State,lookup_value_for_existing_id) |
557 | | -> check_val(Val,Id,State),Res=Val |
558 | | ; add_internal_error('Call Failed: ',lookup_value_for_existing_id(Id,State,Res)), |
559 | | Res=fail |
560 | | ). |
561 | | |
562 | | :- assert_pre(store:lookup_value_for_existing_id(Id,LS,State,_Val), |
563 | | (type_check(Id,variable_id),type_check(LS,store),type_check(State,store),list_skeleton(LS),list_skeleton(State))). |
564 | | :- assert_post(store:lookup_value_for_existing_id(_Id,_LS,_State,_Val), true). |
565 | | |
566 | | lookup_value_for_existing_id(Id,LocalState,State,Val) :- |
567 | | (member_bind(Id,Val,LocalState) %safe_member(bind(Id,Val),LocalState,lookup_value_for_existing_id__4) |
568 | | -> check_val(Val,Id,LocalState) |
569 | | ; lookup_value_for_existing_id(Id,State,Val)). |
570 | | |
571 | | lookup_value(Id,State,Val) :- |
572 | | (member_bind(Id,Val,State) %safe_member(bind(Id,Val),State,lookup_value) |
573 | | -> check_val(Val,Id,State) |
574 | | ). |
575 | | lookup_value(Id,LocalState,State,Val) :- |
576 | | (member_bind(Id,Val,LocalState) %safe_member(bind(Id,Val),LocalState,lookup_value__4) |
577 | | -> check_val(Val,Id,LocalState) |
578 | | ; member_bind(Id,Val,State) -> check_val(Val,Id,State)). |
579 | | lookup_value_with_span(Id,LocalState,State,Val,Span) :- |
580 | | (member_bind(Id,Val,LocalState) %safe_member(bind(Id,Val),LocalState,lookup_value__4) |
581 | | -> check_val_with_span(Val,Id,LocalState,Span) |
582 | | ; member_bind(Id,Val,State) -> check_val_with_span(Val,Id,State,Span)). |
583 | | lookup_value_without_check(Id,LocalState,State,Val) :- % does not check if value is undefined |
584 | | (member_bind(Id,Val,LocalState) %safe_member(bind(Id,Val),LocalState,lookup_value__4) |
585 | | -> true |
586 | | ; member_bind(Id,Val,State) -> true). |
587 | | |
588 | | % a faster version of member(bind(Id,Val),List) with only one solution |
589 | | member_bind(Id,Val,[H|T]) :- |
590 | | arg(1,H,Id) -> arg(2,H,Val) ; member_bind(Id,Val,T). |
591 | | |
592 | | get_id_value(Id,State,Val) :- safe_member(bind(Id,Val),State,get_id_value). /* can be backtracked over */ |
593 | | |
594 | | %safe_member(X,T) :- safe_member(X,T,safe_member). |
595 | | safe_member(_,[],_) :- !,fail. |
596 | | safe_member(X,[H|T],Loc) :- !, (X=H ; safe_member(X,T,Loc)). |
597 | | safe_member(X,T,Loc) :- add_internal_error('Argument not a list: ',safe_member(X,T,Loc)),fail. |
598 | | |
599 | | check_val_with_span(X,V,_State,Span) :- |
600 | | (X==term(undefined) -> |
601 | | add_error(reading_undefined_variable,'Trying to read undefined variable: ',V,Span) % do not fail; otherwise we will look elsewhere and generate another error message, see test 1660 |
602 | | ; true). |
603 | | |
604 | | check_val(X,V,_State) :- |
605 | | (X==term(undefined) -> |
606 | | add_error(reading_undefined_variable,'Trying to read undefined variable: ',V) % do not fail |
607 | | ; true). |
608 | | |
609 | | :- assert_must_succeed(( store:lookup_and_delete_value(x,X,[bind(y,2),bind(x,3)],R,true,_WF,F), |
610 | | X==3, R==[bind(y,2)],F==true )). |
611 | | :- assert_must_succeed(( store:lookup_and_delete_value(x,X,[bind(y,2)|T],R,true,_WF,F), |
612 | | T = [bind(x,3)], |
613 | | X==3, R==[bind(y,2)],F==true )). |
614 | | |
615 | | lookup_and_delete_value(Var,Value,T,UT,ReportError,WF,Finished) :- |
616 | | lookup_and_delete_value1(T,Var,Value,UT,ReportError,WF,Finished). |
617 | | :- use_module(kernel_waitflags,[add_abort_error_span/5]). |
618 | | :- block lookup_and_delete_value1(-,?,?,?,?,?,?). |
619 | | lookup_and_delete_value1([],Var,Value,[],ReportError,WF,Finished) :- |
620 | | (ReportError=report_error(WF) |
621 | | -> add_abort_error_span(missing_assignment_error,'Statement did not assign to variable: ',Var,unknown,WF) |
622 | | /* lookup_and_delete is called only from get_results */ |
623 | | ; true |
624 | | ), no_value_for_variable(Value,Var), |
625 | | Finished=true. |
626 | | lookup_and_delete_value1([bind(Var2,Value2)|T],Var,Value,Res,ReportError,WF,Finished) :- |
627 | | lookup_and_delete_value2(Var2,Value2,T,Var,Value,Res,ReportError,WF,Finished). |
628 | | :- block lookup_and_delete_value2(-,?,?,?,?,?,?,?,?). |
629 | | lookup_and_delete_value2(Var2,Value2,T,Var,Value,Res,ReportError,WF,Finished) :- |
630 | | (Var=Var2 |
631 | | -> Value=Value2, T=Res, Finished=true |
632 | | ; Res=[bind(Var2,Value2)|UT], |
633 | | lookup_and_delete_value1(T,Var,Value,UT,ReportError,WF,Finished) |
634 | | ). |
635 | | |
636 | | no_value_for_variable(term(no_value_for(Var)),Var). |
637 | | |
638 | | :- assert_must_succeed(( store:search_and_delete_value(x,22,X,[bind(y,2),bind(x,3)],R), |
639 | | X==3, R==[bind(y,2)] )). |
640 | | :- assert_must_succeed(( store:search_and_delete_value(x,22,X,[bind(y,2)],R), |
641 | | X==22, R==[bind(y,2)] )). |
642 | | :- assert_must_succeed(( store:search_and_delete_value(x,22,X,[bind(y,2)|T],R), |
643 | | T = [bind(x,3)], |
644 | | X==3, R==[bind(y,2)] )). |
645 | | |
646 | | :- block search_and_delete_value(-,?,?,?,?). |
647 | | search_and_delete_value(Var,OldVal,Value,InStore,OutStore) :- |
648 | | search_and_delete_value2(InStore,Var,OldVal,Value,OutStore). |
649 | | |
650 | | :- block search_and_delete_value2(-,?,?,?,?). |
651 | | search_and_delete_value2([],_Var,OldVal,Value,[]) :- |
652 | ? | Value = OldVal. |
653 | | search_and_delete_value2([bind(Var2,Value2)|T],Var,OldVal,Value,Res) :- |
654 | | search_and_delete_value3(Var2,Value2,T,Var,OldVal,Value,Res). |
655 | | |
656 | | :- block search_and_delete_value3(-,?,?,?,?,?,?). |
657 | | search_and_delete_value3(Var2,Value2,T,Var,OldVal,Value,Res) :- |
658 | | (Var=Var2 |
659 | | -> Value=Value2, T=Res |
660 | | ; Res=[bind(Var2,Value2)|UT], |
661 | | search_and_delete_value2(T,Var,OldVal,Value,UT) |
662 | | ). |
663 | | |
664 | | empty_state([]). |
665 | | add_var_to_localstate(Var,Val,InState,[bind(Var,Val)|InState]). |
666 | | |
667 | | :- assert_pre(store:set_up_localstate(Vars,Vals,In,_), |
668 | | (type_check(Vars,list(variable_id)),type_check(Vals,vlist(any)),type_check(In,store))). |
669 | | :- assert_post(store:set_up_localstate(_,_,_,Out), type_check(Out,store)). |
670 | | |
671 | | set_up_localstate([],[],S,S). |
672 | | set_up_localstate([Var|T],[Val|FT],InS,[bind(VarID,Val)|OutS]) :- |
673 | | /* add Var,Val to Local state at the beginning to properly handle nested |
674 | | blocks with same variable names */ |
675 | | (Var=b(identifier(Id),_,_) -> %print(typed_identifier_for_set_up_localstate(Var)),nl, |
676 | | VarID = Id |
677 | | ; VarID = Var), |
678 | | set_up_localstate(T,FT,InS,OutS). |
679 | | |
680 | | set_up_undefined_localstate([],S,S). |
681 | | set_up_undefined_localstate([Var|T],InS,[bind(Id,term(undefined))|OutS]) :- |
682 | | def_get_texpr_id(Var,Id), |
683 | | /* add Var,Val to Local state at the beginning to properly handle nested |
684 | | blocks with same variable names */ |
685 | | set_up_undefined_localstate(T,InS,OutS). |
686 | | |
687 | | % sets up undefined values for variables, except for a list of predefined variables (all of which must be used) |
688 | | set_up_undefined_localstate_with_predefined([],PredefinedValues,S,S) :- |
689 | | (PredefinedValues=[] -> true |
690 | | ; add_internal_error('Unknown predefined values: ',set_up_undefined_localstate_with_predefined([],PredefinedValues,S,S))). |
691 | | set_up_undefined_localstate_with_predefined([Var|T],PredefinedValues,InS,[bind(Id,Val)|OutS]) :- |
692 | | def_get_texpr_id(Var,Id), |
693 | | delete(InS,bind(Id,_),InS2), % in case of name clash: remove the old binding from the state |
694 | | (select(bind(Id,Val),PredefinedValues,Rest) |
695 | | -> set_up_undefined_localstate_with_predefined(T,Rest,InS2,OutS) |
696 | | ; Val=term(undefined), |
697 | | set_up_undefined_localstate_with_predefined(T,PredefinedValues,InS2,OutS)). |
698 | | |
699 | | :- assert_pre(store:delete_variables_from_state(Vars,In,_), |
700 | | (type_check(Vars,list(variable_id)),type_check(In,store))). |
701 | | :- assert_post(store:delete_variables_from_state(_,_,Out), type_check(Out,store)). |
702 | | |
703 | | delete_variables_from_state([],S,S). |
704 | | delete_variables_from_state([Var|T],InState,OutState) :- |
705 | | delete_variable(InState, Var, S2), |
706 | | delete_variables_from_state(T,S2,OutState). |
707 | | |
708 | | delete_variable([],_,[]). |
709 | | delete_variable([bind(V,Val)|T],Var,Res) :- |
710 | | (Var==V |
711 | | -> Res = T |
712 | | ; Res = [bind(V,Val)|DT], delete_variable(T,Var,DT) |
713 | | ). |
714 | | /* --------------------------------- */ |
715 | | |
716 | | % unused at the moment: |
717 | | %:- assert_pre(store:copy_store_template(In,_), |
718 | | % (type_check(In,store))). |
719 | | %:- assert_post(store:copy_store_template(_,Out), type_check(Out,store)). |
720 | | %copy_store_template([],[]). |
721 | | %copy_store_template([bind(Var,_)|T],[bind(Var,_)|CT]) :- copy_store_template(T,CT). |
722 | | |
723 | | :- use_module(library(ordsets)). |
724 | | % copy_store_template copies a store and its values except some changing variables |
725 | | % Two new stores are created: constants are not copied into the first new update state, but |
726 | | % to the second new full state |
727 | | copy_variable_store(InState,SortedChanges,Updates,NewFullState) :- |
728 | | (SortedChanges=[] -> Updates = [],NewFullState=InState % Query Operation/Event ,print(no_upd),nl |
729 | | ; copy_variable_store2(InState,SortedChanges,Updates,NewFullState)). |
730 | | |
731 | | copy_variable_store2([],_,[],[]). |
732 | | copy_variable_store2([bind(Var,Old)|T],SortedChanges,Updates,NewFullState) :- |
733 | | ( b_is_constant(Var) -> |
734 | | Updates = CT, NewFullState = [bind(Var,Old)|FT] |
735 | | %; safe_member(Var,SortedChanges,copy_variable_store) -> |
736 | | ; ord_member(Var,SortedChanges) -> |
737 | | %; ord_delete(SortedChanges,Var,SortedChanges2) -> % in principle better than ord_member; but seems slightly slower on examples/EventBPrologPackages/Advance_WP2/v6_Sep2014/ex_mch.eventb |
738 | | Updates = [bind(Var,New)|CT], NewFullState = [bind(Var,New)|FT] |
739 | | ; otherwise -> |
740 | | Updates = CT, NewFullState = [bind(Var,Old)|FT] |
741 | | ), copy_variable_store2(T,SortedChanges,CT,FT). |
742 | | |
743 | | %ord_delete([H|T],El,Res) :- El @>= H, |
744 | | % (H==El -> Res=T ; Res = [H|RR], ord_delete(T,El,RR)). |
745 | | |
746 | | |
747 | | % ------------------------------- |
748 | | |
749 | | :- assert_must_succeed(store:check_valid_store([bind(x,int(1)), bind(y,int(2))],unit_test)). |
750 | | |
751 | | :- block check_valid_store(-,?). |
752 | | check_valid_store([],_PP). |
753 | | check_valid_store([bind(Var,Value)|T],PP) :- member(bind(Var,Val2),T), |
754 | | add_internal_error('Multiple occurences of variable: ',bind(Var,Value,Val2,PP)), |
755 | | fail. |
756 | | check_valid_store([_|T],PP) :- check_valid_store(T,PP). |
757 | | |
758 | | |