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