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)). |