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