1		% (c) 2012-2019 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(external_functions,[call_external_function/7, call_external_predicate/8,
6		call_external_substitution/6,
7		reset_external_functions/0,
8		external_pred_always_true/1,
9		reset_side_effect_occurred/0,
10		side_effect_occurred/1,
11		performs_io/1, not_declarative/1,
12		is_external_function_name/1,
13		external_subst_enabling_condition/3,
14		external_fun_has_wd_condition/1,
15		external_fun_can_be_inverted/1,
16		do_not_evaluate_args/1,
17		reset_argv/0, set_argv_from_list/1, set_argv_from_atom/1,
18
19		observe_parameters/2, observe_state/1, observe_value/2
20		]).
21
22		% Note: there is also the predicate external_procedure_used/1 in bmachine_construction
23
24		:- use_module(error_manager).
25		:- use_module(self_check).
26		:- use_module(library(avl)).
27		:- use_module(library(lists)).
28		:- use_module(translate).
29
30		% TO DO: add external Prolog files
31		% Should we do auto-conversion of B to Prolog types ,... ?
32
33		:- use_module(kernel_waitflags).
34		:- use_module(debug).
35		:- use_module(bsyntaxtree).
36
37		:- use_module(module_information,[module_info/2]).
38		:- module_info(group,external_functions).
39		:- module_info(description,'This module provides a way to call external functions and predicates.').
40
41		:- dynamic side_effect_occurred/1.
42		% TRUE if a side effect has occured
43		% possible values (user_output, file)
44		reset_side_effect_occurred :- retractall(side_effect_occurred(_)).
45		assert_side_effect_occurred(Location) :-
46		(side_effect_occurred(Location) -> true ; assert(side_effect_occurred(Location))).
47
48		:- discontiguous expects_waitflag/1.
49		:- discontiguous expects_spaninfo/1.
50		:- discontiguous expects_type/1. % only used for external functions, not predicates or subst
51		:- discontiguous performs_io/1.
52		:- discontiguous is_not_declarative/1. % does not perform io but is still not declarative
53		:- discontiguous does_not_modify_state/1.
54		:- discontiguous expects_unevaluated_args/1. % currently only used for external predicates
55		:- discontiguous do_not_evaluate_args/1. % currently only used for external predicates
56		:- discontiguous expects_state/1. % currently only used for external predicates
57		:- discontiguous external_pred_always_true/1. % external predicates which are always true
58		:- discontiguous external_subst_enabling_condition/3. % external predicates which are always true
59		:- discontiguous external_fun_has_wd_condition/1.
60		:- discontiguous external_fun_can_be_inverted/1.
61		:- discontiguous external_fun_type/3. % external_fun_type(FUN,ListOfTypeParameters,ListOfArgTypes); also applicable to external predicates
62
63		:- meta_predicate safe_call(0,-).
64
65		not_declarative(FunName) :- (performs_io(FunName) -> true ; is_not_declarative(FunName)).
66
67		is_external_function_name(Name) :- external_fun_type(Name,_,_).
68		is_external_function_name(Name) :- expects_waitflag(Name), \+ external_fun_type(Name,_,_).
69		is_external_function_name(Name) :- expects_spaninfo(Name), \+ expects_waitflag(Name), \+ external_fun_type(Name,_,_).
70		is_external_function_name(Name) :- external_subst_enabling_condition(Name,_,_),
71		\+ expects_spaninfo(Name), \+ expects_waitflag(Name), \+ external_fun_type(Name,_,_).
72
73
74		:- assert_must_succeed(( external_functions:call_external_function('COS',[b(integer(0),integer,[])],
75		[int(0)],int(100),integer,unknown,_WF) )).
76		:- assert_must_succeed(( external_functions:call_external_function('SIN',[b(integer(0),integer,[])],
77		[int(0)],int(0),integer,unknown,_WF) )).
78		% first a few hard-wired external functions for efficiency:
79		call_external_function('COS',_,[X],Value,_,_,_WF) :- !, 'COS'(X,Value). % already use safe_is
80		call_external_function('SIN',_,[X],Value,_,_,_WF) :- !, 'SIN'(X,Value).
81		call_external_function('TAN',_,[X],Value,_,_,_WF) :- !, 'TAN'(X,Value).
82		%call_external_function('STRING_APPEND',_,[A,B],Value,_,_,WF) :- !, 'STRING_APPEND'(A,B,Value,WF). % do we need safe_call?
83		%call_external_function('STRING_LENGTH',_,[A],Value,_,_,_WF) :- !, 'STRING_LENGTH'(A,Value).
84		% now the generic case:
85		call_external_function(F,Args,EvaluatedArgs,Value,Type,SpanInfo,WF) :-
86		(expects_waitflag(F) -> E1=[WF] ; E1=[]),
87		(expects_spaninfo(F) -> E2=[SpanInfo|E1] ; E2=E1),
88		(expects_unevaluated_args(F) -> E3=[Args|E2] ; E3=E2),
89		(expects_type(F) -> E4=[Type|E3] ; E4=E3),
90		append(EvaluatedArgs,[Value|E4],AV),
91		% Check if there is better way to do this
92		Call =.. [F|AV],
93		% print('EXTERNAL FUNCTION CALL: '), print(F), print(' '), print(Call),nl,
94		safe_call(Call,SpanInfo)
95		%, print(result(Value)),nl.
96		.
97
98		call_external_predicate(F,Args,EvaluatedArgs,LocalState,State,PREDRES,SpanInfo,WF) :-
99		(expects_waitflag(F) -> E1=[WF] ; E1=[]),
100		(expects_spaninfo(F) -> E2=[SpanInfo|E1] ; E2=E1),
101		(expects_unevaluated_args(F) -> E3=[Args|E2] ; E3=E2),
102		(expects_state(F) -> E4=[LocalState,State|E3] ; E4=E3),
103		append(EvaluatedArgs,[PREDRES|E4],AV),
104		Call =.. [F|AV],
105		% print('EXTERNAL PREDICATE CALL: '), print(Call),nl, %%
106		safe_call(Call,SpanInfo).
107
108		call_external_substitution(FunName,Args,InState,OutState,Info,WF) :-
109		% TO DO: signal if substitution can be backtracked
110		get_wait_flag_for_subst(FunName,WF,Flag),
111		(does_not_modify_state(FunName) -> OutState=[] ; OutState = OutState2),
112		call_external_substitution2(Flag,FunName,Args,InState,OutState2,Info,WF).
113
114		get_wait_flag_for_subst(FunName,WF,Flag) :- perform_directly(FunName),!,
115		get_wait_flag1(WF,Flag). % ensure that precondition, ... have been evaluated
116		get_wait_flag_for_subst(FunName,WF,Flag) :- performs_io(FunName),!,
117		get_enumeration_finished_wait_flag(WF,Flag). % ensure that precondition, ... have been evaluated
118		% get_enumeration_starting_wait_flag(external(FunName),WF,Flag).
119		get_wait_flag_for_subst(FunName,WF,Flag) :- get_binary_choice_wait_flag(external(FunName),WF,Flag).
120
121		:- block call_external_substitution2(-,?,?,?,?,?,?).
122		call_external_substitution2(_,F,Args,InState,OutState,_Info,WF) :-
123		(expects_waitflag(F) -> E1=[WF] ; E1=[]),
124		(expects_spaninfo(F) -> E2=[SpanInfo|E1] ; E2=E1),
125		append(Args,[InState,OutState|E2],AV),
126		Call =.. [F|AV],
127		% print('EXTERNAL SUBSTITUTION CALL: '), print(Call),nl, %%
128		safe_call(Call,SpanInfo).
129
130		safe_call(X,SpanInfo) :-
131		on_exception(Exception, call(X),
132		(add_exception_error(Exception,X,SpanInfo),fail)).
133
134		%safe_is(Context,X,Y) :- safe_is(Context,X,Y,unknown).
135		safe_is(Context,X,Y,Span) :- % print(safe_is(Context,X,Y)),nl,
136		on_exception(Exception, X is Y,
137		(add_exception_error(Exception,Context,Span),fail)). %, print(res(X)),nl.
138
139		add_exception_error(Exception,Context,Span) :-
140		get_function_call_info(Context,SimplifiedContext),
141		add_exception_error2(Exception,SimplifiedContext,Span),
142		(debug:debug_mode(on) -> tools_printing:print_term_summary(Context),nl ; true).
143
144		get_function_call_info(external_functions:X,Func) :- nonvar(X),!,functor(X,Func,_Arity).
145		get_function_call_info(M:X,M:Func) :- nonvar(X),!,functor(X,Func,_Arity).
146		get_function_call_info(X,X).
147
148		add_exception_error2(error(existence_error(procedure,external_functions:FUN),_),_X,SpanInfo) :- !,
149		add_error(external_functions,'### EXTERNAL function does not exist (check that you have an up-to-date version of ProB): ',FUN,SpanInfo).
150		add_exception_error2(error(undefined,ERR),X,SpanInfo) :-
151		is_error(ERR),!,
152		add_error(external_functions,'### Arithmetic operation not defined: ',X,SpanInfo).
153		add_exception_error2(error(evaluation_error(undefined),ERR),X,SpanInfo) :-
154		is_error(ERR),!,
155		add_error(external_functions,'### Arithmetic operation not defined: ',X,SpanInfo).
156		add_exception_error2(error(evaluation_error(zero_divisor),ERR),X,SpanInfo) :-
157		is_error(ERR),!,
158		% TO DO: use add_wd_error_set_result:
159		add_error(external_functions,'### Division by 0 in arithmetic operation: ',X,SpanInfo).
160		add_exception_error2(error(existence_error(source_sink,File),_),X,SpanInfo) :- !,
161		add_error(external_functions,'### File does not exist (calling external function): ',File:X,SpanInfo).
162		add_exception_error2(error(consistency_error(Msg,_,format_arguments),_),_X,SpanInfo) :- !,
163		add_error(external_functions,'### Illegal format string (see SICStus Prolog reference manual for syntax): ',Msg,SpanInfo).
164		add_exception_error2(enumeration_warning(A,B,C,D,E),X,SpanInfo) :-
165		Exception = enumeration_warning(A,B,C,D,E),!,
166		debug_println(20,Exception),
167		get_predicate_name(X,Pred),
168		add_warning(external_functions,'### Enumeration warning occured while calling external function: ',Pred,SpanInfo),
169		% or should we just print a message on the console ?
170		% or use
171		throw(Exception).
172		add_exception_error2(user_interrupt_signal,_X,_SpanInfo) :- !,
173		print('User Interrupt during external function evaluation'),nl,
174		throw(user_interrupt_signal).
175		add_exception_error2(Exception,X,SpanInfo) :-
176		debug_println(20,Exception),
177		add_error(external_functions,'### Exception occurred while calling external function: ',X:Exception,SpanInfo).
178
179		get_predicate_name(Var,P) :- var(Var),!,P='_VAR_'.
180		get_predicate_name(external_functions:C,P) :- !, get_predicate_name(C,P).
181		get_predicate_name(Module:C,Module:P) :- !, get_predicate_name(C,P).
182		get_predicate_name(Call,F/P) :- functor(Call,F,P).
183
184		is_error(evaluation_error('is'(_,_),2,_,_)).
185		is_error(domain_error('is'(_,_),2,_,_)).
186
187		% STANDARD EXTERNAL FUNCTIONS
188
189
190		% -------------------------------
191
192		% MATHEMATICAL FUNCTIONS
193
194		external_fun_type('COS',[],[integer,integer]).
195		:- public 'COS'/2.
196		:- block 'COS'(-,?). % redundant; we could add CLPFD constraints for R
197		'COS'(int(X),int(R)) :- cos2(100,X,R,unknown).
198		external_fun_type('COSx',[],[integer,integer,integer]).
199		expects_spaninfo('COSx').
200		:- public 'COSx'/4.
201		:- block 'COSx'(-,?,?,?),'COSx'(?,-,?,?).
202		'COSx'(int(PrecisionMultiplier),int(X),int(R),Span) :- cos2(PrecisionMultiplier,X,R,Span).
203		:- block cos2(-,?,?,?),cos2(?,-,?,?).
204		cos2(Multiplier,X,R,Span) :- safe_is('COSx',R,round(Multiplier*cos(X/Multiplier)),Span).
205
206		external_fun_type('SIN',[],[integer,integer]).
207		:- public 'SIN'/2.
208		:- block 'SIN'(-,?). % redundant; we could add CLPFD constraints for R
209		'SIN'(int(X),int(R)) :- sin2(100,X,R,unknown).
210		expects_spaninfo('SINx').
211		:- public 'SINx'/4.
212		:- block 'SINx'(-,?,?,?),'SINx'(?,-,?,?).
213		'SINx'(int(PrecisionMultiplier),int(X),int(R),Span) :- %print('SINx'(PrecisionMultiplier,X,R)),nl,
214		sin2(PrecisionMultiplier,X,R,Span).
215		:- block sin2(-,?,?,?),sin2(?,-,?,?).
216		sin2(Multiplier,X,R,Span) :- safe_is('SINx',R,round(Multiplier*sin(X/Multiplier)),Span).
217
218		external_fun_type('TAN',[],[integer,integer]).
219		:- public 'TAN'/2.
220		:- block 'TAN'(-,?). % redundant; we could add CLPFD constraints for R
221		'TAN'(int(X),int(R)) :- tan2(100,X,R,unknown).
222		external_fun_type('TANx',[],[integer,integer,integer]).
223		expects_spaninfo('TANx').
224		:- public 'TANx'/4.
225		:- block 'TANx'(-,?,?,?),'TANx'(?,-,?,?).
226		'TANx'(int(PrecisionMultiplier),int(X),int(R),Span) :- tan2(PrecisionMultiplier,X,R,Span).
227		:- block tan2(?,-,?,?),tan2(-,?,?,?).
228		tan2(Multiplier,X,R,Span) :- safe_is('TANx',R,round(Multiplier*tan(X/Multiplier)),Span).
229
230
231		external_fun_type('PROLOG_FUN',[],[string,integer,integer,integer]).
232		external_fun_has_wd_condition('PROLOG_FUN').
233		expects_spaninfo('PROLOG_FUN').
234		:- public 'PROLOG_FUN'/5.
235		'PROLOG_FUN'(string(Function),int(PrecisionMultiplier),int(Argument),int(Result),Span) :-
236		prolog_fun2(Function,PrecisionMultiplier,Argument,Result,Span).
237		% Function can be:
238		% sin, cos, tan, cot, sinh, cosh, tanh, asin, acos, atan, acot, asinh, acosh, atanh, acoth, sqrt, log, exp
239		:- block prolog_fun2(?,-,?,?,?),prolog_fun2(-,?,?,?,?), prolog_fun2(?,?,-,?,?).
240		prolog_fun2(Function,Multiplier,X,R,Span) :-
241		E =.. [Function,X/Multiplier],
242		safe_is(Function,R,round(Multiplier*E),Span).
243
244		external_fun_has_wd_condition('LOGx').
245		expects_spaninfo('LOGx').
246		:- public 'LOGx'/5.
247		:- block 'LOGx'(-,?,?,?,?),'LOGx'(?,-,?,?,?), 'LOGx'(?,?,-,?,?).
248		'LOGx'(int(PrecisionMultiplier),int(Base),int(X),int(R),Span) :-
249		log2(PrecisionMultiplier,Base,X,R,Span).
250		:- block log2(?,-,?,?,?),log2(-,?,?,?,?),log2(?,?,-,?,?).
251		log2(Multiplier,Base,X,R,Span) :-
252		safe_is('LOGx',R,round(Multiplier*log(Base/Multiplier,X/Multiplier)),Span).
253
254		external_fun_type('GCD',[],[integer,integer,integer]).
255		:- public 'GCD'/3.
256		:- block 'GCD'(-,?,?),'GCD'(?,-,?).
257		'GCD'(int(X),int(Y),int(R)) :- gcd2(X,Y,R).
258		:- block gcd2(?,-,?),gcd2(-,?,?).
259		% we could assert abs(X) #>= R, abs(Y) #>= R
260		gcd2(X,Y,R) :- R is gcd(X,Y).
261
262		external_fun_type('ABS',[],[integer,integer]).
263		:- public 'ABS'/2.
264		:- use_module(clpfd_interface,[clpfd_eq_expr/2]).
265		:- block 'ABS'(-,-). % do we need this ??
266		'ABS'(int(X),int(R)) :-
267		clpfd_eq_expr(R,abs(X)).
268
269
270		external_fun_type('MSB',[],[integer,integer]).
271		expects_spaninfo('MSB').
272		:- public 'MSB'/3.
273		:- block 'MSB'(-,?,?).
274		'MSB'(int(X),int(R),Span) :- msb2(X,R,Span). % most significant bit
275		:- block msb2(-,?,?).
276		msb2(X,R,Span) :- safe_is('MSB',R,msb(X),Span). % TO DO: could be made reversible by propagating constraint if R known
277
278		% BITWISE OPERATORS
279		external_fun_type('BNOT',[],[integer,integer]).
280		expects_spaninfo('BNOT').
281		:- public 'BNOT'/3.
282		:- block 'BNOT'(-,-,?).
283		'BNOT'(int(X),int(R),Span) :- bitwise_not(X,R,Span).
284		:- block bitwise_not(-,-,?).
285		bitwise_not(X,R,Span) :- number(X),!,safe_is('BNOT',R,\(X),Span).
286		bitwise_not(X,R,Span) :- safe_is('BNOT',X,\(R),Span).
287
288		external_fun_type('BAND',[],[integer,integer,integer]).
289		:- public 'BAND'/3.
290		:- block 'BAND'(-,?,?),'BAND'(?,-,?).
291		'BAND'(int(X),int(Y),int(R)) :- bitwise_and(X,Y,R).
292		:- block bitwise_and(?,-,?),bitwise_and(-,?,?).
293		bitwise_and(X,Y,R) :- R is X /\ Y. % we could do some early consistency checking, e.g., when X and R known
294
295		external_fun_type('BOR',[],[integer,integer,integer]).
296		:- public 'BOR'/3.
297		:- block 'BOR'(-,?,?),'BOR'(?,-,?).
298		'BOR'(int(X),int(Y),int(R)) :- bitwise_or(X,Y,R).
299		:- block bitwise_or(?,-,?),bitwise_or(-,?,?).
300		bitwise_or(X,Y,R) :- R is X \/ Y. % we could do some early consistency checking, e.g., when X and R known
301
302		external_fun_type('BXOR',[],[integer,integer,integer]).
303		:- public 'BXOR'/3.
304		:- block 'BXOR'(-,-,?),'BXOR'(?,-,-),'BXOR'(-,?,-).
305		'BXOR'(int(X),int(Y),int(R)) :- bitwise_xor(X,Y,R).
306		:- block bitwise_xor(-,-,?),bitwise_xor(?,-,-),bitwise_xor(-,?,-).
307		% DO WE NEED TO KNOW THE sizes of X,Y,R ?
308		bitwise_xor(X,Y,R) :- var(X),!, X is xor(R,Y).
309		bitwise_xor(X,Y,R) :- var(Y),!, Y is xor(X,R).
310		bitwise_xor(X,Y,R) :- R is xor(X,Y).
311
312		% TO DO: do some clpfd propagations ? X:0..N & Y:0..M -> BAND(X,Y) : 0..min(N,M)
313
314		% EXTERNAL_FUNCTION_BITS == INTEGER --> seq(INTEGER)
315		% BITS(x) == [0]
316		external_fun_type('BLSHIFT',[],[integer,integer,integer]).
317		:- public 'BLSHIFT'/3.
318		:- block 'BLSHIFT'(-,?,?),'BLSHIFT'(?,-,?).
319		'BLSHIFT'(int(X),int(Y),int(R)) :- bitwise_left_shift(X,Y,R).
320		:- block bitwise_left_shift(?,-,?),bitwise_left_shift(-,?,?).
321		bitwise_left_shift(X,Y,R) :- R is X << Y.
322		external_fun_type('BRSHIFT',[],[integer,integer,integer]).
323		:- public 'BRSHIFT'/3.
324		:- block 'BRSHIFT'(-,?,?),'BRSHIFT'(?,-,?).
325		'BRSHIFT'(int(X),int(Y),int(R)) :- bitwise_right_shift(X,Y,R).
326		:- block bitwise_right_shift(?,-,?),bitwise_right_shift(-,?,?).
327		bitwise_right_shift(X,Y,R) :- R is X >> Y.
328
329		:- assert_must_succeed(( external_functions:call_external_function('BITS',[12],[int(12)],R,integer,unknown,_WF),
330		equal_object(R,[(int(1),int(1)),(int(2),int(1)),(int(3),int(0)),(int(4),int(0))]) )).
331
332		external_fun_type('BITS',[],[integer,seq(integer)]).
333		:- public 'BITS'/2.
334		:- block 'BITS'(-,?).
335		'BITS'(int(X),Res) :- convert_to_bits(X,Res).
336
337		:- block convert_to_bits(-,?).
338		convert_to_bits(0,Res) :- !, convert_set_to_seq([int(0)],Res).
339		convert_to_bits(N,Res) :- convert_to_bits(N,[],List),
340		convert_set_to_seq(List,Res).
341		convert_to_bits(0,Acc,Res) :- !, Res=Acc.
342		convert_to_bits(X,Acc,Res) :- XM2 is X mod 2, XD2 is X // 2,
343		convert_to_bits(XD2,[int(XM2)|Acc],Res).
344		% TO DO: maybe do some constraint propagation from Result to number, or use CLP(FD) size info to infer size of sequence?
345
346		% -------------------------------
347
348		% THE CHOOSE operator (for TLA, recursive functions over sets,...)
349		% or choice operator from Abrial Book, page 60ff
350
351		:- use_module(custom_explicit_sets).
352		:- use_module(kernel_waitflags,[add_wd_error_span/4]).
353		external_fun_type('CHOOSE',[X],[set(X),X]).
354		external_fun_has_wd_condition('CHOOSE').
355		expects_waitflag('CHOOSE').
356		expects_spaninfo('CHOOSE').
357		:- public 'CHOOSE'/4.
358		:- block 'CHOOSE'(-,?,?,?).
359		'CHOOSE'([],_,Span,WF) :-
360		add_wd_error_span('CHOOSE applied to empty set: ',[],Span,WF).
361		'CHOOSE'(CS,H,_,_) :- is_interval_closure_or_integerset(CS,Low,Up),
362		!,
363		choose_interval(Low,Up,H).
364		'CHOOSE'([H|T],C,Span,WF) :- !,
365		when(ground([H|T]),
366		(convert_to_avl([H|T],AVL) -> 'CHOOSE'(AVL,C,Span,WF)
367		; add_wd_error_span('Cannot determine minimum element for CHOOSE: ',[H|T],Span,WF),
368		kernel_objects:equal_object(C,H))
369		).
370		'CHOOSE'(avl_set(A),H,_,_) :- !, avl_min(A,Min),kernel_objects:equal_object(H,Min).
371		'CHOOSE'(global_set(GS),H,_,_) :- !, H = fd(1,GS). % assume GS not empty, integer sets covered above
372		'CHOOSE'(freetype(ID),H,Span,WF) :- !,
373		(kernel_freetypes:enumerate_freetype(basic,FV,freetype(ID))
374		-> kernel_objects:equal_object(FV,H)
375		; add_internal_error('Could not generate freetype element: ','CHOOSE'(freetype(ID),H,Span,WF))).
376		'CHOOSE'(CS,H,Span,WF) :- custom_explicit_sets:is_cartesian_product_closure(CS,Set1,Set2),!,
377		'CHOOSE'(Set1,H1,Span,WF),
378		'CHOOSE'(Set2,H2,Span,WF),
379		kernel_objects:equal_object(H,(H1,H2)).
380		'CHOOSE'(closure(P,T,B),H,Span,WF) :-
381		custom_explicit_sets:expand_custom_set(closure(P,T,B),ER),
382		'CHOOSE'(ER,H,Span,WF).
383
384		:- block choose_interval(-,?,?).
385		choose_interval(Low,_Up,H) :- number(Low),!,H=int(Low).
386		choose_interval(_Low,Up,H) :- choose_interval2(Up,H). % lower-bound is minus infinity
387		:- block choose_interval2(-,?).
388		choose_interval2(Up,H) :- number(Up),!,H=int(Up). % for those intervals we choose Up
389		choose_interval2(_,int(0)). % we have INTEGER or something equivalent; simply choose 0
390
391		:- use_module(kernel_objects,[singleton_set_element/4]).
392		external_fun_type('MU',[X],[set(X),X]).
393		external_fun_has_wd_condition('MU').
394		expects_waitflag('MU').
395		expects_spaninfo('MU').
396		:- public 'MU'/4.
397		'MU'(Set,Res,Span,WF) :-
398		singleton_set_element(Set,Res,Span,WF).
399		% -----------------
400
401		% sort a set and generate a sequence
402		external_fun_has_wd_condition('SORT').
403		expects_waitflag('SORT').
404		expects_spaninfo('SORT').
405		external_fun_type('SORT',[X],[set(X),seq(X)]).
406		:- public 'SORT'/4.
407		:- block 'SORT'(-,?,?,?).
408		'SORT'([],Res,_Span,_WF) :- !, Res=[].
409		'SORT'(CS,Res,_,WF) :- custom_explicit_sets:is_custom_explicit_set(CS),!,
410		custom_explicit_sets:expand_custom_set_to_list_wf(CS,ER,Done,'SORT',WF),
411		sort_aux(Done,ER,Res,WF).
412		'SORT'([H|T],Res,_,WF) :-
413		when(ground([H|T]),
414		(maplist(convert_to_avl_if_possible,[H|T],List),
415		sort(List,SList),sort_aux(done,SList,Res,WF))).
416
417		convert_to_avl_if_possible(H,Res) :- convert_to_avl(H,CH),!,Res=CH.
418		convert_to_avl_if_possible(H,H) :-
419		add_warning(external_functions,'Cannot guarantee order when sorting:',H).
420
421		:- block sort_aux(-,?,?,?).
422		sort_aux(_,ER,Res,_WF) :- convert_set_to_seq(ER,Res).
423
424		% construct a B sequence
425		convert_set_to_seq(ER,Res) :- convert_set_to_seq(ER,1,Seq), equal_object_optimized(Seq,Res).
426
427		convert_set_to_seq([],_,[]).
428		convert_set_to_seq([H|T],N,[(int(N),H)|CT]) :- N1 is N+1, convert_set_to_seq(T,N1,CT).
429
430		% :- use_module(library(samsort),[samsort/3]).
431		% TO DO: version of SORT with samsort/3 and user provided sorting predicate
432
433		% Z Compaction / squash operator to fill up gaps in sequence
434		external_fun_has_wd_condition('SQUASH').
435		expects_waitflag('SQUASH').
436		external_fun_type('SQUASH',[X],[set(couple(integer,X)),seq(X)]). % input not necessarily proper sequence
437
438		:- use_module(kernel_z,[compaction/3]).
439		:- public 'SQUASH'/3.
440		'SQUASH'(Sequence,Value,WF) :- compaction(Sequence,Value,WF).
441
442		% Prolog term order on encoding
443		external_fun_type('LESS',[X],[X,X,boolean]).
444		:- public 'LESS'/3.
445		:- block 'LESS'(-,?,?), 'LESS'(?,-,?).
446		'LESS'(string(A),string(B),Res) :- !, less2(A,B,Res).
447		'LESS'(int(A),int(B),Res) :- !, less_clpfd(A,B,Res). % use CLPFD less ?
448		'LESS'(fd(A,G),fd(B,G),Res) :- !, less_clpfd(A,B,Res).
449		'LESS'(pred_false,B,Res) :- !, B=Res. % if B=pred_true then < , otherwise not
450		'LESS'(pred_true,_,Res) :- !, Res=pred_false.
451		% TO DO: expand finite closures, couples, avl_sets, ...
452		'LESS'(X,Y,Res) :- when((ground(X),ground(Y)), less2(X,Y,Res)).
453		% TO DO: use kernel_ordering,[ordered_value/2]).
454
455		:- use_module(clpfd_interface,[clpfd_leq_expr/2,clpfd_lt_expr/2]).
456		:- block less_clpfd(-,?,-), less_clpfd(?,-,-).
457		less_clpfd(A,B,Res) :- Res==pred_true, !, clpfd_lt_expr(A,B).
458		less_clpfd(A,B,Res) :- Res==pred_false, !, clpfd_leq_expr(B,A).
459		less_clpfd(A,B,Res) :- (A < B -> Res=pred_true ; Res=pred_false).
460
461
462		:- block less2(-,?,?), less2(?,-,?).
463		less2(A,B,Res) :- (A @< B -> Res=pred_true ; Res=pred_false).
464
465		:- use_module(kernel_ordering,[leq_ordered_value/3]).
466
467		external_fun_type('LEQ_SYM_BREAK',[X],[X,X,boolean]).
468		:- public 'LEQ_SYM_BREAK'/3.
469		:- block 'LEQ_SYM_BREAK'(-,?,?), 'LEQ_SYM_BREAK'(?,-,?).
470		% true if arg1 <= arg2 according to Prolog term order; may return true for some symbolic representations
471		%'LEQ_SYM_BREAK'(X,Y,Res) :- print('LEQ_SYM_BREAK'(X,Y,Res)),nl,fail.
472		'LEQ_SYM_BREAK'(string(A),string(B),Res) :- !, less_eq2(A,B,Res).
473		'LEQ_SYM_BREAK'(int(A),int(B),Res) :- !, less_eq2(A,B,Res). % use CLPFD less ?
474		'LEQ_SYM_BREAK'(fd(A,G),fd(B,G),Res) :- !, less_eq2(A,B,Res). % use CLPFD less
475		'LEQ_SYM_BREAK'(pred_false,B,Res) :- !, less_eq2(pred_false,B,Res).
476		'LEQ_SYM_BREAK'(pred_true,B,Res) :- !, less_eq2(pred_true,B,Res).
477		% TO DO: expand finite closures, couples, avl_sets, ...
478		'LEQ_SYM_BREAK'(closure(_,_,_),_,Res) :- !, Res=pred_true. % otherwise we would have to expand it
479		'LEQ_SYM_BREAK'(_,closure(_,_,_),Res) :- !, Res=pred_true.
480		'LEQ_SYM_BREAK'((A,B),(X,Y),Res) :- Res==pred_true,!, leq_ordered_value((A,B),(X,Y),_Equal).
481		'LEQ_SYM_BREAK'(rec(FA),rec(FB),Res) :- Res==pred_true,!, leq_ordered_value(rec(FA),rec(FB),_Equal).
482		'LEQ_SYM_BREAK'(X,Y,Res) :- when((ground(X),ground(Y)), less_eq2(X,Y,Res)). % unsafe to use; we should normalize AVLs ...
483		% TO DO: use kernel_ordering:leq_ordered_value/2 more or use lex_chain([[X,X],[Y,Z]],[op(#=<)]) for pairs/records of FD values
484		% Note: it is reified in b_interpreter_check
485
486
487
488		:- block less_eq2(-,?,?), less_eq2(?,-,?).
489		less_eq2(A,B,Res) :- (A @=< B -> Res=pred_true ; Res=pred_false).
490
491		% -------------------------------
492
493		% a first prototype for implementing recursive functions
494		% still a bit clumsy to define recursive functions (using STRING parameter for names)
495		% a restriction is that we can only have one version per machine, i.e.
496		% one can only define recursive function in the CONSTANTS section and only
497		% in a deterministic fashion not depending on enumerated constants,...
498		% also: we still need to ensure that the recurisve closures are not expanded
499		% this should probably go hand in hand with the symbolic pragma
500
501		reset_external_functions :-
502		retractall(last_walltime(_)),
503		reset_profiler, % maybe we should do this only if profiler was used ?
504		reset_ident,
505		reset_kodkod,
506		close_all_files.
507
508		:- use_module(eventhandling,[register_event_listener/3]).
509		:- register_event_listener(clear_specification,reset_external_functions,
510		'Reset B External Functions.').
511
512		%:- dynamic recursive_function/2.
513		%expects_waitflag('REC'). % DEPRECATED
514		%expects_spaninfo('RECx'). % DEPRECATED
515		%expects_spaninfo('REC_LET'). % DEPRECATED
516
517
518		% -------------------------------
519
520		expects_waitflag('FORCE').
521		:- public 'FORCE'/3.
522		% example usage halve = FORCE( %x.(x:0..1000 & x mod 2 = 0 | x/2))
523		:- block 'FORCE'(-,?,?).
524		%'FORCE'(A,B,_) :- print(force(A)),nl,fail.
525		'FORCE'(avl_set(A),Result,_) :- !, equal_object(avl_set(A),Result).
526		'FORCE'([],Result,_) :- !, equal_object([],Result).
527		'FORCE'(closure(P,T,B),Result,WF) :- !,
528		(debug:debug_mode(on) -> print('FORCING : '),translate:print_bvalue(closure(P,T,B)),nl ; true),
529		custom_explicit_sets:expand_closure_to_avl_or_list(P,T,B,ExpandedValue,no_check,WF),
530		(debug:debug_mode(on) -> print('RESULT : '),translate:print_bvalue(ExpandedValue),nl,
531		print(' ASSIGNING TO : '), translate:print_bvalue(Result),nl
532		; true),
533		equal_object(ExpandedValue,Result).
534		'FORCE'((A,B),(FA,FB),WF) :- !,'FORCE'(A,FA,WF), 'FORCE'(B,FB,WF).
535		% TO DO: treat lists and records ...
536		'FORCE'(A,B,_) :- equal_object_optimized(A,B,'FORCE').
537
538
539		% force enumeration of certain basic datatypes; at the moment this is quite limited : TO DO: extend
540		% maybe we also want to add priorities or several variables in one go (several variables can be sent as a pair though)
541		expects_waitflag('ENUMERATE').
542		:- public 'ENUMERATE'/3.
543		% example usage: x:1..2 & y:200..300 & x = y mod 3 & ENUMERATE(y)
544		%:- block 'ENUMERATE'(-,?,?).
545		'ENUMERATE'(Obj,pred_true,WF) :-
546		get_wait_flag(1.1,WF,WF1), % ensures that wait_flag1 phase done, e.g., setting up intervals
547		enumerate_aux(Obj,WF1,WF).
548
549		:- block enumerate_aux(?,-,?).
550		%enumerate_aux(X,_,_WF) :- translate_bvalue(X,OS), format('*** ENUMERATE: ~w --> ~w ~n',[X,OS]),fail.
551		enumerate_aux(X,_,WF) :- kernel_waitflags:find_waitflag_info(WF,Info,Prio,LWF), % linear in size of waitflag store !
552		var(LWF), Info == element_of_avl(X),
553		!,
554		debug_println(9,found_element_of_avl_trigger(Prio,X)),
555		LWF = Prio.
556		enumerate_aux(X,_,WF) :- var(X), !, frozen(X,G), %trace, print(frozen(X,G)),nl,
557		trigger_enumerators(G,X,Triggered),
558		(Triggered == true -> true ; add_message('ENUMERATE','Could not trigger ENUMERATE: ',X), enumerate_aux(X,X,WF)).
559		enumerate_aux(fd(X,GS),_,WF) :- !, kernel_objects:enumerate_basic_type_wf(fd(X,GS),global(GS),WF).
560		enumerate_aux(int(X),_,WF) :- !,
561		kernel_objects:enumerate_basic_type_wf(int(X),integer,WF).
562		enumerate_aux((A,B),WF1,WF) :- !, % should we look for a element_of_avl(X) waitflag in WF store ?
563		enumerate_aux(A,WF1,WF), enumerate_aux(B,WF1,WF).
564		enumerate_aux(rec(Fields),WF1,WF) :- !, % ditto
565		maplist(enumerate_field(WF1,WF),Fields).
566		enumerate_aux(Obj,_,_WF) :- %kernel_waitflags:portray_waitflags(_WF),trace,
567		add_error(external_functions,'Cannot ENUMERATE value yet: ',Obj).
568
569		trigger_enumerators((A,B),V,Triggered) :- !, trigger_enumerators(A,V,Triggered), trigger_enumerators(B,V,Triggered).
570		trigger_enumerators(custom_explicit_sets:element_of_avl_set_wf3(Var,_,ApproxSize,WF1,_),V,Triggered) :-
571		Var==V, var(WF1), !, print(trigger(Var,ApproxSize)),nl,WF1=float(ApproxSize), Triggered=true.
572		% TO DO: detect other enumerators (safe_avl_member,...)
573		trigger_enumerators(_,_,_).
574
575		enumerate_field(WF1,WF,field(_,Val)) :- enumerate_aux(Val,WF1,WF).
576
577		% a predicate to ensure that certain variables are enumerated together:
578		% as soon as first value is known, the second value gets enumerated
579		expects_waitflag('LINKED_ENUMERATION').
580		:- public 'LINKED_ENUMERATION'/4.
581		:- block 'LINKED_ENUMERATION'(-,?,?,?).
582		'LINKED_ENUMERATION'(Obj1,Obj2,pred_true,WF) :- link_enum_aux(Obj1,Obj2,WF).
583
584		link_enum_aux(fd(X,_),Obj2,WF) :- !, link_enum_block(X,Obj2,WF).
585		link_enum_aux(int(X),Obj2,WF) :- !, link_enum_block(X,Obj2,WF).
586		link_enum_aux(string(X),Obj2,WF) :- !, link_enum_block(X,Obj2,WF).
587		link_enum_aux(Obj1,Obj2,WF) :- when(ground(Obj1),link_enum_block(1,Obj2,WF)).
588
589		:- block link_enum_block(-,?,?).
590		link_enum_block(_X,Obj2,WF) :- %print(linked_enumeration(_X,Obj2)), tools_printing:print_arg(Obj2),nl,
591		get_wait_flag1(WF,WF1), % give chance to run deterministic propagations
592		enumerate_aux(Obj2,WF1,WF).
593
594		expects_unevaluated_args('DO_NOT_ENUMERATE').
595		:- public 'DO_NOT_ENUMERATE'/3.
596		:- block 'DO_NOT_ENUMERATE'(-,?,?).
597		'DO_NOT_ENUMERATE'((A,B),PredRes,UEA) :- !, 'DO_NOT_ENUMERATE'(A,PredRes,UEA),'DO_NOT_ENUMERATE'(B,PredRes,UEA).
598		'DO_NOT_ENUMERATE'(fd(V,_),PredRes,UEA) :- !, 'DO_NOT_ENUMERATE'(V,PredRes,UEA).
599		'DO_NOT_ENUMERATE'(int(V),PredRes,UEA) :- !, 'DO_NOT_ENUMERATE'(V,PredRes,UEA).
600		'DO_NOT_ENUMERATE'(string(V),PredRes,UEA) :- !, 'DO_NOT_ENUMERATE'(V,PredRes,UEA).
601		'DO_NOT_ENUMERATE'(_Obj,PredRes,_UEA) :-
602		%print('INSTANTIATED: '),nl, _UEA=[UnEvalArg],translate:print_bexpr(UnEvalArg),nl, print(_Obj),nl,
603		PredRes=pred_true.
604		% add_message('DO_NOT_ENUMERATE','Enumerating: ',UnEvalArgs).
605
606		% a utility to avoid propagation of values, can be used as "enumeration barrier"
607		expects_waitflag('COPY').
608		:- public 'COPY'/3.
609		:- block 'COPY'(-,?,?).
610		'COPY'(Val,Result,WF) :- ground_value_check(Val,GrVal),
611		when(nonvar(GrVal),equal_object_optimized_wf(Val,Result,'COPY',WF)).
612
613
614		% -------------------------------
615
616		:- assert_must_succeed(( external_functions:call_external_function('STRING_APPEND',[a,b],[string(a),string(b)],string(ab),string,unknown,_WF) )).
617		% STRING MANIPULATION FUNCTIONS
618
619		:- use_module(kernel_strings,[string_append_wf/4, string_chars/2, string_codes/2, string_length/2]).
620
621		% function to append two strings, reversible
622		external_fun_can_be_inverted('STRING_APPEND').
623		expects_waitflag('STRING_APPEND').
624		external_fun_type('STRING_APPEND',[],[string,string,string]).
625		:- public 'STRING_APPEND'/4.
626		'STRING_APPEND'(A,B,C,WF) :- string_append_wf(A,B,C,WF).
627
628		expects_waitflag('STRING_CONC').
629		external_fun_type('STRING_CONC',[],[seq(string),string]).
630		:- public 'STRING_CONC'/3.
631		:- block 'STRING_CONC'(-,?,?).
632		'STRING_CONC'(List,Res,WF) :-
633		convert_seq_to_sorted_list(List,SortedList),
634		string_conc_aux(SortedList,1,Res,WF).
635
636		:- block string_conc_aux(-,?,?,?).
637		string_conc_aux([],_,string(''),_WF).
638		string_conc_aux([(int(Idx),H)|T],Idx,Res,WF) :-
639		(T==[] -> Res=H % values are strings; no need to call equal_object
640		; Idx1 is Idx+1,
641		string_conc_aux(T,Idx1,TRes,WF),
642		string_append_wf(H,TRes,Res,WF)).
643
644		% ensure indexes of B sequence are sorted correctly (TO DO: no need to call when we have constructed list from avl_set)
645		convert_seq_to_sorted_list(List,SortedList) :-
646		custom_explicit_sets:expand_custom_set_to_list(List,ESet,_,string_conc),
647		convert_list_to_sorted_list(ESet,[],SortedList).
648
649		:- block convert_list_to_sorted_list(-,?,?).
650		convert_list_to_sorted_list([],Acc,Res) :- sort(Acc,Res).
651		convert_list_to_sorted_list([(int(Idx),El)|T],Acc,Res) :-
652		convert_list_to_sorted_list2(Idx,T,[(int(Idx),El)|Acc],Res).
653
654		:- block convert_list_to_sorted_list2(-,?,?,?).
655		convert_list_to_sorted_list2(_,List,Acc,Res) :- convert_list_to_sorted_list(List,Acc,Res).
656
657		external_fun_can_be_inverted('STRING_CHARS').
658		external_fun_type('STRING_CHARS',[],[string,seq(string)]).
659		:- public 'STRING_CHARS'/2.
660		% to do: make it reversible
661		'STRING_CHARS'(Str,SeqRes) :- string_chars(Str,SeqRes).
662
663		external_fun_can_be_inverted('CODES_TO_STRING').
664		external_fun_type('CODES_TO_STRING',[],[seq(integer),string]).
665		:- public 'CODES_TO_STRING'/2.
666		'CODES_TO_STRING'(A,SeqRes) :- 'STRING_CODES'(SeqRes,A).
667
668		external_fun_can_be_inverted('STRING_CODES').
669		external_fun_type('STRING_CODES',[],[string,seq(integer)]).
670		:- public 'STRING_CODES'/2.
671		'STRING_CODES'(A,SeqRes) :- string_codes(A,SeqRes).
672
673		:- assert_must_succeed(( external_functions:call_external_function('STRING_LENGTH',[a],[string(a)],int(1),integer,unknown,_WF) )).
674		% function to get length of a string
675		external_fun_type('STRING_LENGTH',[],[string,integer]).
676		:- public 'STRING_LENGTH'/2.
677		'STRING_LENGTH'(S,L) :- string_length(S,L).
678
679		:- use_module(kernel_strings,[string_split_wf/4, string_join_wf/5]).
680
681		% function to split a string into a list of strings which were delimited by a separator
682		% WARNING: if the seperator is of length more than one, then first match-strategy will be used
683		external_fun_can_be_inverted('STRING_SPLIT').
684		expects_waitflag('STRING_SPLIT').
685		:- public 'STRING_SPLIT'/4.
686		'STRING_SPLIT'(Str,Sep,Strings,WF) :- string_split_wf(Str,Sep,Strings,WF).
687
688		:- public 'STRING_JOIN'/5.
689		expects_waitflag('STRING_JOIN').
690		expects_spaninfo('STRING_JOIN').
691		'STRING_JOIN'(SplitAtoms,Sep,Res,Span,WF) :- string_join_wf(SplitAtoms,Sep,Res,Span,WF).
692
693
694		expects_waitflag('STRING_CONTAINS_STRING').
695		external_fun_type('STRING_CONTAINS_STRING',[],[string,string,boolean]).
696		% TRUE when arg2 occurs as contiguous substring in arg1
697		:- public 'STRING_CONTAINS_STRING'/4.
698		:- block 'STRING_CONTAINS_STRING'(-,?,?,?), 'STRING_CONTAINS_STRING'(?,-,?,?).
699		'STRING_CONTAINS_STRING'(string(A),string(B),PredRes,_WF) :-
700		string_contains_string_aux(A,B,PredRes).
701		:- use_module(library(lists),[sublist/5]).
702		% TO DO: we could enumerate B if A known and waitflag instantiated
703		:- block string_contains_string_aux(-,?,?),string_contains_string_aux(?,-,?).
704		string_contains_string_aux(A,B,PredRes) :-
705		atom_codes(A,ACodes),
706		atom_codes(B,BCodes),
707		(sublist(ACodes,BCodes,_,_,_) -> PredRes=pred_true ; PredRes=pred_false).
708
709		:- use_module(kernel_strings,[substring_wf/6]).
710		:- public 'SUB_STRING'/6.
711		expects_spaninfo('SUB_STRING').
712		expects_waitflag('SUB_STRING').
713		external_fun_type('SUB_STRING',[],[string,integer,integer,string]).
714		'SUB_STRING'(S,From,Len,Res,Span,WF) :- substring_wf(S,From,Len,Res,Span,WF).
715
716
717		external_fun_has_wd_condition('TYPED_STRING_TO_ENUM').
718		expects_waitflag('TYPED_STRING_TO_ENUM').
719		expects_spaninfo('TYPED_STRING_TO_ENUM').
720		:- public 'TYPED_STRING_TO_ENUM'/5.
721		:- block 'TYPED_STRING_TO_ENUM'(?,-,-,?,?),'TYPED_STRING_TO_ENUM'(-,?,?,?,?).
722		'TYPED_STRING_TO_ENUM'(Type,string(S),Res,Span,WF) :-
723		string_to_enum2(S,fd(Nr,GS)),
724		check_type(Type,S,Nr,GS,Res,Span,WF).
725
726		:- block check_type(-,?,?, ?,?,?,?), check_type(?,-,?, ?,?,?,?), check_type(?,?,-, ?,?,?,?).
727		check_type(GSTypeExpr,S,Nr,GS,Res,Span,WF) :- get_global_set_value_type(GSTypeExpr,ExpectedGS),
728		ExpectedGS=GS,
729		!,
730		membership_test_wf(GSTypeExpr,fd(Nr,GS),MemTest,WF),
731		check_value(MemTest,Nr,GS,Res,S,GSTypeExpr,Span,WF).
732		check_type(GSTypeExpr,S,_,GS,_,Span,WF) :-
733		get_global_set_value_type(GSTypeExpr,ExpectedGS),
734		tools:ajoin(['String value ',S,' is of type ',GS,' and not of expected type:'],Msg),
735		add_wd_error_span(Msg,ExpectedGS,Span,WF).
736
737		:- block check_value(-,?,?,?,?,?,?,?).
738		check_value(pred_true,Nr,GS,Res,_,_,_,_) :- !, Res=fd(Nr,GS).
739		check_value(pred_false,_,_GS,_,S,GSTypeExpr,Span,WF) :-
740		tools:ajoin(['String value ',S,' is of correct type but not in set:'],Msg),
741		translate:translate_bvalue(GSTypeExpr,SetStr),
742		add_wd_error_span(Msg,SetStr,Span,WF).
743
744		% get type of a set of enumerated/deferred set elements
745		get_global_set_value_type(global_set(GS),Res) :- !, Res=GS.
746		get_global_set_value_type([fd(_,GS)|_],Res) :- !, Res=GS.
747		get_global_set_value_type(avl_set(node(fd(_,GS),_True,_,_,_)),Res) :- !, Res=GS.
748		get_global_set_value_type(A,_) :-
749		add_error('TYPED_STRING_TO_ENUM','First argument not a SET:',A),fail.
750
751		external_fun_can_be_inverted('STRING_TO_ENUM').
752		external_fun_has_wd_condition('STRING_TO_ENUM').
753		:- public 'STRING_TO_ENUM'/2.
754		:- block 'STRING_TO_ENUM'(-,-).
755		'STRING_TO_ENUM'(string(S),FD) :- string_to_enum2(S,FD).
756
757		:- block string_to_enum2(-,-).
758		string_to_enum2(S,Res) :- nonvar(S),!,
759		(b_global_sets:lookup_global_constant(S,FD) ->
760		Res=FD % fd(Nr,GS)
761		; % TO DO: use add_wd_error_set_result
762		add_error('Could not convert string to enumerated set element: ',S),fail).
763		string_to_enum2(S,fd(Nr,GS)) :-
764		string_to_enum3(S,Nr,GS).
765
766		:- block string_to_enum3(-,-,?),string_to_enum3(-,?,-).
767		string_to_enum3(S,Nr,GS) :- nonvar(S),!,
768		(b_global_sets:lookup_global_constant(S,fd(SNr,SGS)) -> (SGS,SNr) = (GS,Nr)
769		; add_error('Could not convert string to enumerated set element: ',S),fail).
770		string_to_enum3(S,Nr,GS) :-
771		(b_global_sets:is_b_global_constant(GS,Nr,GNS) -> GNS=S
772		; add_error('Could not convert deferred set element to string: ',GS:Nr),fail).
773
774		:- use_module(kernel_strings,[string_is_int/2]).
775		:- public 'STRING_IS_INT'/2.
776		'STRING_IS_INT'(S,Res) :- string_is_int(S,Res).
777
778		% A Utility to convert Decimal Strings to Integers
779		% TO DO: make a more precise version using just integers: currently DEC_STRING_TO_INT("1024.235",2) = 102423 !
780		external_fun_has_wd_condition('DEC_STRING_TO_INT').
781		expects_spaninfo('DEC_STRING_TO_INT').
782		expects_waitflag('DEC_STRING_TO_INT').
783
784		:- assert_must_succeed((atom_codes(A,"1024"),
785		external_functions:'DEC_STRING_TO_INT'(string(A),int(0),int(1024),unknown,no_wf_available))).
786		:- assert_must_succeed((atom_codes(A,"1024.1"),
787		external_functions:'DEC_STRING_TO_INT'(string(A),int(1),int(10241),unknown,no_wf_available))).
788		:- public 'DEC_STRING_TO_INT'/5.
789		:- block 'DEC_STRING_TO_INT'(-,?,?,?,?),'DEC_STRING_TO_INT'(?,-,?,?,?).
790		'DEC_STRING_TO_INT'(string(S),int(Precision),int(Res),Span,WF) :-
791		dec_str_to_int(S,Precision,Res,Span,WF).
792
793		:- use_module(tools,[split_chars/3]).
794		:- block dec_str_to_int(-,?,?,?,?),dec_str_to_int(?,-,?,?,?).
795		dec_str_to_int(S,Precision,Res,Span,WF) :-
796		atom_codes(S,Codes),
797		split_chars(Codes,".",[Left|T]),
798		(T=[] -> Right="", dec_str_to_int2(Left,Right,Precision,Res,Span,WF)
799		; T = [Right] -> dec_str_to_int2(Left,Right,Precision,Res,Span,WF)
800		; %add_error(external_functions,'Expecting integer or decimal number:',S,Span),fail
801		add_wd_error_span('String contains multiple dots, expecting integer or decimal number for DEC_STRING_TO_INT:',S,Span,WF)
802		).
803
804
805		get_sign([45|T],-1,Res) :- !,strip_ws(T,Res).
806		get_sign([32|T],PosNeg,Res) :- !, get_sign(T,PosNeg,Res).
807		get_sign(L,1,L).
808		strip_ws([32|T],R) :- !, strip_ws(T,R).
809		strip_ws(R,R).
810
811		rounding([H|_]) :- member(H,"56789").
812
813		is_zero(48). % code of 0
814		is_digit(Code) :- Code >= 48, Code =< 57.
815		check_digits(Codes,_,_,Res) :- maplist(is_digit,Codes),!,Res=ok.
816		check_digits(Codes,Span,WF,ko) :-
817		append([39|Codes],[39],C2), atom_codes(A,C2), % generate atom with quotes
818		%add_error(external_functions,'Illegal number: ',A,Span),fail.
819		add_wd_error_span('String contains illegal characters, expecting integer or decimal number for DEC_STRING_TO_INT:',A,Span,WF).
820
821		dec_safe_number_codes(Number,[],_,_) :- !, Number=0.
822		dec_safe_number_codes(Number,Codes,Span,WF) :-
823		(safe_number_codes(Nr,Codes) -> Number=Nr
824		; append([39|Codes],[39],C2), atom_codes(A,C2),
825		%add_error(external_functions,'Cannot convert to number: ',A,Span),fail
826		add_wd_error_span('Cannot convert string to number for DEC_STRING_TO_INT:',A,Span,WF),
827		Number='$WDERROR$'
828		).
829
830		dec_str_to_int2(Left,Right,Precision,Res,Span,WF) :-
831		maplist(is_zero,Right), Precision >= 0,
832		!,
833		dec_safe_number_codes(LeftNumber,Left,Span,WF),
834		(LeftNumber=='$WDERROR$' -> true
835		; safe_is('DEC_STRING_TO_INT',Res,LeftNumber*(10^Precision),Span)).
836		dec_str_to_int2(Left,Right,Precision,Res,Span,WF) :- get_sign(Left,Sign,NewLeft),
837		check_digits(NewLeft,Span,WF,Res1), check_digits(Right,Span,WF,Res2),
838		(Res1==ok,Res2==ok
839		-> shift(Precision,NewLeft,Right,ResL,ResR),
840		dec_safe_number_codes(LeftInteger,ResL,Span,WF),
841		(rounding(ResR)
842		-> Res is Sign*(LeftInteger+1)
843		; Res is Sign*LeftInteger)
844		; true).
845
846		:- use_module(library(lists),[append_length/4]).
847		% shift decimal values left or right depending on precision argument
848		shift(0,Left,Right,Left,Right) :- !.
849		shift(Pos,Left,Right,ResL,ResR) :- Pos>0,!,
850		append(Left,Left2,ResL),
851		length(Right,RLen),
852		(RLen >= Pos -> append_length(Left2,ResR,Right,Pos) % take first Pos elements from R and shift left of .
853		; append(Right,Zeros,Left2), % take all of Right and add Zeros
854		ResR = [],
855		NrZeros is Pos - RLen,
856		length(Zeros,NrZeros), maplist(is_zero,Zeros)
857		).
858		shift(Pos,Left,Right,ResL,ResR) :- % Pos < 0
859		length(Left,LLen), PPos is -Pos,
860		(LLen >= PPos
861		-> Shift is LLen-PPos, append_length(ResL,L2,Left,Shift), append(L2,Right,ResR)
862		; %Result always 0.0...
863		NrZeros is PPos - LLen,length(Zeros,NrZeros), maplist(is_zero,Zeros),
864		ResL = "0",
865		append(Zeros,LR,ResR),
866		append(Left,Right,LR)).
867
868
869		:- use_module(kernel_strings,[string_to_int_wf/4]).
870		external_fun_has_wd_condition('STRING_TO_INT').
871		expects_waitflag('STRING_TO_INT').
872		expects_spaninfo('STRING_TO_INT').
873		:- public 'STRING_TO_INT'/4.
874		:- block 'STRING_TO_INT'(-,-,?,?).
875		'STRING_TO_INT'(S,I,Span,WF) :- string_to_int_wf(S,I,Span,WF).
876
877
878		:- use_module(kernel_strings,[int_to_string/2]).
879		external_fun_type('INT_TO_STRING',[],[integer,string]).
880		:- public 'INT_TO_STRING'/2.
881		'INT_TO_STRING'(I,S) :- int_to_string(I,S).
882
883		:- use_module(kernel_strings,[int_to_dec_string/3]).
884		external_fun_type('INT_TO_DEC_STRING',[],[integer,integer,string]).
885		:- public 'INT_TO_DEC_STRING'/3.
886		'INT_TO_DEC_STRING'(I,Precision,S) :- int_to_dec_string(I,Precision,S).
887
888
889		:- use_module(kernel_strings,[to_string/2,format_to_string/3]).
890		external_fun_type('TO_STRING',[X],[X,string]).
891		:- public 'TO_STRING'/2.
892		'TO_STRING'(Value,S) :- to_string(Value,S).
893
894		external_fun_type('FORMAT_TO_STRING',[X],[string,seq(X),string]).
895		:- public 'FORMAT_TO_STRING'/3.
896		'FORMAT_TO_STRING'(FormatString,ListOfStrings,Res) :- format_to_string(FormatString,ListOfStrings,Res).
897
898
899		external_fun_type('STRINGIFY',[X],[X,string]).
900		expects_unevaluated_args('STRINGIFY').
901		:- public 'PRETTY_PRINT_TO_STRING'/3.
902		:- public 'STRINGIFY'/3.
903		% pretty print a formula to string, the value is not used (but will currently be evaluated !)
904		% TO DO: should we enforce a certain mode? (ascii, unicode, ...)
905
906		'PRETTY_PRINT_TO_STRING'(V,R,A) :- 'STRINGIFY'(V,R,A). % old name
907		'STRINGIFY'(_Value,Res,[AST]) :-
908		translate:translate_bexpression(AST,S),
909		Res = string(S).
910
911		external_fun_type('HASH',[X],[X,integer]).
912		:- public 'HASH'/2.
913		:- block 'HASH'(-,?).
914		'HASH'(Value,Int) :-
915		% TO DO: use ground_value_check
916		when(ground(Value),(term_hash(Value,H),Int=int(H))).
917
918
919		% -------------------------------
920		% REGULAR EXPRESSION FUNCTIONS
921		% Using ECMAScript syntax: http://www.cplusplus.com/reference/regex/ECMAScript/
922
923		:- use_module(extension('regexp/regexp'),
924		[regexp_match/2, is_regexp/1, regexp_replace/4,
925		regexp_search_first/3, regexp_search_first_detailed/4]).
926		:- public 'REGEX_MATCH'/3.
927		:- block 'REGEX_MATCH'(-,?,?), 'REGEX_MATCH'(?,-,?).
928		'REGEX_MATCH'(string(String),string(Pattern),Res) :- block_regex_match(String,Pattern,Res).
929		:- block block_regex_match(-,?,?), block_regex_match(?,-,?).
930		block_regex_match(String,Pattern,Res) :-
931		(regexp_match(String,Pattern) -> Res=pred_true ; Res=pred_false).
932
933		:- public 'IS_REGEX'/2.
934		:- block 'IS_REGEX'(-,?).
935		'IS_REGEX'(string(Pattern),Res) :- block_is_regexp(Pattern,Res).
936		:- block block_is_regexp(-,?).
937		block_is_regexp(Pattern,Res) :-
938		(is_regexp(Pattern) -> Res=pred_true ; Res=pred_false).
939
940		:- public 'REGEX_REPLACE'/4.
941		:- block 'REGEX_REPLACE'(-,?,?,?), 'REGEX_REPLACE'(?,-,?,?), 'REGEX_REPLACE'(?,?,-,?).
942		'REGEX_REPLACE'(string(String),string(Pattern),string(ReplString),Res) :-
943		block_regex_replace(String,Pattern,ReplString,Res).
944		:- block block_regex_replace(-,?,?,?), block_regex_replace(?,-,?,?), block_regex_replace(?,?,-,?).
945		block_regex_replace(String,Pattern,ReplString,Result) :-
946		regexp_replace(String,Pattern,ReplString,Res), Result=string(Res).
947
948
949		:- public 'REGEX_SEARCH_STR'/3.
950		:- block 'REGEX_SEARCH_STR'(-,?,?), 'REGEX_SEARCH_STR'(?,-,?).
951		'REGEX_SEARCH_STR'(string(String),string(Pattern),Res) :- block_regex_search_first(String,Pattern,Res).
952		:- block block_regex_search_first(-,?,?), block_regex_search_first(?,-,?).
953		block_regex_search_first(String,Pattern,Result) :-
954		regexp_search_first(String,Pattern,Res), Result=string(Res).
955
956		:- public 'REGEX_SEARCH'/4.
957		:- block 'REGEX_SEARCH'(-,?,?,?), 'REGEX_SEARCH'(?,-,?,?), 'REGEX_SEARCH'(?,?,-,?).
958		'REGEX_SEARCH'(string(String),int(From),string(Pattern),Res) :-
959		block_regex_search_first_detailed(String,From,Pattern,Res).
960		:- block block_regex_search_first_detailed(-,?,?,?),
961		block_regex_search_first_detailed(?,-,?,?), block_regex_search_first_detailed(?,?,-,?).
962		block_regex_search_first_detailed(String,FromIndex,Pattern,Result) :-
963		regexp_search_first_detailed(String,FromIndex,Pattern,Res),
964		construct_match_result(Res,Result).
965
966		construct_match_result(match(Pos,Len,[Str|SubMatches]),Res) :- !,
967		BPos is Pos+1,
968		maplist(mkstring,SubMatches,SubMatchesStr),
969		convert_set_to_seq(SubMatchesStr,SubList),
970		Res = rec([field(length,int(Len)), field(position,int(BPos)),
971		field(string,string(Str)), field(submatches,SubList)]).
972		construct_match_result('no-match',Res) :- !,
973		Res = rec([field(length,int(-1)), field(position,int(-1)), field(string,string('')), field(submatches,[])]).
974
975		mkstring(A,string(A)).
976
977		:- use_module(extension('regexp/regexp'), [regexp_search_all/3]).
978		:- public 'REGEX_SEARCH_ALL'/3.
979		:- block 'REGEX_SEARCH_ALL'(-,?,?), 'REGEX_SEARCH_ALL'(?,-,?).
980		'REGEX_SEARCH_ALL'(string(String),string(Pattern),Res) :- block_regex_search_all(String,Pattern,Res).
981		:- block block_regex_search_all(-,?,?), block_regex_search_all(?,-,?).
982		block_regex_search_all(String,Pattern,Result) :-
983		regexp_search_all(String,Pattern,Matches),
984		maplist(mkstring,Matches,MatchesStr),
985		convert_set_to_seq(MatchesStr,Result).
986		% -------------------------------
987
988		external_fun_type('SHA_HASH',[X],[X,set(couple(integer,integer))]).
989		expects_waitflag('SHA_HASH').
990		:- use_module(extension('probhash/probhash'),[raw_sha_hash/2]).
991		:- use_module(store,[normalise_value_for_var/3]).
992		:- public 'SHA_HASH'/3.
993		:- block 'SHA_HASH'(-,?,?).
994		'SHA_HASH'(Value,Res,WF) :-
995		normalise_value_for_var('SHA_HASH',Value,NValue),
996		ground_value_check(NValue,Gr),
997		sha_hash(NValue,Gr,Res,WF).
998		:- block sha_hash(?,-,?,?).
999		sha_hash(Value,_,Res,WF) :-
1000		raw_sha_hash(Value,List),
1001		convert_to_int_seq(List,1,Seq),
1002		equal_object_optimized_wf(Seq,Res,'SHA_HASH',WF).
1003
1004		convert_to_int_seq([],_,[]).
1005		convert_to_int_seq([H|T],N,[(int(N),int(H))|CT]) :- N1 is N+1, convert_to_int_seq(T,N1,CT).
1006
1007		external_fun_type('SHA_HASH_HEX',[X],[X,string]).
1008		:- public 'SHA_HASH_HEX'/2.
1009		:- block 'SHA_HASH_HEX'(-,?).
1010		'SHA_HASH_HEX'(Value,Res) :-
1011		normalise_value_for_var('SHA_HASH_HEX',Value,NValue),
1012		ground_value_check(NValue,Gr),
1013		sha_hash_string(NValue,Gr,Res).
1014		:- block sha_hash_string(?,-,?).
1015		sha_hash_string(Value,_,Res) :-
1016		sha_hash_as_hex_codes(Value,SHAHexCodes), atom_codes(Atom,SHAHexCodes),
1017		Res = string(Atom).
1018
1019		% -------------------------------
1020
1021		% STRING FILE SYSTEM FUNCTIONS
1022
1023
1024		:- use_module(kernel_objects).
1025		:- use_module(library(file_systems)).
1026		:- public 'FILES'/2.
1027		:- block 'FILES'(-,?).
1028		'FILES'(string(A),L) :- files2(A,L).
1029		:- block files2(-,?).
1030		files2(Dir,List) :- b_absolute_file_name(Dir,ADir),
1031		findall(string(F),file_member_of_directory(ADir,F,_FLong),L),
1032		equal_object_optimized(L,List,files2).
1033		:- public 'FULL_FILES'/2.
1034		:- block 'FULL_FILES'(-,?).
1035		'FULL_FILES'(string(A),L) :- full_files2(A,L).
1036		:- block full_files2(-,?).
1037		full_files2(Dir,List) :-
1038		b_absolute_file_name(Dir,ADir),
1039		findall(string(FLong),file_member_of_directory(ADir,_F,FLong),L),
1040		equal_object_optimized(L,List,full_files2).
1041
1042
1043		:- public 'DIRECTORIES'/2.
1044		:- block 'DIRECTORIES'(-,?).
1045		'DIRECTORIES'(string(A),L) :- dir2(A,L).
1046		:- block dir2(-,?).
1047		dir2(Dir,List) :- b_absolute_file_name(Dir,ADir),
1048		findall(string(F),directory_member_of_directory(ADir,F,_FLong),L),
1049		equal_object_optimized(L,List,dir2).
1050		:- public 'FULL_DIRECTORIES'/2.
1051		:- block 'FULL_DIRECTORIES'(-,?).
1052		'FULL_DIRECTORIES'(string(A),L) :- full_dir2(A,L).
1053		:- block full_dir2(-,?).
1054		full_dir2(Dir,List) :- b_absolute_file_name(Dir,ADir),
1055		findall(string(FLong),directory_member_of_directory(ADir,_,FLong),L),
1056		equal_object_optimized(L,List,full_dir2).
1057
1058		:- public 'FILE_EXISTS'/2.
1059		:- block 'FILE_EXISTS'(-,?).
1060		'FILE_EXISTS'(string(A),PREDRES) :- file_exists2(A,PREDRES).
1061		:- block file_exists2(-,?).
1062		file_exists2(A,PREDRES) :- b_absolute_file_name(A,AA),
1063		(file_exists(AA) -> PREDRES=pred_true ; PREDRES=pred_false).
1064		:- public 'DIRECTORY_EXISTS'/2.
1065		:- block 'DIRECTORY_EXISTS'(-,?).
1066		'DIRECTORY_EXISTS'(string(A),PREDRES) :- dir_exists2(A,PREDRES).
1067		:- block dir_exists2(-,?).
1068		dir_exists2(A,PREDRES) :- b_absolute_file_name(A,AA),
1069		(directory_exists(AA) -> PREDRES=pred_true ; PREDRES=pred_false).
1070
1071		% a variant of the predicate b_absolute_file_name_relative_to_main_machine in bmachine using safe_call:
1072		b_absolute_file_name(File,AbsFileName) :- b_absolute_file_name(File,AbsFileName,unknown).
1073		b_absolute_file_name(File,AbsFileName,Span) :-
1074		bmachine:b_get_main_filename(MainFileName),
1075		safe_call(
1076		absolute_file_name(File,AbsFileName,[relative_to(MainFileName)]),
1077		Span).
1078
1079		:- public 'FILE_PROPERTY'/3.
1080		:- block 'FILE_PROPERTY'(-,?,?), 'FILE_PROPERTY'(?,-,?).
1081		'FILE_PROPERTY'(string(A),string(P),BoolRes) :-
1082		file_property2(A,P,BoolRes).
1083		:- block file_property2(-,?,?), file_property2(?,-,?).
1084		file_property2(File,Prop,BoolRes) :-
1085		b_absolute_file_name(File,AFile),
1086		file_property(AFile,Prop) -> BoolRes=pred_true ; BoolRes=pred_false.
1087		% possible properties: readable, writable, executable
1088
1089		:- public 'FILE_PROPERTY_VALUE'/3.
1090		:- block 'FILE_PROPERTY_VALUE'(-,?,?), 'FILE_PROPERTY_VALUE'(?,-,?).
1091		'FILE_PROPERTY_VALUE'(string(A),string(P),int(R)) :-
1092		file_property_val2(A,P,R).
1093		:- block file_property_val2(-,?,?), file_property_val2(?,-,?).
1094		file_property_val2(File,Prop,Res) :-
1095		b_absolute_file_name(File,AFile),
1096		file_property(AFile,Prop,Val) -> Res=Val
1097		; add_error(external_functions,'Illegal FILE_PROPERTY',Prop),Res=int(-1).
1098		% possible properties:
1099		% size_in_bytes, create_timestamp, modify_timestamp, access_timestamp
1100		% + on unix the follwing is also an integer: owner_user_id, owner_group_id
1101
1102		:- public 'DIRECTORY_PROPERTY'/3.
1103		:- block 'DIRECTORY_PROPERTY'(-,?,?), 'DIRECTORY_PROPERTY'(?,-,?).
1104		'DIRECTORY_PROPERTY'(string(A),string(P),BoolRes) :-
1105		dir_property2(A,P,BoolRes).
1106		:- block dir_property2(-,?,?), dir_property2(?,-,?).
1107		dir_property2(File,Prop,BoolRes) :-
1108		b_absolute_file_name(File,AFile),
1109		directory_property(AFile,Prop) -> BoolRes=pred_true ; BoolRes=pred_false.
1110
1111		:- public 'DIRECTORY_PROPERTY_VALUE'/3.
1112		:- block 'DIRECTORY_PROPERTY_VALUE'(-,?,?), 'DIRECTORY_PROPERTY_VALUE'(?,-,?).
1113		'DIRECTORY_PROPERTY_VALUE'(string(A),string(P),int(R)) :-
1114		dir_property_val2(A,P,R).
1115		:- block dir_property_val2(-,?,?), dir_property_val2(?,-,?).
1116		dir_property_val2(File,Prop,Res) :-
1117		b_absolute_file_name(File,AFile),
1118		directory_property(AFile,Prop,Val) -> Res=Val
1119		; add_error(external_functions,'Illegal DIRECTORY_PROPERTY',Prop), Res=int(-1).
1120		% --------------------------------
1121
1122		% I/O
1123
1124
1125		% printf as predicate; can also be used as a function to BOOL
1126		expects_spaninfo('fprintf').
1127		external_pred_always_true('fprintf').
1128		:- public fprintf/5.
1129		:- block fprintf(-,?,?,?,?), fprintf(?,-,?,?,?), fprintf(?,?,-,?,?).
1130		fprintf(string(File),string(FormatString),Value,PredRes,Span) :- !, PredRes = pred_true,
1131		when((ground(FormatString),ground(Value)),
1132		fprintf2(File,FormatString,Value,Span)).
1133		fprintf(File,F,V,P,S) :- add_internal_error('Illegal call: ',fprintf(File,F,V,P,S)), P=pred_true.
1134
1135		expects_spaninfo('printf_opt_trace').
1136		external_pred_always_true('printf_opt_trace').
1137		:- public printf_opt_trace/5.
1138		:- block printf_opt_trace(-,?,?,?,?), printf_opt_trace(?,-,?,?,?).
1139		printf_opt_trace(string(FormatString),Value,Trace,PredRes,Span) :- !, PredRes = pred_true,
1140		when((ground(FormatString),ground(Value)),
1141		(fprintf2(user_output,FormatString,Value,Span),
1142		(Trace==pred_true -> trace ; true)
1143		)
1144		).
1145		printf_opt_trace(F,V,T,P,S) :- add_internal_error('Illegal call: ',printf_opt_trace(F,V,T,P,S)), P=pred_true.
1146
1147
1148		expects_spaninfo('printf').
1149		external_pred_always_true('printf').
1150		:- assert_must_succeed(external_functions:printf(string('test ok = ~w~n'),[(int(1),pred_true)],pred_true,unknown)).
1151		:- block printf(-,?,?,?), printf(?,-,?,?).
1152		printf(string(FormatString),Value,PredRes,Span) :- !, PredRes = pred_true,
1153		when((ground(FormatString),ground(Value)),
1154		fprintf2(user_output,FormatString,Value,Span)).
1155		printf(F,V,P,S) :- add_internal_error('Illegal call: ',printf(F,V,P,S)), P=pred_true.
1156
1157		expects_spaninfo('printf_two'). % print two values, triggers as soon as first value is known
1158		external_pred_always_true('printf_two').
1159		:- assert_must_succeed(external_functions:printf_two(string('test ok = ~w~n'),[(int(1),pred_true)],string('test ok = ~w~n'),[(int(1),pred_true)],pred_true,unknown)).
1160		:- public printf_two/6.
1161		:- block printf_two(-,?,?,?,?,?), printf_two(?,-,?,?,?,?).
1162		printf_two(string(FormatString),Value,string(FormatString2),Value2,PredRes,Span) :- !, PredRes = pred_true,
1163		when((ground(FormatString),ground(Value)),
1164		(fprintf2(user_output,FormatString,Value,Span),
1165		fprintf2(user_output,FormatString2,Value2,Span))).
1166		printf_two(F,V,F2,V2,P,S) :- add_internal_error('Illegal call: ',printf_two(F,V,F2,V2,P,S)), P=pred_true.
1167
1168
1169		expects_spaninfo('printf_nonvar'). % print as soon as value becomes nonvar (printf waits until the value is ground)
1170		external_pred_always_true('printf_nonvar').
1171		:- public printf_nonvar/4.
1172		:- block printf_nonvar(-,?,?,?), printf_nonvar(?,-,?,?).
1173		printf_nonvar(string(FormatString),Value,PredRes,Span) :- !, PredRes = pred_true,
1174		when((ground(FormatString),nonvar(Value)),
1175		fprintf2(user_output,FormatString,Value,Span)).
1176		printf_nonvar(F,V,P,S) :- add_internal_error('Illegal call: ',printf(F,V,P,S)), P=pred_true.
1177
1178
1179		expects_spaninfo('dprintf'). % a version of printf which delays setting itself to TRUE until printing is performed
1180		external_pred_always_true('dprintf').
1181		:- public dprintf/4.
1182		:- block dprintf(-,?,?,?), dprintf(?,-,?,?).
1183		dprintf(string(FormatString),Value,PredRes,Span) :- !,
1184		when((ground(FormatString),ground(Value)),
1185		(fprintf2(user_output,FormatString,Value,Span),PredRes = pred_true)).
1186		dprintf(F,V,P,S) :- add_internal_error('Illegal call: ',dprintf(F,V,P,S)), P=pred_true.
1187
1188		:- use_module(kernel_strings,[convert_b_sequence_to_list_of_atoms/3]).
1189		fprintf2(File,FormatString,Value,Span) :-
1190		convert_b_sequence_to_list_of_atoms(Value,ListOfAtoms,Done),
1191		when(nonvar(Done),
1192		(file_format(File,FormatString,ListOfAtoms,Span),
1193		print_hash((FormatString,Value)),
1194		print_stats,
1195		fprint_log_info(File,Span)
1196		)).
1197		%fprintf2(File,FormatString,Value,Span) :- print('BACKTRACKING ') , file_format(File,FormatString,['?'],Span),nl,fail.
1198		% warning: format can call an argument as goal with ~@; this is dangerous
1199		% and we should prohibit this
1200		% Luckily PRINTF("@: <>~@<>~n","print(danger)") where print(danger)
1201		% is arbitrary code is not a security exploit:
1202		% our PRINTF translates the argument to an atom, i.e., one could
1203		% only call Prolog predicates without arguments, anything else leads to an exception
1204		% (even PRINTF("@: <>~@<>~n","nl") leads to an exception)
1205
1206
1207		:- use_module(hashing,[my_term_hash/2]).
1208		% optionally print hash and allow breakpoints
1209		print_hash(V) :-
1210		external_fun_pref(printf_hash,'TRUE'), % use SET_PREF("printf_hash","TRUE")
1211		!,
1212		my_term_hash(V,H), format('% HASH = ~w~n',H),
1213		%((H = 158201315 ; H=29759067) -> trace ; true),
1214		true.
1215		print_hash(_).
1216
1217
1218		:- dynamic nr_of_printfs/1.
1219		nr_of_printfs(0).
1220		print_stats :-
1221		external_fun_pref(printf_stats,PFS), % use SET_PREF("printf_stats","TRUE")
1222		PFS='TRUE',
1223		retract(nr_of_printfs(N)),
1224		!,
1225		N1 is N+1,
1226		assert(nr_of_printfs(N1)),
1227		statistics(walltime,[X,SL]),
1228		statistics(memory_used,M), MB is M / 1048576,
1229		statistics(gc_count,GCs),
1230		format('% Call ~w at walltime ~w ms (since last ~w ms), memory ~3f MB (~w GCs)~n',[N1,X,SL,MB,GCs]).
1231		print_stats.
1232
1233		:- dynamic external_fun_pref/2.
1234		% valid keys: log_info
1235		valid_external_fun_pref(log_info).
1236		valid_external_fun_pref(printf_stats).
1237		valid_external_fun_pref(printf_hash).
1238
1239		fprint_log_info(File,Span) :- external_fun_pref(log_info,X),
1240		'GET_INFO'(string(X),string(Res)),
1241		file_format(File,'%%% ~w~n',[Res],Span).
1242		fprint_log_info(_,_).
1243
1244		% example usage SET_PREF("log_info","time")
1245		external_fun_type('SET_PREF',[],[string,string,boolean]).
1246		:- public 'SET_PREF'/3.
1247		:- block 'SET_PREF'(-,?,?), 'SET_PREF'(?,-,?).
1248		'SET_PREF'(string(S),string(Val),R) :-
1249		preferences:eclipse_preference(S,Pref),!, R=pred_true,
1250		format('Setting ProB preference ~w := ~w~n',[S,Val]),
1251		preferences:set_preference(Pref,Val).
1252		'SET_PREF'(string(S),string(Val),R) :- valid_external_fun_pref(S),!,
1253		R=pred_true,
1254		retractall(external_fun_pref(S,_)),
1255		format('Setting external function preference ~w := ~w~n',[S,Val]),
1256		assert(external_fun_pref(S,Val)).
1257		'SET_PREF'(P,V,R) :-
1258		add_internal_error('Illegal call: ','SET_PREF'(P,V,R)), R=pred_false.
1259
1260		external_fun_type('GET_PREF',[],[string,string]).
1261		expects_waitflag('GET_PREF').
1262		expects_spaninfo('GET_PREF').
1263		:- assert_must_succeed(external_functions:'GET_PREF'(string('CLPFD'),string(_),unknown,_)).
1264		:- public 'GET_PREF'/4.
1265		'GET_PREF'(Str,Res,Span,WF) :-
1266		kernel_waitflags:get_wait_flag(10,'GET_PREF',WF,WF10), % will enumerate possible input strings
1267		get_pref2(Str,Res,_,WF10,Span).
1268		external_fun_type('GET_PREF_DEFAULT',[],[string,string]).
1269		expects_waitflag('GET_PREF_DEFAULT').
1270		expects_spaninfo('GET_PREF_DEFAULT').
1271		:- assert_must_succeed(external_functions:'GET_PREF_DEFAULT'(string('CLPFD'),string(true),unknown,_)).
1272		:- public 'GET_PREF_DEFAULT'/4.
1273		'GET_PREF_DEFAULT'(Str,Res,Span,WF) :-
1274		(nonvar(Str) -> true
1275		; kernel_waitflags:get_wait_flag(10,'GET_PREF',WF,WF10)), % will enumerate possible input strings
1276		get_pref2(Str,_,Res,WF10,Span).
1277
1278		:- block get_pref2(-,?,?,-,?).
1279		get_pref2(string(S),Res,Res2,_,Span) :-
1280		if((preferences:eclipse_preference(S,Pref),
1281		preferences:get_preference(Pref,Val),
1282		preferences:preference_default_value(Pref,DefVal)),
1283		(make_string(Val,Res),make_string(DefVal,Res2)),
1284		(add_error(external_functions,'Illegal argument for GET_PREF: ',S,Span),
1285		fail)).
1286
1287
1288		% printf followed by fail; useful for print fail loops in the REPL
1289		expects_spaninfo('printfail').
1290		:- assert_must_fail(external_functions:printfail(string('test ok = ~w~n'),[(int(1),pred_true)],pred_true,unknown)).
1291		:- block printfail(-,?,?,?), printfail(?,-,?,?).
1292		printfail(string(FormatString),Value,PredRes,Span) :- !, PredRes = pred_true,
1293		when((ground(FormatString),ground(Value)),
1294		(fprintf2(user_output,FormatString,Value,Span),fail)).
1295		printfail(F,V,P,S) :-
1296		add_internal_error('Illegal call: ',printfail(F,V,P,S)), P=pred_true.
1297
1298		% a version of printf with automatic indenting and backtracking feedback
1299		expects_spaninfo('iprintf').
1300		external_pred_always_true('iprintf').
1301		:- assert_must_succeed(external_functions:iprintf(string('test ok = ~w~n'),[(int(1),pred_true)],pred_true,unknown)).
1302		:- block iprintf(-,?,?,?), iprintf(?,-,?,?).
1303		iprintf(string(FormatString),Value,PredRes,Span) :- !, PredRes = pred_true,
1304		when((ground(FormatString),ground(Value)),
1305		ifprintf2(user_output,FormatString,Value,no_trace,Span)).
1306		iprintf(F,V,P,S) :- add_internal_error('Illegal call: ',iprintf(F,V,P,S)), P=pred_true.
1307		ifprintf2(File,FormatString,Value,Trace,Span) :-
1308		my_term_hash((FormatString,Value),Hash),
1309		format(user_output,'[hash ~w] ',[Hash]), % (Hash=1087266573122589201 -> (trace ; trace,fail) ; true),
1310		translate:translate_bvalue(Value,TV),
1311		indent_format(File,FormatString,[TV],Trace),
1312		fprint_log_info(File,Span).
1313		expects_spaninfo('itprintf').
1314		external_pred_always_true('itprintf').
1315		:- public itprintf/4.
1316		:- block itprintf(-,?,?,?), itprintf(?,-,?,?).
1317		itprintf(string(FormatString),Value,PredRes,Span) :- PredRes = pred_true,
1318		when((ground(FormatString),ground(Value)),
1319		ifprintf2(user_output,FormatString,Value,trace,Span)).
1320
1321
1322		:- public observe/5.
1323		expects_spaninfo('observe').
1324		expects_unevaluated_args('observe').
1325		expects_waitflag('observe').
1326		external_pred_always_true('observe').
1327		% observe pairs of values
1328		observe(Value,PredRes,UnEvalArgs,Span,WF) :-
1329		observe2(Value,PredRes,UnEvalArgs,no_trace,Span,WF).
1330
1331		:- public tobserve/5.
1332		expects_spaninfo('tobserve'). % observe but with tracing enabled
1333		expects_unevaluated_args('tobserve').
1334		expects_waitflag('tobserve').
1335		external_pred_always_true('tobserve').
1336		tobserve(Value,PredRes,UnEvalArgs,Span,WF) :-
1337		observe2(Value,PredRes,UnEvalArgs,trace,Span,WF).
1338
1339		observe2(Value,PredRes,[Arg],Trace,Span,WF) :- PredRes=pred_true,
1340		%kernel_waitflags:portray_waitflags(WF),
1341		kernel_waitflags:get_wait_flag0(WF,WF0),
1342		kernel_waitflags:get_wait_flag1(WF,WF1),
1343		when(nonvar(WF0),(indent_format(user_output,'WAITFLAG 0 set~n',[],no_trace),kernel_waitflags:portray_waitflags(WF))),
1344		when(nonvar(WF1),(indent_format(user_output,'WAITFLAG 1 set~n',[],no_trace),kernel_waitflags:portray_waitflags(WF))),
1345		Hook = print_value_as_table_if_possible(Arg,Value),
1346		observe_aux(Value,Arg,1,_,Trace,Span,Hook),
1347		iprintf(string("observe full value complete: ~w~n~n"),Value,_,Span).
1348
1349		:- use_module(table_tools,[print_value_as_table/2]).
1350		:- public print_value_as_table_if_possible/2. % used as hook above
1351		%print_value_as_table_if_possible(_,_) :- !.
1352		print_value_as_table_if_possible(Arg,Value) :-
1353		translate:print_bexpr(Arg),nl,
1354		(table_tools:print_value_as_table(Arg,Value) -> true ; true).
1355
1356		observe_aux((V1,V2),b(couple(A1,A2),_,_),Nr,R,Trace,Span,Hook) :- !,
1357		observe_aux(V1,A1,Nr,N1,Trace,Span,Hook),
1358		observe_aux(V2,A2,N1,R,Trace,Span,Hook).
1359		observe_aux(V,Arg,Nr,R,Trace,Span,Hook) :- R is Nr+1,
1360		translate:translate_bexpression(Arg,ArgString), %print(obs(Nr,ArgString)),nl,
1361		atom_codes(ArgString,ArgCodes),
1362		observe_value(V,ArgCodes,Nr,Trace,Span,Hook).
1363
1364		% entry for other modules:
1365		observe_value(Value,Info) :- (Info=[_|_] -> PCodes = Info ; atom_codes(Info,PCodes)),
1366		observe_value(Value,PCodes,1,no_trace,unknown,true).
1367
1368		observe_value(Value,ArgCodes,Nr,Trace,Span,Hook) :- %print(obs(Nr,ArgString)),nl,
1369		number_codes(Nr,NrCodes), append(NrCodes,") = ~w~n",Tail1), append(" (",Tail1,Tail2),
1370		append(ArgCodes,Tail2,FormatString),
1371		observe_set(Value,ArgCodes,1,Trace,Span,Value,Hook),
1372		when((ground(FormatString),ground(Value)),ifprintf2(user_output,FormatString,Value,Trace,Span)).
1373		observe_value_with_full_value(Value,ArgCodes,Nr,Trace,Span,FullValue,Hook) :- %print(obs(Nr,ArgString)),nl,
1374		number_codes(Nr,NrCodes), append(NrCodes,"):FULL = ~w~n",Tail1), append(" (",Tail1,Tail2),
1375		append(ArgCodes,Tail2,FormatString),
1376		observe_set(Value,ArgCodes,1,Trace,Span,Value,Hook),
1377		when((ground(FormatString),ground(Value)),
1378		observe_ground(FormatString,Value,FullValue,Trace,Span,Hook)).
1379
1380		observe_ground(FormatString,Value,FullValue,Trace,Span,Hook) :-
1381		ifprintf2(user_output,FormatString,rec([field(value,Value),field(full,FullValue)]),Trace,Span),
1382		(call(Hook) -> true ; print(hook_failed(Hook)),nl).
1383
1384
1385
1386		% observe sets and records:
1387		:- block observe_set(-,?,?,?,?,?,?).
1388		observe_set([],_ArgCodes,_,_Trace,_Span,_,_) :- !.
1389		observe_set([Value|T],ArgCodes,Pos,Trace,Span,FullValue,Hook) :- !, %print(obs(Value,Pos)),nl,
1390		append(ArgCodes," el -> ",ArgN),
1391		observe_value_with_full_value(Value,ArgN,Pos,Trace,Span,FullValue,Hook),
1392		%tools_files:put_codes(ArgN,user_output),print(Pos),print(' = '),tools_printing:print_arg(Value),nl,
1393		P1 is Pos+1, observe_set(T,ArgCodes,P1,Trace,Span,FullValue,Hook).
1394		observe_set((V1,V2),ArgCodes,Pos,Trace,Span,FullValue,Hook) :-
1395		preferences:preference(observe_precise_values,true),
1396		!, %print(obs(Value,Pos)),nl,
1397		append(ArgCodes," prj1 -> ",ArgN1),
1398		observe_value_with_full_value(V1,ArgN1,Pos,Trace,Span,FullValue,Hook),
1399		%tools_files:put_codes(ArgN,user_output),print(Pos),print(' = '),tools_printing:print_arg(Value),nl,
1400		Pos2 is Pos+1,
1401		append(ArgCodes," prj2 -> ",ArgN2),
1402		observe_value_with_full_value(V2,ArgN2,Pos2,Trace,Span,FullValue,Hook).
1403		observe_set(rec(Fields),ArgCodes,Pos,Trace,Span,_FullValue,Hook) :-
1404		preferences:preference(observe_precise_values,true),
1405		!,
1406		append(ArgCodes," rec -> ",ArgN),
1407		observe_field(Fields,ArgN,Pos,Trace,Span,Hook).
1408		observe_set(_,_,_,_,_,_,_).
1409
1410		:- block observe_field(-,?,?,?,?,?).
1411		observe_field([],ArgN,Pos,Trace,Span,_Hook) :-
1412		append(ArgN," complete (~w)~n",FormatString),
1413		ifprintf2(user_output,FormatString,Pos,Trace,Span).
1414		observe_field([field(Name,Value)|TFields],ArgN,Pos,Trace,Span,Hook) :-
1415		observe_value((string(Name),Value),ArgN,Pos,Trace,Span,Hook),
1416		observe_field(TFields,ArgN,Pos,Trace,Span,Hook).
1417
1418		:- use_module(bsyntaxtree,[get_texpr_id/2]).
1419		:- use_module(store,[lookup_value_with_span/5]).
1420		% utility function for other modules to use observe on parameters
1421		observe_parameters(Parameters,LocalState) :-
1422		skel(LocalState,SetupDone),
1423		reset_ident, reset_walltime,
1424		when(nonvar(SetupDone),observe_parameters_aux(Parameters,1,LocalState)).
1425		:- block skel(-,?).
1426		skel([],pred_true).
1427		skel([_|T],Done) :- skel(T,Done).
1428		:- block observe_parameters_aux(-,?,?), observe_parameters_aux(?,?,-).
1429		observe_parameters_aux([],_,_).
1430		observe_parameters_aux([TID|T],Nr,LS) :-
1431		safe_get_texpr_id(TID,ID), atom_codes(ID,PCodes),
1432		store:lookup_value_with_span(ID,[],LS,Value,TID),
1433		debug_println(9,observing(ID,Value,LS)),
1434		Hook = print_value_as_table_if_possible(TID,Value),
1435		observe_value(Value,PCodes,Nr,no_trace,unknown,Hook),
1436		N1 is Nr+1,
1437		observe_parameters_aux(T,N1,LS).
1438		safe_get_texpr_id(TID,ID) :- (atom(TID) -> ID=TID ; get_texpr_id(TID,ID)).
1439
1440		% utility to observe a state using the observe external function
1441		observe_state(State) :-
1442		reset_ident, reset_walltime,
1443		observe_state_aux(State,1).
1444		:- block observe_state_aux(-,?).
1445		observe_state_aux(no_state,_) :- !.
1446		observe_state_aux([],_) :- !.
1447		observe_state_aux(concrete_constants(C),Nr) :- !, observe_state_aux(C,Nr).
1448		observe_state_aux([bind(Id,Value)|T],Nr) :-
1449		atom_codes(Id,PCodes), !,
1450		%print(observe(Id,Value,Nr,T)),nl,
1451		observe_value(Value,PCodes,Nr,no_trace,unknown,true),
1452		N1 is Nr+1,
1453		observe_state_aux(T,N1).
1454		observe_state_aux(State,Nr) :- add_internal_error('Illegal state: ',observe_state_aux(State,Nr)).
1455
1456
1457		external_fun_type('observe_fun',[X],[X,boolean]).
1458		expects_unevaluated_args('observe_fun').
1459		external_pred_always_true('observe_fun').
1460		:- public observe_fun/3.
1461		% a specific predicate to observe enumeration of functions,...
1462		:- block observe_fun(-,-,?).
1463		observe_fun(Value,PredRes,[UnEvalArg]) :-
1464		translate:translate_bexpression(UnEvalArg,Str), format('Observe function : ~w~n',[Str]),
1465		obs_fun(Value,Str,Value),PredRes=pred_true.
1466
1467		:- block obs_fun(-,?,?).
1468		obs_fun([],_,_) :- !.
1469		obs_fun([(A,B)|T],Str,FullVal) :- !,
1470		obs_idx(A,B,Str,FullVal),
1471		obs_fun(T,Str,FullVal).
1472		obs_fun(V,Str,_) :- print(uncovered_obs_fun(V,Str)),nl.
1473
1474		:- block obs_idx(-,?,?,?), obs_idx(?,-,?,?).
1475		obs_idx(A,B,Str,FullVal) :-
1476		when(ground((A,B)),obs_idx_complete(FullVal,A,B,Str)).
1477
1478		obs_idx_complete(FullVal,A,B,Str) :-
1479		format('~n ~w = ',[Str]),obs_idx_complete_aux(FullVal,A,B).
1480		obs_idx_complete(FullVal,A,B,Str) :-
1481		format('~n [BACKTRACK] ~w = ',[Str]),obs_idx_complete_aux(FullVal,A,B),fail.
1482
1483		obs_idx_complete_aux(V,_,_) :- var(V),!,print(' OPEN '),nl.
1484		obs_idx_complete_aux([],_,_) :- !, nl.
1485		obs_idx_complete_aux([(X,Y)|T],A,B) :- !,
1486		((X,Y)==(A,B) -> print(' * ') ; print(' ')), print_bvalue((X,Y)),
1487		obs_idx_complete_aux(T,A,B).
1488		obs_idx_complete_aux(_,_,_) :- print(unknown),nl.
1489
1490
1491		% -----------------------------
1492
1493		:- public tprintf/4.
1494		expects_spaninfo('tprintf').
1495		external_pred_always_true('tprintf').
1496		% a debugging version that switches into trace mode
1497		:- block tprintf(-,?,?,?), tprintf(?,-,?,?).
1498		tprintf(string(FormatString),Value,PredRes,Span) :- PredRes = pred_true,
1499		when((ground(FormatString),ground(Value)),
1500		(fprintf2(user_output,FormatString,Value,Span),trace)).
1501
1502		:- public 'prolog_printf'/5.
1503		expects_spaninfo('prolog_printf').
1504		expects_waitflag('prolog_printf').
1505		external_pred_always_true('prolog_printf').
1506		prolog_printf(string(FormatString),Value,PredRes,Span,WF) :- PredRes = pred_true,
1507		file_format(user_output,FormatString,[initial(Value,WF)],Span),
1508		when(nonvar(Value),file_format(user_output,FormatString,[nonvar(Value,WF)],Span)),
1509		when((ground(FormatString),ground(Value)),
1510		fprintf2(user_output,FormatString,Value,Span)).
1511
1512		% vprintf: expression which returns argument as value
1513		expects_spaninfo('vprintf').
1514		:- public vprintf/4.
1515		vprintf(Format,Value,ValueRes,Span) :-
1516		printf(Format,[(int(1),Value)],pred_true,Span), % use itprintf for tracing
1517		equal_object(Value,ValueRes,vprintf). % we could generate a version which only instantiates when printing done
1518		expects_spaninfo('fvprintf').
1519		:- public fvprintf/5.
1520		fvprintf(File,Format,Value,ValueRes,Span) :-
1521		fprintf(File,Format,[(int(1),Value)],pred_true,Span),
1522		equal_object(Value,ValueRes,fvprintf). % we could generate a version which only instantiates when printing done
1523
1524
1525		% PRINT a single value as substitution
1526		performs_io('PRINT').
1527		external_subst_enabling_condition('PRINT',_,Truth) :- create_texpr(truth,pred,[],Truth).
1528		does_not_modify_state('PRINT').
1529		:- public 'PRINT'/3.
1530		:- block 'PRINT'(-,?,?), 'PRINT'(?,-,?).
1531		'PRINT'(Val,_Env,OutEnv) :- %print('PRINT : '), print(Env),nl,
1532		assert_side_effect_occurred(user_output),
1533		print_value(Val),nl, OutEnv=[].
1534
1535		% PRINT a single value as substitution; show backtracking
1536		performs_io('PRINT_BT').
1537		perform_directly('PRINT_BT').
1538		external_subst_enabling_condition('PRINT_BT',_,Truth) :- create_texpr(truth,pred,[],Truth).
1539		does_not_modify_state('PRINT_BT').
1540		:- public 'PRINT_BT'/3.
1541		:- block 'PRINT_BT'(-,?,?), 'PRINT_BT'(?,-,?).
1542		'PRINT_BT'(Val,_Env,OutEnv) :- %print('PRINT : '), print(Env),nl,
1543		assert_side_effect_occurred(user_output),
1544		print_value(Val),nl, OutEnv=[].
1545		'PRINT_BT'(Val,_Env,_OutEnv) :-
1546		assert_side_effect_occurred(user_output),
1547		print('BACKTRACKING: '),print_value(Val),nl, fail.
1548
1549		print_value(Val) :- translate:translate_bvalue(Val,TV), print(TV).
1550
1551
1552		performs_io('DEBUG_PRINT_STATE').
1553		external_subst_enabling_condition('DEBUG_PRINT_STATE',_,Truth) :- create_texpr(truth,pred,[],Truth).
1554		does_not_modify_state('DEBUG_PRINT_STATE').
1555		:- public 'DEBUG_PRINT_STATE'/3.
1556		:- block 'DEBUG_PRINT_STATE'(-,?,?).
1557		'DEBUG_PRINT_STATE'(Value,Env,OutEnv) :-
1558		assert_side_effect_occurred(user_output),
1559		print_value(Value),translate:print_bstate(Env),nl, OutEnv=[].
1560
1561		% PRINTF as substitution
1562		expects_spaninfo('PRINTF').
1563		performs_io('PRINTF').
1564		external_subst_enabling_condition('PRINTF',_,Truth) :- create_texpr(truth,pred,[],Truth).
1565		does_not_modify_state('PRINTF').
1566		:- public 'PRINTF'/5.
1567		:- block 'PRINTF'(-,?,?,?,?), 'PRINTF'(?,-,?,?,?), 'PRINTF'(?,?,-,?,?).
1568		'PRINTF'(string(FormatString),Value,_Env,OutEnvModifications,Span) :-
1569		% print('PRINTF'(FormatString,Value,_Env)),nl,
1570		when((ground(FormatString),ground(Value)),
1571		(fprintf2(user_output,FormatString,Value,Span),
1572		OutEnvModifications=[] /* substitution finished */
1573		)).
1574
1575		expects_spaninfo('FPRINTF').
1576		performs_io('FPRINTF').
1577		external_subst_enabling_condition('FPRINTF',_,Truth) :- create_texpr(truth,pred,[],Truth).
1578		does_not_modify_state('FPRINTF').
1579		:- public 'FPRINTF'/6.
1580		:- block 'FPRINTF'(-,?,?,?,?,?), 'FPRINTF'(?,-,?,?,?,?), 'FPRINTF'(?,?,-,?,?,?).
1581		'FPRINTF'(string(File),string(FormatString),Value,_Env,OutEnvModifications,Span) :-
1582		when((ground(FormatString),ground(Value)),
1583		(fprintf2(File,FormatString,Value,Span),
1584		OutEnvModifications=[] /* substitution finished */
1585		)).
1586
1587		file_format(user_output,FormatString,Args,Span) :- !,
1588		assert_side_effect_occurred(user_output),
1589		safe_call(myformat(user_output,FormatString,Args,Span),Span).
1590		file_format(File,FormatString,Args,Span) :-
1591		open(File,append,Stream,[encoding('UTF-8')]),
1592		assert_side_effect_occurred(file),
1593		safe_call(myformat(Stream,FormatString,Args,Span),Span),
1594		close(Stream). % TO DO: call_cleanup
1595
1596		:- public myformat/4.
1597		myformat(Stream,FormatString,Args,Span) :-
1598		on_exception(error(consistency_error(_,_,format_arguments),_),
1599		format(Stream,FormatString,Args),
1600		% backup: the user probably has not provided ~w annotations:
1601		(on_exception(error(consistency_error(_,_,format_arguments),_),
1602		format(Stream,FormatString,[]),
1603		(length(Args,NrArgs),
1604		ajoin(['Illegal format string, expecting ',NrArgs,' ~w arguments (see SICStus Prolog reference manual for syntax):'],Msg),
1605		add_error(external_functions,Msg,FormatString,Span))),
1606		format_args(Stream,Args))
1607		),
1608		flush_output(Stream).
1609
1610		format_args(_Stream,[]).
1611		format_args(Stream,[H|T]) :- format(Stream,'~w~n',H), format_args(Stream,T).
1612
1613		% a format with indentation and backtracking info:
1614		:- dynamic indentation_level/1.
1615		indentation_level(0).
1616		inc_indent :- retract(indentation_level(X)), X1 is X+1, assert(indentation_level(X1)).
1617		dec_indent :- retract(indentation_level(X)), X1 is X-1, assert(indentation_level(X1)).
1618		reset_ident :- retractall(indentation_level(_)), assert(indentation_level(0)).
1619		indent(Stream) :- indentation_level(L), %(L>28 -> trace ; true),
1620		indent_aux(L,Stream).
1621		indent_aux(X,Stream) :- X < 1, !, write(Stream,' ').
1622		indent_aux(X,Stream) :- write(Stream,'+-'), X1 is X-1, indent_aux(X1,Stream).
1623
1624		indent_format(Stream,Format,Args,Trace) :- inc_indent,
1625		indent(Stream), format(Stream,Format,Args),
1626		print_walltime(Stream),
1627		% my_term_hash(Args,Hash), format(Stream,'[hash ~w]~n',[Hash]), (Hash=101755762 -> trace ; true), %%
1628		flush_output(Stream),
1629		(Trace=trace -> trace ; true).
1630		%indent_format(_Stream,_Format,Args,_Trace) :- my_term_hash(Args,Hash),(Hash=553878463258718990 -> trace).
1631		indent_format(Stream,Format,Args,Trace) :-
1632		indent(Stream), write(Stream,'BACKTRACKING '),
1633		% my_term_hash(Args,Hash), format(Stream,'[hash ~w] ',[Hash]), %% (Hash=553878463258718990 -> trace ; true), %%
1634		format(Stream,Format,Args),
1635		print_walltime(Stream), %% comment in to see walltime info
1636		flush_output(Stream),
1637		dec_indent,
1638		(Trace=trace -> trace ; true),
1639		fail.
1640
1641		:- dynamic ref_walltime/1, prev_walltime/1.
1642		reset_walltime :- retractall(prev_walltime(_)), retractall(ref_walltime(_)),
1643		statistics(walltime,[WT,_]),
1644		assert(prev_walltime(WT)),
1645		assert(ref_walltime(WT)).
1646		print_walltime(File) :- statistics(walltime,[WT,_]),
1647		(ref_walltime(RefWT) -> RWT is WT-RefWT ; RWT = 0, assert(ref_walltime(WT))),
1648		(retract(prev_walltime(PWT)) -> T is WT-PWT, indent(File),format(File,' ~w ms (walltime; total ~w ms)~n',[T,RWT])
1649		; true),
1650		assert(prev_walltime(WT)).
1651		:- public 'TRACE'/2.
1652		:- block 'TRACE'(-,?).
1653		'TRACE'(pred_true,R) :- !,trace,R=pred_true.
1654		'TRACE'(pred_false,pred_true).
1655
1656		% --------------------------------------------
1657
1658		% ARGV, ARGC
1659
1660		:- dynamic argv_string/2, argc_number/1.
1661		argc_number(0).
1662		reset_argv :-
1663		retractall(argv_string(_,_)),
1664		retractall(argc_number(_)),
1665		assert(argc_number(0)).
1666
1667		:- use_module(kernel_strings,[split_atom_string/3]).
1668		% call to set the commandline arguments, e.g., from probcli
1669		set_argv_from_atom(X) :-
1670		retractall(argv_string(_,_)),
1671		retractall(argc_number(_)),
1672		split_atom_string(X,' ',List),
1673		set_argv_from_list(List).
1674		set_argv_from_list(List) :-
1675		retractall(argv_string(_,_)),
1676		retractall(argc_number(_)),
1677		set_argv_from_list_aux(List).
1678		set_argv_from_list_aux(List) :-
1679		length(List,Len),
1680		assert(argc_number(Len)),
1681		debug:debug_println(9,argc(Len)),
1682		nth1(N,List,String), % we number the arguments in B style
1683		debug:debug_println(9,argv(N,String)),
1684		assert(argv_string(N,String)),
1685		fail.
1686		set_argv_from_list_aux(_).
1687
1688		external_fun_type('ARGV',[],[integer,string]).
1689		% access to the command-line arguments provided to probcli (after --)
1690		% first argument is ARGV(1) not ARGV(0)
1691		:- public 'ARGV'/2.
1692		:- block 'ARGV'(-,?).
1693		'ARGV'(int(N),S) :- argv2(N,S).
1694		:- block argv2(-,?).
1695		argv2(Nr,Res) :- % print(get_argv(Nr,Res)),nl,
1696		(argv_string(Nr,S) -> Res=string(S)
1697		; Nr=0 -> add_error(external_functions,'Command-line argument does not exist, numbering starts at 1: ',Nr), Res=string('')
1698		; add_error(external_functions,'Command-line argument does not exist: ',Nr), Res=string('')).
1699
1700		external_fun_type('ARGC',[],[integer]).
1701		:- public 'ARGC'/1.
1702		'ARGC'(int(X)) :- argc_number(X).
1703
1704		% --------------------------------------------
1705
1706		% RANDOM
1707
1708		:- assert_must_succeed(( external_functions:call_external_function('RANDOM',[0,1],[int(0),int(1)],int(0),integer,unknown,_WF) )).
1709		:- use_module(library(random)).
1710		% Generate a random number >= Low and < Up
1711		% warning: this is not a mathematical function
1712		:- public 'RANDOM'/3.
1713		is_not_declarative('RANDOM').
1714		:- block 'RANDOM'(-,?,?), 'RANDOM'(?,-,?).
1715		'RANDOM'(int(Low),int(Up),int(R)) :- random2(Low,Up,R).
1716		:- block random2(-,?,?), random2(?,-,?).
1717		random2(L,U,R) :- random(L, U, R).
1718
1719		% pick a random element from a set
1720		:- public 'random_element'/4.
1721		is_not_declarative('random_element').
1722		expects_waitflag('random_element').
1723		expects_spaninfo('random_element').
1724		:- block 'random_element'(-,?,?,?).
1725		random_element([],_,Span,WF) :- !,
1726		add_wd_error_span('random_element applied to empty set: ',[],Span,WF).
1727		random_element([H|T],El,_,WF) :- !,
1728		custom_explicit_sets:expand_custom_set_to_list_wf(T,ET,_Done,'random_element',WF),
1729		block_length(ET,1,Len),
1730		random_select_from_list([H|ET],Len,El).
1731		random_element(CS,Res,_,_) :- is_interval_closure_or_integerset(CS,Low,Up),!,
1732		U1 is Up+1,
1733		random(Low,U1,H), Res = int(H).
1734		random_element(CS,X,Span,WF) :-
1735		custom_explicit_sets:expand_custom_set(CS,ER),
1736		random_element(ER,X,Span,WF).
1737
1738		:- block block_length(-,?,?).
1739		block_length([],Acc,Acc).
1740		block_length([_|T],Acc,R) :- A1 is Acc+1, block_length(T,A1,R).
1741
1742		:- block random_select_from_list(?,-,?).
1743		random_select_from_list(List,Len,Res) :-
1744		random(0,Len,RandNr),
1745		nth0(RandNr,List,El),
1746		kernel_objects:equal_object(El,Res).
1747
1748
1749		% generates a random subset of a finite set
1750		:- public 'random_subset'/4.
1751		is_not_declarative('random_subset').
1752		expects_waitflag('random_subset').
1753		expects_spaninfo('random_subset').
1754		:- block 'random_subset'(-,?,?,?).
1755		random_subset(Set,Subset,Span,WF) :- !,
1756		custom_explicit_sets:expand_custom_set_to_list_wf(Set,ESet,Done,'random_subset',WF),
1757		random_subset_aux(Done,ESet,Subset,Span,WF).
1758
1759		:- use_module(library(random),[random_subseq/3]).
1760		:- block random_subset_aux(-,?,?,?,?).
1761		random_subset_aux(_Done,ESet,Subset,_Span,WF) :-
1762		random_subseq(ESet,Result,_Rest),
1763		kernel_objects:equal_object_wf(Result,Subset,WF).
1764
1765		% generates a random subset of a finite set
1766		:- public 'random_permutation'/4.
1767		is_not_declarative('random_permutation').
1768		expects_waitflag('random_permutation').
1769		expects_spaninfo('random_permutation').
1770		:- block 'random_permutation'(-,?,?,?).
1771		random_permutation(Set,Permutation,Span,WF) :- !,
1772		custom_explicit_sets:expand_custom_set_to_list_wf(Set,ESet,Done,'random_permutation',WF),
1773		random_perm_aux(Done,ESet,Permutation,Span,WF).
1774
1775		:- use_module(library(random),[random_permutation/2]).
1776		:- block random_perm_aux(-,?,?,?,?).
1777		random_perm_aux(_Done,ESet,Permutation,_Span,_WF) :-
1778		random_permutation(ESet,Result),
1779		convert_set_to_seq(Result,Permutation). % should we call WF version
1780
1781		:- use_module(library(system)).
1782
1783		:- assert_must_succeed(( external_functions:call_external_function('TIME',[y],[string(year)],int(Y),integer,unknown,_WF), number(Y), Y>2011 )).
1784		:- assert_must_succeed(( external_functions:call_external_function('TIME',[m],[string(month)],int(M),integer,unknown,_WF), number(M), M>0, M<13 )).
1785		:- public 'TIME'/2.
1786		is_not_declarative('TIME'). % as time can change with next call
1787		'TIME'(string(S),int(N)) :- time2(S,N).
1788		:- block time2(-,?).
1789		time2(now,N) :- !, now(N). % provide UNIX timesstamp
1790		time2(year,N) :- !,datime(datime(N,_,_,_,_,_)).
1791		time2(month,N) :- !,datime(datime(_,N,_,_,_,_)).
1792		time2(day,N) :- !,datime(datime(_,_,N,_,_,_)).
1793		time2(hour,N) :- !,datime(datime(_,_,_,N,_,_)).
1794		time2(min,N) :- !,datime(datime(_,_,_,_,N,_)).
1795		time2(sec,N) :- !,datime(datime(_,_,_,_,_,N)).
1796		time2(OTHER,_) :- add_error(time2,'Illegal time field (must be now,year,month,day,hour,min,sec): ',OTHER),fail.
1797
1798		:- assert_must_succeed(( external_functions:call_external_function('GET_INFO',[time],[string(time)],string(M),string,unknown,_WF), atom(M) )).
1799		:- public 'GET_INFO'/2.
1800		'GET_INFO'(string(S),Res) :- get_info2(S,Res).
1801		:- use_module(library(codesio)).
1802		:- block get_info2(-,?).
1803		get_info2(time,Res) :- !, datime(datime(Year,Month,Day,Hour,Min,Sec)),
1804		(Min<10
1805		-> format_to_codes('~w/~w/~w - ~wh0~w ~ws',[Day,Month,Year,Hour,Min,Sec],Codes)
1806		; format_to_codes('~w/~w/~w - ~wh~w ~ws',[Day,Month,Year,Hour,Min,Sec],Codes)
1807		),
1808		atom_codes(INFO, Codes), Res=string(INFO).
1809		get_info2(OTHER,_) :- add_error(time2,'Illegal GET_INFO field (must be time): ',OTHER),fail.
1810
1811		:- public 'TIMESTAMP_INFO'/3.
1812		:- assert_must_succeed(external_functions:'TIMESTAMP_INFO'(string('year'),int(1498484624),int(2017))).
1813		:- assert_must_succeed(external_functions:'TIMESTAMP_INFO'(string('month'),int(1498484624),int(6))).
1814		% second argument is ticks obtained by TIME("now")
1815		:- block 'TIMESTAMP_INFO'(-,-,-).
1816		'TIMESTAMP_INFO'(string(S),int(Ticks),int(Res)) :- time_info2(S,Ticks,Res).
1817		:- block time_info2(-,?,?), time_info2(?,-,?).
1818		time_info2(year,Ticks,N) :- !,datime(Ticks,datime(N,_,_,_,_,_)).
1819		time_info2(month,Ticks,N) :- !,datime(Ticks,datime(_,N,_,_,_,_)).
1820		time_info2(day,Ticks,N) :- !,datime(Ticks,datime(_,_,N,_,_,_)).
1821		time_info2(hour,Ticks,N) :- !,datime(Ticks,datime(_,_,_,N,_,_)).
1822		time_info2(min,Ticks,N) :- !,datime(Ticks,datime(_,_,_,_,N,_)).
1823		time_info2(sec,Ticks,N) :- !,datime(Ticks,datime(_,_,_,_,_,N)).
1824		time_info2(OTHER,_,_) :- add_error(time_info2,'Illegal time field (must be now,year,month,day,hour,min,sec): ',OTHER),fail.
1825
1826		:- public 'TIMESTAMP'/7.
1827		:- assert_must_succeed((external_functions:'TIMESTAMP'(int(2017),int(6),int(26),int(H),int(Min),int(S),int(1498484624)), H==15, Min==43,S==44)).
1828		:- block 'TIMESTAMP'(-,-,-,-,-,-,-).
1829		'TIMESTAMP'(int(Y),int(M),int(D),int(H),int(Min),int(S),int(Res)) :-
1830		timestamp2(Y,M,D,H,Min,S,Res).
1831
1832		:- block timestamp2(-,?,?,?,?,?,-), timestamp2(?,-,?,?,?,?,-), timestamp2(?,?,-,?,?,?,-),
1833		timestamp2(?,?,?,-,?,?,-), timestamp2(?,?,?,?,?,-,-).
1834		timestamp2(Y,M,D,H,Min,S,ResTimeStamp) :- datime(ResTimeStamp, datime(Y,M,D,H,Min,S)).
1835
1836
1837		:- public 'WALLTIME'/1.
1838		is_not_declarative('WALLTIME'). % as time can change with next call
1839		'WALLTIME'(int(X)) :- statistics(walltime,[X,_]).
1840
1841		:- volatile last_walltime/1.
1842		:- dynamic last_walltime/1.
1843		:- public 'DELTA_WALLTIME'/1.
1844		is_not_declarative('DELTA_WALLTIME'). % as time can change with next call
1845		'DELTA_WALLTIME'(int(D)) :- statistics(walltime,[X,_]),
1846		(retract(last_walltime(L)) -> D is X-L ; D = 0),
1847		assert(last_walltime(X)).
1848
1849		:- public 'RUNTIME'/1.
1850		is_not_declarative('RUNTIME'). % as time can change with next call
1851		'RUNTIME'(int(X)) :- statistics(runtime,[X,_]).
1852
1853		:- public 'SLEEP'/3.
1854		external_subst_enabling_condition('SLEEP',_,Truth) :- create_texpr(truth,pred,[],Truth).
1855		:- use_module(library(system),[sleep/1]).
1856		:- block 'SLEEP'(-,?,?), 'SLEEP'(?,-,?).
1857		'SLEEP'(int(X),_Env,OutEnvModifications) :- when(nonvar(X),
1858		(Seconds is X / 1000, sleep(Seconds), OutEnvModifications=[])).
1859
1860
1861		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1862		% check if a given expression is valued in the deterministic phase; warn otherwise
1863
1864		:- use_module(kernel_tools,[ground_value_check/2]).
1865		expects_spaninfo('CHECK_DET').
1866		expects_unevaluated_args('CHECK_DET').
1867		expects_waitflag('CHECK_DET').
1868		:- public 'CHECK_DET'/5.
1869		'CHECK_DET'(Value,PredRes,[UnEvalArg],Span,WF) :-
1870		ground_value_check(Value,Ground),
1871		kernel_waitflags:get_wait_flag0(WF,WF0),
1872		kernel_waitflags:get_wait_flag1(WF,WF1),
1873		PredRes=pred_true,
1874		check_det_aux(Ground,Value,WF0,WF1,UnEvalArg,Span).
1875
1876		:- block check_det_aux(-,?,?,-,?,?).
1877		check_det_aux(Ground,Value,_WF0,_WF1,UnEvalArg,Span) :- var(Ground),!,
1878		translate:translate_bexpression(UnEvalArg,S),
1879		add_error(external_functions,'Argument has not been computed deterministically: ',S,Span),
1880		translate:print_bvalue(Value),nl.
1881		check_det_aux(_Ground,Value,WF0,WF1,UnEvalArg,_Span) :- debug:debug_mode(on),!,
1882		translate:translate_bexpression(UnEvalArg,S),
1883		format('Value determined (WF0=~w,WF1=~w) : ~w~n',[WF0,WF1,S]),
1884		translate:print_bvalue(Value),nl.
1885		check_det_aux(_Ground,_Value,_WF0,_WF1,_UnEvalArgs,_Span).
1886
1887		% check if a given expression has already a ground value when
1888		% the predicate is called
1889
1890		% the predicate is true when the value is ground, false otherwise
1891		:- public 'IS_DETERMINED'/2.
1892		'IS_DETERMINED'(Value,PredRes) :- ground(Value),!,PredRes=pred_true.
1893		'IS_DETERMINED'(_Value,pred_false).
1894
1895		% other variant: the predicate is always true, the information if the variable is written
1896		% to a file to check it later.
1897		expects_spaninfo('IS_DETERMINED_INTO_FILE').
1898		:- public 'IS_DETERMINED_INTO_FILE'/5.
1899		'IS_DETERMINED_INTO_FILE'(FileValue,VariableValue,Value,PredRes,SpanInfo) :-
1900		check_value_is_string(FileValue,'IS_DETERMINED_INTO_FILE','file name',SpanInfo,File),
1901		check_value_is_string(VariableValue,'IS_DETERMINED_INTO_FILE','variable name',SpanInfo,Varname),
1902		( ground(File) ->
1903		open(File,write,S,[encoding('UTF-8')]),
1904		call_cleanup( check_determined2(Value,S,Varname), close(S))
1905		; otherwise ->
1906		add_error(external_functions,'### EXTERNAL Unspecified file in check_determined','',SpanInfo)),
1907		PredRes = pred_true.
1908		check_determined2(Value,S,Varname) :-
1909		check_determined3(Value,Varname,Term),
1910		writeq(S,Term),write(S,'.\n').
1911		check_determined3(Value,Name,Term) :- ground(Value),!,Term=determined_value(Name,Value).
1912		check_determined3(_Value,Name,not_determined_value(Name)).
1913
1914		check_value_is_string(string(S),_PredName,_Location,_SpanInfo,String) :-
1915		!, String=S.
1916		check_value_is_string(Value,PredName,Location,SpanInfo,_String) :-
1917		atom_concat('### EXTERNAL ',PredName,Msg1),
1918		atom_concat(Msg1,': Type error, expected string as ',Msg2),
1919		atom_concat(Msg2,Location,Msg),
1920		add_error(external_functions,Msg,Value,SpanInfo),
1921		fail.
1922
1923
1924		:- public 'SEE'/3.
1925		is_not_declarative('SEE').
1926		:- dynamic open_stream/2.
1927		'SEE'(string(File),_S,[]) :- b_absolute_file_name(File,AFile),
1928		open_stream(AFile,_),!,
1929		print('File already open: '), print(File),nl.
1930		'SEE'(string(File),_S,[]) :-
1931		b_absolute_file_name(File,AFile),
1932		open_absolute_file_for_reading(AFile,_Stream).
1933
1934		open_file_for_reading_if_necessary(File,Stream) :-
1935		b_absolute_file_name(File,AFile),
1936		(open_stream(AFile,S) -> Stream=S
1937		; open_absolute_file_for_reading(AFile,Stream)).
1938		open_absolute_file_for_reading(AFile,Stream) :-
1939		open(AFile,read,Stream,[encoding('UTF-8')]),
1940		print(opened_file(AFile,Stream)),nl,
1941		assert_side_effect_occurred(file),
1942		assert(open_stream(AFile,Stream)).
1943
1944		%correct_file_open_mode(read).
1945		%correct_file_open_mode(write).
1946		%correct_file_open_mode(append).
1947
1948		:- public 'GET_CODE'/2.
1949		performs_io('GET_CODE').
1950		'GET_CODE'(string(File),int(Code)) :-
1951		b_absolute_file_name(File,AFile),
1952		open_stream(AFile,S),
1953		assert_side_effect_occurred(file),
1954		get_code(S,Code). %,print(got_code(S,Code)),nl.
1955
1956		:- public 'GET_CODE_STDIN'/1.
1957		'GET_CODE_STDIN'(int(Code)) :- get_code(user_input,Code).
1958
1959		:- public 'SEEN'/3.
1960		is_not_declarative('SEEN').
1961		'SEEN'(string(File),_S,[]) :- b_absolute_file_name(File,AFile),
1962		retract(open_stream(AFile,S)),
1963		assert_side_effect_occurred(file),
1964		close(S).
1965
1966		close_all_files :- retract(open_stream(_File,S)),
1967		close(S),fail.
1968		close_all_files.
1969
1970
1971		open_utf8_file_for_reading(AFile,Stream,SpanInfo) :-
1972		safe_call(open(AFile,read,Stream,[encoding('UTF-8')]),SpanInfo).
1973
1974		:- public 'READ_FILE_AS_STRINGS'/3.
1975		performs_io('READ_FILE_AS_STRINGS').
1976		external_subst_enabling_condition('READ_FILE_AS_STRINGS',_,Truth) :- create_texpr(truth,pred,[],Truth).
1977		expects_spaninfo('READ_FILE_AS_STRINGS').
1978		:- block 'READ_FILE_AS_STRINGS'(-,?,?).
1979		'READ_FILE_AS_STRINGS'(string(File),Res,SpanInfo) :-
1980		b_absolute_file_name(File,AFile,SpanInfo),
1981		open_utf8_file_for_reading(AFile,Stream,SpanInfo),!,
1982		format('% Opened file: ~w~n',[File]),
1983		% no side-effect: as everything read in one go
1984		call_cleanup(read_lines(Stream,Res),
1985		close(Stream)).
1986		'READ_FILE_AS_STRINGS'(string(File),_Res,_SpanInfo) :-
1987		format('% Opening file failed: ~w~n',[File]),fail.
1988		read_lines(File,Res) :- read_lines_loop(1,File,Lines),
1989		kernel_objects:equal_object(Res,Lines).
1990		read_lines_loop(Nr,Stream,Lines) :- read_line(Stream,Line),
1991		debug:debug_println(9,read_line(Nr,Line)),
1992		(Line = end_of_file -> Lines = []
1993		; atom_codes(Atom,Line), Lines = [(int(Nr),string(Atom))|T],
1994		N1 is Nr+1,read_lines_loop(N1,Stream,T)).
1995
1996
1997		:- public 'READ_FILE_AS_STRING'/3.
1998		performs_io('READ_FILE_AS_STRING').
1999		external_subst_enabling_condition('READ_FILE_AS_STRING',_,Truth) :- create_texpr(truth,pred,[],Truth).
2000		expects_spaninfo('READ_FILE_AS_STRING').
2001		:- block 'READ_FILE_AS_STRING'(-,?,?).
2002		'READ_FILE_AS_STRING'(string(File),Res,SpanInfo) :-
2003		b_absolute_file_name(File,AFile,SpanInfo),
2004		open_utf8_file_for_reading(AFile,Stream,SpanInfo),!,
2005		format('% Opened file: ~w~n',[File]),
2006		% no side-effect: as everything read in one go
2007		call_cleanup(read_all_codes(Stream,All,[]),
2008		close(Stream)),
2009		atom_codes(ResStr,All), Res = string(ResStr).
2010
2011		% read all codes in the stream:
2012		read_all_codes(Stream) --> {read_line(Stream,Line), Line \= end_of_file, !},
2013		Line, "\n",
2014		read_all_codes(Stream).
2015		read_all_codes(_) --> "".
2016
2017
2018		:- public 'READ_LINE'/3.
2019		expects_spaninfo('READ_LINE').
2020		external_subst_enabling_condition('READ_LINE',_,Truth) :- create_texpr(truth,pred,[],Truth).
2021		performs_io('READ_LINE').
2022		'READ_LINE'(string(File),Res,_SpanInfo) :-
2023		open_file_for_reading_if_necessary(File,Stream),
2024		read_line(Stream,Line),
2025		debug:debug_println(9,read_line(Line)),
2026		assert_side_effect_occurred(file),
2027		(Line = end_of_file
2028		-> add_error(external_functions,'Attempting to read past EOF: ',File),
2029		Res = ""
2030		; atom_codes(Atom,Line), Res = string(Atom)).
2031
2032		:- public 'EOF'/2.
2033		'EOF'(string(File),Res) :- eof2(File,Res).
2034		:- block eof2(-,?).
2035		eof2(File,Res) :-
2036		open_file_for_reading_if_necessary(File,Stream),
2037		((peek_code(Stream,C), C = -1) -> Res = pred_true ; Res = pred_false). % for Linux compatibility
2038		% (at_end_of_stream(Stream) -> Res = pred_true ; Res=pred_false).
2039
2040		:- public 'EOF_STDIN'/2.
2041		'EOF_STDIN'(_,Res) :- % dummy argument to enable valid external predicate type declarations
2042		((peek_code(user_input,C), C = -1) -> Res = pred_true ; Res = pred_false).
2043
2044
2045		:- public 'CURRENT_FILE_POSITION'/3.
2046		'CURRENT_FILE_POSITION'(string(File),string(Field),Res) :-
2047		open_file_for_reading_if_necessary(File,Stream),
2048		stream_position(Stream,Pos),
2049		% POS must be one of byte_count [only for binary streams], line_count, character_count, line_position
2050		stream_position_data(Field,Pos,R), Res=int(R).
2051
2052		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2053
2054		:- public 'ADD_ERROR'/5.
2055		expects_spaninfo('ADD_ERROR').
2056		'ADD_ERROR'(string(Msg),Expr,_S,[],SpanInfo) :-
2057		add_error(b_user_program,Msg,Expr,SpanInfo).
2058
2059
2060		:- public 'ASSERT_TRUE'/5.
2061		expects_spaninfo('ASSERT_TRUE').
2062		expects_waitflag('ASSERT_TRUE').
2063		external_fun_has_wd_condition('ASSERT_TRUE').
2064
2065		'ASSERT_TRUE'(PredVal,string(Msg),PredRes,SpanInfo,WF) :-
2066		assert_true(PredVal,Msg,PredRes,SpanInfo,WF).
2067
2068		:- block assert_true(-,?,?,?,?).
2069		assert_true(pred_true,_Msg,pred_true,_SpanInfo,_WF).
2070		assert_true(pred_false,Msg,Res,SpanInfo,WF) :-
2071		formatsilent('% Waiting for enumeration to finish to raise ASSERT_TRUE:~n ~w~n',[Msg]),
2072		add_error_ef('ASSERT_TRUE',Msg,'',SpanInfo,WF,Res).
2073
2074		% we could also use: add_wd_error_set_result
2075		add_error_ef(Source,Msg,Term,Span,WF,Res) :-
2076		get_enumeration_finished_wait_flag(WF,AWF),
2077		add_error_ef_aux(AWF,Source,Msg,Term,Span,WF,Res).
2078
2079		:- block add_error_ef_aux(-,?,?,?,?,?,?).
2080		add_error_ef_aux(_AWF,Source,Msg,Term,Span,_WF,Res) :-
2081		add_error(Source,Msg,Term,Span),
2082		Res = pred_false.
2083
2084		:- public 'ASSERT_EXPR'/6.
2085		expects_spaninfo('ASSERT_EXPR').
2086		expects_waitflag('ASSERT_EXPR').
2087		external_fun_has_wd_condition('ASSERT_EXPR').
2088
2089		'ASSERT_EXPR'(PredVal,string(Msg),ExprVal,Res,SpanInfo,WF) :-
2090		% TO DO: call assertion_expression(Cond,ErrMsg,Expr)
2091		assert_expr(PredVal,Msg,ExprVal,Res,SpanInfo,WF).
2092
2093		:- block assert_expr(-,?,?,?,?,?).
2094		assert_expr(pred_true,_Msg,ExprVal,Res,_SpanInfo,_WF) :-
2095		Res = ExprVal.
2096		assert_expr(pred_false,Msg,_ExprVal,Res,SpanInfo,WF) :-
2097		add_error_ef('ASSERT_EXPR',Msg,'',SpanInfo,WF,Res).
2098
2099		% --------------------------
2100		% Reflection Functions
2101
2102		external_fun_type('STATE_AS_STRING',[],[integer,string]).
2103		:- public 'STATE_AS_STRING'/3.
2104		expects_waitflag('STATE_AS_STRING').
2105		'STATE_AS_STRING'(int(X),StateStr,WF) :-
2106		state_space:get_state_space_stats(NrNodes,_NrTransitions,_ProcessedNodes),
2107		get_wait_flag(NrNodes,'STATE_AS_STRING',WF,LWF),
2108		get_state2(X,StateStr,LWF).
2109		:- block get_state2(-,?,-).
2110		get_state2(X,StateStr,_) :-
2111		convert_id_to_nr(IDX,X),
2112		state_space:visited_expression(IDX,S),
2113		translate:translate_bstate(S,Str),
2114		StateStr = string(Str).
2115
2116		:- public 'STATE_SUCC'/4.
2117		external_fun_type('STATE_SUCC',[],[integer,integer,boolean]).
2118		expects_waitflag('STATE_SUCC').
2119		'STATE_SUCC'(X,Y,Res,WF) :- 'STATE_TRANS'(X,_,Y,Res,WF).
2120
2121		external_fun_type('STATE_TRANS',[],[integer,string,integer,boolean]).
2122		expects_waitflag('STATE_TRANS').
2123		'STATE_TRANS'(int(X),OperationName,int(Y),Res,WF) :-
2124		'STATE_TRANS_ARGS'(int(X),OperationName,_,int(Y),Res,WF).
2125
2126		external_fun_type('STATE_TRANS_ARGS',[X],[integer,string,X,integer,boolean]).
2127		expects_waitflag('STATE_TRANS_ARGS').
2128		'STATE_TRANS_ARGS'(int(X),OperationName,OperationArgs,int(Y),Res,WF) :-
2129		state_space:get_state_space_stats(NrNodes,_NrTransitions,_ProcessedNodes),
2130		get_wait_flag(NrNodes,'STATE_TRANS',WF,LWF),
2131		get_wait_flag1(WF,WF1),
2132		get_succ2(X,OperationName,OperationArgs,Y,Res,LWF,WF1).
2133		:- block get_succ2(-,?,?,-,?,-,?),
2134		get_succ2(?,?,?,?,?,?,-). % wait at least until WF1 (or at least wf0); as we do non-deterministic enumeration ! (e.g., otherwise b_interprter_components gets confused !!)
2135		get_succ2(X,OperationName,OperationArgs,Y,Res,_,_) :- convert_id_to_nr(IDX,X), convert_id_to_nr(IDY,Y),
2136		if(state_space_transition(IDX,IDY,OperationName,OperationArgs),Res=pred_true,Res=pred_false).
2137
2138		state_space_transition(IDX,IDY,OperationName,OperationArgs) :-
2139		state_space:transition(IDX,Transition,IDY),
2140		op_functor(Transition,OperationName),
2141		op_args(Transition,OperationArgs).
2142
2143		% root is represented as -1
2144		:- block convert_id_to_nr(-,-).
2145		convert_id_to_nr(ID,X) :- ID==root, !, X is -1.
2146		convert_id_to_nr(ID,X) :- X == -1, !, ID=root.
2147		convert_id_to_nr(X,X).
2148
2149		:- use_module(specfile,[get_operation_name/2,get_operation_arguments/2]).
2150		op_functor(OpTerm,Res) :- get_operation_name(OpTerm,Name),
2151		Res = string(Name).
2152
2153		:- use_module(tools,[convert_list_into_pairs/2]).
2154		op_args(OpTerm,OperationArgs) :- get_operation_arguments(OpTerm,As),
2155		convert_list_into_pairs(As,ArgTerm),
2156		kernel_objects:equal_object(OperationArgs,ArgTerm).
2157
2158
2159		:- public 'STATE_SAT'/4.
2160		expects_waitflag('STATE_SAT').
2161		external_fun_type('STATE_SAT',[],[integer,string,boolean]).
2162		% check whether formula as string holds in a state
2163		:- block 'STATE_SAT'(?,-,?,?).
2164		'STATE_SAT'(int(X),string(Formula),Res,WF) :- %print(parsing(Formula)),nl, trace,
2165		parse_pred(Formula,TFormula),
2166		state_space:get_state_space_stats(NrNodes,_NrTransitions,_ProcessedNodes),
2167		get_wait_flag(NrNodes,'STATE_SAT',WF,LWF),
2168		state_sat2(X,TFormula,Res,LWF,WF).
2169		:- block state_sat2(?,-,?,?,?),state_sat2(-,?,?,-,?).
2170		state_sat2(X,TFormula,PredRes,_,WF) :-
2171		(number(X) -> test_formula_in_state(X,TFormula,PredRes,WF)
2172		; test_formula_in_state(ID,TFormula,PredRes,WF), ID \= root, X=ID % avoid CLPFD errors on X
2173		).
2174
2175		:- use_module(b_global_sets,[add_prob_deferred_set_elements_to_store/3]).
2176		:- use_module(specfile,[expand_const_and_vars_to_full_store/2,state_corresponds_to_fully_setup_b_machine/2]).
2177		%:- use_module(b_interpreter,[b_try_check_boolean_expression_wf/5]).
2178		test_formula_in_state(ID,Pred,PredRes,WF) :-
2179		state_space:visited_expression(ID,State),
2180		state_corresponds_to_fully_setup_b_machine(State,FullState),
2181		add_prob_deferred_set_elements_to_store(FullState,FullState1,visible),
2182		debug_println(9,check(Pred,FullState1,PredRes)),
2183		b_interpreter:b_try_check_boolean_expression_wf(Pred,[],FullState1,WF,PredRes).
2184
2185
2186		:- public 'EVAL'/4.
2187		expects_waitflag('EVAL'). % external function with unknown return type
2188		'EVAL'(int(X),string(Expr),Value,WF) :-
2189		'STATE_EVAL'(int(X),string(Expr),Value,pred_true,WF).
2190		:- public 'STATE_EVAL'/5.
2191		expects_waitflag('STATE_EVAL'). % external predicate
2192		% evaluate expression and check whether value corresponds to provided value
2193		% (needed for type inference of the external predicate)
2194		:- block 'STATE_EVAL'(?,-,?,?,?).
2195		'STATE_EVAL'(int(X),string(Expr),Value,PredRes,WF) :-
2196		% string must be provided ; we assume it will be ground
2197		parse_expr(Expr,TExpr),
2198		state_space:get_state_space_stats(NrNodes,_NrTransitions,_ProcessedNodes),
2199		get_wait_flag(NrNodes,'STATE_SAT',WF,LWF),
2200		state_eval2(X,TExpr,Value,LWF,PredRes).
2201		:- block state_eval2(?,-,?,?,?),state_eval2(-,?,?,-,?).
2202		state_eval2(X,TExpr,Value,_,PredRes) :-
2203		(number(X) -> eval_formula_in_state(X,TExpr,Value,PredRes)
2204		; eval_formula_in_state(ID,TExpr,Value,PredRes), ID \= root, X=ID % avoid CLPFD errors on X
2205		).
2206		:- use_module(kernel_equality,[equality_objects/3]).
2207		eval_formula_in_state(ID,TExpr,Value,PredRes) :-
2208		state_space:visited_expression(ID,State),
2209		state_corresponds_to_fully_setup_b_machine(State,FullState),
2210		add_prob_deferred_set_elements_to_store(FullState,FullState1,visible),
2211		debug_println(9,eval(TExpr,FullState1,Value)),
2212		kernel_equality:equality_objects(Value,TExprValue,PredRes), % TO DO: Stronger Checks that types compatible
2213		b_interpreter:b_compute_expression_nowf(TExpr,[],FullState1,TExprValue).
2214
2215		:- use_module(library(terms),[term_hash/2]).
2216		:- use_module(bmachine,[b_parse_machine_predicate/3]).
2217		:- dynamic parse_pred_cache/3.
2218		parse_pred(PredStr,TPred) :- term_hash(PredStr,Hash), parse_pred(PredStr,Hash,TPred).
2219		parse_pred(PredStr,Hash,TPred) :- parse_pred_cache(Hash,PredStr,TC),!, TPred=TC.
2220		parse_pred(PredStr,Hash,TPred) :-
2221		bmachine:b_parse_machine_predicate(PredStr,[prob_ids(visible),variables],TC),
2222		assert(parse_pred_cache(Hash,PredStr,TC)),
2223		TPred=TC.
2224
2225		:- dynamic parse_expr_cache/3.
2226		parse_expr(ExprStr,TExpr) :- term_hash(ExprStr,Hash), parse_expr(ExprStr,Hash,TExpr).
2227		parse_expr(ExprStr,Hash,TExpr) :- parse_expr_cache(Hash,ExprStr,TC),!, TExpr=TC.
2228		parse_expr(ExprStr,Hash,TExpr) :-
2229		atom_codes(ExprStr,Codes), %print(parsing(Expr,Codes)),nl,
2230		bmachine:b_parse_machine_expression_from_codes_with_prob_ids(Codes,TC),
2231		assert(parse_expr_cache(Hash,ExprStr,TC)),
2232		TExpr=TC.
2233
2234		:- use_module(kernel_strings,[generate_code_sequence/3]).
2235		external_fun_type('HISTORY',[],[seq(integer)]).
2236		:- public 'HISTORY'/1.
2237		'HISTORY'(Value) :-
2238		state_space:history(RH), reverse(RH,[root|Rest]),
2239		generate_code_sequence(Rest,1,Hist),
2240		kernel_objects:equal_object(Value,Hist).
2241
2242		:- use_module(state_space,[is_initial_state_id/1]).
2243
2244		:- public 'INITIAL_STATE'/3.
2245		expects_waitflag('INITIAL_STATE'). % external function with unknown return type
2246		'INITIAL_STATE'(int(InitialState),PredRes,WF) :-
2247		get_wait_flag(2,'INITIAL_STATE',WF,LWF),
2248		is_init2(InitialState,PredRes,LWF).
2249		:- block is_init2(-,-,?), is_init2(-,?,-).
2250		is_init2(InitialState,PredRes,_) :-
2251		PredRes == pred_true,!,
2252		is_initial_state_id(InitialState).
2253		is_init2(InitialState,PredRes,_) :- number(InitialState),!,
2254		(is_initial_state_id(InitialState) -> PredRes=pred_true ; PredRes=pred_false).
2255		is_init2(InitialState,PredRes,_LWF) :-
2256		PredRes == pred_false,!,
2257		when(nonvar(InitialState), \+is_initial_state_id(InitialState)).
2258		is_init2(InitialState,PredRes,LWF) :-
2259		add_internal_error('Uncovered case: ', is_init2(InitialState,PredRes,LWF)),fail.
2260
2261
2262		% provide information about a particular B machine in the project
2263		:- public 'MACHINE_INFO'/4.
2264		expects_waitflag('MACHINE_INFO').
2265		:- block 'MACHINE_INFO'(?,-,?,?).
2266		'MACHINE_INFO'(M,string(I),Value,WF) :-
2267		get_wait_flag(2,'MACHINE_INFO',WF,LWF), % TO DO: use number of machines
2268		machine_info2(I,M,Value,LWF).
2269
2270		:- use_module(b_machine_hierarchy,[machine_type/2]).
2271		:- block machine_info2(-,?,?,?), machine_info2(?,-,?,-).
2272		machine_info2(INFO,M,Value,_LWF) :-
2273		(ground(M) -> M = string(MachineName) ; true),
2274		machine_info3(INFO,MachineName,Type),
2275		(M,Value) = (string(MachineName),string(Type)).
2276
2277		:- use_module(b_machine_hierarchy,[machine_type/2]).
2278		:- use_module(extension('probhash/probhash'),[raw_sha_hash/2]).
2279		:- use_module(bmachine,[get_full_b_machine/2]).
2280		machine_info3('TYPE',MachineName,Type) :- !, machine_type(MachineName,Type).
2281		% SHA_HASH
2282		machine_info3(INFO,_,_) :- add_error('MACHINE_INFO','Unknown info field (TYPE recognised): ',INFO),fail.
2283
2284
2285		external_fun_type('INT_TO_HEX',[],[integer,string]).
2286		:- public 'INT_TO_HEX_STRING'/2.
2287		:- block 'INT_TO_HEX_STRING'(-,?).
2288		'INT_TO_HEX_STRING'(int(Int),Res) :-
2289		(Int >= 0 -> Nat=Int ; Nat is -(Int)),
2290		get_hex_codes(Nat,Chars),
2291		(Int >= 0 -> atom_codes(Atom,Chars) ; atom_codes(Atom,[45|Chars])), % "-" = [45]
2292		Res = string(Atom).
2293
2294		% ---------- hex utilities: to do move to tools ?
2295		get_hex_codes(0,Chars) :- !, Chars="0".
2296		get_hex_codes(Nr,Chars) :- get_hex_codes(Nr,[],Chars).
2297
2298		get_hex_codes(0,Acc,R) :- !, R=Acc.
2299		get_hex_codes(Nr,Acc,R) :-
2300		DigNr is Nr mod 16,
2301		get_hex_code(DigNr,Char),
2302		N1 is Nr // 16,
2303		get_hex_codes(N1,[Char|Acc],R).
2304
2305		sha_hash_as_hex_codes(Term,SHAHexCodes) :-
2306		raw_sha_hash(Term,RawListOfBytes),
2307		get_hex_bytes(RawListOfBytes,SHAHexCodes).
2308
2309		get_hex_bytes([],[]).
2310		get_hex_bytes([Byte|T],[C1,C2|HT]) :- get_hex_byte(Byte,C1,C2), get_hex_bytes(T,HT).
2311
2312		get_hex_byte(Byte,C1,C2) :-
2313		N1 is Byte // 16, N2 is Byte mod 16,
2314		get_hex_code(N1,C1), get_hex_code(N2,C2).
2315		get_hex_code(Nr,Digit) :- Nr<10,!, Digit is Nr+48. % "0" = [48]
2316		get_hex_code(Nr,Digit) :- Nr<16,!, Digit is Nr+87. % "A" = [65], "a" = [97]
2317
2318
2319		%-------------------
2320
2321		% returns list of strings for info string such as files, variables,...
2322		external_fun_type('PROJECT_STATISTICS',[],[string,integer]).
2323		expects_waitflag('PROJECT_STATISTICS').
2324		expects_spaninfo('PROJECT_STATISTICS').
2325		:- public 'PROJECT_STATISTICS'/4.
2326		'PROJECT_STATISTICS'(Str,Res,Span,WF) :-
2327		kernel_waitflags:get_wait_flag(10,'PROJECT_STATISTICS',WF,WF10), % will enumerate possible input strings
2328		project_stats1(Str,Res,WF10,Span).
2329
2330		:- use_module(bmachine,[b_machine_statistics/2]).
2331		:- block project_stats1(-,?,-,?).
2332		project_stats1(string(INFO),Res,_,Span) :-
2333		if(b_machine_statistics(INFO,Nr), Res=int(Nr),
2334		add_error('PROJECT_STATISTICS','Unknown info field: ',INFO,Span)).
2335
2336
2337		% returns list of strings for info string such as files, variables,...
2338		external_fun_type('PROJECT_INFO',[],[string,set(string)]).
2339		expects_waitflag('PROJECT_INFO').
2340		expects_spaninfo('PROJECT_INFO').
2341		:- public 'PROJECT_INFO'/4.
2342		'PROJECT_INFO'(Str,Res,Span,WF) :-
2343		kernel_waitflags:get_wait_flag(10,'PROJECT_INFO',WF,WF10), % will enumerate possible input strings
2344		project_info1(Str,Res,WF10,Span).
2345
2346		:- block project_info1(-,?,-,?).
2347		project_info1(string(INFO),Res,_,_Span) :- INFO==help,!,
2348		L = [files, absolute-files, main-file, variables, constants, sets, operations, assertion_labels, invariant_labels],
2349		maplist(make_string,L,SL),
2350		kernel_objects:equal_object(SL,Res).
2351		project_info1(string(INFO),Res,_,Span) :-
2352		if(list_info(INFO,L),
2353		(maplist(make_string,L,SL),
2354		kernel_objects:equal_object(SL,Res)),
2355		(add_error(external_functions,'Illegal argument for PROJECT_INFO or :list (use help to obtain valid arguments) : ',INFO,Span),
2356		fail)).
2357
2358		:- use_module(bmachine).
2359		:- use_module(bsyntaxtree, [get_texpr_ids/2, get_texpr_label/2]).
2360		:- use_module(tools,[get_tail_filename/2]).
2361		list_info(files,TL) :- (b_get_all_used_filenames(L) -> true ; L=[]), maplist(get_tail_filename,L,TL).
2362		list_info('absolute-files',L) :- (b_get_all_used_filenames(L) -> true ; L=[]).
2363		list_info('main-file',L) :- (b_get_main_filename(F) -> get_tail_filename(F,TF),L=[TF] ; L=[]).
2364		list_info('main-machine',L) :- findall(Name,get_full_b_machine(Name,_),L). % gets only the main machine
2365		list_info('sha-hash',[AtomHash]) :-
2366		get_full_b_machine(_,M),
2367		sha_hash_as_hex_codes(M,Hash), atom_codes(AtomHash,Hash).
2368		list_info(variables,L) :- b_get_machine_variables(LT), get_texpr_ids(LT,L).
2369		list_info(constants,L) :- b_get_machine_constants(LT), get_texpr_ids(LT,L).
2370		list_info(sets,L) :- findall(S,b_get_machine_set(S),L).
2371		list_info(operations,L) :- findall(S,b_top_level_operation(S),L).
2372		list_info(assertion_labels,L) :-
2373		findall(ID,(b_get_assertions(all,_,Ass), member(Assertion,Ass),get_texpr_label(Assertion,ID)),L).
2374		list_info(invariant_labels,L) :-
2375		findall(ID,(b_get_invariant_from_machine(C), conjunction_to_list(C,CL),
2376		member(Inv,CL),get_texpr_label(Inv,ID)),L).
2377
2378
2379		make_string(X,Res) :- atom(X),!,Res=string(X).
2380		make_string(X,Res) :- format_to_codes('~w',X,C), atom_codes(Atom,C), Res=string(Atom).
2381
2382		% obtain the source code of an identifier
2383		external_fun_type('SOURCE',[],[string,string]).
2384		:- public 'SOURCE'/2.
2385		'SOURCE'(string(ID),SourceCode) :- source2(ID,SourceCode).
2386		:- block source2(-,?).
2387		source2(ID,SourceCode) :-
2388		source_code_for_identifier(ID,_,_,_OriginStr,_,Source),
2389		translate:translate_bexpression(Source,SC),
2390		SourceCode = string(SC).
2391
2392
2393		% obtain various information about ProB (STRING result)
2394		external_fun_type('PROB_INFO_STR',[],[string,string]).
2395		expects_waitflag('PROB_INFO_STR').
2396		:- assert_must_succeed(external_functions:'PROB_INFO_STR'(string('prob-version'),string(_),_)).
2397		:- public 'PROB_INFO_STR'/3.
2398		% :- block 'PROB_INFO_STR'(-,?). % no block: this way we can via backtracking generate solutions
2399		'PROB_INFO_STR'(Str,Res,WF) :-
2400		kernel_waitflags:get_wait_flag(10,'PROB_INFO_STR',WF,WF10), % will enumerate possible input strings
2401		prob_info1(Str,Res,WF10).
2402
2403		:- block prob_info1(-,?,-).
2404		prob_info1(string(INFO),Res,_) :-
2405		prob_info2(INFO,Str), make_string(Str,Res).
2406
2407		:- use_module(probsrc(tools_strings),[ajoin/2]).
2408		:- use_module(parsercall,[get_parser_version/1, get_java_command_path/1, get_java_fullversion/3]).
2409		:- use_module(version, [version_str/1, revision/1, lastchangeddate/1]).
2410		prob_info2('prob-version',V) :- version_str(V).
2411		prob_info2('parser-version',V) :- get_parser_version(V).
2412		prob_info2('prolog-version',V) :- prolog_flag(version,V).
2413		prob_info2('prob-revision',V) :- revision(V).
2414		prob_info2('prob-last-changed-date',V) :- lastchangeddate(V).
2415		prob_info2('java-version',V) :- get_java_fullversion(Maj,Min,Sfx), ajoin([Maj,'.',Min,'.',Sfx],V).
2416		prob_info2('java-command-path',V) :- get_java_command_path(V).
2417		prob_info2('current-time',V) :- get_info2(time,string(V)). % Maybe we can get rid of GET_INFO ?
2418
2419
2420		% obtain various information about ProB (INTEGER result)
2421		external_fun_type('PROB_STATISTICS',[],[string,integer]).
2422		expects_waitflag('PROB_STATISTICS').
2423		expects_spaninfo('PROB_STATISTICS').
2424		:- public 'PROB_STATISTICS'/4.
2425		'PROB_STATISTICS'(Str,Res,Span,WF) :-
2426		kernel_waitflags:get_wait_flag(10,'PROB_STATISTICS',WF,WF10), % will enumerate possible input strings
2427		prob_info_int1(Str,Res,Span,WF10).
2428
2429		% old name of function:
2430		:- public 'PROB_INFO_INT'/4.
2431		'PROB_INFO_INT'(Str,Res,Span,WF) :- 'PROB_STATISTICS'(Str,Res,Span,WF).
2432
2433		:- block prob_info_int1(-,?,?,-).
2434		prob_info_int1(string(INFO),Res,Span,_) :-
2435		if(prob_info_int1(INFO,I), Res=int(I),
2436		add_error('PROB_STATISTICS','Unknown info field: ',INFO,Span)).
2437
2438		:- use_module(state_space,[current_state_id/1, get_state_space_stats/3]).
2439		prob_info_int1('current-state-id',StateIDNr) :- current_state_id(ID),convert_id_to_nr(ID,StateIDNr).
2440		prob_info_int1('states',NrNodes) :- get_state_space_stats(NrNodes,_,_).
2441		prob_info_int1('transitions',NrTransitions) :- get_state_space_stats(_,NrTransitions,_).
2442		prob_info_int1('processed-states',ProcessedNodes) :- get_state_space_stats(_,_,ProcessedNodes).
2443		prob_info_int1('now-timestamp',N) :- now(N). % provide UNIX timesstamp
2444		prob_info_int1('prolog-runtime',V) :- statistics(runtime,[V,_]).
2445		prob_info_int1('prolog-walltime',V) :- statistics(walltime,[V,_]).
2446		prob_info_int1('prolog-memory-bytes-used',V) :- statistics(memory_used,V).
2447		prob_info_int1('prolog-memory-bytes-free',V) :- statistics(memory_free,V).
2448		prob_info_int1('prolog-global-stack-bytes-used',V) :- statistics(global_stack_used,V).
2449		prob_info_int1('prolog-local-stack-bytes-used',V) :- statistics(local_stack_used,V).
2450		%prob_info_int1('prolog-global-stack-bytes-free',V) :- statistics(global_stack_free,V).
2451		%prob_info_int1('prolog-local-stack-bytes-free',V) :- statistics(local_stack_free,V).
2452		prob_info_int1('prolog-trail-bytes-used',V) :- statistics(trail_used,V).
2453		prob_info_int1('prolog-choice-bytes-used',V) :- statistics(choice_used,V).
2454		prob_info_int1('prolog-atoms-bytes-used',V) :- statistics(atoms_used,V).
2455		prob_info_int1('prolog-atoms-nb-used',V) :- statistics(atoms_nbused,V).
2456		prob_info_int1('prolog-gc-count',V) :- statistics(gc_count,V).
2457		prob_info_int1('prolog-gc-time',V) :- statistics(gc_time,V).
2458
2459
2460		% obtain various information about bvisual2 Formulas
2461		external_fun_type('FORMULA_INFOS',[],[string,seq(string)]).
2462		expects_waitflag('FORMULA_INFOS').
2463		:- public 'FORMULA_INFOS'/3.
2464		'FORMULA_INFOS'(Str,Res,WF) :-
2465		kernel_waitflags:get_wait_flag(10,'FORMULA_INFOS',WF,WF10), % will enumerate possible input strings
2466		formula_info(Str,_,Res,_,WF10).
2467		external_fun_type('FORMULA_VALUES',[],[string,seq(string)]).
2468		expects_waitflag('FORMULA_VALUES').
2469		:- public 'FORMULA_VALUES'/3.
2470		'FORMULA_VALUES'(Str,Res,WF) :-
2471		kernel_waitflags:get_wait_flag(10,'FORMULA_VALUES',WF,WF10), % will enumerate possible input strings
2472		formula_info(Str,_,_,Res,WF10).
2473
2474		:- use_module(bvisual2,[bv_get_top_level_formula/4, bv_value_to_atom/2]).
2475
2476		:- block formula_info(-,?,?,?,-).
2477		formula_info(string(TopLevelCategory),CatTextRes,LabelRes,ValuesRes,_) :-
2478		bv_get_top_level_formula(TopLevelCategory,CatText,Labels,Values),
2479		CatTextRes = string(CatText),
2480		maplist(make_string,Labels,LS),
2481		convert_set_to_seq(LS,LabelRes),
2482		maplist(make_value,Values,LV),
2483		convert_set_to_seq(LV,ValuesRes).
2484
2485		make_value(V,string(A)) :- bv_value_to_atom(V,A).
2486		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2487
2488
2489		% --------------------------
2490
2491		:- use_module(hit_profiler,[add_hit/2, add_hit_if_not_covered/2, reset_profiler/0,
2492		get_profile_statistics/2, profile_functor/1]). %profiler:profile_statistics.
2493
2494		:- public 'GET_PROFILE_STATISTICS'/3.
2495		is_not_declarative('GET_PROFILE_STATISTICS').
2496		:- block 'GET_PROFILE_STATISTICS'(-,?,?).
2497		'GET_PROFILE_STATISTICS'(string(PP),_DummyType,Res) :- % DummyType is just there for typing purposes
2498		if(profile_functor(PP),
2499		(get_profile_statistics(PP,Hits),
2500		maplist(translate_hit_to_b,Hits,List)),
2501		List = []),
2502		equal_object_optimized(List,Res, 'GET_PROFILE_STATISTICS').
2503		%equal_object(List,Res,'GET_PROFILE_STATISTICS'), print(res(Res)),nl.
2504
2505		translate_hit_to_b(hit(Arg,Nr),(Arg,int(Nr))).
2506
2507		:- public 'GET_PROFILE_POINTS'/1.
2508		'GET_PROFILE_POINTS'(Res) :- findall(string(S),profile_functor(S),List),
2509		equal_object_optimized(List,Res,'PROFILE_POINT').
2510
2511		expects_spaninfo('PROFILE').
2512		:- public 'PROFILE'/5.
2513		:- block 'PROFILE'(-,?,?,?,?), 'PROFILE'(?,-,?,?,?). %, 'PROFILE'(?,-,?,?,?).
2514		'PROFILE'(string(PP),Count,Value,ValueRes,SpanInfo) :-
2515		add_profile_exf_hit(Value,PP,SpanInfo,Count),
2516		equal_object(Value,ValueRes,'PROFILE').
2517
2518		:- block add_profile_exf_hit(-,?,?,?), add_profile_exf_hit(?,-,?,?).
2519		add_profile_exf_hit(pred_true,PP,SpanInfo,Count) :- !, add_value_hit(Count,pred_true,PP,SpanInfo).
2520		add_profile_exf_hit(pred_false,PP,SpanInfo,Count) :- !, add_value_hit(Count,pred_false,PP,SpanInfo).
2521		add_profile_exf_hit(int(X),PP,SpanInfo,Count) :- !, add_int_hit(X,PP,SpanInfo,Count).
2522		add_profile_exf_hit(string(X),PP,SpanInfo,Count) :- !, add_string_hit(X,PP,SpanInfo,Count).
2523		add_profile_exf_hit(Value,PP,SpanInfo,Count) :- when(ground(Value), add_complex_hit(Value,PP,SpanInfo,Count)).
2524
2525		add_complex_hit(Value,PP,SpanInfo,Count) :- print(PP), print(' : '), translate:print_bvalue(Value),nl,
2526		add_value_hit(Count,Value,PP,SpanInfo).
2527
2528		:- block add_int_hit(-,?,?,?).
2529		add_int_hit(X,PP,SpanInfo,Count) :- add_value_hit(Count,int(X),PP,SpanInfo).
2530		:- block add_string_hit(-,?,?,?).
2531		add_string_hit(X,PP,SpanInfo,Count) :- add_value_hit(Count,string(X),PP,SpanInfo).
2532
2533		add_value_hit(pred_true,Val,PP,_) :- add_hit(PP,Val).
2534		add_value_hit(pred_false,Val,PP,_) :- add_hit_if_not_covered(PP,Val).
2535
2536		% -------------------
2537
2538		:- use_module(memoization,[get_registered_function/2]).
2539
2540		expects_spaninfo('MEMOIZE_STORED_FUNCTION').
2541		:- public 'MEMOIZE_STORED_FUNCTION'/3.
2542		:- block 'MEMOIZE_STORED_FUNCTION'(-,?,?).
2543		'MEMOIZE_STORED_FUNCTION'(int(MemoID),Res,Span) :- memoize_get_aux(MemoID,Res,Span).
2544
2545		:- block memoize_get_aux(-,?,?).
2546		memoize_get_aux(MemoID,Res,Span) :-
2547		if(get_registered_function(MemoID,RV),
2548		kernel_objects:equal_object(Res,RV),
2549		add_error(external_functions,'Function ID not registered:',MemoID,Span)).
2550
2551
2552		% -------------------
2553		% a few ugraphs (unweighted graphs) utilities:
2554
2555		% an alternate implementation of closure1
2556		expects_spaninfo('CLOSURE1').
2557		external_fun_type('CLOSURE1',[X],[set(couple(X,X)),set(couple(X,X))]).
2558		:- public 'CLOSURE1'/3.
2559		:- block 'CLOSURE1'(-,?,?).
2560		'CLOSURE1'([],Res,_) :- !, kernel_objects:equal_object(Res,[]).
2561		'CLOSURE1'(avl_set(A),Res,_) :- !, closure1_for_avl_set(A,R), kernel_objects:equal_object_optimized(R,Res).
2562		'CLOSURE1'(A,Res,Span) :- ground_value_check(A,Gr), closure1_gr(A,Gr,Res,Span).
2563
2564		closure1_gr(Set,_,Res,Span) :- convert_to_avl(Set,AVL),!, 'CLOSURE1'(AVL,Res,Span).
2565		closure1_gr(Set,_,_,Span) :-
2566		add_error(external_functions,'Cannot convert CLOSURE1 argument to set: ',Set,Span).
2567
2568		% compute strongly connected components
2569		expects_spaninfo('SCCS').
2570		external_fun_type('SCCS',[X],[set(couple(X,X)),set(set(couple(X)))]).
2571		:- public 'SCCS'/3.
2572		:- block 'SCCS'(-,?,?).
2573		'SCCS'([],Res,_) :- !, kernel_objects:equal_object(Res,[]).
2574		'SCCS'(avl_set(A),Res,_) :- !, sccs_for_avl_set(A,R), kernel_objects:equal_object_optimized(R,Res).
2575		'SCCS'(A,Res,Span) :- ground_value_check(A,Gr), sccs_gr(A,Gr,Res,Span).
2576
2577		sccs_gr(Set,_,Res,Span) :- convert_to_avl(Set,AVL),!, 'SCCS'(AVL,Res,Span).
2578		sccs_gr(Set,_,_,Span) :-
2579		add_error(external_functions,'Cannot convert SCCS argument to set: ',Set,Span).
2580
2581		:- use_module(probsrc(avl_ugraphs),[avl_transitive_closure/2, avl_scc_sets/2]).
2582		closure1_for_avl_set(A,Res) :-
2583		avl_transitive_closure(A,TC),
2584		construct_avl_set(TC,Res).
2585		sccs_for_avl_set(A,Res) :-
2586		avl_scc_sets(A,TC),
2587		construct_avl_set(TC,Res).
2588		construct_avl_set(Avl,Res) :- empty_avl(Avl) -> Res = [] ; Res = avl_set(Avl).
2589		% -------------------
2590
2591		reset_kodkod :-
2592		true. %retractall(kodkod_pred(_,_)).
2593
2594		%:- use_module(probsrc(bsyntaxtree), [b_compute_expression/5]).
2595
2596		% KODKOD(ProblemID, LocalIDsOfPredicate, WaitToBeGroundBeforePosting, PredicateAsBooleanFunction)
2597		% EXTERNAL_PREDICATE_KODKOD(T1,T2) == INTEGER*T1*T2*BOOL;
2598		%:- dynamic kodkod_pred/2. % now stored as attribute in WF store
2599		do_not_evaluate_args('KODKOD').
2600		expects_unevaluated_args('KODKOD').
2601		expects_waitflag('KODKOD').
2602		expects_state('KODKOD').
2603
2604		:- use_module(bsyntaxtree,[create_negation/2]).
2605		:- use_module(b_compiler,[b_optimize/6]).
2606		:- use_module(b_interpreter,[b_compute_expression/5]).
2607		:- public 'KODKOD'/5.
2608		:- block 'KODKOD'(-,?,?,?,?).
2609		'KODKOD'(PredRes,LocalState,State,UnevaluatedArgs,WF) :-
2610		UnevaluatedArgs = [TID,IDEXPR,WAITIDEXPR,UEA],
2611		get_integer(TID,ID),
2612		construct_predicate(UEA,KPredicate),
2613		(PredRes == pred_false -> create_negation(KPredicate,Predicate) ; Predicate=KPredicate),
2614		must_get_identifiers(IDEXPR,TIdentifiers),
2615		get_texpr_ids(TIdentifiers,Ids),
2616		b_interpreter:b_compute_expression(WAITIDEXPR,LocalState,State,WaitVal,WF),
2617		when(ground(WaitVal),
2618		( %print(compile_for(ID,Ids)),nl,
2619		b_optimize(Predicate,Ids,LocalState,State,CPredicate,WF),
2620		(debug:debug_mode(off) -> true
2621		; format('STORING FOR KODKOD ~w (~w): ',[ID,PredRes]), translate:print_bexpr(CPredicate),nl),
2622		kernel_waitflags:my_add_predicate_to_kodkod(WF,ID,CPredicate),
2623		%assert(kodkod_pred(ID,CPredicate)), % TO DO: attach to WF Store !; assert will break Prolog variable links !
2624		% TO DO: retract upon backtracking + store negation if PredRes = pred_false
2625		PredRes=pred_true
2626		)).
2627
2628		get_integer(b(V,_,_),I) :- get_integer2(V,I).
2629		get_integer2(integer(V),V).
2630		get_integer2(value(IV),V) :- nonvar(IV), IV=int(V), number(V).
2631
2632		:- use_module(probsrc(bsyntaxtree), [safe_create_texpr/3]).
2633		construct_predicate(b(convert_bool(P),_,_),Res) :- !, Res=P.
2634		construct_predicate(BoolExpr,Res) :-
2635		safe_create_texpr(equal(BoolExpr,b(boolean_true,boolean,[])),pred,Res).
2636
2637		:- use_module('kodkod/kodkod', [replace_by_kodkod/3]).
2638		% EXTERNAL_PREDICATE_KODKOD_SOLVE(T1,T2) == INTEGER*T1*T2;
2639		expects_unevaluated_args('KODKOD_SOLVE').
2640		expects_waitflag('KODKOD_SOLVE').
2641		expects_state('KODKOD_SOLVE').
2642		:- public 'KODKOD_SOLVE'/8.
2643		:- block 'KODKOD_SOLVE'(-,?,?,?,?,?,?,?).
2644		'KODKOD_SOLVE'(int(ID),Ids,WaitIds,PredRes,LocalState,State,UEA,WF) :-
2645		when(ground(WaitIds),
2646		kodkod_solve_aux(ID,Ids,WaitIds,PredRes,LocalState,State,UEA,WF)).
2647
2648		:- use_module(library(ordsets),[ord_subtract/3]).
2649		kodkod_solve_aux(ID,Ids,_WaitIds,PredRes,LocalState,State,UEA,WF) :-
2650		%print(trigger_SOLVE(_WaitIds)),nl,
2651		get_wait_flag(2,'KODKOD_SOLVE',WF,LWF), % give other co-routines chance to fire
2652		kodkod_solve_aux2(ID,Ids,PredRes,LocalState,State,UEA,WF,LWF).
2653
2654		:- block kodkod_solve_aux2(?,?,?,?,?,?,?,-).
2655		kodkod_solve_aux2(ID,_,PredRes,LocalState,State,[_,IDEXPR,WAITIDEXPR],WF,_) :-
2656		%print(ls(LocalState,State)),nl,
2657		%findall(P,kodkod_pred(ID,P),Ps), % TO DO: obtain from WF Store
2658		kernel_waitflags:my_get_kodkod_predicates(WF,ID,Ps),
2659		length(Ps,Len),
2660		reverse(Ps,RPs), % we reverse Ps to put predicates in same order they were added by KODKOD / seems to influence analysis time
2661		conjunct_predicates(RPs,Predicate),
2662		%translate:print_bexpr(Predicate),nl,
2663		must_get_identifiers(IDEXPR,TIdentifiers),
2664		get_texpr_ids(TIdentifiers,Ids),
2665		((get_identifiers(WAITIDEXPR,TWaitIds,[]), get_texpr_ids(TWaitIds,WaitIds),
2666		sort(WaitIds,SWIds),
2667		formatsilent('KODKOD_SOLVE Problem ~w (~w conjuncts), Identifiers: ~w, Waiting for ~w~n',[ID,Len,Ids,SWIds]),
2668		sort(Ids,SIds),
2669		ord_subtract(SIds,SWIds,IdsToSolve))
2670		-> b_optimize(Predicate,IdsToSolve,LocalState,State,CPredicate,WF), % inline known values
2671		(silent_mode(on) -> true ; print('compiled: '),translate:print_bexpr(CPredicate),nl,nl)
2672		; CPredicate=Predicate
2673		),
2674		(replace_by_kodkod(TIdentifiers,CPredicate,NewPredicate)
2675		-> (silent_mode(on) -> true ; print('AFTER KODKOD: '),translate:print_bexpr(NewPredicate),nl),
2676		b_interpreter:b_test_boolean_expression(NewPredicate,LocalState,State,WF)
2677		; print('KODKOD cannot be applied'),nl,
2678		b_interpreter:b_test_boolean_expression(CPredicate,LocalState,State,WF)
2679		),
2680		PredRes=pred_true.
2681
2682		must_get_identifiers(TExpr,Res) :-
2683		(get_identifiers(TExpr,Ids,[]) -> Res=Ids
2684		; add_error('KODKOD_SOLVE','Could not get identifiers: ',TExpr),fail).
2685
2686		get_identifiers(b(couple(A1,A2),_,_)) --> !, get_identifiers(A1), get_identifiers(A2).
2687		get_identifiers(b(identifier(ID),T,I)) --> [b(identifier(ID),T,I)].
2688		get_identifiers(b(integer(_),_,_)) --> []. % to do: accept other ground values; in case they are compiled
2689		get_identifiers(b(value(_),_,_)) --> []. % identifier has already been compiled
2690
2691
2692		% -------------------
2693		do_not_evaluate_args('SATSOLVER').
2694		expects_unevaluated_args('SATSOLVER').
2695		expects_waitflag('SATSOLVER').
2696		expects_state('SATSOLVER').
2697
2698		:- public 'SATSOLVER'/5.
2699		:- block 'SATSOLVER'(-,?,?,?,?).
2700		'SATSOLVER'(PredRes,LocalState,State,UnevaluatedArgs,WF) :-
2701		UnevaluatedArgs = [TID,IDEXPR,WAITIDEXPR,UEA],
2702		get_integer(TID,ID),
2703		construct_predicate(UEA,KPredicate),
2704		(PredRes == pred_false -> create_negation(KPredicate,Predicate) ; Predicate=KPredicate),
2705		must_get_identifiers(IDEXPR,TIdentifiers),
2706		get_texpr_ids(TIdentifiers,Ids),
2707		b_interpreter:b_compute_expression(WAITIDEXPR,LocalState,State,WaitVal,WF),
2708		when(ground(WaitVal),
2709		( %print(compile_for(ID,Ids)),nl,
2710		b_optimize(Predicate,Ids,LocalState,State,CPredicate,WF),
2711		(debug:debug_mode(off) -> true
2712		; format('STORING FOR SATSOLVER ~w (~w): ',[ID,PredRes]), translate:print_bexpr(CPredicate),nl),
2713		kernel_waitflags:my_add_predicate_to_satsolver(WF,ID,CPredicate),
2714		% TO DO: retract upon backtracking + store negation if PredRes = pred_false
2715		PredRes=pred_true
2716		)).
2717
2718		expects_unevaluated_args('SATSOLVER_SOLVE').
2719		expects_waitflag('SATSOLVER_SOLVE').
2720		expects_state('SATSOLVER_SOLVE').
2721		:- public 'SATSOLVER_SOLVE'/8.
2722		:- block 'SATSOLVER_SOLVE'(-,?,?,?,?,?,?,?).
2723		'SATSOLVER_SOLVE'(int(ID),Ids,WaitIds,PredRes,LocalState,State,UEA,WF) :-
2724		when(ground(WaitIds),
2725		satsolver_solve_aux(ID,Ids,WaitIds,PredRes,LocalState,State,UEA,WF)).
2726
2727		:- use_module(library(ordsets),[ord_subtract/3]).
2728		satsolver_solve_aux(ID,Ids,_WaitIds,PredRes,LocalState,State,UEA,WF) :-
2729		%print(trigger_SOLVE(_WaitIds)),nl,
2730		get_wait_flag(2,'SATSOLVER_SOLVE',WF,LWF), % give other co-routines chance to fire
2731		satsolver_solve_aux2(ID,Ids,PredRes,LocalState,State,UEA,WF,LWF).
2732
2733		:- use_module(extension('satsolver/satsolver'), [b_sat/2]).
2734
2735		:- block satsolver_solve_aux2(?,?,?,?,?,?,?,-).
2736		satsolver_solve_aux2(ID,_,PredRes,LocalState,State,[_,IDEXPR,WAITIDEXPR],WF,_) :-
2737		print('SATSOLVER_SOLVE:'),nl,
2738		kernel_waitflags:my_get_satsolver_predicates(WF,ID,Ps),
2739		nl,print(got_predicates(ID)),nl,
2740		length(Ps,Len), print(len(Len)),nl,
2741		reverse(Ps,RPs), % we reverse Ps to put predicates in same order they were added by KODKOD / seems to influence analysis time
2742		conjunct_predicates(RPs,Predicate),
2743		translate:print_bexpr(Predicate),nl,
2744		must_get_identifiers(IDEXPR,TIdentifiers),
2745		get_texpr_ids(TIdentifiers,Ids),
2746		((get_identifiers(WAITIDEXPR,TWaitIds,[]), get_texpr_ids(TWaitIds,WaitIds),
2747		sort(WaitIds,SWIds),
2748		formatsilent('Sat Solver identifiers: ~w ; waiting for ~w~n',[Ids,SWIds]),
2749		sort(Ids,SIds),
2750		ord_subtract(SIds,SWIds,IdsToSolve))
2751		-> b_optimize(Predicate,IdsToSolve,LocalState,State,CPredicate,WF), % inline known values
2752		(silent_mode(on) -> true
2753		; print('compiled: '),translate:print_bexpr(CPredicate),nl,nl)
2754		; CPredicate=Predicate
2755		),
2756		(b_sat(CPredicate,State)
2757		% TODO: catch errors if b_sat fails!
2758		%-> true
2759		% ; print('Calling SAT solver failed'),nl,
2760		% b_interpreter:b_test_boolean_expression(CPredicate,LocalState,State,WF)
2761		),
2762		PredRes=pred_true.
2763		% -------------------
2764
2765
2766		expects_waitflag('UNSAT_CORE'). % WF not used at the moment
2767		expects_spaninfo('UNSAT_CORE').
2768		:- public 'UNSAT_CORE'/5.
2769		% EXTERNAL_FUNCTION_UNSAT_CORE(T) == (POW(T)-->BOOL)*POW(T) --> POW(T);
2770		% UNSAT_CORE(Fun,Set) == Set
2771		% example: UNSAT_CORE(f,0..200) = {2} with f = %x.(x:POW(INTEGER)|bool(x /\ 1..2={}))
2772		'UNSAT_CORE'(FunToBool,Set,ValueRes,SpanInfo,WF) :-
2773		'UNSAT_CORE_ACC'(FunToBool,Set,[],ValueRes,SpanInfo,WF).
2774
2775
2776		expects_waitflag('UNSAT_CORE_ACC'). % WF not used at the moment
2777		expects_spaninfo('UNSAT_CORE_ACC').
2778		% EXTERNAL_FUNCTION_UNSAT_CORE_ACC(T) == (POW(T)-->BOOL)*POW(T)*POW(T) --> POW(T);
2779		% UNSAT_CORE_ACC(Fun,Set,Acc) == Set\/Acc;
2780		% example: UNSAT_CORE_ACC(f,0..200,{}) = {2} & f = %x.(x:POW(INTEGER)|bool(x /\ 1..2={}))
2781		% provides a way to initialise the accumulator of the unsat core computation
2782		'UNSAT_CORE_ACC'(FunToBool,Set,Acc,ValueRes,SpanInfo,WF) :-
2783		custom_explicit_sets:expand_custom_set_to_list_wf(Set,ESet,_,compute_apply_true,WF),
2784		custom_explicit_sets:expand_custom_set_to_list_wf(Acc,EAcc,_,compute_apply_true,WF),
2785		debug_println(9,computing_unsat_core(ESet,EAcc)),
2786		when(ground((FunToBool,ESet)), compute_unsat_core(ESet,FunToBool,no_time_out,EAcc,ValueRes,SpanInfo,WF)).
2787
2788		% EXTERNAL_FUNCTION_UNSAT_CORE_ACC_TIMEOUT(T) == (POW(T)-->BOOL)*POW(T)*POW(T)*INTEGER --> POW(T);
2789		% UNSAT_CORE_ACC_TIMEOUT(Fun,Set,Acc,TO) == Set\/Acc;
2790		% example: UNSAT_CORE_ACC_TIMEOUT(f,0..200,{},100) = {2} & f = %x.(x:POW(INTEGER)|bool(x /\ 1..2={}))
2791		expects_waitflag('UNSAT_CORE_ACC_TIMEOUT'). % WF not used at the moment
2792		expects_spaninfo('UNSAT_CORE_ACC_TIMEOUT').
2793		:- public 'UNSAT_CORE_ACC_TIMEOUT'/7.
2794		'UNSAT_CORE_ACC_TIMEOUT'(FunToBool,Set,Acc,int(TimeOut),ValueRes,SpanInfo,WF) :-
2795		custom_explicit_sets:expand_custom_set_to_list_wf(Set,ESet,_,compute_apply_true,WF),
2796		custom_explicit_sets:expand_custom_set_to_list_wf(Acc,EAcc,_,compute_apply_true,WF),
2797		debug_println(9,computing_unsat_core(ESet,EAcc)),
2798		when(ground((FunToBool,ESet,TimeOut)), compute_unsat_core(ESet,FunToBool,TimeOut,EAcc,ValueRes,SpanInfo,WF)).
2799
2800		compute_unsat_core([],_FunToBool,_TimeOut,Core,Result,_SpanInfo,_WF) :- equal_object(Result,Core).
2801		compute_unsat_core([H|T],FunToBool,TimeOut,Core,Result,SpanInfo,WF) :-
2802		debug_println(9,trying_to_remove(H,core(Core))),
2803		append(Core,T,CoreT),
2804		if(compute_apply_true_timeout(TimeOut,FunToBool,CoreT,SpanInfo),
2805		compute_unsat_core(T,FunToBool,TimeOut,[H|Core],Result,SpanInfo,WF), % we found a solution, H is needed in core
2806		compute_unsat_core(T,FunToBool,TimeOut, Core, Result,SpanInfo,WF) % contradiction also exists without H
2807		).
2808
2809		:- use_module(library(timeout)).
2810		compute_apply_true_timeout(no_time_out,FunToBool,CoreT,SpanInfo) :- !,
2811		compute_apply_true(FunToBool,CoreT,SpanInfo).
2812		compute_apply_true_timeout(TO,FunToBool,CoreT,SpanInfo) :-
2813		time_out(compute_apply_true(FunToBool,CoreT,SpanInfo), TO, TORes),
2814		(TORes == success -> true ,format(user_output,'~nSUCCESS~n~n',[])
2815		; format(user_output,'~nTIME-OUT: ~w~n~n',[TORes]),fail). % treat time-out like failure
2816
2817		compute_apply_true(FunToBool,CoreT,SpanInfo) :- init_wait_flags(WF1),
2818		bsets_clp:apply_to(FunToBool,CoreT,pred_true,SpanInfo,WF1), % TO DO: also pass function type
2819		ground_wait_flags(WF1).
2820
2821		expects_waitflag('MAX_SAT').
2822		expects_spaninfo('MAX_SAT').
2823		:- public 'MAX_SAT'/5.
2824		% EXTERNAL_FUNCTION_MAX_SAT(T) == (POW(T)-->BOOL)*POW(T) --> POW(T);
2825		% MAX_SAT(Fun,Set) == Set;
2826		% example: MAX_SAT(f,0..3) = {0,3} & f = %x.(x:POW(INTEGER)|bool(x /\ 1..2={}))
2827
2828		'MAX_SAT'(FunToBool,Set,ValueRes,SpanInfo,WF) :-
2829		custom_explicit_sets:expand_custom_set_to_list_wf(Set,ESet,_,compute_apply_true,WF),
2830		debug_println(9,computing_unsat_core(ESet)),
2831		when(ground((FunToBool,ESet)), compute_maxsat_ground(ESet,FunToBool,ValueRes,SpanInfo,WF)).
2832
2833		compute_maxsat_ground(ESet,FunToBool,ValueRes,SpanInfo,WF) :-
2834		debug_println(9,computing_maxsat(ESet)), %nl,reset_walltime,
2835		get_wait_flag(1,'MAX_SAT',WF,LWF), % avoid computing straightaway in case pending co-routines fail; not really sure it is needed
2836		when(nonvar(LWF),compute_maxsat(ESet,FunToBool,[],ValueRes,SpanInfo,WF)).
2837		compute_maxsat([],_FunToBool,Core,Result,_SpanInfo,_WF) :- equal_object(Result,Core).
2838		compute_maxsat([H|T],FunToBool,Core,Result,SpanInfo,WF) :-
2839		debug_println(9,trying_to_add(H,core(Core))),
2840		%nl,nl,nl,print(maxsat(H,Core)),nl, print_walltime(user_output),nl,
2841		if(compute_apply_true(FunToBool,[H|Core],SpanInfo),
2842		compute_maxsat(T,FunToBool,[H|Core],Result,SpanInfo,WF),
2843		compute_maxsat(T,FunToBool, Core, Result,SpanInfo,WF) % contradiction also exists without H
2844		).
2845
2846		:- use_module(clpfd_interface,[clpfd_domain/3, clpfd_inrange/3, clpfd_size/2, clpfd_eq/2]).
2847		expects_waitflag('MAXIMIZE_EXPR').
2848		expects_spaninfo('MAXIMIZE_EXPR').
2849		:- public 'MAXIMIZE_EXPR'/4.
2850		'MAXIMIZE_EXPR'(int(X),int(X),Span,WF) :-
2851		get_wait_flag1(WF,WF1),
2852		maximize_expr_wf(WF1,X,Span).
2853		:- block maximize_expr_wf(-,?,?).
2854		maximize_expr_wf(_WF,X,_Span) :-
2855		clpfd_size(X,Size), Size \= sup,
2856		clpfd_domain(X,Min,Max),
2857		Mid is round((Min + Max)/2),
2858		maximize_expr_wf(Min,Mid,Max,X).
2859		maximize_expr_wf(_,_,Span) :-
2860		add_error(external_functions,'MAXIMIZE_EXPR / MINIMIZE_EXPR called on unbounded expression',Span),
2861		fail.
2862		maximize_expr_wf(X,X,X,X).
2863		maximize_expr_wf(_Min,Mid,Max,X) :-
2864		clpfd_inrange(X,Mid,Max), !,
2865		NMid is round((Mid+Max)/2),
2866		maximize_expr_wf(Mid,NMid,Max,X).
2867		maximize_expr_wf(Min,Mid,_Max,X) :-
2868		clpfd_inrange(X,Min,Mid), !,
2869		NMid is round((Min+Mid)/2),
2870		maximize_expr_wf(Min,NMid,Mid,X).
2871
2872		expects_waitflag('MINIMIZE_EXPR').
2873		expects_spaninfo('MINIMIZE_EXPR').
2874		:- public 'MINIMIZE_EXPR'/4.
2875		'MINIMIZE_EXPR'(int(X),int(X),Span,WF) :-
2876		clpfd_eq(-X,MaxVar),
2877		'MAXIMIZE_EXPR'(int(MaxVar),int(MaxVar),Span,WF).
2878
2879		:- use_module(kernel_tools,[bexpr_variables/2]).
2880		% maximize is actually quite similar to CHOOSE; but it will choose maximum and use special algorithm for closures
2881		expects_waitflag('MAXIMIZE').
2882		expects_spaninfo('MAXIMIZE').
2883		:- public 'MAXIMIZE'/4.
2884		:- block 'MAXIMIZE'(-,?,?,?).
2885		'MAXIMIZE'([],_,Span,WF) :- !,
2886		add_wd_error_span('MAXIMIZE applied to empty set: ',[],Span,WF).
2887		'MAXIMIZE'(avl_set(A),H,_,_) :- !, avl_max(A,Max),kernel_objects:equal_object(H,Max).
2888		'MAXIMIZE'(closure(P,T,Body),FunValue,SpanInfo,WF) :- !,
2889		kernel_tools:bexpr_variables(Body,ClosureWaitVars),
2890		print(wait_maximize(P,ClosureWaitVars)),nl,
2891		when(ground(ClosureWaitVars),maximize_closure(P,T,Body,FunValue,SpanInfo,WF)).
2892		'MAXIMIZE'([H|T],C,Span,WF) :- !,
2893		when(ground([H|T]),
2894		(convert_to_avl([H|T],AVL) -> 'MAXIMIZE'(AVL,C,Span,WF)
2895		; add_wd_error_span('Cannot determine maximum element for MAXIMIZE: ',[H|T],Span,WF),
2896		kernel_objects:equal_object(C,H))
2897		).
2898		'MAXIMIZE'(_,_,SpanInfo,_WF) :-
2899		add_error(external_functions,'MAXIMIZE requires set of values',SpanInfo),
2900		fail.
2901
2902		maximize_closure(Parameters,ParameterTypes,ClosureBody,FunValue,_SpanInfo,WF) :-
2903		debug_println(maximizing(Parameters)),
2904		length(Parameters,Len), length(ParValues,Len),
2905		test_closure(Parameters,ParameterTypes,ClosureBody,ParValues),
2906		debug_println(found_initial_solution(ParValues)),
2907		!,
2908		maximize_closure2(Parameters,ParameterTypes,ClosureBody,ParValues,FunValue,WF).
2909		maximize_closure(_Parameters,_ParameterTypes,_ClosureBody,_FunValue,SpanInfo,_WF) :-
2910		add_error(external_functions,'MAXIMIZE: could not find solution for set comprehension',SpanInfo),
2911		fail.
2912
2913		maximize_closure2(Parameters,ParameterTypes,ClosureBody,PrevSol,FunValue,WF) :-
2914		Parameters=[PMax|_], ParameterTypes=[T1|_],
2915		PrevSol = [ PrevVal | _],
2916		print(trying_to_improve_upon(PrevVal,PMax)),nl,
2917		better_sol_pred(PMax,T1,PrevVal,Better), translate:print_bexpr(Better),nl,
2918		bsyntaxtree:conjunct_predicates([Better,ClosureBody],NewBody),
2919		length(Parameters,Len), length(NewParValues,Len),
2920		test_closure(Parameters,ParameterTypes,NewBody,NewParValues),
2921		debug_println(found_better_solution(NewParValues)),
2922		!,
2923		maximize_closure2(Parameters,ParameterTypes,ClosureBody,NewParValues,FunValue,WF).
2924		maximize_closure2(_Parameters,_ParameterTypes,_ClosureBody,PrevSol,FunValue,_WF) :-
2925		print(cannot_improve),nl,
2926		tools:convert_list_into_pairs(PrevSol,ParTuple),
2927		kernel_objects:equal_object(ParTuple,FunValue).
2928
2929		test_closure(Parameters,ParameterTypes,Body,ParValues) :-
2930		kodkod:apply_kodkod(Parameters,ParameterTypes,Body,Body2),
2931		custom_explicit_sets:b_test_closure(Parameters,ParameterTypes,Body2,ParValues,positive,no_wf_available). % positive instead of all_solutions
2932
2933		% generate predicate for better solution; % TO DO: support MINIMIZE by inverting args
2934		better_sol_pred(PMax,integer,PrevVal,Better) :- !,
2935		Better = b(less(b(value(PrevVal),integer,[]),b(identifier(PMax),integer,[])),pred,[]).
2936		better_sol_pred(PMax,set(T1),PrevVal,Better) :- !,
2937		% WARNING: for sets we will only find one maximum, not all due to the cuts in maximize_closure(2) above
2938		Better = b(strict_subset(b(value(PrevVal),set(T1),[]),b(identifier(PMax),set(T1),[])),pred,[]).
2939		better_sol_pred(PMax,Type,_Val,_) :-
2940		add_error(external_functions,'MAXIMIZE requires first argument of set comprehension to be integer or set; cannot optimize: ',PMax:Type),fail.
2941
2942		% ----------------------------------
2943
2944		expects_spaninfo('READ_XML').
2945		:- public 'READ_XML'/3.
2946		:- block 'READ_XML'(-,?,?).
2947		'READ_XML'(string(File),Res,Span) :-
2948		read_xml(File,auto,Res,Span).
2949
2950		%expects_spaninfo('READ_XML'). both versions expect span info
2951		:- public 'READ_XML'/4.
2952		:- block 'READ_XML'(-,?,?,?),'READ_XML'(?,-,?,?).
2953		'READ_XML'(string(File),string(Encoding),Res,Span) :-
2954		read_xml(File,Encoding,Res,Span).
2955
2956		% EXTERNAL_FUNCTION_READ_XML == STRING --> seq(XML_ELement_Type);
2957		% with XML_ELement_Type == struct( recId: NATURAL1, pId:NATURAL, element:STRING, attributes: STRING +-> STRING, meta: STRING +-> STRING );
2958
2959		:- use_module(tools, [read_string_from_file/3]).
2960		:- use_module(xml2b, [convert_xml_to_b/2]).
2961		:- use_module(preferences, [is_of_type/2]).
2962		:- block read_xml(-,?,?,?), read_xml(?,-,?,?).
2963		read_xml(File,EncodingPref,Res,Span) :-
2964		(is_of_type(EncodingPref,text_encoding) -> Encoding = EncodingPref
2965		; add_error(read_xml,'Illegal encoding preference (must be "auto", "UTF-8", "UTF-16", "ISO-8859-1",...): ',EncodingPref),
2966		Encoding=auto
2967		),
2968		b_absolute_file_name(File,AFile,Span),
2969		statistics(walltime,_),
2970		safe_call(read_string_from_file(AFile,Encoding,Codes),Span),
2971		statistics(walltime,[_,W1]), formatsilent('% Walltime ~w ms to read in ~w~n',[W1,AFile]),
2972		(convert_xml_to_b(Codes,BDataSequence) -> true
2973		; add_error(read_xml,'Converting XML file to B failed: ',AFile,Span),fail),
2974		statistics(walltime,[_,W2]),
2975		formatsilent('% Walltime ~w ms to parse and convert XML in ~w~n',[W2,AFile]),
2976		kernel_objects:equal_object_optimized(Res,BDataSequence).
2977
2978
2979		expects_spaninfo('READ_XML_FROM_STRING').
2980		:- public 'READ_XML_FROM_STRING'/3.
2981		:- block 'READ_XML_FROM_STRING'(-,?,?).
2982		'READ_XML_FROM_STRING'(string(Contents),Res,Span) :-
2983		atom_codes(Contents,Codes),
2984		statistics(walltime,[W1,_]),
2985		(convert_xml_to_b(Codes,BDataSequence) -> true
2986		; add_error(read_xml,'Converting XML string to B failed: ',Contents,Span),fail),
2987		statistics(walltime,[W2,_]), W is W2-W1,
2988		formatsilent('% Walltime ~w ms to parse and convert XML~n',[W]),
2989		kernel_objects:equal_object_optimized(Res,BDataSequence).
2990
2991
2992		expects_spaninfo('WRITE_XML').
2993		:- public 'WRITE_XML'/4.
2994		:- block 'WRITE_XML'(-,?,?,?),'WRITE_XML'(?,-,?,?).
2995		'WRITE_XML'(Records,string(File),Res,Span) :- write_xml2(Records,File,Res,Span).
2996		:- block write_xml2(?,-,?,?).
2997		write_xml2(Records,File,Res,Span) :-
2998		b_absolute_file_name(File,AFile,Span),
2999		statistics(walltime,_),
3000		'WRITE_XML_TO_STRING'(Records,String,Span),
3001		String = string(S),
3002		when(nonvar(S),
3003		(statistics(walltime,[_,W1]), formatsilent('% Walltime ~w ms to convert XML for ~w~n',[W1,AFile]),
3004		open(AFile,write,Stream,[encoding('UTF-8')]),
3005		write(Stream,S),nl(Stream),
3006		close(Stream),
3007		statistics(walltime,[_,W2]), formatsilent('% Walltime ~w ms to write XML to file ~w~n',[W2,AFile]),
3008		Res = pred_true
3009		)).
3010
3011
3012		%sequence of records of type:
3013		% rec(attributes:{("version"|->"03.04")},
3014		% element:"Data",
3015		% meta:{("xmlLineNumber"|->"2")},
3016		% pId:0,
3017		% recId:1),
3018		expects_spaninfo('WRITE_XML_TO_STRING').
3019		:- public 'WRITE_XML_TO_STRING'/3.
3020		:- block 'WRITE_XML_TO_STRING'(-,?,?).
3021		'WRITE_XML_TO_STRING'(Records,Res,Span) :-
3022		custom_explicit_sets:expand_custom_set_to_list(Records,ESet,Done,'WRITE_XML_TO_STRING'),
3023		ground_value_check(ESet,Gr),
3024		when((nonvar(Done),nonvar(Gr)),
3025		( % print(expanded(ESet)),nl,
3026		gen_prolog_xml_term(ESet,Prolog,Span),
3027		%print(prolog(Prolog)),nl,
3028		xml:xml_parse(Codes,Prolog),
3029		(debug:debug_mode(on) -> xml:xml_pp(Prolog) ; true),
3030		atom_codes(S,Codes),
3031		Res = string(S))).
3032
3033		gen_prolog_xml_term(List,xml( [version="1.0", encoding="ASCII"], ContentList),Span) :-
3034		InitialLineNr = 2, % first line is xml-header !?
3035		gen_prolog_xml_dcg(InitialLineNr,_,0,[],ContentList,Span,List,[]).
3036
3037		gen_prolog_xml_dcg(LastLineNr,FinalLineNr,CurLevel, Parents, ResContentList,Span) -->
3038		[(int(Index),rec(Fields))],
3039		{ %print(treat(Index,Fields)),nl,
3040		get_parentId(Fields,CurLevel,Span)}, % The element should be added to the current content list
3041		!,
3042		{get_element(Fields,Element,Span),
3043		get_attributes(Fields,Attributes,Span),
3044		get_line(Fields,LineNr,Span),
3045		gen_element(LastLineNr,LineNr,Element, Attributes, InnerContentList, ResContentList, TailContentList)
3046		},
3047		gen_prolog_xml_dcg(LineNr,LineNr2,Index,[CurLevel|Parents],InnerContentList,Span),
3048		gen_prolog_xml_dcg(LineNr2,FinalLineNr,CurLevel, Parents, TailContentList,Span).
3049		gen_prolog_xml_dcg(L,L,_,_,[],_Span) --> [].
3050
3051		gen_element(LastLineNr,NewLineNr,'CText',['='(text,Codes)],[], [PCDATA|Tail],Tail) :-
3052		insert_newlines(LastLineNr,NewLineNr,Codes,NLCodes),
3053		!,
3054		PCDATA=pcdata(NLCodes).
3055		gen_element(LastLineNr,NewLineNr,Element, Attributes, InnerContentList, [pcdata(NL),ELEMENT|Tail],Tail) :-
3056		LastLineNr < NewLineNr,
3057		insert_newlines(LastLineNr,NewLineNr,[],NL),
3058		!,
3059		ELEMENT = element( Element, Attributes, InnerContentList).
3060		gen_element(_,_,Element, Attributes, InnerContentList, [ELEMENT|Tail],Tail) :-
3061		ELEMENT = element( Element, Attributes, InnerContentList).
3062
3063		insert_newlines(LastLineNr,NewLineNr,C,R) :- NewLineNr =< LastLineNr,!,R=C.
3064		% TO DO: maybe we have to use 13 on Windows ??
3065		insert_newlines(LastLineNr,NewLineNr,C,[10|Res]) :- L1 is LastLineNr+1, insert_newlines(L1,NewLineNr,C,Res).
3066
3067		get_parentId(Fields,Nr,Span) :-
3068		(member(field(pId,int(ParentID)),Fields) -> Nr=ParentID
3069		; add_error('WRITE_XML_TO_STRING','The record has no pId field: ',Fields,Span),
3070		Nr = 0).
3071		get_element(Fields,Atom,Span) :-
3072		(member(field(element,string(Atom)),Fields) -> true
3073		; add_error('WRITE_XML_TO_STRING','The record has no element field: ',Fields,Span),
3074		Atom = '??').
3075
3076		get_attributes(Fields,Attrs,Span) :-
3077		(member(field(attributes,Set),Fields)
3078		-> custom_explicit_sets:expand_custom_set_to_list(Set,ESet,_Done,'get_attributes'),
3079		(maplist(get_xml_attr,ESet,Attrs) -> true
3080		; add_error('WRITE_XML_TO_STRING','Illegal attributes field: ',ESet,Span),
3081		Attrs = []
3082		)
3083		; add_error('WRITE_XML_TO_STRING','The record has no attributes field: ',Fields,Span),
3084		Attrs = []).
3085		get_line(Fields,LineNr,Span) :-
3086		(member(field(meta,Set),Fields)
3087		-> custom_explicit_sets:expand_custom_set_to_list(Set,ESet,_Done,'get_line'),
3088		(member((string(xmlLineNumber),string(LineNrS)),ESet)
3089		-> atom_codes(LineNrS,CC), number_codes(LineNr,CC)
3090		; add_error('WRITE_XML_TO_STRING','The meta field has no xmlLineNumber entry: ',ESet,Span),
3091		LineNr = -1
3092		)
3093		; add_error('WRITE_XML_TO_STRING','The record has no meta field: ',Fields,Span),
3094		LineNr = -1).
3095
3096		get_xml_attr((string(Attr),string(Val)),'='(Attr,ValCodes)) :- atom_codes(Val,ValCodes).
3097
3098
3099		% ----------------------------------
3100		% A flexible CVS Reader that always uses the same type
3101		% rec([field(attributes,BAttributes),field(lineNr,LineNr)])
3102
3103		% EXTERNAL_FUNCTION_READ_CSV_STRINGS == STRING --> seq(CSV_ELement_Type);
3104		% with CSV_ELement_Type == STRING +-> STRING ;
3105
3106		expects_spaninfo('READ_CSV_STRINGS').
3107		:- public 'READ_CSV_STRINGS'/3.
3108		:- block 'READ_CSV_STRINGS'(-,?,?).
3109		'READ_CSV_STRINGS'(string(File),Res,Span) :- read_csv_strings(File,Res,Span).
3110
3111		read_csv_strings(File,ResAVL,Span) :-
3112		b_absolute_file_name(File,AFile,Span),
3113		open_utf8_file_for_reading(AFile,Stream,Span),
3114		statistics(walltime,_),
3115		read_line(Stream,Line1),
3116		(Line1 = end_of_file -> ResAVL = []
3117		; split_csv_line([],HeadersCodes,Span,Line1,[]),
3118		maplist(process_header,HeadersCodes,Headers),
3119		formatsilent('CSV Line Headers = ~w for ~w~n',[Headers,AFile]),
3120		safe_call(read_csv_strings_lines(Stream,1,Span,Headers,Res),Span),
3121		statistics(walltime,[_,W1]), formatsilent('% Walltime ~w ms to read in ~w~n',[W1,AFile]),
3122		kernel_objects:equal_object_optimized(Res,ResAVL),
3123		statistics(walltime,[_,W2]), formatsilent('% Walltime ~w ms to normalise in ~w~n',[W2,AFile])
3124		),
3125		close(Stream). % TO DO: call_cleanup
3126
3127		process_header(HeaderC,HeaderAtom) :- safe_atom_codes(HeaderAtom,HeaderC).
3128
3129		read_csv_strings_lines(Stream,PrevLineNr,Span,Headers,Res) :-
3130		read_line(Stream,Line),
3131		(Line = end_of_file -> Res = []
3132		; LineNr is PrevLineNr+1,
3133		split_csv_line([],AtomsC,Span,Line,[]),
3134		Res = [(int(PrevLineNr),Attrs)|ResT],
3135		construct_attributes(AtomsC,Headers,Attrs,Span,LineNr),
3136		read_csv_strings_lines(Stream,LineNr,Span,Headers,ResT)
3137		).
3138
3139		construct_attributes([],_,[],_,_).
3140		construct_attributes([ [] | T],[ _|HT],Res,Span,LineNr) :- !,
3141		construct_attributes(T,HT,Res,Span,LineNr).
3142		construct_attributes([ AtomC | _T], [], Res,Span,LineNr) :- !,
3143		safe_atom_codes(A,AtomC),
3144		ajoin(['Additional field on line ',LineNr,' : '],Msg),
3145		add_error('READ_CSV_STRINGS',Msg,A,Span),
3146		Res=[].
3147		construct_attributes([ AtomC | T], [ Header | HT], [ (string(Header),string(A)) | ResT],Span,LineNr) :-
3148		safe_atom_codes(A,AtomC),
3149		construct_attributes(T,HT,ResT,Span,LineNr).
3150
3151		% ----------------------------------
3152		% A CSV Reader that uses the B types to adapt how it reads in values
3153
3154		expects_spaninfo('READ_CSV').
3155		expects_type('READ_CSV').
3156
3157		:- public 'READ_CSV'/6.
3158		:- block 'READ_CSV'(-,?,?,?,?,?).
3159		'READ_CSV'(string(File),BoolSkipLine1,AllowExtraValues,Res,Type,Span) :-
3160		read_csv(File,BoolSkipLine1,AllowExtraValues,pred_false,Res,Type,Span).
3161
3162		:- public 'READ_CSV'/4.
3163		:- block 'READ_CSV'(-,?,?,?).
3164		'READ_CSV'(string(File),Res,Type,Span) :-
3165		read_csv(File,pred_false,pred_false,pred_false,Res,Type,Span).
3166
3167		expects_spaninfo('READ_CSV_SEQUENCE').
3168		expects_type('READ_CSV_SEQUENCE').
3169		:- block 'READ_CSV_SEQUENCE'(-,?,?,?,?,?).
3170		:- public 'READ_CSV_SEQUENCE'/6.
3171		'READ_CSV_SEQUENCE'(string(File),BoolSkipLine1,AllowExtraValues,Res,Type,Span) :-
3172		read_csv(File,BoolSkipLine1,AllowExtraValues,pred_true,Res,Type,Span).
3173
3174		:- use_module(bsyntaxtree,[get_set_type/2]).
3175		:- block read_csv(-,?,?,?,?,?,?).
3176		read_csv(File,BoolSkipLine1,AllowExtraValues,CreateSequence,Res,InType,Span) :-
3177		(CreateSequence=pred_true
3178		-> (get_set_type(InType,couple(integer,T)) -> Type=set(T), SeqIndex=1
3179		; add_error('READ_CSV_SEQUENCE','Expecting sequence as return type:',InType),
3180		Type=InType, SeqIndex=none
3181		)
3182		; SeqIndex=none,Type=InType),
3183		get_column_types(Type,Types,Skel,Vars,Span),
3184		b_absolute_file_name(File,AFile,Span),
3185		open_utf8_file_for_reading(AFile,Stream,Span),
3186		(debug:debug_mode(off) -> true
3187		; formatsilent('~nReading CSV file ~w with Types = ~w and Skel = ~w for Vars = ~w~n~n',[AFile,Types,Skel,Vars])),
3188		(read_csv_lines(1,SeqIndex,BoolSkipLine1,AllowExtraValues,Stream,Types,Skel,Vars,Res,Span) -> true
3189		; add_error('READ_CSV','Reading CSV File failed: ',AFile)),
3190		close(Stream). % TO DO: call_cleanup
3191
3192		read_csv_lines(Nr,SeqIndex,BoolSkipLine1,AllowExtraValues,Stream,Types,Skel,Vars,Res,Span) :- %print(line(Nr,Types)),nl,
3193		read_line(Stream,Line),
3194		debug:debug_println(9,read_line(Nr,Line)),
3195		(Line = end_of_file -> Res = []
3196		; split_csv_line([],AtomsC,Span,Line,[]),
3197		%print(atoms(Nr,Atoms)),nl,
3198		%maplist(convert_atom_codes(Span),Types,Atoms,Tuple), % TO DO: check same length
3199		(Nr=1,BoolSkipLine1=pred_true
3200		-> maplist(codes_to_atom,AtomsC,Atoms), format('Skipping line 1: ~w~n',[Atoms]),
3201		Res=ResT
3202		; Line=[] -> format('Skipping empty line ~w~n',[Nr]), Res=ResT
3203		; l_convert_atom_codes(Types,AtomsC,Tuple,Span,Nr,AllowExtraValues),
3204		copy_term((Vars,Skel),(Tuple,BValue)),
3205		(number(SeqIndex) -> S1 is SeqIndex+1, Res = [(int(SeqIndex),BValue)|ResT]
3206		; S1 = SeqIndex, Res = [BValue|ResT]
3207		)
3208		),
3209		N1 is Nr+1,
3210		read_csv_lines(N1,S1,BoolSkipLine1,AllowExtraValues,Stream,Types,Skel,Vars,ResT,Span)).
3211
3212		codes_to_atom(C,A) :- atom_codes(A,C).
3213
3214		l_convert_atom_codes([],[],Vals,_Span,_LineNr,_) :- !, Vals=[].
3215		l_convert_atom_codes([Type|TT],[AtomC|TC],[Val|VT],Span,LineNr,AllowExtraValues) :- !,
3216		convert_atom_codes(Span,LineNr,Type,AtomC,Val),
3217		l_convert_atom_codes(TT,TC,VT,Span,LineNr,AllowExtraValues).
3218		l_convert_atom_codes([Type|TT],[],_,Span,LineNr,_) :- !,
3219		ajoin(['Missing value(s) on CSV line ',LineNr,' for types: '],Msg),
3220		add_error('READ_CSV',Msg,[Type|TT],Span),fail.
3221		l_convert_atom_codes([],[AtomC|AT],Vals,Span,LineNr,AllowExtraValues) :- !,
3222		(AllowExtraValues=pred_true -> true
3223		; safe_atom_codes(Atom,AtomC),
3224		ajoin(['Extra value(s) on CSV line ',LineNr,' : ',Atom,' Rest = '],Msg),
3225		add_error('READ_CSV',Msg,AT,Span)
3226		), Vals=[].
3227
3228		convert_atom_codes(Span,LineNr,T,AtomC,Val) :-
3229		(convert_atom2(T,AtomC,Val,Span,LineNr) -> true ;
3230		atom_codes(Atom,AtomC),
3231		ajoin(['Could not convert value to type ',T,' on CSV line ',LineNr,': '],Msg),
3232		add_error('READ_CSV',Msg,Atom,Span),
3233		Val = term('READ_CSV_ERROR')).
3234		:- use_module(tools,[safe_number_codes/2, safe_atom_codes/2]).
3235		convert_atom2(string,C,string(A),_,_) :- safe_atom_codes(A,C).
3236		convert_atom2(integer,C,int(Nr),_Span,LineNr) :-
3237		(C=[] -> (debug:debug_mode(off) -> true ; format('Translating empty string to -1 on line ~w~n',[LineNr])),
3238		% add_warning('READ_CSV','Translating empty string to -1 on line: ',LineNr,Span),
3239		Nr is -1
3240		; safe_number_codes(Nr,C)).
3241		convert_atom2(global(G),C,FD,Span,LineNr) :- safe_atom_codes(A,C),convert_to_enum(G,A,FD,Span,LineNr).
3242		convert_atom2(boolean,C,Bool,Span,LineNr) :- safe_atom_codes(A,C),
3243		(convert_to_bool(A,Bool) -> true
3244		; ajoin(['Could not convert value to BOOL on line ',LineNr,'; assuming FALSE: '],Msg),
3245		add_warning('READ_CSV',Msg,A,Span),
3246		Bool=pred_false).
3247		% TO DO: support set(_), seq(_)
3248
3249		convert_to_bool('0',pred_false).
3250		convert_to_bool('1',pred_true).
3251		convert_to_bool('FALSE',pred_false).
3252		convert_to_bool('TRUE',pred_true).
3253		convert_to_bool('false',pred_false).
3254		convert_to_bool('true',pred_true).
3255
3256		convert_to_enum(G,A,FD,Span,LineNr) :- string_to_enum2(A,FD),
3257		(FD=fd(_,G) -> true ; add_error('READ_CSV','Enumerated element of incorrect type: ',A:expected(G):line(LineNr),Span)).
3258
3259		% split a CSV line into individual AtomCode lists
3260		split_csv_line([],T,Span) --> " ", !, split_csv_line([],T,Span).
3261		split_csv_line(Acc,[AtomC|T],Span) --> sep, !,
3262		{reverse(Acc,AtomC)}, split_csv_line([],T,Span).
3263		split_csv_line([],[String|T],Span) --> [34], % "
3264		scan_to_end_of_string([],String,Span),
3265		(sep -> split_csv_line([],T,Span)
3266		; [XX] -> {add_error('READ_CSV','String not followed by separator: ',String,Span)}, split_csv_line([XX],T,Span)
3267		; {T=[]}).
3268		split_csv_line(Acc,Atoms,Span) --> [X], !, split_csv_line([X|Acc],Atoms,Span).
3269		split_csv_line(Acc,[AtomC],_Span) --> !, % end of line
3270		{reverse(Acc,AtomC)}.
3271
3272		sep --> " ",!, sep.
3273		sep --> ("," ; ";" ; " ,").
3274
3275		scan_to_end_of_string(Acc,AtomC,_) --> [34],!,{reverse(Acc,AtomC)}.
3276		scan_to_end_of_string(Acc,String,Span) --> [X],!, scan_to_end_of_string([X|Acc],String,Span).
3277		scan_to_end_of_string(Acc,String,Span) -->
3278		{reverse(Acc,RAcc),atom_codes(String,RAcc),add_error('READ_CSV','String not terminated: ',String,Span)}.
3279
3280		% get the list of column types along with Value skeleton with variables in the places where CSV values should be inserted
3281		get_column_types(set(X),Types,Skel,Vars,_) :- !,flatten_pairs(X,Types,[]), %print(types(Types)),nl,
3282		flatten_pairs_value_skeleton(X,Skel,Vars,[]). % print(skel(Skel,Vars)),nl.
3283		get_column_types(seq(X),Types,Skel,Vars,Span) :- !,
3284		get_column_types(set(couple(integer,X)),Types,Skel,Vars,Span).
3285		get_column_types(Type,_,_,_,Span) :- add_error('READ_CSV','Invalid return type (must be relation): ',Type,Span),fail.
3286
3287		% flatten couple pairs and generate skeleton term
3288		flatten_pairs(couple(A,B)) --> !,flatten_pairs(A), flatten_pairs(B).
3289		flatten_pairs(record(Fields)) --> !, flatten_fields(Fields).
3290		flatten_pairs(X) --> [X].
3291
3292		/* note: currently record fields have to be alphabetically in the same order as in CSV file: the fields are sorted by ProB's kernel ! : TO DO: try and recover the original order of the fields */
3293		flatten_fields([]) --> [].
3294		flatten_fields([field(_Name,Type)|T]) --> [Type], % no nesting allowed; this has to be a basic type for CSV reading to work
3295		flatten_fields(T).
3296
3297		% generate a value skeleton
3298		flatten_pairs_value_skeleton(couple(A,B),(CA,CB)) --> !,
3299		flatten_pairs_value_skeleton(A,CA), flatten_pairs_value_skeleton(B,CB).
3300		flatten_pairs_value_skeleton(record(Fields),rec(SF)) --> !, flatten_field_skel(Fields,SF).
3301		flatten_pairs_value_skeleton(_X,Var) --> [Var].
3302
3303		flatten_field_skel([],[]) --> [].
3304		flatten_field_skel([field(Name,_Type)|T],[field(Name,Var)|ST]) --> [Var],
3305		flatten_field_skel(T,ST).