1		% (c) 2009-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
6		:- module(error_manager,[init_error_manager/0,
7		add_warning/2, add_warning/3, add_warning/4,
8		reset_errors/0, clear_wd_errors/0,
9		add_error/2, add_error/3, add_error/4,
10		add_error_and_fail/3, add_error_and_fail/2,
11		add_error_fail/3,
12		add_failed_call_error/1, add_internal_error/2, add_internal_error/4,
13		register_optional_error/1, reset_optional_errors/0,
14		assert_true/1,
15		add_message/2, add_message/3, add_message/4,
16		add_all_perrors/1, add_all_perrors/2, add_all_perrors/3,
17		no_real_perror_occurred/1,
18		get_all_errors/1, tcltk_get_all_errors/4,
19		get_all_errors_and_reset/1, % call if you want to start with a fresh top-level error scope
20		get_all_errors_with_span_info_and_reset/1, % ditto + obtain location info
21		get_all_errors_and_clear/1,
22		get_error/2, get_error_with_span/3,
23		get_warning/2, check_error_occured/2, check_warning_occured/2,
24		get_error_span_linecol/5, get_error_span_linecol/4, get_error_span_linecol_for_main_file/4,
25		register_error_span/2,
26		check_error_span_file_linecol/6,
27		position_is_not_in_main_file/1,
28		error_or_warning_occured/0,
29		real_error_occurred/0, reset_real_error_occurred/0, assert_real_error_occurred/0,
30		test_error_occurred/1, count_errors_occurred/2,
31		get_total_number_of_errors/1,
32		reset_error_spans/0,
33
34		backup_errors/0, backed_up_error/4,
35
36		set_error_context/1, clear_error_context/0,
37		get_error_context/1, restore_error_context/1,
38
39		extract_span_description/2,
40		extract_line_col/5, extract_file_line_col/6,
41		extract_all_line_col/5,
42		extract_line_col_for_main_file/5,
43		extract_subsidiary_tail_file_name/2, extract_tail_file_name/2,
44		extract_file_number_and_name/3,
45		extract_additional_description/2,
46		print_error_span/1, print_message_span/1,
47
48		turn_show_error_source_on/0, turn_show_error_source_off/0,
49
50		enter_new_error_scope/1, enter_new_error_scope/2,
51		enter_new_clean_error_scope/1,
52		exit_error_scope/2, exit_error_scope/3,
53		error_occurred_at_level/1, specific_event_occurred_at_level/2,
54		%throw_errors_in_scope/3,
55		add_new_event_in_error_scope/1, add_new_event_in_error_scope/2,
56		event_occurred_in_error_scope/1, error_occurred_in_error_scope/0,
57		clear_events_in_error_scope/2, clear_events_in_current_error_scope/1,
58		clear_all_errors_in_error_scope/1,
59		call_in_fresh_error_scope_for_one_solution/1,
60		enumeration_warning_occured_in_error_scope/0,
61		abort_error_occured_in_error_scope/0,
62		on_enumeration_warning/2, on_enumeration_warning_with_continue/3,
63		throw_enumeration_warnings_in_current_scope/0,
64		throw_enumeration_warnings_in_scope/3,
65		catch_enumeration_warning_exceptions/2, catch_enumeration_warning_exceptions/3,
66		call_with_enumeration_warning/1,
67		observe_enumeration_warnings/2,
68		critical_enumeration_warning_occured_in_error_scope/4, critical_enumeration_warning_occured_in_error_scope/0,
69		clear_enumeration_warnings/0,
70		translate_events_in_current_scope_to_warnings/2,
71		time_out_with_enum_warning_one_solution/3, % use this for finding one solution
72		time_out_with_enum_warning_one_solution_no_new_error_scope/3,
73		is_time_out_result/1,
74		time_out_with_enum_warning_for_findall/3, % use this if you cycle through all solutions
75		time_out_with_enum_warning_for_findall_in_current_error_scope/4,
76		logged_error/4,
77		display_error_statistics/0
78		]).
79
80		% meta_predicate annotations should appear before loading any code:
81		:- meta_predicate add_failed_call_error(0).
82		:- meta_predicate add_internal_error(-,:).
83		:- meta_predicate add_new_event_in_error_scope(-,2).
84
85		:- meta_predicate on_enumeration_warning(0,0).
86		:- meta_predicate on_enumeration_warning_with_continue(0,0,0).
87
88		:- meta_predicate catch_enumeration_warning_exceptions(0,0).
89		:- meta_predicate catch_enumeration_warning_exceptions(0,0,-).
90
91		:- meta_predicate observe_enumeration_warnings(0,0).
92
93		:- meta_predicate time_out_with_enum_warning_one_solution(0,-,-).
94
95		:- meta_predicate call_in_fresh_error_scope_for_one_solution(0).
96
97		:- meta_predicate call_with_enumeration_warning(0).
98
99		:- meta_predicate time_out_with_enum_warning_one_solution_no_new_error_scope(0,-,-).
100
101		:- meta_predicate time_out_with_enum_warning_for_findall(0,-,-).
102		:- meta_predicate time_out_with_enum_warning_for_findall2(-,0,-,-).
103
104		:- meta_predicate time_out_with_enum_warning_for_findall_in_current_error_scope(-,0,-,-).
105
106		:- meta_predicate assert_true(0).
107		% ------------
108
109		:- use_module(library(lists)).
110
111		:- use_module(tools,[get_tail_filename/2]).
112		:- use_module(tools_lists,[count_occurences/2]).
113		:- use_module(tools_printing,[print_error/1,print_message_on_output/2,format_error/2,format_with_colour/4]).
114		:- use_module(tools_strings,[ajoin/2, string_concatenate/3]).
115
116		:- use_module(module_information,[module_info/2]).
117		:- module_info(group,infrastructure).
118		:- module_info(description,'The error_manager controls error messages. Error messages can be added, retrieved, counted,etc. The module also takes care of extracting source spans from error messages.').
119
120		%:- use_module(translate).
121		:- use_module(debug, [debug_mode/1, debug_println/1, debug_println/2]).
122		:- use_module(preferences,[get_preference/2,reset_temporary_preference/2,
123		temporary_set_preference/3]).
124
125
126		:- use_module(extension('counter/counter')).
127
128		% cur_block_level is now stored as a C counter, which needs to be initialised
129		init_error_manager :- counter_init, new_counter(cur_block_level).
130
131
132		:- dynamic optional_error/1.
133		register_optional_error(Type) :-
134		(optional_error(Type) -> true ; assert(optional_error(Type))).
135		reset_optional_errors :- retractall(optional_error(_)).
136
137		% INTERNAL ERRORS
138
139
140		add_failed_call_error(Call) :- !,
141		add_internal_error('Internal Error; call failed: ',Call).
142
143		add_internal_error(Module,Msg,Term,Span) :-
144		add_error(internal_error(Module),Msg,Term,Span).
145		add_internal_error(Msg,Module:Call) :- !,
146		add_error(internal_error(Module),Msg,Call).
147		add_internal_error(Msg,Call) :-
148		add_internal_error(Msg,unknown_module:Call).
149
150
151		% ERROR SCOPING
152
153		%:- dynamic cur_block_level/1.
154		%cur_block_level(0). % no realised as a C counter
155		:- volatile error_occurred_at_level/1.
156		:- dynamic error_occurred_at_level/1.
157		:- volatile throw_error/3.
158		:- dynamic throw_error/3.
159
160
161
162		enter_new_error_scope(Level,_PP) :-
163		enter_new_error_scope(Level). %, tools_printing:print_term_summary(enter(Level,PP)),nl.
164		enter_new_error_scope(Level) :-
165		enter_new_clean_error_scope(Level),
166		L1 is Level - 1,
167		copy_throw_errors(L1,Level).
168	?	copy_throw_errors(L1,L) :- throw_error(L1,Error,Span), %print(copy(throw(L1,L,Error))),nl,
169		assert(throw_error(L,Error,Span)),fail.
170		copy_throw_errors(_,_).
171		enter_new_clean_error_scope(Level) :-
172		inc_counter(cur_block_level,L1),
173		retractall(throw_error(L1,_,_)),
174		% print(enter(L1)),nl,trace,
175		Level=L1.
176		% mark that everything unifying with Error should be thrown rather than collected
177		throw_errors_in_scope(Level,Error,Span) :-
178		(\+ throw_error(Level,Error,Span) % TO DO: check that we are an instance of existing error !
179		-> asserta(throw_error(Level,Error,Span))
180		; true).
181
182		clear_all_errors_in_error_scope(Level) :- %print(clearing(Level)),nl,
183		clear_events_in_error_scope(Level,_),
184		error_occurred_at_level(L1), L1>Level, %print(clearing(L1)),nl,
185		clear_events_in_error_scope(Level,_),fail.
186		clear_all_errors_in_error_scope(_).
187
188		exit_error_scope(Level,ErrorOcc) :- exit_error_scope(Level,ErrorOcc,unknown).
189		exit_error_scope(Level,ErrorOcc,PP) :- get_counter(cur_block_level,CurL),
190		% print(exit(Level,CurL,PP)),nl,
191		(CurL = Level -> NewL is CurL-1
192		; Level < CurL -> NewL is Level-1, format('*** exiting multiple error blocks (~w -> ~w) for ~w ***~n',[CurL,NewL,PP])
193		; format('*** block ~w already exited (currently at ~w) for ~w ***~n',[Level,CurL,PP]),
194		NewL is CurL
195		), set_counter(cur_block_level,NewL),
196		copy_error_scope_events(CurL,NewL),
197		retractall(throw_error(CurL,_,_)),
198		(retract(error_occurred_at_level(CurL))
199		-> ErrorOcc=true,
200		(error_occurred_at_level(NewL) -> true ; assert(error_occurred_at_level(NewL)))
201		; ErrorOcc=false).
202
203
204		% versions of enter_new_error_scope and exit_error_scope which re_enter blocks and clean up upon backtracking
205		%enter_new_error_scope_bt(Level,PP) :- enter_new_error_scope(Level,PP), exit_upon_fail(Level,PP).
206		%exit_upon_fail(_,_).
207		%exit_upon_fail(Level,PP) :- print(exit_upon_backtrack(Level,PP)),nl,
208		% exit_error_scope(Level,_,PP),fail.
209		%
210		%exit_error_scope_bt(Level,ErrorOcc,PP) :- exit_error_scope(Level,ErrorOcc,PP).
211		%exit_error_scope_bt(Level,_ErrorOcc,PP) :- print(re_enter_block(Level,PP)),nl,
212		% enter_new_error_scope(Level2,PP),
213		% (Level2=Level -> true ; print(mismatch_when_reentering_block(Level,PP)),nl),
214		% fail.
215
216		% ---------------------------
217
218
219
220		assert_real_error_in_current_block :- get_counter(cur_block_level,L),L>0,
221		\+ error_occurred_at_level(L), assert(error_occurred_at_level(L)),!.
222		assert_real_error_in_current_block.
223
224
225		reset_error_scopes :-
226		set_counter(cur_block_level,0),
227		retractall(error_occurred_at_level(_)),
228		retractall(specific_event_occurred_at_level(_,_)).
229
230		% for debugging / portraying error scopes:
231		:- public print_error_scopes/0.
232		print_error_scopes :-
233		if(get_counter(cur_block_level,L),
234		format(' Cur Block Level = ~w~n',[L]),
235		format(' *** NO Cur Block Level Information !!',[])
236		),
237		fail.
238		print_error_scopes :-
239		findall(L,error_occurred_at_level(L),LL),
240		format(' Errors occured at levels = ~w~n',[LL]),
241		specific_event_occurred_at_level(Level,Err),
242		format(' ~w --> ~w~n',[Level,Err]),
243		fail.
244		print_error_scopes.
245
246		% call a predicate in fresh error scope (assuming one solution is searched for only; failure is also ok)
247		% and then discard all errors
248		call_in_fresh_error_scope_for_one_solution(Call) :-
249		enter_new_error_scope(Level,call_in_fresh_error_scope_for_one_solution),
250		call_cleanup(Call,
251		(clear_all_errors_in_error_scope(_),
252		exit_error_scope(Level,_,call_in_fresh_error_scope_for_one_solution))).
253
254		:- volatile specific_event_occurred_at_level/2.
255		:- dynamic specific_event_occurred_at_level/2.
256
257		% can be used to keep track of whether specific events occurred within an error_scope
258		add_new_event_in_error_scope(Event) :-
259		add_new_event_in_error_scope(Event,do_nothing).
260		do_nothing(_,_).
261		add_new_event_in_error_scope(Event,PrintMessageCall) :-
262		get_counter(cur_block_level,L),
263		(specific_event_occurred_at_level(L,Event) -> fail
264		; (throw_error(L,Event,Span)
265		-> (debug_mode(off) -> true ; print_message(informational,throwing(Event))), % trace, % <---
266		call(PrintMessageCall,throwing,Span),
267		% Note: event is not asserted ! See e.g. tests 1089, 1519, 1522, 1661, 1199, 1291, ...
268		throw(Event)
269		; assert(specific_event_occurred_at_level(L,Event)),
270		call(PrintMessageCall,not_throwing,unknown)
271		)
272		).
273
274		% call if you just want to add the error information; without throwing
275		assert_event_in_error_scope_without_throw(Event) :- get_counter(cur_block_level,L),
276		(specific_event_occurred_at_level(L,Event) -> true
277		; assert(specific_event_occurred_at_level(L,Event))).
278
279		error_occurred_in_error_scope :- get_counter(cur_block_level,L),error_occurred_at_level(L).
280	?	event_occurred_in_error_scope(Event) :- get_counter(cur_block_level,L),specific_event_occurred_at_level(L,Event).
281
282		copy_error_scope_events(FromLevel,ToLevel) :- retract(specific_event_occurred_at_level(FromLevel,Event)),
283		\+ specific_event_occurred_at_level(ToLevel,Event),
284		% print(copying_event(FromLevel,ToLevel,Event)),nl,
285		assert(specific_event_occurred_at_level(ToLevel,Event)), % should we throw if this level demands it ?
286		(throw_error(ToLevel,Event,_Span)
287		-> debug_println(20,throw_copied_event(Event)), throw(Event)),
288		fail.
289		copy_error_scope_events(_,_).
290
291		clear_events_in_current_error_scope(Event) :- get_counter(cur_block_level,L),clear_events_in_error_scope(L,Event).
292
293		%clear_events_in_error_scope(L,Event) :-retract(specific_event_occurred_at_level(L,Event)), print(retract(L,Event)),nl,fail.
294		clear_events_in_error_scope(L,Event) :-
295		retractall(specific_event_occurred_at_level(L,Event)),
296		(specific_event_occurred_at_level(L,_) -> true
297		; retractall(error_occurred_at_level(L))).
298
299		throw_enumeration_warnings_in_current_scope :-
300		get_counter(cur_block_level,L), throw_enumeration_warnings_in_scope(L,_,unknown).
301
302		throw_enumeration_warnings_in_scope(Level,Critical,Span) :-
303		simplify_span(Span,SimplifiedSpan), % relevant for test 1562
304		throw_errors_in_scope(Level,enumeration_warning(_,_,_,_,Critical),SimplifiedSpan).
305
306		on_enumeration_warning(Call, BackupCall) :-
307		on_enumeration_warning_with_continue(Call, BackupCall, true).
308		% sets up a new error scope and forces enumeration_warnings to be thrown
309		% if an enumeration_warning happens the BackupCall is executed
310		on_enumeration_warning_with_continue(Call, BackupCall, TrueContinuation) :-
311	?	enter_new_error_scope(Level,on_enumeration_warning_with_continue),
312	?	throw_enumeration_warnings_in_scope(Level,_,unknown),
313	?	on_exception(enumeration_warning(_,_,_,_,_),
314		if(Call,
315		(exit_error_scope(Level,_,on_enumeration_warning_with_continue_true),call(TrueContinuation)),
316		(exit_error_scope(Level,_,on_enumeration_warning_with_continue_false),fail)
317		),
318		(exit_error_scope(Level,_,on_enumeration_warning_with_continue_exception),BackupCall)).
319
320		catch_enumeration_warning_exceptions(Call, BackupCall) :-
321		catch_enumeration_warning_exceptions(Call,BackupCall,false).
322
323
324
325		% AddAsEventError = true means that caught exceptions are added as event_errors in scope
326		% (this can be important if we later want to decide whether an enumeration warning occured)
327		catch_enumeration_warning_exceptions(Call, BackupCall,AddAsEventError) :-
328		enter_new_error_scope(Level,catch_enumeration_warning_exceptions),
329		% difference: we do not force to throw_errors_in_scope
330		on_exception(enumeration_warning(A,B,C,D,E),
331		call_cleanup(Call, exit_error_scope(Level,_,catch_enumeration_warning_exceptions)),
332		% call_cleanup can be tricky in case of success of Call: the error scope may not be exited immediately; TO DO: maybe rewrite using same style as above (using if + on_exception)
333		((AddAsEventError=false -> true
334		; assert_event_in_error_scope_without_throw(enumeration_warning(A,B,C,D,E))),
335		BackupCall)).
336
337		% execute some code when enumeration warning occurs; and then throw exception again
338		observe_enumeration_warnings(Call,ObserverCallToExecute) :-
339		on_exception(enumeration_warning(A,B,C,D,E),Call,
340		call_cleanup(ObserverCallToExecute, throw(enumeration_warning(A,B,C,D,E)))).
341
342
343		% sets up a new error scope and forces enumeration_warnings to be thrown
344		% the exceptions are not caught !
345		call_with_enumeration_warning(Call) :-
346		enter_new_error_scope(Level,call_with_enumeration_warning),
347		throw_enumeration_warnings_in_scope(Level,_,unknown),
348		on_exception(E,
349		if(Call,
350		exit_error_scope(Level,_,call_with_enumeration_warning_true),
351		(exit_error_scope(Level,_,call_with_enumeration_warning_false),fail)
352		),
353		(exit_error_scope(Level,_,call_with_enumeration_warning_exception),throw(E))).
354
355
356		% a version of time_out which treats enumeration_warnings like time-outs
357		% and also checks enumeration_warnings in case of failure
358		% assumes we only look for one solution (otherwise error scope cleanup has to be changed !! )
359		time_out_with_enum_warning_one_solution(Call,TO,TimeOutRes) :-
360		enter_new_error_scope(Level,time_out_with_enum_warning_one_solution),
361		%% print(time_out_with_enum_warning_one_solution(TO)),nl, %%
362		call_cleanup(
363		on_exception(enumeration_warning(A,B,C,D,E),
364		time_out_check_enum_warning_for_failure(Call,TO,TimeOutRes,no_clear,perform_cut), % no need to clear: we leave error_scope below
365		%% (print(enum_warning),nl,TimeOutRes=time_out)). %%
366		TimeOutRes=virtual_time_out(thrown_enumeration_warning(A,B,C,D,E))),
367		exit_error_scope(Level,_,time_out_with_enum_warning_one_solution)).
368
369		enumeration_warning_occured_in_error_scope :-
370		event_occurred_in_error_scope(enumeration_warning(_,_,_,_,_)).
371		abort_error_occured_in_error_scope :-
372		event_occurred_in_error_scope(abort_error(_)).
373
374		% just like above; but does not set up new error_scope (for performance) and clears enumeration warnings in case of failure and success
375		time_out_with_enum_warning_one_solution_no_new_error_scope(Call,TO,TimeOutRes) :-
376		(enumeration_warning_occured_in_error_scope
377		-> %trace,
378		add_internal_error('Error block already has enumeration warnings',time_out_with_enum_warning_one_solution_no_new_error_scope(Call,TO,TimeOutRes))
379		; true),
380		on_exception(enumeration_warning(A,B,C,D,E),
381		time_out_check_enum_warning_for_failure(Call,TO,TimeOutRes,clear_errors,perform_cut), % clear errors so we can continue using same error scope
382		%% (print(enum_warning),nl,TimeOutRes=time_out)). %%
383		TimeOutRes=virtual_time_out(thrown_enumeration_warning(A,B,C,D,E))).
384
385
386		% check if a result is a time_out:
387		is_time_out_result(time_out).
388		is_time_out_result(virtual_time_out(_)).
389
390		% a version which is to be used not for a single call but for backtracking
391		% generate virtual time_out at the end if enumeration warning occured
392
393		time_out_with_enum_warning_for_findall(Call,TO,TimeOutRes) :-
394		enter_new_error_scope(Level,time_out_with_enum_warning_for_findall),
395		time_out_with_enum_warning_for_findall2(Level,Call,TO,TimeOutRes).
396
397		time_out_with_enum_warning_for_findall2(_Level,Call,TO,TimeOutRes) :- %print(enter(_Level)),nl,
398		on_exception(enumeration_warning(Cause,_,_,_,_),
399		time_out_check_enum_warning_for_failure(Call,TO,TimeOutRes,no_clear,no_cut),
400		get_virtual_time_out_res(Cause,TimeOutRes)). % virtual time_out
401		time_out_with_enum_warning_for_findall2(Level,_Call,_TO,_TimeOutRes) :- % print(exit(Level)),nl,
402		clear_events_in_error_scope(Level,enumeration_warning(_,_,_,_,_)),
403		exit_error_scope(Level,_,time_out_with_enum_warning_for_findall2),fail.
404
405		get_virtual_time_out_res(kodkod_timeout,Res) :- !, Res= virtual_time_out(kodkod_timeout).
406		get_virtual_time_out_res(_,virtual_time_out(exception)).
407
408		% a version of time_out_with_enum_warning_for_findall where you manually have to enter_new_error_scope before
409		% and exit_error_scope afterwards; useful if you repeatedly call this predicate and want to set up the block only once
410		time_out_with_enum_warning_for_findall_in_current_error_scope(_Level,Call,TO,TimeOutRes) :- %print(enter(_Level)),nl,
411	?	on_exception(enumeration_warning(Cause,_,_,_,_),
412		time_out_check_enum_warning_for_failure(Call,TO,TimeOutRes,no_clear,no_cut),
413		get_virtual_time_out_res(Cause,TimeOutRes)). % virtual time_out
414		time_out_with_enum_warning_for_findall_in_current_error_scope(Level,_Call,_TO,_TimeOutRes) :-
415		% does not exit level
416		clear_events_in_error_scope(Level,enumeration_warning(_,_,_,_,_)),fail.
417
418		:- use_module(tools_meta,[safe_time_out/3]).
419		% a version of time_out which upon failure checks if enumeration warnings were generated
420		time_out_check_enum_warning_for_failure(Call,TO,TimeOutRes,ClearErrors,CutAfterFirstSol) :-
421	?	safe_time_out(Call,TO,TimeOutRes), % a safe version which checks that time-out value TO is not too large
422		(TimeOutRes = time_out -> ! %, print(real_timeout),nl
423		; (ClearErrors=clear_errors -> clear_enumeration_warnings ; true),
424		(CutAfterFirstSol=perform_cut -> ! ; true)
425		%,print(sol),nl
426		).
427		time_out_check_enum_warning_for_failure(_Call,_TO,TimeOutRes,ClearErrors,_) :- % print(failure),nl,
428	?	event_occurred_in_error_scope(enumeration_warning(A,B,C,D,critical)), % print(virtual),nl,
429		TimeOutRes = virtual_time_out(failure_enumeration_warning(A,B,C,D,critical)), % we have not investigated all possibilities; generate virtual time_out
430		(ClearErrors=clear_errors -> clear_enumeration_warnings ; true).
431
432		critical_enumeration_warning_occured_in_error_scope :-
433		critical_enumeration_warning_occured_in_error_scope(_,_,_,_).
434		critical_enumeration_warning_occured_in_error_scope(A,B,C,D) :-
435		event_occurred_in_error_scope(enumeration_warning(A,B,C,D,critical)).
436
437		clear_enumeration_warnings :-
438		clear_events_in_current_error_scope(enumeration_warning(_,_,_,_,_)).
439
440		% retract events and raise real warnings
441		% Src and Msg used if these are not enumeration warnings
442		translate_events_in_current_scope_to_warnings(Src,Msg) :-
443		get_counter(cur_block_level,L),
444		retract(specific_event_occurred_at_level(L,Event)),
445		(translate_enumeration_warning(Event,EMsg)
446		-> add_warning(enumeration_warning,EMsg)
447		; add_warning(Src,Msg,Event)),
448		fail.
449		translate_events_in_current_scope_to_warnings(_,_).
450
451		% see also: print_enum_warning
452		translate_enumeration_warning(enumeration_warning(Enumerating,Type,Range,RestrictedRange,_Throwing), Msg) :-
453		translate_enumeration_info(Enumerating,Info),
454		ajoin(['Unbounded enumeration of ',Info,':',Type,', narrowing range: ',Range,' ---> ',RestrictedRange],Msg).
455		% Throwing=throwing -> print_pending_abort_info ?
456
457		translate_enumeration_info(enumerating(Info),Res) :- !, Res=Info. % TO DO: call get_trigger_info
458		translate_enumeration_info(I,I).
459
460		% -----------------------
461
462		:- volatile logged_error_hash/5, real_error_occurred/0, logged_error_spans/2.
463		:- dynamic logged_error_hash/5.
464		:- dynamic real_error_occurred/0.
465		:- dynamic logged_error_spans/2.
466
467
468		reset_real_error_occurred :- retractall(real_error_occurred).
469		reset_errors :- %print(reset_errors),nl, trace,
470		reset_errors_but_not_scopes,
471		reset_error_limit_reached,
472		reset_error_scopes. % call if you want to start again at a fresh top-level, without error scopes
473		reset_errors_but_not_scopes :-
474		reset_real_error_occurred,
475		retractall(logged_error_hash(_,_,_,_,_)),retractall(logged_error_spans(_,_)),
476		clear_error_context.
477
478		reset_error_span_if_required :-
479		(logged_error_hash(_,_,_,_,_) -> true
480		; retractall(logged_error_spans(_,_))).
481
482		reset_error_spans :- retractall(logged_error_spans(_,_)).
483
484
485		clear_wd_errors :-
486		clear_errors_with_source(well_definedness_error).
487		clear_errors_with_source(Source) :-
488		retractall(logged_error_spans(Source,_)),
489		retractall(logged_error_hash(_,Source,_S1,_TContext1,_Span1)),
490		(logged_error_hash(_,_Source2,_S2,_TContext2,_Span2) -> true
491		; reset_real_error_occurred).
492
493		print_error_span(Span) :- print_error_span(Span,error).
494		print_error_span(unknown,_) :- !.
495		print_error_span(Span,Kind) :-
496		extract_span_description(Span,PosMsg), !,
497		print_error(Kind,PosMsg).
498		print_error_span(b(E,T,I),Kind) :- translate:translate_subst_or_bexpr_with_limit(b(E,T,I),1000,S),!,
499		print_error(Kind,S).
500		print_error_span(Span,Kind) :- print_error(Kind,Span). % span not recognized !
501
502		% the same, but not using user_error and red and only printing when span recognised
503		% more detailed than translate:print_span
504		print_message_span(unknown) :- !.
505		print_message_span(Span) :-
506		extract_span_description(Span,PosMsg), !, print(PosMsg).
507		print_message_span(_). % span not recognized !
508
509		% try and extract a string (aka atom) describing the position
510		extract_span_description(Span,PosMsg) :-
511		extract_line_col(Span,StartLine,StartCol,EndLine,EndCol),!,
512		POS = ['Line: ',StartLine,' Column: ',StartCol|POS1],
513		POS1 = [' until Line: ',EndLine,' Column: ',EndCol|POS2],
514		(extract_file_name(Span,Filename),
515		Filename \=null -> % Filename = null occurs in eval_strings !?
516		POS2 = [' in file: ',Filename|POS3] ; POS2 = POS3),
517		(extract_additional_description(Span,ContextMsg)
518		-> POS3 = [' within ',ContextMsg] ; POS3=[]),
519		ajoin(POS,PosMsg).
520		extract_span_description(Span,PosMsg) :-
521		extract_symbolic_pos(Span,Symbolic),!,
522		% TO DO: we could try and find section for Rodin
523		ajoin(['@label: ',Symbolic],PosMsg).
524
525		assert_true(Code) :-
526		(call(Code) -> true ; add_internal_error('Assertion failed: ',Code)).
527
528		add_error_fail(Source,ErrMsg, ErrTerm) :- add_error_and_fail(Source,ErrMsg, ErrTerm).
529		add_error_and_fail(Source,ErrMsg, ErrTerm) :- add_error(Source,ErrMsg, ErrTerm),fail.
530		add_error_and_fail(Source,ErrMsg) :- add_error(Source,ErrMsg),fail.
531
532		% add_error/2, add_error/3 and add_error/4
533		add_error(Source,ErrMsg) :- add_error4(Source,ErrMsg, '',unknown).
534		add_error(Source,ErrMsg, ErrTerm) :- add_error4(Source,ErrMsg, ErrTerm,unknown).
535		add_error(Source,ErrMsg,ErrTerm,Span) :- add_error4(Source,ErrMsg,ErrTerm,Span).
536
537		add_error4(Source,ErrMsg,ErrTerm,Span) :-
538		assert_real_error_occurred,
539		combine_msg_and_error_term(ErrMsg,ErrTerm,S),
540		add_error_or_warning(Source,S,Span).
541
542		%:- use_module(translate, [translate_error_term/2, translate_context/2]).
543		combine_msg_and_error_term(Msg,'',Res) :- !, Res=Msg.
544		combine_msg_and_error_term(ErrMsg,ErrTerm,S) :-
545		string_concatenate(ErrMsg,' ',ST),
546		safe_translate_error_term(ErrTerm,RString),
547		string_concatenate(ST,RString,S).
548
549
550		:- dynamic show_error_source/0.
551		show_error_source. % True if error source and span to be printed
552		turn_show_error_source_on :- (show_error_source -> true ; assert(show_error_source)).
553		turn_show_error_source_off :- retractall(show_error_source).
554
555		trace_if_user_wants_it :- (preferences:get_preference(trace_upon_error,true) -> safe_trace ; true).
556
557		% try Prolog's trace; if this fails (compiled code), then ask user for input.
558		safe_trace :- translate:install_b_portray_hook,
559		on_exception(error(existence_error(_,_),_), trace, type_to_continue).
560
561		:- dynamic do_not_interrupt_user_anymore/0.
562
563		type_to_continue :- do_not_interrupt_user_anymore,!.
564		type_to_continue :- format(user_output,'(type <RETURN> to continue, z<RETURN> to zip) ===> ',[]),
565		read_line(user_input,X),
566		(zip(X) -> assert(do_not_interrupt_user_anymore) ; true).
567
568		zip([122|_]). %starts with z
569
570
571		print_error_source(well_definedness_error) :- !,print_error('A well-definedness error occured !').
572		print_error_source(warning(Source)) :- show_error_source,!,
573		format_error('! A warning occurred (source: ~w) !~n',[Source]).
574		print_error_source(internal_error(Source)) :- show_error_source,!,
575		format_error('! An internal error occurred (source: ~w) !~n',[Source]).
576		print_error_source(Source) :- show_error_source,!,
577		format_error('! An error occurred (source: ~w) !~n',[Source]).
578		print_error_source(_).
579
580	?	print_error_context(Kind,Context) :- ((Context = '' ; \+show_error_source) -> true ; print_error(Kind,Context)).
581
582		print_error(message,Term) :- !, print_message_on_output([blue],Term).
583		print_error(_,Term) :- print_error(Term).
584
585		safe_translate_error_term(ErrTerm,RString) :-
586		temporary_set_preference(expand_avl_upto,5,CHNG),
587		translate:translate_error_term(ErrTerm,RString),
588		reset_temporary_preference(expand_avl_upto,CHNG).
589
590		safe_translate_context(Result) :-
591		% avoid infinite loop when error occurs inside translate_context
592		current_context(Context),
593		!,
594		set_error_context(translate_context),
595		temporary_set_preference(expand_avl_upto,4,CHNG),
596		(translate:translate_context(Context,TContext)
597		-> true ; TContext=Context),
598		reset_temporary_preference(expand_avl_upto,CHNG),
599		restore_error_context(Context),
600		Result=TContext.
601		safe_translate_context(''). % no context
602
603
604		add_error_or_warning(Source,ErrMsg,Span) :-
605		safe_translate_context(Context),
606		reset_error_span_if_required,
607		simplify_span(Span,SSpan), % for better hashing, assert, retract
608		assertz_logged_error_if_new(Source,ErrMsg,Context,SSpan,New),
609		log_error(Source,ErrMsg,SSpan),
610		(New=false -> true
611		; optional_error(Source) ->
612		(extract_span_description(SSpan,PosMsg) -> true ; PosMsg=''),
613		format(user_output,'% Optional error ~w occured: ~w ~w~n',[Source,ErrMsg,PosMsg]),
614		register_error_span(Source,SSpan,_)
615		; register_error_span(Source,SSpan,NewSrcSpan),
616		(NewSrcSpan=false, error_limit_reached
617		-> true % this is not a new Source,SSpan combination and we have already several errors
618		; print_error_source(Source),
619		print_error(ErrMsg),
620		print_error_context(error,Context),
621		print_error_span(SSpan)
622		),
623		trace_if_user_wants_it
624		).
625
626		% :- use_module(tools,[b_string_escape_codes/2]).
627		% optionally log errors in to a ndsjon logfile
628		log_error(Source,ErrMsg,Span) :- get_preference(error_log_file,LogFile),
629		LogFile \= '',
630		extract_position_from_span(Span,Filename,StartLine,StartCol,EndLine,EndCol),
631		decompose_error_source(Source,Type,Src),
632		% TO DO: escape Filename and ErrMsg
633		atom_codes(ErrMsg,EMC),tools:b_string_escape_codes(EMC,EscErrMsgC),
634		atom_codes(Filename,EFC),tools:b_string_escape_codes(EFC,EscFileC),
635		on_exception(E,intelligent_open(LogFile,append,S),
636		(format(user_error,'*** Cannot open error log file: ~w~n*** Exception: ~w~n',[LogFile,E]),fail)),
637		!, %ndjson format
638		format(S,'{"~w": {"message": "~s", type: "~w", "file": "~s", "start": {"line": ~w, "col": ~w}, "end": {"line": ~w, "col": ~w} }}~n',
639		[Type,EscErrMsgC,Src,EscFileC,StartLine,StartCol,EndLine,EndCol]),
640		close(S).
641		log_error(_,_,_).
642
643		intelligent_open(user_error,Mode,Stream) :- (Mode=append ; Mode=write), !, Stream=user_error.
644		intelligent_open(stderr,Mode,Stream) :- (Mode=append ; Mode=write), !, Stream=user_error.
645		intelligent_open(user_output,Mode,Stream) :- (Mode=append ; Mode=write), !, Stream=user_output.
646		intelligent_open(stdout,Mode,Stream) :- (Mode=append ; Mode=write), !, Stream=user_output.
647		intelligent_open(File,Mode,Stream) :- open(File,Mode,Stream).
648
649		decompose_error_source(warning(Source),warning,Res) :- !, Res=Source.
650		decompose_error_source(internal_error(Source),internal_error,Res) :- !, Res=Source.
651		decompose_error_source(Msg,error,Msg).
652		:- dynamic total_number_of_errors/1.
653		total_number_of_errors(0).
654
655		% the total number of errors since start; no way to reset this; useful for validation reports
656		% TO DO: maybe use counter extension; but tricky to get dependency and initialisation right
657		get_total_number_of_errors(X) :-
658		(total_number_of_errors(X) -> true
659		; format(user_error,'No total_number_of_errors/1 fact!~n',[]), X=0).
660
661		:- dynamic error_limit_reached_printed/0.
662		:- dynamic total_number_of_errors_at_last_reset/1.
663		total_number_of_errors_at_last_reset(0).
664
665		reset_error_limit_reached :-
666		retractall(error_limit_reached_printed),
667		retractall(total_number_of_errors_at_last_reset(_)),
668		get_total_number_of_errors(T),
669		assert(total_number_of_errors_at_last_reset(T)).
670
671		error_limit_reached :- error_limit_reached_printed,!.
672		error_limit_reached :- get_total_number_of_errors(Nr), Nr >= 100,
673		total_number_of_errors_at_last_reset(Last), Nr-Last >= 100,
674		print_error('Error limit reached; only printing new error source and locations!'),
675		assert(error_limit_reached_printed).
676
677		assert_warning_occured :-
678		(preferences:get_preference(strict_raise_warnings,true)
679		-> assert_real_error_occurred ; true).
680		assert_real_error_occurred :-
681		(real_error_occurred -> true ; assert(real_error_occurred)),
682		(retract(total_number_of_errors(X))
683		-> X1 is X+1, assert(total_number_of_errors(X1))
684		; assert(total_number_of_errors(1))),
685		assert_real_error_in_current_block.
686
687		:- use_module(library(terms),[term_hash/3]).
688		assertz_logged_error_if_new(Source,S,TContext,Span,New) :-
689		% limit depth mainly for TContext/Span; avoiding generating many similar error messages with same msg
690		% however, for WD errors often the msg varies (e.g. argument for function application); so this will not prevent a lot of errors
691		term_hash(logged_error_hash(Source,S,TContext,Span),[if_var(ignore),depth(4)],Hash),
692		(logged_error_hash(Hash,Source,S,TContext,Span)
693		-> debug_println(repeated_error(Hash)),New=false
694		; %print(new(Hash,Source,S,TContext,Span)),nl,
695		assertz(logged_error_hash(Hash,Source,S,TContext,Span)),
696		New=true).
697
698		logged_error(Source,S,TContext,Span) :- logged_error_hash(_Hash,Source,S,TContext,Span).
699
700		add_warning(Source,ErrMsg, ErrTerm) :-
701		add_warning(Source,ErrMsg, ErrTerm,unknown).
702		add_warning(Source,ErrMsg, ErrTerm,Span) :-
703		safe_translate_error_term(ErrTerm,RString),
704		string_concatenate(ErrMsg,RString,S),
705		assert_warning_occured,
706		add_error_or_warning(warning(Source),S,Span).
707		add_warning(Source,Message) :-
708		assert_warning_occured,
709		add_error_or_warning(warning(Source),Message,unknown).
710
711		add_message(Source,ErrMsg, ErrTerm,Span) :- /* same as add_error but does not add err msg */
712		safe_translate_error_term(ErrTerm,RString),
713		string_concatenate(ErrMsg,RString,S),
714		add_message(Source,S),
715		(Span=unknown -> true
716		; safe_translate_context(Context),
717		print_error_context(message,Context),
718		print_error_span(Span,message)).
719
720		add_message(Source,ErrMsg, ErrTerm) :- /* same as add_error but does not add err msg */
721		add_message(Source,ErrMsg, ErrTerm,unknown).
722
723		add_message(Source,ErrMsg) :-
724		(show_error_source -> format_with_colour(user_output,[blue],'! Message (source: ~w):~n',[Source]) ; true),
725		print_error(message,ErrMsg).
726		%assertz(logged_error(Source,ErrMsg,_,_)).
727
728		% adds a list of errors with position information
729		% [error(Msg,Pos)] or [warning(Msg,Pos)...]
730		no_real_perror_occurred([]).
731		no_real_perror_occurred([warning(_,_)|T]) :- no_real_perror_occurred(T).
732
733		add_all_perrors(Errors) :- add_all_perrors(Errors,[],bmachine).
734		add_all_perrors(Errors,Files) :- add_all_perrors(Errors,Files,bmachine).
735		add_all_perrors(Errors,Files,Context) :- add_all_perrors(Errors,Files,Context,0,100).
736		add_all_perrors([],_,_,_,_).
737		add_all_perrors([H|Rest],_Filenames,ContextOfError,NrOfErrors,MaxErrors) :-
738		NrOfErrors >= MaxErrors,!,
739		length([H|Rest],Len),
740		add_error(ContextOfError,'Reached maximium number of errors; number of errors not reported: ',Len).
741		add_all_perrors([Error|Rest],Filenames,ContextOfError,NrOfErrors,MaxErrors) :-
742		get_perror(Error,ErrOrWarn,Msg,Pos),
743		extract_perror_pos(Pos,Filenames,NewPos),
744		(ErrOrWarn == warning -> add_warning(ContextOfError,Msg,'',NewPos)
745		; ErrOrWarn = internal_error -> add_internal_error(ContextOfError,Msg,'',NewPos)
746		; add_error(ContextOfError,Msg,'',NewPos)),
747		N1 is NrOfErrors+1,
748		add_all_perrors(Rest,Filenames,ContextOfError,N1,MaxErrors).
749
750		extract_perror_pos(pos(_,Filenumber,Srow,Scol,Erow,Ecol),Filenames,POS) :-
751		get_filename(Filenumber,Filenames,Filename),!,
752		%Ecol1 is Ecol+1,
753		POS = src_span(Filenumber,Filename,Srow,Scol,Erow,Ecol,[],[]).
754		extract_perror_pos(pos(_,_Filenumber,Srow,Scol,Erow,Ecol),_,POS) :- !,
755		%Ecol1 is Ecol+1,
756		POS = src_span(Srow,Scol,Erow,Ecol,[],[]).
757		extract_perror_pos(pos(Srow,Scol,Filename),_,POS) :- !, % deprecated ?
758		S1 is Scol+0, % zero width span
759		POS = src_position_with_filename_and_ec(Srow,Scol,Srow,S1,Filename).
760		extract_perror_pos(pos(Srow,Scol,Erow,Ecol,Filename),_,POS) :- !,
761		%Ecol1 is Ecol+1,
762		POS = src_position_with_filename_and_ec(Srow,Scol,Erow,Ecol,Filename).
763		extract_perror_pos(pos(Srow,Scol),_,POS) :- !, print(deprecated_pos(Srow,Scol)),nl,
764		POS = src_position(Srow,Scol,none,1).
765		extract_perror_pos(Pos,_,Pos).
766
767
768		get_perror(error(Msg,Pos),error,Msg,Pos) :- !.
769		get_perror(internal_error(Msg,Pos),internal_error,Msg,Pos) :- !.
770		get_perror(warning(Msg,Pos),warning,Msg,Pos) :- !.
771		get_perror(M,_,M,unknown) :- format(user_error,'!!! unknown perror: ~w~n',[M]).
772
773		get_filename(Filenumber,Filenames,Filename) :-
774		number(Filenumber),!,
775		nth1(Filenumber,Filenames,Filename).
776		get_filename(N,F,R) :-
777		add_internal_error('Cannot get filename: ',get_filename(N,F,R)),
778		N=1,F=[R|_]. % return first file if possible
779
780		% check if error/warning occured and retract matching error/warning
781		get_error_with_span(Source,ErrMsg,Span) :-
782	?	retract(logged_error_hash(_Hash,Source,ErrMsg,_Context,Span)).
783		get_error(Source,ErrMsg) :-
784		retract(logged_error_hash(_,Source,ErrMsg,_,_)).
785		get_warning(Source,ErrMsg) :-
786		retract(logged_error_hash(_,warning(Source),ErrMsg,_,_)).
787
788		% now the same without actually retracting the error/warning:
789		check_error_occured(Source,ErrMsg) :- logged_error(Source,ErrMsg,_,_).
790		check_warning_occured(Source,ErrMsg) :- logged_error(warning(Source),ErrMsg,_,_).
791
792		get_error(Msg) :-
793		retract(logged_error_hash(_Hash,Source,ErrMsg,Context,Span)),
794		(extract_line_col(Span,StartLine,StartCol,EndLine,EndCol)
795		-> POS = ['\n ### Line: ',StartLine,', Column: ',StartCol|POS1],
796		((StartLine,StartCol) \= (EndLine,EndCol)
797		-> (StartLine=EndLine -> POS1 = [' until ',EndCol|POS2]
798		; POS1 = ['\n ### until Line: ',EndLine,', Column: ',EndCol|POS2]
799		)
800		; POS1 = POS2
801		),
802		(extract_additional_description(Span,CMsg)
803		-> POS2 = ['\n ### within: ',CMsg,'\n\n']
804		; POS2 = ['\n\n']
805		),
806		(extract_file_name(Span,Filename)
807		-> PosMsg = ['\n ### File: ',Filename | POS]
808		; PosMsg = POS
809		),
810		tools:ajoin(PosMsg,EndStr)
811		; EndStr = '\n\n'
812		),
813		((Context='' ; Context = '???')
814		-> string_concatenate(ErrMsg,EndStr,S0)
815		; safe_translate_error_term(Context,CString),
816		string_concatenate(CString,EndStr,CString2),
817		string_concatenate(': Context = ',CString2,CString3),
818		string_concatenate(ErrMsg,CString3,S0)
819		),
820		(debug_mode(off) -> Msg = S0
821		; decompose_error_source(Source,_,SrcAtom),
822		string_concatenate(SrcAtom,': ',S1),
823		string_concatenate(S1,S0,Msg)
824		).
825
826
827
828		get_error_with_span_info(ErrMsg,Type,ErrLocations) :-
829		retract(logged_error_hash(_Hash,Source,ErrMsg,_Context,Span)), % should we integrate source,context ?
830		(Source = warning(_) -> Type=warning
831		; Source = internal_error(_) -> Type=internal_error
832		; Type=error),
833		findall( error_span(Filename,StartLine,StartCol,EndLine,EndCol),
834		extract_position_from_span(Span,Filename,StartLine,StartCol,EndLine,EndCol),
835		ErrLocations).
836
837		extract_position_from_span(Span,Filename,StartLine,StartCol,EndLine,EndCol) :-
838		extract_line_col(Span,StartLine,StartCol,EndLine,EndCol),
839		(extract_file_name(Span,FName) -> Filename=FName ; Filename='').
840
841
842		tcltk_get_all_errors(Limit,list(Res),NrErrorsShown,NrErrors) :-
843		get_all_errors(All),
844		length(All,NrErrors),
845		(NrErrors =< Limit -> Res = All, NrErrorsShown = NrErrors
846		; prefix_length(All,Res,Limit), % truncate
847		NrErrorsShown = Limit
848		).
849
850		get_all_errors(All) :-
851		findall(Err,get_error(Err),All),
852		All \= [], clear_error_context.
853
854		get_all_errors_and_clear(All) :- findall(Err,get_error(Err),All),reset_errors_but_not_scopes,All \= [].
855		get_all_errors_and_reset(All) :- findall(Err,get_error(Err),All),reset_errors,All \= [].
856		get_all_errors_with_span_info_and_reset(All) :-
857		findall(error(ErrMsg,ErrType,ErrLocations),get_error_with_span_info(ErrMsg,ErrType,ErrLocations),All),
858		reset_errors.
859
860		error_or_warning_occured :- logged_error(_Source,_,_,_),!.
861		test_error_occurred(Source) :- logged_error(Source,_,_,_),real_error_occurred,!.
862
863		%:- use_module(library(lists),[length/2]). length is builtin
864
865		count_errors_occurred(Source,NrOfErrors) :-
866		findall(1,logged_error(Source,_,_,_),Ls),
867		length(Ls,NrOfErrors).
868
869		display_error_statistics :- findall(Source,logged_error(Source,_,_,_),L),
870		count_occurences(L,Occ),
871		format('Error manager summary: ~w~n',[Occ]).
872
873
874
875		:- volatile current_context/1.
876		:- dynamic current_context/1.
877
878		/* add context information; will be added to any error messages */
879		/* will be removed upon backtracking */
880		%push_error_context(_Ctx) :- !.
881		set_error_context(Ctx) :- % print(ctx(Ctx)),nl,
882		retractall(current_context(_)),
883		assert(current_context(Ctx)).
884		%push_error_context(_Ctx) :-
885		% (retract(current_context(_Ctx)) -> true ; print_error(could_not_retract_context(_Ctx))).
886
887		clear_error_context :- %print(clearing_ctx),nl,
888		retractall(current_context(_)).
889
890		%pop_error_context :-
891		% (retract(current_context(_Ctx)) -> true ; print_error(could_not_pop_context(_Ctx))).
892
893		get_error_context(C) :- (current_context(C) -> true ; C='???').
894
895		% restore an error context obtained by get_error_context
896		restore_error_context('???') :- !, clear_error_context.
897		restore_error_context(C) :- set_error_context(C).
898
899		get_error_span(Source,Span) :-
900		retract(logged_error_spans(Source,Span)).
901
902		% a way for external modules to register error locations, e.g., for display by Tcl/Tk HighlightSyntaxErrors
903		register_error_span(Source,Span) :- register_error_span(Source,Span,_).
904		register_error_span(_,unknown,New) :- !,New=false.
905		register_error_span(Source,Span,New) :- logged_error_spans(Source,Span),!,New=false.
906		register_error_span(Source,Span,New) :- assert(logged_error_spans(Source,Span)),New=true.
907
908		get_error_span_linecol(Line,Col,EndLine,EndCol) :- get_error_span_linecol(_Source,Line,Col,EndLine,EndCol).
909		get_error_span_linecol(Source,Line,Col,EndLine,EndCol) :-
910		get_error_span(Source,Span), % looks at logged_error_spans and retracts
911		extract_line_col(Span,Line,Col,EndLine,EndCol).
912
913		get_error_span_linecol_for_main_file(Line,Col,EndLine,EndCol) :-
914		get_error_span(_Source,Span), % looks at logged_error_spans and retracts even if not in main file !
915		extract_line_col_for_main_file(Span,Line,Col,EndLine,EndCol).
916
917		% just like get_error_span_linecol but does not retract and gets Filename
918		check_error_span_file_linecol(Source, FullFilename,Line,Col,EndLine,EndCol) :-
919		logged_error_spans(Source,Span),
920		extract_file_line_col(Span,FullFilename,Line,Col,EndLine,EndCol).
921
922		extract_file_line_col(Span,FullFilename,Line,Col,EndLine,EndCol) :-
923		(extract_file_number_and_name(Span,_,FullFilename) -> true ; FullFilename = unknown),
924		extract_line_col(Span,Line,Col,EndLine,EndCol).
925
926		% try and extract symbolic (Rodin label) information
927		extract_symbolic_pos([],_) :- !,fail.
928		extract_symbolic_pos([H|T],SymbolicPos) :- !,
929		posinfo_member(N,[H|T]),
930		extract_symbolic_pos(N,SymbolicPos),!.
931		extract_symbolic_pos(rodinpos(Label,_),Label). % see also get_texpr_labels in bsyntaxtree
932		extract_symbolic_pos(rodinpos(Model,Name,_),Label) :- ajoin([Model,':',Name],Label).
933		extract_symbolic_pos(label(Label),Label).
934
935		% quickly try and simplify a span, e.g., before asserting it in a fact (as it may become big)
936		simplify_span(b(E,_,Infos),Res) :- !,
937	?	(posinfo_member(N,Infos) -> Res=N
938		; first_sub_expr(E,A) -> simplify_span(A,Res)
939		; otherwise -> Res=unknown).
940		simplify_span(span_predicate(P,_,_),Res) :- !, simplify_span(P,Res).
941		simplify_span(S,S).
942
943		% choose first sub-expression in case top-expression has no position info (it would be better if extract_info/3 in bsyntaxtree merges position info)
944		first_sub_expr(negation(A,_),A).
945		first_sub_expr(conjunct(A,_),A).
946		first_sub_expr(disjunct(A,_),A).
947		first_sub_expr(implication(A,_),A).
948		first_sub_expr(equivalence(A,_),A).
949		first_sub_expr(exists([A|_],_),A).
950		first_sub_expr(forall([A|_],_),A).
951		first_sub_expr(let_predicate([A|_],_,_),A).
952		first_sub_expr(let_expression([A|_],_,_),A).
953		first_sub_expr(let_expression_global([A|_],_,_),A).
954		first_sub_expr(sequence([A|_]),A).
955		first_sub_expr(parallel([A|_]),A).
956		first_sub_expr(assign([A|_],_),A).
957		first_sub_expr(var([A|_],_),A).
958
959		%extract_line_col(S,_,_,_,_) :- print(extract(S)),nl,fail.
960		extract_line_col([],_,_,_,_) :- !,fail.
961		extract_line_col([H|T],Srow,Scol,Erow,Ecol) :- !,
962		posinfo_member(N,[H|T]),
963		extract_line_col(N,Srow,Scol,Erow,Ecol),!.
964		extract_line_col(closure(_,_,B),Srow,Scol,Erow,Ecol) :- !,
965		extract_line_col(B,Srow,Scol,Erow,Ecol).
966		extract_line_col(b(E,_,Infos),Srow,Scol,Erow,Ecol) :- !,
967		(extract_line_col(Infos,Srow,Scol,Erow,Ecol) -> true
968		; first_sub_expr(E,A) -> extract_line_col(A,Srow,Scol,Erow,Ecol)).
969		extract_line_col(span_predicate(P,_,_),Srow,Scol,Erow,Ecol) :- !,
970		extract_line_col(P,Srow,Scol,Erow,Ecol).
971		extract_line_col(pos(_,_Filenumber,Srow,Scol,Erow,Ecol),Srow,S1,Erow,E1) :- number(Srow),
972		% _Filenumber is an index into list provided by b_get_all_used_filenames
973		number(Scol), number(Erow), number(Ecol),!,
974		(Scol>0 -> S1 is Scol-1 ; S1 = Scol), % the BParser starts column numbering at 1
975		(Ecol>0 -> E1 is Ecol-1 ; E1 = Ecol).
976		%E1=Ecol. %Somehow the Ecol info is ok for Tcl
977		extract_line_col(unknown,_,_,_,_) :- !,fail.
978		extract_line_col(pos_context(A,_,_),StartLine,StartCol,EndLine,EndCol) :- !,
979		extract_line_col(A,StartLine,StartCol,EndLine,EndCol).
980		extract_line_col(src_span(_Filenumber,_Filename,StartLine,SC,EndLine,EC,Offset,LenBytes),StartLine,StartCol,EndLine,EndCol)
981		:- !, extract_line_col(src_span(StartLine,SC,EndLine,EC,Offset,LenBytes),StartLine,StartCol,EndLine,EndCol).
982		extract_line_col(src_span(StartLine,SC,EndLine,EC,_Off,[]),StartLine,StartCol,EndLine,EndCol)
983		:- !, StartCol is SC-1, EndCol is EC-1.
984		extract_line_col(src_span(SL,SC,EL,EC,_Off,_LenBytes),StartLine,StartCol,EndLine,EndCol) :- !,
985		StartLine=SL,StartCol is SC-1,EndLine = EL, EndCol is EC-1.
986		%:- !, StartCol is SC-1, EndCol is StartCol+LenBytes, EndLine = StartLine. %% fix because new library generates erroneous EndLine/EndCol info
987		% EndCol is EC-1.
988		extract_line_col(span_info(_Info,Span),SL,SC,EL,EC) :- !, extract_line_col(Span,SL,SC,EL,EC).
989		extract_line_col(src_span_operator(SP1,SP2),SL,SC,EL,EC) :- !,
990		(extract_line_col(SP1,SL,SC,EL,EC) ; extract_line_col(SP2,SL,SC,EL,EC)).
991		extract_line_col(multi_span(SL,SC,EL,EC,_Off,_Len,TAIL),StartLine,StartCol,EndLine,EndCol) :- !,
992		% TO DO: replace by multi_span/2
993		( StartLine = SL, StartCol is SC-1,
994		EndLine = EL, EndCol is EC-1
995		; extract_line_col(TAIL,StartLine,StartCol,EndLine,EndCol)).
996		%extract_line_col(multi_span(A,B),StartLine,StartCol,EndLine,EndCol) :- !,
997		% (extract_line_col(A,StartLine,StartCol,EndLine,EndCol) ;
998		% extract_line_col(B,StartLine,StartCol,EndLine,EndCol)).
999		extract_line_col(src_position(StartLine,SC,_Off,LenBytes),StartLine,StartCol,EndLine,EndCol) :- !,
1000		StartCol is SC-1, EndCol is StartCol+LenBytes, EndLine is StartLine.
1001		extract_line_col(src_position_with_filename(StartLine,SC,LenBytes,_Filename),StartLine,StartCol,EndLine,EndCol) :-
1002		!,
1003		StartCol is SC-1, EndCol is StartCol+LenBytes, EndLine is StartLine.
1004		extract_line_col(src_position_with_filename_and_ec(SL,SC,EL,EC,_Fname),StartLine,StartCol,EndLine,EndCol) :-
1005		!,
1006		StartLine=SL,StartCol is SC-1,EndLine = EL, EndCol is EC-1.
1007		extract_line_col(lineCol(StartLine,StartCol),StartLine,StartCol,EndLine,EndCol) :- !,
1008		EndLine=StartLine, EndCol=StartCol.
1009		extract_line_col(Struct,StartLine,StartCol,EndLine,EndCol) :-
1010		is_argument_of_compound_term(Struct,Arg),
1011		/* recursively look for error spans inside */
1012		extract_line_col(Arg,StartLine,StartCol,EndLine,EndCol),!.
1013		%extract_line_col(S,_,_,_,_) :- print('COULD NOT EXTRACT LINE/COL INFO: '), print(S),
1014		% functor(S,F,N), print(' '),print(F/N),nl,nl,fail.
1015
1016		:- use_module(library(between),[between/3]).
1017		is_argument_of_compound_term(Term,Arg) :- functor(Term,_,Arity),
1018		between(1,Arity,ArgNr), arg(ArgNr,Term,Arg).
1019
1020		/* For TCL TK: extract all line_col information in one go and in 4 lists */
1021		extract_all_line_col(Span, StartLineList,StartColList,EndLineList,EndColList) :-
1022		findall(lc(SL,SC,EL,EC), extract_line_col(Span,SL,SC,EL,EC),All),
1023		%print(all(All,Span)),nl,
1024		split_lc(All,StartLineList,StartColList,EndLineList,EndColList).
1025
1026		split_lc([], [],[],[],[]).
1027		split_lc([lc(SL,SC,EL,EC)|T],[SL|T1],[SC|T2],[EL|T3],[EC|T4]) :-
1028		split_lc(T,T1,T2,T3,T4).
1029
1030		% TO DO: merge with line_col and in Tcl/Tk use info to highlight proper file !
1031
1032		extract_file_name(Pos,Filename) :- extract_valid_file_number_and_name(Pos,_,Filename).
1033		extract_tail_file_name(Pos,Filename) :-
1034		extract_valid_file_number_and_name(Pos,_,FullFilename),
1035		tools:get_tail_filename(FullFilename,Filename).
1036		extract_subsidiary_tail_file_name(Pos,Filename) :-
1037		extract_valid_file_number_and_name(Pos,Nr,FullFilename),
1038		not_main_file(Nr,FullFilename),
1039		tools:get_tail_filename(FullFilename,Filename).
1040
1041		extract_valid_file_number_and_name(Pos,Nr,Filename) :-
1042		extract_file_number_and_name(Pos,Nr,Filename),
1043		valid_filename(Filename).
1044		valid_filename(F) :- atom(F). % not unknown(-1) which can come from REPL
1045
1046		% a version of extract_line_col which fails if the error is not in the main file
1047		extract_line_col_for_main_file(Span,Line,Col,EndLine,EndCol) :-
1048		extract_line_col(Span,Line,Col,EndLine,EndCol),
1049		\+((extract_file_number_and_name(Span,Nr,FullFilename),
1050		not_main_file(Nr,FullFilename))).
1051
1052
1053		extract_file_number_and_name(V,_,_) :- var(V),!,fail.
1054		extract_file_number_and_name(value(_),_,_) :- !,fail.
1055		extract_file_number_and_name(pos_context(A,_,_), Filenumber,Filename) :- !,
1056		extract_file_number_and_name(A, Filenumber,Filename).
1057		extract_file_number_and_name(pos(_,Filenumber,_,_,_,_), ResFileNr,Res) :-
1058		bmachine:b_get_all_used_filenames(FN),
1059		get_filename(Filenumber,FN,Filename),!,
1060		ResFileNr=Filenumber,Res=Filename.
1061		extract_file_number_and_name(pos(_,Filenumber,_,_,_,_), ResFileNr,Res) :- !, ResFileNr=Filenumber,Res=unknown(Filenumber). % unknown(-1) which can come from REPL
1062		extract_file_number_and_name(src_span(_,Filename,_,_,_,_,_,_), ResFileNr, Res) :- !,ResFileNr=unknown, Res=Filename.
1063		extract_file_number_and_name(src_position_with_filename(_,_,_,Filename), ResFileNr, Res) :- !,ResFileNr=unknown,Res=Filename.
1064		extract_file_number_and_name(src_position_with_filename_and_ec(_,_,_,_,Filename), ResFileNr, Res) :- !,ResFileNr=unknown,Res=Filename.
1065		extract_file_number_and_name(section(RodinFilename), ResFileNr, Res) :- !,ResFileNr=unknown,Res=RodinFilename.
1066		extract_file_number_and_name([H|T],Filenumber,Filename) :- !,
1067		posinfo_member(Arg,[H|T]),
1068		extract_file_number_and_name(Arg,Filenumber,Filename),!.
1069		extract_file_number_and_name(closure(_,_,B),Filenumber,Filename) :- !,
1070		extract_file_number_and_name(B,Filenumber,Filename).
1071		extract_file_number_and_name(b(E,_,Infos),Filenumber,Filename) :- !,
1072		(extract_file_number_and_name(Infos,Filenumber,Filename) -> true
1073		; first_sub_expr(E,A) -> extract_file_number_and_name(A,Filenumber,Filename)).
1074		extract_file_number_and_name(Struct,Filenumber,Filename) :-
1075		/* recursively look for error spans inside */
1076		is_argument_of_compound_term(Struct,Arg),
1077		extract_file_number_and_name(Arg,Filenumber,Filename),!.
1078
1079		posinfo_member(Arg,Args) :- % first look for a nodeid(.) member
1080	?	(member(nodeid(POS),Args) -> Arg=POS ; member(Arg,Args)).
1081
1082		%:- use_module(bmachine,[b_get_all_used_filenames/1,b_get_main_filenumber/1]).
1083		position_is_not_in_main_file(pos(_,Filenumber,_,_,_,_)) :- !, % B position info
1084		not_main_filenumber(Filenumber).
1085		position_is_not_in_main_file(src_span(_,Filename,_,_,_,_,_,_)) :- !,
1086		specfile:currently_opened_file_status(Main,_), Main \= Filename.
1087		position_is_not_in_main_file(src_position_with_filename(_,_,_,Filename)) :- !,
1088		specfile:currently_opened_file_status(Main,_), Main \= Filename.
1089		position_is_not_in_main_file(src_position_with_filename_ec(_,_,_,_,Filename)) :- !,
1090		specfile:currently_opened_file_status(Main,_), Main \= Filename.
1091		position_is_not_in_main_file(Struct) :- \+ atomic(Struct), Struct =.. [_|Args],
1092		/* recursively look for error spans inside */
1093	?	member(Arg,Args), position_is_not_in_main_file(Arg),!.
1094
1095
1096		not_main_file(Filenumber,_) :- number(Filenumber),!, % B Position info
1097		not_main_filenumber(Filenumber).
1098		not_main_file(_,Filename) :- % probably CSP position info; or unknown
1099		specfile:currently_opened_file_status(Main,_), \+ same_file_name(Main,Filename). %Main \= Filename.
1100
1101		:- use_module(tools,[get_tail_filename/2]).
1102		same_file_name(F1,F2) :-
1103		(F1=F2 -> true
1104		; get_tail_filename(F1,T1), get_tail_filename(F2,T2), T1=T2).
1105
1106		not_main_filenumber(Filenumber) :-
1107		bmachine:b_get_main_filenumber(MainFN),
1108		MainFN \= Filenumber.
1109
1110
1111
1112		% extract additional information about error span, e.g., Definition call context, other spans,...
1113		extract_additional_description(b(E,_,Infos),Desc) :- !,
1114		(extract_additional_description(Infos,Desc) -> true
1115		; first_sub_expr(E,A),extract_additional_description(A,Desc)).
1116		extract_additional_description(span_predicate(P,_,_),Desc) :- !,
1117		extract_additional_description(P,Desc).
1118		extract_additional_description([H|T],Desc) :- !,
1119		posinfo_member(N,[H|T]),
1120		extract_additional_description(N,Desc).
1121		extract_additional_description(closure(_,_,B),Desc) :- !,
1122		extract_additional_description(B,Desc).
1123		extract_additional_description(pos_context(MainPos,Context,CtxtPos),Desc) :- !,
1124		%nl,print(pos_context(MainPos,Context,CtxtPos)),nl,
1125		(extract_inner_context_description(MainPos,InnerCMsg)
1126		-> extract_context_msg(Context,OuterCMsg),
1127		ajoin([InnerCMsg,' within ',OuterCMsg],CMsg)
1128		; extract_context_msg(Context,CMsg)
1129		),
1130		(extract_span_description(CtxtPos,PosMsg)
1131		-> ajoin([CMsg,' at ',PosMsg],Desc)
1132		; Desc=CMsg). % no position info available
1133
1134		extract_context_msg(definition_call(Name),Msg) :- !, ajoin(['DEFINITION call of ',Name],Msg).
1135		extract_context_msg(C,Msg) :- ajoin(['CONTEXT: ',C],Msg).
1136
1137		extract_inner_context_description(pos_context(MainPos,Context,CtxtPos),Desc) :- !,
1138		extract_additional_description(pos_context(MainPos,Context,CtxtPos),Desc).
1139		% ---------------------------------
1140		:- dynamic backed_up_error/4.
1141
1142		% copy current error facts into backed_up_error facts
1143		backup_errors :-
1144		retractall(backed_up_error(_,_,_,_)),
1145		logged_error(Source,S,TContext,Span),
1146		assert(backed_up_error(Source,S,TContext,Span)),
1147		fail.
1148		backup_errors.
1149
1150