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(delay,[delay_setof_wf/7, | |
6 | delay_setof_check_wf/9, | |
7 | delay_setof_list_wf/5, | |
8 | %delay_call/2, delay_call/3, | |
9 | %delay_not/3, compute_wait_variables/3 | |
10 | not_with_enum_warning/4 | |
11 | ]). | |
12 | ||
13 | % meta_predicate annotations should appear before loading any code: | |
14 | :- meta_predicate my_findall(-,0,-,-). | |
15 | :- meta_predicate my_findall_catch(-,0,-,-,-). | |
16 | :- meta_predicate my_findall_catch(-,0,-,-,-,-). | |
17 | :- meta_predicate my_findall_check(-,0,-,-,0,0,-,-). | |
18 | ||
19 | :- meta_predicate delay_setof_wf(-,0,-,-,-,-,-). | |
20 | %:- meta_predicate block_my_findall_catch_wf(-,-,0,-,-,-). | |
21 | ||
22 | :- meta_predicate delay_setof_check_wf(-,0,-,-,-,0,0,-,-). | |
23 | :- meta_predicate block_findall_check(-,-,0,-,0,0,-,-,-,-). | |
24 | ||
25 | :- meta_predicate delay_setof_list_wf(-,0,-,-,-). | |
26 | ||
27 | ||
28 | %:- meta_predicate delay_call(0,-,-). | |
29 | %:- meta_predicate delay_call(0,-). | |
30 | ||
31 | %:- meta_predicate delay_not(0,-,-). | |
32 | :- meta_predicate not_with_enum_warning(0,-,?,?). | |
33 | :- meta_predicate not_with_enum_warning2(0,-,-,-). | |
34 | ||
35 | % -------------- | |
36 | ||
37 | ||
38 | ||
39 | :- use_module(module_information,[module_info/2]). | |
40 | :- module_info(group,kernel). | |
41 | :- module_info(description,'Utilities to delay calls until sufficiently instantiated.'). | |
42 | ||
43 | %:- use_module(self_check). | |
44 | ||
45 | :- use_module(tools). | |
46 | :- use_module(debug). /* so that calls can call unqualified debug_prints */ | |
47 | ||
48 | :- use_module(error_manager). | |
49 | :- use_module(kernel_tools). | |
50 | :- use_module(kernel_waitflags,[add_wd_error_span_now/4, init_wait_flags/2,ground_wait_flags/1, | |
51 | pending_abort_error/1]). | |
52 | ||
53 | ||
54 | :- use_module(tools_printing,[print_term_summary/1]). | |
55 | :- load_files(library(system), [when(compile_time), imports([environ/2])]). | |
56 | :- use_module(tools_meta,[call_residue/2]). | |
57 | ||
58 | :- if(environ(prob_debug_watch_flag,true)). | |
59 | :- meta_predicate call_residue_check(0). | |
60 | call_residue_check(Call) :- call(Call). | |
61 | my_findall(X,P,L,_) :- | |
62 | statistics(runtime,[Start,_]), | |
63 | findall(X,P,L), | |
64 | statistics(runtime,[End,_]), | |
65 | Tot is End-Start, | |
66 | (Tot>50 -> nl, %nl,print(Call),nl, | |
67 | print('*** FINDALL: '),print_term_summary(P), | |
68 | print('*** exceeded limit: '), print(Tot), print(' ms'),nl, | |
69 | length(L,Len), | |
70 | print('*** SOLUTIONS: '), print(Len), nl | |
71 | ; true). | |
72 | :- elif(environ(prob_safe_mode,true)). % not enabled by default; performance impact seems small; except for test 469 | |
73 | % for test 469 we have a call like this: delay:custom_explicit_sets:test_closure_and_convert/5: [_zzzz_unary]: [integer]: PRED(disjunct/2,z_ : #3906:{1,3,...,3906,3907} or z_ : 3908 .. 19532): VARIABLE: _348117: no_wf_available | |
74 | % with 19531 solutions | |
75 | :- meta_predicate call_residue_check(0). | |
76 | call_residue_check(Call) :- % print_term_summary(Call),nl, | |
77 | call_residue(Call,Residue), | |
78 | (Residue = [] -> true | |
79 | ; add_internal_error('Call had residue: ',residue(Residue)/call(Call)), | |
80 | print_goal(Residue),nl | |
81 | ). | |
82 | my_findall(X,P,L,ExpectedFinalResult) :- | |
83 | (ExpectedFinalResult==[] | |
84 | -> \+(call_residue_check(P)), | |
85 | L=[] % we know the end result to be empty; not necessary to try and find all solutions; <--- we should probably treat this somewhere else to ensure that we do not throw all_solutions enumeration warnings | |
86 | ; findall(X,call_residue_check(P),L) | |
87 | ). | |
88 | :- else. | |
89 | my_findall(X,P,L,ExpectedFinalResult) :- | |
90 | (ExpectedFinalResult==[] | |
91 | -> \+(P),L=[] % we know the end result to be empty; not necessary to try and find all solutions; <--- we should probably treat this somewhere else to ensure that we do not throw all_solutions enumeration warnings | |
92 | ; findall(X,P,L)). | |
93 | %; findall(X,(P,print(sol(X)),nl,nl,trace),L)). | |
94 | :- endif. | |
95 | ||
96 | ||
97 | ||
98 | ||
99 | my_findall_catch(X,P,L,ExpectedFinalResult,Span) :- | |
100 | my_findall_catch(X,P,L,ExpectedFinalResult,EnumWarningWhichOcc,Span), | |
101 | (enum_warning_occ(EnumWarningWhichOcc) -> throw(EnumWarningWhichOcc) ; true). | |
102 | ||
103 | enum_warning_occ(EnumWarningWhichOcc) :- | |
104 | nonvar(EnumWarningWhichOcc),EnumWarningWhichOcc=enumeration_warning(_,_,_,_,_). | |
105 | ||
106 | my_findall_catch(X,P,L,ExpectedFinalResult,EnumWarningWhichOcc,Span) :- | |
107 | enter_new_error_scope(Level,my_findall_catch), | |
108 | throw_enumeration_warnings_in_scope(Level,critical,Span), % critical enumeration warnings are thrown straight away | |
109 | call_cleanup( | |
110 | my_findall(X,P,L,ExpectedFinalResult), | |
111 | (event_occurred_in_error_scope(enumeration_warning(A,B,C,D,E)) | |
112 | -> exit_error_scope(Level,_,my_findall_catch_error), | |
113 | % do we need to throw the enumeration warning ? | |
114 | EnumWarningWhichOcc=enumeration_warning(A,B,C,D,E), | |
115 | debug_println(9,my_findall_catch(enumeration_warning(A,B,C,D,E))), | |
116 | true %throw(enumeration_warning(A,B,C,D,E)) | |
117 | ; exit_error_scope(Level,_,my_findall_catch_no_error), | |
118 | EnumWarningWhichOcc=false)). | |
119 | ||
120 | :- use_module(runtime_profiler,[observe_runtime_wf/4]). | |
121 | my_findall_check(X,P,L,ExpectedFinalResult,TimeOutCode,VirtualTimeOutCode,WF,Span) :- | |
122 | statistics(runtime,[Start,_]), | |
123 | statistics(walltime,[WStart,_]), Timer = [Start,WStart], | |
124 | get_total_number_of_errors(Nr1), % now also does count stored wd errors, see WD_SetCompr_Error | |
125 | %format('Start closure expansion at ~w ms~n',[Start]),print_message_span(Span),nl, | |
126 | call_cleanup((my_findall_catch(X,P,L,ExpectedFinalResult,EnumWarningWhichOcc,Span),Ok=true), | |
127 | (Ok==true,EnumWarningWhichOcc==false | |
128 | -> get_total_number_of_errors(Nr2), | |
129 | (Nr2>Nr1 -> add_set_compr_err(Nr1,Nr2,Span,WF), | |
130 | %TODO: this message is probably less useful / redundant now due to call stack info display | |
131 | fail % TO DO: see comment below in delay_setof_wf | |
132 | ; observe_runtime_wf(Timer,'==PERF-MESSAGE==> Long closure expansion: ',Span,WF) %, print(done),nl | |
133 | %,statistics(runtime,[End,_]), Tot is End-Start, | |
134 | %(Tot>10 -> length(L,Len),add_message(delay,'Long closure expansion:',ms_sols(Tot,Len),Span) ; true) | |
135 | ) | |
136 | ; /* failure or time-out; --> time-out as findall should never fail */ | |
137 | statistics(runtime,[End,_]), Tot is End-Start, | |
138 | (enum_warning_occ(EnumWarningWhichOcc) | |
139 | -> (VirtualTimeOutCode = _:true -> true | |
140 | ; print('### VIRTUAL TIME-OUT after: '), print(Tot), print(' ms'),nl, | |
141 | call(VirtualTimeOutCode) | |
142 | ), %print(throw(EnumWarningWhichOcc)),nl, | |
143 | throw(EnumWarningWhichOcc) % ??? this is a set-comprehension expression; failure would mean not-well-defined | |
144 | ; Tot>1000 -> % TO DO: could also be CTRL-C ! we could use catch_interrupt_assertion_call(my_findall_catch) or catch(my_finall_catch,user_interrupt_signal) | |
145 | call(TimeOutCode), % Warning: this call is also called if an outer-time-out is triggered ! | |
146 | format('Runtime for set comprehension expansion until TIME-OUT: ~w ms~n',[Tot]) | |
147 | % WHY DON'T WE FAIL HERE ---> because exception is passed on to outer calls after call_cleanup | |
148 | ; true) % check if the findall is probably responsible for the time-out | |
149 | )). | |
150 | ||
151 | add_set_compr_err(Nr1,Nr2,Span,WF) :- | |
152 | NrErrs is Nr2-Nr1, | |
153 | (NrErrs=1 -> Msg= 'Error occurred during expansion of set comprehension' | |
154 | ; ajoin(['Errors (',NrErrs,') occurred during expansion of set comprehension'],Msg) | |
155 | ), | |
156 | add_wd_error_span_now(Msg,'',Span,WF). | |
157 | % add_error_wf(well_definedness_error,Msg,'',Span,WF). | |
158 | ||
159 | /* ----------------------------------------- */ | |
160 | ||
161 | /* Below is a findall that delays until all | |
162 | non-output variables have become ground. | |
163 | Ideally, one would want a delay_findall that | |
164 | figures out by itself when it has all the answers | |
165 | (by looking at call_residue) and that may | |
166 | even progressively instantiate the output list | |
167 | such as in: | |
168 | delay_findall(X,delay_member(X,[a|T]),R), delay_member(Z,R) | |
169 | But this will require more involved machinery. | |
170 | */ | |
171 | ||
172 | ||
173 | :- use_module(kernel_objects,[equal_object_wf/4]). | |
174 | :- use_module(kernel_tools,[ground_value_check/2]). | |
175 | :- use_module(kernel_waitflags,[start_attach_inner_abort_errors/2, re_attach_pending_inner_abort_errors/3]). | |
176 | ||
177 | % the following is called by expand_normal_closure_direct | |
178 | % which uses ground_inner_wait_flags_in_context, which registers pending WD errors | |
179 | % these are re-attached to the outer WF by re_attach_pending_inner_abort_errors | |
180 | delay_setof_wf(V,G,FullSetResult,WVars,Done,WF,Span) :- %print(delay_set_of(V)),nl, | |
181 | ground_value_check(WVars,GW), | |
182 | block_my_findall_catch_wf2(GW,V,G,FullSetResult,Done,WF,Span). | |
183 | % comment in to perform idling to allow outer co-routines to run; useful when WD condition attached to Body G | |
184 | %:- use_module(kernel_waitflags,[get_idle_wait_flag/3]). | |
185 | %:- block block_my_findall_catch_wf(-,?,?,?,?,?). | |
186 | %block_my_findall_catch_wf(_,V,G,FullSetResult,Done,WF) :- | |
187 | % get_idle_wait_flag(delay_setof_wf,WF,LWF), | |
188 | % print(idling(WF,LWF)),nl, | |
189 | % block_my_findall_catch_wf2(LWF,V,G,FullSetResult,Done,WF,Span). | |
190 | :- block block_my_findall_catch_wf2(-,?,?,?,?,?,?). | |
191 | block_my_findall_catch_wf2(_,V,G,FullSetResult,Done,WF,Span) :- | |
192 | get_total_number_of_errors(Nr1), | |
193 | start_attach_inner_abort_errors(Level,block_my_findall_catch_wf2), | |
194 | call_cleanup(my_findall_catch(V,G,RRes,FullSetResult,Span), | |
195 | re_attach_pending_inner_abort_errors(Level,WF,Pending)), | |
196 | transform_result_into_set(RRes,SetRes), | |
197 | get_total_number_of_errors(Nr2), %print(f(Nr1,Nr2)),nl, | |
198 | (Nr2>Nr1 | |
199 | -> add_set_compr_err(Nr1,Nr2,Span,WF), % should we use add_wd_error_span('...: ','@compr'(..),Span,WF) | |
200 | fail | |
201 | % TO DO?: we could add_abort error here instead of adding a real error | |
202 | % for this, however, the inner abort_errors should only be recorded, not yet raised for the user | |
203 | ; true), | |
204 | ? | eq_object_findall_result(SetRes,FullSetResult,Pending,WF), |
205 | Done=true. | |
206 | ||
207 | eq_object_findall_result(SetRes,FullSetResult,_Pending,WF) :- | |
208 | ? | equal_object_wf(SetRes,FullSetResult,delay_setof_wf,WF). |
209 | % TODO: activate the following: see test 2459 and test 1921 | |
210 | %eq_object_findall_result(SetRes,FullSetResult,Pending,WF) :- | |
211 | % (Pending=pending_abort_errors, get_preference(find_abort_values,true) | |
212 | % -> true, write(wd_error),nl % avoid instantiating result to avoid failing on result value (which is not wd anyway) | |
213 | % ; equal_object_wf(SetRes,FullSetResult,delay_setof_wf,WF) | |
214 | % ). | |
215 | ||
216 | % called by expand_normal_closure2, calling b_test_closure | |
217 | % which uses ground_inner_wait_flags_in_context, which registers pending WD errors | |
218 | % these are re-attached to the outer WF by re_attach_pending_inner_abort_errors | |
219 | delay_setof_check_wf(V,G,FullSetResult,WVars,Done,TimeOutCode,VirtualTimeOutCode,WF,Span) :- %print(delay_set_of(V)),nl, | |
220 | %% print(wait_vars(WVars,G)),nl, %% | |
221 | ground_value_check(WVars,GW), | |
222 | block_findall_check(GW,V,G,FullSetResult,TimeOutCode,VirtualTimeOutCode,Done,FullSetResult,WF,Span). | |
223 | ||
224 | :- block block_findall_check(-,?,?,?,?,?,?,?,?,?). | |
225 | block_findall_check(_,V,G,FullSetResult,TimeOutCode,VirtualTimeOutCode,Done,FullSetResult,WF,Span) :- | |
226 | start_attach_inner_abort_errors(Level,block_findall_check), | |
227 | call_cleanup(my_findall_check(V,G,RRes,FullSetResult,TimeOutCode,VirtualTimeOutCode,WF,Span), | |
228 | re_attach_pending_inner_abort_errors(Level,WF,Pending)), | |
229 | transform_result_into_set(RRes,SetRes), % will generate AVL tree | |
230 | % print(delay_setof_result(SetRes,FullSetResult)),nl, translate:print_bvalue(SetRes),nl, | |
231 | eq_object_findall_result(SetRes,FullSetResult,Pending,WF), | |
232 | Done=true. | |
233 | ||
234 | :- use_module(tools_printing,[print_term_summary/1]). | |
235 | :- use_module(custom_explicit_sets,[convert_to_avl/2]). | |
236 | :- use_module(closures,[is_symbolic_closure/1]). | |
237 | transform_result_into_set([ONE],SetRes) :- is_symbolic_closure(ONE),!, | |
238 | debug_println(9,not_expanding_singleton_delay_result), | |
239 | % do not convert_to_avl; would lead to enumeration warning (see test 2157) | |
240 | SetRes = [ONE]. | |
241 | transform_result_into_set(RRes,SetRes) :- % print(transform_result_into_set(RRes,SetRes)), | |
242 | (convert_to_avl(RRes,SetRes) % we are sure that RRes is ground !!?? | |
243 | -> true | |
244 | ; print_term_summary(convert_to_avl_failed(RRes,SetRes)), | |
245 | convert_list_of_expressions_into_set(RRes,SetRes)). | |
246 | ||
247 | :- use_module(b_interpreter,[convert_list_of_expressions_into_set_wf/4]). | |
248 | convert_list_of_expressions_into_set(List,Set) :- | |
249 | init_wait_flags(WF,[convert_list_of_expressions_into_set]), | |
250 | convert_list_of_expressions_into_set_wf(List,Set,set(any),WF), | |
251 | ground_wait_flags(WF). | |
252 | ||
253 | /* same as above but Result is a list of elements; */ | |
254 | /* the list should not be interpreted as a set, but each element is a value for a parameter */ | |
255 | /* There is a very small chance that the same value is represented twice in the list (e.g., once as closure once as explicit list) */ | |
256 | % last argument is simple waitflag | |
257 | % used for forall-domain | |
258 | ||
259 | :- block delay_setof_list_wf(?,?,?,-,?). | |
260 | delay_setof_list_wf(V,G,FullSetResult,_BodyGround,WF) :- | |
261 | start_attach_inner_abort_errors(Level,delay_setof_list_wf), | |
262 | call_cleanup(my_findall(V,G,RRes,FullSetResult), | |
263 | re_attach_pending_inner_abort_errors(Level,WF,_Pending)), | |
264 | ll_norm(RRes,NormRRes), | |
265 | sort(NormRRes,SNormRRes), % removes duplicates | |
266 | FullSetResult=SNormRRes. % Note: we instantiate even if Pending=pending_abort_errors | |
267 | ||
268 | ||
269 | % normalise a list of list of values; the inner lists are not sets but values for parameters | |
270 | ll_norm([],[]). | |
271 | ll_norm([El1|T1],[El2|T2]) :- l_check_norm_required(El1,El2,NormRequired), | |
272 | (var(NormRequired) -> T1=T2 % no normalisation required: simply copy rest of list | |
273 | % TO DO: we could also statically determine based on parameter types whether normalising is required | |
274 | ; ll_norm2(T1,T2)). | |
275 | ||
276 | :- use_module(store,[l_normalise_values/2]). | |
277 | ll_norm2([],[]). | |
278 | ll_norm2([El1|T1],[El2|T2]) :- l_normalise_values(El1,El2), ll_norm2(T1,T2). | |
279 | ||
280 | % normalise a value and return norm_required in last argument if it is needed | |
281 | l_check_norm_required([],[],_). | |
282 | l_check_norm_required([H|T],[NH|NT],NormRequired) :- | |
283 | check_norm_required(H,NH,NormRequired), | |
284 | l_check_norm_required(T,NT,NormRequired). | |
285 | ||
286 | check_norm_required(pred_true,R,_) :- !, R=pred_true. | |
287 | check_norm_required(pred_false,R,_) :- !, R=pred_false. | |
288 | check_norm_required(int(S),R,_) :- !, R=int(S). | |
289 | check_norm_required(fd(X,T),R,_) :- !, R=fd(X,T). | |
290 | check_norm_required(string(S),R,_) :- !, R=string(S). | |
291 | check_norm_required((A,B),(NA,NB),NormRequired) :- !, | |
292 | check_norm_required(A,NA,NormRequired), check_norm_required(B,NB,NormRequired). | |
293 | % to do: add record and freeval | |
294 | check_norm_required(V,NV,norm_required) :- | |
295 | store:normalise_value(V,NV). % does not normalise closure/3 values | |
296 | ||
297 | ||
298 | ||
299 | ||
300 | ||
301 | %:- use_module(tools,[remove_variables/3]). | |
302 | %compute_wait_variables(WaitTerm,OutputVars,WaitVars) :- | |
303 | % term_variables(WaitTerm,Vars), | |
304 | % term_variables(OutputVars,RealOutputVars), | |
305 | % remove_variables(Vars,RealOutputVars,WaitVars). | |
306 | ||
307 | ||
308 | %delay_call(Call,WaitTerm,OutputVars) :- | |
309 | % compute_wait_variables(WaitTerm,OutputVars,WaitVars), | |
310 | %print_message(delay(Call,WaitVars)), | |
311 | % when(ground(WaitVars),Call). | |
312 | ||
313 | %delay_call(Call,OutputVars) :- | |
314 | % delay_call(Call,Call,OutputVars). | |
315 | ||
316 | % LocalWF: created by create_inner_wait_flags; enumeration finished waitflag should not be grounded here | |
317 | %delay_not(Call,OutputVars, LocalWF) :- % print_message(informational,delay_not(Call,OutputVars,LocalWF)), | |
318 | % delay_call( not_with_enum_warning(Call, LocalWF) , OutputVars). | |
319 | ||
320 | :- use_module(probsrc(kernel_waitflags),[add_message_wf/5]). | |
321 | not_with_enum_warning(Call, LocalWF, PP, Span) :- | |
322 | %% print_term_summary(neg_call(Call, LocalWF)), %% | |
323 | enter_new_clean_error_scope(Level), | |
324 | call_cleanup((not_with_enum_warning2(Call,Level,LocalWF,Span) -> Ok=true ; Ok=false), | |
325 | ((var(Ok), silent_mode(off) | |
326 | -> add_message_wf(delay,'TIME OUT or Exception inside: ',PP,Span,LocalWF) | |
327 | ; true), | |
328 | exit_error_scope(Level,_ErrOccured,not_with_enum_warn))), | |
329 | Ok==true. | |
330 | ||
331 | :- use_module(tools_printing,[print_goal/1]). | |
332 | :- use_module(preferences,[get_preference/2]). | |
333 | :- use_module(kernel_waitflags,[add_error_wf/5, add_warning_wf/5]). | |
334 | not_with_enum_warning2(Call,Level,LocalWF,Span) :- | |
335 | (pending_abort_error(LocalWF) | |
336 | -> add_warning_wf(not_with_enum_warning,'Abort error pending before call:',Level,Span,LocalWF),nl | |
337 | ; true), | |
338 | ? | (call_residue(Call,Residue) -> |
339 | % Call has succeeded, negation thus fails | |
340 | (pending_abort_error(LocalWF) | |
341 | -> write(pending_abort_error(LocalWF)),nl, | |
342 | PENDING_ABORT = true | |
343 | % we do not fail in this case, so that abort errors can be raised | |
344 | % relevant for test 1966 or predicate f={1|->2} & not(#s.(s:1..2 & f(s)=3)) with -p TRY_FIND_ABORT TRUE | |
345 | ; Residue \= [] -> | |
346 | (get_preference(use_chr_solver,true) | |
347 | -> add_warning_wf(not_with_enum_warning,'Call (in negation) had residue (possibly due to use of CHR making call_residue imprecise): ',residue(Residue)/call(Call),Span,LocalWF) | |
348 | ; add_error_wf(not_with_enum_warning, | |
349 | 'Call (in negation) had residue: ',residue(Residue)/call(Call),Span,LocalWF), | |
350 | print_goal(Residue),nl | |
351 | ), | |
352 | fail | |
353 | ; clear_enumeration_warning_in_error_scope(Level), fail | |
354 | % call has succeeded without pending abort errors | |
355 | ) | |
356 | ; true | |
357 | ), | |
358 | % Note: everything else is ground; so Call should not trigger any other co-routines/enumeration ?! | |
359 | Event = enumeration_warning(_,_,_,_,_), | |
360 | (event_occurred_in_error_scope(Event) % critical ? only at this level ? or also below ? | |
361 | -> PENDING_ABORT==true, %print(grd(LocalWF)),nl, kernel_waitflags:portray_waitflags(LocalWF),nl, | |
362 | ground_wait_flags(LocalWF), % raise any potential abort errors | |
363 | debug_println(19,grounded_wait_flag_for_pending_abort_error), % THIS print is important due to issue SPRM-20473 in SICStus Prolog which will otherwise *not* activate the pending co-routines attached to LocalWF ! | |
364 | fail | |
365 | %, print_message(throwing(Event)), throw(Event) % or simply re-post enum warning ? | |
366 | % we could also simply fail and raise an enumeration warning; meaning we havent explored all possibilities | |
367 | % Note: at the moment the error is copied into the outer scope by copy_error_scope_events | |
368 | ; true | |
369 | ). | |
370 | ||
371 | ||
372 |