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