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