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