1		% (c) 2009-2019 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2		% Heinrich Heine Universitaet Duesseldorf
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5		:- module(haskell_csp_analyzer,[is_csp_process/1, is_possible_csp_process/1, agent_functor/2, is_csp_constructor/1,
6		cspPrintCompiled/2, channel_type_list/2, csp_full_type_constructor/3,csp_full_type_constant/2,
7		%% csp_sub_type_constructor/3, csp_sub_type_constant/2, % reported as unnecessary exports by infolog
8		name_type/2, agent_compiled/3, csp_constant/2, analyze/0,
9		undefined_process_construct/1, definite_cspm_process_construct/4, csp_constructor/3,
10		is_a_channel_name/1,agent_parameters/3, is_list_skeleton/1,
11		lift/4, is_defined_agent/1,
12		definite_cspm_process_expression/1,
13		get_internal_csp_representation/1,
14		%% blocking_append/3, % reported as an unnecessary export by infolog
15		mynumbervars/1]).
16
17		:- use_module(probsrc(module_information)).
18		:- module_info(group,csp).
19		:- module_info(description,'Pre-compiler and analyzer for CSP.').
20
21		/******** SICSTUS libraries ********/
22		:- use_module(library(lists)).
23		:- use_module(library(codesio)).
24		/******** ----------------- ********/
25
26		/************** PROB modules **************/
27		:- use_module(probsrc(self_check)).
28		:- use_module(probsrc(debug),[debug_println/2, debug_mode/1, debug_print/2,
29		debug_nl/1, debug_stats/1, debug_level/1]).
30		:- use_module(probsrc(error_manager)).
31		:- use_module(probsrc(tools), [string_concatenate/3,remove_variables/3]).
32		:- use_module(probsrc(gensym),[gensym/2]).
33		:- use_module(probsrc(tools),[list_difference/3,exact_member/2]).
34		%--------- CSP modules:
35		:- use_module(probcspsrc(haskell_csp),[add_symbol_error/4, is_a_datatype/2,
36		channel/2, bindval/3, agent/3, agent_curry/3, dataTypeDef/2, subTypeDef/2, nameType/2,
37		cspTransparent/1, cspPrint/1, valid_constant/1,
38		extract_span_info/2,
39		evaluate_type_list/2, evaluate_argument/2]).
40		:- use_module(probcspsrc(csp_sets),[extract_variables_from_generator_list/2]).
41		:- use_module(probcspsrc(csp_tuples),[pattern_match_function_argument/3, is_constructor/3]).
42		/************** ------------ **************/
43
44		:- dynamic is_csp_constructor/1.
45		:- dynamic csp_full_type_constructor/3.
46		:- dynamic csp_sub_type_constructor/3.
47		:- dynamic csp_full_type_constant/2.
48		:- dynamic csp_sub_type_constant/2.
49
50		undefined_process_construct(X) :- \+ definite_cspm_process_construct(X,_,_,_),
51		\+ potential_cspm_process_construct(X,_,_,_).
52		/*defined_process_constructs(R) :- findall(F/N,(haskell_csp:clause(cspm_trans(X,_,_),_),nonvar(X), functor(X,F,N)),L),sort(L,R).
53		haskell_csp:defined_process_constructs(L), write_term(L,[quoted(true)]),nl. */
54
55		%:- dynamic cspm_trans/3.
56		/* findall(F/N,(haskell_csp:clause(cspm_trans(X,_,_),_),nonvar(X), functor(X,F,N)),L),sort(L,R),
57		member(F2/N2,R), functor(X2,F2,N2) ,write_term(cspm_process_construct(X2),[quoted(true)]), print('.'), nl, fail */
58
59		% definite_cspm_process_construct(Construct, Span(s), OtherSubConstructs, DefiniteCSPSubConstructs)
60		definite_cspm_process_construct(&(Grd,B), [],[Grd],[B]).
61		%%definite_cspm_process_construct('&'(_G,B),[_G],[B]).
62		definite_cspm_process_construct('/\\'(A,B,Span), [Span],[],[A,B]).
63		definite_cspm_process_construct(';'(A,B,Span), [Span],[],[A,B]).
64		definite_cspm_process_construct('[>'(A,B,Span), [Span],[],[A,B]).
65		definite_cspm_process_construct('[]'(A,B,Span), [Span],[],[A,B]).
66		definite_cspm_process_construct('\\'(A,Set,Span), [Span],[Set],[A]).
67		definite_cspm_process_construct(ehide(A,Set,Span),[Span],[Set],[A]).
68		definite_cspm_process_construct(exception(Set,A,B,Span), [Span],[Set],[A,B]).
69		definite_cspm_process_construct(eexception(Set,A,B,Span),[Span],[Set],[A,B]).
70		definite_cspm_process_construct(omega, [],[],[]).
71		definite_cspm_process_construct(skip(Span), [Span],[],[]).
72		definite_cspm_process_construct(stop(Span), [Span],[],[]).
73		definite_cspm_process_construct('CHAOS'(Span,B), [Span],[B],[]).
74		definite_cspm_process_construct('|||'(A,B,Span), [Span],[],[A,B]).
75		definite_cspm_process_construct('|~|'(A,B,Span), [Span],[],[A,B]).
76		definite_cspm_process_construct(val_of(A,Span), [Span],[],[A]).
77		definite_cspm_process_construct(eprocRenaming(RenList,B,Span),[Span],[RenList],[B]).
78		definite_cspm_process_construct(prefix(Span,A,B,C,Span2), [Span,Span2],[A,B],[C]).
79		definite_cspm_process_construct(procRenaming(RenList,B,Span),[Span],[RenList],[B]).
80		definite_cspm_process_construct(repSequence(Gen,A,Span), [Span],[Gen],[A]).
81		definite_cspm_process_construct(elinkParallel(A,B,C,Span), [Span],[A],[B,C]).
82		definite_cspm_process_construct(repChoice(Gen,A,Span), [Span],[Gen],[A]).
83		definite_cspm_process_construct(repInterleave(Gen,A,Span), [Span],[Gen],[A]).
84		definite_cspm_process_construct(repInternalChoice(Gen,A,Span),[Span],[Gen],[A]).
85		definite_cspm_process_construct(lParallel(LinkList,B,C,Span),[Span],[LinkList],[B,C]).
86		definite_cspm_process_construct(sharing(Set,B,C,Span), [Span],[Set],[B,C]).
87		definite_cspm_process_construct(esharing(Set,B,C,Span), [Span],[Set],[B,C]).
88		definite_cspm_process_construct(aParallel(E,A,C,B,Span), [Span],[E,C],[A,B]).
89		definite_cspm_process_construct(eaParallel(C,A,D,B,Span), [Span],[C,D],[A,B]).
90		definite_cspm_process_construct(procRepAParallel(Generators,pair(SYNC,A),Span),[Span],[Generators,SYNC],[A]).
91		definite_cspm_process_construct(procRepLinkParallel(Generators,SYNC,A,Span), [Span],[Generators,SYNC],[A]).
92		definite_cspm_process_construct(procRepSharing(SYNC,Generators,A,Span), [Span],[SYNC,Generators],[A]).
93		definite_cspm_process_construct(procRenamingComp(A,Gen,Ren),[],[Gen,Ren],[A]).
94		definite_cspm_process_construct(builtin_call(X), Span,Gen,P) :- definite_cspm_process_construct(X,Span,Gen,P).
95		definite_cspm_process_construct(P,[],[],[]) :- is_csp_process(P).
96		% potential CSPM constructs:
97
98		% potential_cspm_process_construct(Construct, Span(s), OtherSubConstructs, PossibleCSPSubConstructsIfConstructItselfIsCSP)
99		potential_cspm_process_construct(head(L),[],[],[L]).
100		potential_cspm_process_construct(ifte(G,B,C,S1,S2,S3),[S1,S2,S3],[G],[B,C]). % version with source-spans
101		potential_cspm_process_construct(agent_call(Span,A,Par), [Span],[A],[Par]).
102		potential_cspm_process_construct(agent_call_curry(A,Par), [], [A],[Par]).
103
104
105
106
107		:- dynamic is_function/1.
108		:- dynamic is_csp_process/1.
109		:- dynamic is_possible_csp_process/1.
110		:- dynamic change_happened/0.
111		:- dynamic cspPrintCompiled/2.
112
113		definite_cspm_process_expression(X) :- var(X),!,fail.
114		definite_cspm_process_expression(ifte(_Tst,T,E,_,_,_)) :- !,
115		(definite_cspm_process_expression(T) ; definite_cspm_process_expression(E)). /* assume no typing error */
116		% let(_,E) and val_of(X,_) will be precompiled to agents, therefore the two clauses below will never matched
117		%definite_cspm_process_expression(let(_,E)) :- !, definite_cspm_process_expression(E).
118		%definite_cspm_process_expression(val_of(X,_)) :- !,is_csp_process(X).
119		definite_cspm_process_expression(agent_call(_Span,F,Par)) :-
120		atomic(F), !, /* Note: with currying we can have expressions here ! TO DO: ADAPT */
121		X=..[F|Par],is_csp_process(X).
122		definite_cspm_process_expression(agent_call(_Span,lambda(_Args,Body),_Par)) :- !,
123		%%print(check(Body)),nl,
124		definite_cspm_process_expression(Body).
125		definite_cspm_process_expression(agent_call_curry(F,[Par1|_])) :- !,
126		atomic(F), /* Note: with currying we can have expressions here ! TO DO: ADAPT */
127		X=..[F|Par1],is_csp_process(X).
128		definite_cspm_process_expression(head(X)) :- !, /* shouldn't X be a list of CSP constructs ??? */
129		definite_cspm_process_expression(X).
130		definite_cspm_process_expression(lambda(_Head,Body)) :- \+var(Body), !, definite_cspm_process_construct(Body,_,_,_).
131		definite_cspm_process_expression(X) :- definite_cspm_process_construct(X,_,_,_).
132
133		possible_cspm_process_expression(X) :- var(X),!.
134		possible_cspm_process_expression(ifte(_Tst,T,E,_,_,_)) :- !,
135		(possible_cspm_process_expression(T) , possible_cspm_process_expression(E)).
136		/* assume no typing error; if either was definitely a CSP we would have matched above */
137		/* we require both to be possible CSP expressions ; influences unfolding of agent_calls,... see coz-example.csp*/
138		% the same as above for definite_cspm_process_expression applies to let(_,E) and val_of(X,_) (see comment above)
139		% they are precompiled to agents
140		%possible_cspm_process_expression(let(_,E)) :- !, possible_cspm_process_expression(E).
141		%possible_cspm_process_expression(val_of(X,_)) :- !, is_possible_csp_process(X).
142		possible_cspm_process_expression(agent_call(_Span,F,Par)) :- atomic(F),!,
143		X=..[F|Par], is_possible_csp_process(X).
144		possible_cspm_process_expression(agent_call(_,_,_)). /* TO DO: refine this */
145		possible_cspm_process_expression(agent_call_curry(_,_)). /* TO DO: refine this */
146		possible_cspm_process_expression(head(_)).
147
148		check_definition_body(X,_,_) :- var(X),!,true.
149		check_definition_body('$VAR'(X),_,_) :- !, cur_numbervars_index(Idx), X =< Idx.
150		% let expressions will be first precomiled into agent calls (case for check_definition_body/3 will never occur)
151		%check_definition_body(let(_,E),Def,Span) :- !,
152		% check_definition_body(E,Def,Span).
153		check_definition_body(lambda(_,E),Def,Span) :- !,
154		check_definition_body(E,Def,Span).
155		%check_definition_body(head(L),Def,Span) :- !, %% covered below by potential_cspm_process_construct
156		% val_of(_,X) expressions will be first precomiled into agent calls (case for check_definition_body/3 will never occur)
157		%check_definition_body(val_of(X,CallSpan),_Def,_Span) :- !,
158		% (is_defined_value(X) -> true ; add_internal_error(haskell_csp_analyzer,'Undefined Value: ',X,CallSpan)).
159		check_definition_body(agent_call(CallSpan,F,Par),_Def,_Span) :- atomic(F),!, X=..[F|Par],
160		((is_defined_agent(X); is_builtin_agent(X)) -> true ; add_error(haskell_csp_analyzer,'Undefined Agent Call: ',X,CallSpan)).
161		check_definition_body(agent_call(CallSpan,X,Par),_Def,_Span) :-
162		nonvar(X), X=lambda(Var,Body),!,
163		length(Par,PL), length(Var,VL),
164		(PL=VL -> true
165		; add_error(haskell_csp_analyzer,'Lambda parameters and arguments do not match: ',(Par,Var,Body),CallSpan)).
166		check_definition_body(agent_call(CallSpan,F,Par),Def,_Span) :- !,
167		(var(F) -> true ;
168		(F=agent_call(Span2,F2,Par2)
169		-> check_definition_body(agent_call(Span2,F2,Par2),Def,CallSpan)
170		; add_error(haskell_csp_analyzer,'Complicated LHS not yet supported in agent_call: ',
171		agent_call(F,Par),CallSpan)
172		)
173		).
174		check_definition_body(X,Def,Span) :-
175		definite_cspm_process_construct(X,Spans,OtherSubExprs,List),!,
176		l_check_spans(Spans,Span), l_check_non_csp_args(OtherSubExprs,Span),
177		l_check_definite_csp_args(List,Def,Span).
178		check_definition_body(X,Def,Span) :-
179		potential_cspm_process_construct(X,Spans,OtherSubExprs,List),
180		l_check_spans(Spans,Span), l_check_non_csp_args(OtherSubExprs,Span),
181		l_check_possible_csp_args(List,Def,Span).
182
183		check_definite_cspm_body_construct(X,D,S) :-
184		check_definition_body(X,D,S),!.
185		check_definite_cspm_body_construct(X,_Def,Span) :-
186		add_internal_error(haskell_csp_analyzer,'Unknown CSP construct: ',X,Span).
187
188		l_check_spans([],_Span).
189		l_check_spans([H|T],OuterSpan) :-
190		(extract_span_info(H,_Info) -> true
191		; add_internal_error('Illegal AST; unknown Span info: ',H:OuterSpan)),
192		l_check_spans(T,OuterSpan).
193
194		l_check_non_csp_args([],_Span).
195		l_check_non_csp_args([H|T],OuterSpan) :-
196		(\+ definite_cspm_process_expression(H) -> true
197		; (definite_cspm_process_construct(H,[Span|_],_,_) -> true ; Span=OuterSpan),
198		add_error(haskell_csp_analyzer,'Illegal AST; CSP process in illegal position: ',H,Span)),
199		l_check_non_csp_args(T,OuterSpan).
200		l_check_definite_csp_args([],_,_Span).
201		l_check_definite_csp_args([H|T],Def,Span) :-
202		check_definite_cspm_body_construct(H,Def,Span),l_check_definite_csp_args(T,Def,Span).
203		l_check_possible_csp_args([],_,_Span).
204		l_check_possible_csp_args([H|T],Def,Span) :-
205		check_definition_body(H,Def,Span),l_check_possible_csp_args(T,Def,Span).
206
207		is_defined_agent(EX) :- var(EX),!,fail.
208		is_defined_agent(EX) :- functor(EX,F,N), functor(Skel,F,N),
209		agent_compiled_without_constraints(Skel,_,_). % avoid executing Constraint
210		%is_defined_value(X) :- bindval(X,_,_).
211
212		is_builtin_agent(Term) :- var(Term),!,fail.
213		is_builtin_agent(Term) :-
214		member(Term,[ union(_,_), inter(_,_), diff(_,_), 'Union'(_), 'Inter'(_), member(_,_), card(_), empty(_),
215		set(_), head(_), tail(_), concat(_), null(_), elem(_,_), length(_), 'Set'(_), 'Seq'(_), seq(_)]),!.
216
217
218		agent_compiled_without_constraints(Head,Body,Span) :-
219		clause(agent_compiled(Head,Body,Span),_Constr).
220		agent_compiled_with_constraints(Head,Body,Span,Constr) :-
221		clause(agent_compiled(Head,Body,Span),Constr).
222
223		/* compute which values/agents are CSP processes and which ones are just ordinary functions/values */
224		analyze :- reset_csp_analyzer,
225		precompile_datatypes(init),% initialiazing constructors before starting to check the process bodies
226		debug_stats(precompile_constants),
227		precompile_constants,
228		debug_stats(compile_nested_let_expressions),
229		compile_nested_let_expressions,
230		opt_csp_listing,
231		debug_stats(find_csp_processes),
232		debug_print(19,'% Finding Definite CSP Processes:'),
233		analyze_recursively,
234		debug_nl(19),debug_print(19,'% Finding Possible CSP Processes: '),
235		analyze_recursively_possible,
236		check,
237		debug_stats(precompile_nametypes),
238		precompile_nametypes, /* must be put before datatypes */
239		precompile_datatypes(eval),
240		generate_channel_type_lists,
241		precompile_cspPrint,
242		debug_stats(precompile_finished).
243
244		reset_csp_analyzer :-
245		retractall(is_csp_process(_)),
246		retractall(is_function(_)),
247		retractall(is_possible_csp_process(_)),
248		retractall(multiple_let_equations_for(_,_)),
249		retractall(cspPrintCompiled(_,_)),
250		retractall(csp_full_type_constructor(_,_,_)),
251		retractall(csp_sub_type_constructor(_,_,_)),
252		retractall(csp_full_type_constant(_,_)),
253		retractall(csp_sub_type_constant(_,_)),
254		retractall(is_csp_constructor(_)),
255		retractall(channel_type_list(_,_)),
256		retractall(name_type(_,_)),
257		retractall(agent_functor(_,_)),
258		retractall(agent_compiled(_,_,_)),
259		retractall(agent_parameters(_,_,_)).
260
261		precompile_cspPrint :- cspPrint(Expr),
262		haskell_csp_analyzer:compile_body(Expr,'print',[],[],CompiledExpr),
263		assert(cspPrintCompiled(Expr,CompiledExpr)),
264		fail.
265		precompile_cspPrint.
266
267		analyze_recursively :-
268		retractall(change_happened),
269		agent_compiled_without_constraints(X,Body,_Span),
270		functor(X,F,N),functor(X2,F,N),
271		\+ is_csp_process(X2),
272		(is_function(X2) -> true ; assert(is_function(X2))),
273		definite_cspm_process_expression(Body),
274		assert(is_csp_process(X2)),
275		assert(change_happened),
276		debug_mode(on),print(' '),print_agent(X2),
277		fail.
278		analyze_recursively :- debug_print(19,';'),
279		(change_happened -> analyze_recursively ; debug_nl(19)).
280
281		analyze_recursively_possible :-
282		retractall(change_happened),
283		is_function(X2),
284		\+ is_csp_process(X2), \+ is_possible_csp_process(X2),
285		findall(Body,agent_compiled_without_constraints(X2,Body,_Span),AllBodies),
286		maplist(possible_cspm_process_expression,AllBodies),
287		assert(is_possible_csp_process(X2)),
288		assert(change_happened),
289		debug_mode(on),print(' '),print_agent(X2),
290		fail.
291		analyze_recursively_possible :- debug_print(19,';'),
292		(change_happened -> analyze_recursively_possible ; debug_nl(19)).
293
294
295		check :- debug_println(15,'% Checking Definitions:'),
296		findall(V,bindval(V,_,_),LBV),
297		check_for_multiples(LBV),
298		findall(W,(agent(W,_,_);agent_curry(W,_,_)),LAG),
299		check_for_contig(LAG),
300		% Note: we cannot detect if a function definition is interrupted by a bindval or channel def
301		debug_nl(15),
302		debug_println(9,'% Checking Definition bodies:'),
303		agent_compiled_without_constraints(X,Body,Span),
304		(debug_mode(on) -> print(' '),print_agent(X) ; true),
305		check_definition_body(Body,X,Span),
306		fail.
307		check :- debug_nl(15).
308
309		% ----------------------------------------------
310
311
312
313		csp_constant(C,T) :- csp_full_type_constant(C,T).
314		csp_constant(C,T) :- csp_sub_type_constant(C,T).
315
316		csp_constructor(C,T,A) :- csp_full_type_constructor(C,T,A).
317		csp_constructor(C,T,A) :- csp_sub_type_constructor(C,T,A).
318
319		csp_full_type_constant(apples,'FRUIT'). csp_full_type_constant(oranges,'FRUIT'). csp_full_type_constant(pears,'FRUIT'). % complementary to default CSP-M spec
320
321		precompile_datatypes(E) :-
322		(E = eval -> debug_println(15,'% Precompiling datatype constructor types: ')
323		; debug_println(15,'% Initialising datatype constructor types: ')),
324		retractall(csp_full_type_constructor(_,_,_)),
325		dataTypeDef(Type,ConstructorList), debug_println(15,Type), debug_println(15,' '),
326		member(X,ConstructorList),
327		(X = constructor(_)
328		-> fail /* already asserted */
329		; (X = 'constructorC'(C,dotTupleType(CT)),(E = eval -> evaluate_type_list(CT,CTypes) ; true)
330		-> assert(csp_full_type_constructor(C,Type,CTypes))
331		; (X = 'constructorC'(C,typeTuple([dotTuple(CT)])),(E = eval -> evaluate_type_list(CT,CTypes) ; true) % can appear for example for sq.(x.y)
332		-> assert(csp_full_type_constructor(C,Type,CTypes))
333		; (X = 'constructorC'(C,typeTuple(CT)),(E = eval -> evaluate_type_list(CT,CTypes) ; true)
334		-> assert(csp_full_type_constructor(C,Type,[typeTuple(CTypes)]))
335		; add_internal_error('Unknown constructor in precompile_datatypes: ',(Type:X))
336		)
337		)
338		)
339		),
340		fail.
341		precompile_datatypes(E) :- nl,
342		retractall(csp_sub_type_constructor(_,_,_)),
343		subTypeDef(Type,ConstructorList), debug_println(15,Type), debug_println(15,' '),
344		member(X,ConstructorList),
345		(X = constructor(_)
346		-> fail /* already asserted */
347		; (X = 'constructorC'(C,dotTupleType(CT)),(E = eval -> evaluate_type_list(CT,CTypes) ; true) % eval only when all declarations are pre-compiled
348		-> assert(csp_sub_type_constructor(C,Type,CTypes))
349		; (X = 'constructorC'(C,typeTuple([dotTuple(CT)])),(E = eval -> evaluate_type_list(CT,CTypes) ; true) % can appear for example for sq.(x.y)
350		-> assert(csp_sub_type_constructor(C,Type,CTypes))
351		; (X = 'constructorC'(C,typeTuple(CT)),(E = eval -> evaluate_type_list(CT,CTypes) ; true)
352		-> assert(csp_sub_type_constructor(C,Type,[typeTuple(CTypes)]))
353		; add_error(precompile_datatypes,'Unknown constructor: ',(Type:X))
354		)
355		)
356		)
357		),
358		fail.
359		precompile_datatypes(_E) :- debug_nl(15).
360
361		/* can be executed before definitions are parsed; as no need to call evaluate_list */
362		precompile_constants :- debug_print(20,'% Precompiling datatype constants: '),
363		retractall(csp_full_type_constant(_,_)),
364		retractall(csp_sub_type_constant(_,_)),
365		retractall(is_csp_constructor(_)),
366		dataTypeDef(Type,ConstructorList), debug_print(20,Type), debug_print(20,' '),
367		member(constructor(C),ConstructorList),
368		assert(csp_full_type_constant(C,Type)),
369		fail.
370		precompile_constants :-
371		is_a_datatype(_Type,ConstructorList),
372		member('constructorC'(C,_),ConstructorList),
373		assert(is_csp_constructor(C)),fail.
374		precompile_constants :-
375		subTypeDef(SubType,ConstructorList), debug_print(20,SubType), debug_print(20,' '),
376		member(constructor(C),ConstructorList),
377		(csp_full_type_constant(C,_SuperType) -> true
378		; add_error(precompile_constants,'Subtype introduces new constant: ',(SubType:C))
379		),
380		assert(csp_sub_type_constant(C,SubType)),
381		fail.
382		precompile_constants :- debug_nl(20).
383
384		% ----------------------------------------------
385
386		:- dynamic channel_type_list/2, name_type/2.
387
388		channel_type_list(left,[dataType('FRUIT')]).
389		channel_type_list(right,[dataType('FRUIT')]).
390		channel_type_list(mid,[dataType('FRUIT')]).
391		channel_type_list(ack,[]).
392		channel_type_list(a,[intType]). /* for test cases */
393		channel_type_list(b,[intType]). /* for test cases */
394		channel_type_list(c,[intType]). /* for test cases */
395		channel_type_list(gen1,[intType,intType]). /* for test cases */
396		channel_type_list(gen2,[intType,intType]). /* for test cases */
397
398		/* test cases for the is_not_infinite_type/1 predicate in haskell_csp module (see lines 374 - 398) */
399
400		channel_type_list(receive,[dataType('SubMsg')]).
401		channel_type_list(contact,[dataType('SubSubMsg'),intType,boolType]).
402		channel_type_list(infinite,[dataType('Inf')]).
403
404		is_a_channel_name(Ch) :- channel(Ch,_). % use channel/2 rather than channel_type_list/2, as channel/2 available before precompilation
405
406		/* TO DO: check if there can be a nesting of associative dotTuples and non-associative Tuples */
407		generate_channel_type_lists :- debug_print(20,'% Analyzing channels:'),
408		retractall(channel_type_list(_,_)),
409		channel(X,CType), debug_print(20,' '),debug_print(20,X),
410		(CType = type(Type) -> true ; add_error_fail(haskell_csp_analyzer,'Channel type in wrong format: ',channel(X,Type))),
411		(Type = dotTupleType(List)
412		-> ((evaluate_type_list(List,EList),flatten_dotTupleTypes(EList,FlatEList))
413		-> assert(channel_type_list(X,FlatEList)) %% EList ????? <----------
414		%, nl, print(dotTupleType(List,EList,FlatEList)),nl
415		; add_symbol_error(haskell_csp_analyzer,'Could not evaluate channel type list: ',channel(X,Type),X)
416		)
417		; Type = dotUnitType -> assert(channel_type_list(X,[]))
418		; Type = typeTuple(List)
419		-> (evaluate_type_list(List,EList)
420		-> assert(channel_type_list(X,[typeTuple(EList)]))
421		; add_symbol_error(haskell_csp_analyzer,'Could not evaluate non-associative tuple:',channel(X,Type),X)
422		)
423		; otherwise -> add_symbol_error(haskell_csp_analyzer,'Unexpected channel type: ',channel(X,Type),X)
424		),
425		fail.
426		generate_channel_type_lists :- debug_nl(20).
427
428		flatten_dotTupleTypes([],[]).
429		flatten_dotTupleTypes([dotTupleType(L)|T],R) :- !,
430		flatten_dotTupleTypes(L,RL),
431		append(RL,RR,R),
432		flatten_dotTupleTypes(T,RR).
433		flatten_dotTupleTypes([H|T],[H|R]) :- flatten_dotTupleTypes(T,R).
434
435
436		precompile_nametypes :- debug_print(20,'% Analyzing nametypes:'),
437		retractall(name_type(_,_)),
438		nameType(X,CType), debug_print(20,' '),debug_print(20,X),
439		(CType = type(Type) -> true ; add_error_fail(haskell_csp_analyzer,'Nametype type in wrong format: ',nameType(X,Type))),
440		(Type = dotTupleType(List)
441		-> (evaluate_type_list(List,EList)
442		-> (EList = [TheType] -> true /* we have a single type; not really a dotTuple */
443		; TheType = dotTupleType(EList)), %% was typeTuple ??? <----------
444		assert(name_type(X,TheType))
445		; add_symbol_error(haskell_csp_analyzer,'Could not evaluate nametype list:',nameType(X,Type),X)
446		)
447		; Type = dotUnitType -> assert(name_type(X,dotUnitType))
448		; Type = typeTuple(List)
449		-> (evaluate_type_list(List,EList)
450		-> assert(name_type(X,typeTuple(EList)))
451		; add_symbol_error(haskell_csp_analyzer,'Could not evaluate non-associative tuple:',nameType(X,Type),X)
452		)
453		; otherwise -> add_symbol_error(haskell_csp_analyzer,'Unexpected nametype: ',nameType(X,Type),X)
454		),
455		fail.
456		precompile_nametypes :- debug_nl(20).
457
458		:- use_module(library(samsort)).
459		%check_for_multiples(S) :- length(S,Len), remove_dups(S,S2),length(S2,Len),!.
460		check_for_multiples(S) :- samsort(S,SS),check_for_multiples2(SS).
461		check_for_multiples2([]).
462		check_for_multiples2([H|T]) :-
463		(T=[H|T2] -> add_symbol_error(haskell_csp,'Multiple Definitions of: ',H,H) ; T2=T),
464		check_for_multiples2(T2).
465
466		check_for_contig([]).
467		check_for_contig([H,H2|T]) :- functor(H,F,N), functor(H2,F,N), !, check_for_contig(T).
468		check_for_contig([H|T]) :-
469		(member(H,T) -> add_symbol_error(haskell_csp,'Definition not contiguous: ',H,H) ; true),
470		check_for_contig(T).
471
472		print_agent(T) :- nonvar(T),functor(T,F,N), print(F/N).
473
474
475
476		/* ------------------------ LET COMPILATION ----------------------------- */
477
478		:- dynamic agent_compiled/3.
479		:- dynamic agent_parameters/3.
480		%agent_compiled(H,B) :- agent_compiled(H,B_SRCSPAN).
481
482
483		get_agent(Head,Body,SRCSPAN) :- bindval(F,FBody,SRCSPAN),
484		% (FBody = lambda(Args,Body)
485		% -> Head =.. [F|Args] /* translate m = \ x,y @ BODY into m(x,y) = BODY */
486		% ;
487		Head=F, Body=FBody
488		% )
489		.
490		get_agent(Head,Body,SRCSPAN) :- agent(Head,Body,SRCSPAN).
491		get_agent(Head,Body,SRCSPAN) :- agent_curry(CHead,CBody,SRCSPAN),
492		translate_agent_curry(CHead,CBody,Head,Body,SRCSPAN).
493
494
495		translate_agent_curry(CHead,CBody,Head,Body,SPAN) :-
496		CHead =.. [Function,Args1|Rest],
497		Head =.. [Function|Args1], translate_into_lambda(Rest,CBody,Body,SPAN).
498		%,nl,print(agent_curry(Head,Body)),nl,nl,nl.
499
500		translate_into_lambda([],Body,Body,_SPAN).
501		translate_into_lambda([Args1|Rest],Body,Res,SPAN) :-
502		l_compile_head_para(Args1,NewParas,Constraint,lambda(Args1),SPAN),
503		(Constraint = true
504		-> LBody=RB
505		; S=no_loc_info_available,
506		LBody = ifte(prolog_constraint(Constraint),RB,error(illegal_curried_arg),S,S,S)
507		),
508		Res = lambda(NewParas,LBody),
509		translate_into_lambda(Rest,Body,RB,SPAN).
510
511
512		:- dynamic agent_functor/2.
513		init_agent_functor :- retractall(agent_functor(_,_)),
514		get_agent(X,_B,_SRCSPAN), nonvar(X),
515		functor(X,F,Arity),
516		assert(agent_functor(F,Arity)),
517		fail.
518		init_agent_functor.
519
520		%agent_functor(F,Arity) :- agent_parameters(F,Arity,_).
521
522		:- if(current_prolog_flag(dialect,sicstus)).
523		:- if((current_prolog_flag(version_data,sicstus(4,X,_,_,_)),X<3)).
524		:- use_module(library(terms),[term_variables/2]). % is built-in in SICSTUS 4.3
525		:- endif.
526		:- endif.
527
528		% below we compile let expression into separate agent definitions
529		% so that we get the treatment of local variables from Prolog
530		% the same is applied to prefixes with input variables (which are also local variables)
531		compile_nested_let_expressions :- debug_println(5,'% Compiling nested let expressions:'),
532		retractall(agent_compiled(_,_,_)),
533		retractall(agent_parameters(_,_,_)),
534		init_agent_functor, reset_cur_numbervars_index,
535		get_agent(X,Body,SRCSPAN),
536		(var(X) ->
537		add_internal_error(haskell_csp,'Error in compiled .pl File: Uninstantiated LHS in bindval or agent',(X,Body),SRCSPAN),fail
538		; true),
539		compile_head(X,NX,Constraints,SRCSPAN),
540		debug_println(5,compiled_head(X,NX,Constraints)),
541
542		NX=..[F|_N_XARGS],
543		(debug_mode(on) -> print(' '),print_agent(X),nl ; true),
544		term_variables(X,InnerVariables), XARGS=InnerVariables, % these are the variables before extracting pattern matches into Constraints
545		%debug_println(9,compiling_body(Body,F,_N_XARGS,XARGS)),
546		(compile_body(Body,F,XARGS,[],Res)
547		-> true
548		; add_internal_error(haskell_csp,'Unable to compile body of agent: ',agent(X,Body),SRCSPAN), fail
549		),
550		assert_agent_compiled_head(NX,Res,SRCSPAN,Constraints),
551		% (Constraints = true -> assert_agent_compiled(NX,Res,SRCSPAN) ; assert_agent_compiled(NX,Res,SRCSPAN,Constraints)),
552		%portray_clause( (agent_compiled(NX,Res) :- Constraints)),
553		fail.
554		compile_nested_let_expressions :- (debug_mode(on) -> nl ; true).
555
556
557		:- dynamic multiple_let_equations_for/2.
558
559		multiple_definitions(Head) :- functor(Head,F,_),
560		multiple_let_equations_for(F,_),!.
561		multiple_definitions(Head) :- functor(Head,F,N), functor(CH,F,N), functor(CH2,F,N),
562		get_agent(CH,Body,SRCSPAN), get_agent(CH2,Body2,SRCSPAN2),
563		(CH,Body,SRCSPAN) \= (CH2,Body2,SRCSPAN2).
564
565		compile_head(Head,NewHead,Constraints,SPAN) :-
566		Head =.. [Func|Args],
567		l_compile_head_para(Args,NewArgs,Constraints,Head,SPAN),
568		NewHead =.. [Func|NewArgs].
569
570		l_compile_head_para([],[],true,_,_).
571		l_compile_head_para([H|T],[NH|NT],Constraints,Head,SPAN) :-
572		compile_head_para(H,NH,CH,Head,SPAN),
573		l_compile_head_para(T,NT,CT,Head,SPAN),
574		(CH=true -> Constraints=CT ; (CT=true -> Constraints=CH ; Constraints = ','(CH,CT))).
575
576
577		compile_head_para(Var,NewPara,Constraint,_Head,_Span) :- var(Var),!, NewPara=Var, Constraint=true.
578		compile_head_para(emptySet,NewPara,Constraint,_Head,_Span) :- !, Constraint=true, NewPara = setValue([]).
579		compile_head_para(listPat(List),NewPara,RestConstr,Head,Span) :- !, NewPara=list(NList),
580		l_compile_head_para(List,NList,RestConstr,Head,Span).
581		compile_head_para(singleSetPat(List),NewPara,RestConstr,Head,Span) :- !, NewPara=setValue(NList),
582		l_compile_head_para(List,NList,RestConstr,Head,Span).
583		compile_head_para(dotpat(List),NewPara,Constraint,Head,Span) :- !,
584		% TO DO: check if we have a record constructor and can construct a record pattern: we would need no constraint
585		Constraint = (pattern_match_function_argument(tuple(WNList),NewPara,Head),RestConstr),
586		l_compile_head_para(List,NList,RestConstr,Head,Span),
587		wrap_free_vars(NList,WNList). % wrap free vars with in(.)
588		compile_head_para(tuplePat(List),NewPara,Constraint,Head,Span) :- !, NewPara = na_tuple(NList),
589		l_compile_head_para(List,NList,Constraint,Head,Span).
590		compile_head_para(alsoPattern([Pat1]),NewPara,Constraint1,Head,Span) :- !,
591		compile_head_para(Pat1,NewPara,Constraint1,Head,Span).
592		compile_head_para(alsoPattern([Pat1|Tail]),NewPara,Constr,Head,Span) :- !,
593		compile_head_para(Pat1,NewPara,Constraint1,Head,Span),
594		compile_head_para(alsoPattern(Tail),NewPara2,Constraint2,Head,Span),
595		Constr = (NewPara=NewPara2,Constraint1,Constraint2).
596		compile_head_para(appendPattern([Pat1]),NewPara,Constraint1,Head,Span) :- !,
597		compile_head_para(Pat1,NewPara,Constraint1,Head,Span).
598		compile_head_para(appendPattern([H|T]),NewPara,Constraints,Head,Span) :-
599		nonvar(H), H=listPat(HList),is_list_skeleton(HList),!,
600		compile_head_para(H,NH,ConstraintH,Head,_), NH=list(NHList),
601		NewPara = list(NewList),
602		compile_head_para(appendPattern(T),NewT,ConstraintsT,Head,Span),
603		Constraints = ','(ConstraintH,ConstraintsT),
604		NewT = list(TList), append(NHList,TList,NewList).
605		compile_head_para(appendPattern(Pat),NewPara,Constraint,Head,Span) :-
606		is_list_skeleton(Pat),
607		append(T,[H],Pat),
608		nonvar(H), H=listPat(HList),is_list_skeleton(HList),!,
609		compile_head_para(H,NH,ConstraintH,Head,_), NH=list(NHList),
610		compile_head_para(appendPattern(T),NewT,ConstraintsT,Head,Span),
611		NewPara = list(NewList), NewT = list(TList),
612		Constraint=','(ConstraintH,','(append(TList,NHList,NewList),ConstraintsT)).
613		% to do: appendPattern with more parameters
614		compile_head_para(appendPattern(Pat),_,_,_Head,Span) :-
615		%haskell_csp:get_symbol_span(Head,HeadSpan),
616		add_error(compile_head_para,'Unsupported Append Pattern: ',Pat,Span),fail.
617		compile_head_para(X,_,_,Head,Span) :-
618		atomic(X),
619		channel(X,_), %print(Head),nl,
620		(multiple_definitions(Head)
621		-> add_message(compile_head_para,'Warning: Channel name used as Function/Process argument: ',X)
622		; % haskell_csp:get_symbol_span(Head,HeadSpan),
623		add_error(compile_head_para,'Warning: Channel name used as Function/Process argument: ',X, Span)
624		),
625		fail.
626		compile_head_para(X,NewPara,Constraint,_Head,_Span) :-
627		atomic(X), evaluate_argument(X,NewPara), !,
628		%% print(compiled_head_para(X,NewPara)),nl,
629		Constraint=true.
630		compile_head_para(P,P,true,_Head,_Span).
631
632
633		wrap_free_vars([],[]).
634		wrap_free_vars([H|T],[WH|WT]) :-
635		(var(H) -> WH=in(H) ; WH=H),
636		wrap_free_vars(T,WT).
637
638		is_list_skeleton(X) :- var(X),!,fail.
639		is_list_skeleton([]).
640		is_list_skeleton([_|T]) :- is_list_skeleton(T).
641
642		/* compile_body(ExpressionToCompile, Top-Level-FunName, ArgumentsToAddToNestedLetsOrPrefixes,LocalLets, CompiledExpr) */
643		compile_body(Body,F,XARGS,NDEFS,Res) :- compile_body(Body,F,XARGS,NDEFS,false,Res).
644		/* false = we are not in a dangerous context where prefixes with input variables need to be lifted out */
645
646		%compile_body(X,F,XA,D,DC,R) :- print(compile_body(X,F,XA,D,DC,R)),nl,fail.
647		compile_body(X,_F,_XARGS,_DEFS,_DC,Res) :- var(X),!, Res=X.
648		%add_error(haskell_csp_analyzer,'Variable in compile_body:'(X,F)),Res=X.
649		compile_body(lambda(Args,Body),F,XARGS,DEFS,DC,Res) :- !, %nl,print(lambda1(Args,Body)),nl,
650		l_compile_head_para(Args,CArgs,Constraints,lambda(Args,Body),unknown_span),
651		(Constraints=true -> true
652		; add_error(compile_body,'ProB does not (yet) support complicated patterns inside lambda: ',lambda(Args,Body))),
653		mynumbervars(CArgs), % note: important that compilation of body does detect $VAR
654		% otherwise will fail to add necessary parameters
655		Res = lambda(CArgs,ResBody),
656		append(Args,XARGS,NewXARGS),
657		compile_body(Body,F,NewXARGS,DEFS,DC,ResBody).
658		compile_body(val_of(X,Span),_F,_XARGS,DEFS,_DC,Res) :- !, /* we do not need to compile X itself !? */
659		% haskell_csp:get_symbol_span(X,Span), % does this work for local lets ???
660		(is_local_let2(X,0,[],DEFS,NX,NPar,_)
661		-> Res = agent_call(Span,NX,NPar)
662		; Res=agent_call(Span,X,[])).
663		compile_body(agent_call(_Span,TFun,[Arg]),F,XARGS,DEFS,DC,Res) :-
664		cspTransparent([TFun]), !,
665		compile_body(Arg,F,XARGS,DEFS,DC,Res).
666		compile_body(agent_call_curry(X,Paras),F,XARGS,DEFS,DC,Res) :- !,
667		/* translate agent_call_curry into nested agent_calls : */
668		(Paras=[Paras1|RestParas]
669		-> compile_body(agent_call_curry(agent_call(no_loc_info_available,X,Paras1),RestParas),F,XARGS,DEFS,DC,Res)
670		; compile_body(X,F,XARGS,DEFS,DC,Res)
671		).
672		compile_body(agent_call(_Span,X,Para),F,XARGS,DEFS,DC,Res) :- atomic(X),
673		Term=..[X|Para], length(Para,N), length(NPara,N), Fun=..[X|NPara],
674		(\+ agent(Fun,_Body,_Src), is_builtin_agent(Term), \+is_local_let(Fun,DEFS,_NewFun,_FXArgs,_)),!,
675		compile_body(builtin_call(Term),F,XARGS,DEFS,DC,Res).
676		compile_body(agent_call(Span,X,Para),F,XARGS,DEFS,_DC,Res) :- atomic(X),
677		CX=X, %%%%compile_body(X,F,XARGS,DEFS,true,CX),
678		l_compile_body(Para,F,XARGS,DEFS,true,CPara),
679		(is_local_let2(CX,_Arity,CPara,DEFS,NX,NPara,_) -> Res = agent_call(Span,NX,NPara) ; Res=agent_call(Span,CX,CPara)).
680		compile_body(prefix(Span,Values,ChannelExpr,CSP,Span2),F,XARGS,DEFS,DC,Res) :- !,
681		compile_body(ChannelExpr,F,XARGS,DEFS,DC,NewChExpr),
682		l_compile_channel_value(Values,F,XARGS,DEFS,NewVals,NewXARGS,Span),
683		%print(comp_channel(Values,NewVals)),nl,
684		compile_body(CSP,F,NewXARGS,DEFS,DC,NewCSP),
685		ResBody = prefix(Span,NewVals,NewChExpr,NewCSP,Span2),
686		(NewXARGS \= XARGS %,DC = true always lift out so that states are ground and that we need no variant/instance checks !
687		-> /* need to lift prefix */
688		gensym('->',GSF), debug_println(5,generating_agent_for_prefix(F,GSF, ResBody)),
689		string_concatenate(F,GSF,PrefixName),
690		Call =.. [PrefixName|XARGS],
691		Res = agent_call(Span,PrefixName,XARGS),
692		% portray_clause( prefix_agent(Call,ResBody) ),
693		assert_agent(Call, ResBody,Span),
694		functor(Call,CF,CN), functor(CallSkel,CF,CN),
695		assert( is_csp_process(CallSkel) )
696		; %print(not_lifting_prefix(Values,F,XARGS,DC, NewXARGS),nl,
697		Res = ResBody
698		).
699		compile_body(X,F,XARGS,DEFS,DC,Res) :-
700		replicated_or_comprehension(X,Op,Vars,OutsideOfScope,InScope,NewDC,ISCSP,Span),!,
701		% print(repl(X,Op,Vars)),nl,print(inscope(InScope)),nl, print(outofscope(OutsideOfScope)),nl,
702		(var(Vars)
703		-> add_error(haskell_csp_analyzer,'Replicated variables var: ',X),fail ; true),
704		%%print(compiling_set(OutsideOfScope,XARGS)),nl,
705		% This part does not need the extra variables Vars as parameters
706		compile_body(OutsideOfScope,F,XARGS,DEFS,DC,NewOutsideOfScope),
707		% print(done_outside(NewOutsideOfScope)),nl,
708		append(Vars,XARGS,NewXARGS), % add the variables of the comprehension as additional parameters to nested calls
709		%%print(compiling_csp(InScope,NewXARGS)),nl,
710		compile_body(InScope,F,NewXARGS,DEFS,NewDC,NewInScope),
711		% print(done_csp(InScope,NewInScope)),nl,
712		replicated_or_comprehension(ResBody,Op,Vars,NewOutsideOfScope,NewInScope,_,ISCSP,Span),
713		(true %DC = true always lift out so that states are ground and that we need no variant/instance checks !
714		-> gensym('@',GSF), debug_println(5,generating_agent_for_repOp(F,GSF, ResBody)),
715		string_concatenate(F,GSF,PrefixName),
716		Call =.. [PrefixName|XARGS],
717		Res = agent_call(Span,PrefixName,XARGS), % use Span ?? or no_loc_info_available
718		% portray_clause( replicated(Call,ResBody) ),
719		assert_agent(Call, ResBody, unknown_span),
720		functor(Call,CF,CN), functor(CallSkel,CF,CN),
721		(ISCSP=true -> assert( is_csp_process(CallSkel) ) ; true)
722		; Res = ResBody
723		).
724		compile_body(let(LIST,Body),F,XARGS,DEFS,DC,Res) :- !, %print(let(LIST)),nl,
725		expand_let_definitions(LIST,ExpLIST), %print(extracting(ExpLIST)),nl,
726		extract_new_funs_from_lets(ExpLIST,F,XARGS,[],LetDefs),
727		append(LetDefs,DEFS,NDEFS),
728		debug_println(5,new_funs(NDEFS)),
729		compile_lets(ExpLIST,F,XARGS,NDEFS,DC),
730		debug_println(5,nested_let_compile(Body,NDEFS)),
731		compile_body(Body,F,XARGS,NDEFS,DC,Res). % check builtin calls in let declarations list
732		compile_body(builtin_call(X),F,XARGS,DEFS,DC,Res) :- !,
733		translate_builtin_call(X,TX),
734		%(translate_builtin_call(X,TX) -> true ; TX=X),
735		compile_body(TX,F,XARGS,DEFS,DC,Res).
736		compile_body([H|T],F,XARGS,DEFS,DC,Res) :- !, l_compile_body([H|T],F,XARGS,DEFS,DC,Res).
737		compile_body(FunName,_F,_XARGS,DEFS,_DC,Res) :- atomic(FunName),
738		%(FunName=getPrio -> print(compile(FunName,DEFS)),nl ; true),
739		is_local_let2(FunName,OriginalArity,[],DEFS,NewF,_,LLXARGS) ,!, %% append(LLXARGS,_,_XARGS) ??
740		%print(replacing(FunName,NewF,LLXARGS)),nl,
741		% We have a local function whose function name is used: replace by a lambda closure which hides
742		% the additional parameters required to call the lifted version NewF
743		length(OrigArgs,OriginalArity),
744		mynumbervars(OrigArgs),
745		(LLXARGS=[]
746		-> Res = NewF
747		; (append(OrigArgs,LLXARGS,FullArgs),
748		haskell_csp:get_symbol_span(FunName,Span),
749		Res = lambda(OrigArgs,agent_call(Span,NewF,FullArgs))
750		% ,print(generated(Res)),nl
751		)
752		). %% ,print(res(Res)),nl.
753		compile_body(NV,F,XARGS,DEFS,DC,Res) :- nonvar(NV), NV=..[FN|Args], !, /* TO DO: IMPROVE ! */
754		l_compile_body(Args,F,XARGS,DEFS,DC,ResArgs),
755		Res =.. [FN|ResArgs] %%,print(compiled(NV,Res)),nl
756		.
757		compile_body(X,_F,_X,_D,_DC,X).
758
759		l_compile_body([],_F,_XARGS,_DEFS,_DC,[]).
760		l_compile_body([H|T],F,XARGS,DEFS,DC,[RH|RT]) :-
761		%print(compiling(H)),nl,
762		compile_body(H,F,XARGS,DEFS,DC,RH), %print(finished(H)), nl,
763		add_new_parameters(H,XARGS,NewXARGS), %print(newargs(NewXARGS,H)),nl,
764		l_compile_body(T,F,NewXARGS,DEFS,DC,RT).
765
766		% check whether we have to add parameters of the body to calls to the right
767		add_new_parameters(X,Vars,NewVars) :- var(X),!,Vars=NewVars.
768		add_new_parameters(comprehensionGenerator(VAR,_SET),Vars,NewVars) :- !,
769		(var(VAR) -> NewVars=[VAR|Vars]
770		; %nl,print(comprehensionGenerator(VAR,_SET)),nl,
771		NewVars=Vars)
772		. %, check_var(VAR,_SET).
773		add_new_parameters(_,V,V).
774
775		:- public check_var/2.
776		:- block check_var(-,?).
777		check_var(V,SET) :- nl, print(not_var(V)),nl,print(SET),nl.
778
779		% give some of CSP's operators are more distinctive name
780		translate_builtin_call(set(X),R) :- !, R=seq_to_set(X).
781		translate_builtin_call(seq(X),R) :- !, R=set_to_seq(X).
782		translate_builtin_call(X,X).
783
784		assert_agent(Head,Body,Span) :-
785		compile_head(Head,NewHead,Constraints,Span),
786		assert_agent_compiled_head(NewHead,Body,Span,Constraints).
787
788		assert_agent_compiled_head(Head,OrigBody,Span,Constr) :-
789		(preferences:get_preference(cspm_strip_source_location,true)
790		-> clear_span(OrigBody,Body) %,print(clear_span(Res,CRes)),nl
791		; Body=OrigBody),
792		lift(Head,LHead,(Body,Constr),(LBody,LConstr)),
793		assert((agent_compiled(LHead,LBody,Span) :- LConstr)),
794		LHead =.. [Functor|Args],
795		length(Args,Arity),
796		compute_lazy_strict_types(Args,TL),
797		(retract(agent_parameters(Functor,Arity,OldTL))
798		-> merge_lazy_strict_types(TL,OldTL,NewTL) ; NewTL = TL ),
799		%% print(agent_parameters(Functor,Arity,NewTL)),nl,
800		assert(agent_parameters(Functor,Arity,NewTL)),
801		(agent_functor(Functor,Arity) -> true ; assert(agent_functor(Functor,Arity))).
802
803		compute_lazy_strict_types([],[]).
804		compute_lazy_strict_types([H|T],[HT|TT]) :-
805		(var(H) -> HT=lazy ; HT=strict),
806		compute_lazy_strict_types(T,TT).
807		merge_lazy_strict_types([],[],[]).
808		merge_lazy_strict_types([H1|T1],[H2|T2],[HH|TT]) :-
809		(H1=strict -> HH=strict ; HH=H2),
810		merge_lazy_strict_types(T1,T2,TT).
811
812		:- assert_must_succeed( (X=p('$VAR'(1),R,f('$VAR'(1),'$VAR'(2))),haskell_csp_analyzer:lift(X,R,true,true),
813		R=X) ).
814
815		/* lift all the variables which have been numbervar'd in the head to real variables */
816		lift(Head,LiftedHead,Body,LiftedBody) :-
817		lift2(Head,LiftedHead,[],VL,true),
818		lift2(Body,LiftedBody,VL,_,false). /* do not lift $VARs inside Body which are not in head */
819
820		lift2(X,R,VL,AVL,_INS) :- (var(X); atomic(X)),!,R=X, VL=AVL.
821		lift2('$VAR'(X),R,VarList,RVL,INS) :- !,lookup_insert(VarList,X,R,RVL,INS).
822		lift2(lambda(Args,Body),ResTerm,VarList,RVL,false) :- !,
823		ResTerm = lambda(Args,LiftedBody), RVL = VarList,
824		lift2(Args,_LiftedArgs,[],LambdaVARs,true),
825		list_difference(VarList,LambdaVARs,InnerVarList), % do not lift local $VARS (which hide outer $VAR)
826		lift2(Body,LiftedBody,InnerVarList,_,false).
827		% ,print(lifted_lambda(Args,Body,ResTerm)),nl.
828		lift2(Term,ResTerm,VarList,RVL,INS) :-
829		Term =.. [Functor|Args],
830		l_lift2(Args,RArgs,VarList,RVL,INS),
831		ResTerm =.. [Functor|RArgs].
832
833		% TO DO: check if we need to treat lambda's here: what if a lambda by accident has as
834		% its local variable a $VAR which is currently being lifted !!
835
836
837		l_lift2([],[],V,V,_INS).
838		l_lift2([H|T],[LH|LT],Vin,Vout,INS) :-
839		lift2(H,LH,Vin,V2,INS),
840		l_lift2(T,LT,V2,Vout,INS).
841
842		lookup_insert([],X,R,[X/R],INSERT) :-
843		(INSERT=true -> true %Vout = [X/R]
844		; %Vout=[],
845		R='$VAR'(X)).
846		lookup_insert([K/V|T],X,R,[K/V|RT],INS) :-
847		(K==X
848		-> V=R,T=RT
849		; lookup_insert(T,X,R,RT,INS)
850		).
851
852		%translate_builtin_call(set(X),set_to_seq(X)).
853
854		replicatedOperator(repChoice(Generators,Body,Span),repChoice,Vars,Generators,Body,false,Span) :-
855		/* false -> Body is not in a dangerous context (even if repChoice itself is in
856		a dangerous context) */
857		extract_variables_from_generator_list(Generators,Vars). /* should the generators be put together with Body ?? */
858		replicatedOperator(repInternalChoice(Generators,Body,Span),repInternalChoice,Vars,Generators,Body,false,Span) :-
859		extract_variables_from_generator_list(Generators,Vars).
860		replicatedOperator(repInterleave(Generators,Body,Span),repInterleave,Vars,Generators,Body,true,Span) :-
861		extract_variables_from_generator_list(Generators,Vars).
862		replicatedOperator(repSequence(Generators,Body,Span),repSequence,Vars,Generators,Body,true,Span) :-
863		extract_variables_from_generator_list(Generators,Vars).
864		replicatedOperator(procRepAParallel(Generators,pair(Sync,Body),Span),procRepAParallel,Vars,Generators,[Sync,Body],true,Span) :-
865		%print(repA(Generators)),nl,
866		extract_variables_from_generator_list(Generators,Vars).
867		replicatedOperator(procRepLinkParallel(Sync,Generators,Body,Span),procRepLinkParallel,Vars,[Generators,Sync],Body,true,Span) :-
868		extract_variables_from_generator_list(Generators,Vars).
869		replicatedOperator(procRepSharing(Sync,Generators,Body,Span),procRepSharing,Vars,[Generators,Sync],Body,true,Span) :-
870		extract_variables_from_generator_list(Generators,Vars).
871		/* last arg == true ->means-> dangerous as several branches active simultaneously -> local variables need
872		to be extracted*/
873
874		% replicated_or_comprehension(EXPR, OperatorAsAtom, Variables,
875		% Term(s)OutsideOfReplicatedVariablesScope (possibly defining new ones),
876		% TermInScopeofVariables, Replicated_true/false, Span)
877		replicated_or_comprehension(X,Op,Vars,Set,CSP,NewDC,true,Span) :-
878		replicatedOperator(X,Op,Vars,Set,CSP,NewDC,Span).
879		replicated_or_comprehension(X,Op,Vars,OutsideOfScope,InScope,NewDC,false,no_loc_info_available) :-
880		comprehension_aux(X,Op,Vars,OutsideOfScope,InScope), NewDC=true.
881
882		comprehension_aux(listExp(rangeEnum(Tuples),Generators),listComp, Vars , Generators, InScope) :-
883		InScope = Tuples,
884		extract_variables_from_generator_list(Generators,Vars).
885		comprehension_aux(setExp(rangeEnum(Tuples),Generators), setComp, Vars , Generators, InScope) :-
886		InScope = Tuples,
887		extract_variables_from_generator_list(Generators,Vars).
888		% TO DO: other setExp patterns !
889		comprehension_aux(procRenamingComp(A,Generators,RenameList),procRenamingComp,Vars,OutsideOfScope,InScope) :-
890		OutsideOfScope = [A|Generators],
891		InScope = RenameList,
892		extract_variables_from_generator_list(Generators,Vars).
893
894		l_compile_channel_value([],_F,XA,_DEFS,Res,XA,_Span) :- !, Res = [].
895		l_compile_channel_value([H|T],F,XA,DEFS,Res,NewXA,Span) :- !,
896		compile_channel_value(H,F,XA,DEFS,ResH,XA1,Span), append(ResH,ResT,Res),
897		l_compile_channel_value(T,F,XA1,DEFS,ResT,NewXA,Span).
898		l_compile_channel_value(E,F,XA,_,R,NXA,Span) :-
899		add_internal_error(haskell_csp_analyzer,'Unkown channel value list: ',(E,F),Span), R=E,NXA=XA.
900
901
902		compile_channel_value(VAR,F,XA,_DEFS,Res,NXA,Span) :- var(VAR),!,
903		add_internal_error(compile_channel_value,'Variable as channel value: ',F,Span),NXA=XA, Res=[VAR].
904		compile_channel_value(out(Expr),F,XA,DEFS,Res,NXA,_Span) :- !,
905		Res=[out(CE)],NXA=XA,compile_body(Expr,F,XA,DEFS,CE).
906		compile_channel_value(dot(Expr),F,XA,DEFS,Res,NXA,_Span) :- !,
907		Res=[out(CE)],NXA=XA,compile_body(Expr,F,XA,DEFS,CE).
908		compile_channel_value(in(Expr),F,XA,DEFS,Res,NXA,Span) :- ground(Expr), !,
909		add_message(haskell_csp_analyzer,'CSP Warning: Channel input contains no variable: ',Expr,Span),
910		Res=[out(CE)],NXA=XA,compile_body(Expr,F,XA,DEFS,CE).
911		compile_channel_value(in(Expr),F,XA,DEFS,Res,NXA,Span) :-
912		compile_top_level_in_channel_value(Expr,F,XA,DEFS,Res,NXA,Span,warn),!.
913		compile_channel_value(inGuard(Var,Guard),F,XA,DEFS,Res,NXA,Span) :- Res = [inGuard(VarNew,NewGuard)],
914		compile_in_channel_value(Var,XA,VarRes,NXA,Span,warn),
915		%print(compile_inGuard(Var,Guard,Res)),nl,
916		VarRes=[in(VarNew)],!,
917		compile_body(Guard,F,XA,DEFS,NewGuard). % XA instead of NXA: the input value cannot be used in the set expression
918		compile_channel_value(E,F,XA,_,Res,NXA,Span) :-
919		add_internal_error(haskell_csp_analyzer,'Illegal channel value or guard: ',E:F,Span), Res=[E],NXA=XA.
920
921		compile_top_level_in_channel_value(Expr,F,XA,DEFS,Res,NXA,Span,_) :- % print(compile(Expr,XA,Res,NXA)),nl,
922		nonvar(Expr),Expr = dotpat(List),
923		List=[H|T], \+ is_csp_constructor(H),!, % we have a ?(x.y) --> treate like ?x?y
924		compile_top_level_in_channel_value(H,F,XA,DEFS,R1,NXA1,Span,nowarn),append(R1,R2,Res),
925		compile_top_level_in_channel_value(dotpat(T),F,NXA1,DEFS,R2,NXA,Span,nowarn).
926		% here we need a case for treating channel fields like a?P.x as a.P?x or a?x.P.y as a?x.P?y where P is a constructor
927		compile_top_level_in_channel_value(Expr,F,XA,DEFS,Res,NXA,Span,_) :-
928		nonvar(Expr),Expr = dotpat(List),
929		List = [H|T], nonvar(H),is_constructor(H,C,_Args),!, (length(T,1) -> T=[H1|_], LL = [out(C),in(H1)]; LL = [out(C),in(dotpat(T))]),
930		l_compile_channel_value(LL,F,XA,DEFS,Res,NXA,Span).
931		compile_top_level_in_channel_value(Expr,_F,XA,_DEFS,Res,NXA,_Span,_) :- % print(compile(Expr,XA,Res,NXA)),nl,
932		nonvar(Expr),Expr = dotpat(List),List=[],!, % we have a ?(x.y) --> treate like ?x.?y
933		Res = [],NXA=XA.
934		compile_top_level_in_channel_value(Expr,_F,XtraArgs,_DEFS,Res,NewXtraArgs,Span,WarnIfNoVariables) :-
935		compile_in_channel_value(Expr,XtraArgs,Res,NewXtraArgs,Span,WarnIfNoVariables).
936
937		compile_in_channel_value(Expr,XA,[ResTerm],NXA,Span,Warn) :- !,
938		add_extra_input_variable(Expr,XA,NXA,Res,Span),
939		(XA==NXA ->
940		%add_error(haskell_csp_analyzer,'Channel input contains no variable: ',Expr,Span)
941		(Warn=nowarn -> true
942		; add_message(haskell_csp_analyzer,'CSP Warning: Channel input contains no variable: ',Expr,Span)),
943		ResTerm = out(Res)
944		; ResTerm=in(Res)).
945
946		% add_extra_input_variable(InputVariableTerm, ExtraLocalVariablesSoFar,
947		% NewExtraLocalVariablesAfter, ResTransformedInputVariableTerm, Span)
948
949		% Note: expression wrapped in in(.) can contain variables; they can thus not
950		% yet be fully evaluated (mainly due to the CSP dot constructor)
951
952		:- public blocking_append/3. % returned as constraint for pattern match
953		:- block blocking_append(?,?,-).
954		blocking_append(L1,L2,L3) :- append(L1,L2,L3).
955
956		add_extra_input_variable(Var,XA,NXA,Res,Span) :- %print(add(Var,XA,NXA)),nl,
957		var(Var),!,
958		(exact_member(Var,XA) %% case will be catched from the CSP-M parser (e.g. c?x?x => Error message: Redefinition of x)
959		-> (add_internal_error(haskell_csp_analyzer,'Internal Error: Channel input variable already used: ',Var,Span),NXA=XA)
960		; NXA=[Var|XA]
961		),Res=Var.
962		add_extra_input_variable(listPat(List),XA,NXA,Res,Span) :- !, Res = list(RList),
963		add_extra_input_variables(List,XA,NXA,RList,Span).
964		add_extra_input_variable(singleSetPat(List),XA,NXA,Res,Span) :- !, Res = setValue(RList),
965		add_extra_input_variables(List,XA,NXA,RList,Span).
966		add_extra_input_variable(tuplePat(List),XA,NXA,Res,Span) :- !, Res = na_tuple(RList),
967		add_extra_input_variables(List,XA,NXA,RList,Span).
968		add_extra_input_variable(dotpat(List),XA,NXA,Res,Span) :- !, Res = dotTuple(RList),
969		/* dotTuple or dotpat because it still needs to be evaluated */
970		/* TODO: CHECK if we don't have to detect records here ?? */
971		add_extra_input_tuple_variables(List,XA,NXA,RList,Span).
972		add_extra_input_variable(alsoPattern([X,Y]),XA,NXA,Res,Span) :- !, Res = alsoPat(RX,RY),
973		add_extra_input_variable(X,XA,NXX,RX,Span),
974		add_extra_input_variable(Y,XA,NXY,RY,Span), append(NXX,NXY,NXA). % was NXA=NXX.
975		add_extra_input_variable(appendPattern(List),_XA,_NXA,Res,Span) :- !,
976		compile_append_pat(appendPattern(List),LRes,Constr),
977		get_append_agent_result('AppPatFun',LRes,Constr,Res,Span).
978		add_extra_input_variable(Expr,XA,NXA,Res,_Span) :-
979		(Expr = int(_); valid_constant(Expr)),!, XA=NXA, Res=Expr.
980		add_extra_input_variable(Expr,XA,NXA,Res,Span) :-
981		add_error(haskell_csp_analyzer,'Channel input not recognized: ',Expr,Span),
982		NXA=XA, Res=Expr.
983		% TODO: check if other patterns can appear here,...
984
985		get_append_agent_result(FunName,VarExpr,Constr,Res,Span) :-
986		gensym(FunName,NewFun),
987		%functor(Head,NewFun,1),arg(1,Head,VarExpr),
988		Head =.. [NewFun|[VarExpr]],
989		Res = appendPat(VarExpr,Head),
990		assert_agent_compiled_head(Head,VarExpr,Span,Constr). %,print(assert_agent_compiled_head(Head,VarExpr,Span,Constr)),nl.
991
992		compile_append_pat(appendPattern([Pat1]),NewPara,Constraint1) :- !,
993		compile_head_para(Pat1,NewPara,Constraint1,_Head,_Span).
994		compile_append_pat(appendPattern([H|T]),NewPara,ConstraintsT) :-
995		nonvar(H), H=listPat(HList),is_list_skeleton(HList),!,
996		NewPara = list(NewList),
997		compile_append_pat(appendPattern(T),NewT,ConstraintsT),
998		NewT = list(TList), append(HList,TList,NewList).
999		compile_append_pat(appendPattern(Pat),NewPara,Constraint) :-
1000		is_list_skeleton(Pat),
1001		append(T,[H],Pat),
1002		nonvar(H), H=listPat(HList),is_list_skeleton(HList),!,
1003		compile_append_pat(appendPattern(T),NewT,_ConstraintsT),
1004		NewPara = list(NewList), NewT = list(TList),
1005		Constraint=blocking_append(TList,HList,NewList).
1006		compile_append_pat(Pat,_NewPara,_Constraint) :-
1007		add_internal_error('Internal Error: Expected append pattern instead of ', Pat),fail.
1008
1009		add_extra_input_tuple_variable(Expr,XA,NXA,Res,_Span) :- % allow record constructors
1010		%print(addi(Expr)),nl,
1011		nonvar(Expr), is_csp_constructor(Expr),!, XA=NXA, Res=Expr. % TO DO: should we check the args ?!
1012		add_extra_input_tuple_variable(Expr,XA,NXA,Res,Span) :- add_extra_input_variable(Expr,XA,NXA,Res,Span).
1013
1014		add_extra_input_tuple_variables([],XA,XA,[],_).
1015		add_extra_input_tuple_variables([V|T],XA,NXA,[CV|CT],Span) :-
1016		add_extra_input_tuple_variable(V,XA,XA1,CV,Span),
1017		add_extra_input_tuple_variables(T,XA1,NXA,CT,Span).
1018
1019		add_extra_input_variables([],XA,XA,[],_).
1020		add_extra_input_variables([V|T],XA,NXA,[CV|CT],Span) :-
1021		add_extra_input_variable(V,XA,XA1,CV,Span),
1022		add_extra_input_variables(T,XA1,NXA,CT,Span).
1023
1024		compile_lets([],_F,_XA,_D,_DC).
1025		compile_lets([L1|T],F,XA,D,DC) :-
1026		compile_let(L1,F,XA,D,DC), compile_lets(T,F,XA,D,DC).
1027
1028
1029		compile_let(agent_curry(Fun,Body,SRCSPAN),F,XARGS,DEFS,DC) :- !,
1030		translate_agent_curry(Fun,Body,TFun,TBody,SRCSPAN),
1031		compile_let(agent(TFun,TBody,SRCSPAN),F,XARGS,DEFS,DC).
1032		compile_let(agent(Fun,Body,SRCSPAN),F,XARGS,DEFS,DC) :-
1033		/* TO DO: treat multiple agent facts for same fun ;; DONE ?? */
1034		( is_local_let(Fun,DEFS,NewFun,_FXArgs,_)
1035		-> term_variables(Fun,ArgumentsToFun),
1036		append(XARGS,ArgumentsToFun,NewXARGS),
1037		debug_println(5,compile_within_let(Fun,NewXARGS)),
1038		compile_body(Body,F,NewXARGS,DEFS,DC,Res), /* one could pass NewF instead of F */
1039		% portray_clause( let_agent(NewFun,Res) ),
1040		assert_agent(NewFun,Res,SRCSPAN)
1041		%print(assert_agent(NewFun,Res,SRCSPAN)),nl
1042		; add_internal_error(haskell_csp,'Could not find let function in defs: ',(Fun,DEFS),SRCSPAN)
1043		).
1044
1045		:- meta_predicate findall_keepvars(-,0,-).
1046		expand_let_definitions(Lets,ExpLets) :- %print(expanding(Lets)),nl,
1047		findall_keepvars(EA, member_expand(Lets,EA), ExpLets). % important to use findall_keepvars instead of findall to avoid free variable (parameters of outer function) renaming apart
1048
1049		member_expand(Lets,EA) :- member(A,Lets),expand(A,EA).
1050
1051		/* a version of findall that does not rename apart unbound variables */
1052		findall_keepvars(V,Goal,SolList) :- term_variables(Goal,GVars), term_variables(V,VVars),
1053		remove_variables(GVars,VVars,Vars),
1054		findall( sol(V,Vars), Goal, ISol),
1055		% print(findall( sol(V,Vars), Goal, ISol)),nl,
1056		l_unify(ISol,Vars,SolList).
1057		l_unify([],_,[]).
1058		l_unify([sol(V,SVars)|T],Vars,[V|TT]) :-
1059		(SVars=Vars -> l_unify(T,Vars,TT)
1060		; add_internal_error('Variable Binding Clash in l_unify: ',l_unify([sol(V,SVars)|T],Vars,[V|TT])),
1061		fail).
1062
1063		expand(bindval(Fun,Body,Span),R) :- !,expand(agent(Fun,Body,Span),R).
1064		expand(agent(Fun,Body,Span),R) :- !, R = agent(EFun,EBody,Span),
1065		if(expand_agent(Fun,Body,outer,Span,EFun,EBody),
1066		true, %(print(expanded_agent(R)),nl),
1067		(add_internal_error(expand_agent,'Expand agent failed: ',agent(Fun,Body),Span),fail)).
1068		expand(X,X).
1069
1070		% expand definitions such as (p1,p2,p3) = c into three definitions of agent
1071		%expand_agent(F,B,_,_,_FF,_BB) :- print(ea(F,B,_FF,_BB)),nl,fail.
1072		expand_agent(Var,_Body,_,_,_RV,_RB) :- var(Var),!,fail. /* we have a variable; we assume this combes from a Wildcard _ underscore !!! example let (_,a) = Body .... */
1073		/* the wildcard value is thrown away: we do not need to compute this projection */ %RV=Var,RB=Body.
1074		expand_agent('tuplePat'(Pat),Body, _,Span,Fun, ExpandedBody) :- !,
1075		nth1(Nr,Pat,Head),
1076		expand_agent(Head,na_tuple_projection(int(Nr),Body,Span),inner,Span,Fun,ExpandedBody).
1077		%,print(expanded(Fun,ExpandedBody)),nl.
1078		expand_agent(dotpat(Pat),Body, _,Span,Fun, ExpandedBody) :- !,
1079		nth1(Nr,Pat,Head),
1080		expand_agent(Head,tuple_projection(int(Nr),Body,Span),inner,Span,Fun,ExpandedBody).
1081		expand_agent(singleSetPat([Pat]),Body, _,Span,Fun, ExpandedBody) :- !,
1082		expand_agent(Pat,singleSetPatValue(Body,Span),inner,Span,Fun,ExpandedBody).
1083		expand_agent(listPat(Pat),Body, _,Span,Fun, ExpandedBody) :- !,
1084		nth1(Nr,Pat,Head), length(Pat,Len),
1085		expand_agent(Head,list_projection(int(Nr),int(Len),Body,Span),inner,Span,Fun,ExpandedBody).
1086		% TO DO: add more patterns
1087		% TO DO: generate error if pattern contains constructs not yet translated
1088		expand_agent(Fun,Body,inner,Span,FunR,BodyR) :- !,
1089		((atomic(Fun), \+ number(Fun)) -> FunR=Fun, BodyR=Body
1090		; add_error(expand_agent,'Cannot treat expression in LHS of let (use fresh variable): ',Fun,Span),fail).
1091		expand_agent(Fun,Body,_,_,Fun,Body). %% check if Fun is atomic ??
1092
1093
1094
1095		extract_new_funs_from_lets([],_F,_XA,D,D).
1096		extract_new_funs_from_lets([L1|T],F,XA,D,ND) :-
1097		extract_new_funs_from_let(L1,F,XA,D,ND1),
1098		extract_new_funs_from_lets(T,F,XA,ND1,ND).
1099
1100		extract_new_funs_from_let(bindval(Fun,Body,SRCSPAN),F,XARGS,DEFS, NewDEFS) :- !,
1101		extract_new_funs_from_let(agent(Fun,Body,SRCSPAN),F,XARGS,DEFS, NewDEFS).
1102		extract_new_funs_from_let(agent_curry(Fun,Body,SRCSPAN),F,XARGS,DEFS, NewDEFS) :- !,
1103		translate_agent_curry(Fun,Body,TFun,TBody,SRCSPAN),
1104		extract_new_funs_from_let(agent(TFun,TBody,SRCSPAN),F,XARGS,DEFS, NewDEFS).
1105		extract_new_funs_from_let(agent(Fun,_Body,_SRCSPAN),F,XARGS,DEFS, NewDEFS) :-
1106		%Fun=.. [FunF|_FunArgs],
1107		functor(Fun,FunF,Arity),
1108		(builtin_functor(FunF,Arity)
1109		-> add_error(extract_new_funs_from_let,'Not a user-definable function:',FunF/Arity,_SRSCPAN),
1110		NewF = FunF
1111		; (is_local_let(Fun,DEFS,_,_,NewF)
1112		-> %print(multiple_equations_for(F,Fun,SRCSPAN,NewF)),nl,
1113		assert(multiple_let_equations_for(NewF,Fun))
1114		; gensym(FunF,FunFGS),
1115		string_concatenate('*',FunFGS,P2),
1116		string_concatenate(F,P2,NewF) /* This is not really required: but makes it more readable?? */
1117		)
1118		),
1119		debug_println(5,rename_let(FunF,NewF,XARGS)),
1120		NewDEFS = [ local_let(FunF,Arity, NewF,XARGS) | DEFS].
1121		% commented out: is_possible_csp_process is computed by analyze_recursively_possible ????
1122		% functor(NewFun,CF,CN), functor(CallSkel,CF,CN).
1123		% (is_possible_csp_process(CallSkel) -> true
1124		% ; assert( is_possible_csp_process(CallSkel) ) ).
1125
1126
1127
1128
1129		builtin_functor('tuplePat',1).
1130		builtin_functor(dotpat,1).
1131		builtin_functor(Nr,0) :- number(Nr).
1132		% TO DO: add more cases
1133
1134
1135
1136		/* lookup if agent is a locally defined one and if so return the new call */
1137		is_local_let(X,DEFS,Res,XARGS,NewF) :- % print(check_is_local_let(X,DEFS,Res)),nl,
1138		functor(X,F,Arity),
1139		member(local_let(F,Arity,NewF,XARGS),DEFS),
1140		X =.. [_|Args],
1141		append(Args,XARGS,NA),
1142		Res =.. [NewF|NA].%, print(res(Res)),nl.
1143
1144		% same as above but with functor and args treated seperately
1145		is_local_let2(Fun,OldArity,Args,DEFS,NewF,NA,XARGS) :- % print(check_is_local_let(X,DEFS,Res)),nl,
1146		member(local_let(Fun,OldArity,NewF,XARGS),DEFS),
1147		append(Args,XARGS,NA). %, print(res(Res)),nl.
1148
1149
1150		:- dynamic cur_numbervars_index/1.
1151		cur_numbervars_index(0).
1152
1153		reset_cur_numbervars_index :- retractall(cur_numbervars_index(_)),
1154		assert(cur_numbervars_index(0)).
1155		mynumbervars(Term) :-
1156		cur_numbervars_index(Idx),
1157		numbervars(Term,Idx,NewIdx),
1158		retract(cur_numbervars_index(Idx)),
1159		assert(cur_numbervars_index(NewIdx)).
1160
1161		% ------------------------------------------
1162
1163
1164		csp_span(no_loc_info_available).
1165		csp_span(src_span(_,_,_,_,_,_)).
1166		csp_span(src_position(_,_,_,_)).
1167		csp_span(span_info(_,_)).
1168		csp_span(multi_span(_,_,_,_,_,_,_)).
1169		csp_span(src_span_operator(_,_)).
1170
1171		% visited_expression(ID,E), haskell_csp:clear_span(E,CE), visited_expression(ID2,E2), ID2@>ID, haskell_csp:clear_span(E2,CE).
1172		clear_span(X,R) :- var(X),!,R=X.
1173		clear_span('|~|'(X,Y,SrcSpan),R) :- R='|~|'(CX,CY,SrcSpan),
1174		% keep span for internal choice; it is currently being used for tau-priority partial order reduction
1175		clear_span(X,CX), clear_span(Y,CY).
1176		%clear_span(prefix(Span,NewVals,NewChExpr,X,_),R) :- !,
1177		% R=prefix(Span,NewVals,NewChExpr,CX,no_loc_info_available),
1178		% clear_span(X,CX).
1179		clear_span(X,R) :- csp_span(X),!,R=no_loc_info_available.
1180		clear_span(X,R) :- atomic(X),!,R=X.
1181		clear_span(X,R) :- X=..[F|A], maplist(clear_span,A,CA), R=..[F|CA].
1182
1183		% ------------------------------------------
1184
1185		opt_csp_listing :- debug_level(L), (L<5 -> csp_listing ; true).
1186
1187		csp_listing :-
1188		nl,
1189		agent_compiled_without_constraints(Head,Body,_Span),
1190		portray_clause((Head :- Body)),
1191		functor(Head,F,A),
1192		(agent_parameters(F,A,List)
1193		-> (List=[] -> true ; (print(' /* '), print(List), print('*/')))
1194		; print(' **** NO agent_parameter fact ! ****')
1195		),nl,
1196		fail.
1197		csp_listing.
1198
1199		get_internal_csp_representation(CodesClauses) :-
1200		findall(Clause, csp_clause(Clause), CL), append(CL,CodesClauses).
1201
1202		csp_clause(Clause) :- channel_type_list(C,T),
1203		format_to_codes('~q.~N',[channel_type_list(C,T)],Clause).
1204		csp_clause(Clause) :- name_type(C,T),
1205		format_to_codes('~q.~N',[name_type(C,T)],Clause).
1206		csp_clause(Clause) :-
1207		haskell_csp_analyzer:agent_compiled_with_constraints(Head,Body,_Span,Constr),
1208		functor(Head,F,A),
1209		(agent_parameters(F,A,List) -> true ; List = no_agent_parameter_fact),
1210		numbervars((Head,Body,Constr),0,_),
1211		%portray_clause((Head :- Body)),
1212		((List=[],Constr=true) -> format_to_codes('~q :-~N ~q.~N',[Head,Body],Clause)
1213		; List=[] -> format_to_codes('~q :- ~q, /* Constraints */~N ~q.~N',[Head,Constr,Body],Clause)
1214		; Constr\=true -> format_to_codes('~q :- /* ~p */~N ~q, /* Constraints */~N ~q.~N',[Head,List,Constr,Body],Clause)
1215		; format_to_codes('~q :- /* ~p */~N ~q.~N',[Head,List,Body],Clause)).