1		% (c) 2009-2024 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2		% Heinrich Heine Universitaet Duesseldorf
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5		:- module(parsercall, [load_b_machine_as_term/3,
6		load_b_machine_probfile_as_term/2, % a way to directly load a .prob file
7		load_b_machine_probfile_as_term/3,
8		load_b_machine_list_of_facts_as_term/2,
9		get_parser_version/1,
10		get_parser_version/2,
11		get_parser_version/6,
12		get_java_command_path/1,
13		check_java_version/2,
14		get_java_fullversion/1, get_java_fullversion/3, get_java_version/1,
15		ensure_console_parser_launched/0, % just make sure the console parser is up and running
16		connect_to_external_console_parser_on_port/1, % connect to a separately started parser
17		release_console_parser/0,
18		console_parser_jar_available_in_lib/0,
19		call_ltl_parser/3,
20		call_tla2b_parser/1, tla2b_filename/2,
21		%call_promela_parser/1, promela_prolog_filename/2,
22		call_alloy2pl_parser/2,
23		tla2prob_filename/2,
24		parse/3,
25		parse_at_position_in_file/5,
26		parse_formula/2, parse_predicate/2, parse_expression/2,
27		parse_substitution/2,
28		transform_string_template/3,
29		call_fuzz_parser/2,
30		register_parsing_call_back/1, deregister_parsing_call_back/0,
31		set_default_filenumber/2, reset_default_filenumber/2
32		]).
33
34		:- meta_predicate register_parsing_call_back(4).
35
36		:- use_module(module_information,[module_info/2]).
37		:- module_info(group,typechecker).
38		:- module_info(description,'This module takes care of calling the Java B Parser if necessary.').
39
40		:- use_module(library(lists)).
41		:- use_module(library(process)).
42		:- use_module(library(file_systems)).
43		:- use_module(library(codesio)).
44		:- use_module(library(system)).
45		:- use_module(library(sockets)).
46
47		:- use_module(error_manager,[add_error/2, add_error/3, add_error/4, add_error_fail/3,
48		add_failed_call_error/1, add_internal_error/2, add_warning/3, add_warning/4, real_error_occurred/0,
49		add_message/3, add_message/4, extract_line_col/5, add_all_perrors/3]).
50		:- use_module(self_check).
51		:- use_module(preferences).
52		:- use_module(tools, [split_filename/3, same_file_name/2, get_PROBPATH/1, safe_atom_chars/3]).
53		:- use_module(tools_platform, [host_platform/1, platform_is_64_bit/0]).
54		:- use_module(tools_strings,[ajoin_with_sep/3, ajoin/2]).
55		:- use_module(tools_printing,[print_error/1, format_with_colour_nl/4]).
56		:- use_module(debug).
57		:- use_module(bmachine,[b_get_definition/5, b_machine_is_loaded/0]).
58		:- use_module(specfile, [b_or_z_mode/0]).
59
60		:- set_prolog_flag(double_quotes, codes).
61
62		:- dynamic java_parser_version/6.
63
64		% stores the java process of the parser, consisting of ProcessIdentifier, Socket Stream, STDErrStream
65		:- dynamic java_parser_process/4.
66		:- volatile java_parser_process/4.
67
68
69		send_definition(Stream,def(Name,Type,Arity)) :-
70		write(Stream,'definition'), nl(Stream),
71		format(Stream,'~w\n~w\n~w\n',[Name,Type,Arity]).
72
73		:- dynamic definitions_already_sent/0.
74		:- volatile definitions_already_sent/0.
75
76		send_definitions(ToParser) :-
77		b_or_z_mode, b_machine_is_loaded,
78		\+ definitions_already_sent,
79		!,
80		findall_definitions(L),
81		% format('~nSending definitions ~w~n~n',[L]),
82		maplist(send_definition(ToParser),L),
83		assertz(definitions_already_sent).
84		send_definitions(_).
85
86		findall_definitions(DefList) :-
87		findall(def(Name,Type,Arity),(b_get_definition(Name,Type,Args,_,_),length(Args,Arity)),DefList).
88
89		get_definitions(L) :- b_or_z_mode, b_machine_is_loaded,!, findall_definitions(L).
90		get_definitions([]).
91
92		reset_definitions :-
93		retractall(definitions_already_sent),
94		parser_is_launched, % otherwise no need to reset; inside prob2_kernel there is no Java parser for probcli
95		(debug_mode(off) -> true
96		; get_parser_version(Version),
97		format('Resetting DEFINITIONS for parser version ~w ~n',[Version])
98		),
99		% TO DO: check if parser Version is at least 2.9.27
100		get_console_parser(ParserStream,Out,Err),!,
101		write(ParserStream,'resetdefinitions'), nl(ParserStream), % only supported in more recent versions of the parser
102		flush_output(ParserStream),
103		display_pending_outputs(Out,user_output),
104		display_pending_outputs(Err,user_error).
105		reset_definitions.
106
107		% update preferences of parser using new PREPL commands
108		update_jvm_parser_preferences :-
109		get_preference(jvm_parser_fastrw,FAST),
110		try_set_parser_option_nc(fastPrologOutput,FAST,_),
111		get_preference(jvm_parser_position_infos,LINENO),
112		try_set_parser_option_nc(addLineNumbers,LINENO,_),
113		(debug_mode(off) -> VERBOSE=false ; VERBOSE=true),
114		try_set_parser_option_nc(verbose,VERBOSE,_).
115
116
117		:- dynamic cur_defaultFileNumber/1.
118
119		try_set_parser_option(defaultFileNumber,Value,Res) :- !,
120		(cur_defaultFileNumber(Value) % cache last value to avoid unnecessary parser calls
121		-> Res=prev_value(Value) % nothing to do
122		; retractall(cur_defaultFileNumber(_)),
123		assert(cur_defaultFileNumber(Value)),
124		try_set_parser_option_nc(defaultFileNumber,Value,Res)
125		).
126		try_set_parser_option(Name,Value,Res) :-
127		try_set_parser_option_nc(Name,Value,Res).
128
129		reset_parser_option_cache :- retractall(cur_defaultFileNumber(_)).
130
131		% try_set_parser_option_nc: non-caching version
132		try_set_parser_option_nc(Name,Value,Res) :-
133		parser_command_supported(setoption),
134		!,
135		debug_format(4,'Updating parser option: ~q=~q~n',[Name,Value]),
136		get_console_parser(Stream,_Out,Err),
137		write(Stream,setoption), nl(Stream),
138		write(Stream,Name), nl(Stream),
139		write(Stream,Value), nl(Stream),
140		flush_output(Stream),
141		read_line(Stream,CodesIn),
142		my_read_from_codes(CodesIn,Res,Stream,Err).
143		try_set_parser_option_nc(Name,Value,Res) :-
144		old_option_command(Name,Command),
145		parser_command_supported(Command),
146		!,
147		debug_format(19,'Updating JVM parser option (using old command ~q): ~q=~q~n',[Command,Name,Value]),
148		get_console_parser(Stream,_Out,_Err),
149		write(Stream,Command), nl(Stream),
150		write(Stream,Value), nl(Stream),
151		flush_output(Stream),
152		Res = changed. % prev_value isn't returned here
153		try_set_parser_option_nc(Name,Value,unsupported) :-
154		debug_format(19,'Parser too old to change option at runtime: ~q=~q~n',[Name,Value]).
155
156
157
158		old_option_command(addLineNumbers,lineno).
159		old_option_command(verbose,verbose).
160		old_option_command(fastPrologOutput,fastprolog).
161		old_option_command(compactPrologPositions,compactpos).
162		old_option_command(machineNameMustMatchFileName,checkname).
163
164		reset_old_parser_option_value(Name,Value,prev_value(Old)) :- \+ unchanged(Value,Old), !,
165		try_set_parser_option(Name,Old,_).
166		reset_old_parser_option_value(_,_,_).
167
168		% the Java values are stored as strings, even for number attributes
169		unchanged(V,V).
170		unchanged(N,A) :- number(N), atom(A), number_codes(N,C), atom_codes(A,C).
171
172		reset_parser :- reset_definitions, reset_parser_option_cache.
173		:- use_module(probsrc(eventhandling),[register_event_listener/3]).
174		:- register_event_listener(clear_specification,reset_parser,
175		'Remove DEFINITIONS from parser cache and reset parer options cache.').
176
177		crlf(10).
178		crlf(13).
179
180		% remove newlines in a B formula so that we can pass the formula as a single line to the parser
181		cleanup_newlines([],[]).
182		cleanup_newlines([H|T],CleanCodes) :- crlf(H),!,
183		% this could also be inside a multi-line string; the string will be modified by this conversion
184		CleanCodes=[8232|TC], % 8232 \x2028 is Unicode line separator
185		cleanup_newlines(T,TC).
186		%cleanup_newlines([47,47|T],CleanCodes) :-
187		% % a B Comment '//': we used to skip until end of line
188		% % but this could be inside a string ! see test 2236
189		% CleanCodes=[8232|TC], skip_until_crlf(T,T2), !, cleanup_newlines(T2,TC).
190		cleanup_newlines([H|T],[H|R]) :- cleanup_newlines(T,R).
191
192		%skip_until_crlf([],[]).
193		%skip_until_crlf([H|T],T) :- crlf(H),!.
194		%skip_until_crlf([_|T],R) :- skip_until_crlf(T,R).
195
196		% register parsing call back from prob_socket_server within ProB2
197		:- dynamic prob2_call_back_available/1.
198		register_parsing_call_back(CallBackPred4) :- deregister_parsing_call_back,
199		assertz(prob2_call_back_available(CallBackPred4)).
200		deregister_parsing_call_back :-
201		retractall(prob2_call_back_available(_)).
202
203		% ---------
204
205		%! parse_x(+Kind,+Codes,-Tree)
206		% Kind is formula, expression, predicate, substitution
207		%:- use_module(prob_socketserver,[prob2_call_back_available/0, prob2_call_back/2]).
208		parse_x(Kind,CodesWithNewlines,Tree) :-
209		parse_simple(Kind,CodesWithNewlines,Res),!,
210		% format('Parse simple ~s : ~w~n',[CodesWithNewlines,Res]),
211		Tree=Res.
212		parse_x(Kind,CodesWithNewlines,Tree) :-
213		parse_y(Kind,CodesWithNewlines,Tree).
214
215		% a version which does not attempt simple parsing without calling Java:
216		parse_y(Kind,CodesWithNewlines,Tree) :-
217		prob2_call_back_available(ParseCallBackPred),
218		cleanup_newlines(CodesWithNewlines,Codes), atom_codes(Formula,Codes),
219		debug_format(19,'Parsing ~w via call_back: ~w~n',[Kind,Formula]),
220		get_definitions(DefList),
221		call(ParseCallBackPred,Kind,DefList,Formula,Tree),
222		% TO DO: deal with substitutions
223		debug_println(19,prob2_call_back_available_parse_result(Tree)),
224		(Tree = call_back_not_supported ->
225		% Parsing callback isn't implemented (e. g. ProB Rodin plugin) - don't try to use it again in the future.
226		deregister_parsing_call_back,
227		fail
228		; true),
229		!,
230		(Tree = parse_error(Exception)
231		-> handle_parser_exception(Exception)
232		; functor(Tree,parse_error,_) % deprecated
233		-> throw(parse_errors([error('Parse error occurred via ProB2 call_back:',unknown)]))
234		; true).
235		parse_y(Kind,CodesWithNewlines,Tree) :-
236		% Java parser expects only one line of input -> remove newlines
237		cleanup_newlines(CodesWithNewlines,Codes),
238		% statistics(walltime,[Tot,Delta]), format('~s~n~w~n0 ~w (Delta ~w) ms ~n',[Codes,Kind,Tot,Delta]),
239		get_console_parser(Stream,Out,Err),
240		send_definitions(Stream),
241		write(Stream,Kind),
242		nl(Stream),
243		format(Stream,'~s',[Codes]), %format(user_output,'sent: ~s~n',[Codes]),
244		nl(Stream),
245		flush_output(Stream),
246		read_line(Stream,CodesIn),
247		%format('read: ~s~n',[CodesIn]),
248		catch(
249		(my_read_from_codes(CodesIn,Tree,Stream,Err),handle_parser_exception(Tree)),
250		error(_,_),
251		(append("Illegal parser result exception: ",CodesIn,ErrMsgCodes),
252		atom_codes(ErrMsg,ErrMsgCodes),
253		throw(parse_errors([internal_error(ErrMsg,none)])))),
254		display_pending_outputs(Out,user_output).
255		%statistics(walltime,[Tot4,Delta4]), format('4 ~w (Delta ~w) ms ~n ~n',[Tot4,Delta4]).
256
257		% a few very simple cases, which can be parsed without accessing Java parser:
258		% common e.g., in JSON trace files or Latex files to avoid overhead of calling parser
259		parse_simple(Kind,Codes,AST) :-
260		(Kind=expression -> true ; Kind=formula),
261		(cur_defaultFileNumber(FN) -> true ; FN = -1),
262		parse_simple_codes(Codes,FN,1,1,AST).
263
264		% ---------------------------
265
266		% benchmarking code:
267		% statistics(walltime,[_W1,_]),(for(I,1,10000) do parsercall:parse_formula("123",Tree)),statistics(walltime,[_W2,_]),D is _W2-_W1.
268		% | ?- findall("|-> 123",between(2,10000,X),L), append(["123 "|L],Str), statistics(walltime,[_W1,_]),parsercall:parse_expression(Str,Tree), statistics(walltime,[_W2,_]),D is _W2-_W1.
269
270		parse_simple_codes(Codes,FileNr,SL,SC,AST) :-
271		parse_int_codes(Codes,Len,Val), !,
272		L2 is Len+SC, % EndColumn of p4 position (same line)
273		AST=integer(p4(FileNr,SL,SC,L2),Val).
274		parse_simple_codes("TRUE",FileNr,SL,SC,AST) :- !, EC is SC+4, AST=boolean_true(p4(FileNr,SL,SC,EC)).
275		parse_simple_codes("FALSE",FileNr,SL,SC,AST) :- !, EC is SC+5, AST=boolean_false(p4(FileNr,SL,SC,EC)).
276		parse_simple_codes("{}",FileNr,SL,SC,AST) :- !, EC is SC+2, AST=empty_set(p4(FileNr,SL,SC,EC)).
277		parse_simple_codes(Codes,FileNr,SL,SC,AST) :- is_real_literal_codes(Codes),!,
278		length(Codes,Len), L2 is Len+SC,
279		atom_codes(Atom,Codes),
280		AST=real(p4(FileNr,SL,SC,L2),Atom).
281		% TO DO: maybe simple string values, simple identifiers: but we need to know the keyword list for this
282
283		:- assert_must_succeed((parsercall:parse_int_codes("0",Len,Res), Len==1, Res==0)).
284		:- assert_must_succeed((parsercall:parse_int_codes("1",Len,Res), Len==1, Res==1)).
285		:- assert_must_succeed((parsercall:parse_int_codes("12",Len,Res), Len==2, Res==12)).
286		:- assert_must_succeed((parsercall:parse_int_codes("931",Len,Res), Len==3, Res==931)).
287		:- assert_must_succeed((parsercall:parse_int_codes("100931",Len,Res), Len==6, Res==100931)).
288		parse_int_codes([Digit|T],Len,Res) :- digit_code_2_int(Digit,DVal),
289		(DVal=0 -> T=[], Len=1, Res=0
290		; parse_int2(T,DVal,Res,1,Len)).
291
292		parse_int2([],Acc,Acc,LenAcc,LenAcc).
293		parse_int2([Digit|T],Acc,Res,LenAcc,Len) :-
294		digit_code_2_int(Digit,DVal),
295		NewAcc is Acc*10 + DVal,
296		L1 is LenAcc+1,
297		parse_int2(T,NewAcc,Res,L1,Len).
298
299		digit_code_2_int(X,Val) :- X >= 48, X =< 57, Val is X - 48.
300		is_digit(X) :- X >= 48, X =< 57.
301
302		:- assert_must_succeed(parsercall:is_real_literal_codes("0.0")).
303		:- assert_must_succeed(parsercall:is_real_literal_codes("112300.0010")).
304		:- assert_must_succeed(parsercall:is_real_literal_codes("1234567890.9876543210")).
305		:- assert_must_succeed(parsercall:is_real_literal_codes("001.0")). % is accepted by parser
306		:- assert_must_fail(parsercall:is_real_literal_codes("0")).
307		:- assert_must_fail(parsercall:is_real_literal_codes("11.")).
308		:- assert_must_fail(parsercall:is_real_literal_codes(".12")).
309		:- assert_must_fail(parsercall:is_real_literal_codes("12a.0")).
310		% TODO: we could return length and merge with parse_int_codes to do only one traversal
311
312	?	is_real_literal_codes([Digit|T]) :- is_digit(Digit), is_real_lit1(T).
313		is_real_lit1([0'.,Digit|T]) :- is_digit(Digit), is_real_lit2(T).
314	?	is_real_lit1([Digit|T]) :- is_digit(Digit), is_real_lit1(T).
315		is_real_lit2([]).
316		is_real_lit2([Digit|T]) :- is_digit(Digit), is_real_lit2(T).
317
318		% ---------------------
319
320		my_read_from_codes(end_of_file,_,_,Err) :- !,
321		read_line_if_ready(Err,Err1Codes), % we just read one line
322		safe_name(ErrMsg,Err1Codes),
323		add_error(parsercall,'Abnormal termination of parser: ',ErrMsg),
324		missing_parser_diagnostics,
325		ajoin(['Parser not available (',ErrMsg,')'],FullErrMsg),
326		read_lines_and_add_as_error(Err), % add other info on error stream as single error
327		throw(parse_errors([error(FullErrMsg,none)])).
328		my_read_from_codes(ErrorCodes,_Tree,Out,_) :-
329		append("Error",_,ErrorCodes),!,
330		atom_codes(ErrMsg,ErrorCodes),
331		add_error(parsercall,'Error running/starting parser: ',ErrMsg),
332		read_lines_and_add_as_error(Out),
333		fail.
334		my_read_from_codes(CodesIn,Tree,_,_) :- read_from_codes(CodesIn,Tree).
335
336		% a version of my_read_from_codes which has no access to error stream
337		my_read_from_codes(end_of_file,_) :- !,
338		missing_parser_diagnostics,
339		throw(parse_errors([error('Parser not available (end_of_file on input stream)',none)])).
340		my_read_from_codes(ErrorCodes,_Tree) :-
341		append("Error",_,ErrorCodes),!,
342		atom_codes(ErrMsg,ErrorCodes),
343		add_error(parsercall,'Error running/starting parser: ',ErrMsg),
344		fail.
345		my_read_from_codes(CodesIn,Tree) :- read_from_codes(CodesIn,Tree).
346
347		:- use_module(probsrc(preferences),[get_prob_application_type/1]).
348		missing_parser_diagnostics :-
349		parser_location(Classpath), debug_println(9,classpath(Classpath)),fail.
350		missing_parser_diagnostics :- runtime_application_path(P),
351		atom_concat(P,'/lib/probcliparser.jar',ConParser), % TODO: adapt for GraalVM cliparser
352		(file_exists(ConParser)
353		-> add_error(parsercall,'The Java B parser (probcliparser.jar) cannot be launched: ',ConParser),
354		(get_prob_application_type(tcltk) ->
355		add_error(parsercall,'Please check that Java and B Parser are available using the "Check Java and Parser Version" command in the Debug menu.')
356		; host_platform(windows) ->
357		add_error(parsercall,'Please check that Java and B Parser are available, e.g., using "probcli.exe -check_java_version" command.')
358		; add_error(parsercall,'Please check that Java and B Parser are available, e.g., using "probcli -check_java_version" command.')
359		% application_type
360		% TODO: avoid printing the message when the user is already calling check_java_version
361		),
362		(get_preference(jvm_parser_additional_args,ExtraArgStr), ExtraArgStr\=''
363		-> add_error(parsercall,'Also check your JVM_PARSER_ARGS preference value:',ExtraArgStr)
364		; true)
365		; add_internal_error('Java B parser (probcliparser.jar) is missing from lib directory in: ',P)
366		).
367
368		% ProB2 cli builds do not have the cli parser bundled
369		% check if there is a jar available in the lib folder:
370		% should only happen for get_prob_application_type(probcli) in ProB2
371		console_parser_jar_available_in_lib :-
372		runtime_application_path(P),
373		atom_concat(P,'/lib/probcliparser.jar',ConParser),
374		file_exists(ConParser).
375
376		handle_parser_exception(Exception) :-
377		handle_parser_exception(Exception,ExAuxs,[]),
378		!,
379		throw(parse_errors(ExAuxs)).
380		handle_parser_exception(_).
381
382		handle_parser_exception(compound_exception([])) --> [].
383		handle_parser_exception(compound_exception([Ex|MoreEx])) -->
384		handle_parser_exception(Ex),
385		handle_parser_exception(compound_exception(MoreEx)).
386		% Non-list version of parse_exception is handled in handle_parser_exception_aux.
387		% (Note: The non-list version is no longer generated by the parser -
388		% see comments on handle_console_parser_result below.)
389		handle_parser_exception(parse_exception([],_Msg)) --> [].
390		handle_parser_exception(parse_exception([Pos|MorePos],Msg)) -->
391		[error(Msg,Pos)],
392		handle_parser_exception(parse_exception(MorePos,Msg)).
393		handle_parser_exception(Ex) -->
394		{handle_parser_exception_aux(Ex,ExAux)},
395		[ExAux].
396
397		handle_parser_exception_aux(parse_exception(Pos,Msg),error(SanitizedMsg,Pos)) :-
398		remove_msg_posinfo_known(Msg,SanitizedMsg).
399		handle_parser_exception_aux(io_exception(Pos,Msg),error(Msg,Pos)).
400		handle_parser_exception_aux(io_exception(Msg),error(Msg,unknown)).
401		handle_parser_exception_aux(exception(Msg),error(Msg,unknown)). % TO DO: get Pos from Java parser !
402
403		%! parse_formula(+Codes,-Tree)
404		parse_formula(Codes,Tree) :-
405		parse_x(formula,Codes,Tree).
406
407		%! parse_expression(+Codes,-Tree)
408		parse_expression(Codes,Tree) :-
409		parse_x(expression,Codes,Tree).
410
411		%! parse_predicate(+Codes,-Tree)
412		parse_predicate(Codes,Tree) :-
413		parse_x(predicate,Codes,Tree).
414
415		%! parse_substitution(+Codes,-Tree)
416		parse_substitution(Codes,Tree) :-
417		parse_x(substitution,Codes,Tree).
418
419		% parse in the context of particular files and position within the file (e.g., VisB JSON file)
420
421		parse_at_position_in_file(Kind,Codes,Tree,Span,Filenumber) :- Span \= unknown,
422		%format('Parse @ ~w~n ~s~n',[Span,Codes]),
423		extract_line_col_for_b_parser(Span,Line,Col),!,
424		parse_at_position_in_file2(Kind,Codes,Tree,Filenumber,Line,Col).
425		parse_at_position_in_file(Kind,Codes,Tree,_,_) :-
426		parse_x(Kind,Codes,Tree).
427
428		parse_at_position_in_file2(Kind,Codes,Tree,Filenumber,Line,Col) :-
429		(Kind=expression -> true ; Kind=formula),
430		% special case to avoid setting parser options if parser not called in parse_x !
431		parse_simple_codes(Codes,Filenumber,Line,Col,AST),!,
432		Tree=AST.
433		parse_at_position_in_file2(Kind,Codes,Tree,Filenumber,Line,Col) :-
434		(Line \= 1 -> try_set_parser_option_nc(startLineNumber,Line,_OldLine)
435		; true), % default in ParsingBehaviour.java: 1
436		(Col \= 1 -> try_set_parser_option_nc(startColumnNumber,Col,_OldCol)
437		; true), % default in ParsingBehaviour.java: 1
438		(integer(Filenumber) -> Fnr=Filenumber ; format('Invalid filenumber : ~w~n',[Filenumber]), Fnr = -1),
439		try_set_parser_option(defaultFileNumber,Fnr,OldFile),
440		% Note: Filenumber will be used in AST, but parse errors will have null as filename
441		% format('Parsing at line ~w col ~w in file ~w (old ~w:~w in ~w)~n',[Line,Col,Filenumber,OldLine,OldCol,OldFile]),
442		call_cleanup(parse_y(Kind,Codes,Tree),
443		(%reset_old_parser_option_value(startLineNumber,Line,OldLine), % not required anymore, is now volatile
444		%reset_old_parser_option_value(startColumnNumber,Col,OldCol), % not required anymore, is now volatile
445		% TODO: should we check at startup whether the parser has volatilePosOptions feature?
446		reset_old_parser_option_value(defaultFileNumber,Filenumber,OldFile))).
447
448		extract_line_col_for_b_parser(Span,Line,Col1) :-
449		extract_line_col(Span,Line,Col,_EndLine,_EndCol),
450		Col1 is Col+1. % the BParser starts column numbering at 1
451
452		set_default_filenumber(Filenumber,OldFile) :- try_set_parser_option(defaultFileNumber,Filenumber,OldFile).
453		reset_default_filenumber(Filenumber,OldFile) :- reset_old_parser_option_value(defaultFileNumber,Filenumber,OldFile).
454
455		%! parse(+Kind,+Codes,-Tree)
456		parse(Kind,Codes,Tree) :- parse_x(Kind,Codes,Tree).
457
458		%! parse_temporal_formula(+Kind,+LanguageExtension,+Formula,-Tree)
459		parse_temporal_formula(Kind,LanguageExtension,Formula,Tree) :-
460		write_to_codes(Formula,CodesWithNewlines),
461		% Java parser expects only one line of input -> remove newlines
462		cleanup_newlines(CodesWithNewlines,Codes),
463		get_console_parser(Stream,Out,Err),
464		send_definitions(Stream),
465		format(Stream,'~s', [Kind]), nl(Stream),
466		format(Stream,'~s', [LanguageExtension]), nl(Stream),
467		format(Stream,'~s',[Codes]), nl(Stream),
468		flush_output(Stream),
469		% format('Parsing temporal formula, kind=~s, lge=~s, formula="~s"~n',[Kind,LanguageExtension,Codes]),
470		read_line(Stream,CodesIn), % TODO: Improve feedback from java!
471		catch(my_read_from_codes(CodesIn,Tree,Stream,Err),_,throw(parse_errors([error(exception,none)]))),
472		display_pending_outputs(Out,user_output).
473
474		% throws parse_errors(Errors) in case of syntax errors
475		load_b_machine_as_term(Filename, Machine,Options) :- %print(load_b_machine(Filename)),nl,
476		prob_filename(Filename, ProBFile),
477		debug_println(9,prob_filename(Filename,ProBFile)),
478		( get_preference(jvm_parser_force_parsing,false),
479		dont_need_compilation(Filename,ProBFile,Machine,LoadResult,Options) ->
480		% no compilation is needed, .prob file was loaded
481		release_parser_if_requested(Options),
482		(LoadResult=loaded -> debug_println(20,'.prob file up-to-date')
483		; print_error('*** Loading failed *** '),nl,fail)
484		; % we need to parse and generate .prob file
485		(debug:debug_mode(on) ->
486		time_with_msg('generating .prob file with Java parser',call_console_parser(Filename,ProBFile))
487		; call_console_parser(Filename,ProBFile)
488		),
489		release_parser_if_requested(Options),
490		load_b_machine_probfile_as_term(ProBFile, Options, Machine)
491		).
492		release_parser_if_requested(Options) :- (member(release_java_parser,Options) -> release_console_parser ; true).
493
494		% converts the filename of the machine into a filename for the parsed machine
495		prob_filename(Filename, ProB) :-
496		split_filename(Filename,Basename,_Extension),
497		safe_atom_chars(Basename,BasenameC,prob_filename1),
498		append(BasenameC,['.','p','r','o','b'],ProBC),
499		safe_atom_chars(ProB,ProBC,prob_filename2),!.
500		prob_filename(Filename, ProB) :-
501		add_failed_call_error(prob_filename(Filename,ProB)),fail.
502
503		check_version_and_read_machine(Filename,ProBFile, ProbTime, Version, GitSha, Machine,Options) :-
504		(Version='$UNKNOWN'
505		-> add_warning(parsercall,'*** Unknown parser version number. Trying to load parsed file: ',ProBFile)
506		/* keep CheckVersionNr as variable */
507		; CheckVersionNr=Version),
508		read_machine_term_from_file(ProBFile,prob_parser_version(CheckVersionNr,GitSha),
509		[check_if_up_to_date(Filename,ProbTime)|Options],Machine).
510
511		read_machine_term_from_file(ProBFile,VersionTerm,Options,CompleteMachine) :-
512		(debug:debug_mode(on)
513		-> time_with_msg('loading .prob file',
514		read_machine_term_from_file_aux(ProBFile,VersionTerm,Options,CompleteMachine))
515		; read_machine_term_from_file_aux(ProBFile,VersionTerm,Options,CompleteMachine)).
516
517		read_machine_term_from_file_aux(ProBFile,VersionTerm,Options,complete_machine(MainName,Machines,Files)) :-
518		open_probfile(ProBFile,Options,Stream,Opt2),
519		call_cleanup(( safe_read_term(Stream,Opt2,ProBFile,parser_version,VersionTermInFile),
520		debug_format(9,'Parser version term in file: ~w~n',[VersionTermInFile]),
521		same_parser_version(VersionTermInFile,VersionTerm), % CHECK correct version
522		read_machines(Stream,ProBFile,Opt2,Machines,MainName,Files),
523		(var(MainName)
524		-> add_internal_error('Missing classical_b fact',ProBFile), MainName=unknown,Files=[]
525		; true)
526		),
527		close(Stream)).
528
529		% open a .prob file:
530		open_probfile(ProBFile,Options,NewStream,NewOptions) :-
531		open(ProBFile, read, Stream),
532		file_property(ProBFile,size_in_bytes,Size),
533		check_prob_file_not_empty(Stream,Size,ProBFile,Options),
534		peek_code(Stream,Code),
535		open_probfile_aux(Code,Size,Stream,ProBFile,Options,NewStream,NewOptions).
536
537		open_probfile_aux(Code,_,Stream,ProBFile,Options,NewStream,NewOptions) :-
538		fastrw_start_code(Code),!,
539		close(Stream),
540		add_message(parsercall,'Reading .prob file using fastrw library: ',ProBFile),
541		open(ProBFile, read, NewStream, [type(binary)]),
542		% delete(use_fastread)
543		NewOptions = [use_fastrw|Options].
544		open_probfile_aux(Code,Size,Stream,ProBFile,Options,Stream,NewOptions) :-
545		check_prob_file_first_code(Code,Stream,ProBFile,Options),
546		update_options(Options,Size,NewOptions).
547
548		% automatically use fastread if file large
549		update_options(Options,Size,Opt2) :- nonmember(use_fastread,Options),
550		nonmember(use_fastrw,Options),
551		Size>1000000, % greater than 1 MB
552		!, Opt2 = [use_fastread|Options],
553		debug_println(19,automatically_using_fastread(Size)).
554		update_options(Opts,_,Opts).
555
556		% check if the file starts out in an expected way
557		check_prob_file_not_empty(Stream,Size,ProBFile,Options) :- Size=<0,!,
558		close(Stream),
559		(member(check_if_up_to_date(_,_),Options)
560		-> add_warning(parsercall,'Re-running parser as .prob file is empty: ',ProBFile)
561		% due to possible crash or CTRL-C of previous parser run
562		; add_internal_error('Generated .prob file is empty',ProBFile)
563		),fail.
564		check_prob_file_not_empty(_,_,_,_).
565
566		% check first character code
567		check_prob_file_first_code(Code,Stream,ProBFile,Options) :-
568		(valid_start_code(Code) -> true
569		; fastrw_start_code(Code)
570		-> close(Stream),
571		% we need to do: open(ProBFile,read,S,[type(binary)]),
572		(member(check_if_up_to_date(_,_),Options)
573		-> add_warning(parsercall,'Re-running parser as .prob file seems to be in new fast-rw format: ',ProBFile)
574		; add_error(parsercall,'Cannot load .prob file; it seems to be in new fast-rw format:',ProBFile)
575		),
576		fail
577		; add_message(parsercall,'Strange start character code in .prob file: ',[Code]) % probably syntax error will happen
578		).
579
580		fastrw_start_code(0'D). % typical start DSparser_version
581
582		valid_start_code(0'p). % from parser_version(_) term
583		valid_start_code(37). % percentage sign; appears when parser called with verbose flag
584		valid_start_code(47). % start of comment slash (inserted by user)
585		valid_start_code(39). % ' (inserted by user)
586		valid_start_code(32). % whitespace (inserted by user)
587		valid_start_code(8). % tab (inserted by user)
588		valid_start_code(10). % lf (inserted by user)
589		valid_start_code(13). % cr (inserted by user)
590
591		% --------------------
592
593		% use various read_term mechanisms depending on Options
594
595		safe_read_term(Stream,Options,File,Expecting,T) :-
596		catch(
597		safe_read_term2(Options,Stream,File,Expecting,T),
598		error(permission_error(_,_,_),ERR),
599		(
600		ajoin(['Permission error in .prob file trying to read ',Expecting,' term in ',File,':'],Msg),
601		add_internal_error(Msg,ERR),
602		fail
603		)).
604
605		:- use_module(tools_fastread,[read_term_from_stream/2, fastrw_read/3]).
606
607		safe_read_term2([use_fastrw|_],Stream,File,Expecting,Term) :- !,
608		fastrw_read(Stream,Term,Error),
609		(Error=false -> true
610		; ajoin(['.prob (fastrw) file has error in ',Expecting,' term:'],Msg),
611		add_internal_error(Msg,File),
612		fail
613		), functor(Term,F,N),debug_println(19,fast_read_term(F,N)).
614		safe_read_term2([use_fastread|_],Stream,File,Expecting,Term) :- !,
615		(read_term_from_stream(Stream,Term) -> true
616		; ajoin(['.prob file has Prolog syntax error in ',Expecting,' term:'],Msg),
617		add_internal_error(Msg,File), fail
618		).
619		safe_read_term2([_|Opts],Stream,File,Expecting,T) :- !,
620		safe_read_term2(Opts,Stream,File,Expecting,T).
621		safe_read_term2([],Stream,File,Expecting,T) :- % use regular SICStus Prolog reader
622		catch(read(Stream,T), error(E1,E2), (
623		ajoin(['.prob file (',File,') has error in ',Expecting,' term:'],Msg),
624		add_error(parser_call,Msg,error(E1,E2)),
625		fail
626		)).
627
628
629
630		% ------------------
631
632		% check if file was parsed with same parser version as currently in use by ProB
633		same_parser_version(parser_version(V), prob_parser_version(VB,GitSha)) :- !,
634		(V=VB -> true ; V=GitSha).
635		same_parser_version(end_of_file,_) :- !, debug_format(19,'.prob file is empty~n',[]).
636		same_parser_version(T,_) :-
637		add_internal_error('.prob file contains illegal parser_version term:',T),fail.
638
639		load_b_machine_list_of_facts_as_term(Facts,Machine) :-
640		read_machine_term_from_list_of_facts(Facts,_,Machine).
641		read_machine_term_from_list_of_facts(Facts,VersionTerm,complete_machine(MainName,Machines,FileList)) :-
642		(select(parser_version(VERS),Facts,F2) -> VersionTerm = parser_version(VERS)
643		; add_internal_error('No parser_version available',read_machine_from_list_of_facts),
644		F2=Facts, VersionTerm = unknown),
645		(select(classical_b(MainName,FileList),F2,F3) -> true
646		; add_internal_error('No classical_b file information available',read_machine_from_list_of_facts),
647		fail),
648		debug_println(9,loading_classical_b(VersionTerm,MainName,FileList)),
649		include(is_machine_term,F3,F4),
650		maplist(get_machine_term,F4,Machines).
651
652		is_machine_term(machine(_M)).
653		get_machine_term(machine(M),M).
654
655		load_b_machine_probfile_as_term(ProBFile, Machine) :-
656		load_b_machine_probfile_as_term(ProBFile, [], Machine).
657
658		load_b_machine_probfile_as_term(ProBFile, Options, Machine) :-
659		debug_println(9,consulting(ProBFile)),
660		( read_machine_term_from_file(ProBFile,_VersionTerm,Options,Machine) -> true
661		; add_error(parsercall,'Failed to read parser output: wrong format?',ProBFile),fail).
662
663		read_machines(S,ProBFile,Options,Machines,MainName,Files) :-
664		safe_read_term(S,Options,ProBFile,machine,Term),
665		%, write_term(Term,[max_depth(5),numbervars(true)]),nl,
666		( Term == end_of_file ->
667		Machines = []
668		; Term = classical_b(M,F) ->
669		((M,F)=(MainName,Files) -> true ; add_internal_error('Inconsistent classical_b fact: ',classical_b(M,F))),
670		(member(check_if_up_to_date(MainFileName,ProbTime),Options)
671		-> debug_format(9,'Checking if .prob file up-to-date for subsidiary files and if it was generated for ~w~n',[MainFileName]),
672		all_older(Files, ProbTime), % avoid reading rest if subsidiary source files not all_older !
673		(Files = [File1|_],
674		same_file_name(MainFileName,File1) -> true
675		; format('Re-parsing: .prob file created for different source file:~n ~w~n',[MainFileName]),
676		% this can happen, e.g., when we have M.def and M.mch and we previously loaded the other file
677		Files = [File1|_],
678		format(' ~w~n',[File1]),
679		fail
680		)
681		; true),
682		read_machines(S,ProBFile,Options,Machines,MainName,Files)
683		; Term = machine(M) ->
684		Machines = [M|Mrest],
685		read_machines(S,ProBFile,Options,Mrest,MainName,Files)
686		).
687
688
689		% checks if all files that the prob-file depends on
690		% are older than the prob-file
691		dont_need_compilation(Filename,ProB,Machine,LoadResult,Options) :-
692		file_exists(Filename),
693		catch( ( get_parser_version(Version,GitSha),
694		file_property(Filename, modify_timestamp, BTime),
695		debug_format(9, 'Parser Version: ~w, Filename Timestamp: ~w : ~w~n',[Version,Filename,BTime]),
696		file_exists(ProB), % the .prob file exists
697		file_property(ProB, modify_timestamp, ProbTime),
698		debug_format(9, '.prob Timestamp: ~w : ~w~n',[ProB,ProbTime]),
699		% print(time_stamps(ProB,ProbTime,Filename,BTime)),nl,
700		BTime < ProbTime, % .mch file is older than .prob file
701		file_property(ProB,size_in_bytes,Size),
702		(Size>0 -> true
703		; debug_mode(on),
704		add_message(parsercall,'.prob file is empty; parsing again',ProB),
705		% possibly due to crash or error before, cf second run of test 254
706		fail),
707		check_version_and_read_machine(Filename,ProB, ProbTime, Version, GitSha, Machine,Options),
708		%Machine = complete_machine(_,_,_),
709		LoadResult = loaded),
710		error(A,B),
711		(debug_println(9,error(A,B)),
712		(A=resource_error(memory)
713		-> add_error(load_b_machine,'Insufficient memory to load file.\nTry starting up ProB with more memory\n (e.g., setting GLOBALSTKSIZE=500M before starting ProB).'),
714		LoadResult=A
715		; fail))).
716
717		% check that all included files are older than the .prob file (ProbTime):
718		all_older([],_).
719		all_older([File|Rest],ProbTime) :-
720		(file_exists(File)
721		-> file_property(File, modify_timestamp, BTime),
722		debug_format(9,' Subsidiary File Timestamp: ~w:~w~n',[File,BTime]),
723		( BTime < ProbTime -> true
724		; format('File has changed : ~w : ~w~n',[File,BTime]),
725		fail )
726		; virtual_dsl_file(File) -> debug_format(9,'Virtual file generated by DSL translator: ~w~n',[File])
727		; debug_format(20,'File does not exist anymore: ~w; calling parser.~n',[File]),fail),
728		all_older(Rest,ProbTime).
729
730		virtual_dsl_file(File) :- atom_codes(File,Codes),
731		Codes = [95|_], % file name starts with _ underscore
732		nonmember(47,Codes), % no slash
733		nonmember(92,Codes). % no backslash
734
735		:- use_module(system_call).
736
737		get_extra_args_list(ExtraArgs) :-
738		get_preference(jvm_parser_additional_args,ExtraArgsStr),
739		ExtraArgsStr \= '',
740		atom_codes(ExtraArgsStr,C),
741		split_chars(C," ",CA),
742		maplist(atom_codes,ExtraArgs,CA).
743
744		jvm_options -->
745		({get_preference(jvm_parser_heap_size_mb,Heap), Heap>0} ->
746		{ajoin(['-Xmx',Heap,'m'],HeapOpt)},
747		[HeapOpt]
748		;
749		% comment in to simulate low-memory situations
750		% use -Xmx221500000m instead to force exception and test ProB's response
751		[] %['-Xmx20m']
752		),
753
754		({get_extra_args_list(ExtraArgs)} ->
755		{debug_format(19,'Using additional arguments for JVM (JVM_PARSER_ARGS): ~w~n',[ExtraArgs])},
756		ExtraArgs
757		% use the former LARGE_JVM / use_large_jvm_for_parser by default
758		% if we are running on a 64-bit system
759		% FIXME Is it intentional that this option is not added if JVM_PARSER_ARGS is set?
760		; {platform_is_64_bit} -> ['-Xss5m'] % default stacksize; set to -Xss150k to mimic low stack setting
761		; []
762		).
763
764		parser_jvm_options -->
765		{get_PROBPATH(PROBPATH), atom_concat('-Dprob.stdlib=', PROBPATH, Stdlibpref)},
766		[Stdlibpref],
767		jvm_options.
768
769
770		% we could do something like this: or allow user to provide list of JVM options
771		%get_gc_options([]) :- !,get_preference(jvm_parser_aggressive_gc,true).
772		%get_gc_options(['-XX:GCTimeRatio=19', '-XX:MinHeapFreeRatio=20', '-XX:MaxHeapFreeRatio=30']).
773		% see https://stackoverflow.com/questions/30458195/does-gc-release-back-memory-to-os
774
775		parser_cli_options -->
776		%% ['-v'], % comment in for verbose, -time for timing info
777		({debug_mode(on)} -> ['-v', '-time'] ; []),
778
779		% useful for very large data validation machines
780		({get_preference(jvm_parser_position_infos,true)} -> ['-lineno'] ; []),
781
782		%( get_preference(jvm_parser_fastrw,false) ; parser_version_at_least(2,12,0) )
783		% we cannot call: parser_version_at_least(2,12,0) as parser not yet started
784		% older parsers were printing comments into the binary fastrw output; TODO: perform check later
785		({get_preference(jvm_parser_fastrw,true)} -> ['-fastprolog'] ; ['-prolog']),
786
787		% -compactpos enables new p3, p4, p5 position terms and disables node numbering
788		['-prepl', '-compactpos'].
789
790		parser_command_args(native(NativeCmd), NativeCmd) -->
791		parser_jvm_options,
792		parser_cli_options.
793		parser_command_args(java_jar(NativeCmd,JarPath), NativeCmd) -->
794		parser_jvm_options,
795		['-jar', JarPath],
796		parser_cli_options.
797
798		% ensure that the console Java process is running
799		ensure_console_parser_launched :-
800		catch(parse_formula("1",_), E, (
801		add_internal_error('Cannot launch console parser (probcliparser.jar)',E),
802		fail
803		)).
804
805		parser_is_launched :-
806		java_parser_process(_,_,_,_).
807
808
809		% TO DO: also store output stream for debugging messages
810		get_console_parser(Stream,Out,Err) :-
811		java_parser_process(PID,Stream,Out,Err),
812		% On SICStus, calling is_process seams to be unreliable (if the process has crashed)
813		% and process_wait does not always work either,
814		% so first check if in and output streams are still available.
815		\+ at_end_of_stream(Stream),
816		% On SWI, at_end_of_stream doesn't detect broken pipes,
817		% so additionally also check that the process has not exited/crashed.
818		process_wait(PID,timeout,[timeout(0)]),
819		!,
820		(at_end_of_stream(Err)
821		-> add_error(parsercall,'Java process not running'),
822		read_lines_and_add_as_error(Stream)
823		; true).
824		get_console_parser(Stream,Out,Err) :-
825		clear_old_console_parsers,
826		get_java_command_for_parser(ParserCmd),
827		phrase(parser_command_args(ParserCmd, NativeCmd), FullArgs),
828		debug_println(19,launching_java_console_parser(NativeCmd,FullArgs)),
829		debug_print_system_call(NativeCmd,FullArgs),
830		system_call_keep_open(NativeCmd,FullArgs,PID,_In,Out,Err,[]), % note: if probcliparser.jar does not exist we will not yet get an error here !
831		debug_println(9,java_console_parser_launched(PID)),
832		% read first line to get port number
833		safe_read_line(Out,Err,1,[],PortTerm),
834		connect_to_console_parser_on_port(PortTerm,PID,Out,Err,Stream),
835		!.
836		get_console_parser(_,_,_) :- missing_parser_diagnostics, fail.
837
838
839
840
841		connect_to_console_parser_on_port(PortTerm,PID,Out,Err,Stream) :-
842		catch(
843		socket_client_open('':PortTerm, Stream, [type(text),encoding(utf8)]),
844		Exc, %error(system_error,system_error(E)), % SPIO_E_NET_HOST_NOT_FOUND
845		(
846		ajoin(['Exception while opening parser socket on port ', PortTerm,
847		' (possibly an error occurred during startup of the parser): '],Msg),
848		add_internal_error(Msg,Exc),
849		% e.g., not enough memory to start parser and wait for socket connection
850		read_lines_and_add_as_error(Err), % try and read additional info;
851		% if we set the stack size to be very small (-Xss20k) we get: Error: Could not create the Java Virtual Machine
852		fail
853		)),
854		assertz(java_parser_process(PID,Stream,Out,Err)).
855
856		% connect to a separately started parser
857		% allow to connect to a separately started java command line parser (java -jar probcliparser.jar -prepl)
858		connect_to_external_console_parser_on_port(PortNumber) :-
859		clear_old_console_parsers,
860		format('Trying to connect to external parser on port ~w~n',[PortNumber]),
861		Out=user_input, Err=user_input,
862		(connect_to_console_parser_on_port(PortNumber,external_process,Out,Err,_)
863		-> format('Connected to parser on port ~w~n',[PortNumber])
864		; add_error(parsercall,'Could not connect to parser on port:',PortNumber)
865		).
866
867		clear_old_console_parsers :-
868		retract(java_parser_process(PID,_,_,_)),
869		parser_process_release(PID),
870		fail.
871		clear_old_console_parsers.
872
873		parser_process_release(external_process) :- !.
874		parser_process_release(PID) :- process_release(PID).
875
876		% useful to try and free up memory
877		% alternatively we could add some JVM options: -XX:GCTimeRatio=19 -XX:MinHeapFreeRatio=20 -XX:MaxHeapFreeRatio=30
878		% see https://stackoverflow.com/questions/30458195/does-gc-release-back-memory-to-os
879		release_console_parser :-
880		(java_parser_process(PID,Stream,_,_),
881		PID \= external_process
882		-> format('Releasing Java parser id=~w (note: access to DEFINITIONS is lost)~n',[PID]),
883		write(Stream,'halt'), nl(Stream),
884		flush_output(Stream), % handled in Java in runPRepl in CliBParser.java;
885		retract(java_parser_process(PID,_,_,_)),
886		parser_process_release(PID) % or should we call process_kill ?
887		%process_kill(PID)
888		% Note: parser maybe launched again, but then not have access to DEFINITIONS
889		; true).
890
891		:- use_module(runtime_profiler,[profile_single_call/3]).
892		call_console_parser(Filename, ProB) :-
893		profile_single_call('$parsing',unknown,parsercall:call_console_parser2(Filename, ProB)).
894		call_console_parser2(Filename, ProB) :-
895		update_jvm_parser_preferences,
896		get_console_parser(Stream,Out,Err),
897
898		% path to the .prob file
899		replace_windows_path_backslashes(ProB,ProBW),
900		% the input file
901		replace_windows_path_backslashes(Filename,FilenameW),
902		% call PREPL 'machine' command
903		debug_format(4,'PREPL command: machine~n~w~n~w~n',[FilenameW,ProBW]),
904		format(Stream,'machine~n~w~n~w~n',[FilenameW,ProBW]), % tell parser to write output to ProBW .prob file
905		flush_output(Stream),
906
907		%% WARNING: if the java parser writes too much output on the out stream it will block
908		%% until its output is read and we have a deadlock !
909		%% hence we use safe_polling_read_line
910		safe_polling_read_line(Stream,Out,Err,1,[],Term),
911
912		display_pending_outputs(Out,user_output),
913		handle_console_parser_result(Term,Err).
914
915
916		safe_read_line(Out,Err,LineNr,SoFar,Term) :-
917		safe_read_line_aux(read_line,Out,Err,LineNr,SoFar,Term).
918
919		safe_read_line_if_ready(Out,Err,LineNr,SoFar,Term) :-
920		safe_read_line_aux(read_line_if_ready,Out,Err,LineNr,SoFar,Term).
921
922		% a version that will check every second if there is output to be read
923		safe_polling_read_line(Stream,_Out,Err,LineNr,SoFar,Term) :-
924		stream_ready_to_read(Stream,2),!, % try for two seconds
925		safe_read_line_aux(read_line,Stream,Err,LineNr,SoFar,Term).
926		safe_polling_read_line(Stream,Out,Err,LineNr,SoFar,Term) :-
927		% this should normally not happen unless we have a debugging version of the parser
928		debug_format(19,'Parser not responded yet, trying to read its output~n',[]),
929		display_pending_outputs(Out,user_output),
930		read_lines_and_add_as_error(Err),
931		safe_polling_read_line(Stream,Out,Err,LineNr,SoFar,Term).
932
933		safe_read_line_aux(Pred,Out,Err,LineNr,SoFar,Term) :-
934		catch(call(Pred,Out,Codes),Exception, % read another line
935		(add_error(parsercall,'Exception while reading next line: ',Exception),
936		read_lines_and_add_as_error(Err),
937		display_pending_outputs(user_error,Out),
938		throw(Exception))),
939		Codes \= end_of_file, !, % happens if parser crashed and stream is closed
940		append(SoFar,Codes,NewCodes),
941		catch(my_read_from_codes(NewCodes,Term,Out,Err),Exception,
942		safe_read_exception(Out,Err,LineNr,Exception,NewCodes,Term)).
943		safe_read_line_aux(_Pred,_Out,Err,_LineNr,CodesSoFar,_) :-
944		safe_name(T,CodesSoFar),
945		add_error(parsercall,'Unexpected error while parsing machine: ',T),
946		read_lines_and_add_as_error(Err),fail.
947
948
949		safe_read_exception(Out,_,1,_Exception,CodesSoFar,_Term) :- append("Error",_,CodesSoFar),!,
950		% probably some Java error, we do not obtain a correct Prolog term, but probably something like:
951		% "Error occurred during initialization of VM"
952		safe_name(T,CodesSoFar),
953		add_error(parsercall,'Java error while parsing machine: ',T),
954		read_lines_and_add_as_error(Out),fail.
955		safe_read_exception(Out,Err,LineNr,error(syntax_error(M),_),CodesSoFar,Term) :- LineNr<10, % avoid infinite loop in case unexpected errors occur which cannot be solved by reading more input lines
956		!,
957		%(debug:debug_mode(off) -> true ; format('Syntax error in parser result (line ~w): ~w~nTrying to read another line.~n',[LineNr,M])),
958		add_warning(parsercall,'Syntax error in parser result; trying to read another line. Line:Error = ',LineNr:M),
959		L1 is LineNr+1,
960		safe_read_line_if_ready(Out,Err,L1,CodesSoFar,Term). % try and read another line; we assume the syntax error is because the TERM is not complete yet and transmitted on multiple lines (Windows issue)
961		safe_read_exception(_,_,_LineNr,parse_errors(Errors),_CodesSoFar,_Term) :- !,
962		debug_println(4,read_parse_errors(Errors)),
963		throw(parse_errors(Errors)).
964		safe_read_exception(_,_,_LineNr,Exception,_CodesSoFar,_Term) :-
965		add_internal_error('Unexpected exception occurred during parsing: ',Exception),fail.
966		%safe_name(T,CodesSoFar), add_error_fail(parsercall,'Unexpected error while parsing machine: ',T).
967
968		safe_name(Name,Codes) :- var(Name),Codes == end_of_file,!,
969		%add_internal_error('Parser does not seem to be available',''),
970		Name=end_of_file.
971		safe_name(Name,Codes) :- number(Name),!,
972		safe_number_codes(Name,Codes).
973		safe_name(Name,Codes) :-
974		catch(atom_codes(Name,Codes), E,
975		(print('Exception during atom_codes: '),print(E),nl,nl,throw(E))).
976
977		safe_number_codes(Name,Codes) :-
978		catch(number_codes(Name,Codes), E,
979		(print('Exception during number_codes: '),print(E),nl,nl,throw(E))).
980
981		% Note: As of parser version 2.9.28 commit ee2592d8ca2900b4e339da973920e034dff43658,
982		% all parse errors are reported as terms of the form
983		% parse_exception(Positions,Msg) where Positions is a list of pos/5 terms.
984		% The term formats preparse_exception(Tokens,Msg) (where Tokens is a list of none/0 or pos/3 terms)
985		% and parse_exception(Pos,Msg) (where Pos is a single none/0, pos/3 or pos/5 term)
986		% are no longer generated by the parser.
987		% The code for handling these old term formats can probably be removed soon.
988
989		% see also handle_parser_exception
990		%handle_console_parser_result(E,_) :- nl,print(E),nl,fail.
991		handle_console_parser_result(exit(0),_) :- !.
992		handle_console_parser_result(io_exception(Msg),_) :- !,
993		add_error_fail(parsercall,'Error while opening the B file: ',Msg).
994		handle_console_parser_result(compound_exception(List),ErrStream) :- !,
995		get_compound_exceptions(List,ErrStream,ParseErrors,[]),
996		throw(parse_errors(ParseErrors)).
997		handle_console_parser_result(preparse_exception(Tokens,Msg),_) :- !,
998		remove_msg_posinfo(Msg,SanitizedMsg,MsgPos),
999		findall(error(SanitizedMsg,Pos),member(Pos,Tokens),Errors1),
1000		(Errors1 = []
1001		-> /* if there are no error tokens: use pos. info from text Msg */
1002		Errors = [error(SanitizedMsg,MsgPos)]
1003		; Errors = Errors1),
1004		debug_println(4,preparse_exception_parse_errors(Tokens,Msg,Errors)),
1005		throw(parse_errors(Errors)).
1006		handle_console_parser_result(parse_exception([],Msg),_) :-
1007		atom(Msg), atom_codes(Msg,MC),
1008		append("StackOverflowError",_,MC),!,
1009		add_error(parsercall,'Java VM error while running parser: ',Msg),
1010		print_hint('Try increasing stack size for Java using the JVM_PARSER_ARGS preference (e.g.,"-Xss10m").'),
1011		fail.
1012		handle_console_parser_result(parse_exception(Positions,Msg),_) :-
1013		(Positions = [] ; Positions = [_|_]), !,
1014		remove_msg_posinfo(Msg,SanitizedMsg,MsgPos),
1015		findall(error(SanitizedMsg,Pos),member(Pos,Positions),Errors1),
1016		(Errors1 = []
1017		-> /* if there are no error tokens: use pos. info from text Msg */
1018		Errors = [error(SanitizedMsg,MsgPos)]
1019		; Errors = Errors1),
1020		debug_println(4,parse_exception_parse_errors(Positions,Msg,Errors)),
1021		throw(parse_errors(Errors)).
1022		handle_console_parser_result(parse_exception(Pos,Msg),_) :- !,
1023		remove_msg_posinfo_known(Msg,SanitizedMsg), %print(sanitized(SanitizedMsg)),nl,
1024		debug_println(4,parse_exception(Pos,Msg,SanitizedMsg)),
1025		throw(parse_errors([error(SanitizedMsg,Pos)])).
1026		handle_console_parser_result(exception(Msg),_) :- !,
1027		%add_error(bmachine,'Error in the classical B parser: ', Msg),
1028		remove_msg_posinfo(Msg,SanitizedMsg,Pos),
1029		debug_println(4,exception_in_parser(Msg,SanitizedMsg,Pos)),
1030		throw(parse_errors([error(SanitizedMsg,Pos)])).
1031		handle_console_parser_result(end_of_file,Err) :- !,
1032		% probably NullPointerException or similar in parser; no result on StdOut
1033		debug_println(9,end_of_file_on_parser_output_stream),
1034		format(user_error,'Detected abnormal termination of B Parser~n',[]), % print in case we block
1035		read_line_if_ready(Err,Err1),
1036		(Err1=end_of_file -> Msg = 'Abnormal termination of B Parser: EOF on streams'
1037		; append("Abnormal termination of B Parser: ",Err1,ErrMsgCodes),
1038		safe_name(Msg,ErrMsgCodes),
1039		read_lines_and_add_as_error(Err) % also show additional error infos
1040		),
1041		throw(parse_errors([error(Msg,none)])).
1042		handle_console_parser_result(compound_exception(Exs),_) :- !,
1043		maplist(handle_parser_exception_aux,Exs,ExAuxs),
1044		debug_println(4,compound_exception(Exs,ExAuxs)),
1045		throw(parse_errors(ExAuxs)).
1046		handle_console_parser_result(Term,_) :- !,
1047		write_term_to_codes(Term,Text,[]),
1048		safe_name(Msg,Text),
1049		%add_error(bmachine,'Error in the classical B parser: ', Msg),
1050		remove_msg_posinfo(Msg,SanitizedMsg,Pos),
1051		debug_println(4,unknown_error_term(Term,SanitizedMsg,Pos)),
1052		throw(parse_errors([error(SanitizedMsg,Pos)])).
1053
1054		% get all compound exceptions as a single result to be thrown once later:
1055		get_compound_exceptions([],_) --> [].
1056		get_compound_exceptions([Err1|T],ErrStream) -->
1057		{handle_and_catch(Err1,ErrStream,ParseErrors) },
1058		ParseErrors,
1059		get_compound_exceptions(T,ErrStream).
1060
1061		handle_and_catch(Exception,ErrStream,ParseErrors) :-
1062		catch(
1063		(handle_console_parser_result(Exception,ErrStream) -> ParseErrors=[] ; ParseErrors=[]),
1064		parse_errors(Errors1),
1065		ParseErrors=Errors1).
1066
1067		% now replaced by remove_msg_posinfo:
1068		%extract_position_info(Text,pos(Row,Col,Filename)) :-
1069		% atom_codes(Text,Codes),
1070		% epi(Row,Col,Filename,Codes,_),!.
1071		%extract_position_info(_Text,none).
1072
1073		:- assert_must_succeed((parsercall:epi(R,C,F,"[2,3] xxx in file: /usr/lib.c",[]), R==2,C==3,F=='/usr/lib.c')).
1074		:- assert_must_succeed((parsercall:epi(R,C,F,"[22,33] xxx yyy ",_), R==22,C==33,F=='unknown')).
1075
1076		% we expect error messages to start with [Line,Col] information
1077		epi(Row,Col,Filename) --> " ",!,epi(Row,Col,Filename).
1078		epi(Row,Col,Filename) --> "[", epi_number(Row),",",epi_number(Col),"]",
1079		(epi_filename(Filename) -> [] ; {Filename=unknown}).
1080		epi_number(N) --> epi_numbers(Chars),{safe_number_codes(N,Chars)}.
1081		epi_numbers([C|Rest]) --> [C],{is_number(C)},epi_numbers2(Rest).
1082		epi_numbers2([C|Rest]) --> [C],{is_number(C),!},epi_numbers2(Rest).
1083		epi_numbers2("") --> !.
1084	?	is_number(C) :- member(C,"0123456789"),!.
1085		epi_filename(F) --> " in file: ",!,epi_path2(Chars),{safe_name(F,Chars)}.
1086		epi_filename(F) --> [_], epi_filename(F).
1087		epi_path2([C|Rest]) --> [C],!,epi_path2(Rest). % assume everything until the end is a filename
1088		epi_path2([]) --> [].
1089
1090		:- assert_must_succeed((parsercall:remove_rowcol(R,C,"[22,33] xxx yyy ",_), R==22,C==33)).
1091		% remove parser location info from message to avoid user clutter
1092		remove_rowcol(Row,Col) --> " ",!, remove_rowcol(Row,Col).
1093		remove_rowcol(Row,Col) --> "[", epi_number(Row),",",epi_number(Col),"]".
1094
1095		:- assert_must_succeed((parsercall:remove_filename(F,C,"xxx yyy in file: a.out",R), F == 'a.out', C == "xxx yyy", R==[])).
1096		remove_filename(F,[]) --> " in file: ",!,epi_path2(Chars),{safe_name(F,Chars)}.
1097		remove_filename(F,[C|T]) --> [C], remove_filename(F,T).
1098
1099		:- assert_must_succeed((parsercall:remove_filename_from_codes("xxx yyy in file: a.out",F,C), F == 'a.out', C == "xxx yyy")).
1100		:- assert_must_succeed((parsercall:remove_filename_from_codes("xxx yyy zzz",F,C), F == 'unknown', C == "xxx yyy zzz")).
1101		remove_filename_from_codes(Codes,F,NewCodes) :-
1102		(remove_filename(F,C1,Codes,C2) -> append(C1,C2,NewCodes) ; F=unknown, NewCodes=Codes).
1103
1104		% obtain position information from a message atom and remove the parts from the message at the same time
1105		remove_msg_posinfo_known(Msg,NewMsg) :- remove_msg_posinfo(Msg,NewMsg,_,pos_already_known).
1106		remove_msg_posinfo(Msg,NewMsg,Pos) :- remove_msg_posinfo(Msg,NewMsg,Pos,not_known).
1107		remove_msg_posinfo(Msg,NewMsg,Pos,AlreadyKnown) :- %print(msg(Msg,AlreadyKnown)),nl,
1108		atom_codes(Msg,Codes),
1109		(remove_rowcol(Row,Col,Codes,RestCodes)
1110		-> Pos=pos(Row,Col,Filename),
1111		remove_filename_from_codes(RestCodes,Filename,NewCodes)
1112		; AlreadyKnown==pos_already_known ->
1113		Pos = none,
1114		remove_filename_from_codes(Codes,_Filename2,NewCodes)
1115		;
1116		NewCodes=Codes, Pos=none
1117		% do not remove filename: we have not found a position and cannot return the filename
1118		% see, e.g., public_examples/B/Tickets/Hansen27_NestedMchErr/M1.mch
1119		),
1120		!,
1121		atom_codes(NewMsg,NewCodes).
1122		remove_msg_posinfo(M,M,none,_).
1123
1124
1125		% ----------------------
1126
1127		parser_command_supported(_) :-
1128		prob2_call_back_available(_), % TODO: support at least setoption in parser callback in ProB2
1129		!,
1130		fail.
1131		parser_command_supported(Command) :-
1132		parser_version_at_least(2,12,2),
1133		!,
1134		query_command_supported(Command,true).
1135		parser_command_supported(Command) :-
1136		(Command = fastprolog
1137		; Command = compactpos
1138		; Command = verbose
1139		; Command = checkname
1140		; Command = lineno
1141		),
1142		!,
1143		parser_version_at_least(2,12,0).
1144
1145		:- dynamic query_command_supported_cached/2.
1146
1147		query_command_supported(Command,Res) :-
1148		query_command_supported_cached(Command,Res),
1149		!.
1150		query_command_supported(Command,Res) :-
1151		get_console_parser(Stream,_Out,Err),
1152		!,
1153		write(Stream,'commandsupported'), nl(Stream),
1154		write(Stream,Command), nl(Stream),
1155		flush_output(Stream),
1156		read_line(Stream,CodesIn),
1157		my_read_from_codes(CodesIn,Res,Stream,Err),
1158		assertz(query_command_supported_cached(Command,Res)).
1159
1160		% java_parser_version(VersionStr) :- java_parser_version(VersionStr,_,_,_,_,_).
1161
1162		parser_version_at_least(RV1,RV2,RV3) :-
1163		get_parser_version(_,V1,V2,V3,_,_),
1164		lex_leq([RV1,RV2,RV3],[V1,V2,V3]).
1165
1166		lex_leq([V1|_],[VV1|_]) :- V1 < VV1,!.
1167		lex_leq([V1|T1],[V1|T2]) :- lex_leq(T1,T2).
1168		lex_leq([],_).
1169
1170
1171		get_parser_version(VersionStr) :- get_parser_version(VersionStr,_).
1172		get_parser_version(VersionStr,GitSha) :- get_parser_version(VersionStr,_,_,_,_,GitSha).
1173
1174		get_parser_version(VersionStr,V1,V2,V3,SNAPSHOT,GitSha) :- java_parser_version(VersionStr,V1,V2,V3,SNAPSHOT,GitSha),!.
1175		get_parser_version(VersionStr,V1,V2,V3,SNAPSHOT,GitSha) :-
1176		get_version_from_parser(VersionStr),
1177		!,
1178	?	(get_version_numbers(VersionStr,V1,V2,V3,SNAPSHOT,GitSha)
1179		-> assertz(java_parser_version(VersionStr,V1,V2,V3,SNAPSHOT,GitSha)),
1180		debug_format(19,'Parser version recognized ~w.~w.~w (SNAPSHOT=~w)~n',[V1,V2,V3,SNAPSHOT])
1181		; assertz(java_parser_version(VersionStr,'?','?','?','?','?'))
1182		).
1183		get_parser_version(_Vers,_V1,_V2,_V3,_SNAPSHOT,_GitSha) :-
1184		(real_error_occurred -> true % already produced error messages in get_version_from_parser
1185		; add_error(get_parser_version,'Could not get parser version.')),
1186		%missing_parser_diagnostics, % already called if necessary by get_version_from_parser
1187		fail.
1188
1189		:- use_module(probsrc(tools),[split_atom/3,atom_to_number/2]).
1190		% newer parsers generate a version string like 2.9.27-GITSHA or 2.9.27-SNAPSHOT-GITSHA; older ones just GITSHA
1191		get_version_numbers(VersionStr,V1,V2,V3,SNAPSHOT,GitSha) :-
1192		split_atom(VersionStr,['.'],List),
1193		[AV1,AV2,AV3T] = List,
1194		split_atom(AV3T,['-'],List2),
1195		[AV3,Suffix1|T] = List2,
1196	?	atom_to_number(AV1,V1),
1197	?	atom_to_number(AV2,V2),
1198	?	atom_to_number(AV3,V3),
1199		(Suffix1 = 'SNAPSHOT' -> SNAPSHOT=true, [GitSha]=T
1200		; T=[], SNAPSHOT=false, GitSha=Suffix1).
1201
1202
1203		get_version_from_parser(Version) :-
1204		get_console_parser(Stream,Out,Err),
1205		write(Stream,'version'), nl(Stream),
1206		flush_output(Stream),
1207		read_line(Stream,Text), % if parser cannot be started we receive end_of_file; length will fail
1208		(Text = end_of_file -> add_error(parsercall,'Could not get parser version: '),
1209		read_lines_and_add_as_error(Err),fail
1210		; length(Text,Length),
1211		( append("Error",_,Text)
1212		-> atom_codes(ErrMsg,Text),
1213		add_error(parsercall,'Error getting parser version: ',ErrMsg),
1214		read_lines_and_add_as_error(Stream),fail
1215		; Length < 100 -> atom_codes(Version,Text)
1216		; prefix_length(Text,Prefix,100),
1217		append(Prefix,"...",Full),
1218		safe_name(Msg,Full),
1219		add_error_fail(parsercall, 'B parser returned unexpected version string: ', Msg))
1220		),
1221		display_pending_outputs(Out,user_output).
1222
1223		:- use_module(library(sockets),[socket_select/7]).
1224		% check if a stream is ready for reading
1225		stream_ready_to_read(Out) :- stream_ready_to_read(Out,1). % wait 1 second, off: wait forever
1226		stream_ready_to_read(Out,TO) :- var(Out),!,
1227		add_internal_error('Illegal stream: ',stream_ready_to_read(Out,TO)),fail.
1228		stream_ready_to_read(Out,TO) :-
1229		socket_select([],_, [Out],RReady, [],_, TO), % wait TO sec at most %print(ready(Out,RReady)),nl,
1230		RReady == [Out].
1231
1232
1233		read_lines_and_add_as_error(Out) :- read_lines_until_eof(Out,false,ErrMsgCodes,[]),
1234		(ErrMsgCodes=[] -> true
1235		; ErrMsgCodes=[10] -> true % just a single newline
1236		; ErrMsgCodes=[13] -> true % ditto
1237		; safe_name(ErrMsg,ErrMsgCodes),
1238		add_error(parsercall,'Additional information: ',ErrMsg),
1239		analyse_java_error_msg(ErrMsgCodes)
1240		).
1241
1242		% analyse error messages from the JVM; providing possible solutions:
1243		analyse_java_error_msg(ErrMsgCodes) :-
1244		append([_,"java.lang.OutOfMemoryError",_],ErrMsgCodes),!,
1245		% a typical message contains: Exception in thread "main" java.lang.OutOfMemoryError: GC overhead limit exceeded
1246		% or: Exception in ...: Java heap space
1247		print_hint('Try increasing memory for Java by setting the JVM_PARSER_HEAP_MB preference.'),
1248		print_hint('You can also provide custom JVM arguments using the JVM_PARSER_ARGS preference.').
1249		analyse_java_error_msg(ErrMsgCodes) :-
1250		append([_,"java.lang.StackOverflowError",_],ErrMsgCodes),!,
1251		print_hint('Try increasing stack size for Java using the JVM_PARSER_ARGS preference (e.g.,"-Xss10m").').
1252		analyse_java_error_msg(_).
1253
1254		print_hint(Msg) :- format_with_colour_nl(user_error,[blue],'~w',[Msg]).
1255
1256		read_line_if_ready(Stream,Line) :- stream_ready_to_read(Stream), !, read_line(Stream,Line).
1257		read_line_if_ready(_,end_of_file). % pretend we are at the eof
1258
1259		read_lines_until_eof(Out,NewlineRequired) --> {read_line_if_ready(Out,Text)},
1260		!,
1261		({Text = end_of_file} -> []
1262		; ({NewlineRequired==true} -> "\n" ; []),
1263		Text, %{format("read: ~s~n",[Text])},
1264		read_lines_until_eof(Out,true)).
1265		read_lines_until_eof(_Out,_) --> [].
1266
1267		% display pending output lines from a stream
1268		display_pending_outputs(OutStream,ToStream) :- stream_ready_to_read(OutStream,0), !, read_line(OutStream,Line),
1269		(Line=end_of_file -> true
1270		; format(ToStream,' =parser-output=> ~s~n',[Line]),
1271		display_pending_outputs(OutStream,ToStream)).
1272		display_pending_outputs(_,_).
1273
1274		:- use_module(tools,[get_tail_filename/2]).
1275		get_java_command_for_parser(native(GraalNativeCmd)) :-
1276		(parser_location(GraalNativeCmd)
1277		-> get_tail_filename(GraalNativeCmd,'cliparser'),
1278		(file_exists(GraalNativeCmd) -> true
1279		; add_warning(parsercall,'Path to parser points to non-existant compiled GraalVM binary: ',GraalNativeCmd)
1280		)
1281		; fail, % comment out fail to enable auto-detection of cliparser in lib folder
1282		library_abs_name('cliparser',GraalNativeCmd),
1283		file_exists(GraalNativeCmd)
1284		),
1285		format('Using GRAAL native parser at ~w~n',[GraalNativeCmd]),
1286		!.
1287		get_java_command_for_parser(java_jar(JavaCmdW,JarPathW)) :-
1288		(parser_location(JarPath) -> true ; library_abs_name('probcliparser.jar',JarPath)),
1289		get_java_command_path(JavaCmdW),
1290		replace_windows_path_backslashes(JarPath,JarPathW).
1291
1292		parser_location(PathToParser) :- get_preference(path_to_java_parser,PathToParser), PathToParser \= ''.
1293
1294		% a predicate to check whether we have correct java version number and whether java seems to work ok
1295		% ResultStatus=compatible if everything is ok
1296		check_java_version(VersionCheckResult,ResultStatus) :- get_java_fullversion(Version),!,
1297		check_java_version_aux(Version,VersionCheckResult,ResultStatus).
1298		check_java_version(VersionCheckResult,error) :- get_java_command_for_parser(java_jar(JavaCmdW,JarPathW)),!,
1299		ajoin(['*** Unable to launch java command: ',JavaCmdW,' (classpath: ',JarPathW,')!'],VersionCheckResult).
1300		check_java_version('*** Unable to launch Java or get path to java command!',error). % should not happen
1301
1302		check_java_version_aux(VersionCodes,VersionCheckResult,ResultStatus) :-
1303		get_java_fullversion_numbers(VersionCodes,V1,V2,V3Atom),!,
1304		check_java_version_aux2(V1,V2,V3Atom,VersionCheckResult,ResultStatus).
1305		check_java_version_aux(VersionCodes,VersionCheckResult,error) :-
1306		atom_codes(VersionA,VersionCodes),
1307		ajoin(['*** Unable to identify Java version number: ',VersionA, ' !'],VersionCheckResult).
1308
1309		check_java_version_aux2(V1,V2,V3Atom,VersionCheckResult,compatible) :- java_version_ok_for_parser(V1,V2,V3Atom),
1310		get_java_version(_),!, % if get_java_version fails, this is an indication that Java not fully installed with admin rights
1311		ajoin(['Java is correctly installed and version ',V1,'.',V2,'.',V3Atom,
1312		' is compatible with ProB requirements (>= 1.7).'],VersionCheckResult).
1313		check_java_version_aux2(V1,V2,V3Atom,VersionCheckResult,error) :- java_version_ok_for_parser(V1,V2,V3Atom),!,
1314		ajoin(['*** Java version ',V1,'.',V2,'.',V3Atom,
1315		' is compatible with ProB requirements (>= 1.7) ',
1316		'but does not seem to be correctly installed: reinstall Java with admin rights!'],VersionCheckResult).
1317		check_java_version_aux2(V1,V2,V3Atom,VersionCheckResult,incompatible) :-
1318		get_java_version(_),!,
1319		ajoin(['*** Java is correctly installed but version ',V1,'.',V2,'.',V3Atom,
1320		' is *not* compatible with ProB requirements (>= 1.7)!'],VersionCheckResult).
1321		check_java_version_aux2(V1,V2,V3Atom,VersionCheckResult,error) :-
1322		ajoin(['*** Java is not correctly installed and version ',V1,'.',V2,'.',V3Atom,
1323		' is *not* compatible with ProB requirements (>= 1.7)!'],VersionCheckResult).
1324
1325
1326		% we need Java 1.7 or higher
1327		java_version_ok_for_parser(V1,_V2,_) :- V1>1.
1328		java_version_ok_for_parser(1,V2,_) :- V2>=7.
1329
1330		get_java_fullversion(V1,V2,V3Atom) :-
1331		get_java_fullversion(VersionCodes),
1332		get_java_fullversion_numbers(VersionCodes,VV1,VV2,VV3),!,
1333		V1=VV1, V2=VV2, V3Atom=VV3.
1334
1335		:- assert_must_succeed((parsercall:get_java_fullversion_numbers("openjdk full version \"1.8.0_312\"",V1,V2,V3),
1336		V1==1, V2==8, V3=='0_312')).
1337		:- assert_must_succeed((parsercall:get_java_fullversion_numbers("openjdk full version \"15+36-1562\"",V1,V2,V3),
1338		V1==1, V2==15, V3=='36-1562')).
1339		:- assert_must_succeed((parsercall:get_java_fullversion_numbers("java full version \"17.0.1+12-LTS-39\"",V1,V2,V3),
1340		V1==1, V2==17, V3=='0.1+12-LTS-39')). % Oracle JDK on macOS
1341		:- use_module(tools,[split_chars/3]).
1342		get_java_fullversion_numbers(VersionCodes,V1,V2,V3Atom) :-
1343		append("java full version """,Tail,VersionCodes), !,
1344		get_java_fullversion_numbers_aux(Tail,V1,V2,V3Atom).
1345		get_java_fullversion_numbers(VersionCodes,V1,V2,V3Atom) :-
1346		append("openjdk full version """,Tail,VersionCodes), !,
1347		get_java_fullversion_numbers_aux(Tail,V1,V2,V3Atom).
1348		get_java_fullversion_numbers_aux(Tail,1,V2,V3Atom) :-
1349		% new version scheme (https://openjdk.java.net/jeps/223), leading 1 dropped, 13+33 stands for 1.13.33
1350		split_chars(Tail,"+",[V2C,V3C]),
1351		!,
1352		(try_number_codes(V2,V2C)
1353		-> get_v3_atom(V3C,V3Atom)
1354		; append(V2CC,[0'. | FurtherC], V2C) % there is at least one more dot in the version nr (e.g. 17.0.1+12-LTS-39)
1355		->
1356		try_number_codes(V2,V2CC),
1357		append(FurtherC,[0'+ | V3C], V3C3),
1358		get_v3_atom(V3C3,V3Atom)
1359		).
1360		get_java_fullversion_numbers_aux(Tail,V1,V2,V3Atom) :-
1361		split_chars(Tail,".",[V1C,V2C|FurtherC]),
1362		append(FurtherC,V3C),
1363		try_number_codes(V1,V1C),
1364		try_number_codes(V2,V2C),!,
1365		get_v3_atom(V3C,V3Atom).
1366
1367		get_v3_atom(V3C,V3Atom) :- strip_closing_quote(V3C,V3C2),
1368		atom_codes(V3Atom,V3C2).
1369
1370		try_number_codes(Name,Codes) :-
1371		catch(number_codes(Name,Codes), _Exc, fail).
1372
1373		strip_closing_quote([],[]).
1374		strip_closing_quote([H|_],R) :- (H=34 ; H=32),!, R=[]. % closing " or newline
1375		strip_closing_quote([H|T],[H|R]) :- strip_closing_quote(T,R).
1376
1377		% get java fullversion as code list; format "java full version "...."\n"
1378		get_java_fullversion(Version) :-
1379		get_java_command_path(JavaCmdW),
1380		(my_system_call(JavaCmdW, ['-fullversion'],java_version,Text) -> Text=Version
1381		; format(user_error,'Could not execute ~w -fullversion~n',[JavaCmdW]),
1382		fail).
1383
1384		% when java -fullversion works but not java -version it seems that Java was improperly
1385		% installed without admin rights (http://stackoverflow.com/questions/11808829/jre-1-7-returns-java-lang-noclassdeffounderror-java-lang-object)
1386		get_java_version(Version) :-
1387		get_java_command_path(JavaCmdW),
1388		(my_system_call(JavaCmdW, ['-version'],java_version,Text) -> Text=Version
1389		; format(user_error,'Could not execute ~w -version~n',[JavaCmdW]),
1390		fail).
1391		% should we check for JAVA_PATH first ? would allow user to override java; but default pref would have to be set to ''
1392		get_java_command_path(JavaCmdW) :-
1393		%host_platform(darwin)
1394		get_preference(path_to_java,X),
1395		debug_println(8,path_to_java_preference(X)),
1396		(X=''
1397		; preference_default_value(path_to_java,Default), debug_println(8,default(Default)),
1398		Default=X
1399		),
1400		% only try this when the Java path has not been set explicitly
1401		% on Mac: /usr/bin/java exists even when Java not installed ! it is a fake java command that launches a dialog
1402	?	absolute_file_name(path(java),
1403		JavaCmd,
1404		[access(exist),extensions(['.exe','']),solutions(all),file_errors(fail)]),
1405		debug_println(8,obtained_java_cmd_from_path(JavaCmd)),
1406		replace_windows_path_backslashes(JavaCmd,JavaCmdW),
1407		!.
1408		get_java_command_path(JavaCmdW) :- get_preference(path_to_java,JavaCmd),
1409		JavaCmd \= '',
1410		debug_println(8,using_path_to_java_preference(JavaCmd)),
1411		(file_exists(JavaCmd) -> true
1412		; directory_exists(JavaCmd) -> add_warning(get_java_command_path,'No Java Runtime (7 or newer) found; please correct the JAVA_PATH advanced preference (it has to point to the java tool, *not* the directory enclosing it): ',JavaCmd)
1413		; add_warning(get_java_command_path,'No Java Runtime (7 or newer) found; please correct the JAVA_PATH advanced preference: ',JavaCmd)),
1414		replace_windows_path_backslashes(JavaCmd,JavaCmdW),
1415		!.
1416		get_java_command_path(_JavaCmd) :-
1417		add_error(get_java_command_path,'Could not get path to the java tool. Make sure a Java Runtime (7 or newer) is installed',''),
1418		fail.
1419
1420		library_abs_name(Lib,Abs) :- absolute_file_name(prob_lib(Lib),Abs).
1421
1422
1423		call_ltl_parser(Formulas, CtlOrLtl, Result) :-
1424		get_ltl_lang_spec(LangSpec),
1425		maplist(parse_temporal_formula(CtlOrLtl,LangSpec),Formulas,Result).
1426
1427		:- use_module(specfile,[b_or_z_mode/0,csp_with_bz_mode/0]).
1428		get_ltl_lang_spec('B,none') :- csp_with_bz_mode,!.
1429		get_ltl_lang_spec('B') :- b_or_z_mode,!.
1430		get_ltl_lang_spec(none).
1431
1432		/* unused code :
1433		generate_formula_codes([F]) -->
1434		!,generate_formula_codes2(F),"\n".
1435		generate_formula_codes([F|Rest]) -->
1436		generate_formula_codes2(F), "###\n",
1437		generate_formula_codes(Rest).
1438		generate_formula_codes2(F) -->
1439		write_to_codes(F).
1440		*/
1441
1442
1443		% ---------------------------
1444
1445		% call the TLA2B parser to translate a TLA file into a B machine
1446		call_tla2b_parser(TLAFile) :-
1447		get_java_command_path(JavaCmdW),
1448		replace_windows_path_backslashes(TLAFile,TLAFileW),
1449		phrase(jvm_options, XOpts),
1450		absolute_file_name(prob_lib('TLA2B.jar'),TLA2BJAR),
1451		append(XOpts,['-jar',file(TLA2BJAR),file(TLAFileW)],FullArgs),
1452		% other possible options -verbose -version -config FILE
1453		(my_system_call(JavaCmdW, FullArgs,tla2b_parser)
1454		-> true
1455		; \+ file_exists(TLA2BJAR),
1456		print_error('Be sure to download TLA2B.jar from https://stups.hhu-hosting.de/downloads/prob/tcltk/jars/,'),
1457		print_error('and put it into the ProB lib/ directory.'),
1458		fail
1459		).
1460
1461		%call_cspmj_parser(CSPFile,PrologFile) :-
1462		% get_java_command_path(JavaCmdW),
1463		% replace_windows_path_backslashes(CSPFile,CSPFileW),
1464		% phrase(jvm_options, XOpts),
1465		% absolute_file_name(prob_lib('cspmj.jar'),CSPMJAR),
1466		% get_writable_compiled_filename(CSPFile,'.pl',PrologFile),
1467		% tools:string_concatenate('--prologOut=', PrologFile, PrologFileOutArg),
1468		% append(XOpts,['-jar',CSPMJAR,'-parse',CSPFileW,PrologFileOutArg],FullArgs),
1469		% debug_println(9,calling_java(FullArgs)),
1470		% (my_system_call(JavaCmdW, FullArgs,cspmj_parser) -> true
1471		% ; print_error('Be sure that cspmj.jar parser is installed.'),
1472		% fail).
1473
1474
1475		tla2prob_filename(TLAFile,GeneratedProbFile) :-
1476		split_filename(TLAFile,Basename,_Extension),
1477		atom_chars(Basename,BasenameC),
1478		append(BasenameC,['.','p','r','o','b'],TLABC),
1479		atom_chars(GeneratedProbFile,TLABC),!.
1480		tla2prob_filename(Filename, GeneratedProbFile) :-
1481		add_failed_call_error(tla2b_filename(Filename,GeneratedProbFile)),fail.
1482
1483		tla2b_filename(TLAFile,BFile) :-
1484		split_filename(TLAFile,Basename,_Extension),
1485		atom_chars(Basename,BasenameC),
1486		append(BasenameC,['_',t,l,a,'.','m','c','h'],TLABC),
1487		atom_chars(BFile,TLABC),!.
1488		tla2b_filename(Filename, BFile) :-
1489		add_failed_call_error(tla2b_filename(Filename,BFile)),fail.
1490
1491
1492		my_system_call(Command,Args,Origin) :- my_system_call(Command,Args,Origin,_Text).
1493		my_system_call(Command,Args,Origin,ErrText) :-
1494		debug_print_system_call(Command,Args),
1495		system_call(Command,Args,ErrText,Exit), %nl,print(exit(Exit)),nl,nl,
1496		treat_exit_code(Exit,Command,Args,ErrText,Origin).
1497
1498		debug_print_system_call(Command,Args) :-
1499		(debug_mode(off) -> true ; print_system_call(Command,Args)).
1500		print_system_call(Command,Args) :-
1501		ajoin_with_sep(Args,' ',FS), format(user_output,'Executing: ~w ~w~n',[Command,FS]).
1502
1503		my_system_call5(Command,Args,Origin,OutputText,ErrText) :-
1504		system_call(Command,Args,OutputText,ErrText,Exit), %nl,print(exit(Exit)),nl,nl,
1505		treat_exit_code(Exit,Command,Args,ErrText,Origin).
1506
1507		treat_exit_code(exit(0),_,_,_,_) :- !.
1508		treat_exit_code(Exit,Command,Args,ErrText,Origin) :-
1509		debug_println(9,treat_exit_code(Exit,Command,Args,ErrText,Origin)),
1510		catch( my_read_from_codes(ErrText,Term),
1511		_,
1512		(safe_name(T,ErrText),Term = T)), !,
1513		%print_error(Term),
1514		(Term = end_of_file -> ErrMsg = '' ; ErrMsg = Term),
1515		ajoin(['Exit code ',Exit,' for command ',Command, ', error message: '],Msg),
1516		(get_error_position_from_term(Origin,Term,Pos)
1517		-> add_error(Origin,Msg,ErrMsg,Pos)
1518		; add_error(Origin,Msg,ErrMsg)
1519		),
1520		fail.
1521
1522
1523		get_error_position_from_term(alloy2b,Term,Pos) :- atom(Term),
1524		atom_codes(Term,Codes), get_error_position_from_codes(Codes,Pos).
1525
1526		% Alloy error message: ! Exception in thread "main" Type error in .../Restrictions.als at line 41 column 23:
1527		get_error_position_from_codes([97,116,32,108,105,110,101,32|Tail],lineCol(Line,Col)) :- % "at line "
1528		epi_number(Line,Tail,RestTail),
1529		(RestTail = [32,99,111,108,117,109,110,32|Tail2], % "column "
1530		epi_number(Col,Tail2,_) -> true
1531		; Col=0).
1532		get_error_position_from_codes([_|T],Pos) :- get_error_position_from_codes(T,Pos).
1533
1534		% replace backslashes by forward slashes in atoms, only under windows
1535		% TODO(DP,14.8.2008): Check if still needed with SICStus 4.0.4 and if
1536		% everybody uses that version
1537		replace_windows_path_backslashes(Old,New) :-
1538		( host_platform(windows) ->
1539		safe_name(Old,OldStr),
1540		replace_string_backslashes(OldStr,NewStr),
1541		safe_name(New,NewStr)
1542		;
1543		Old=New).
1544
1545		replace_string_backslashes([],[]) :- !.
1546		replace_string_backslashes([C|OldRest],[N|NewRest]) :- !,
1547		( C=92 /* backslash */ ->
1548		N=47 /* forward slash */
1549		;
1550		N=C ),
1551		replace_string_backslashes(OldRest,NewRest).
1552		replace_string_backslashes(X,Y) :-
1553		add_error(parsercall,'Illegal call: ',replace_string_backslashes(X,Y)),
1554		fail.
1555
1556		% ---------------------------
1557
1558		:- assert_must_succeed((parsercall:parse_string_template("0",Res), Res==[string_codes("0")])).
1559		:- assert_must_succeed((parsercall:parse_string_template("ab${xy}cd",Res),
1560		Res==[string_codes("ab"),template_codes("xy",2,3,[]),string_codes("cd")])).
1561		:- assert_must_succeed((parsercall:parse_string_template("ab${xy}$<<z>>cd$\xab\v\xbb\",Res),
1562		Res==[string_codes("ab"),template_codes("xy",2,3,[]),template_codes("z",3,5,[]),
1563		string_codes("cd"),template_codes("v",2,3,[])])). % \xab\ is double angle
1564
1565		% parse a ProB string template
1566		% each recognised template is an expression.
1567		parse_string_template(Codes,TemplateList) :- %format("parsing: ~s~n",[Codes]),
1568		parse_string_template([],TemplateList,Codes,[]).
1569
1570		parse_string_template(Acc,TemplateList) -->
1571	?	template_inside_string(Str,StartOffset,AdditionalChars,Options),!,
1572		{add_acc_string(Acc,TemplateList,
1573		[template_codes(Str,StartOffset,AdditionalChars,Options)|T])},
1574		parse_string_template([],T).
1575		parse_string_template(Acc,TemplateList) --> [H], !, parse_string_template([H|Acc],TemplateList).
1576		parse_string_template(Acc,TemplateList) --> "", {add_acc_string(Acc,TemplateList,[])}.
1577
1578		% add accumulator as regular string before a detected template ${...}
1579		add_acc_string([],L,R) :- !, L=R.
1580		add_acc_string(Acc,[string_codes(Str)|T],T) :- reverse(Acc,Str).
1581
1582		template_inside_string(Str,StartOffset,AdditionalChars,Options) --> "$",
1583		template_options(Options,OptLen),
1584	?	template_open_paren(ClosingParen,ParenLen),
1585		{StartOffset is OptLen+ParenLen+1,
1586		AdditionalChars is StartOffset+ParenLen}, % add closing parentheses length
1587		template_content(Str,ClosingParen).
1588
1589		template_options(Options,Len) --> "[", template_options2(Options,Len).
1590		template_options([],0) --> [].
1591
1592		template_options2([H|T],Len) --> template_option(H,HLen), !, template_options3(T,HLen,Len).
1593		template_options2([],2) --> "]".
1594		template_options3([H|T],AccLen,Len) --> ",", template_option(H,HLen), !,
1595		{A1 is AccLen+HLen},template_options3(T,A1,Len).
1596		template_options3([],AccLen,Len) --> "]", {Len is AccLen+2}.
1597		template_option(ascii,5) --> "ascii".
1598		template_option(ascii,1) --> "a".
1599		template_option(unicode,7) --> "unicode".
1600		template_option(unicode,1) --> "u".
1601		template_option(template_width(Option,Nr),L1) --> digits(Nr,Len),template_width_option(Option,LO), {L1 is Len+LO}.
1602		% other options could be hex output or padding, ...
1603		% TODO: provide error feedback when option/template parsing fails
1604
1605		template_width_option(float_fixed_point,1) --> "f".
1606		template_width_option(integer_decimal_string,1) --> "d".
1607		template_width_option(pad_string(' '),1) --> "p".
1608
1609		digits(MinusNr,Len) --> "-",!, digit(X), digits2(X,Nr,2,Len), {MinusNr is -Nr}.
1610		digits(Nr,Len) --> digit(X), digits2(X,Nr,1,Len).
1611		digits2(X,Nr,AccLen,Len) --> digit(Y), !, {XY is X*10+Y, A1 is AccLen+1}, digits2(XY,Nr,A1,Len).
1612		digits2(X,X,Len,Len) --> "".
1613
1614		digit(Nr) --> [X], {X >= 48, X=<57, Nr is X-48}.
1615
1616		template_open_paren("}",1) --> "{".
1617		template_open_paren(">>",2) --> "<<".
1618		template_open_paren([187],1) --> [ 171 ]. % Double angle quotation mark "«»"
1619
1620		template_content("",Closing) --> Closing,!.
1621		template_content([H|T],Closing) --> [H], template_content(T,Closing).
1622
1623		% TODO: offset span within template
1624		parse_template_b_expression(Span,Filenumber,template_codes(Codes,_,_,Options),RawStrExpr) :-
1625		\+ get_prob_application_type(rodin), % in Rodin parser callback is not available
1626		!,
1627		catch( parse_at_position_in_file(expression,Codes,RawExpr,Span,Filenumber),
1628		parse_errors(Errors),
1629		(add_all_perrors(Errors,[],parse_template_string), % add_all_perrors_in_context_of_used_filenames?
1630		fail)
1631		),
1632		create_to_string_conversion(RawExpr,Span,Options,RawStrExpr).
1633		parse_template_b_expression(Span,_,template_codes(Codes,_,_,_),string(Span,Atom)) :-
1634		atom_codes(Atom,Codes).
1635		parse_template_b_expression(Span,_,string_codes(Codes),string(Span,Atom)) :-
1636		atom_codes(Atom,Codes).
1637
1638		:- assert_must_succeed((parsercall:transform_string_template('1+1 = ${1+1}',p3(1,1,12),Res),
1639		Res= general_concat(_,sequence_extension(_,[_|_])) )).
1640		:- assert_must_succeed((parsercall:transform_string_template('abc',p3(1,1,3),Res),
1641		Res= string(_,'abc') )).
1642
1643		:- use_module(error_manager,[extract_file_number_and_name/3]).
1644		% transform a string template into a raw expression that computes a string value
1645		transform_string_template(Atom,Span,RawExpr) :-
1646		atom_codes(Atom,Codes),
1647		parse_string_template(Codes,TemplateList),
1648	?	transform_str_templ_aux(TemplateList,Atom,Span,RawExpr).
1649
1650		transform_str_templ_aux([string_codes(_)],Atom,Span,RawExpr) :- !,
1651		debug_println(19,unnecessary_string_template(Span)), % regular string suffices
1652		RawExpr = string(Span,Atom).
1653		transform_str_templ_aux(TemplateList,_,Span,RawExpr) :-
1654		(extract_file_number_and_name(Span,FileNr,_) -> true ; FileNr = -1),
1655		InitialOffset = 3, % for three starting quotes
1656	?	l_parse_templates(TemplateList,0,InitialOffset,Span,FileNr,BTemplateList),
1657		generate_conc_expr(BTemplateList,Span,RawExpr).
1658
1659		:- use_module(tools_positions, [add_col_offset_to_position/3, add_line_col_offset_to_position/4]).
1660		l_parse_templates([],_,_,_,_,[]).
1661		l_parse_templates([Templ1|T],LineOffset,ColOffset,Span,FileNr,[RawStrExpr|BT]) :-
1662		templ_start_offset(Templ1,StartOffset),
1663		CO2 is ColOffset+StartOffset, % e.g., add two chars for ${ in case Templ1 is a template
1664		add_line_col_offset_to_position(Span,LineOffset,CO2,Span1),
1665		% it is only start position of Span1 that is important
1666		parse_template_b_expression(Span1,FileNr,Templ1,RawStrExpr),
1667	?	count_template_offset(Templ1,LineOffset,ColOffset,LineOffset2,ColOffset2),
1668	?	l_parse_templates(T,LineOffset2,ColOffset2,Span,FileNr,BT).
1669
1670		% accumulate length of template part and add to line/col offset to be added to start of template string
1671		count_template_offset(template_codes(Codes,_StartOffset,AdditionalChars,_),L,C,LineOffset,C3) :-
1672	?	count_offset(Codes,L,C,LineOffset,ColOffset),
1673		C3 is ColOffset+AdditionalChars. % e.g., 3 for ${.}
1674		count_template_offset(string_codes(Codes),L,C,LineOffset,ColOffset) :-
1675	?	count_offset(Codes,L,C,LineOffset,ColOffset).
1676
1677		templ_start_offset(template_codes(_,StartOffset,_,_),StartOffset). % usually 2 for ${
1678		templ_start_offset(string_codes(_),0).
1679
1680		% count line/column offset inside a list of codes:
1681		%count_offset(Codes,LineOffset,ColOffset) :- count_offset(Codes,0,0,LineOffset,ColOffset).
1682		count_offset([],Line,Col,Line,Col).
1683		count_offset(Codes,L,_ColOffset,Line,Col) :- newline(Codes,T),!,
1684		L1 is L+1,
1685		count_offset(T,L1,0,Line,Col).
1686		count_offset([_|T],L,ColOffset,Line,Col) :- C1 is ColOffset+1,
1687	?	count_offset(T,L,C1,Line,Col).
1688
1689		newline([10|T],T).
1690		newline([13|X],T) :- (X=[10|TX] -> T=TX ; T=X). % TO DO: should we check if we are on Windows ?
1691
1692		% generate a raw expression for the concatenation of a list of expressions
1693		generate_conc_expr([],Pos,string(Pos,'')).
1694		generate_conc_expr([OneEl],_,Res) :- !, Res = OneEl. % no need to concatenate
1695		generate_conc_expr(List,Pos,general_concat(Pos,sequence_extension(Pos,List))).
1696
1697		create_to_string_conversion(RawExpr,Pos,Options,
1698		external_function_call_auto(Pos,'STRING_PADLEFT',[RawStrExpr,Len,Char])) :-
1699		select(template_width(pad_string(PadChar),Nr),Options,RestOpts),!,
1700		create_to_string_conversion(RawExpr,Pos,RestOpts,RawStrExpr),
1701		Char = string(Pos,PadChar),
1702		Len = integer(Pos,Nr).
1703		create_to_string_conversion(RawExpr,Pos,Options,RawStrExpr) :-
1704		is_definitely_string(RawExpr),!,
1705		(Options=[] -> true
1706		; add_warning(string_template,'Ignoring options in string template (already a string): ',Options, Pos)),
1707		RawStrExpr=RawExpr.
1708		create_to_string_conversion(RawExpr,Pos,Options,external_function_call_auto(Pos,'REAL_TO_DEC_STRING',[RawExpr,Prec])) :-
1709		select_option(template_width(float_fixed_point,Nr),Options,Pos),!,
1710		Prec = integer(Pos,Nr).
1711		create_to_string_conversion(RawExpr,Pos,Options,external_function_call_auto(Pos,'INT_TO_DEC_STRING',[RawExpr,Prec])) :-
1712		select_option(template_width(integer_decimal_string,Nr),Options,Pos),!,
1713		Prec = integer(Pos,Nr).
1714		create_to_string_conversion(RawExpr,Pos,Options,external_function_call_auto(Pos,'TO_STRING_UNICODE',[RawExpr])) :-
1715		select_option(unicode,Options,Pos),!. % TODO use a TO_STRING function with options list
1716		create_to_string_conversion(RawExpr,Pos,_Options,external_function_call_auto(Pos,'TO_STRING',[RawExpr])).
1717
1718		select_option(Option,Options,Pos) :-
1719		select(Option,Options,Rest),
1720		(Rest=[] -> true ; add_warning(string_template,'Ignoring additional string template options: ',Rest,Pos)).
1721
1722
1723		is_definitely_string(string(_,_)).
1724
1725		% ---------------------------
1726		:- use_module(pathes,[runtime_application_path/1]).
1727
1728		call_jar_parser(PMLFile,JARFile,Args,ParserName) :-
1729		get_java_command_path(JavaCmdW),
1730		replace_windows_path_backslashes(PMLFile,PMLFileW),
1731		phrase(jvm_options, XOpts),
1732		absolute_file_name(prob_lib(JARFile),FullJAR),
1733		append(XOpts,['-jar',FullJAR,PMLFileW|Args],FullArgs),
1734		%format('Java: ~w, Parser: ~w, Args: ~w~n',[JavaCmdW,ParserName,FullArgs]),
1735		my_system_call(JavaCmdW, FullArgs,ParserName).
1736
1737
1738
1739		call_alloy2pl_parser(AlloyFile,BFile) :-
1740		alloy_pl_filename(AlloyFile,BFile),
1741		call_alloy2pl_parser_aux(AlloyFile,'alloy2b.jar',BFile).
1742
1743		call_alloy2pl_parser_aux(AlloyFile,JARFile,PrologBFile) :-
1744		compilation_not_needed(AlloyFile,PrologBFile,JARFile),!.
1745		call_alloy2pl_parser_aux(AlloyFile,JARFile,PrologBFile) :-
1746		(file_exists(PrologBFile) -> delete_file(PrologBFile) ; true), % TODO: only delete generated files
1747		replace_windows_path_backslashes(PrologBFile,BFileW),
1748		call_jar_parser(AlloyFile,JARFile,['-toProlog',BFileW],alloy2b).
1749
1750		alloy_pl_filename(AlloyFile,BFile) :- atom_codes(AlloyFile,BasenameC),
1751		append(BasenameC,".pl",NewC),
1752		atom_codes(BFile,NewC),!.
1753		alloy_pl_filename(Filename, BFile) :-
1754		add_failed_call_error(alloy_pl_filename(Filename,BFile)),fail.
1755
1756		compilation_not_needed(BaseFile,DerivedFile,LibraryFile) :-
1757		file_exists(BaseFile),
1758		file_property(BaseFile, modify_timestamp, BTime),
1759		%system:datime(BTime,datime(_Year,Month,Day,Hour,Min,Sec)), format('~w modfied on ~w/~w at ~w:~w (~w sec)~n',[BaseFile,Day,Month,Hour,Min,Sec]),
1760		file_exists(DerivedFile),
1761		file_property(DerivedFile, modify_timestamp, DTime),
1762		DTime > BTime,
1763		absolute_file_name(prob_lib(LibraryFile),FullLibFile),
1764		(file_exists(FullLibFile)
1765		-> file_property(FullLibFile, modify_timestamp, LibTime),
1766		DTime > LibTime % check that file was generated by this library (hopefully); ideally we should put version numbers into the DerivedFiles
1767		; true % Jar/command not available anyway; use the derived file
1768		).
1769
1770		% ---------------------------
1771
1772		call_fuzz_parser(TexFile,FuzzFile) :-
1773		get_command_in_lib(fuzz,FuzzCmd),
1774		absolute_file_name(prob_lib('fuzzlib'),FUZZLIB), % TO DO: windows
1775		fuzz_filename(TexFile,FuzzFile),
1776		% fuzz options:
1777		% -d Allow use before definition
1778		% -l Lisp-style echoing of input
1779		% -p file Use <file> in place of standard prelude
1780		debug_format(19,'Fuzz: running ~w -d -l with library ~w on ~w~n',[FuzzCmd,FUZZLIB,TexFile]),
1781		(file_exists(FUZZLIB)
1782		-> my_system_call5(FuzzCmd,['-d', '-l', '-p', file(FUZZLIB), file(TexFile)],call_fuzz_parser,Text,_ErrText)
1783		; my_system_call5(FuzzCmd,['-d', '-l', file(TexFile)],call_fuzz_parser,Text,_ErrText)
1784		),
1785		format('Writing fuzz AST to ~s~n',[FuzzFile]),
1786		open(FuzzFile,write,Stream),
1787		call_cleanup(format(Stream,'~s~n',[Text]), close(Stream)).
1788
1789		get_command_in_lib(Name,Command) :-
1790		get_binary_extensions(Extensions),
1791		absolute_file_name(prob_lib(Name),
1792		Command,
1793		[access(exist),extensions(Extensions),solutions(all),file_errors(fail)]).
1794
1795		get_binary_extensions(List) :-
1796		host_platform(windows),!, List=['.exe','']. % will backtrack in get_command_in_lib
1797		get_binary_extensions(['']).
1798
1799		fuzz_filename(TexFile,FuzzFile) :-
1800		split_filename(TexFile,Basename,_Extension),
1801		atom_chars(Basename,BasenameC),
1802		append(BasenameC,['.','f','u','z','z'],CC),
1803		atom_chars(FuzzFile,CC),!.
1804		fuzz_filename(TexFile, FuzzFile) :-
1805		add_failed_call_error(fuzz_filename(TexFile,FuzzFile)),fail.