1 % (c) 2009-2020 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(evalstores,[
6 evalstore_reset/0
7 ,evalstore_create_type_env_by_state/2
8 ,evalstore_create_store_by_state/2
9 ,evalstore_eval_formula/4
10 ,evalstore_bindings/2
11 ]).
12
13 :- use_module(module_information,[module_info/2]).
14 :- module_info(group,misc).
15 :- module_info(description,'This module provides methods to construct stores dynamically and evaluate expressions in them, possibly used only by ProB1 for Rodin.').
16
17 :- use_module(library(lists)).
18 :- use_module(library(samsort),[samsort/3]).
19 :- use_module(tools_meta,[safe_time_out_or_virtual_time_out/3]). %:- use_module(library(timeout),[time_out/3]).
20
21 :- use_module(state_space, [visited_expression/2]).
22 :- use_module(specfile, [state_corresponds_to_set_up_constants/2
23 ,state_corresponds_to_initialised_b_machine/1]).
24 :- use_module(bsyntaxtree, [create_texpr/4
25 ,get_texpr_type/2]).
26 :- use_module(b_global_sets, [is_b_global_constant/3
27 ,b_global_set/1]).
28 :- use_module(bmachine, [full_b_machine/1
29 ,b_get_machine_constants/1
30 ,b_get_machine_variables/1]).
31 :- use_module(bmachine_construction,[type_open_formula/8]).
32 :- use_module(btypechecker, [env_empty/1
33 ,add_identifiers_to_environment/3
34 ,env_lookup_type/3
35 ,env_identifiers/2]).
36 :- use_module(store, [empty_state/1
37 ,normalise_store/2
38 ,merge_updates/3]).
39 :- use_module(kernel_waitflags,[init_wait_flags/1
40 ,ground_wait_flags/1]).
41 :- use_module(b_interpreter, [set_up_typed_localstate/6
42 ,b_test_boolean_expression/4
43 ,b_compute_expression/5]).
44 :- use_module(b_enumerate, [b_tighter_enumerate_values/2]).
45 :- use_module(error_manager, [get_all_errors_and_clear/1
46 ,reset_errors/0]).
47
48 :- use_module(extension('user_signal/user_signal'),[protect_from_user_interrupt_det/1]).
49 :- use_module(extension('probhash/probhash'),[hash_term/2]).
50
51 % Each node represents a variable binding like a state in the state space
52 % The main difference to a state in the state space is that we usually have an evolution
53 % of nodes by adding successively new variables.
54
55 % A node is encoded with terms that describe combinations / references to other states
56 % (see expand_node/2 for details).
57 %
58
59 :- dynamic stored_evalstores/3. % stored_evalstores(EvalstoreId,Store,TypeEnvId)
60 :- dynamic evalstore_hashes/2. % evalstore_hashes(Hash,EvalstoreId)
61 :- dynamic next_evalstore_id/1. % next_evalstore_id(EvalstoreId)
62
63 :- dynamic stored_type_environment/2. % stored_type_environment(TypeEnvId,TypeEnv)
64 :- dynamic type_environment_hashes/2. % type_environment_hashes(Hash,TypeEnvId)
65 :- dynamic next_type_environment_id/1. % next_type_environment_id(TypeEnvId)
66 %:- dynamic standard_type_env/2. % standard_type_env(Description,TypeEnvId)
67
68 % remove all existing nodes
69 evalstore_reset :-
70 protect_from_user_interrupt_det(reset_evalstores2).
71 reset_evalstores2 :-
72 retractall(stored_evalstores(_,_,_)),
73 retractall(evalstore_hashes(_,_)),
74 retractall(next_evalstore_id(_)),
75 assert(next_evalstore_id(1)),
76 retractall(stored_type_environment(_,_)),
77 retractall(next_type_environment_id(_)),
78 retractall(type_environment_hashes(_,_)),
79 assert(next_type_environment_id(1)).
80
81
82 store_type_environment(Env,Id) :-
83 hash_type_env(Env,Hash),
84 ( type_environment_hashes(Hash,ExistingId) ->
85 Id = ExistingId
86 ; otherwise ->
87 assert_type_env(Env,Hash,Id)).
88 assert_type_env(Env,Hash,Id) :-
89 protect_from_user_interrupt_det(assert_type_env2(Env,Hash,Id1)),
90 Id1=Id.
91 assert_type_env2(Env,Hash,Id) :-
92 retract(next_type_environment_id(Id)),
93 Next is Id+1,
94 assert(next_type_environment_id(Next)),
95 assert(stored_type_environment(Id,Env)),
96 assert(type_environment_hashes(Hash,Id)).
97
98 create_new_node(NodeExpr,TypeEnvId,EvalstoreId) :-
99 expand_node(NodeExpr,Store),
100 hash_node(Store,TypeEnvId,Hash),
101 ( evalstore_hashes(Hash,Id) ->
102 EvalstoreId = Id
103 ; otherwise ->
104 assert_new_node(NodeExpr,Hash,TypeEnvId,EvalstoreId)).
105
106 hash_node(Store,TypeEnvId,Hash) :-
107 hash_term(Store/TypeEnvId,Hash).
108
109 assert_new_node(Node,Hash,TypeEnvId,Id) :-
110 % the assert should be protected from interrupts to prevent an inconsistent database
111 protect_from_user_interrupt_det(assert_new_node2(Node,Hash,TypeEnvId,Id2)),
112 Id=Id2.
113 assert_new_node2(Node,Hash,TypeEnvId,Id) :-
114 retract(next_evalstore_id(Id)),
115 Next is Id+1,
116 assert(next_evalstore_id(Next)),
117 assert(evalstore_hashes(Hash,Id)),
118 assert(stored_evalstores(Id,Node,TypeEnvId)).
119
120 % expand_node(NodeExpr,Store):
121 % get the full store that the node represents
122 expand_node(Node,Store) :-
123 expand_node2(Node,UStore),
124 samsort(cmp_bind,UStore,Store).
125 expand_node2(empty,Store) :-
126 empty_state(Store).
127 expand_node2(state(StateId),Store) :- % refers to a state in the state space
128 ( StateId=root -> expand_node2(empty,Store)
129 ; otherwise ->
130 visited_expression(StateId,State),
131 state_corresponds_to_set_up_constants(State,Store)).
132 expand_node2(store(Store),Store). % <- directly defines a store
133 expand_node2(update(Orig,New),Store) :- % <- updates the values of a store by another one,
134 expand_node2(Orig,OrigStore), % the new store overrides old values
135 expand_node2(New,NewStore),
136 merge_updates(OrigStore,NewStore,Store).
137
138 cmp_bind(bind(A,_),bind(B,_)) :- A @< B.
139
140 % Generate a hash of the normalised type environment
141 hash_type_env(Env,Hash) :-
142 env_identifiers(Env,Ids), % Ids is sorted
143 maplist(lookup_for_type(Env),Ids,Types),
144 hash_term(Types,Hash).
145 lookup_for_type(Env,Id,type(Id,Type)) :-
146 env_lookup_type(Id,Env,Type).
147
148 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
149 % Type Environments
150 extract_type_environment(State,Env) :-
151 % by starting with a list of sorted identifiers, we try to make
152 % sure that two environments with the same identifiers and types
153 % are treated as equal.
154 extract_type_environment2(State,UIds),
155 create_normalised_type_environment(UIds,Env).
156 create_normalised_type_environment(UIds,Env) :-
157 sort(UIds,Ids),
158 env_empty(Empty),
159 add_identifiers_to_environment(Ids,Empty,Env).
160
161 extract_type_environment2(root,Ids) :-
162 % the root node has already some identifiers in the type environment:
163 % deferred sets, enumerated sets and their elements
164 !,global_identifiers(Ids,[]).
165 extract_type_environment2(State,Ids) :-
166 state_corresponds_to_initialised_b_machine(State),!,
167 global_identifiers(Ids,I1),
168 constant_identifiers(I1,I2),
169 variable_identifiers(I2,[]).
170 extract_type_environment2(_State,Ids) :-
171 global_identifiers(Ids,I1),
172 constant_identifiers(I1,[]).
173
174 global_identifiers -->
175 % the enumerated set elements:
176 findall(TId,
177 (is_b_global_constant(G,_,N),create_texpr(identifier(N),global(G),[],TId))),
178 % the deferred/enumerated sets:
179 findall(TId,
180 (b_global_set(G),create_texpr(identifier(G),set(global(G)),[],TId))).
181 constant_identifiers(In,Out) :-
182 b_get_machine_constants(Csts),
183 append(Csts,Out,In).
184 variable_identifiers(In,Out) :-
185 b_get_machine_variables(Vars),
186 append(Vars,Out,In).
187
188 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
189 % evaluation
190 eval_in_evalstore(TypedFormula,StoreExpr,NewIdentifiers,Timeout,Result) :-
191 reset_errors,
192 expand_node(StoreExpr,Store),
193 get_texpr_type(TypedFormula,Type),
194 empty_state(Empty),
195 set_up_typed_localstate(NewIdentifiers,_NewValues,TypedVals,Empty,LocalStore,positive),
196 init_wait_flags(WF),
197 b_tighter_enumerate_values(TypedVals,WF),
198 time_out_eval(Timeout,Type,TypedFormula,LocalStore,Store,WF,Result1,TOResult),
199 ( TOResult \== success ->
200 Result = timeout
201 ; error_occurred(Result1,Msg) ->
202 Result = error(Msg)
203 ; Result1 = ok(V,ResultStore) ->
204 update_store(StoreExpr,ResultStore,NewStore),
205 Result = ok(V,NewStore)
206 ).
207 update_store(OldStore,AdditionalStore,NewStore) :-
208 empty_state(AdditionalStore),!,OldStore=NewStore.
209 update_store(OldStore,AdditionalStore,update(OldStore,store(AdditionalStore))).
210
211 time_out_eval(none,Type,TypedFormula,LocalStore,Store,WF,Result,TOResult) :-
212 !,evaluate_formula(Type,TypedFormula,LocalStore,Store,WF,Result1),
213 Result=Result1,TOResult=success.
214 time_out_eval(Timeout,Type,TypedFormula,LocalStore,Store,WF,Result,TOResult) :-
215 safe_time_out_or_virtual_time_out( evaluate_formula(Type,TypedFormula,LocalStore,Store,WF,Result),
216 Timeout,
217 TOResult),!.
218
219 evaluate_formula(pred,F,LS,S,WF,ok(pred(V),ResultStore)) :- !,
220 ( b_test_boolean_expression(F,LS,S,WF), ground_wait_flags(WF) ->
221 normalise_store(LS,ResultStore), V=true
222 ; otherwise ->
223 empty_state(ResultStore), V=false).
224 evaluate_formula(subst,_F,_LS,_S_,_WF,error('Substitutions are not yet supported')) :- !.
225 evaluate_formula(_Type,F,LS,S,WF,ok(value(Value),ResultStore)) :-
226 b_compute_expression(F,LS,S,Value,WF),!,
227 empty_state(ResultStore).
228
229 :- use_module(library(codesio),[write_to_codes/2]).
230 :- use_module(tools_strings,[atom_codes_with_limit/3]).
231 error_occurred(error(ErrorMsg),ErrorMsg) :- !.
232 error_occurred(_,ErrorMsg) :-
233 get_all_errors_and_clear([Error|_]),
234 write_to_codes(Error,ErrorCodes),
235 atom_codes_with_limit(ErrorMsg,200,ErrorCodes).
236
237
238 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
239 % type checking
240 evalstore_typecheck(Raw,EnvId,Result) :-
241 stored_type_environment(EnvId,Env),
242 full_b_machine(Machine),
243 AllowNewIds=false,
244 type_open_formula(Raw,[env(Env)],AllowNewIds,Machine,_Type,NewIdentifiers,TExpr,Errors),
245 ( Errors = [] ->
246 evalstore_typecheck_update_typeenv(NewIdentifiers,Env,EnvId,NewEnvId),
247 Result=ok(TExpr,NewIdentifiers,NewEnvId)
248 ; otherwise ->
249 Result=errors(Errors)).
250 evalstore_typecheck_update_typeenv([],_Env,EnvId,NewEnvId) :-
251 !, EnvId = NewEnvId.
252 evalstore_typecheck_update_typeenv(NewIdentifiers,Env,_EnvId,NewEnvId) :-
253 add_identifiers_to_environment(NewIdentifiers,Env,NewEnv),
254 store_type_environment(NewEnv,NewEnvId).
255
256
257 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
258 % entry points
259 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
260 % type environments
261
262 evalstore_create_type_env_by_state(StateId,EnvId) :-
263 ( StateId=root -> State=root
264 ; otherwise -> visited_expression(StateId,State)),
265 extract_type_environment(State,Env),
266 store_type_environment(Env,EnvId).
267
268 evalstore_create_store_by_state(StateId,EvalstoreId) :-
269 evalstore_create_type_env_by_state(StateId,EnvId),
270 create_new_node(state(StateId),EnvId,EvalstoreId).
271
272 evalstore_eval_formula(EvalstoreId,Raw,Timeout,Result) :-
273 stored_evalstores(EvalstoreId,StoreExpr,EnvId),
274 evalstore_typecheck(Raw,EnvId,TypeResult),
275 evalstore_eval_formula2(TypeResult,StoreExpr,Timeout,Result).
276 evalstore_eval_formula2(errors(Errors),_StoreExpr,_Timeout,errors(Errors)).
277 evalstore_eval_formula2(ok(TExpr,NewIdentifiers,NewEnvId),StoreExpr,Timeout,Result) :-
278 eval_in_evalstore(TExpr,StoreExpr,NewIdentifiers,Timeout,EvalResult),
279 evalstore_eval_formula3(EvalResult,NewIdentifiers,NewEnvId,Result).
280 evalstore_eval_formula3(error(Msg),_Ids,_EnvId,errors([Msg])).
281 evalstore_eval_formula3(timeout,_Ids,_EnvId,timeout).
282 evalstore_eval_formula3(ok(Value,NewStore),Ids,EnvId,ok(Value,Ids,StoreId)) :-
283 create_new_node(NewStore,EnvId,StoreId).
284
285 evalstore_bindings(EvalstoreId,Binding) :-
286 stored_evalstores(EvalstoreId,StoreExpr,_),
287 expand_node(StoreExpr,Binding).
288
289 :- use_module(eventhandling,[register_event_listener/3]).
290 :- register_event_listener(specification_initialised,evalstore_reset,
291 'Initialise module evalstore').