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(haskell_csp,[%clear_cspm_spec/0, % triggerred by clear specification event
6		parse_and_load_cspm_file/1, load_cspm_pl_file/1,
7
8		cspm_trans_enum/3,
9		animatable_process/1, animatable_process_cli/1,animatable_process_without_arguments/1,
10		channel/2, %cspPrintCompiled/2,
11		evaluate_argument/2, force_evaluate_argument/2, evaluate_int_argument/2,
12		force_evaluate_argument_for_member_check/2,
13		check_boolean_expression/1,
14
15		enumerate_channel_input_value/4,
16		enumerate_datatype_el/5,
17
18		is_a_datatype/2, csp_constructor/3,
19		%% csp_full_type_constructor/3,csp_full_type_constant/2, % exported by haskell_csp_analyzer.pl
20		dataTypeDef/2,
21		channel_type_list/2,
22		agent_compiled/3, % called in slicer_csp.pl ???
23		is_not_infinite_type/1,
24		channel_type_is_finite/2,
25		get_symbol_span/2,
26		extract_span_from_event/4, extract_span_info/2,
27		get_internal_csp_representation/1,
28		get_csp_assertions_as_string/2,get_csp_assertions/1, get_csp_processes/1,
29		translate_csp_assertion/2, %translate_csp_assertions/2, %get_csp_assertions_enum/2,
30		parse_and_load_cspm_file_into_specific_pl_file/2,
31		evaluate_type_list/2,
32		%% get_formula_from_cspm_file/2,
33		filter_formulas_from_pragmas/3,
34		add_error_with_span/4,add_internal_error_with_span/4,
35		evaluate_csp_expression/2,evaluate_csp_expression/3, parse_single_csp_expression/3,
36		evaluate_parsed_csp_expression_with_timing/2,
37		parse_single_csp_declaration/3,
38		add_symbol_error/4,
39		bindval/3, agent/3, agent_curry/3, subTypeDef/2, nameType/2,
40		symbol/4, cspTransparent/1, cspPrint/1, valid_constant/1,
41		parse_single_csp_expression_file/3,
42		%% perform_csp_self_check/0,
43		normalise_cspm_state/2,
44		check_compiled_term/1,
45		get_cspm_identifier/2,
46		ignore_infinite_datatypes/0 % TODO: get rid of this ugly hack
47		]).
48
49
50		:- meta_predicate read_compiled_prolog_file(-,-,1).
51
52		:- use_module(probsrc(module_information)).
53		:- module_info(group,csp).
54		:- module_info(description,'Interpreter for CSP.').
55
56		:- use_module(library(lists)).
57		:- use_module(library(file_systems)).
58		%% :- use_module(library(process)).
59		%% :- use_module(library(system)).
60
61		/* the new CSP interpreter using the format produced by
62		Marc's Haskell compiler fecsp/cspcomp */
63
64		/********* PROB modules *********/
65		:- use_module(probsrc(error_manager)).
66		:- use_module(probsrc(self_check)).
67		:- use_module(probsrc(debug)).
68		:- use_module(probsrc(typechecker)).
69		:- use_module(probsrc(kernel_objects),[top_level_dif/2,enumerate_basic_type/3]).
70		:- use_module(probsrc(tools),[string_concatenate/3,flatten/2,split_atom/3, get_set_optional_prolog_flag/3]).
71		:- use_module(probsrc(preferences),[preference/2, set_preference/2, get_preference/2,init_preferences/0]).
72		:- use_module(probsrc(system_call),[system_call/4,system_call/5, get_writable_compiled_filename/3]).
73		:- use_module(probsrc(kernel_waitflags)).
74		:- use_module(probsrc(translate),[translate_cspm_state/2,translate_cspm_expression/2]).
75		:- use_module(probsrc(specfile),[process_algebra_mode/0,csp_with_bz_mode/0,currently_opened_file/1]).
76		/******** ------------ *********/
77
78		:- set_prolog_flag(double_quotes, codes).
79
80		/* Predicate for performing self check for all CSP modules */
81
82		:- public perform_general_csp_self_check/0.
83		perform_general_csp_self_check :-
84		perform_csp_self_check,
85		get_preference(use_clpfd_solver,Value),
86		(Value=false ->
87		NewValue = true
88		; NewValue = false),
89		set_preference(use_clpfd_solver,NewValue),
90		perform_csp_self_check,
91		% reverting to the old use_clpfd_solver preference
92		set_preference(use_clpfd_solver,Value).
93
94		perform_csp_self_check :-
95		init_preferences,
96		perform_self_check(csp_basic),
97		perform_self_check(csp_tuples),
98		perform_self_check(csp_sequences),
99		perform_self_check(csp_sets),
100		perform_self_check(haskell_csp),
101		perform_self_check(haskell_csp_analyzer).
102
103		/* ------------------------------------- */
104
105
106		:- dynamic channel/2, bindval/3, agent/3, agent_curry/3, dataTypeDef/2, subTypeDef/2.
107		:- dynamic nameType/2, symbol/4, cspTransparent/1, cspPrint/1, assertRef/5.
108		:- dynamic assertModelCheck/3, assertModelCheckExt/4, pragma/1.
109		%:- dynamic assertLtl/4, assertCtl/4. % dynamic declarations still generated by parser it seems, but not used
110
111		:- discontiguous channel/2, agent/3, bindval/3, assertModelCheck/3.
112
113		:- use_module(probcspsrc(haskell_csp_analyzer)).
114		:- use_module(probcspsrc(csp_tuples)).
115		:- use_module(probcspsrc(csp_sets)).
116		:- use_module(probcspsrc(csp_basic)).
117
118		/* ------------------------------------- */
119		/* Sample .pl Translation of a CSP file */
120
121		dataTypeDef('FRUIT',[constructor(apples),constructor(oranges),constructor(pears)]).
122		channel(left,type(dotTupleType(['FRUIT']))).
123		bindval('SEND',prefix(span,[in(_x)],left,prefix(span,[out(_x)],mid,prefix(span,[],ack,val_of('SEND',no_loc_info_available))),span2),span).
124		symbol('SEND','SEND',src,'Process').
125
126
127		:- use_module(probsrc(eventhandling),[register_event_listener/3]).
128		:- register_event_listener(start_unit_tests,reset_for_selfcheck,'Setup CSP dataTypeDef, channel,..').
129		%:- register_event_listener(stop_unit_tests, set_silent(false), 'Printing wf warnings again').
130
131		reset_for_selfcheck :- % TO DO: reset all facts and link with event_handling
132		clear_cspm_spec,
133		retractall(dataTypeDef(_,_)),
134		assertz( dataTypeDef('FRUIT',[constructor(apples),constructor(oranges),constructor(pears)])),
135		/* for testing is_not_infinite_type predicate */
136		assertz( dataTypeDef('Msg',[constructor('A'),constructor('B'),constructorC('con',dotTupleType(['SubMsg']))]) ),
137		assertz( dataTypeDef('Msg1',[constructor('A'),constructor('B')]) ),
138		assertz( dataTypeDef('SubMsg',[constructor('KA'),
139		constructorC(conc,dotTupleType(['Msg'])),constructorC(ste,dotTupleType([builtin_call('Seq'('Msg'))]))]) ),
140		assertz( dataTypeDef('Inf',[constructorC(ste,dotTupleType([builtin_call('Seq'('FRUIT'))]))]) ),
141		retractall( channel(_,_)),
142		assertz( channel(left,type(dotTupleType(['FRUIT']))) ),
143		assertz( channel(right,type(dotTupleType(['FRUIT']))) ),
144		assertz( channel(mid,type(dotTupleType(['FRUIT']))) ),
145		assertz( channel(receive,type(dotTupleType(['Msg']))) ),
146		assertz( channel(infinite,type(dotTupleType(['Inf']))) ),
147		retractall( bindval(_,_,_) ),
148		assertz( bindval('SEND',
149		prefix(no_loc_info_available,[in(_x)],left,
150		prefix(no_loc_info_available,[out(_x)],mid,
151		prefix(no_loc_info_available,[],ack,val_of('SEND',no_loc_info_available),no_loc_info_available),
152		no_loc_info_available),
153		no_loc_info_available),no_loc_info_available) ),
154		assertz( bindval('REC',prefix(no_loc_info_available,[in(_x)],mid,
155		prefix(no_loc_info_available,[out(_x)],right,
156		prefix(no_loc_info_available,[],ack,val_of('REC',no_loc_info_available),no_loc_info_available),
157		no_loc_info_available),no_loc_info_available),no_loc_info_available) ),
158		assertz( bindval('SYSTEM',sharing(closure([mid,ack]),val_of('SEND',no_loc_info_available),
159		val_of('REC',no_loc_info_available),no_loc_info_available),no_loc_info_available) ),
160		assertz( bindval('GEN1',
161		prefix(no_loc_info_available,[out(oranges)],
162		left,
163		prefix(no_loc_info_available,[out(oranges)],right,val_of('GEN2',no_loc_info_available),no_loc_info_available),
164		no_loc_info_available),no_loc_info_available) ),
165		assertz( bindval('GEN2',
166		prefix(no_loc_info_available,[out(pears)],left,
167		prefix(no_loc_info_available,[out(pears)],
168		right,val_of('GEN1',no_loc_info_available),no_loc_info_available),no_loc_info_available),no_loc_info_available) ),
169		assertz( bindval('MAIN',sharing(closure([left,right]),val_of('SYSTEM',no_loc_info_available),val_of('GEN1',no_loc_info_available),no_loc_info_available),no_loc_info_available) ),
170		assertz( bindval('P1',agent_call(no_loc_info_available,'Q',[int(10)]),no_loc_info_available) ),
171		retractall(agent(_,_,_)),
172		assertz( agent('P'(_),'prefix'('src_span'(8,8,8,9,87,1),['in'(_i2)],'c',
173		'prefix'('src_span'(8,15,8,16,94,1),['out'(_i2)],'c',
174		'stop'('src_span'(8,22,8,26,101,4)),'src_span'(8,19,8,21,97,10)),
175		'src_span'(8,12,8,14,90,17)),'src_span'(8,8,8,26,87,18)) ),
176		%assertz( agent('P2'(_n),agent_call(no_loc_info_available,'Q',['-'(_n, int(10))]),no_loc_info_available) ),
177		%assertz( agent('P1',agent_call(no_loc_info_available,'Q',[int(10)]),no_loc_info_available) ),
178		assertz( agent('Q'(_n),ifte('=='(_n,int(0)),stop(no_loc_info_available),
179		prefix(no_loc_info_available,[],'a',
180		agent_call(no_loc_info_available,'Q',['-'(_n,'int'(1))]),no_loc_info_available),
181		no_loc_info_available,no_loc_info_available,no_loc_info_available),no_loc_info_available) ),
182		retractall(symbol(_,_,_,_)),
183		assertz( symbol('SEND','SEND',src,'Process') ),
184		assertz( symbol('REC','REC',src(8,1,8,4,4,3),'Procsess') ),
185		assertz( symbol('SYSTEM','SYSTEM',src,'Process') ),
186		assertz( symbol('GEN1','GEN1',src,'Process') ),
187		assertz( symbol('GEN2','GEN2',src,'Process') ),
188		assertz( symbol('MAIN','MAIN',src(3,1,3,5,20,4),'Process') ),
189		retractall(assertRef(_,_,_,_,_)),
190		assertz( assertRef('False','val_of'('MAIN',no_loc_info_available),'Trace',
191		'val_of'('PROB_TEST_TRACE',no_loc_info_available),no_loc_info_available) ),
192		assertz( assertRef('True', 'val_of'('PROB_TEST_TRACE',no_loc_info_available),
193		'Trace', 'val_of'('MAIN',no_loc_info_available),no_loc_info_available) ),
194		retractall(assertModelCheckExt(_,_,_,_)),
195		assertz( assertModelCheckExt('False',
196		sharing(closure([left,right]),val_of('SYSTEM',no_loc_info_available),
197		val_of('GEN1',no_loc_info_available),no_loc_info_available), 'Deterministic','F') ),
198		assertz( assertModelCheckExt('True',
199		sharing(closure([left,right]),val_of('SYSTEM',no_loc_info_available),
200		val_of('GEN1',no_loc_info_available),no_loc_info_available), 'DeadlockFree','FD') ),
201		retractall(assertModelCheck(_,_,_)),
202		assertz( assertModelCheck('False',
203		'prefix'(no_loc_info_available,[],'dotTuple'(['a','int'(1)]),
204		'val_of'('P',no_loc_info_available),no_loc_info_available),'LivelockFree')),
205		retractall(pragma(_)),
206		assertz(pragma('assert_ltl "GF(a)"')),
207		assertz(pragma('ASSERT_LTL "GF(b)"')),
208		assertz(pragma('ASSERT_LTL_TRUE "true"')),
209		haskell_csp_analyzer:analyze.
210
211
212		% these predicates are generated by the csp analyzer, there are not the standard generated predicates from the translation
213		% process csp -> pl
214
215		/* ------------------------------------- */
216
217		/* ------------------------------------- */
218
219		animatable_process_without_arguments(X) :-
220	?	symbol(RenamedX,X,_,_),
221	?	(is_csp_process(RenamedX);is_possible_csp_process(RenamedX)).
222
223		animatable_process(X) :-
224	?	(symbol(RenamedX,X,_,_),(is_csp_process(RenamedX);is_possible_csp_process(RenamedX))) ;
225		(nonvar(X), X=agent_call(_Src,_F,_Args)) ;
226		(nonvar(X), X=agent_call_curry(_F,_Args)) ;
227	?	(agent(F,_,_),is_csp_process(F),animatable_process_with_arguments(F,proc(FName,N)),proc_with_arguments_to_string(FName,N,X)).
228
229		animatable_process_cli(X) :-
230		symbol(RenamedX,X,_,_),
231		(is_csp_process(RenamedX) ; is_possible_csp_process(RenamedX)).
232
233		animatable_process_with_arguments(X,proc(F,N)) :-
234		functor(X,F,N),N>0.
235
236		check_compiled_term(Term) :-
237		nonvar(Term),!,
238		Term=agent_call(_Src,F,Args),
239		length(Args,N),
240		( (symbol(RenamedF,F,_,_),functor(P,RenamedF,N),is_csp_process(P)) ->
241		true
242		; translate_cspm_state(Term,Proc),
243		add_error_fail(check_compiled_term, 'There is no such process in file: ',Proc)
244		).
245
246		/* ------------------------------------- */
247
248		/* Predicates for calling the CSPM Parser and loading the corresponding to the Csp File Prolog File */
249
250		parse_and_load_cspm_file(CSPFile) :-
251		\+ file_exists(CSPFile),
252		!,
253		add_error_fail(parse_and_load_cspm_file,'CSP file does not exist:',CSPFile).
254		parse_and_load_cspm_file(CSPFile) :-
255		get_writable_compiled_filename(CSPFile,'.pl',PrologFile),
256		parse_and_load_cspm_file_into_specific_pl_file(CSPFile,PrologFile).
257
258		%% parse_and_load_cspm_file(CSPFile) :-
259		%% (parsercall: call_cspmj_parser(CSPFile,PrologFile)
260		%% -> load_cspm_pl_file(PrologFile,CSPFile)
261		%% ; add_error(parse_and_load_cspm_file,'Error while parsing CSP file: ',CSPFile),
262		%% add_error_fail(parse_and_load_cspm_file,'Std error: ','to be added')
263		%% ).
264
265		/* Specific predicate for parsing and re-writting the Parse-Output into already existing prolog file.*/
266		% It will be needed by parsing a temporary files when the Csp Assertion Viewer is used.
267		parse_and_load_cspm_file_into_specific_pl_file(CSPFile, PrologFile) :-
268		debug_println(15,reading_cspm_file(CSPFile)),
269		get_cspm_parser_command(AbsParseCmd),
270		debug_println(5,parsecmd(AbsParseCmd)),
271		string_concatenate('--prologOut=', PrologFile, PrologFileOutArg),
272		debug_stats(parsing(AbsParseCmd,'translate',PrologFileOutArg, CSPFile)),
273		system_call(AbsParseCmd, ['translate',PrologFileOutArg, CSPFile], Text,JExit),
274		debug_stats(done_parsing),
275		debug_println(15,parse_exit(JExit)),
276		(JExit=exit(0)
277		-> load_cspm_pl_file(PrologFile,CSPFile)
278		; add_internal_error('Error while parsing CSP file: ',CSPFile),
279		atom_codes(T,Text),
280		add_error_fail(parse_and_load_cspm_file,'Std error: ',T)
281		).
282
283		parse_single_csp_declaration(Decl,CSPFile,Result) :-
284		get_cspm_parser_command(Cmd),
285		string_concatenate('--declarationToPrologTerm=', Decl, DeclarationArgument),
286		system_call(Cmd, ['translate', DeclarationArgument, CSPFile],Text,ErrText,JExit),
287		(JExit=exit(0)
288		-> read_from_codes(Text,Result)
289		; atom_codes(ErrT,ErrText),
290		add_error_fail(parsing_csp_declaration,'Std error: ',ErrT)
291		).
292
293		:- use_module(probsrc(xtl_interface),[last_opened_cspm_file/1]).
294		parse_single_csp_expression(Context,Expr,Res) :-
295		( Context==eval -> Filename='no-file'
296		; Context==ltl ->
297		(csp_with_bz_mode
298		-> last_opened_cspm_file(Filename)
299		; currently_opened_file(Filename)
300		)
301		; add_internal_error('Internal Error: Unknown context argument: ', Context),fail
302		),
303		parse_single_csp_expression_file(Expr,Filename,Res).
304
305		:- use_module(library(codesio)).
306		parse_single_csp_expression_file(Expr,CSPFile,Res) :-
307		get_cspm_parser_command(Cmd),
308		string_concatenate('--expressionToPrologTerm=', Expr, ExpressionArgument),
309		system_call(Cmd, ['translate', ExpressionArgument, CSPFile],Text,ErrText,JExit),
310		(JExit=exit(0)
311		-> read_from_codes(Text,Result),
312		translate_expression(Result,Res)
313		; atom_codes(ErrT,ErrText),
314		add_error_fail(parsing_csp_expression,'Std error: ',ErrT)
315		).
316
317		evaluate_csp_expression(Expr,Result) :-
318		( parse_single_csp_expression(eval,Expr,ParsedExpr) ->
319		evaluate_parsed_csp_expression(ParsedExpr,Expr,Result)
320		; add_error_fail(parsing_csp_expression, 'Error while parsing expression: ', Expr)
321		).
322
323		evaluate_parsed_csp_expression(ParsedExpr,Expr,Result) :-
324		debug_println(9,parsed_csp_expression(ParsedExpr)),
325	?	haskell_csp_analyzer:compile_body(ParsedExpr,'evaluate',[],[],CompiledExpr),
326		( evaluate_parsed_csp_expression_with_timing(CompiledExpr,Res) ->
327		( translate_cspm_expression(Res, R) -> R=Result
328		; add_error_fail(pretty_printing_evaluated_expression, 'Error while pretty-printing result: ', Res)
329		)
330		; add_error_fail(evaluating_expression, 'Error while evaluating expression: ',Expr)
331		).
332
333		evaluate_csp_expression(Expr,CSPFile,Result) :-
334		( parse_single_csp_expression_file(Expr, CSPFile,ParsedExpr) ->
335	?	evaluate_parsed_csp_expression(ParsedExpr,Expr,Result)
336		; add_error_fail(parsing_csp_expression, 'Error while parsing typed expression: ', Expr)
337		).
338
339		:- use_module(probsrc(tools),[cputime/1]).
340		evaluate_parsed_csp_expression_with_timing(ParsedExpr,Res) :-
341		cputime(T1),
342		evaluate_expression(ParsedExpr,Res),
343		cputime(T2),
344		D is T2-T1,
345		print('% Time to evaluate expression: '),print(D), print(' ms.%'),nl.
346
347		% TODO: Which are the expressions allowed to be written in events
348		translate_expression(listExp(rangeEnum(List)),Res) :- !, Res=list(List).
349		translate_expression(setExp(rangeEnum(List)),Res) :- !, Res=setValue(List).
350		translate_expression(dotTuple(List),dotTuple(Res)) :- !,
351		maplist(translate_expression,List,Res).
352		translate_expression(X,X).
353
354		/* Predicates for reading a Prolog file (usually generated after translating the appropriate Csp file with the CSPM-Tool)
355		and filtering the asssertion declarations from it. Needed for the 'Check Csp Assertions' window in Tcl_Tk. */
356		read_compiled_prolog_file(CSPFile,Result,PredName) :-
357		get_writable_compiled_filename(CSPFile,'.pl', PrologFile),
358		debug_print(9,'opening Prolog file: '), debug_println(9,PrologFile),
359		my_see(PrologFile),
360		call(PredName,Result),
361		!,seen,debug_println(9,done).
362
363		my_see(File) :-
364		catch(see(File),
365		error(existence_error(_,_),_),
366		add_error_fail(my_see,'File does not exist: ',File)).
367
368		filter_assertion_declarations(Assertions) :-
369		read(Term), !,
370		((Term = end_of_file) -> (Assertions = [])
371		; (is_assertion(Term)
372		-> (Assertions = [Term|T])
373		; (Assertions = T)
374		), filter_assertion_declarations(T)
375		).
376
377		:- assert_must_succeed((is_assertion(assertRef(_,_,_,_,_)),is_assertion(assertModelCheck(_,_,_)), is_assertion(assertModelCheckExt(_,_,_,_)))).
378
379		is_assertion(assertRef(_,_,_,_,_)).
380		is_assertion(assertModelCheck(_,_,_)).
381		is_assertion(assertModelCheckExt(_,_,_,_)).
382		is_assertion(assertLtl(_,_,_,_)).
383		is_assertion(assertCtl(_,_,_,_)).
384
385		filter_formulas_from_pragmas(Type,FlNList,FlFList) :-
386		findall(Formulas,(pragma(S),get_formulas_from_pragma(Type,pragma(S),_Names,Formulas)),FList),
387		findall(Names,(pragma(S),get_formulas_from_pragma(Type,pragma(S),Names,_Formulas)),NList),
388		flatten(NList,FlNList),
389		flatten(FList,FlFList).
390
391		get_formula_from_cspm_file(Type,Formula) :-
392		filter_formulas_from_pragmas(Type,_Ns,[String|_]),
393		(var(String) ->
394		Formula = ''
395		; Formula=String
396		).
397
398		get_formulas_from_cspm_file(Type,String) :-
399		filter_formulas_from_pragmas(Type,_Ns,Formulas),
400		convert_string_list_to_string(Formulas,String).
401
402		string_concatenate_sep(Sep,Atom,R) :-
403		string_concatenate(Atom,Sep,R).
404
405		convert_string_list_to_string(L,Res) :-
406		maplist(string_concatenate_sep(';'),L,LRes),
407		concatenate_string_list(LRes,Res).
408
409		get_formulas_from_pragma(Type,pragma(Str),Names,Formulas) :-
410		atom_codes(Str,CodeList),
411		(Type = ltl ->
412	?	ltl_equations(Names,Formulas,CodeList,[])
413		;Type = ctl ->
414		ctl_equations(Names,Formulas,CodeList,[])
415		;
416		Names=[], Formulas=[]
417		).
418
419		%%%%%%%%%%%%%%%%%% Tests for the ASSERT_LTL Equations Parser below %%%%%%%%%%%%%%%%%%%%%%%%%%%%%
420
421		:- assert_must_succeed((haskell_csp:reset_for_selfcheck)).
422		:- assert_must_succeed((haskell_csp: get_formulas_from_pragma(ltl,pragma('ASSERT_LTL_123=="F(e(a))" "Checking simple LTL property."'),
423		Names,Formulas),Names==[123],Formulas==['F(e(a))'])).
424		:- assert_must_fail((haskell_csp: get_formulas_from_pragma(ltl,pragma('ASSERT_LTL_0123=="F(e(a))" "First digit in number must be nonzero."'),
425		_Names,_Formulas))).
426		:- assert_must_succeed((haskell_csp: get_formulas_from_pragma(ltl,pragma('ASSERT_LTL=="F(e(a))"'),
427		Names,Formulas),Names==[[95]],Formulas==['F(e(a))'])).
428		:- assert_must_succeed((haskell_csp: get_formulas_from_pragma(ltl,pragma('assert_ltl "F(e(a))" "Checking simple LTL property."'),
429		Names,Formulas),Names==[[95]],Formulas==['F(e(a))'])).
430		:- assert_must_succeed((haskell_csp: get_formulas_from_pragma(ctl,pragma('assert_ctl "true" "Checking simple CTL property."'),
431		Names,Formulas),Names==[[95]],Formulas==['true'])).
432		:- assert_must_succeed((haskell_csp: get_formulas_from_pragma(ltl,pragma('assert_ltl "F(e(a))" "Parsing multiple LTL equations."; ASSERT_LTL_TRUE "F(e(b))"; ASSERT_LTL_2=="F(e(c))"; ASSERT_LTL "F(e(d))"'),
433		Names,Formulas),Names==[[95],[84,82,85,69],2,[95]],Formulas==['F(e(a))','F(e(b))','F(e(c))','F(e(d))'])).
434		:- assert_must_succeed((
435		haskell_csp: get_formulas_from_cspm_file(ltl,S), S == 'GF(a);GF(b);true;')).
436		:- assert_must_succeed((
437		haskell_csp: get_formula_from_cspm_file(ltl,S), S == 'GF(a)')).
438
439		%%%%%%%%%%%%%%%%%% Simple Parser for Parsing ASSERT_LTL Equations %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
440
441		%%%%%%%%%%%%% CTL assertions %%%%%%%%%%%%%%%
442		ctl_equations([N|Ns],[F|Fs]) --> ctl_equation(N,F),ctl_equations2(Ns,Fs).
443		ctl_equations2(Ns,Fs) --> ows,sep,ows,ctl_equations(Ns,Fs),{Fs\=[],Ns\=[]}.
444		ctl_equations2([],[]) --> ows.
445
446		ctl_equation(N,F) --> ows,assert_id_ctl(N), ows, eq,!, ows, string(F), ows, optional_string.
447
448		assert_id_ctl(N) --> ass_ctl,!,ass_name(N).
449		assert_id_ctl(N) --> "assert_ctl",{N="_"},!.
450		assert_id_ctl(N) --> "ASSERT_CTL",{N="_"},!.
451
452		ass_ctl --> "ASSERT_CTL_".
453		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
454
455	?	ltl_equations([N|Ns],[F|Fs]) --> ltl_equation(N,F),ltl_equations2(Ns,Fs).
456	?	ltl_equations2(Ns,Fs) --> ows,sep,ows,ltl_equations(Ns,Fs),{Fs\=[],Ns\=[]}.
457		ltl_equations2([],[]) --> ows.
458
459		ltl_equation(N,F) --> ows,assert_id_ltl(N), ows, eq,!, ows, string(F), ows, optional_string.
460
461		string(Atom) --> [34], stringcontent(String), [34], {atom_codes(Atom,String)}. %34 is Ascii Code of "
462
463		optional_string --> [34], stringcontent(_String), [34],!.
464		optional_string --> "",!.
465
466		stringcontent([C|Rest]) --> [C], {C \= 34}, !, stringcontent(Rest).
467		stringcontent([]) --> [].
468
469		assert_id_ltl(N) --> ass,!,ass_name(N).
470		assert_id_ltl(N) --> "assert_ltl",{N="_"},!.
471		assert_id_ltl(N) --> "ASSERT_LTL",{N="_"},!.
472
473	?	ass_name(N) --> num(N),{number(N)},!.
474		ass_name(N) --> name_tail(N),!.
475
476		name_tail([C|Cs]) --> [C],{is_digit(C) ;
477		(0'A =< C,C =< 0'Z) ;
478		(0'a =< C,C =< 0'z) ;
479		C=0'_},
480		name_tail(Cs),!.
481		name_tail([]) --> [],!.
482
483		num(Number) --> nonzerodigit(D), num2(Rest),{number_codes(Number,[D|Rest])}.
484		num(Number) --> digit(D),{number_codes(Number,[D])}.
485		num2([D|Rest]) --> digit(D),!,num2(Rest).
486		num2([]) --> [].
487
488		digit(D) --> [D], {is_digit(D)},!.
489		nonzerodigit(ND) --> [ND], {is_nz_digit(ND)},!.
490
491		is_digit(D) :- 0'0 =< D, D =< 0'9.
492		is_nz_digit(D) :- 0'0 < D, D =< 0'9.
493
494	?	sep --> [C],{member(C,";,")}.
495
496	?	ows --> [C], {member(C," \t\n\r")}, !, ows.
497		ows --> "".
498
499		eq --> "==",!.
500		eq --> [32],!.
501		eq --> "",!.
502
503		ass --> "ASSERT_LTL_",!.
504
505		/* ------------------------------------------------------------------------------------------------------------- */
506
507		/* Predicates for getting the CSPM-Tool command from the library and loading cspm Prolog files.*/
508		get_cspm_parser_command(AbsParseCmd) :-
509		debug_println(9,getting_parser_cmd),
510		catch(
511		absolute_file_name(prob_lib(cspmf),AbsParseCmd,[access(exist),extensions(['.exe',''])]),
512		error(E,_),
513		add_error_fail(haskell_csp,'Could not find CSP-M Parser. Be sure to install cspmf in your ProB lib directory. ',E)),
514		debug_println(9,parser(AbsParseCmd)).
515
516
517		:- dynamic parseResult/5.
518		load_cspm_pl_file(PFile) :- load_cspm_pl_file(PFile,PFile).
519		load_cspm_pl_file(PrologFile,CSPFile) :- clear_cspm_spec,
520		\+ file_exists(PrologFile),!,
521		add_error(haskell_csp,'Could not generate Prolog encoding of CSP file: ',CSPFile),fail.
522		load_cspm_pl_file(PrologFile,CSPFile) :-
523		debug_println(15,consulting(PrologFile)),
524		cia_consult_without_redefine_warning(PrologFile), debug_stats(done_loading_pl_file),
525		/* TO DO: replace by safer load which checks that
526		only correct facts are loaded !!!! */
527		parseResult(ParseResult,ErrorMsg,StartLine,SC,Off),
528		(ParseResult='ok' -> analyze ;
529		add_error(haskell_csp,'Error while parsing CSP-M: ',ParseResult:CSPFile),
530		add_error(haskell_csp,'CSP-M Parse error message: ',ErrorMsg,src_position(StartLine,SC,Off,1))
531		).
532
533		/* ------------------------------------------------------------------------------------------------------------ */
534
535		% A small pretty-printer for printing assert declarations
536		refinement_operator('Trace',' [T= ') :- !.
537		refinement_operator('Failure', ' [F= ') :- !.
538		refinement_operator('FailureDivergence',' [FD= ') :- !.
539		refinement_operator('RefusalTesting',' [R= ') :- !.
540		refinement_operator('RefusalTestingDiv',' [RD= ') :- !.
541		refinement_operator('RevivalTesting',' [V= ') :- !.
542		refinement_operator('RevivalTestingDiv',' [VD= ') :- !.
543		/* the clauses below will be called if we check the particular assertion direct from the command line and not from the .pl file */
544		refinement_operator('[T=',' [T= ') :- !.
545		refinement_operator('[F=', ' [F= ') :- !.
546		refinement_operator('[FD=',' [FD= ') :- !.
547		refinement_operator('[R=',' [R= ') :- !.
548		refinement_operator('[RD=',' [RD= ') :- !.
549		refinement_operator('[V=',' [V= ') :- !.
550		refinement_operator('[VD=',' [VD= ') :- !.
551		refinement_operator(A, _) :- add_error_fail(haskell_csp, 'Error while pretty-printing assert declaration. Invalid or unsupported refinement operator: ', A).
552
553		adding_not('True', 'not ') :- !.
554		adding_not('False', '') :- !.
555		adding_not(A,_) :- add_error_fail(haskell_csp,'Error while pretty-printing assert declaration. Unexpected argument infront the assertion declaration: ',A).
556
557		fdr_model('Deterministic', ' :[ deterministic ') :- !.
558		fdr_model('DeadlockFree', ' :[ deadlock free ') :- !.
559		fdr_model('LivelockFree', ' :[ livelock free ') :- !.
560		fdr_model(A,_) :- add_error_fail(haskell_csp, 'Error while pretty-printing assert declaration. Invalid or unsupported model inside of process assertion: ', A).
561
562		fdr_single_model('Deterministic', ' :[ deterministic [FD] ]') :- !.
563		fdr_single_model('DeadlockFree', ' :[ deadlock free [FD] ]') :- !.
564		fdr_single_model('LivelockFree', ' :[ livelock free ]') :- !.
565		fdr_single_model(A,_) :- add_error_fail(haskell_csp, 'Error while pretty-printing assert declaration. Invalid or unsupported model inside of process assertion: ', A).
566
567		fdr_ext('F', '[F] ]') :- !.
568		fdr_ext('FD', '[FD] ]') :- !.
569		fdr_ext(Ext, _) :- add_error_fail(haskell_csp, 'Not supported assertion type model: ',Ext).
570
571		:- assert_must_fail(proc_with_arguments_to_string('P',0,_)).
572		:- assert_must_fail(proc_with_arguments_to_string('P',-10,_)).
573		:- assert_must_succeed((proc_with_arguments_to_string('P',1,String), String=='P(-)')).
574		:- assert_must_succeed((proc_with_arguments_to_string('P',3,String), String=='P(-,-,-)')).
575
576		proc_with_arguments_to_string(Fun,N,FunRes) :-
577		( N>1 ->
578		count_proc_arguments(N,R),
579		concatenate_string_list([Fun,'('|R],FunRes)
580		; N =:= 1 ->
581		string_concatenate(Fun,'(-)',FunRes)
582		).
583
584		count_proc_arguments(N,Res) :-
585		count_proc_arguments(N,['-',')'],Res).
586
587		count_proc_arguments(N,L,Res) :-
588		(N =:= 1 ->
589		Res=L
590		; N>1 ->
591		N1 is N-1,
592		count_proc_arguments(N1,['-',','|L],Res)
593		).
594
595		:- assert_must_succeed((string_to_proc_term('P(-,-,-)',Term), Term = 'P'(_A,_B,_C))).
596		:- assert_must_succeed((string_to_proc_term('P(-)',Term), Term = 'P'(_X))).
597		:- assert_must_succeed((string_to_proc_term('P',Term), Term = 'P')).
598		:- assert_must_succeed((string_to_proc_term(p(1,2),Term), Term == p(1,2))).
599
600		string_to_proc_term(Proc,Term) :-
601		atom(Proc),!,
602		split_atom(Proc,['(',',',')'],[Fun|A]),
603		length(A,N),
604		gen_vars(N,Args),
605		Term =.. [Fun|Args].
606		string_to_proc_term(X,X).
607
608		:- assert_must_succeed((string_to_proc_term('P(-,-,-)',Term), functor(Term,F,N), proc_with_arguments_to_string(F,N,Str), Str == 'P(-,-,-)')).
609
610		gen_vars(N,Vars) :-
611		( N>0 -> N1 is N-1, gen_vars(N1,T),Vars=[_X|T]
612		; N =:= 0 -> Vars = []).
613
614		:- assert_must_succeed(string_term_with_args('Fun(1,2,-)')).
615		:- assert_must_fail(string_term_with_args('Fun(1,2,3)')).
616		:- assert_must_fail(string_term_with_args('Fun(X,_,_Y)')).
617		:- assert_must_fail(string_term_with_args(_Fun)).
618
619		string_term_with_args(StrTerm) :-
620		atom(StrTerm),!,
621		split_atom(StrTerm,['(',',',')'],[_Fun|A]),
622		A\=[],member(-,A).
623
624		:- assert_must_succeed((haskell_csp:concatenate_string_list(['A','B','C'],'ABC'))).
625		:- assert_must_succeed((haskell_csp:concatenate_string_list([],''))).
626
627		concatenate_string_list(L,Res) :-
628		concatenate_string_list(L,'',Res).
629
630		concatenate_string_list([],Res,Res).
631		concatenate_string_list([H|T],Str,Res) :-
632		string_concatenate(Str,H,StrRes),
633		concatenate_string_list(T,StrRes,Res).
634
635		translate_csp_assertions(L,Res) :-
636		maplist(translate_csp_assertion_with_sep,L,LRes),
637		concatenate_string_list(LRes,Res).
638
639		translate_csp_assertion_with_sep(Ass,AssStrWithSep) :-
640		translate_with_sep(translate_csp_assertion,Ass,'$',AssStrWithSep).
641
642		% Sep must be an atom
643		translate_with_sep(TranslationPredicate,Arg,Sep,ArgStrSep) :-
644		functor(Fun,TranslationPredicate,2),arg(1,Fun,Arg),arg(2,Fun,ArgStr),
645		%Fun =.. [TranslationPredicate,Arg,ArgStr],
646		call(Fun),
647		string_concatenate(ArgStr,Sep,ArgStrSep).
648
649		translate_csp_assertion(AssertionExpr,ConcRes) :-
650		/* assert not? P [Op= Q */
651		(AssertionExpr = assertRef(N,P,Op,Q,_) ->
652		refinement_operator(Op,Operator),
653		translate_cspm_state(Q,Proc_2),
654		L=[Operator,Proc_2]
655		/* assert P |= LTL: "ltl-formula" */
656		;AssertionExpr = assertLtl(N,P,Formula,_) ->
657		L = [' |= ', 'LTL: ', '\"', Formula, '\"']
658		/* assert P |= CTL: "ctl-formula" */
659		;AssertionExpr = assertCtl(N,P,Formula,_) ->
660		L = [' |= ', 'CTL: ', '\"', Formula, '\"']
661		/* assert not? P :[Mod [E]] */
662		;AssertionExpr = assertModelCheckExt(N,P,Mod,E) ->
663		fdr_model(Mod,Model),
664		fdr_ext(E,Ext),
665		L=[Model,Ext]
666		/* assert not? P :[Mod] */
667		;AssertionExpr = assertModelCheck(N,P,Mod) ->
668		fdr_single_model(Mod,Model),
669		L=[Model]
670		;
671		add_internal_error('Internal Error (CSP-M Parser): Unexpected assertion predicate: ',
672		translate_csp_assertion(AssertionExpr,ConcRes))
673		),
674		adding_not(N,Not),
675		translate_cspm_state(P,Proc),
676		concatenate_string_list([Not, Proc|L], ConcRes).
677
678		%%%%%%%%%%%%%%%%%%%%%%%%%%% Testing get_csp_processes/1, get_csp_process/2 and translate_csp_assertions/2 predicates %%%%%%%%%%%%%%%%%%%%%%%%%%%%
679		find_and_assert_all_csp_processes_from_arity_zero :-
680		findall(P,(bindval(P,Body,_),definite_cspm_process_expression(Body),assertz(is_csp_process(P))),_L).
681
682		clear_all_is_csp_process_facts :- retractall(is_csp_process(_)).
683
684		:- assert_must_succeed((find_and_assert_all_csp_processes_from_arity_zero,
685		get_csp_processes(Res), %print(Res),nl,
686		clear_all_is_csp_process_facts,
687		Res==list(['P(-)','Q(-)','SEND','REC','SYSTEM','GEN1','GEN2','MAIN']))).
688		:- assert_must_succeed((findall(assertRef(A,B,C,D,S),
689		haskell_csp: assertRef(A,B,C,D,S),L),haskell_csp: translate_csp_assertions(L,String),
690		String == 'CSP: MAIN [T= CSP: PROB_TEST_TRACE$not CSP: PROB_TEST_TRACE [T= CSP: MAIN$')).
691		:- assert_must_succeed((findall(assertModelCheckExt(A,B,C,D),
692		haskell_csp: assertModelCheckExt(A,B,C,D),L),
693		findall(assertModelCheck(A,B,C),haskell_csp:assertModelCheck(A,B,C),L1,L),
694		haskell_csp: translate_csp_assertions(L1,String),
695		String == 'CSP: a.1->P :[ livelock free ]$CSP: SYSTEM [|{|left,right|}|] GEN1 :[ deterministic [F] ]$not CSP: SYSTEM [|{|left,right|}|] GEN1 :[ deadlock free [FD] ]$')).
696
697		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
698
699		/* Tcl_Tk cannot handle complicated prolog strings, that's why we have to convert the from the Csp prolog file filtered assertions
700		into simple string. Assertions will be separated with the '$' symbol. */
701		get_csp_assertions_as_string(CSPFile,R) :-
702		read_compiled_prolog_file(CSPFile,A,filter_assertion_declarations),
703		translate_csp_assertions(A,R),debug_print(9,'string_for_tcl: '),debug_println(9,R).
704
705		/* The same as above for the processes, these will be separate by '$' as well. Needed for the process comboboxes in the
706		'Check Csp Assertions' window in Tcl_Tk. */
707		get_csp_processes(list(R1)) :-
708		debug_nl(9), debug_println(9,getting_csp_processes),
709		findall(bindval(P,_,_),bindval(P,_,_),L),
710		findall(agent(F,Body,_),agent(F,Body,_),L1,L),
711		get_processes(L1,R1),
712		debug_println(9,R1), debug_nl(9).
713
714		get_processes([],[]).
715		get_processes([bindval(A,_,_)|T],R) :- !,
716	?	( animatable_process(A) -> R=[A|Res] ; R=Res),
717		get_processes(T,Res).
718		get_processes([agent(Fun,Body,_)|T],R) :- !,
719	?	( (definite_cspm_process_expression(Body),animatable_process_with_arguments(Fun,proc(F,N)))
720		-> proc_with_arguments_to_string(F,N,FunRes),R = [FunRes|Res]
721		; R=Res
722		),
723		get_processes(T,Res).
724
725		/* ------------------------------------------------------------------------------------------------------------------------- */
726
727		clear_cspm_spec :- % nl,print('RESET CSPM'),nl,nl,
728		retractall(parseResult(_,_,_,_,_)),
729		retractall(channel(_,_)),
730		retractall(bindval(_,_,_)),
731		retractall(cspTransparent(_)),
732		retractall(agent(_,_,_)),
733		retractall(dataTypeDef(_,_)),
734		retractall(subTypeDef(_,_)),
735		retractall(nameType(_,_)),
736		retractall(assertRef(_,_,_,_,_)),
737		% retractall(assertTauTrio(_,_,_,_,_,_)),
738		retractall(assertModelCheckExt(_,_,_,_)),
739		retractall(assertModelCheck(_,_,_)),
740		retractall(channel_type_list(_,_)),
741		retractall(csp_full_type_constructor(_,_,_)),
742		retractall(pragma(_)),
743		retractall(enum_warning_occured(_,_,_)).
744		%retractall(csp_full_expanded_type(_,_)),
745		%retractall(expanded_setFromTo(_,_,_)).
746
747		%:- use_module(probsrc(eventhandling),[register_event_listener/3]).
748		:- register_event_listener(clear_specification,clear_cspm_spec,
749		'Clearing any CSPM Specification.').
750
751		is_a_datatype(DT,L) :-
752	?	(dataTypeDef(DT,L) ; subTypeDef(DT,L)).
753
754		/* Tests for the is_not_infinite_type/1 predicate (see .pl translation sample on lines 68-106 ) */
755
756		:- assert_must_fail((assertz(csp_full_type_constructor(_,'SubMsg',[dataType('Msg')])),
757		assertz(csp_full_type_constructor(_,'Msg',[dataType('SubMsg')])),
758		haskell_csp:is_not_infinite_type(closure([tuple([receive])])))).
759		:- assert_must_succeed((assertz(csp_full_type_constructor(_,'FRUIT',
760		[constructor(apples),construcor(oranges),constructor(pears)])),
761		haskell_csp:is_not_infinite_type(closure([tuple([left])])))).
762		:- assert_must_fail((assertz(csp_full_type_constructor(_,'FRUIT',
763		[constructor(apples),construcor(oranges),constructor(pears)])),
764		assertz(csp_full_type_constructor(_,'SubMsg',[dataType('Msg')])),
765		assertz(csp_full_type_constructor(_,'Msg',[dataType('SubMsg')])),
766		haskell_csp:is_not_infinite_type(closure([tuple([left]),
767		tuple([mid]),tuple([right]),tuple([receive])])))).
768		:- assert_must_fail((assertz(csp_full_type_constructor(ste,'Inf',['Seq'(dataType('FRUIT'))])),
769		assertz(csp_full_type_constructor(_,'FRUIT',
770		[constructor(apples),construcor(oranges),constructor(pears)])),
771		haskell_csp:is_not_infinite_type(closure([tuple([infinite])])))).
772		:- assert_must_succeed((assertz(csp_full_type_constructor(_,'FRUIT',
773		[constructor(apples),construcor(oranges),constructor(pears)])),
774		haskell_csp:is_not_infinite_type(closure([tuple([left]),tuple([mid]),tuple([right])])))).
775		:- assert_must_fail((assertz(csp_full_type_constructor(_,'FRUIT',
776		[constructor(apples),construcor(oranges),constructor(pears)])),
777		assertz(csp_full_type_constructor(_,'SubMsg',[dataType('Msg')])),
778		assertz(csp_full_type_constructor(_,'Msg',[dataType('SubMsg')])),
779		assertz(csp_full_type_constructor(ste,'Inf',['Seq'(dataType('FRUIT'))])),
780		haskell_csp:is_not_infinite_type(closure([tuple([left]),tuple([mid]),
781		tuple([right]),tuple([infinite]),tuple([receive])])))).
782
783		:- assert_must_fail(haskell_csp:is_not_infinite_type(setFrom(1))).
784		:- assert_must_fail(haskell_csp:channel_type_is_finite('dotTupleType'([setValue([int(1),int(2)]), setFrom(1)]),2)).
785		:- assert_must_succeed((assertz(name_type('S', setFromTo(1,3))), haskell_csp: channel_type_is_finite('S',2))).
786
787		/* is_not_infinite_type/1 */
788		/* check if the Event set is from infinite type */
789		/* needed for the refinement checker, when generating counter-examples, TODO: re-implement predicate */
790		is_not_infinite_type(X) :- var(X),!,fail.
791		% at first we are only interesting of checking the whole closure for infinite types
792		is_not_infinite_type(closure(X)) :- !,
793		closure_is_finite_set(X).
794		%% TODO: Cover all other cases for this predicate (like setValue, setFrom, ...)
795
796
797		closure_is_finite_set(L) :-
798		maplist(single_element_closure_is_finite,L).
799
800		% the closure is basically the set of all channels in a specification
801		single_element_closure_is_finite(tuple([Ch|_List])) :-
802		(channel_type_list(Ch,ChannelTypeList) -> true
803		; print(no_channel_type(Ch))),
804		!,
805		l_channel_type_is_finite(ChannelTypeList,2).
806		single_element_closure_is_finite(_X).
807
808		channel_type_is_finite(intType,_Rec) :- !,fail.
809		channel_type_is_finite(boolType,_Rec) :- !.
810		channel_type_is_finite(setFromTo(_L,_U),_Rec) :- !.
811		channel_type_is_finite(setFrom(_L),_Rec) :- !,fail. % endless set
812		% we got a dot tuple of types, we need to check for infinity all types in the tuple.
813		channel_type_is_finite('dotTupleType'(List),Rec):-!,
814		l_channel_type_is_finite(List,Rec).
815		channel_type_is_finite('typeTuple'(List),Rec) :- !,
816		l_channel_type_is_finite(List,Rec). % the same as last clausel
817		channel_type_is_finite(setValue(_L),_Rec) :- !.
818		channel_type_is_finite(dataType(DT),Rec) :-
819	?	is_a_datatype(DT,_),!,
820		check_datatype_el(DT,Rec).
821		channel_type_is_finite('Seq'(setValue([])),_Rec) :- !. % Seq({}) is the empty sequence <>
822		channel_type_is_finite('Seq'(_Type),_Rec) :- !, fail. % e.g. Seq({a,b,c}) indicator for endless datatype (there are endless numbers of sequences)
823		channel_type_is_finite(X,Rec) :-
824		name_type(X,Type),!,
825		channel_type_is_finite(Type,Rec).
826		channel_type_is_finite(_X,_Rec).
827
828		check_datatype_el(DT,MaxRec) :-
829		(MaxRec > 0 -> M1 is MaxRec -1,
830	?	(csp_constructor(_Cons,DT,ArgSubTypes) -> /* Subtypes recursion. */ l_channel_type_is_finite(ArgSubTypes,M1)
831		; /* constructors from finite type (there is no recursion)*/ true)).
832		/* ending recursion of datatypes (recursion doesn't mean infinite type) */
833
834		channel_type_is_finite_rec(Rec,HType) :-
835		channel_type_is_finite(HType,Rec).
836
837		l_channel_type_is_finite(L,Rec) :-
838		maplist(channel_type_is_finite_rec(Rec),L).
839
840		/*
841		l_channel_type_is_finite([],_Rec).
842		l_channel_type_is_finite([HType|T],Rec) :-
843		(channel_type_is_finite(HType,Rec) ->
844		l_channel_type_is_finite(T,Rec)).
845		*/
846
847		/* end of the implementation of is_not_infinite_type/1 predicate */
848
849		get_csp_assertions(CSP_Assertions) :-
850		findall(Ass, (is_assertion(Ass),Ass), CSP_Assertions),
851		debug_println(9,CSP_Assertions).
852
853		/*
854		get_csp_assertions_enum(CSPFile, Result) :-
855		read_compiled_prolog_file(CSPFile,CSP_Assertions,filter_assertion_declarations),
856		enumerate_assertions(CSP_Assertions,Result).
857
858		:- assert_must_succeed(haskell_csp:enumerate_assertions([a,b,c,d,e,f],[(a,0),(b,1),(c,2),(d,3),(e,4),(f,5)])).
859		:- assert_must_succeed(haskell_csp:enumerate_assertions([],[])).
860		enumerate_assertions(L,R) :- enumerate_assertions_acc(L,R,0).
861		enumerate_assertions_acc([],[],_).
862		enumerate_assertions_acc([H|T],[(H,Acc)|R],Acc) :- New_Acc is Acc +1, enumerate_assertions_acc(T,R,New_Acc).
863		*/
864
865		cia_consult_without_redefine_warning(File) :-
866		(file_exists(File) -> true ; (add_error(haskell_csp,'CSP-M PL File does not exist: ',File),fail)),
867		debug_println(15,consult_without_redefine(File)),
868		get_set_optional_prolog_flag(redefine_warnings, Old, off),
869		get_set_optional_prolog_flag(single_var_warnings, Old2, off),
870		get_set_optional_prolog_flag(discontiguous_warnings, Old3, off),
871		(load_files(File,[compilation_mode(assert_all)]) %consult(File)
872		-> OK=true ; OK=false),
873		get_set_optional_prolog_flag(redefine_warnings, _, Old),
874		get_set_optional_prolog_flag(single_var_warnings, _, Old2),
875		get_set_optional_prolog_flag(discontiguous_warnings, _, Old3),
876		OK=true.
877
878		/* ------------------------------------- */
879
880
881		/* THE CSP OPERATIONAL SEMANTICS */
882
883
884		/* ------------------------------------- */
885		%
886		%trans_pre_compute(X,Results) :-
887		% findall(res(X,A,X1,Residue),call_residue(cspm_trans(X,A,X1),Residue), Results).
888		%
889		%
890		%trans_cont(Results,X,A,X1) :-
891		% member(res(X,A,X1,Residue),Results),
892		% % print(trans_cont(X,A,X1,Residue)),nl,
893		% call(Residue).
894
895		/* ------------------------------------- */
896
897		%cspm_trans(E,_,_) :- print(cspm_trans(E)),nl,fail.
898
899		:- assert_must_succeed(( haskell_csp:functor_dif(X,f), X=g(_) )).
900		:- assert_must_fail(( haskell_csp:functor_dif(X,f), X=f(_) )).
901
902		:- block functor_dif(-,?).
903		functor_dif(X,FY) :- functor(X,FX,_), FX\=FY.
904
905		:- assert_pre(haskell_csp:cspm_trans(E,_,_,_), nonvar(E)).
906		:- assert_post(haskell_csp:cspm_trans(_,A,NE,_), (nonvar(A),nonvar(NE))).
907		:- block cspm_trans(-,?,?,?).
908		% TO DO: comment out for efficiency:
909		/* ------ */
910		%cspm_trans(X,_,_) :- debug_println(9,cspm_trans(X)), var(X),
911		% add_error(csp_interpreter,'### Variable process expression in cspm_trans !!',X), fail.
912		cspm_trans(X,_,_,_) :- undefined_process_construct(X),
913		(get_preference(cspm_animate_all_processes,true),string_term_with_args(X) ->
914		add_message(cspm_trans,'Warning: Tried to expand a process with non-ground arguments: ',X),fail
915		;add_error_fail(csp_interpreter,'### Undefined Construct in cspm_trans !! ',X)
916		).
917		/* ------ */
918
919		cspm_trans(stop(_),_,_,_) :- fail.
920		cspm_trans(omega,_,_,_) :- fail.
921
922		cspm_trans(skip(SrcSpan),tick(SrcSpan),omega,_).
923		%cspm_trans(skip(SrcSpan),tick(SrcSpan),stop(SrcSpan),_).
924
925		%cspm_trans(cspPrint(X),io(V1,print,no_loc_info_available),cspPrint(X)) :- evaluate_argument(X,V1).
926
927		cspm_trans('CHAOS'(SrcSpan,_Set),tau(chaos_stop(SrcSpan)),stop(SrcSpan),_).
928		cspm_trans('CHAOS'(SrcSpan,Set),io(V1,Ch,SrcSpan),'CHAOS'(SrcSpan,Set),_WF) :- /* or should we add an intermediate tau ?? */
929		% print(evaluate_argument(Set,S)),nl,
930		evaluate_argument(Set,S),
931		% print(chaos(S)),nl,
932		expand_channel_pattern_expression(S,ECList,SrcSpan),
933		% print(setup_channel_skeleton(io(V1,Ch,SrcSpan))),nl,
934	?	setup_channel_skeleton(io(V1,Ch,SrcSpan)),
935		% print(chaos(io(V1,Ch),ECList)),nl,
936		hidden(io(V1,Ch,SrcSpan),ECList).
937
938		% print(hidden(io(V1,Ch,SrcSpan),ECList)),nl.
939
940		/* external choice */
941	?	cspm_trans('[]'(X,Y,Span),NA,Res,WF) :- cspm_trans(X,A,X1,WF),
942		shift_span_for_left_branch(Span,LSpan),
943	?	merge_span_into_event(A,LSpan,NA),
944		( top_level_dif(A,tau(_)), Res=X1
945		;
946		A=tau(_), tl_normalise('[]'(X1,Y,Span),Res) ).
947	?	cspm_trans('[]'(X,Y,Span),NA,Res,WF) :- cspm_trans(Y,A,Y1,WF),
948		shift_span_for_right_branch(Span,RSpan),
949	?	merge_span_into_event(A,RSpan,NA),
950		( top_level_dif(A,tau(_)), Res=Y1
951		;
952		A=tau(_), tl_normalise('[]'(X,Y1,Span),Res) ).
953
954		/* internal choice */
955		cspm_trans('|~|'(X,_Y,SrcSpan),tau(int_choice_left(SrcSpan,LSpan)),X,_WF) :-
956		shift_span_for_left_branch(SrcSpan,LSpan).
957		cspm_trans('|~|'(_X,Y,SrcSpan),tau(int_choice_right(SrcSpan,RSpan)),Y,_WF) :-
958		shift_span_for_right_branch(SrcSpan,RSpan).
959
960		/* -> PREFIX */
961		/* Note: set restrictions on values are encoded as inGuard Expressions */
962		cspm_trans(prefix(SPAN1,Values,ChannelExpr,CSP,SPAN2), io(EV,Channel,SPAN), NormCSP,WF) :-
963	?	evaluate_channel_outputs(Values,ChannelExpr,EV,Channel,SPAN,WF),
964		unify_spans(SPAN1,SPAN2,SPAN),
965	?	full_normalise_csp_process(CSP,NormCSP). % ,print(prefix(io(EV,Channel))),nl.
966
967
968		/* interleave */
969		%cspm_trans('|||'(X,Y,Span),A,R,WF) :- cspm_trans(sharing(setValue([]),X,Y),A,R).
970		/* Firing rules for the |||-operator:
971
972		P -a> P'
973		----------------------------
974		P ||| Q -a> P' ||| Q
975
976		Q -a> Q'
977		----------------------------
978		P ||| Q -a> P ||| Q'
979
980
981		P -tick> P'
982		----------------------------
983		P ||| Q -tau> Omega ||| Q
984
985
986		Q -tick> Q'
987		----------------------------
988		P ||| Q -tau> P ||| Omega
989
990		*/
991
992		cspm_trans('|||'(omega,omega,Span),tick(Span),omega,_).
993		cspm_trans('|||'(X,Y,ISpan),A,Res,WF) :-
994	?	cspm_trans(X, ActionX, X1,WF),
995		shift_span_for_left_branch(ISpan,LSpan),
996		( ActionX=tick(_), X2=omega
997		; functor_dif(ActionX,tick), X2=X1
998		),
999		merge_span_into_event(ActionX,LSpan,MA),
1000		(ActionX=tick(_) -> A=tau(MA); A=MA),
1001	?	tl_normalise('|||'(X2,Y,ISpan),Res).
1002		cspm_trans('|||'(X,Y,ISpan),A,Res,WF) :-
1003	?	cspm_trans(Y, ActionY, Y1,WF),
1004		shift_span_for_right_branch(ISpan,RSpan),
1005		( ActionY=tick(_), Y2=omega
1006		; functor_dif(ActionY,tick), Y2=Y1
1007		),
1008		merge_span_into_event(ActionY,RSpan,MA),
1009		(ActionY=tick(_) -> A=tau(MA); A=MA),
1010	?	tl_normalise('|||'(X,Y2,ISpan),Res).
1011
1012		/* sequential composition */
1013		cspm_trans(';'(P,Q,SeqSpan),AX,Res,WF) :-
1014	?	cspm_trans(P,A,P1,WF),
1015		( A=tick(_),
1016		merge_span_into_event(A,SeqSpan,MA),
1017		AX = tau(MA),
1018	?	full_normalise_csp_process(Q,Res) /* is this required ?? */
1019		; functor_dif(A,tick), AX=A,
1020		tl_normalise(';'(P1,Q,SeqSpan),Res)
1021		).
1022
1023
1024		/* Sharing: [| a |] */
1025		cspm_trans(sharing(CList,X,Y,SrcSpan),A,Res,WF) :-
1026		evaluate_argument(CList,EvCList),
1027		expand_channel_pattern_expression(EvCList,ECList,SrcSpan),
1028	?	cspm_trans(esharing(ECList,X,Y,SrcSpan),A,Res,WF).
1029		cspm_trans(esharing(_,omega,omega,SrcSpan), tick(SrcSpan), omega ,_WF).
1030		cspm_trans(esharing(CList,X,Y,SrcSpan), Action, Result,WF) :-
1031	?	cspm_trans(X, ActionX, X1,WF),
1032		( (ActionX=tick(TS),
1033		shift_span_for_left_branch(SrcSpan,LSpan),
1034		merge_span_into_event(tau(tick(TS)),LSpan,Action),
1035		Result = esharing(CList,omega,Y,SrcSpan))
1036		; (functor_dif(ActionX,tick),
1037		shift_span_for_left_branch(SrcSpan,LSpan),
1038		merge_span_into_event(ActionX,LSpan,Action),
1039		not_hidden(ActionX,CList), /* covers tau */
1040		Result = esharing(CList,X1,Y,SrcSpan))
1041		; (ActionX=io(V1,Ch,Sp1), Action = io(V,Ch,Span),
1042		%((transferReq,[int(3),ac1,ac2,true])=(Ch,V1) -> trace ; true),
1043		Result = esharing(CList,X1,Y1,SrcSpan),
1044		unify_spans(Sp1,SrcSpan,SP1b),
1045		hidden(Action,CList),
1046		unify_values(V1,V2,V,Ch,SP1b), % try and also incorporate Sp2 Span, without compromising speed
1047		% print(call_cspm_transY_B1(Y,io(V2,Ch),Y1)),nl,
1048	?	cspm_trans(Y, io(V2,Ch,Sp2), Y1,WF), /* <---- Y will be recomputed for every solution of X !!! */
1049		unify_spans(SP1b,Sp2,Span3),
1050		Span = span_info(sharing,Span3)
1051		)
1052		).
1053		cspm_trans(esharing(CList,X,Y,SrcSpan), Action2, Result,WF) :-
1054		shift_span_for_right_branch(SrcSpan,RSpan),
1055		% print(esharing_call_cspm_transY_B2(Y,ActionY,Y1)),nl,
1056	?	cspm_trans(Y,ActionY,Y1,WF), /* this gets computed a second time; is there a way to avoid this? */
1057		%print(esharing_cspm_transY_B2(Y,ActionY)),nl,
1058		( ActionY = tick(TS), Action=tau(tick(TS)), Result=esharing(CList,X,omega,SrcSpan)
1059		; functor_dif(ActionY,tick), ActionY = Action,
1060		%print(try_non_sharing(ActionY)),nl,
1061		not_hidden(ActionY,CList), /* covers tau */
1062		Result = esharing(CList,X,Y1,SrcSpan)
1063		),
1064		merge_span_into_event(Action,RSpan,Action2).
1065
1066
1067		/* Linked Parallel [ l <-> r,.. ] */
1068		cspm_trans(lParallel(LinkList,X,Y,Span), Action,Result,WF) :-
1069		evaluate_link_list(LinkList,EvLinkRenameList),
1070		%print(evlinklist(LinkList,EvLinkRenameList)),nl, %
1071	?	cspm_trans(elinkParallel(EvLinkRenameList,X,Y,Span),Action,Result,WF).
1072		cspm_trans(elinkParallel(_,omega,omega,Span), tick(Span), omega ,_WF).
1073		cspm_trans(elinkParallel(EvLinkRenameList,X,Y,LinkSpan),Action,Result,WF) :-
1074	?	cspm_trans(X,AX,X2,WF), % print(elink_x(X,AX,X2,EvLinkRenameList)),nl, print('State: '),print(X),nl,
1075		( AX = tick(TS),
1076		shift_span_for_left_branch(LinkSpan,LSpan),
1077		merge_span_into_event(tau(tick(TS)),LSpan,Action),
1078		Result=elinkParallel(EvLinkRenameList,omega,Y,LinkSpan)
1079		;
1080		functor_dif(AX,tick),
1081		( shift_span_for_left_branch(LinkSpan,LSpan),
1082		merge_span_into_event(AX,LSpan,Action),
1083		Result = elinkParallel(EvLinkRenameList,X2,Y,LinkSpan),
1084	?	not_renamed(AX,EvLinkRenameList)
1085		% ,print(not_renamed(AX,EvLinkRenameList)),nl %%
1086		;
1087		Action=tau(link(AX,io(V,Ch,Span))),
1088		Result = elinkParallel(EvLinkRenameList,X2,Y2,LinkSpan),
1089	?	force_rename_action(AX,EvLinkRenameList,io(V1,Ch,Sp0)),
1090		unify_spans(LinkSpan,Sp0,Sp1),
1091		%% print(renamed(AX,io(V1,Ch),EvLinkRenameList)),nl, %%
1092		unify_values(V1,V2,V,Ch,Sp1), % try and also incorporate Sp2 Span, without compromising speed
1093		% MAYBE TO DO ?: instantiate V2 as much as possible ! --> in()/dot issues
1094		%% print(cspm_trans(Y,io(V2,Ch,Sp2),Y2)),nl, %%
1095	?	cspm_trans(Y,io(V2,Ch,Sp2),Y2,WF), /* <---- Y will be recomputed for every solution of X !!! */
1096		unify_spans(Sp1,Sp2,Span3),
1097		%% print(unify(Sp1,Sp2,Span3)),nl, %%
1098		Span = span_info(sharing,Span3)
1099		)
1100		).
1101		cspm_trans(elinkParallel(EvLinkRenameList,X,Y,LinkSpan),Action2,
1102		elinkParallel(EvLinkRenameList,X,YR,LinkSpan),WF) :-
1103		shift_span_for_right_branch(LinkSpan,RSpan),
1104		rev_rename_list(EvLinkRenameList,RevList),
1105	?	cspm_trans(Y,ActionY,Y2,WF), /* TO DO: try and avoid recomputation of cspm_trans(Y) ?! */
1106		( ActionY=tick(TS), Action=tau(tick(TS)), YR=omega
1107		;
1108	?	functor_dif(ActionY,tick),ActionY=Action,YR=Y2,not_renamed(Action,RevList)
1109		),
1110		merge_span_into_event(Action,RSpan,Action2).
1111
1112		cspm_trans(aParallel(CListX,X,CListY,Y,SrcSpan),A,NewState,WF) :- %print(expanding_aparx),nl,
1113		evaluate_argument(CListX,EvCListX),
1114		expand_channel_pattern_expression(EvCListX,ECListX,SrcSpan), %print(expanding_apary),nl,
1115	?	evaluate_argument(CListY,EvCListY),
1116		expand_channel_pattern_expression(EvCListY,ECListY,SrcSpan),
1117		Expanded = eaParallel(ECListX,X,ECListY,Y,SrcSpan),
1118		%we have expanded the channel synchronisation sets; avoid recomputing them every time
1119		% TO DO: investigate whether it also makes sense to precompute intersection
1120	?	cspm_trans(Expanded,A,NewState,WF).
1121		cspm_trans(eaParallel(_,omega,_,omega,SrcSpan), tick(SrcSpan), omega ,_WF).
1122		cspm_trans(eaParallel(ECListX,X,ECListY,Y,SrcSpan),A,eaParallel(ECListX,X2,ECListY,Y1,SrcSpan),WF) :-
1123		%trans_pre_compute(Y,Results),
1124	?	cspm_trans(X, AX, X1,WF),
1125		% print(apar_x(AX, from(X))),nl,
1126		( X2=X1,Y1=Y,
1127		hidden_or_tau(AX,ECListX),
1128		not_hidden(AX,ECListY),
1129		shift_span_for_left_branch(SrcSpan,LSpan),
1130		merge_span_into_event(AX,LSpan,A)
1131		;
1132		AX=tick(_TS), X2=omega,Y1=Y,
1133		shift_span_for_left_branch(SrcSpan,LSpan),
1134		merge_span_into_event(tau(AX),LSpan,A)
1135		;
1136		AX=io(V1,Ch,Sp1), X2=X1, A = io(V,Ch,Span),
1137		% nl,print(try_apar_sync(V1,Ch)),nl,
1138		hidden(io(V1,Ch,Sp1),ECListX), % print(left_ok),nl, % do V1 instead of V ?
1139		hidden(io(V,Ch,Span),ECListY), % print(right_ok),nl, % V2 instead of V
1140		% Synchronisation possible
1141		unify_spans(Sp1,SrcSpan,SP1b),
1142		unify_values(V1,V2,V,Ch,SP1b), % try and also incorporate Sp2 Span, without compromising speed
1143		%print(trying(aparY(io(V2,Ch,Sp2)))),nl, %
1144	?	cspm_trans(Y, io(V2,Ch,Sp2), Y1,WF), /* <---- Y will be recomputed for every solution of X !!! */
1145		% trans_cont(Results,Y, io(V2,Ch,Sp2), Y1),
1146		% print(done(aparY(io(V2,Ch,Sp2)))),nl, %
1147		unify_spans(SP1b,Sp2,Span3),
1148		Span = span_info(sharing,Span3)
1149		).
1150		cspm_trans(eaParallel(ECListX,X,ECListY,Y,SrcSpan),AS,eaParallel(ECListX,X,ECListY,Y2,SrcSpan),WF) :-
1151	?	cspm_trans(Y, AY, Y1,WF), /* To do: try and avoid recomputation of cspm_trans(Y) ?! */
1152		( AY=A, Y2=Y1,
1153		hidden_or_tau(A,ECListY), not_hidden(A,ECListX)
1154		;
1155		AY=tick(_TS), A = tau(AY), Y2=omega
1156		),
1157		shift_span_for_right_branch(SrcSpan,RSpan),
1158		merge_span_into_event(A,RSpan,AS).
1159
1160		/* only used for outside xtl_interface ; not used internally anymore */
1161	?	cspm_trans(val_of(X,Span),A,NewExpr,WF) :- (symbol(RenamedX,X,_,_) -> cspm_trans(agent_call(Span,RenamedX,[]),A,NewExpr,WF);
1162		cspm_trans(X,A,NewExpr,WF)).
1163		cspm_trans(agent_call(Span,F,Par),NA,NNewExpr,WF) :-
1164	?	unfold_function_call_once(F,Par,Value,Span),
1165	?	cspm_trans(Value,A,NewExpr,WF),
1166	?	full_normalise_csp_process(NewExpr,NNewExpr),
1167		% print(merge_agcall(A,Span)),nl,
1168	?	merge_span_into_event(A,Span,NA).
1169
1170		% Par = [[x],[y]]
1171		cspm_trans(agent_call_curry(F,Par),NA,NNewExpr,WF) :-
1172		Span=no_loc_info_available,
1173		unfold_function_call_curry_once(F,Par,Value,Span),
1174		cspm_trans(Value,A,NewExpr,WF),
1175		full_normalise_csp_process(NewExpr,NNewExpr),
1176		% print(merge_agcall(A,Span)),nl,
1177		merge_span_into_event(A,Span,NA).
1178
1179		cspm_trans(builtin_call(X),Action,NewExpr,WF) :- % builtin_call is normally removed by precompilation; but can remain, e.g., for assertions
1180		cspm_trans(X,Action,NewExpr,WF).
1181		cspm_trans(head(X),Action,NewExpr,WF) :- force_evaluate_argument(X,EX),head_list(EX,Result),
1182	?	cspm_trans(Result,Action,NewExpr,WF).
1183
1184		/* hiding '\\' */
1185
1186		cspm_trans('\\'(Expr,CList,Span), A, Res ,WF) :-
1187	?	evaluate_argument(CList,EvCList),
1188		expand_channel_pattern_expression(EvCList,ECList,no_loc_info_available),
1189		% print(ehide(Expr,ECList,Span)),nl,
1190	?	cspm_trans(ehide(Expr,ECList,Span),A,Res,WF).
1191
1192		cspm_trans(ehide(Expr,CList,Span), A, Res ,WF) :-
1193		% (nonvar(A) -> ((A=io(_,_,_);A=tick(_)) -> ActionX=A ; A=tau(hide(ActionX)))
1194		% ; true),
1195	?	cspm_trans(Expr,ActionX,X,WF),
1196	?	cspm_hide_action(ActionX,X, CList,Span, A,Res).
1197
1198
1199		cspm_trans(exception(CList,X,Y,Span), A, Res ,WF) :-
1200		evaluate_argument(CList,EvCList),
1201		expand_channel_pattern_expression(EvCList,ECList,no_loc_info_available),
1202		%print(exception(ECList,X,Y)),nl,
1203	?	cspm_trans(eexception(ECList,X,Y,Span),A,Res,WF).
1204
1205		cspm_trans(eexception(CList,X,Y,Span),A,Res,WF) :- % expanded version of exception
1206	?	cspm_trans(X, ActionX, X1,WF),
1207		( functor_dif(ActionX,tick), ActionX=A,
1208		Res = eexception(CList,X1,Y,Span),
1209		not_hidden(A,CList)
1210		; merge_span_into_event(ActionX,Span,A),
1211		Res = Y,
1212		hidden(ActionX,CList)
1213		; A=tick(TS), ActionX=tick(TS), Res=omega % is this correct ??
1214		).
1215
1216
1217		/* timeout */
1218	?	cspm_trans('[>'(P,Q,SrcSpan),AS,Res,WF) :- cspm_trans(P,A,P1,WF),
1219		( A=tau(_), Res='[>'(P1,Q,SrcSpan)
1220		;
1221		top_level_dif(A,tau(_)), % a transition which can be removed by the tau below
1222		Res=P1 ),
1223		shift_span_for_left_branch(SrcSpan,LSpan),
1224		merge_span_into_event(A,LSpan,AS).
1225		cspm_trans('[>'(_P,Q,SrcSpan),tau(timeout(SrcSpan)),Q,_WF).
1226
1227
1228		/* interrupt */
1229
1230		cspm_trans('/\\'(X,Y,Span),NA,Res,WF) :-
1231	?	cspm_trans(X,A,X1,WF), %%print(interrupt_left(X,A,X1)),nl,
1232		shift_span_for_left_branch(Span,LSpan),
1233		merge_span_into_event(A,LSpan,NA),
1234		( A=tick(_), Res=X1
1235		; functor_dif(A,tick), tl_normalise('/\\'(X1,Y,Span),Res)
1236		).
1237		cspm_trans('/\\'(X,Y,Span),NA,Res,WF) :-
1238	?	cspm_trans(Y,A,Y1,WF),
1239		shift_span_for_right_branch(Span,RSpan),
1240		merge_span_into_event(A,RSpan,NA),
1241		( top_level_dif(A,tau(_)), Res=Y1
1242		; A=tau(_), tl_normalise('/\\'(X,Y1,Span),Res)
1243		).
1244
1245		/* renaming [[ old <- new,... | Generators ]] */
1246		cspm_trans(procRenamingComp(X,GeneratorList,RenameList),RA,Res,WF) :-
1247		% print(procCompRenaming(GeneratorList)),nl, %%
1248		% warning: does not have the rangeEnum wrapper expected
1249		expand_set_comprehension(rangeEnum(RenameList),GeneratorList,setValue(ExpandedRenames)),
1250		%print(exp(ExpandedRenames)),nl,
1251	?	cspm_trans(procRenaming(ExpandedRenames,X,no_loc_info_available),RA,Res,WF).
1252
1253		/* renaming [[ old <- new,... ]] */
1254		cspm_trans(procRenaming(RenameList,X,Span),RA,Res,WF) :- %print(procRename(RenameList)),nl,
1255		evaluate_rename_list(RenameList,ERenameList),
1256	?	cspm_trans(eprocRenaming(ERenameList,X,Span),RA,Res,WF).
1257		cspm_trans(eprocRenaming(RenameList,X,Span),RAS,Res,WF) :-
1258		%print('RENAME: '), translate:print_cspm_state(X),nl,
1259	?	cspm_trans(X,A,X2,WF),
1260		tl_normalise(eprocRenaming(RenameList,X2,Span),Res),
1261		%print(try_rename(A,RenameList,RA,Span)),nl, %%
1262		% it's still possible that A is non-ground term, i.e. there are a non-ground variables (c?x?y) in the sub-process,
1263		% which have to be unified before applying renaming on them.
1264	?	(ground(A) -> true; enumerate_action(A)),
1265	?	rename_action(A,RenameList,RA),
1266		%%% print(done_rename_action(A,RenameList,RA)),nl,
1267		merge_span_into_event(RA,Span,RAS).
1268		% print(merge_span(RA,Span,RAS)),nl,
1269
1270		/* if then else */
1271		cspm_trans(ifte(Test,Then,Else,S1,S2,S3),A,X1,WF) :-
1272		%nl,print(checking_if_test(Test,Then,Else)),nl,
1273	?	evaluate_boolean_expression(Test,Res),
1274		% print(if_evaluated_boolean_expression(Test,Res)),nl,nl,
1275	?	cspm_if_trans(Res,Then,Else,A,X1,S1,S2,S3,WF).
1276
1277		cspm_trans('&'(Test,Then),A,X1,WF) :- S=no_loc_info_available,
1278	?	cspm_trans(ifte(Test,Then,stop(S),S,S,S),A,X1,WF).
1279
1280
1281		cspm_trans(repChoice(GeneratorList,Body,Span), Action,X1,WF) :-
1282		%% nl,print(repChoice(GeneratorList,Body)),nl,
1283		replicate_expand_set_comprehension([Body],GeneratorList,setValue(Bodies)),
1284		%% print(bodies(Bodies)),nl,
1285		convert_into_choice(Bodies,Span,CHOICE),
1286		%% print(choice(CHOICE)),nl,
1287	?	cspm_trans(CHOICE,Action,X1,WF).
1288
1289		cspm_trans(repInternalChoice(GeneratorList,Body,Span), tau(rep_int_choice(Span)),Res,_WF) :-
1290		% print(repInternalChoice(GeneratorList,Span)),nl,
1291		replicate_expand_set_comprehension([Body],GeneratorList,Bodies),
1292		% print(bodies(Bodies)),nl,nl,
1293		(is_empty_set(Bodies,true)
1294		-> add_error(cspm_trans,'Empty set for replicated internal choice: ',Bodies,Span),fail
1295	?	; is_member_set(Res,Bodies)).
1296
1297		cspm_trans(repInterleave(GeneratorList,Body,Span), A, X,WF) :-
1298		%% tools:print_bt_message(repInterleave(GeneratorList)), %%
1299		% multiplicity is relevant for |||, so add variables to Body below in case Variables are not used
1300		extract_variables_from_generator_list(GeneratorList,Variables),
1301		replicate_expand_set_comprehension([na_tuple([Body|Variables])],GeneratorList,setValue(Bodies)),
1302		convert_into_interleave(Bodies,Span,INTLV),
1303		%% tools:print_bt_message(intlv(INTLV)), %%
1304	?	cspm_trans(INTLV,A,X,WF). %, tools:print_bt_message(sol(A,X)).
1305
1306
1307		cspm_trans(repSequence(GeneratorList,Body,Span),A,X,WF) :-
1308		% print(repSequence(GeneratorList)),nl, %%
1309		expand_listcomprehension(rangeEnum([Body]),GeneratorList,list(Bodies)),
1310		% print(bodies(Bodies)),nl, %%
1311		convert_into_seqcomp(Bodies,Span,SEQ), %print(sequential(SEQ)),nl,
1312	?	cspm_trans(SEQ,A,X,WF).
1313
1314
1315		cspm_trans(procRepAParallel(GeneratorList,pair(SyncSet,Body),Span), A, X,WF) :-
1316		% multiplicity is relevant for sharing (it makes a difference if 1 or 2 copies are present), so add variables to Body below in case Variables are not used
1317		extract_variables_from_generator_list(GeneratorList,Variables),
1318		replicate_expand_set_comprehension([list([SyncSet,Body,Variables])],GeneratorList,setValue(Bodies)),
1319	?	convert_into_eaParallel(Bodies,Span,APAR,_ALPH),
1320	?	cspm_trans(APAR,A,X,WF).
1321
1322
1323		cspm_trans(procRepLinkParallel(SyncSet,GeneratorList,Body,Span), A, X,WF) :-
1324		expand_listcomprehension(rangeEnum([Body]),GeneratorList,list(Bodies)),
1325		convert_into_linkParallel(Bodies,SyncSet,Span,APAR,Body),
1326		%when((ground(APAR)),
1327	?	cspm_trans(APAR,A,X,WF).
1328
1329		cspm_trans(procRepSharing(SyncSet,GeneratorList,Body,Span), A, X,WF) :-
1330		% print(procRepSharing(GeneratorList)),nl,
1331		% multiplicity is relevant for sharing, so add variables to Body below in case Variables are not used
1332		extract_variables_from_generator_list(GeneratorList,Variables),
1333		replicate_expand_set_comprehension([na_tuple([Body|Variables])],GeneratorList,setValue(Bodies)),
1334		% print(bodies(Bodies)),nl,
1335		convert_into_Sharing(Bodies,SyncSet,Span,APAR), %print(repshare(APAR)),nl,
1336	?	cspm_trans(APAR,A,X,WF).
1337
1338		% ----------
1339
1340		cspm_hide_action(ActionX,X, CList,Span, ActionAfterHiding,ResultingCSPExpr) :-
1341		( functor_dif(ActionX,tick), ActionX=ActionAfterHiding,
1342		tl_normalise(ehide(X,CList,Span),ResultingCSPExpr),
1343		not_hidden(ActionAfterHiding,CList)
1344		; merge_span_into_event(ActionX,Span,NActionX),
1345		ActionAfterHiding=tau(hide(NActionX)),
1346		tl_normalise(ehide(X,CList,Span),ResultingCSPExpr),
1347		hidden(ActionX,CList)
1348		; ActionAfterHiding=tick(TS), ActionX=tick(TS), ResultingCSPExpr=omega
1349		).
1350
1351		:- block cspm_if_trans(-,?,?,?, ?,?,?,?,?).
1352		cspm_if_trans(true,Then,_Else,AS,X1,_S1,S2,_S3,WF) :- !, %print(ifte_true(Then)),nl,
1353		full_normalise_csp_process(Then,NThen),
1354	?	cspm_trans(NThen,A,X1,WF),
1355		merge_span_into_event(A,S2,AS).
1356		cspm_if_trans(false,_Then,Else,AS,X1,_S1,_S2,S3,WF) :- !, %print(ifte_false(Else)),nl,
1357	?	full_normalise_csp_process(Else,NElse), cspm_trans(NElse,A,X1,WF),
1358		merge_span_into_event(A,S3,AS).
1359		cspm_if_trans(Other,Then,Else,AS,X1,S1,S2,S3,WF) :-
1360		add_internal_error('Internal Error: Not a boolean value inside if-then-else: ',
1361		cspm_if_trans(Other,Then,Else,AS,X1,S1,S2,S3,WF)),
1362		fail.
1363
1364		:- block convert_into_interleave(-,-,?).
1365		convert_into_interleave([],Span,skip(Span)).
1366		convert_into_interleave([na_tuple([H|_])|T],Span,R) :- convert_into_interleave3(T,H,Span,R).
1367		:- block convert_into_interleave3(-,?,?,?).
1368		convert_into_interleave3([],X,_Span,X).
1369		convert_into_interleave3([na_tuple([H2|_])|T],H1,Span,'|||'(H1,Rest,Span)) :-
1370		convert_into_interleave3(T,H2,Span,Rest).
1371
1372
1373		:- block convert_into_choice(-,-,?).
1374		convert_into_choice([],Span,stop(Span)).
1375		convert_into_choice([H|T],Span,R) :- convert_into_choice3(T,H,Span,R).
1376		:- block convert_into_choice3(-,?,?,?).
1377		convert_into_choice3([],X,_Span,X).
1378		convert_into_choice3([H2|T],H1,Span,'[]'(H1,Rest,Span)) :- convert_into_choice3(T,H2,Span,Rest).
1379
1380		:- block convert_into_seqcomp(-,-,?).
1381		convert_into_seqcomp(Bodies,Span,Res) :- convert_into_seqcomp2(Bodies,Span,Res).
1382		convert_into_seqcomp2([],Span,skip(Span)) :- print(convert_into_seqcomp2([],Span,skip(Span))),nl.
1383		convert_into_seqcomp2([H|T],Span,R) :- convert_into_seqcomp3(T,H,Span,R).
1384		:- block convert_into_seqcomp3(-,?,?,?).
1385		convert_into_seqcomp3([],X,_Span,X).
1386		convert_into_seqcomp3([H2|T],H1,Span,';'(H1,Rest,Span)) :-
1387		convert_into_seqcomp2([H2|T],Span,Rest).
1388
1389
1390		:- block convert_into_eaParallel(-,-,?,?).
1391		convert_into_eaParallel([],Span,skip(Span),setValue([])).
1392		convert_into_eaParallel([H|T],Span,APAR,ALPH) :-
1393	?	when(nonvar(T),convert_into_eaParallel3([H|T],Span,APAR,ALPH)).
1394	?	convert_into_eaParallel3([list([Sync,X,_])],_Span,X,ESync) :- !, evaluate_argument(Sync,ESync).
1395		convert_into_eaParallel3([list([CListX,X,_]),L2|T], Span,AlphPar, Alphabet ) :-
1396	?	when(nonvar(T),(convert_into_eaParallel3([L2|T],Span, Rest,RestAlphabet),
1397		evaluate_argument(CListX,ECListX),
1398		evaluate_argument(union(RestAlphabet,ECListX),Alphabet),
1399		/* put more complicated process onto the left: better efficiency for cspm_trans */
1400		% TO DO: we could think about splitting the list in two
1401		AlphPar = aParallel(RestAlphabet,Rest,ECListX,X,Span))). % only aParallel
1402
1403
1404
1405		:- block convert_into_Sharing(-,?,-,?).
1406		convert_into_Sharing([],_,Span,skip(Span)).
1407		convert_into_Sharing([na_tuple([H|_])|T],SyncSet,Span,R) :- convert_into_Sharing3([H|T],SyncSet,Span,R).
1408		:- block convert_into_Sharing3(-,?,?,?).
1409		convert_into_Sharing3([X],_Sync,_Span,Res) :- !, Res=X.
1410		convert_into_Sharing3([X|T],CListX,Span,sharing(CListX,Rest,X,Span) ) :-
1411		/* put more complicated process onto the left: better efficiency for cspm_trans */
1412		convert_into_Sharing(T,CListX,Span,Rest).
1413
1414		:- block convert_into_linkParallel(-,?,?,?,?).
1415		convert_into_linkParallel([],_,Span,skip(Span),Body) :-
1416		add_error(haskell_csp,'Empty Set in Replicated Linked Parallel: ',Body,Span).
1417		convert_into_linkParallel([H|T],SyncSet,Span,APAR,Body) :-
1418		convert_into_linkParallel3([H|T],SyncSet,Span,APAR,Body).
1419		:- block convert_into_linkParallel3(-,?,?,?,?).
1420		convert_into_linkParallel3([X],_Sync,_Span,Res,_) :- !, Res=X.
1421		convert_into_linkParallel3([X|T],CListX,Span,lParallel(CListX,X,Rest,Span),Body ) :-
1422		/* in contrast to convert_into_Sharing3: we cannot put more complicated process onto the left: order matters for linked parallel */
1423		convert_into_linkParallel(T,CListX,Span,Rest,Body).
1424
1425		/* ------------------------------------- */
1426
1427		/* top_level_normalise */
1428		/* Just check the top-level of the csp expression to see if it can
1429		be simplified/normalised */
1430		tl_normalise('[]'(X,Y,Span),R) :- !, %print(tl(X)),nl,print(t2(Y)),nl,nl,
1431		(X=Y -> R=X
1432		; is_stop(X,_) -> R=Y
1433		; is_stop(Y,_) -> R=X
1434		; Y='[]'(X,Y2,_) -> tl_normalise('[]'(X,Y2,Span),R) % X [] X [] Y == X [] Y ; relevant e.g. for ASTD library example
1435		; Y='[]'(Y2,X,_) -> tl_normalise('[]'(X,Y2,Span),R)
1436		; X='[]'(Y,X2,_) -> tl_normalise('[]'(Y,X2,Span),R)
1437		; X='[]'(X2,Y,_) -> tl_normalise('[]'(Y,X2,Span),R)
1438		; R='[]'(X,Y,Span)
1439		). /* TO DO: also sort X,Y !? */
1440		tl_normalise('|||'(X,Y,Span),R) :- !,
1441		(is_stop(X,S),is_stop(Y,_)
1442		-> R=stop(S)
1443		; ((X==omega;is_skip(X)) -> R=Y /* law 6.16 on page 142 of Roscoe's book */
1444		; ((Y==omega;is_skip(Y)) -> R=X /* same law, for RHS */
1445		; % this leads to performance loss: tl_normalise should only do top-level normalisation full_normalise_csp_process(X,XR), full_normalise_csp_process(Y,YR),
1446		((preference(cspm_detailed_animation,true);X @=<Y)
1447		-> R='|||'(X,Y,Span)
1448		; R='|||'(Y,X,Span)) %% Warning: this can invalidate left-right Span information
1449		)
1450		)
1451		). % we could replace skip|||P by P
1452		% (X==stop -> R=Y ; (Y==stop -> R=X ; R='|||'(X,Y))). P ||| stop not equal to stop (because of omega)
1453		tl_normalise(ehide(X,CList,Span),R) :- !,
1454		(is_stop(X,S) -> R=stop(S) % Concealement law L4
1455		; is_skip(X,S) -> R=skip(S) % Concealement law L5
1456		; CList == [] -> R=X % Concealement law L1
1457		; try_tl_normalise(X,NX),R=ehide(NX,CList,Span)).
1458		tl_normalise(eprocRenaming(RL,X,Span),R) :- !,
1459		(is_stop(X,S) -> R=stop(S)
1460		; is_skip(X,S) -> R=skip(S)
1461		; try_tl_normalise(X,NX),R=eprocRenaming(RL,NX,Span)).
1462		tl_normalise(';'(X,Y,SPAN),R) :- !,
1463		(is_skip(X) -> R=Y /* Law on page 140 of Roscoe */
1464		; is_stop(X,S) -> R=stop(S)
1465		; is_skip(Y) -> R=X
1466		; R = ';'(X,Y,SPAN) ).
1467		tl_normalise('/\\'(X,Y,Span),R) :- !,
1468		(is_stop(X,_) -> R=Y ; (is_stop(Y,_) -> R=X ; R='/\\'(X,Y,Span))).
1469		tl_normalise(ifte(A,B,C,_,_,_),R) :- !, % print(norm_ifte(A)),nl,
1470		evaluate_boolean_expression(A,ARes),
1471		% print(res(ARes)),nl,
1472		tl_normalise_ifte(ARes,B,C,R).
1473
1474		is_stop(X,S) :- nonvar(X),X=stop(S).
1475
1476		:- block tl_normalise_ifte(-,?,?,?).
1477		tl_normalise_ifte(true,B,_C,R) :- !,full_normalise_csp_process(B,R).
1478	?	tl_normalise_ifte(false,_,C,R) :- !, full_normalise_csp_process(C,R).
1479		% evaluate_boolean_expression/2 will always throw an exception if A is not a boolean test
1480		% probably this case will never occur
1481		% tl_normalise_ifte(A,B,C,_R) :- add_error(tl_normalise,'Not a boolean test: ',A:B:C).
1482
1483		try_tl_normalise(A,R) :- (tl_normalise(A,B) -> R=B ; R=A).
1484
1485		is_skip(X) :- nonvar(X), X=skip(_).
1486		is_skip(X,Y) :- nonvar(X), X=skip(Y).
1487		% TO DO: add rules esharing(_,stop(S),stop(_),_) -> stop(S),
1488
1489		% P [] STOP = P
1490		:- assert_must_succeed((
1491		P='[]'(skip(_),stop(span1),span2),
1492		haskell_csp: full_normalise_csp_process(P,NormP),
1493		NormP=skip(_))).
1494		% P [] P = P
1495		:- assert_must_succeed((
1496		P='[]'(skip(span1),skip(span1),span3),
1497		haskell_csp: full_normalise_csp_process(P,NormP),
1498		NormP=skip(span1))).
1499		% P ||| STOP = STOP
1500		:- assert_must_succeed((
1501		P='|||'(skip(_),stop(span1),span2),
1502		haskell_csp: full_normalise_csp_process(P,NormP),
1503		NormP=stop(span1))).
1504		% SKIP; (P [] STOP) = P
1505		:- assert_must_succeed((
1506		P=';'(skip(_),'[]'(skip(span1),stop(span3),span4),span2),
1507		haskell_csp: full_normalise_csp_process(P,NormP),
1508		NormP='[]'(skip(span1),stop(span3),span4))).
1509		% P; SKIP = P
1510		:- assert_must_succeed((
1511		P=';'(stop(_),skip(span1),span2),
1512		haskell_csp: full_normalise_csp_process(P,NormP),
1513		NormP=stop(_))).
1514
1515		/* ------------------------------------- */
1516		%full_normalise_csp_process(P,_) :- print(full_normalise_csp_process(P)),nl,fail.
1517		/* TO DO: add other procRep,... intermediate operators */
1518	?	full_normalise_csp_process(P,NormP) :- full_normalise_csp_process(P,NormP,outer).
1519		:- block full_normalise_csp_process(-,?,?).
1520		full_normalise_csp_process('|||'(X,Y,Span),Res,_) :- !,
1521		%full_normalise_csp_process(X,NX,inner), full_normalise_csp_process(Y,NY,inner),
1522	?	full_normalise_csp_process(X,NX,outer), full_normalise_csp_process(Y,NY,outer),
1523		tl_normalise('|||'(NX,NY,Span),Res).
1524		% both clausels below will be probably never executed. procRenamingComp/3 and procRepAParallel/3 as
1525		% replicated process expressions will be translated to agent_calls in the compiling/analyzing stage
1526		% of loading the respective CSP model. DEAD CODE:
1527		/*full_normalise_csp_process(procRenamingComp(X,GeneratorList,RenameList),Res,_) :- !,
1528		%print(normalise_procCompRenaming(GeneratorList)),nl,
1529		replicate_expand_set_comprehension(RenameList,GeneratorList,setValue(ExpandedRenames)),
1530		%print(exp(ExpandedRenames)),nl,
1531		Res = procRenaming(ExpandedRenames,X,no_loc_info_available).
1532		full_normalise_csp_process(procRepAParallel(GeneratorList,pair(SyncSet,Body),Span), Res,_) :- !,
1533		%print(procRepAParallel(GeneratorList,SyncSet)),nl,
1534		extract_variables_from_generator_list(GeneratorList,Variables),
1535		replicate_expand_set_comprehension([list([SyncSet,Body,Variables])],GeneratorList,setValue(Bodies)),
1536		%print(bodies(Bodies)),nl,
1537		convert_into_eaParallel(Bodies,Span,APAR,_ALPH), %print(apar(APAR,_ALPH)),nl,
1538		full_normalise_csp_process(APAR,Res,inner). */
1539		full_normalise_csp_process(repInterleave(GeneratorList,Body,Span),Res,_) :- !,
1540		extract_variables_from_generator_list(GeneratorList,Variables),
1541		replicate_expand_set_comprehension([na_tuple([Body|Variables])],GeneratorList,setValue(Bodies)),
1542		convert_into_interleave(Bodies,Span,Res).
1543		full_normalise_csp_process(sharing(CList,X,Y,SrcSpan),Res,_) :- !,
1544		evaluate_argument(CList,EvCList),
1545		expand_channel_pattern_expression(EvCList,ECList,SrcSpan),
1546	?	full_normalise_csp_process(X,NX,outer),
1547	?	full_normalise_csp_process(Y,NY,outer),
1548		Res = esharing(ECList,NX,NY,SrcSpan).
1549		full_normalise_csp_process(aParallel(CListX,X,CListY,Y,SrcSpan),Res,_) :- !,
1550	?	evaluate_argument(CListX,EvCListX),
1551		expand_channel_pattern_expression(EvCListX,ECListX,SrcSpan),
1552	?	evaluate_argument(CListY,EvCListY),
1553		expand_channel_pattern_expression(EvCListY,ECListY,SrcSpan),
1554	?	full_normalise_csp_process(X,NX,outer),
1555	?	full_normalise_csp_process(Y,NY,outer),
1556		%print(eaParallel(ECListX,NX,ECListY,NY,SrcSpan)),nl,
1557		Res = eaParallel(ECListX,NX,ECListY,NY,SrcSpan).
1558		/* Unfold if Par ground and unfolded value ground ?? */
1559		full_normalise_csp_process(agent_call(Span,F,Par),Res,outer) :- % only allow outer agent_calls to be unfolded to avoid infinite expansion for e.g. P(1) = P(1) ||| P(1)
1560		preference(cspm_detailed_animation,false),
1561		%% fail, %% fail: agent_calls are not expanded here, which means better source location feedback in animator
1562		%% WE COULD MAKE THIS AN OPTION IN THE PREFERENCES; I am not sure what the performance impact is
1563		%% for scheduler this leads to a substantial increase in the number of states
1564		!,
1565	?	((ground(Par),unfold_function_call_once(F,Par,Value,Span),
1566		(ground(Value) ;
1567		agent_can_be_unfolded(Value)
1568		)
1569		)
1570	?	-> full_normalise_csp_process(Value,Res,outer)
1571		; Res = agent_call(Span,F,Par)
1572		).
1573		full_normalise_csp_process(val_of(RenamedX,Span),NormState,_) :- !,
1574		(symbol(RenamedX,_X,_,_) ->
1575	?	full_normalise_csp_process(agent_call(Span,RenamedX,[]),NormState,_)
1576		;
1577		% does this occur in some case (see coverage info)
1578		full_normalise_csp_process(RenamedX,NormState,_)
1579		).
1580		full_normalise_csp_process(ifte(Test,Then,Else,S1,S2,S3),R,_) :-
1581		ground(Test),!,
1582		evaluate_boolean_expression(Test,Res),
1583		(Res == true ->
1584	?	full_normalise_csp_process(Then,R)
1585		; Res == false ->
1586	?	full_normalise_csp_process(Else,R)
1587		;
1588		add_internal_error('Internal Error: Not a boolean value inside if-then-else: ',
1589		full_normalise_csp_process(ifte(Test,Then,Else,S1,S2,S3),R,_)),fail
1590		).
1591		full_normalise_csp_process(ifte(Test,Then,Else,S1,S2,S3),R,_) :- !,
1592		R = ifte(Test,Then,Else,S1,S2,S3). % test could be false or true; top-level test could be evaluated ?!
1593		full_normalise_csp_process('&'(Test,Then),R,_) :- !, R = '&'(Test,Then). % test could be false; don't unfold agent_calls inside Then
1594		full_normalise_csp_process(';'(P,Q,SPAN),R,Scope) :- !,
1595	?	full_normalise_csp_process(P,NP,Scope),
1596		tl_normalise(';'(NP,Q,SPAN),R).
1597		full_normalise_csp_process(prefix(SPAN,Values,ChannelExpr,CSP,SPAN2),R,_) :- !,
1598		(empty_inGuard_set(Values) ->
1599		R=stop(SPAN) % (STOP-step) ?x:{} -> P = STOP (law 1.15)
1600		;
1601		R = prefix(SPAN,Values,ChannelExpr,CSP,SPAN2)
1602		).
1603		full_normalise_csp_process(head(List),R,_) :- !, R=head(List). % should we evaluate ??
1604		full_normalise_csp_process(agent_call(Span,A,Par),R,_) :- !, R=agent_call(Span,A,Par).
1605		% DEAD CODE!!! agent_call_curry/2 will be translated into nested agent_call in the precompiling phase.
1606		%full_normalise_csp_process(agent_call_curry(A,Par),R,_) :- !, print(agent_call_curry(A,Par)),nl,R=agent_call_curry(A,Par).
1607		full_normalise_csp_process(ehide(X,CList,Span),R,_) :- !,
1608	?	full_normalise_csp_process(X,NX,inner),
1609		tl_normalise(ehide(NX,CList,Span),R).
1610		full_normalise_csp_process(eprocRenaming(RL,X,Span),R,_) :- !,
1611	?	full_normalise_csp_process(X,NX,inner),
1612		tl_normalise(eprocRenaming(RL,NX,Span),R).
1613		full_normalise_csp_process(Proc,Res,_) :-
1614		binary_top_level_process_operator_possible_to_be_normalised(Proc,F,X,Y,Span),!,
1615	?	full_normalise_csp_process(X,NX,inner),
1616	?	full_normalise_csp_process(Y,NY,inner),
1617		functor(NTerm,F,3),arg(1,NTerm,NX),arg(2,NTerm,NY),arg(3,NTerm,Span),
1618		tl_normalise(NTerm,Res).
1619	?	full_normalise_csp_process(Proc,Res,_) :- definite_cspm_process_construct(Proc,Spans,Rest,RecCSP), !,
1620		functor(Proc,F,N), functor(Res,F,N),
1621	?	maplist(full_normalise_csp_process_inner(inner),RecCSP,NormRecCSP),
1622	?	definite_cspm_process_construct(Res,Spans,Rest,NormRecCSP).
1623		full_normalise_csp_process(P,R,_) :- !,
1624		add_warning(full_normalise_csp_process,'Could not normalise: ',P),R=P.
1625
1626		full_normalise_csp_process_inner(ProcLabel,Proc,NProc) :-
1627	?	full_normalise_csp_process(Proc,NProc,ProcLabel).
1628
1629		binary_top_level_process_operator_possible_to_be_normalised(ProcessTerm,F,X,Y,Span) :-
1630		functor(ProcessTerm,F,3),
1631		memberchk(F,['|||','[]','/\\']),
1632		arg(1,ProcessTerm,X),arg(2,ProcessTerm,Y),arg(3,ProcessTerm,Span).
1633
1634		empty_inGuard_set(Values) :-
1635		member(inGuard(_X,Set),Values),
1636		is_empty_set(Set,true),!.
1637
1638		normalise_cspm_state(State,NormState) :-
1639	?	full_normalise_csp_process(State,NormState).
1640
1641		%% Probably DEAD CODE !!! (wait for the next coverage release to prove this assumption)
1642		:- assert_must_succeed((agent_can_be_unfolded(X), X=procRenamingComp(_,_,_))).
1643		:- assert_must_succeed((agent_can_be_unfolded(X), X=aParallel(_,_,_,_,_))).
1644		agent_can_be_unfolded(procRenamingComp(_,_,_)).
1645		agent_can_be_unfolded(aParallel(_,_,_,_,_)).
1646		agent_can_be_unfolded(repInterleave(_,_,_)).
1647
1648		/* ------------------------------------- */
1649
1650
1651		/* EVALUATING Agent Call arguments */
1652
1653		evaluate_agent_call_parameters(AgentName,Par,_,_) :- var(AgentName),!,
1654		add_internal_error('Internal Error: Trying to call VARIABLE function: ',evaluate_agent_call_parameters(AgentName,Par,_,_)),fail.
1655		evaluate_agent_call_parameters(AgentName,Par,_,_) :- var(Par),!,
1656		add_internal_error('Internal Error: Trying to call VARIABLE parameters: ',evaluate_agent_call_parameters(AgentName,Par,_,_)),fail.
1657		%evaluate_agent_call_parameters(agent_call(AName,[]),Par,EAgentCall) :- atomic(AName),!,
1658		% /* then AName must represent a lambda function which has been compiled ?!!? */
1659		% l_evaluate_arguments(Par,EPar),
1660		% EAgentCall =.. [AName|EPar].
1661		evaluate_agent_call_parameters(_Call,Par,EPar,_) :- Par==[],!, EPar=[]. % nothing to evaluate
1662		evaluate_agent_call_parameters(AgentNameExpr,Par,_EAgentCall,Span) :- \+ atomic(AgentNameExpr),!,
1663		add_error(haskell_csp,'Trying to call non-atomic function: ',agent_call(AgentNameExpr,Par),Span),fail.
1664		evaluate_agent_call_parameters(AName,Par,EPar,Span) :-
1665		length(Par,Arity),
1666		(agent_parameters(AName,Arity,LazyStrictList)
1667		-> true
1668		; add_error(evaluate_agent_call_parameters,'Unknown function call: ',(AName/Arity),Span)
1669		),
1670	?	l_evaluate_arguments(Par,LazyStrictList,EPar).
1671		% EAgentCall =.. [AName|EPar].
1672
1673
1674		l_evaluate_arguments([],[],[]).
1675		l_evaluate_arguments([A|T],[Lazy|TL],[EA|ET]) :-
1676		%% print(eval_arg(A,Lazy)),nl, %%
1677	?	(Lazy=lazy -> evaluate_argument(A,EA)
1678	?	; force_evaluate_argument(A,EA)
1679		),
1680		%% print(arg_res(A,EA)),nl, %%
1681	?	l_evaluate_arguments(T,TL,ET).
1682
1683
1684		evaluate_lambda_arguments([],[],[]).
1685		evaluate_lambda_arguments([A|T],[FormalPar|FT],[EA|ET]) :-
1686		%% print(eval_arg(A,Lazy)),nl,
1687		(var(FormalPar) -> A=EA % will be copied into lambda body and evaluated then evaluate_argument(A,EA)
1688		; force_evaluate_argument(A,EA) % it is a pattern; we need to evaluate argument
1689		),
1690		%% print(arg_res(A,EA)),nl,
1691		evaluate_lambda_arguments(T,FT,ET).
1692		/* ------------------------------------- */
1693
1694		/* EVALUATING Channel arguments */
1695
1696		setup_skel(_,in(_)).
1697
1698		setup_channel_skeleton(io(V,Ch,_)) :-
1699	?	channel_type_list(Ch,ChannelTypes),
1700		maplist(setup_skel,ChannelTypes,V).
1701
1702		/* ------------------------------------- */
1703
1704		/* enumerate_action(A) : if part of the inputs of A are not determined: enumerate
1705		possible values */
1706
1707		cspm_trans_enum(E,A,E2) :-
1708		init_wait_flags(WF),
1709	?	cspm_trans(E,A,E2,WF),
1710		% tools:print_bt_message(grounding_waitflags(A)), %%
1711	?	ground_wait_flags(WF),
1712		% TO DO: we could also add enumerate_action to the WF store: in principle sets inGuards should be smaller
1713		% tools:print_bt_message(enumerate_action(E,A)), %%
1714	?	enumerate_action(A)
1715		% ,tools:print_bt_message(finished_enumerate_action(A)),nl %%
1716		.
1717
1718
1719		/* TO DO: add enumeration to hide + removed values by rename; use tau(V,Ch) ?? */
1720
1721		enumerate_action(X) :- X \= tick(_), X\=tau(_), X\= io(_,_,_), !,
1722		add_internal_error('Internal error: Unknown CSP event: ', enumerate_action(X)).
1723		enumerate_action(tick(_)).
1724	?	enumerate_action(tau(X)) :- (nonvar(X) -> enumerate_tau_argument(X) ; true).
1725		enumerate_action(io(Vals,Channel,Span)) :-
1726		if((channel_type_list(Channel,ChannelTypes)),
1727	?	(enume_ch_vals(ChannelTypes,Vals,Channel,Span,io(Vals,Channel,Span))),
1728		add_error(enumerate_action,'Channel not declared: ',Channel,Span)).
1729
1730		enumerate_tau_argument(io(V,C,S)) :- !,enumerate_action(io(V,C,S)).
1731	?	enumerate_tau_argument(hide(X)) :- !,enumerate_action(X).
1732		enumerate_tau_argument(link(_AX,AY)) :- !,enumerate_action(AY).
1733		enumerate_tau_argument(_).
1734
1735		:- use_module(probsrc(translate),[translate_event/2]).
1736		%% enume_ch_vals(T,V,C,_Span,FullEvent) :- print(enume_ch_vals(T,V,C)),nl,fail. %%
1737		enume_ch_vals([],[],_,_Span,_) :- !.
1738		enume_ch_vals([],Vals,_Channel,Span,FullEvent) :- !,
1739		(Vals = [in(V)]
1740		-> empty_tuple(V) /* the empty dotTuple */
1741		; translate_event(FullEvent,ES),
1742		add_error(enumerate_action,'Too many output values on channel: ',ES:Vals, Span)
1743		).
1744		enume_ch_vals([Type|RestTypes],Vals,Channel,Span,FullEvent) :- % T \= [],
1745	?	enume_ch_vals2(Vals,Type,RestTypes,Channel,Span,FullEvent).
1746
1747		enume_ch_vals2(X,Type,_RestTypes,_Channel,Span,FullEvent) :- % print(ecv2(X,Type,RestTypes,Channel)),nl,
1748		var(X),!,
1749		translate_event(FullEvent,ES),
1750		add_error(haskell_csp,'Variable value list on channel: ',ES:X:Type,Span),fail.
1751		enume_ch_vals2([],Type,RestTypes,_Channel,Span,FullEvent) :- !,
1752		translate_event(FullEvent,ES),
1753		add_error(enumerate_action,'Too few output values on channel: ',ES:[Type:RestTypes], Span).
1754		enume_ch_vals2([in(V)|TAIL],Type,RestTypes,Channel,Span,FullEvent) :- nonvar(V),
1755		V=tuple(X),nonvar(X),X=[H|T], \+ csp_constructor(H,_,_),
1756		!, % sometimes an in contains dot tuples; test above not very elegant; can we simplify this ??
1757		(T==[] ->
1758		enume_ch_vals2([in(H)|TAIL],Type,RestTypes,Channel,Span,FullEvent)
1759		; enume_ch_vals2([in(H),in(tuple(T))|TAIL],Type,RestTypes,Channel,Span,FullEvent)).
1760		enume_ch_vals2([in(V)|TAIL],Type,RestTypes,Channel,Span,_FullEvent) :-
1761		TAIL==[],!, /* only treat it as a tail_in(X) if it is definitely at the end of the list
1762		see example LetTestChannel -> TEST(2) process for complication if we do
1763		not check that TAIL==[] */
1764		(RestTypes=[]
1765	?	-> enumerate_channel_input_value(Type,V,Channel,Span)
1766	?	; enumerate_channel_input_value('dotTupleType'([Type|RestTypes]),V,Channel,Span)
1767		).
1768		enume_ch_vals2([IODVal|TV],Type,RestTypes,Channel,Span,FullEvent) :- !,
1769	?	enumerate_channel_value_type(IODVal,Type,Channel,Span),
1770	?	enume_ch_vals(RestTypes,TV,Channel,Span,FullEvent).
1771
1772
1773		enumerate_channel_value_type(IOD,Type,Channel,Span) :-
1774		%print(enumerate_channel_value_type(IOD,Type,Channel,Span)),nl,
1775		(IOD=in(HX) %; IOD=dot(HX))
1776	?	-> enumerate_channel_input_value(Type,HX,Channel,Span)
1777		; (ground(IOD)
1778		-> check_channel_input_output_value(IOD,Type,Channel,Span,'Type error in channel input: ')
1779	?	; enumerate_channel_input_value(Type,IOD,Channel,Span)
1780		)
1781		).
1782
1783		check_channel_input_output_value(X,Type,Ch,Span,ErrMsg) :-
1784		when(ground(X), ((peel_in(X,PX),is_member_set_alsoPat(PX,Type)) -> true
1785		; add_error(check_channel_output_value,ErrMsg,(Ch:(val(X):type(Type))),Span))).
1786
1787		/* peel input values which may lurk inside datavalues, especially records */
1788		peel_in(in(X),R) :- !, R=X.
1789		peel_in(record(F,L),R) :- !,
1790		R=record(F,PL),
1791		maplist(peel_in,L,PL).
1792		peel_in(X,X).
1793
1794		:- assert_must_succeed(( haskell_csp:enumerate_channel_input_value(setFromTo(1,3),R,c,unknown),
1795		R==int(2) )).
1796
1797		enumerate_channel_input_value(Type,Val,Ch,Span) :-
1798		MAXRECURSIONDEPTH = 2,
1799	?	enumerate_channel_input_value(Type,Val,Ch,MAXRECURSIONDEPTH,Span).
1800
1801
1802		enumerate_channel_input_value(Type,Val,Ch,MaxRec,Span) :-
1803		(ground(Val)
1804		-> check_channel_input_output_value(Val,Type,Ch,Span,'Type error in channel output: ')
1805	?	; enumerate_channel_input_value1(Type,Val,Ch,MaxRec,Span)
1806		).
1807
1808		enumerate_channel_input_value1(Type,Val,Ch,MaxRec,Span) :-
1809		((nonvar(Val),Val=in(VX)) /* can happen when question marks occur inside records, ... */
1810	?	-> enumerate_channel_input_value1_1(Type,VX,Ch,MaxRec,Span)
1811	?	; enumerate_channel_input_value1_1(Type,Val,Ch,MaxRec,Span)
1812		).
1813
1814		enumerate_channel_input_value1_1(Type,Val,Ch,MaxRec,Span) :-
1815		( (nonvar(Val),Val=alsoPat(X,Y)) ->
1816	?	enumerate_channel_input_value2(Type,X,Ch,MaxRec,Span),
1817		%enumerate_channel_input_value2(Type,Y,Ch,MaxRec,Span),
1818		unify_also_patterns(X,Y,_R)
1819		; (nonvar(Val),Val=appendPat(X,FunHead)) ->
1820		agent_compiled(FunHead,_Value,_SRCSPAN),
1821	?	enumerate_channel_input_value2(Type,X,Ch,MaxRec,Span)
1822	?	; enumerate_channel_input_value2(Type,Val,Ch,MaxRec,Span)
1823		).
1824
1825		:- dynamic ignore_infinite_datatypes/0. % set from refinement_checker; very HACKY
1826
1827		%enumerate_channel_input_value2(T,V,Ch,_MaxRec) :- print(enumerate_channel_input_value(T,V,Ch)),nl,fail.
1828		:- assert_must_succeed((findall(Res, enumerate_channel_input_value2('Set'(setValue([int(1),int(2)])),Res,_Ch,_MaxRec,_Span),L),
1829		L == [setValue([int(1),int(2)]),setValue([int(1)]),setValue([int(2)]),setValue([])])).
1830
1831		enumerate_channel_input_value2(intType,X,Ch,_MaxRec,_Span) :- !,
1832	?	enumerate_basic_type(X,integer,trigger_true(Ch)). % NOTE : this uses MAXINT preference value!
1833		enumerate_channel_input_value2(boolType,X,_Ch,_MaxRec,_Span) :- !,(X=true ; X=false).
1834		enumerate_channel_input_value2(setFromTo(Low,Up),Res,Ch,_MaxRec,Span) :- !,
1835		set_enumeration_result(Res,int(X),Ch,setFromTo(Low,Up),Span),
1836	?	enumerate_csp_int(X,Low,Up).
1837		/*(preference(use_clpfd_solver,true),clpfd_interface: fd_var(Res) ->
1838		clpfd_interface: csp_clpfd_labeling([ffc,enum],[Res])
1839		; set_enumeration_result(Res,int(X),Ch,setFromTo(Low,Up),Span),
1840		enumerate_csp_int(X,Low,Up)
1841		).*/
1842		enumerate_channel_input_value2(setFrom(Low),V,Ch,_MaxRec,Span) :- !,
1843		add_symbol_span(Ch,Span,CSpan),
1844		add_error(enumerate_channel_input_value,'Cannot enumerate infinite Type: ',(Ch,(setFrom(Low),V)),CSpan).
1845		enumerate_channel_input_value2('Set'(X),Res,_Ch,_MaxRec,_Span) :- !, /* Probably DEAD CODE */
1846	?	enum_subset(X,Res).
1847		enumerate_channel_input_value2('dotTupleType'(List),Res,Ch,MaxRec,Span) :- !,
1848		set_enumeration_tuple_result(Res,RR,Ch,'dotTupleType'(List),Span),
1849	?	l_enumerate_channel_input_value2(List,RR,Ch,dot_tuple,MaxRec,Span).
1850		enumerate_channel_input_value2('typeTuple'(List),Res,Ch,MaxRec,Span) :- !,
1851		set_enumeration_result(Res,na_tuple(RR),Ch,'typeTuple'(List),Span),
1852		% print(enum_tuple('typeTuple'(List),Res,Ch)),nl,
1853	?	l_enumerate_channel_input_value2(List,RR,Ch,type_tuple,MaxRec,Span).
1854	?	enumerate_channel_input_value2(setValue(L),R,_Ch,_MaxRec,_Span) :- !,member(R,L). /* R should be list skeleton at least */
1855	?	enumerate_channel_input_value2(dataType(DT),C,Channel,MaxRec,Span) :- is_a_datatype(DT,_), !,
1856	?	enumerate_datatype_el(DT,C,Channel,MaxRec,Span).
1857		% TO DO: add all other types supported by is_member_set
1858		enumerate_channel_input_value2('Seq'(setValue([])),V,_Ch,_MaxRec,_Span) :- !, V= list([]).
1859		enumerate_channel_input_value2('Seq'(Type),V,Ch,_MaxRec,Span) :- !,
1860		(ignore_infinite_datatypes -> V=sequence % needed for the Trace Debugger in Tcl/Tk
1861		; add_symbol_span(Ch,Span,CSpan),
1862		add_error(enumerate_channel_input_value,'Cannot enumerate infinite Seq Type: ',(Ch,('Seq'(Type),V)),CSpan)).
1863		enumerate_channel_input_value2(agent_call(_Src, Name,Patterns),Val,Ch,_MaxRec,Span) :- !,
1864		unfold_function_call_once(Name,Patterns,Res,Span),
1865		evaluate_argument(Res,Res1),
1866		enumerate_channel_input_value(Res1,Val,Ch,Span).
1867		enumerate_channel_input_value2(Type,V,Ch,_MaxRec,Span) :-
1868		add_symbol_span(Ch,Span,CSpan),
1869		add_error(enumerate_channel_input_value,'Illegal type for channel: ',(Ch,(Type,V)),CSpan).
1870
1871		:- dynamic enum_warning_occured/3.
1872		:- use_module(probsrc(tools_strings),[ajoin/2]).
1873
1874		enumerate_datatype_el(DT,C,Channel,_MaxRec,Span) :-
1875	?	if(csp_constant(C,DT),true,
1876		(nonvar(C),C \= record(_,_),
1877		add_error(enumerate_datatype_el,'Type error for channel input variable: ', Channel:(C,type(DT)),Span),
1878		fail)).
1879		enumerate_datatype_el(DT,C,Channel,MaxRec,Span) :-
1880		((MaxRec>0 ; nonvar(C))
1881		->((nonvar(C) -> M1 = MaxRec ; M1 is MaxRec-1),
1882		C=record(Cons,Fields),
1883	?	csp_constructor(Cons,DT,ArgSubTypes),
1884		% print(recurse_enum_rec(Cons,DT,ArgSubTypes,Fields)),nl,
1885	?	l_enumerate_channel_input_value2(ArgSubTypes,Fields,Channel,dot_tuple,M1,Span))
1886		; enum_warning_occured(DT,Channel,Span) -> fail
1887		; ajoin(['Maximum recursion depth reached on channel "',Channel,
1888		'" for enumeration of datatype : '],Msg),
1889		add_message(csp,Msg,DT,Span),
1890		assertz(enum_warning_occured(DT,Channel,Span)),
1891		% THIS used to return a variable when ignore_infinite_datatypes true, but causes problems for test 2349
1892		fail
1893		).
1894
1895		% ensure that ResVar is a tuple and flatten the tuple
1896		set_enumeration_tuple_result(ResVar,ResultTerm,Channel,ExpectedType,Span) :-
1897		((tuple(TL)=ResVar;dotTuple(TL)=ResVar) ->
1898		%print(flattening(ResVar)),nl,
1899		flatten_tuple_value(TL,ResultTerm) /* ok, no type error */
1900		; add_symbol_span(Channel,Span,CSpan),
1901		add_error(set_enumeration_tuple_result,'Type error for instantiated channel input variable: ',Channel:(ResVar,type(ExpectedType)),CSpan),
1902		fail).
1903
1904		%%%%%%%%%%%%%%%%%%%%% UNIT TESTS FOR flatten_tuple_value/2, flatten_inner_tuple_value/2 and flatten2/3 %%%%%%%%%%%%%%%%%%%%%%%%%%
1905		:- assert_must_succeed((haskell_csp: flatten_tuple_value(X,R), R == X)).
1906		:- assert_must_succeed((haskell_csp: flatten_tuple_value([],R), R == [])).
1907		:- assert_must_succeed((haskell_csp: flatten_tuple_value([X,tuple([int(1),int(2)])],R), R == [X,int(1),int(2)])).
1908		:- assert_must_succeed((haskell_csp: flatten_tuple_value([tuple([]),tuple([int(1),int(2)]),X,Y,tuple([int(10)])],R), R == [int(1),int(2),X,Y,int(10)])).
1909		:- assert_must_succeed((haskell_csp: flatten_tuple_value([X,tuple([int(1),Y,int(2),Z])],R), R == [X,int(1),Y,int(2),Z])).
1910		:- assert_must_succeed((haskell_csp: flatten_tuple_value([X,tuple([int(1),Y,int(2),Z]),int(3)],R), R == [X,int(1),Y,int(2),Z,int(3)])).
1911		:- assert_must_succeed((haskell_csp: flatten_tuple_value([],[]))).
1912		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1913
1914		flatten_tuple_value(X,R) :- var(X),!, R=X. % this can happen if we have a single in(X) representing ch?x
1915		flatten_tuple_value([],[]).
1916		flatten_tuple_value([H|T],R) :- flatten2(H,T,R).
1917
1918		flatten_inner_tuple_value(X,R) :- var(X),!, print(variable_inner_tuple(X)),nl, R=[X].
1919		flatten_inner_tuple_value([],[]).
1920		flatten_inner_tuple_value([H|T],R) :- flatten2(H,T,R).
1921
1922		flatten2(VAR,T,Res) :- var(VAR),!, Res=[VAR|TR],flatten_inner_tuple_value(T,TR).
1923		flatten2(tuple(LH),T,R) :- !, flatten_inner_tuple_value(LH,FLH),
1924		append(FLH,TR,R), flatten_inner_tuple_value(T,TR).
1925		flatten2(H,T,[H|TR]) :- flatten_inner_tuple_value(T,TR).
1926
1927		set_enumeration_result(ResVar,ResultTerm,Channel,ExpectedType,Span) :-
1928		(ResVar=ResultTerm -> true /* ok, no type error */
1929		;
1930		add_symbol_span(Channel,Span,CSpan),
1931		add_error(set_enumeration_result,'Type error for instantiated channel input variable: ',Channel:(val(ResVar),type(ExpectedType)),CSpan),
1932		fail).
1933
1934		l_enumerate_channel_input_value2([],R,Ch,_SType,_MaxRec,Span) :- !,
1935		(var(R) -> R=[]
1936		; R=[] -> true
1937		; add_error(l_enumerate_channel_input_value,'Too many arguments on channel: ',(Ch,R),Span),fail).
1938		l_enumerate_channel_input_value2([HType|T],[HVal|TV],Ch,SType,MaxRec,Span) :- !,
1939		((TV==[],SType=dot_tuple) -> % enume the rest of the channel types to HVal (only for dotTuple types)
1940	?	enume_ch_vals([HType|T],[in(HVal)],Ch,Span,io([],Ch)) % TO DO: full event
1941		;
1942	?	enumerate_channel_input_value(HType,HVal,Ch,MaxRec,Span), %% <-- add Span
1943	?	l_enumerate_channel_input_value2(T,TV,Ch,SType,MaxRec,Span)
1944		).
1945		l_enumerate_channel_input_value2([HType|T],[],Ch,_SType,_MaxRec,Span) :- !,
1946		add_error(l_enumerate_channel_input_value,'Not enough arguments on channel: ',(Ch,[HType|T]),Span),fail.
1947		l_enumerate_channel_input_value2(X,Y,Ch,SType,MR,Span) :-
1948		add_internal_error('Illegal arguments: ',l_enumerate_channel_input_value2(X,Y,Ch,SType,MR,Span)),fail.
1949
1950		get_symbol_span(S,SPAN) :- atomic(S),symbol(S,_,SPAN,_),!.
1951		get_symbol_span(S,SPAN) :- nonvar(S),functor(S,FS,_),symbol(FS,_,SPAN,_),!.
1952		get_symbol_span(_S,no_loc_info_available).
1953
1954
1955		add_symbol_error(Src,Msg,Term,Ch) :-
1956		get_symbol_span(Ch,Span),
1957		add_error(Src,Msg,Term,Span).
1958
1959		add_symbol_span(Ch,Span,OutSpan) :- get_symbol_span(Ch,SSpan),
1960		SSpan \= no_loc_info_available,
1961		!,
1962		unify_spans(Span,SSpan,OutSpan).
1963		add_symbol_span(_,S,S).
1964
1965		% just like above, but can also be called with ordinary spans
1966		add_error_with_span(Src,Msg,Term,Span) :-
1967		(Span=symbol(S) -> get_symbol_span(S,Span2) ; Span2=Span),
1968		add_error(Src,Msg,Term,Span2).
1969
1970		add_internal_error_with_span(Src,Msg,Term,Span) :-
1971		(Span=symbol(S) -> get_symbol_span(S,Span2) ; Span2 = Span),
1972		add_internal_error(Src,Msg,Term,Span2).
1973
1974		/* ------------------------------------- */
1975		/* BOOLEAN EXPRESSIONS */
1976		/* ------------------------------------- */
1977
1978		%%%%%%%% UNIT TESTS FOR TESTING check_boolean_expressions/1,cond_check_boolean_expression/2,ifte_check_boolean_expression/3 %%%%%%%
1979
1980		:- assert_must_succeed((haskell_csp: check_boolean_expression(true))).
1981		:- assert_must_fail((haskell_csp: check_boolean_expression(X), X = false)).
1982		:- assert_must_succeed((haskell_csp: check_boolean_expression(bool_not(false)))).
1983		:- assert_must_fail((haskell_csp: check_boolean_expression(X), X = false)).
1984		:- assert_must_succeed((haskell_csp: check_boolean_expression(bool_or(true,_X)))).
1985		:- assert_must_succeed((haskell_csp: check_boolean_expression(bool_not('<='(int(1),int(0)))))).
1986		:- assert_must_fail((haskell_csp: check_boolean_expression(bool_not('<='(int(1),int(10)))))).
1987		:- assert_must_succeed((haskell_csp: check_boolean_expression(bool_and('<='(int(1),int(10)), true)))).
1988		:- assert_must_fail((haskell_csp: check_boolean_expression(bool_and(false,'<='(int(1),int(10)))))).
1989		:- assert_must_succeed((haskell_csp: check_boolean_expression(bool_or('<='(int(1),int(0)), true)))).
1990		:- assert_must_fail((haskell_csp: check_boolean_expression(bool_or(false,'<='(int(1),int(0)))))).
1991		:- assert_must_succeed((haskell_csp: check_boolean_expression('<='(int(10),int(X))), X = 30)).
1992		:- assert_must_succeed((haskell_csp: check_boolean_expression('>='(int(10),int(X))), X = 3)).
1993		:- assert_must_succeed((haskell_csp: check_boolean_expression('<='(int(10),int(X))), X = 10)).
1994		:- assert_must_succeed((haskell_csp: check_boolean_expression('>='(int(10),int(X))), X = 10)).
1995		:- assert_must_succeed((haskell_csp: check_boolean_expression('<'(int(10),int(X))), X = 30)).
1996		:- assert_must_succeed((haskell_csp: check_boolean_expression('>'(int(10),int(X))), X = 3)).
1997		:- assert_must_fail((haskell_csp: check_boolean_expression('<'(int(10),int(X))), X = 10)).
1998		:- assert_must_fail((haskell_csp: check_boolean_expression('>'(int(10),int(X))), X = 10)).
1999		:- assert_must_succeed((haskell_csp: check_boolean_expression(ifte('<='(int(3),int(20)),'>='(int(2),int(1)),'<='(int(3),int(1)),span,span,span)))).
2000		:- assert_must_succeed((haskell_csp: check_boolean_expression(ifte('<='(int(3),int(2)),'>='(int(2),int(1)),'<='(int(3),int(10)),span,span,span)))).
2001		:- assert_must_succeed((haskell_csp: check_boolean_expression(ifte('<='(int(3),int(2)),'>='(int(2),int(1)),'<='(int(3),int(10)),span,span,span)))).
2002		:- assert_must_succeed((haskell_csp: check_boolean_expression(ifte(X,'>='(int(2),int(1)),'<='(int(3),int(1)),span,span,span)),
2003		X = head(listExp(rangeEnum(['<='(int(2),int(3)),'>'(int(2),int(3))]))))).
2004		:- assert_must_fail((haskell_csp: check_boolean_expression(ifte(X,'>='(int(2),int(1)),'<='(int(3),int(1)),span,span,span)),
2005		X = head(listExp(rangeEnum(['<='(int(2),int(1)),'>'(int(2),int(3))]))))).
2006		:- assert_must_succeed((haskell_csp: check_boolean_expression(head(listExp(rangeEnum(['<'(int(2),int(3)),'>'(int(2),int(3))])))))).
2007		:- assert_must_succeed((haskell_csp: check_boolean_expression(head(listExp(rangeEnum([true,false])))))).
2008		:- assert_must_fail((haskell_csp: check_boolean_expression(head(listExp(rangeEnum([false,false])))))).
2009		:- assert_must_fail((haskell_csp: check_boolean_expression(head(listExp(rangeEnum([false,true])))))).
2010		:- assert_must_fail((haskell_csp: check_boolean_expression((head(listExp(rangeEnum([null(listExp(rangeEnum([false,true])))]))))))).
2011		:- assert_must_fail((haskell_csp: check_boolean_expression((head(listExp(rangeEnum([empty(setValue([int(1),int(2)]))]))))))).
2012		:- assert_must_succeed((haskell_csp: check_boolean_expression(empty(setExp(rangeEnum([])))))).
2013		:- assert_must_succeed((haskell_csp: check_boolean_expression(head(listExp(rangeEnum([bool_not(false)])))))).
2014		:- assert_must_succeed((haskell_csp: check_boolean_expression(head(listExp(rangeEnum([bool_or(true,false)])))))).
2015		:- assert_must_succeed((haskell_csp: check_boolean_expression(head(listExp(rangeEnum(['<='(int(2),int(3)),'>'(int(2),int(3))])))))).
2016		:- assert_must_fail((haskell_csp: check_boolean_expression(head(listExp(rangeEnum(['<='(int(2),int(1)),'>'(int(2),int(3))])))))).
2017		:- assert_must_succeed((haskell_csp: check_boolean_expression(null(listExp(rangeEnum([])))))).
2018		:- assert_must_fail((haskell_csp: check_boolean_expression(null(listExp(rangeEnum([int(1),int(2),int(3)])))))).
2019		:- assert_must_succeed((haskell_csp: check_boolean_expression(empty(setExp(rangeEnum([])))))).
2020		:- assert_must_fail((haskell_csp: check_boolean_expression(empty(setExp(rangeEnum([int(1),int(2),int(3)])))))).
2021		:- assert_must_succeed((haskell_csp: is_boolean_expression(true), haskell_csp: is_boolean_expression(false))).
2022
2023		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2024
2025		:- block check_boolean_expression(-).
2026
2027		%check_boolean_expression(E) :- %print(check_boolean_expression(E)),nl,
2028		% var(E),add_error(check_boolean_expression,'Variable boolean expression:',E),fail.
2029		check_boolean_expression(true) :- !.
2030		check_boolean_expression(false) :- !, fail.
2031		check_boolean_expression(bool_not(BExpr1)) :- !,
2032		evaluate_boolean_expression(BExpr1,false). /* provide custom check_not_... predicate ?? */
2033		check_boolean_expression(bool_and(BExpr1,BExpr2)) :- !,
2034		check_boolean_expression(BExpr1),
2035	?	check_boolean_expression(BExpr2).
2036		check_boolean_expression(bool_or(BExpr1,BExpr2)) :- !,
2037		evaluate_boolean_expression(BExpr1,R1),
2038		cond_check_boolean_expression(R1,BExpr2).
2039		check_boolean_expression(ifte(Test,Then,Else,_,_,_)) :- !,
2040		evaluate_boolean_expression(Test,TestRes), %print(check_bool_ifte(Test,TestRes)),nl,
2041		ifte_check_boolean_expression(TestRes,Then,Else).
2042		check_boolean_expression(head(X)) :- !, force_evaluate_argument(X,EX),head_list(EX,HResult),
2043		check_boolean_expression(HResult).
2044		check_boolean_expression(null(Arg1)) :- !, force_evaluate_argument(Arg1,EX), is_null_list(EX,true).
2045		check_boolean_expression(empty(Arg1)) :- !, force_evaluate_argument(Arg1,EX), is_empty_set(EX,true).
2046		check_boolean_expression(agent_call(Span,F,Par)) :- !, /* in this context we need the result of the function call */
2047		unfold_function_call_once(F,Par,Body,Span),
2048		%when(nonvar(Body),
2049		check_boolean_expression(Body).
2050		check_boolean_expression('member'(Arg1,Arg2)) :- !, % after bool_binary_op: there is a special rule for member there
2051		force_evaluate_argument(Arg1,EX),
2052		force_evaluate_argument_for_member_check(Arg2,EY), %print(lazy_member(EX,EY)),nl,
2053		% causes 10 % slowdown on basin_olderog_bank, but code is probably required similar to evaluate_boolean_expression below
2054		% when(ground(EX), (ground(EY) -> is_member_set(EX,EY)
2055		% ; /* exploring lazy expression */ force_evaluate_argument(EY,REY),is_member_set(EX,REY))).
2056	?	when((ground(EX),ground(EY)), is_member_set(EX,EY)).
2057		check_boolean_expression(BExpr) :- %covering all boolean expression with relational operators instead of '==' and '!='%
2058		relational_binary_op(BExpr,Arg1,Arg2,EX,EY,Call),!,
2059		evaluate_int_argument(Arg1,EX),
2060		evaluate_int_argument(Arg2,EY),
2061		Call.
2062		check_boolean_expression(BExpr) :-
2063		bool_binary_op(BExpr,Arg1,Arg2,EX,EY,Call), !,
2064		%print(bool_binary_op(Arg1,Arg2,Call)),nl, %
2065		force_evaluate_argument(Arg1,EX),
2066		force_evaluate_argument(Arg2,EY),
2067	?	when((ground(EX),ground(EY)), Call).
2068		check_boolean_expression(X) :-
2069		add_error(haskell_csp,'Not a boolean expression: ',X),
2070		fail.
2071
2072
2073		:- block cond_check_boolean_expression(-,?).
2074		cond_check_boolean_expression(true,_).
2075		cond_check_boolean_expression(false,BExpr2) :- check_boolean_expression(BExpr2).
2076
2077		:- block ifte_check_boolean_expression(-,?,?).
2078		ifte_check_boolean_expression(true,Then,_) :- !, check_boolean_expression(Then).
2079		ifte_check_boolean_expression(false,_,Else) :- !, check_boolean_expression(Else).
2080		% evaluate_boolean_expression/3 will raise an error if the boolean expression in the ifte-condition cannot be evaluated to true or false => Internal Error
2081		ifte_check_boolean_expression(Other,Then,Else) :- add_internal_error(/*ifte_check_boolean_expression,*/
2082		'Internal Error: Not a boolean inside if-then-else test: ',
2083		ifte_check_boolean_expression(Other,Then,Else)),fail.
2084
2085		:- block evaluate_boolean_expression(-,?).
2086		%evaluate_boolean_expression(E,_) :- %print(evaluate_boolean_expression(E)),nl,
2087		% var(E),add_error(evaluate_boolean_expression,'Variable boolean expression:',E),fail.
2088		evaluate_boolean_expression(true,R) :- !, R=true.
2089		evaluate_boolean_expression(false,R) :- !, R=false.
2090		evaluate_boolean_expression(bool_not(BExpr1),Res) :- !,
2091		evaluate_boolean_expression(BExpr1,R1),
2092		negate(R1,Res).
2093		evaluate_boolean_expression(bool_and(BExpr1,BExpr2),Res) :- !,
2094		evaluate_boolean_expression(BExpr1,R1),
2095		cond_evalf_boolean_expression(R1,BExpr2,Res).
2096		evaluate_boolean_expression(bool_or(BExpr1,BExpr2),Res) :- !,
2097		evaluate_boolean_expression(BExpr1,R1),
2098		cond_evalt_boolean_expression(R1,BExpr2,Res).
2099		% when(ground(R1),
2100		% (R1=true -> Res = true
2101		% ; evaluate_boolean_expression(BExpr2,Res))).
2102		evaluate_boolean_expression('<'(Arg1,Arg2),Res) :- !,
2103		evaluate_int_argument(Arg1,EX),evaluate_int_argument(Arg2,EY),safe_less_than(EX,EY,Res).
2104		evaluate_boolean_expression('>'(Arg1,Arg2),Res) :- !,
2105		evaluate_int_argument(Arg1,EX),evaluate_int_argument(Arg2,EY),safe_less_than(EY,EX,Res).
2106		evaluate_boolean_expression('<='(Arg1,Arg2),Res) :- !,
2107		evaluate_int_argument(Arg1,EX),evaluate_int_argument(Arg2,EY),safe_less_than_equal(EX,EY,Res).
2108		evaluate_boolean_expression('>='(Arg1,Arg2),Res) :- !,
2109		evaluate_int_argument(Arg1,EX),evaluate_int_argument(Arg2,EY),safe_less_than_equal(EY,EX,Res).
2110		evaluate_boolean_expression(ifte(Test,Then,Else,_,_,_),R) :- !,
2111		evaluate_boolean_expression(Test,TestRes),
2112		ifte_eval_boolean_expression(TestRes,Then,Else,R).
2113		evaluate_boolean_expression(head(X),R) :- !, force_evaluate_argument(X,EX),head_list(EX,HResult),
2114		evaluate_boolean_expression(HResult,R).
2115		evaluate_boolean_expression(agent_call(Span,F,Par),R) :- !, /* in this context we need the result of the function call */
2116		unfold_function_call_once(F,Par,Body,Span),
2117		%when(nonvar(Body),
2118		evaluate_boolean_expression(Body,R).
2119		evaluate_boolean_expression(prolog_constraint(C),Res) :- !, %% print(prolog_constraint(C)),nl,
2120		(call(C) -> Res = true ; Res = false).
2121		evaluate_boolean_expression(null(Arg1),Res) :- !, force_evaluate_argument(Arg1,EX), is_null_list(EX,Res).
2122		evaluate_boolean_expression(empty(Arg1),Res) :- !, force_evaluate_argument(Arg1,EX), is_empty_set(EX,Res).
2123		evaluate_boolean_expression(BExpr,Res) :-
2124		bool_binary_op(BExpr,Arg1,Arg2,EX,EY,Call), !, % print(binop(BExpr,Arg1,Arg2)),nl,
2125		force_evaluate_argument(Arg1,EX),
2126		force_evaluate_argument(Arg2,EY), %print(ebe(Call)),nl,
2127		when((ground(EX),ground(EY)),
2128		(Call -> Res = true ; Res = false)).
2129		evaluate_boolean_expression('member'(Arg1,Arg2),Res) :- !, % after bool_binary_op: there is a special rule for member there
2130		force_evaluate_argument(Arg1,EX),
2131		force_evaluate_argument_for_member_check(Arg2,EY), %print(lazy_member(EX,EY)),nl,
2132	?	when(ground(EX),
2133		(ground(EY) -> (is_member_set(EX,EY) -> Res = true ; Res = false)
2134		; /* exploring lazy expression */ force_evaluate_argument(EY,REY),(is_member_set(EX,REY) -> Res = true ; Res = false))).
2135		evaluate_boolean_expression(builtin_call(X),Res) :- !, evaluate_boolean_expression(X,Res).
2136		evaluate_boolean_expression(X,_R) :-
2137		add_error(haskell_csp,'Not a boolean expression: ',X),
2138		fail.
2139
2140
2141		:- block negate(-,?).
2142		negate(true,false).
2143		negate(false,true).
2144
2145		:- block cond_evalt_boolean_expression(-,?,?).
2146		cond_evalt_boolean_expression(true,_,true).
2147		cond_evalt_boolean_expression(false,BExpr2,Res) :- evaluate_boolean_expression(BExpr2,Res).
2148
2149		:- block cond_evalf_boolean_expression(-,?,?).
2150		cond_evalf_boolean_expression(false,_,false).
2151		cond_evalf_boolean_expression(true,BExpr2,Res) :- evaluate_boolean_expression(BExpr2,Res).
2152
2153		:- block ifte_eval_boolean_expression(-,?,?,?).
2154		ifte_eval_boolean_expression(true,Then,_,Res) :- !, evaluate_boolean_expression(Then,Res).
2155		ifte_eval_boolean_expression(false,_,Else,Res) :- !, evaluate_boolean_expression(Else,Res).
2156		ifte_eval_boolean_expression(Other,Then,Else,Res) :- /* evaluate_boolean_expression/2 will catch the error if there
2157		is no boolean expression test, thus internal_error must be generated for this clause. */
2158		add_internal_error('Not a boolean inside if-then-else boolean expression test: ',
2159		ifte_eval_boolean_expression(Other,Then,Else,Res)),fail.
2160
2161		bool_binary_int_op('<'(X,Y),X,Y,EX,EY,'<'(EX,EY)).
2162		bool_binary_int_op('>'(X,Y),X,Y,EX,EY,'>'(EX,EY)).
2163		bool_binary_int_op('>='(X,Y),X,Y,EX,EY,'>='(EX,EY)).
2164		bool_binary_int_op('<='(X,Y),X,Y,EX,EY,'=<'(EX,EY)).
2165
2166		relational_binary_op('<'(X,Y),X,Y,EX,EY,safe_less_than(EX,EY)).
2167		relational_binary_op('>'(X,Y),X,Y,EX,EY,safe_less_than(EY,EX)).
2168		relational_binary_op('<='(X,Y),X,Y,EX,EY,safe_less_than_equal(EX,EY)).
2169		relational_binary_op('>='(X,Y),X,Y,EX,EY,safe_less_than_equal(EY,EX)).
2170
2171		bool_binary_op('elem'(X,Y),X,Y,EX,EY,is_elem_list(EX,EY)).
2172		%bool_binary_op('member'(X,Y),X,Y,EX,EY,is_member_set(EX,EY)) :- (X=setValue(_) -> false;true).
2173		bool_binary_op('member'(X,'Set'(Y)),X,Y,EX,EY,is_subset_of(EX,EY)) :-
2174		(X\=setValue(_) -> false; \+ground(X) -> false; true).
2175		bool_binary_op('=='(X,Y),X,Y,EX,EY,equal_element(EX,EY)).
2176		bool_binary_op('!='(X,Y),X,Y,EX,EY,not_equal_element(EX,EY)).
2177
2178		bool_binary_op_symbolic('member'(X,Y),X,Y,EX,EY,is_member_set(EX,EY)). % dealt with separately
2179
2180		unary_op(null(X),X,EX,is_null_list(EX)).
2181		unary_op(empty(X),X,EX,is_empty_set(EX,true)).
2182
2183		is_boolean_expression(true).
2184		is_boolean_expression(false).
2185		is_boolean_expression(bool_not(_)).
2186		is_boolean_expression(bool_and(_,_)).
2187		is_boolean_expression(bool_or(_,_)).
2188		is_boolean_expression(X) :-
2189		(unary_op(X,_,_,_) ; bool_binary_op(X,_,_,_,_,_) ; bool_binary_op_symbolic(X,_,_,_,_,_) ; bool_binary_int_op(X,_,_,_,_,_)).
2190
2191
2192		/* ------------------------------------- */
2193		/* SEQUENCES */
2194		/* ------------------------------------- */
2195
2196		:- use_module(probcspsrc(csp_sequences)).
2197
2198		/* ------------------------------------- */
2199		/* VALUE EXPRESSIONS */
2200		/* ------------------------------------- */
2201
2202		:- type channelio +--> (atomic ; dotTuple(list(atomic))).
2203
2204		:- type channel_set +--> (setValue(list(channelio)) ; closure(list(channelio))).
2205
2206		:- type cspm_expr +--> (type(cspm_arith_expr) ; type(channel_set) ; atomic ; agent_call(ground,nonvar,list(any)) ).
2207
2208		:- type cspm_arith_expr +--> (int(integer) ;
2209		'+'(cspm_arith_expr,cspm_arith_expr) ;
2210		'-'(cspm_arith_expr,cspm_arith_expr) ;
2211		'*'(cspm_arith_expr,cspm_arith_expr) ;
2212		'/'(cspm_arith_expr,cspm_arith_expr) ;
2213		'%'(cspm_arith_expr,cspm_arith_expr) ).
2214
2215		% forcing arguments in the context of a member check; will be used as second arg to is_member_set
2216		% This means that certain things do not need to be computed (Union for example)
2217		:- block force_evaluate_argument_for_member_check(-,?).
2218		force_evaluate_argument_for_member_check(agent_call(Span,F,Par),R) :- !,
2219		%print(unfold(F,Par,Body)),nl,
2220		unfold_function_call_once(F,Par,Body,Span),
2221	?	force_evaluate_argument_for_member_check(Body,R).
2222		% keep the following symbolic:
2223		force_evaluate_argument_for_member_check(setExp(rangeEnum(T),G),R) :- nonvar(T),T=[H|TT],TT==[], var(H), !,
2224		% if the tuples T have more than one element, we currently cannot check membership symbolically
2225		R=setExp(rangeEnum(T),G). % TO DO expand for rangeClosed,...
2226		force_evaluate_argument_for_member_check('Union'(L),R) :- !,
2227		force_evaluate_argument_for_member_check_into_list(L,LL), %print(evalUnion(L,LL)),nl,
2228		R='Union'(LL).
2229		force_evaluate_argument_for_member_check('Inter'(L),R) :- !,
2230		force_evaluate_argument_for_member_check_into_list(L,LL), R='Inter'(LL).
2231		force_evaluate_argument_for_member_check('Seq'(L),R) :- !, R='Seq'(L).
2232
2233	?	force_evaluate_argument_for_member_check(X,EX) :- force_evaluate_argument(X,EX).
2234
2235		% force evaluating a set into a list of elements; do not worry about checking duplicates in list
2236		:- block force_evaluate_argument_for_member_check_into_list(-,?).
2237		%force_evaluate_argument_for_member_check_into_list(A,R) :- print(force_evaluate_argument_for_member_check_into_list(A,R)),nl,fail.
2238		force_evaluate_argument_for_member_check_into_list(agent_call(Span,F,Par),R) :- !,
2239		/* in this context we need the result of the function call */
2240		unfold_function_call_once(F,Par,Body,Span),
2241		force_evaluate_argument_for_member_check_into_list(Body,R).
2242		force_evaluate_argument_for_member_check_into_list(setExp(rangeEnum(L)),R) :- !,
2243		force_evaluate_list_for_member_check(L,LL),R=setExp(rangeEnum(LL)).
2244		force_evaluate_argument_for_member_check_into_list(X,EX) :- force_evaluate_argument(X,EX).
2245
2246		:- block force_evaluate_list_for_member_check(-,?).
2247		force_evaluate_list_for_member_check([],R) :- !,R=[].
2248		force_evaluate_list_for_member_check([H|T],R) :- !, R=[EH|ET],
2249		force_evaluate_argument_for_member_check(H,EH),
2250		force_evaluate_list_for_member_check(T,ET).
2251		force_evaluate_list_for_member_check(X,R) :-
2252		add_internal_error('Iternal Error: Could not evaluate list: ',force_evaluate_list_for_member_check(X,R)),R=X.
2253
2254		%%%%%%%%%%%%%%%%%%%%%%%%%%%%% UNIT TESTS FOR force_evaluate_argument/2, evaluate_argument/2 and evaluate_expression/2 %%%%%%%%%%%%%%%%%%%%%%%
2255		:- assert_must_succeed((haskell_csp: force_evaluate_argument(listFromTo(1,3),R), R == list([int(1),int(2),int(3)]))).
2256		:- assert_must_succeed((haskell_csp: evaluate_argument(listFromTo(1,3),R), R == list([int(1),int(2),int(3)]))).
2257		:- assert_must_succeed((haskell_csp: evaluate_argument(listFrom(1),R), R == listFrom(1))).
2258		:- assert_must_succeed((haskell_csp: evaluate_argument(setFromTo(1,3),R), R == setFromTo(1,3))).
2259		:- assert_must_succeed((haskell_csp: evaluate_argument(list([int(1),int(2)]),R), R == list([int(1),int(2)]))).
2260		:- assert_must_succeed((haskell_csp: force_evaluate_argument(listPat([int(1),int(2)]),R), R == list([int(1),int(2)]))).
2261		:- assert_must_succeed((haskell_csp: evaluate_argument(ifte('<='(int(3),int(20)),'>='(int(2),int(1)),'<='(int(3),int(1)),span,span,span),R) ,R == true)).
2262		:- assert_must_succeed((
2263		haskell_csp: evaluate_argument(ifte('<='(int(3),int(2)),'>='(int(2),int(1)),'<='(int(3),int(1)),span,span,span),R), R ==false)).
2264		:- assert_must_succeed((haskell_csp: evaluate_argument(ifte('<='(int(3),int(2)),int(1),int(2),span,span,span),R), R == int(2))).
2265		:- assert_must_succeed((haskell_csp: evaluate_argument(dataType('FRUIT'),R), R == dataType('FRUIT'))).
2266		:- assert_must_succeed((haskell_csp: evaluate_argument(concat(listExp(rangeEnum([listFromTo(1,3),listExp(rangeEnum([int(4)]))]))),R),
2267		R == list([int(1),int(2),int(3),int(4)]))).
2268		:- assert_must_succeed((haskell_csp: evaluate_argument(listPat([int(1),int(2)]),R), R == list([int(1),int(2)]))).
2269		:- assert_must_succeed((haskell_csp: evaluate_argument(tuplePat([int(1),int(2)]),R), R == na_tuple([int(1),int(2)]))).
2270		:- assert_must_succeed((haskell_csp: evaluate_expression(setExp(rangeEnum([int(1),int(2)])),R), R == setValue([int(1),int(2)]))).
2271		:- assert_must_succeed((haskell_csp: evaluate_expression(setFromTo(1,3),R), R == setValue([int(1),int(2),int(3)]))).
2272		:- assert_must_succeed((haskell_csp: evaluate_expression(stop(src),R), R == 'Typed expression is a process construct.')).
2273		:- assert_must_succeed((haskell_csp: evaluate_expression(left,R), R == 'Typed expression is a channel name.')).
2274		:- assert_must_succeed((haskell_csp: evaluate_expression('Msg1',R), R == setValue(['A','B']))).
2275		:- assert_must_succeed((haskell_csp: evaluate_expression('Msg1',R), R == setValue(['A','B']))).
2276		:- assert_must_succeed((haskell_csp: evaluate_expression(builtin_call(set(listExp(rangeEnum([int(1),int(1)])))),R), R == setValue([int(1)]))).
2277		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2278
2279		evaluate_expression(X,R) :- var(X),!,
2280		add_internal_error('Internal Error: Variable expression to evaluate: ',evaluate_expression(X,R)),
2281		fail.
2282		evaluate_expression('Events',R) :- !,
2283		findall(Channel,is_a_channel_name(Channel),CL),
2284		evaluate_list(CL,CLL), closure_expand(CLL,R).
2285		evaluate_expression(closure(X),R) :- !,
2286		evaluate_list(X,XL), closure_expand(XL,R).
2287		evaluate_expression(builtin_call(X),R) :- !, evaluate_expression(X,R).
2288		evaluate_expression(setExp(X),R) :- !, evaluate_set_expression(X,EX),expand_symbolic_set(EX,R,evaluate_expression).
2289		evaluate_expression(setFromTo(Low,Up),R) :- !, expand_symbolic_set(setFromTo(Low,Up),R,evaluate_expression).
2290		evaluate_expression(val_of(X,Src),R) :- !, evaluate_argument2(val_of(X,Src),R).
2291	?	evaluate_expression(DT,R) :- is_a_datatype(DT,_),!,
2292		expand_symbolic_set(dataType(DT),R,eval).
2293	?	evaluate_expression(Proc,R) :- definite_cspm_process_expression(Proc),!, R='Typed expression is a process construct.'.
2294		evaluate_expression(Ch,R) :- is_a_channel_name(Ch),!, R='Typed expression is a channel name.'.
2295		evaluate_expression(E,R) :- force_evaluate_argument(E,R).
2296
2297		:- block force_evaluate_argument(-,?).
2298		force_evaluate_argument(Num,R) :- number(Num),!,R=int(Num).
2299		force_evaluate_argument(agent_call(Span,F,Par),R) :- !, /* in this context we need the result of the function call */
2300	?	unfold_function_call_once(F,Par,Body,Span),
2301	?	force_evaluate_argument(Body,R).
2302		force_evaluate_argument(setExp(RangeExpr,Generators),R) :- !,
2303		expand_set_comprehension(RangeExpr,Generators,R).
2304		%force_evaluate_argument(comprehensionGenerator(Var,Set),R) :- !,
2305		% R = comprehensionGenerator(Var,ESet),
2306		% force_evaluate_argument(Set,ESet).
2307		force_evaluate_argument(ifte(Test,Then,Else,_S1,_S2,_S3),R) :- !,
2308		evaluate_boolean_expression(Test,TestRes), % print(force_ifte(Test,TestRes)),nl,
2309	?	ifte_force_evaluate_argument(TestRes,Then,Else,R).
2310		force_evaluate_argument(list(X),R) :- !, %print(eval_list(X)),nl,
2311		force_evaluate_list(X,EX), % use force_evaluate_list_skel ??; perf. problem in misusing_lists
2312		R=list(EX).
2313		force_evaluate_argument(listPat(X),R) :- !, %print(eval_list(X)),nl,
2314		force_evaluate_list(X,EX), % use force_evaluate_list_skel ??; perf. problem in misusing_lists
2315		R=list(EX).
2316		force_evaluate_argument(listFromTo(X,Y),Res) :- !, expand_sequence(listFromTo(X,Y),Res).
2317		force_evaluate_argument(listExp(S),ERes) :- !, evaluate_list_expression(S,Res), expand_sequence(Res,ERes).
2318		%force_evaluate_argument(setValue(X),R) :- !, force_evaluate_set(X,R), print(fes(X,R)),nl.
2319		% Maybe we should ensure that setValues are always force evaluated: we only need to
2320		% take care when using set operations for replicated operators
2321		force_evaluate_argument(Destr,Result) :- destructor(Destr),!, % we may need to further evaluate result
2322		evaluate_argument2(Destr,EX), % do ordinary evaluation
2323		force_evaluate_argument(EX,Result).
2324	?	force_evaluate_argument(E,R) :- evaluate_argument2(E,R). /* could there be lazy constructs lurking deep inside E ??? */
2325
2326		destructor(head(_)).
2327		destructor(na_tuple_projection(_,_,_)).
2328		destructor(tuple_projection(_,_,_)).
2329		%destructor(record(_,_)).
2330		% records ?
2331
2332
2333		:- block ifte_force_evaluate_argument(-,?,?,?).
2334	?	ifte_force_evaluate_argument(true,Then,_,Res) :- !, force_evaluate_argument(Then,Res).
2335		ifte_force_evaluate_argument(false,_,Else,Res) :- !, force_evaluate_argument(Else,Res).
2336		/* See comment for the error clause of the ifte_evaluate_argument/4 predicate. Same argument as below
2337		for assuming the error clause as caused by internal call only. */
2338		ifte_force_evaluate_argument(Other,Then,Else,Res) :-
2339		add_internal_error('Internal Error: Not a boolean inside if-then-else test: ',
2340		ifte_force_evaluate_argument(Other,Then,Else,Res) ),fail.
2341
2342		:- block ifte_evaluate_argument(-,?,?,?).
2343		ifte_evaluate_argument(true,Then,_,Res) :- !, evaluate_argument(Then,Res).
2344		ifte_evaluate_argument(false,_,Else,Res) :- !, evaluate_argument(Else,Res).
2345		/* evaluate_boolean_expression/2 predicate is called before ifte_evaluate_argument/4.
2346		evaluate_boolean_expression/2 provides as result either true or false, that's why only internal call can
2347		raise error for this predicate. */
2348		ifte_evaluate_argument(Other,Then,Else,Res) :-
2349		add_internal_error('Internal Error: Not a boolean inside if-then-else test: ',
2350		ifte_evaluate_argument(Other,Then,Else,Res)),fail.
2351
2352		%evaluate_argument(E,R) :- print(evaluate_argument(E,R)),nl,
2353		%(nonvar(R) -> true ; when(nonvar(R),(print(inst_eval(E,R)),nl,trace))), evaluate_argument1(E,R).
2354		:- block evaluate_argument(-,?).
2355	?	evaluate_argument(Expr,Res) :- evaluate_argument2(Expr,Res).
2356
2357		evaluate_argument2(ifte(Test,Then,Else,_S1,_S2,_S3),R) :- !,
2358		evaluate_boolean_expression(Test,TestRes), %print(ifte(Test,TestRes)),nl,
2359		ifte_evaluate_argument(TestRes,Then,Else,R).
2360		% when(ground(TestRes),(TestRes=true -> evaluate_argument(Then,R) ; evaluate_argument(Else,R))).
2361		evaluate_argument2(int(X),R) :- !,R=int(X).
2362		% case should be added because of the clpfd-library
2363		evaluate_argument2(Num,R) :- number(Num),!,R=int(Num).
2364		evaluate_argument2(true,R) :- !,R=true.
2365		evaluate_argument2(false,R) :- !,R=false.
2366		evaluate_argument2(negate(X),Result) :- !, Result = int(Res),
2367		evaluate_int_argument(X,EX),
2368		safe_is(Res,-(EX)).
2369		evaluate_argument2('+'(X,Y),Result) :- !, Result = int(Res),
2370		evaluate_int_argument(X,EX),evaluate_int_argument(Y,EY),
2371		safe_is(Res,EX+EY).
2372		evaluate_argument2('-'(X,Y),Result) :- !, Result = int(Res),
2373		evaluate_int_argument(X,EX),evaluate_int_argument(Y,EY),
2374		safe_is(Res,EX-EY).
2375		evaluate_argument2('*'(X,Y),Result) :- !, Result = int(Res),
2376		evaluate_int_argument(X,EX),evaluate_int_argument(Y,EY),
2377		safe_is(Res,EX * EY).
2378		evaluate_argument2('/'(X,Y),Result) :- !, Result = int(Res),
2379		evaluate_int_argument(X,EX),evaluate_int_argument(Y,EY),
2380		safe_is(Res,EX // EY).
2381		evaluate_argument2('%'(X,Y),Result) :- !, Result = int(Res),
2382		evaluate_int_argument(X,EX),evaluate_int_argument(Y,EY),
2383		safe_is(Res,EX mod EY).
2384		evaluate_argument2(length(X),Result) :- !, force_evaluate_argument(X,EX),length_list(EX,Result).
2385		evaluate_argument2('#'(X),Result) :- !, force_evaluate_argument(X,EX),length_list(EX,Result).
2386		evaluate_argument2(head(X),Result) :- !, force_evaluate_argument(X,EX),
2387		head_list(EX,Result).
2388		evaluate_argument2(tail(X),Result) :- !, force_evaluate_argument(X,EX),tail_list(EX,Result).
2389		evaluate_argument2('^'(X,Y),Result) :- !,
2390		force_evaluate_argument(X,EX),force_evaluate_argument(Y,EY),
2391		%print('^'(X,EX,Y,EY)),nl,
2392		append_list(EX,EY,Result). %, print(append_list(EX,EY,Result)),nl.
2393		evaluate_argument2(concat(X),Result) :- !, force_evaluate_argument(X,EX),
2394		concat_lists(EX,Result).
2395		evaluate_argument2(listFromTo(X,Y),Res) :- !,
2396		%evaluate_int_argument(X,EX),evaluate_int_argument(Y,EY),
2397		expand_sequence(listFromTo(X,Y),Res).
2398		evaluate_argument2(listFrom(X),Res) :- !, Res = listFrom(X). % already evaluated
2399		evaluate_argument2(listExp(S),Res) :- !, evaluate_list_expression(S,Res).
2400		evaluate_argument2(listExp(RangeExpr,Generators),R) :- !, %print(listExp(Generators,RangeExpr)),nl,
2401		expand_listcomprehension(RangeExpr,Generators,R). %, print(res(R)),nl.
2402		%evaluate_argument2(listComp(Generators,Tuples),R) :- !, %force_evaluate_list(Generators,EGen),
2403		% expand_sequence(listComp(Generators,Tuples),R).
2404		evaluate_argument2(set(X),Res) :- !, evaluate_argument2(seq_to_set(X),Res).
2405		evaluate_argument2(seq(X),Res) :- !, evaluate_argument2(set_to_seq(X),Res).
2406		evaluate_argument2(set_to_seq(X),Res) :- !,
2407		force_evaluate_argument(X,EX),
2408		convert_set_to_seq(EX,Res).
2409		evaluate_argument2(seq_to_set(X),Res) :- !,
2410		force_evaluate_argument(X,EX),
2411		convert_seq_to_set(EX,Res).
2412		evaluate_argument2(setFromTo(X,Y),Res) :- !, Res = setFromTo(X,Y). % already computed set expression
2413		evaluate_argument2(setExp(S),Res) :- !, evaluate_set_expression(S,Res).
2414		evaluate_argument2(setExp(RangeExpr,Generators),R) :- !, %print(setExp(Generators,RangeExpr)),nl,
2415		expand_set_comprehension(RangeExpr,Generators,R).
2416		evaluate_argument2(setValue(X),R) :- !, R=setValue(X).
2417		evaluate_argument2(singleSetPatValue(X,Span),R) :- !, force_evaluate_argument(X,EX),
2418		%print(singleSetPatValue(X,EX,R)),nl,
2419		singleSetElement(EX,R,Span).
2420		evaluate_argument2('Seq'(X),R) :- !, evaluate_argument(X,EX),R='Seq'(EX).
2421		evaluate_argument2(intType,R) :- !, R=intType.
2422		evaluate_argument2(boolType,R) :- !, R=boolType.
2423		%evaluate_argument2(setEnum(X),R) :- !, evaluate_list(X,XL), evaluate_set(XL,R).
2424
2425		evaluate_argument2(closureComp(Generators,Tuples),R) :- !,
2426		% print(closureComp(Generators,Tuples)),nl,
2427		expand_symbolic_set(setExp(rangeEnum(Tuples),Generators),setValue(List),evaluate_argument_closureComp),
2428		% print(closureset(List)),nl,
2429		evaluate_argument2(closure(List),R). %print(doneclosureComp(R)),nl.
2430		evaluate_argument2(closure(X),R) :- !, %print(eval(closure(X))),nl,
2431		evaluate_list(X,XL), % print(evaluate_closure(XL,R)),nl,
2432		evaluate_closure(XL,R).
2433		%expand_channel_pattern_expression(closure(X),R,no_loc_info_available).
2434		evaluate_argument2('Events',R) :- !,
2435		findall(Channel,is_a_channel_name(Channel),CL),
2436		evaluate_argument2(closure(CL),R).
2437	?	evaluate_argument2(union(X,Y),Result) :- !, force_evaluate_argument(X,EX), force_evaluate_argument(Y,EY),
2438	?	union_set(EX,EY,Result).
2439		evaluate_argument2('Union'(X),Result) :- !, force_evaluate_argument(X,EX),
2440	?	big_union(EX,Result).
2441		evaluate_argument2('Inter'(X),Result) :- !, force_evaluate_argument(X,EX),
2442	?	big_inter(EX,Result).
2443	?	evaluate_argument2(diff(X,Y),Result) :- !, force_evaluate_argument(X,EX), force_evaluate_argument(Y,EY),
2444		%print(diff_set(X,EX,Y,EY)),nl,
2445		diff_set(EX,EY,Result).
2446	?	evaluate_argument2(inter(X,Y),Result) :- !, force_evaluate_argument(X,EX), force_evaluate_argument(Y,EY),
2447	?	inter_set(EX,EY,Result).
2448	?	evaluate_argument2(card(X),Result) :- !, evaluate_argument(X,EX),
2449		cardinality(EX,Result).
2450		evaluate_argument2('Set'(X),Result) :- !, %print(subsets(X)),nl,
2451		evaluate_argument(X,EX),
2452		%print(calling_subsets(EX)),nl,
2453		subsets(EX,Result). %, print(subset_result(Result)),nl.
2454		evaluate_argument2(agent_call(Span,F,Par),R) :- !,
2455	?	evaluate_agent_call(F,Par,R,Span).
2456		evaluate_argument2(agent_call_curry(F,Par),R) :- !,
2457		Span=no_loc_info_available,
2458		unfold_function_call_curry_once(F,Par,Value,Span),
2459		evaluate_argument(Value,R).
2460		evaluate_argument2(val_of(VAR,Span),R) :- !, /* this can only happen inside channel type expressions;
2461		other val_of's are compiled away by haskell_csp_analyzer */
2462		unfold_function_call_once(VAR,[],Body,Span),
2463		evaluate_argument(Body,R).
2464		evaluate_argument2([],R) :- !,R=[].
2465		evaluate_argument2([H|T],R) :- !,R=[H|T]. /* list of channel outputs */
2466		evaluate_argument2(builtin_call(X),R) :- !, evaluate_argument(X,R).
2467		evaluate_argument2(dotTuple(X),R) :- !, evaluate_dot_tuple(X,R).
2468		evaluate_argument2(dotTupleType(TupleArgs),R) :- !,
2469		evaluate_list(TupleArgs,ETupleArgs), R = dotTupleType(ETupleArgs).
2470		evaluate_argument2(dotpat(X),R) :- !, evaluate_dot_tuple(X,R).
2471		evaluate_argument2(tuple(F),R) :- !, R=tuple(F).
2472		evaluate_argument2(alsoPat(X,Y),R) :- !,
2473		evaluate_argument2(X,EX),
2474		evaluate_argument2(Y,EY),
2475		R=alsoPat(EX,EY).
2476		evaluate_argument2(lambda(A,B),R) :- !, %print(eval(lambda(A,B))),nl,
2477		R=lambda(A,B),
2478		(ground(A) -> true ;
2479		mynumbervars(A)). /* numbervars to avoid nonvar states for ProB (slows down hashing,...) */
2480		evaluate_argument2(tuplePat(TupleArgs),R) :- !, /* a non-associative tuple */
2481		R = na_tuple(EA),force_evaluate_list(TupleArgs,EA).
2482		evaluate_argument2(tupleExp(TupleArgs),R) :- !, /* a non-associative tuple; same as tuplePat but not in pattern position */
2483	?	R = na_tuple(EA),force_evaluate_list(TupleArgs,EA).
2484		evaluate_argument2(typeTuple(TupleArgs),R) :- !,
2485		evaluate_list(TupleArgs,ETupleArgs), R = typeTuple(ETupleArgs).
2486		evaluate_argument2(na_tuple(F),R) :- !, R=na_tuple(F). /* non-associative tuple */
2487		evaluate_argument2(na_tuple_projection(Nr,Tuple,Span),R) :- !,
2488		evaluate_int_argument(Nr,ENr,Span),
2489		force_evaluate_argument(Tuple,ETuple),
2490		na_tuple_projection(ENr,ETuple,R,Span).
2491		evaluate_argument2(list_projection(Nr,Len,List,Span),R) :- !,
2492		evaluate_int_argument(Nr,ENr,Span),
2493		evaluate_int_argument(Len,ELen,Span),
2494		force_evaluate_argument(List,EList),
2495		list_projection(ENr,ELen,EList,R,Span).
2496		evaluate_argument2(tuple_projection(Nr,Tuple,Span),R) :- !,
2497		evaluate_int_argument(Nr,ENr,Span),
2498		force_evaluate_argument(Tuple,ETuple),
2499		tuple_projection(ENr,ETuple,R,Span).
2500		evaluate_argument2(record(C,F),R) :- !, R=record(C,F).
2501		evaluate_argument2(list(X),R) :- !, %print(eval_list(X)),nl,
2502		%evaluate_list(X,EX),
2503		R=list(X). % TO DO: check if we also need listPat
2504		evaluate_argument2(listPat(X),R) :- !,
2505		evaluate_list(X,EX), R=list(EX).
2506		evaluate_argument2(rename(X,Y),R) :- !,
2507		evaluate_rename_channel_expression(X,RX), /* should we evaluate ??? */
2508		evaluate_rename_channel_expression(Y,RY),
2509		R=rename(RX,RY).
2510		evaluate_argument2(link(X,Y),R) :- !,
2511		evaluate_rename_channel_expression(X,RX), /* should we evaluate ??? */
2512		evaluate_rename_channel_expression(Y,RY),
2513		R=link(RX,RY).
2514		evaluate_argument2(dataType(DT),R) :- !, R=dataType(DT).
2515		evaluate_argument2(Channel,R) :-
2516		atomic(Channel),is_a_channel_name(Channel),!,R=tuple([Channel]).
2517		evaluate_argument2(DT,R) :- name_type(DT,DT_Def), !, R=DT_Def.
2518		evaluate_argument2(DT,R) :- dataTypeDef(DT,_), !, R=dataType(DT).
2519		evaluate_argument2(DT,R) :- subTypeDef(DT,_), !, R=dataType(DT).
2520		evaluate_argument2(X,R) :- valid_constant(X),!,R=X.
2521		evaluate_argument2(X,R) :- agent_functor(X,_),!,R=X. /* when a function name is passed */
2522		evaluate_argument2(X,R) :-
2523		is_csp_constructor(X),!,R=X. /* FDR does not allow this as a valid value; but can be fed into closure */
2524		evaluate_argument2(X,R) :-
2525		(undefined_process_construct(X) ->
2526	?	(is_boolean_expression(X) -> evaluate_boolean_expression(X,R)
2527		/* we have a boolean value; we could also decide not to evaluate the argument and put R=X*/
2528		; add_error(evaluate_argument2,'Cannot evaluate expression: ',X), R=X
2529		)
2530		; R=X /* we have a process description which is simply kept as is */
2531		).
2532
2533		% setExp(.)
2534		evaluate_set_expression(rangeEnum(List),Res) :- !, %evaluate_list(List,XL),
2535		evaluate_set(List,Res).%evaluate_set(List,Res,evaluate_argument).
2536		evaluate_set_expression(rangeClosed(X,Y),Res) :- !,
2537		evaluate_int_argument(X,EX),evaluate_int_argument(Y,EY),
2538		((number(X),number(Y),X>Y) -> Res= setValue([]) ; Res = setFromTo(EX,EY)).
2539		evaluate_set_expression(rangeOpen(X),Res) :- !,Res = setFrom(EX),
2540		evaluate_int_argument(X,EX).
2541		evaluate_set_expression(A,Res) :-
2542		add_internal_error('Internal Error: Unknown setExp: ',evaluate_set_expression(A,Res)),Res=[].
2543
2544		% listExp(.)
2545		evaluate_list_expression(rangeEnum(List),Res) :- !, Res=list(LR), evaluate_list(List,LR).
2546		evaluate_list_expression(rangeClosed(X,Y),Res) :- !, % print(evaluate_rangeClosed(X,Y)),nl,
2547		evaluate_int_argument(X,EX),evaluate_int_argument(Y,EY),
2548		((number(X),number(Y),X>Y) -> Res= list([]) ; Res = listFromTo(EX,EY)).
2549		evaluate_list_expression(rangeOpen(X),Res) :- !,Res = listFrom(EX),
2550		evaluate_int_argument(X,EX).
2551		evaluate_list_expression(A,Res) :- /* CSP-M Parser cannot generate list expression,
2552		which is not of the type rangeEnum/1, rangeClosed/2, rangeOpen/1.
2553		That's why we can assume that in this case we have internal error. */
2554		add_internal_error('Internal Error: Unknown listExp: ',evaluate_list_expression(A,Res)),Res=[].
2555
2556
2557
2558		evaluate_function_name(F,EF) :-
2559		(atomic(F) -> EF=F ; force_evaluate_argument(F,EF)).
2560
2561		evaluate_agent_call(F,Par,Res,Span) :- % print(eval_agent_call(F,Par)),nl,
2562	?	evaluate_function_name(F,EF),evaluate_agent_call2(EF,Par,Res,Span).
2563
2564		evaluate_agent_call2(lambda(Args,Body),Par,R,Span) :- !,
2565		unfold_function_call_once2(lambda(Args,Body),Par,NBody,Span),
2566	?	evaluate_argument(NBody,R).
2567		evaluate_agent_call2(F,Par,R,Span) :- !,
2568		(atomic(F) -> true
2569		; add_error(evaluate_argument,'Illegal function name for function application: ',agent_call(F,Par),Span),fail),
2570		X =.. [F|Par],
2571		((is_csp_process(X) ; is_possible_csp_process(X)) % ATTENTION: the parameter in is_possible_csp_process/1 can be a function call, which can be missunderstood as process
2572		% a reimplementation of the is_possible_csp_process/1 is needed.
2573		-> R=agent_call(Span,F,Par) %%%, print(keeping(X)),nl)
2574		/* keep agent_calls lazily; they are processes. If we unfold then the variables will be
2575		propagated into the term; causing problems by instantiation (see e.g. Repeat(Proc) = Proc ; Repeat(Proc)) */
2576		/* QUESTION: what about is_possible_csp_process ??? */
2577		; unfold_function_call_once2(F,Par,Body,Span),
2578	?	evaluate_argument(Body,R) /* TO DO: avoid re-checking when(nonvar ... for recursive calls ?*/
2579		% force_evaluate_argument(Body,R)
2580		).
2581
2582		% --------------------------------------------------------
2583		% integer expressions
2584		% --------------------------------------------------------
2585
2586		% --------------------------------------------------------
2587
2588		evaluate_int_argument(A,Res) :- evaluate_int_argument(A,Res,no_loc_info_available).
2589
2590		:- block evaluate_int_argument(-,?,?).
2591
2592		evaluate_int_argument(int(X),R,_) :- !, R=X.
2593		evaluate_int_argument(agent_call(Span,F,Par),R,Span) :- !, /* in this context we need the result of the function call */
2594		unfold_function_call_once(F,Par,Body,Span),
2595		%print(unfolded(F,Par,Body)),nl,
2596		evaluate_int_argument(Body,R,Span).
2597		evaluate_int_argument(Expr,IntRes,Span) :-
2598		force_evaluate_argument(Expr,Res), % because we need an integer, i.e., agent_calls need to be unfolded
2599		(Res = int(IntRes) -> true
2600		; (Res \= int(_), add_error(haskell_csp,'Expression does not evaluate to integer: ','='(Expr,Res),Span),
2601		fail)
2602		).
2603
2604		:- block evaluate_list(-,?).
2605		evaluate_list([],R) :- !,R=[].
2606		evaluate_list([H|T],R) :- !, R=[EH|ET],evaluate_argument(H,EH), evaluate_list(T,ET).
2607		evaluate_list(X,R) :- add_internal_error('Internal Error: Could not evaluate: ',evaluate_list(X,R)),R=X.
2608
2609		:- block evaluate_type_list(-,?).
2610		evaluate_type_list([],R) :- !,R=[].
2611		evaluate_type_list([H|T],R) :- !, R=[EH|ET],
2612	?	translate_to_type_expr(H,TypeH),
2613	?	evaluate_argument(TypeH,EH),
2614		evaluate_type_list(T,ET).
2615		evaluate_type_list(X,R) :-
2616		add_internal_error('Internal Error: Could not evaluate: ',evaluate_type_list(X,R)),R=X.
2617
2618		translate_to_type_expr(tupleExp(TupleArgs),R) :- !,
2619		R = typeTuple(TupleArgsRes),
2620		compile_tuple_args(TupleArgs,TupleArgsRes).
2621		translate_to_type_expr(dotTuple(TupleArgs),R) :- !,
2622		R = dotTupleType(TupleArgsRes),
2623		compile_tuple_args(TupleArgs,TupleArgsRes).
2624		translate_to_type_expr(X,CX) :-
2625	?	haskell_csp_analyzer:compile_body(X,'compile_tuple_args',[],[],CX).
2626
2627		compile_tuple_args([],R) :- !,R=[].
2628		compile_tuple_args([H|T],R) :- !,
2629		R=[CH|RH],
2630		haskell_csp_analyzer:compile_body(H,'compile_tuple_args',[],[],CH),
2631		compile_tuple_args(T,RH).
2632
2633		% -----------------------------------------------------
2634
2635
2636
2637
2638		force_evaluate_list(L,_EL) :- %print(force_evaluate_list(L,_EL)),nl,
2639		var(L),!, add_error(haskell_csp,'Trying to force evaluation of variable: ',L),fail.
2640		force_evaluate_list([],R) :- !,R=[].
2641		force_evaluate_list([H|T],R) :- !, R=[EH|ET],
2642	?	force_evaluate_argument(H,EH), %force_evaluate_argument(H,EH),
2643	?	force_evaluate_list(T,ET).
2644		force_evaluate_list(X,R) :-
2645		add_internal_error('Could not (force) evaluate list: ',force_evaluate_list(X,R)),R=X.
2646
2647		unfold_function_call_curry_once(F,[],F,_Span).
2648		unfold_function_call_curry_once(F,[Args|As],Value,Span) :-
2649		unfold_function_call_once(F,Args,Val,Span),!,
2650		% Val is a lambda-function
2651		unfold_function_call_curry_once(Val,As,Value,Span).
2652
2653		unfold_function_call_once(F,Par,Res,Span) :-
2654		evaluate_function_name(F,EF),
2655	?	unfold_function_call_once2(EF,Par,Res,Span).
2656
2657		unfold_function_call_once2(lambda(Args,Body),Parameters,R,Span) :- !,
2658		%print(unfold_lambda(Args,Parameters,Body,R)),nl,
2659		% varnumbers(lambda(Args,Body),lambda(CA,CB)), /* lift the frozen parameter-vars back to real-variables; we should only lift variables in Args ! */
2660		lift(Args,CA,Body,CB),
2661		% print(lifted_lambda(CA,CB)),nl,
2662		evaluate_lambda_arguments(Parameters,CA,EvalParas),
2663		(CA=EvalParas -> R = CB
2664		; add_error(cspm_trans,'Could not unify lambda args: ', lambda(CA,Parameters,body(Body)),Span),fail).
2665		unfold_function_call_once2(FunName,Parameters,R,Span) :- %print(unfold(FunName,Parameters)),nl,
2666	?	evaluate_agent_call_parameters(FunName,Parameters,EvalParas,Span),
2667		%%print(call_agent_compiled(FunName,Parameters,EX)),nl,
2668		call_agent_compiled(FunName,Parameters,EvalParas,R,Span).
2669
2670		:- block call_agent_compiled(-,?,?,?,?),call_agent_compiled(?,?,-,?,?).
2671		call_agent_compiled(FunCall,_,[],Res,Span) :- !, % no parameters
2672		call_agent_compiled2(FunCall,Res,Span).
2673		call_agent_compiled(FunName,_Parameters,EvalParas,Res,Span) :-
2674		EX =.. [FunName|EvalParas],
2675		(ground(EvalParas) -> call_agent_compiled2(EX,Res,Span)
2676		; %print(not_ground_call(FunName,Parameters,EvalParas)),nl, %typechecker:debug_non_ground_term(EX),
2677		is_nonvar_list_skel(EvalParas,OK), % was when(ground(EX),...)
2678		call_agent_compiled1(EX,Res,OK,Span)
2679		).
2680		:- block is_nonvar_list_skel(-,?).
2681		%is_nonvar_list_skel([],true). % clause not coverable, [] is always ground (see ground(EvalParas) -> .. in the body of last clause of call_agent_compiled/5)
2682		is_nonvar_list_skel([H|T],R) :- is_nonvar_list_skel(T,H,R).
2683		:- block is_nonvar_list_skel(-,?,?),is_nonvar_list_skel(?,-,?).
2684		is_nonvar_list_skel([],_,true).
2685	?	is_nonvar_list_skel([H|T],_,R) :- is_nonvar_list_skel(T,H,R).
2686
2687		:- block call_agent_compiled1(?,?,-,?).
2688	?	call_agent_compiled1(EX,Res,_,Span) :- call_agent_compiled2(EX,Res,Span).
2689
2690		call_agent_compiled2(EX,Res,Span) :-
2691	?	(agent_compiled(EX,Value,_SRCSPAN)
2692		-> %print(unfolded(Value,Res,EX)),nl,
2693		%(EX='OZS@__25'(_,_) -> trace ; true),
2694		Res=Value /* local cut imposes functional interpetation */
2695		; functor(EX,F,N), functor(Skel,F,N),
2696		(is_defined_agent(Skel) -> add_cspm_error(cspm_trans,'No matching case for function call: ',EX,Span)
2697		; add_cspm_error(cspm_trans,'Trying to apply undefined process/function: ',EX,Span)),
2698		fail
2699		).
2700
2701		safe_is(X,Expr) :- when(ground(Expr), X is Expr).
2702
2703		add_cspm_error(Source,Msg,CSPE,Span) :-
2704		(translate_cspm_state(CSPE,Transl) -> true ; Transl=CSPE),
2705		add_error(Source,Msg,Transl,Span).
2706
2707		/* ------------------------------------- */
2708		/* Renaming related predicates */
2709		/* ------------------------------------- */
2710
2711
2712		:- assert_must_succeed((
2713		retractall(csp_full_type_constructor(_,_,_)),
2714		haskell_csp:rename_action(io([int(1)],left,unknown(test)),[rename(right,left),rename(left,mid)],Res),
2715		Res== io([int(1)],mid,unknown(test)) )).
2716		:- assert_must_succeed((
2717		retractall(csp_full_type_constructor(_,_,_)),
2718		haskell_csp:rename_action(io([int(1)],ack,unknown(test)),[rename(right,left),rename(left,mid)],Res),
2719		Res== io([int(1)],ack,unknown(test)) )).
2720		:- assert_must_succeed((
2721		retractall(csp_full_type_constructor(_,_,_)),
2722		haskell_csp:rename_action(io([int(1)],right,unknown(test)),[rename(ack,right),rename(right,dotTuple([mid,int(2)]))],Res),
2723		Res== io([int(2),int(1)],mid,unknown(test)) )).
2724		:- assert_must_succeed((
2725		retractall(csp_full_type_constructor(_,_,_)),
2726		haskell_csp:rename_action(io([int(1)],ack,unknown(test)),[rename(ack,left),rename(ack,right)],Res),
2727		Res== io([int(1)],left,unknown(test)) )).
2728		:- assert_must_succeed((
2729		retractall(csp_full_type_constructor(_,_,_)),
2730		haskell_csp:rename_action(io([int(1)],ack,unknown(test)),[rename(ack,left),rename(ack,right)],Res),
2731		Res== io([int(1)],right,unknown(test)) )).
2732		% :- assert_must_succeed((
2733		% haskell_csp:haskell_csp:rename_action(io([int(0)],gen,unknown(test)),
2734		% [rename(gen,gen1),rename(gen,dotTuple([gen2,int(1)])),
2735		% rename(dotTuple([gen,int(0)]),dotTuple([gen2,int(9),int(9)])),
2736		% rename(stop(no_loc_info_available),dotTuple([gen2,int(2)+int(3)]))],R),
2737		% R == io([int(1),int(0)],gen2,unknown(test)) )).
2738
2739		:- block rename_action(-,?,-).
2740		rename_action(tick(TS),_,tick(TS)).
2741		rename_action(tau(X),_,tau(X)).
2742		rename_action(io(V,Ch,Span),RenamePatternList,Res) :- Res=io(_,_,_),
2743	?	match_pattern_list(RenamePatternList,V,Ch,Span,Res,false).
2744
2745		force_rename_action(io(V,Ch,Span),RenamePatternList,Res) :- /* as above; but renaming must occur */
2746	?	match_pattern_list(RenamePatternList,V,Ch,Span,Res,true). % true: means MatchOccured: not allowed to not rename
2747
2748		%not_renamed(tick(_),_). % case cannot occur, functor_dif(AX,tick) is always called before the not_renamed/2 predicate
2749		not_renamed(tau(_X),_).
2750		not_renamed(io(V,Ch,_Span),RenamePatternList) :-
2751	?	not_covered_action(RenamePatternList,V,Ch).
2752
2753		not_covered_action([],_,_).
2754		not_covered_action([rename(ChPat,_NewCh)|T],V,Ch) :-
2755		(ChPat= tuple([Ch2|TPat2]) %dotTuple([Ch2|T2])
2756		-> (dif(Ch,Ch2) ; Ch=Ch2,no_match_list(TPat2,V))%,print(nca_dif(V,T2)),nl
2757		; dif(Ch,ChPat)
2758	?	), not_covered_action(T,V,Ch).
2759
2760		:- assert_must_succeed(( haskell_csp:no_match_list([int(1)],[int(2)]) )).
2761		:- assert_must_succeed(( haskell_csp:no_match_list([int(2)],[int(1),int(2)]) )).
2762		:- assert_must_fail(( haskell_csp:no_match_list([],[int(1),int(2)]) )).
2763		:- assert_must_fail(( haskell_csp:no_match_list([int(2),int(3)],[int(2),int(3)]) )).
2764		%% :- assert_must_fail(( haskell_csp:no_match_list([out(int(2)),out(int(3))],[int(2),int(3)]) )).
2765		:- assert_must_succeed(( haskell_csp:no_match_list(X,[int(2),int(1)]),
2766		X=[int(2),int(2)])).
2767
2768		% check if a rename pattern matches a value on a channel:
2769		no_match_list(RenPattern,ChValue) :- % print(no_match_list(A,B)),nl,
2770		l_match_pattern_value(RenPattern,ChValue,match_false).
2771
2772		% check if a value matches an entry in the ChannelPatternList
2773		match_list(ChannelPatternList,V,Ch,Span) :-
2774		match_pattern_list(ChannelPatternList,V,Ch,Span,true,true).
2775
2776		:- block match_pattern_value(-,?,?), match_pattern_value(?,-,?).
2777		match_pattern_value(record(C,PatArgs),record(VC,ValArgs),Res) :- !,
2778		match_record(C,PatArgs,VC,ValArgs,Res).
2779		match_pattern_value(tuple(L1),tuple(L2),Res) :- !,
2780		l_match_pattern_value(L1,L2,Res).
2781		match_pattern_value(X,tuple([H|Rest]),Res) :- !,(H=X -> Res = match_true(Rest); Res=match_false).
2782		match_pattern_value(X,dotTuple([H|Rest]),Res) :- !,(H=X -> Res = match_true(Rest); Res=match_false).
2783		match_pattern_value(X,record([X|Rest]),Res) :- !, Res = match_true(Rest).
2784		match_pattern_value(Pat,Val,Res) :-
2785		when(?=(Pat,Val),(unify_check(Pat,Val)
2786		-> Res=match_true([]) ; Res=match_false)).
2787
2788		unify_check(int(V1),I2) :- !,
2789		(I2=int(V2) -> V1=V2
2790		%; preference(use_clpfd_solver,true), number(I2) -> V1 = I2
2791		; add_internal_error('Type error in unification of values: ',unify_check(int(V1),I2)),fail).
2792		unify_check(true,I2) :- !,
2793		(I2=true -> true ; I2=false -> fail
2794		; add_internal_error('Type error in unification of values: ',unify_check(true,I2)),fail).
2795		unify_check(false,I2) :- !,
2796		(I2=false -> true ; I2=true -> fail
2797		; add_internal_error('Type error in unification of values: ',unify_check(false,I2)),fail).
2798		unify_check(V,V).
2799
2800
2801
2802		:- block match_record(-,?,?,?,?), match_record(?,?,-,?,?).
2803		match_record(C1,_,C2,_,Res) :- C1\=C2,!, Res=match_false.
2804		match_record(C,PatArgs,C,ValArgs,Res) :- l_match_pattern_value(PatArgs,ValArgs,Res).
2805
2806		:- block l_match_pattern_value(-,?,?).
2807		l_match_pattern_value(vclosure,_T,R) :- !, R=match_true(vclosure).
2808		l_match_pattern_value([],T,R) :- !, R=match_true(T).
2809		l_match_pattern_value([H|T],Y,R) :- !, l_match_pattern_value1(Y,H,T,R).
2810		l_match_pattern_value(I,V,R) :-
2811		add_internal_error('Could not evaluate: ',l_match_pattern_value(I,V,R)),fail.
2812
2813		:- block l_match_pattern_value1(-,?,?,?).
2814		l_match_pattern_value1([],H,T,R) :- !, add_error(haskell_csp,'Too many values in rename pattern: ',[H|T]), R=match_false.
2815		l_match_pattern_value1([IODVal|IT],Pat,TPat,R) :- !,
2816		get_value_alsoPat(IODVal,PV),
2817		match_pattern_value(Pat,PV,Res),
2818		% print(matched(Pat,PV,Res,TPat,IT)),nl, %
2819		l_match_pattern_value2(Res,TPat,IT,R).
2820
2821		:- block l_match_pattern_value2(-,?,?,?).
2822		l_match_pattern_value2(match_true(M),TailPat,TailValue,Res) :-
2823		((TailPat=[],TailValue==[]) -> Res=match_true(M) % avoid error message in conjoin
2824		; TailPat=vclosure -> Res = match_true([]) % ignore match M;
2825		% there could be strange pattern match, but
2826		% it can happen that a partial record was provided (e.g., [|{|c_s.c_picks, in philosophers.csp)
2827		; (is_list(M),M\=[]) -> % one of the list arguments was a tuple, we need to pattern match the rest of the tuple arguments
2828		append(TailValue,M,TailValue1),
2829		l_match_pattern_value(TailPat,TailValue1,Res)
2830		;
2831		l_match_pattern_value(TailPat,TailValue,RT), % print(conjoin(RT,match_true(M),Res)),nl,
2832		conjoin_match(RT,match_true(M),Res)).
2833		l_match_pattern_value2(match_false,_,_,match_false).
2834
2835		:- block get_value_alsoPat(-,?).
2836		get_value_alsoPat(X,Res) :-
2837		get_value(X,R),
2838		(nonvar(R),R=alsoPat(V1,_V2) -> Res=V1 ; Res=R).
2839
2840		:- block conjoin_match(-,?,?), conjoin_match(?,-,?).
2841		conjoin_match(match_false,_,match_false).
2842		conjoin_match(match_true(_T),match_false,match_false).
2843		conjoin_match(match_true(T1),match_true(T2),Res) :- %append(T1,T2,TT).
2844		(T2==[] -> Res=match_true(T1) /* note T2: is the first match, T1 the later one */
2845		; T2==vclosure -> Res=match_true(T1) /* vclosure can propagate to the next level up */
2846		; conjoin_error(T2,T1,ResMatch), Res=match_true(ResMatch)).
2847
2848		% note: records (for example) are gradually enumerated; hence delay error message until we know the value of the inner match
2849		% check if we have a pattern match like rec.a.?.b.? -> this cannot be handled by us nor by FDR
2850		:- block conjoin_error(-,?,?).
2851		conjoin_error([],T1,M) :- !, M=T1.
2852		conjoin_error(vclosure,T1,M) :- !, M=T1.
2853		conjoin_error(T2,T1,T1) :- add_error(conjoin_match,'Rename pattern is incomplete in the middle. Ignoring first match: ',T2:T1).
2854
2855		:- assert_must_succeed((
2856		haskell_csp:match_pattern_list([tuple([c,int(0)|vclosure]),tuple([d|vclosure]),tuple([a,int(0),int(0),int(2)|vclosure])],[in(X),in(dotTuple([Y,Z]))],a,span,true,true),
2857		X=int(0), Y=int(0), Z=int(2))).
2858		:- assert_must_succeed((
2859		haskell_csp:match_pattern_list([tuple([c,int(0)|vclosure]),tuple([d|vclosure]),tuple([a,int(0),int(0),int(2)|vclosure])],[in(X),in(Y)],a,span,true,true),
2860		X=int(0), Y=tuple([int(0),int(2)]))).
2861		:- assert_must_succeed((
2862		haskell_csp:match_pattern_list([tuple([c,int(0)|vclosure]),tuple([d|vclosure]),tuple([a,int(0),int(0),int(2)]),tuple([d|vclosure])],[in(X),in(Y)],a,span,true,true),
2863		X=int(0), Y=tuple([int(0),int(2)]))).
2864		:- assert_must_fail((
2865		haskell_csp:match_pattern_list([tuple([a,int(0),int(0),int(2)]),tuple([c,int(0)|vclosure]),tuple([d|vclosure])],[in(X),in(Y)],a,span,true,true),
2866		X=int(0), Y=tuple([int(0),int(3)]))).
2867		:- assert_must_fail((
2868		haskell_csp:match_pattern_list([tuple([c,int(0)|vclosure]),tuple([d|vclosure]),tuple([a,int(0),int(0),int(2)])],[in(X),in(Y)],a,span,true,true),
2869		X=int(0), Y=tuple([int(0),int(3),int(2)]))).
2870
2871		% match_pattern_list(PatOrRenameList, Value,Channel,Span, Rename/MatchResult, HasMatchAlreadyOccured)
2872		match_pattern_list([],V,Ch,Span,io(V,Ch,SpanV),MatchOccured) :- %print(no_match(V,Ch,MatchOccured)),nl,
2873		set_span(SpanV,Span,match_pattern_list(Ch,V)),
2874		MatchOccured=false. % only allow unrenamed action if no match occured earlier
2875		match_pattern_list([rename(ChPat,NewCh)|T],V,Ch,Span,Res,MatchOccured) :- !,
2876		% print(checking_pat_match(ChPat,Ch,V)),nl, %%
2877		match_pattern_value(ChPat,tuple([Ch|V]),MatchRes),
2878	?	rename_action3(MatchRes,T,NewCh,V,Ch,Span,Res,MatchOccured).
2879		match_pattern_list([ChPat|T],V,Ch,Span,Res,MatchOccured) :- % for aParallel
2880		% print(checking_pat_match(ChPat,Ch,V)),nl, %%
2881		match_pattern_value(ChPat,tuple([Ch|V]),MatchRes),
2882		pat_match_action3(MatchRes,T,V,Ch,Span,Res,MatchOccured).
2883
2884		:- block pat_match_action3(-, ?,?,?,?, ?,?).
2885		pat_match_action3(match_true(Rest), _T, _V,_Ch,_Span, Res,_MatchOccured) :-
2886		(Rest=[] -> Res=true ; Rest=vclosure -> Res=true). % when doing a pat_match: we only allow full matches
2887		%pat_match_action3(match_true(_),T,V,Ch,Span,Res,_) :- match_pattern_list(T,V,Ch,Span,Res,true).
2888		pat_match_action3(match_false,T,V,Ch,Span,Res,MatchOccured) :- match_pattern_list(T,V,Ch,Span,Res,MatchOccured).
2889
2890		:- block rename_action3(-, ?,?, ?,?,?, ?,?).
2891		rename_action3(match_true(Rest), _T,NewCh, _V,_Ch,Span, Res,_MatchOccured) :-
2892		r_compose(NewCh,Rest,Span,Res).
2893	?	rename_action3(match_true(_),T,_NewCh,V,Ch,Span,Res,_) :- match_pattern_list(T,V,Ch,Span,Res,true).
2894	?	rename_action3(match_false,T,_NewCh,V,Ch,Span,Res,MatchOccured) :- match_pattern_list(T,V,Ch,Span,Res,MatchOccured).
2895
2896		r_compose(NewCh,Rest,Span,io(VRes,ResultingChannel,VSpan)) :-
2897		set_span(VSpan,Span,r_compose(NewCh)),
2898		%% print(rename_match(NewCh,Rest)),nl, %%
2899		evaluate_argument(dotTuple([NewCh|Rest]), ResultTuple),
2900		(ResultTuple = tuple([TCh|TV])
2901		-> ResultingChannel=TCh,VRes=TV
2902		; add_internal_error('Illegal result tuple: ', evaluate_argument(dotTuple([NewCh|Rest]), ResultTuple)),
2903		ResultingChannel=NewCh, VRes=Rest
2904		).
2905
2906
2907		evaluate_rename_list([],[]).
2908		evaluate_rename_list([rename(X,Y)|T],[rename(EX,EY)|ET]) :-
2909		evaluate_rename_channel_expression(X,EX),
2910		evaluate_rename_channel_expression(Y,EY),
2911		evaluate_rename_list(T,ET).
2912
2913		evaluate_link_list('linkList'(L),R) :- !,evaluate_link_list2(L,R).
2914		evaluate_link_list('linkListComp'(GeneratorList,LinkList),R) :- !,
2915		%print(procCompLinkList(GeneratorList,LinkList)),nl,
2916		% warning: LinkList does not have the rangeEnum wrapper expected
2917		expand_set_comprehension(rangeEnum(LinkList),GeneratorList,setValue(ExpandedLinks)),
2918		evaluate_link_list2(ExpandedLinks,R).
2919		evaluate_link_list(LL,R) :-
2920		add_internal_error('Cannot evaluate for Linked Parallel: ',evaluate_link_list(LL,R)),fail.
2921
2922		evaluate_link_list2([],[]).
2923		evaluate_link_list2([link(X,Y)|T],[rename(EX,EY)|ET]) :- /* note: link becomes rename */
2924		evaluate_rename_channel_expression(X,EX),
2925		evaluate_rename_channel_expression(Y,EY),
2926		evaluate_link_list2(T,ET).
2927
2928		rev_rename_list([],[]).
2929		rev_rename_list([rename(X,Y)|T],[rename(Y,X)|RT]) :- rev_rename_list(T,RT).
2930
2931
2932		evaluate_rename_channel_expression(E,RE) :- evaluate_argument(E,RE).
2933		% (E=dotTuple([CH|V])
2934		% -> (RE=dotTuple([CH|EV]),
2935		% l_evaluate_arguments(V,EV))
2936		% ; RE=E
2937		% ).
2938
2939		%%%%%%%%% DEAD CODE %%%%%%%%%%%%
2940		/*
2941		get_renamelist_range([],[]).
2942		get_renamelist_range([rename(_X,Y)|T],[Y|DT]) :-
2943		get_renamelist_range(T,DT).
2944		*/
2945
2946		/* ------------------------------------- */
2947
2948		/* hidden(Action, ChannelPatternList) */
2949		/* check whether an Action is covered by a CSP Channel Pattern List */
2950
2951		hidden(tau(_),_) :- fail.
2952		hidden(tick(_),_) :- fail.
2953		hidden(io(V,Ch,Span), ChannelPatternList) :- match_list(ChannelPatternList,V,Ch,Span).
2954
2955		/* same as hidden but allows tau; useful for alphab. parallel */
2956		:- block hidden_or_tau(-,?).
2957		hidden_or_tau(tau(_),_).
2958		hidden_or_tau(tick(_),_) :- fail.
2959		hidden_or_tau(io(V,Ch,Span), ChannelPatternList) :- match_list(ChannelPatternList,V,Ch,Span).
2960
2961
2962		expand_channel_pattern_expression(X,_,SrcSpan) :-
2963		% nl,print(expand_channel_pattern_expression(X)),nl,
2964		var(X), !,
2965		add_error(haskell_csp,'VARIABLE in expand_channel_pattern_expression: ',X,SrcSpan),fail.
2966		expand_channel_pattern_expression(agent_call(Span,F,Par),Res,SrcSpan) :- !,
2967		unfold_function_call_once(F,Par,Body,Span), expand_channel_pattern_expression(Body,Res,SrcSpan).
2968		expand_channel_pattern_expression(setValue(List),EList,SrcSpan) :- !,l_expand(List,EList,SrcSpan).
2969		expand_channel_pattern_expression(closure(List),EList,_SrcSpan) :- !,
2970		%print(haskell_csp:l_cexpand(List,EList)),nl,
2971		l_cexpand(List,EList).
2972		%% this two clauses are already computed by expanding the setValue(-) and closure(-) predicates above (DEAD CODE)
2973		/* expand_channel_pattern_expression([],R,_SrcSpan) :- !, R=[]. */ /* already computed */
2974		/*expand_channel_pattern_expression([tuple([C|T])|T2],R,SrcSpan) :- !,*/ /* already computed */
2975		/* (check_channel_value_is_complete(C,T,SrcSpan)
2976		-> R=[tuple([C|T])|R2] ; R=R2),
2977		expand_channel_pattern_expression(T2,R2,SrcSpan).
2978		*/
2979		expand_channel_pattern_expression(Exp,_,SrcSpan) :-
2980		add_error(haskell_csp,'Unknown expand_channel_pattern_expression: ',Exp,SrcSpan),fail.
2981
2982		/* translate a list of channel pattern expr. into uniform format */
2983		l_expand(X,R,SrcSpan) :- var(X),
2984		add_internal_error_with_span(haskell_csp,'Variable List for l_expand',X,SrcSpan), R=[].
2985		l_expand(List,Res,SrcSpan) :-
2986		convlist(expand_1(SrcSpan),List,Res).
2987
2988		expand_1(SrcSpan,El,R) :-
2989		expand(El,R,SrcSpan),!.
2990
2991		/*
2992		l_expand([],[],_).
2993		l_expand([H|T],Res,SrcSpan) :-
2994		(expand(H,EH,SrcSpan)->Res=[EH|ET];Res=ET),
2995		l_expand(T,ET,SrcSpan).
2996		*/
2997
2998		expand(tuple([Ch|List]),R,SrcSpan) :- !,R=tuple([Ch|List]),
2999		check_channel_value_is_complete(Ch,List,SrcSpan).
3000		expand(Channel,R,SrcSpan) :-
3001		(atomic(Channel) -> R=tuple([Channel])
3002		; add_error(haskell_csp,'Non-atomic argument: ',expand(Channel,R,SrcSpan)),fail).
3003
3004		check_channel_value_is_complete(Ch,List,SrcSpan) :-
3005		(channel_type_list(Ch,ChannelTypes)
3006		->
3007		(same_length(ChannelTypes,List) -> true
3008		; length(ChannelTypes,CL), length(List,L),
3009		(CL>L -> add_error(check_channel_value,'Incomplete event: ','.'(Ch,List),SrcSpan)
3010		; add_error(check_channel_value,'Too many values for event: ','.'(Ch,List),SrcSpan)
3011		), fail
3012		)
3013		; add_error(haskell_csp,'Undefined channel: ','.'(Ch,List),SrcSpan),fail
3014		).
3015
3016
3017		/* translate a list of channel pattern expr. into uniform format and add closure at end of list */
3018		l_cexpand(X,R) :- var(X), add_error(l_cexpand,'Variable List',X), R=[].
3019		l_cexpand(L,EL) :- maplist(cl_expand,L,EL).
3020
3021		% what about pat(_,_)
3022		cl_expand(tuple([Ch|List]),R) :- !, R = tuple([Ch|EL]),append_vclosure(List,EL). %, print(app_vcl(Ch,List,EL)),nl.
3023		cl_expand(Channel,R) :-
3024		(atomic(Channel) -> R = tuple([Channel|vclosure])
3025		; add_error(haskell_csp, 'Non-atomic argument: ',cl_expand(Channel,R)),fail).
3026
3027
3028		append_vclosure([record(X,Fields)],Res) :- incomplete_record(record(X,Fields),[_|_],_),!,
3029		Res = [record(X,EFields)|vclosure],
3030		append_vclosure(Fields,EFields).
3031		append_vclosure([],vclosure).
3032		append_vclosure([H|T],[H|VT]) :- append_vclosure(T,VT).
3033
3034
3035		/* not_hidden(Action, ChannelPatternList) */
3036		/* check whether an Action is *not* covered by a CSP Channel Pattern List */
3037
3038		/* not_hidden_test(io(tail_in(X),outf),
3039		[pat([int(2)],outf),pat([int(3)],outf),pat([int(8)],outf)]) */
3040
3041		:- block not_hidden(-,?).
3042		not_hidden(tau(_),_).
3043		not_hidden(tick(_),_).
3044		not_hidden(io(V,Ch,Span),ChannelPatternList) :- % print(not_hidden_test(V,Ch,ChannelPatternList)),nl, %
3045		%not_hidden_test(ChannelPatternList,V,Ch,Span).
3046		match_pattern_list(ChannelPatternList,V,Ch,Span,io(_,_,_),false). % Result is true in case match occurs with list
3047
3048
3049		/* ------------------------------------- */
3050
3051		:- block get_value(-,?).
3052
3053		get_value(in(V),R) :- !,R=V.
3054		get_value(out(V),R) :- !, add_internal_error('Obsolete out: ',get_value(out(V),R)), R=V.
3055		get_value(dot(V),R) :- !, add_internal_error('Obsolete dot: ',get_value(out(V),R)), R=V.
3056		get_value(record(Constructor,Fields),R) :- !, R = record(Constructor,ValueFields),
3057		l_get_value(Fields,ValueFields).
3058		get_value(V,V).
3059
3060		:- block l_get_value(-,?).
3061		l_get_value(L,VL) :- maplist(get_value,L,VL).
3062
3063	?	valid_constant(X) :- atomic(X), (csp_constant(X,_) -> true ; fail).
3064
3065
3066		/* ------------------------------------------ */
3067		/* SPAN Utilities */
3068		/* ------------------------------------------ */
3069
3070		%%%%%%%%%%%%%%%%%%%%% UNIT TESTS FOR THE SPAN UTILITIES %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3071		:- assert_must_succeed((haskell_csp: extract_span_info(_S,Info),Info == [])).
3072		:- assert_must_succeed((haskell_csp: extract_span_info(span_info(info,src_span(3,9,3,12,45,3)),R),R == [info])).
3073		:- assert_must_succeed((haskell_csp: extract_span_info(src_position(3,9,3,12), R),R == [])).
3074		:- assert_must_succeed((haskell_csp: extract_span_info(src_span(3,9,3,12,45,3), R),R == [])).
3075		:- assert_must_succeed((haskell_csp: extract_span_info(unknown(_), R),R == [])).
3076		:- assert_must_succeed((haskell_csp: extract_span_info(multi_span(3,9,3,12,45,3,span_info(info,src_span(3,9,3,12,45,3))), R),
3077		R == [info])).
3078		:- assert_must_succeed((haskell_csp: extract_span_info(src_span_operator(span_info(info,
3079		src_span(94417,10,94421,21,1496266,98)),src_span(94421,2,94421,4,1496345,2)),R), R == [info])).
3080		:- assert_must_succeed((haskell_csp: extract_span_info(no_loc_info_available,R), R == [])).
3081
3082		:- assert_must_succeed((haskell_csp: unify_spans(src_span(3,9,3,12,45,3),S,R),S== src_span(3,9,3,12,45,3), R == src_span(3,9,3,12,45,3))).
3083		:- assert_must_succeed((haskell_csp: unify_spans(src_span(3,9,3,12,45,3),src_span(4,9,5,16,40,5),R),
3084		R == multi_span(3,9,3,12,45,3,src_span(4,9,5,16,40,5)))).
3085		:- assert_must_succeed((haskell_csp: unify_spans(src_span_operator(src_span(94417,10,94421,21,1496266,98),src_span(94421,2,94421,4,1496345,2)),SP2, R), SP2 == src_span(94421,2,94421,4,1496345,2),
3086		R == src_span_operator(src_span(94417,10,94421,21,1496266,98),src_span(94421,2,94421,4,1496345,2)))).
3087		:- assert_must_succeed((haskell_csp: unify_spans(unknown(_),SP2,R), SP2 == R)).
3088		:- assert_must_succeed((haskell_csp: unify_spans(no_loc_info_available,SP2,R), SP2 == R)).
3089		:- assert_must_succeed((haskell_csp: unify_spans(src_span(3,9,3,12,12,3), no_loc_info_available,R), R == src_span(3,9,3,12,12,3))).
3090		:- assert_must_succeed((haskell_csp: unify_spans(span_info(info,src_span(3,9,3,12,45,3)),src_span(3,9,3,12,45,3),R),
3091		R == span_info(info,src_span(3,9,3,12,45,3)))).
3092		:- assert_must_succeed((haskell_csp: unify_spans(src_position(3,9,3,12),src_span(4,9,4,15,45,6),R),
3093		R == multi_span(3,9,3,21,3,12,src_span(4,9,4,15,45,6)))).
3094		:- assert_must_succeed((extract_span_from_event2(start_cspm_MAIN,SPAN, start_cspm_MAIN,_), SPAN == src(3,1,3,5,20,4))).
3095		:- assert_must_succeed((extract_span_from_event2(start_cspm('REC'),SPAN,start_cspm('REC'),_), SPAN == src(8,1,8,4,4,3))).
3096		:- assert_must_fail((extract_span_from_event(_X,_Span,_T,_NS))).
3097		:- assert_must_succeed((extract_span_info(src_position(_,_,_,_),R1), R1 ==[], extract_span_info(unknown(_),R2), R2 ==[])).
3098		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3099
3100		% span can already be set:
3101		% problem: rename_action in eprocRenaming has to instantiate Span; in other contexts hidden should not instantiate span
3102		set_span(SpanVar,SpanValue,PP) :- nonvar(SpanVar),!,
3103		debug_println(9,span_already_set(PP,SpanValue)).
3104		% print('*** Span already set to: '), print(SpanVar),nl,
3105		% print('*** tried to assign value: '),print(SpanValue),nl,print('*** Context: '), print(PP),nl.
3106		set_span(S,S,_C). % :- print(setting_span(S,_C)),nl.
3107
3108		extract_span_info(Span,Info) :- var(Span),!,Info=[].
3109		extract_span_info(span_info(Info,Span),[Info|T]) :- extract_span_info(Span,T).
3110		extract_span_info(src_position(_,_,_,_),[]).
3111		extract_span_info(src_span(_,_,_,_,_,_),[]).
3112		extract_span_info(src_span_operator(WholeSP1,_JustOperatorSP2),T) :- extract_span_info(WholeSP1,T).
3113		extract_span_info(unknown(_),[]).
3114		extract_span_info(multi_span(_,_,_,_,_,_,SP1),T) :- extract_span_info(SP1,T).
3115		extract_span_info(no_loc_info_available,[]).
3116
3117		:- block unify_spans(-,?,?).
3118		%unify_spans(S,_,R) :- !,R=S. % commenting this in gains 10 % performance, e.g., on crossing.csp benchmark
3119		unify_spans(SP1,SP2,R) :- ( unify_spans1(SP1,SP2,R) -> true
3120		; add_internal_error('Failed: ',unify_spans(SP1,SP2,R)),set_span(SP1,R,unify_spans)).
3121		:- block unify_spans1(-,?,?).
3122		unify_spans1(SP1,SP2,R) :- nonvar(R),!,
3123		debug_println(9,span_already_computed(R,unify_spans(SP1,SP2))).
3124		unify_spans1(span_info(Info,SP1),SP2,R) :- !, R=span_info(Info,RS),
3125		unify_spans1(SP1,SP2,RS).
3126		unify_spans1(src_position(StartLine,SC,OffsetByte,LenBytes),SP2,R) :- number(SC), number(LenBytes),!,
3127		EndLine = StartLine, EC is SC+LenBytes,
3128		gen_multi_span(SP2, StartLine,SC,EndLine,EC,OffsetByte,LenBytes, R).
3129		unify_spans1(src_span(StartLine,SC,EndLine,EC,OffsetByte,LenBytes),S,R) :- !,
3130		unify_spans2(src_span(StartLine,SC,EndLine,EC,OffsetByte,LenBytes),S,R).
3131		unify_spans1(src_span_operator(SP1,SP2),SP3,R) :- !, R=src_span_operator(SP1,SP23),
3132		unify_spans1(SP2,SP3,SP23).
3133		unify_spans1(multi_span(StartLine,SC,EndLine,EC,OffsetByte,LenBytes,SP1),SP2,R) :- !,
3134		unify_spans1(SP1,SP2,TailS),
3135		gen_multi_span(TailS, StartLine,SC,EndLine,EC,OffsetByte,LenBytes, R).
3136		unify_spans1(unknown(_),S,R) :- !, R=S.
3137		unify_spans1(no_loc_info_available,S,R) :- !, R=S.
3138		unify_spans1(S,_,S) :- add_error(unify_spans1,'Unknown Span: ',S).
3139
3140
3141		:- block unify_spans2(-,?,?).
3142		unify_spans2(src_span(StartLine,SC,EndLine,EC,OffsetByte,LenBytes),S,R) :-
3143		S=src_span(StartLine,SC,EndLine,EC,OffsetByte,LenBytes),!, R=S.
3144		unify_spans2(src_span(StartLine,SC,EndLine,EC,OffsetByte,LenBytes),SP2,R) :- !,
3145		gen_multi_span(SP2, StartLine,SC,EndLine,EC,OffsetByte,LenBytes, R).
3146
3147
3148		:- block gen_multi_span(-, ?,?,?,?, ?,?,?).
3149		gen_multi_span(no_loc_info_available, StartLine,SC,EndLine,EC, OffsetByte,LenBytes, R) :- !,
3150		R = src_span(StartLine,SC,EndLine,EC,OffsetByte,LenBytes).
3151		gen_multi_span(Span2,StartLine,SC,EndLine,EC,OffsetByte,LenBytes,R) :-
3152		R = multi_span(StartLine,SC,EndLine,EC,OffsetByte,LenBytes, Span2),!.
3153
3154
3155		:- block merge_span_into_event(?,-,?).
3156		merge_span_into_event(Event,no_loc_info_available,NewEvent) :- !,
3157		NewEvent=Event.
3158		merge_span_into_event(Event,AdditionalSpan,NewEvent) :-
3159		(extract_span_from_event(Event,SPAN,Templ,NewSPAN)
3160	?	-> Templ = NewEvent, unify_spans(SPAN,AdditionalSpan,NewSPAN)
3161		; (%add_error(merge_span_into_event,'Unknown Event: ',Event),
3162		% sometimes we cannot extract a source span, e.g., tau(repInternalChoice ...)
3163		NewEvent = Event)
3164		).
3165
3166		%type_of_event(io( or colour_of_event ...
3167		extract_span_from_event(Event,_Span,_Template,_NewSpan) :- var(Event),
3168		debug_println(9,'### extract_span_from_event variable'),!,fail.
3169		extract_span_from_event(Event,Span,Template,NewSpan) :- process_algebra_mode,!,
3170		extract_span_from_event2(Event,Span,Template,NewSpan).
3171
3172		%:- block extract_span_from_event2(-,?,?,?).
3173		extract_span_from_event2(start_cspm_MAIN,SPAN,start_cspm_MAIN,_) :- !,get_symbol_span('MAIN',SPAN).
3174		extract_span_from_event2(start_cspm(S),SPAN,start_cspm(S),_) :- !,get_symbol_span(S,SPAN).
3175		extract_span_from_event2(io(Ev,Ch,SPAN),SPAN,io(Ev,Ch,NewSPAN),NewSPAN).
3176		extract_span_from_event2(tau(link(Left,Right)),SPAN,Templ,NS) :- !, Templ = tau(link(Left,RTempl)),
3177		extract_span_from_event2(Right,SPAN,RTempl,NS). % the linking code already puts info into right branch
3178		%extract_span_from_event2(Left,RS,LTempl,RS),
3179		%unify_spans(LS,RS,NS).
3180		extract_span_from_event2(tau(hide(Event)),SPAN,Templ,NS) :- !, Templ = tau(hide(ETempl)),
3181		extract_span_from_event2(Event,SPAN,ETempl,NS).
3182		%extract_span_from_event2(tau(repInternalChoice(X)),no_loc_info_available,Templ,NS) :- !, Templ = tau(repInternalChoice(X)).
3183		extract_span_from_event2(tau(int_choice_left(S,LSpan)),SPAN,Templ,NS) :- !,
3184		Templ = tau(int_choice_left(S,NS)),
3185		SPAN = LSpan.
3186		extract_span_from_event2(tau(int_choice_right(S,RSpan)),SPAN,Templ,NS) :- !,
3187		Templ = tau(int_choice_right(S,NS)),
3188		SPAN = RSpan.
3189		extract_span_from_event2(tau(Event),SPAN,tau(Templ),NS) :- simple_tau_event(Event,Constructor,SPAN),!,
3190		functor(Templ,Constructor,1),
3191		arg(1,Templ,NS).
3192		%%extract_span_from_event2(i(SPAN),SPAN,i(NS),NS). %% deprecated
3193		extract_span_from_event2(tick(SPAN),SPAN,tick(NS),NS).
3194
3195		simple_tau_event(chaos_stop(Span),chaos_stop,Span).
3196		simple_tau_event(timeout(Span),timeout,Span).
3197		%simple_tau_event(int_choice_left(_,SrcSpan),int_choice_left,SrcSpan).
3198		%shift_span_for_left_branch(SrcSpan,LSpan).
3199		%simple_tau_event(int_choice_right(_,SrcSpan),int_choice_right,SrcSpan).
3200		%shift_span_for_right_branch(SrcSpan,RSpan).
3201		simple_tau_event(rep_int_choice(Span),rep_int_choice,Span).
3202		simple_tau_event(tick(Span),tick,Span).
3203
3204		:- assert_must_succeed((haskell_csp: shift_span_for_left_branch(src_span(3,1,_,_,4,_),R),
3205		R == src_span(3,1,3,2,4,1))).
3206		:- assert_must_succeed((haskell_csp: shift_span_for_left_branch(src_position(3,1,3,_),R),
3207		R == src_position(3,1,3,1))).
3208		:- assert_must_succeed((haskell_csp: shift_span_for_left_branch(src_span_operator(_SP,src_span(3,1,_,_,4,_)),R),
3209		R == src_span(3,1,3,2,4,1))).
3210		:- assert_must_succeed((haskell_csp: shift_span_for_left_branch(no_loc_info_available,R),
3211		R == no_loc_info_available)).
3212		:- assert_must_succeed((haskell_csp: shift_span_for_left_branch(unknown,R),
3213		R == unknown)).
3214		:- assert_must_succeed((haskell_csp: shift_span_for_left_branch(src,R),
3215		R == src)).
3216		:- block shift_span_for_left_branch(-,?).
3217		shift_span_for_left_branch(src_span(StartLine,SC,_EndLine,_EC,Off,_LenBytes),R) :- !,
3218		NEC is SC+1,
3219		R=src_span(StartLine,SC,StartLine,NEC,Off,1).
3220		shift_span_for_left_branch(src_position(StartLine,SC,Off,_LenBytes),R) :- !,
3221		R = src_position(StartLine,SC,Off,1).
3222		shift_span_for_left_branch(src_span_operator(_WholeSpan,JustOperator),R) :- !,
3223		shift_span_for_left_branch(JustOperator,R).
3224		shift_span_for_left_branch(no_loc_info_available,R) :- !, R=no_loc_info_available.
3225		shift_span_for_left_branch(unknown(I),R) :- !, R=unknown(I).
3226		shift_span_for_left_branch(X,X):- debug_println(9,not_shifting_left(X)).
3227
3228		:- assert_must_succeed((haskell_csp: shift_span_for_right_branch(src_span(_,_,3,2,6,5),R),
3229		R == src_span(3,1,3,2,10,1))).
3230		:- assert_must_succeed((haskell_csp: shift_span_for_right_branch(src_position(3,1,3,4),R),
3231		R == src_position(3,4,6,1))).
3232		:- assert_must_succeed((haskell_csp: shift_span_for_right_branch(src_span_operator(_SP,src_span(_,_,3,2,6,5)),R),
3233		R == src_span(3,1,3,2,10,1))).
3234		:- assert_must_succeed((haskell_csp: shift_span_for_right_branch(no_loc_info_available,R),
3235		R == no_loc_info_available)).
3236		:- assert_must_succeed((haskell_csp: shift_span_for_right_branch(unknown,R),
3237		R == unknown)).
3238		:- assert_must_succeed((haskell_csp: shift_span_for_right_branch(src,R),
3239		R == src)).
3240
3241		:- block shift_span_for_right_branch(-,?).
3242		shift_span_for_right_branch(src_span(_StartLine,_SC,EndLine,EC,Off,LenBytes),R) :- !,
3243		NL is 1, NSC is EC-1, NO is Off+LenBytes-1,
3244		R=src_span(EndLine,NSC,EndLine,EC,NO,NL).
3245		shift_span_for_right_branch(src_position(StartLine,SC,Off,LenBytes),R) :- !,
3246		NL is 1, NSC is SC+LenBytes-1, NO is Off+LenBytes-1,
3247		R = src_position(StartLine,NSC,NO,NL).
3248		shift_span_for_right_branch(src_span_operator(_WholeSpan,JustOperator),R) :- !,
3249		shift_span_for_right_branch(JustOperator,R).
3250		shift_span_for_right_branch(no_loc_info_available,R) :- !, R=no_loc_info_available.
3251		shift_span_for_right_branch(unknown(I),R) :- !, R=unknown(I).
3252		shift_span_for_right_branch(X,X):- debug_println(9,not_shifting_right(X)).
3253
3254
3255		% ----------------------
3256
3257		get_cspm_identifier(channel,ID) :- channel(ID,_).
3258		get_cspm_identifier(datatype,DT) :- is_a_datatype(DT,_).