1 | | % (c) 2009-2022 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 | | /* dotTuple: |
6 | | either associative tuples or if first argument constructor a record |
7 | | |
8 | | tuple: |
9 | | associative tuple; already computed; however tuples may be present inside |
10 | | in(.) patterns which have only been instantiated after tuple was computed |
11 | | |
12 | | record: |
13 | | record; already constructed |
14 | | |
15 | | % pat(Vals,Channel): |
16 | | % associative tuple; constructed for a particular channel |
17 | | */ |
18 | | |
19 | | :- module(csp_tuples,[get_constructor_arguments/4, evaluate_channel_outputs/6, |
20 | | evaluate_dot_tuple/3, evaluate_dot_tuple/2, is_constructor/3, unify_values/5, |
21 | | list_projection/5, tuple_projection/4,incomplete_record/3,pattern_match_function_argument/3, |
22 | | na_tuple_projection/4, empty_tuple/1 |
23 | | ]). |
24 | | :- use_module(probsrc(module_information)). |
25 | | :- module_info(group,csp). |
26 | | :- module_info(description,'Operations on CSP tuples.'). |
27 | | |
28 | | :- use_module(library(lists)). |
29 | | |
30 | | /***************** PROB modules ***************/ |
31 | | :- use_module(probsrc(self_check)). |
32 | | :- use_module(probsrc(debug)). |
33 | | :- use_module(probsrc(error_manager)). |
34 | | %--------- CSP modules: |
35 | | :- use_module(probcspsrc(haskell_csp), |
36 | | [force_evaluate_argument/2, |
37 | | evaluate_argument/2,add_error_with_span/4, add_internal_error_with_span/4]). |
38 | | :- use_module(probcspsrc(haskell_csp_analyzer), |
39 | | [is_csp_constructor/1, is_a_channel_name/1, csp_full_type_constructor/3]). |
40 | | :- use_module(probcspsrc(csp_sets),[is_member_set_alsoPat/2]). |
41 | | /***************** ----------- ***************/ |
42 | | |
43 | | empty_tuple(tuple([])). |
44 | | |
45 | | %:- assert_must_succeed(( csp_tuples:evaluate_channel_outputs([in(X)],left,R,RC), R==tail_in(X), RC==left )). |
46 | | |
47 | | evaluate_channel_outputs(Values,ChannelExpr,EvaluatedValueList,Channel,Span,WF) :- |
48 | | % print(ev_channel(ChannelExpr,Values)),nl, |
49 | ? | evaluate_dot_tuple([ChannelExpr|Values],Res,WF), % print(Res),nl, |
50 | | %print(evaluated_dot_tuple(dotTuple([ChannelExpr|Values]),Res)),nl, |
51 | | (Res = tuple([Ch|VL]) |
52 | | -> (EvaluatedValueList,Channel) = (VL,Ch) % if we unify VL without Ch we may get error messages ! |
53 | | ; add_error_with_span(evaluate_channel_outputs,'Not a channel pattern: ', (ChannelExpr,Res),Span),fail |
54 | | ), |
55 | ? | (is_a_channel_name(Channel) -> true |
56 | | ; add_error_with_span(evaluate_channel_outputs,'Channel not declared: ',Channel,Span) ). |
57 | | |
58 | | % ev_channel(dotTuple([gen_high_pri,valarg]),[in(_6892)]) tuple([gen_high_pri,record(valarg,[]),in(_6892)]) |
59 | | |
60 | | % ------------------------------------------------------------ |
61 | | |
62 | | |
63 | | :- assert_must_succeed(( |
64 | | csp_tuples:evaluate_dot_tuple([X,int(2)],R), |
65 | | X = int(1), |
66 | | R == tuple([int(1),int(2)]) )). |
67 | | :- assert_must_succeed((csp_tuples: evaluate_dot_tuple([],R), R == tuple([]))). |
68 | | |
69 | | evaluate_dot_tuple(List,Res) :- |
70 | | evaluate_dot_tuple(List,Res,_WF). %_WF not needed as inGuard cannot appear in normal tuples |
71 | | |
72 | | :- block evaluate_dot_tuple(-,?,?). |
73 | ? | evaluate_dot_tuple(L,Res,WF) :- evaluate_dot_tuple_to_list(L,R,WF),construct_tuple(R,Res). |
74 | | |
75 | | % construct a tuple from a list of evaluated arguments: we need to check if we have a real |
76 | | % tuple or "just" a single record constructed using . |
77 | | :- block construct_tuple(-,?). |
78 | | construct_tuple([],tuple([])). |
79 | ? | construct_tuple([H|T],R) :- construct_tuple2(H,T,R). |
80 | | :- block construct_tuple2(-,?,?), construct_tuple2(?,-,?). |
81 | | construct_tuple2(record(C,F),[],Res) :- !, Res= record(C,F). % this is not a dotTuple but a simple record |
82 | | construct_tuple2(H,T,tuple([H|T])). % we have a real associative tuple |
83 | | |
84 | | |
85 | | % evaluate a dot tuple list to a single list of its constituents |
86 | | :- block evaluate_dot_tuple_to_list(-,?,?). |
87 | | evaluate_dot_tuple_to_list([],R,_WF) :- !,R=[]. |
88 | ? | evaluate_dot_tuple_to_list([H|T],R,WF) :- !, evaluate_cons_to_list(H,T,R,WF). |
89 | | evaluate_dot_tuple_to_list(X,R,_WF) :- add_internal_error('Internal Error: Could not evaluate dotTuple List: ',X),R=X. |
90 | | |
91 | | :- block evaluate_cons_to_list(-,?,?,?). |
92 | | evaluate_cons_to_list(dotTuple(L),T,R,WF) :- !, |
93 | ? | append(L,T,LT), evaluate_dot_tuple_to_list(LT,R,WF). |
94 | | evaluate_cons_to_list(tuple(L),T,R,WF) :- !, |
95 | | append(L,T,LT), evaluate_dot_tuple_to_list(LT,R,WF). |
96 | | evaluate_cons_to_list(tupleExp(L),T,R,WF) :- !, |
97 | | haskell_csp: evaluate_argument2(tupleExp(L),Res), |
98 | | evaluate_dot_tuple_to_list(T,LT,WF), |
99 | | append([Res],LT,R). |
100 | ? | evaluate_cons_to_list(X,T,R,WF) :- is_constructor(X,Constructor,SubTypes),!, |
101 | | % print(constructor(Constructor,SubTypes)),nl, |
102 | | evaluate_dot_tuple_to_list(T,ET,WF), %print(evalt(ET)),nl, |
103 | | get_constructor_arguments(SubTypes,ET,Fields,Rest), |
104 | | R=[record(Constructor,Fields)|Rest]. |
105 | ? | evaluate_cons_to_list(H,T,R,WF) :- !, evaluate_dot_argument(H,EH,WF), |
106 | ? | evaluate_cons_to_list_evhead(EH,T,R,WF). |
107 | | |
108 | | % a version where the head is already evaluated; do not evaluate again |
109 | | % this cannot be a constructor (right ?? ---> check ) |
110 | | :- block evaluate_cons_to_list_evhead(-,?,?,?). |
111 | | %evaluate_cons_to_list_evhead(pat(L,Ch),T,R,WF) :- !, R = pat(R3,Ch),append(L,R2,R3), |
112 | | % evaluate_dot_tuple_to_list(T,R2,WF). |
113 | | evaluate_cons_to_list_evhead(tuple(L),T,R,WF) :- !, append(L,R2,R), |
114 | ? | evaluate_dot_tuple_to_list(T,R2,WF). |
115 | | evaluate_cons_to_list_evhead(REC,T,R,WF) :- |
116 | | incomplete_record(REC,MissingFields,FullREC),!, |
117 | | %print(eval_cons_record(REC,MissingFields,FullREC)),nl, |
118 | | evaluate_dot_tuple_to_list(T,ET,WF), %print(evalt(ET)),nl, |
119 | | get_constructor_arguments(MissingFields,ET,MissingFields,Rest), |
120 | | %print(full_rec(FullREC,Rest)),nl, |
121 | | R=[FullREC|Rest]. |
122 | | evaluate_cons_to_list_evhead(EH,T,R,WF) :- R=[EH|ET], evaluate_dot_tuple_to_list(T,ET,WF). |
123 | | |
124 | | % check if we have an incomplete record, or a record whose last element is incomplete .... |
125 | | incomplete_record(record(X,Fields), MissingFields, record(Constructor,FullFields)) :- |
126 | | is_constructor(X,Constructor,SubTypes), |
127 | | get_missing_fields(Fields,SubTypes,MissingFields,FullFields). |
128 | | |
129 | | get_missing_fields([],[H|T],MissingFields,MissingFields) :- same_length([H|T],MissingFields). |
130 | | get_missing_fields([Rec],[_TH],MissingFields,[FullRec]) :- % we could have incomplete record at end |
131 | | incomplete_record(Rec,MissingFields,FullRec),!. |
132 | | get_missing_fields([FH|FT],[_TH|TT],MF,[FH|FFT]) :- get_missing_fields(FT,TT,MF,FFT). |
133 | | |
134 | | |
135 | | |
136 | | is_constructor(out(Constructor),Constructor,ArgSubTypes) :- atomic(Constructor), |
137 | | csp_full_type_constructor(Constructor,_Type,ArgSubTypes). |
138 | | is_constructor(Constructor,Constructor,ArgSubTypes) :- atomic(Constructor), |
139 | | csp_full_type_constructor(Constructor,_Type,ArgSubTypes). |
140 | | |
141 | | /* some special constructs are allowed in the presence of channel dot tuples: */ |
142 | | :- block evaluate_dot_argument(-,?,?). |
143 | | |
144 | | evaluate_dot_argument(out(X),R,_) :- !, force_evaluate_argument(X,R). |
145 | | evaluate_dot_argument(in(X),R,_) :- !, R=in(X). |
146 | | evaluate_dot_argument(inGuard(X,Set),R,WF) :- !, R = in(X), |
147 | | %print(check_guard(X,Set)),nl, |
148 | ? | check_guard(X,Set,WF). |
149 | ? | evaluate_dot_argument(H,EH,_) :- force_evaluate_argument(H,EH). %%% was evaluate_argument |
150 | | |
151 | | |
152 | | :- use_module(probsrc(kernel_waitflags)). |
153 | | :- use_module(probcspsrc(csp_sets),[try_get_cardinality_for_wait_flag/2]). |
154 | | check_guard(Var,Guard,WF) :- %print(check_guard(Var,Guard)),nl, |
155 | | %(is_boolean_expression(Guard) -> check_boolean_expression(Guard) /* syntax in CIA-CSP but actually not allowed in CSP-M ! */ |
156 | ? | haskell_csp:force_evaluate_argument_for_member_check(Guard,Set), |
157 | | /* already evaluate before Var is ground; avoid re-evaluation */ |
158 | | try_get_cardinality_for_wait_flag(Set,Prio), |
159 | | get_wait_flag(Prio,check_guard,WF,LWF), |
160 | | % print(check_guard(Var,Guard,LWF)),nl, |
161 | | % TO DO: trigger earlier; Set must be a subset of the channel type; so we can always enumerate before full channel enumeration ! |
162 | | when((ground(Var);nonvar(LWF)),( % |
163 | | (ground(Var) -> evaluate_argument(Var,EVar) ; EVar=Var), % relevant for CorrectRouter.csp; TODO: investigate why |
164 | | %print(is_member_set(Var,Set)),nl, |
165 | | is_member_set_alsoPat(EVar,Set))). |
166 | | :- assert_must_succeed((csp_tuples: get_constructor_arguments([],[X,Y],[],Rest), Rest == [X,Y])). |
167 | | :- assert_must_fail((csp_tuples: get_constructor_arguments([dotTupleType([int(1),X,int(3)])],[int(1),X],Fields,Rest), |
168 | | Fields == [int(1),X], Rest == [int(3)])). |
169 | | :- assert_must_fail((csp_tuples: get_constructor_arguments([int(1),X,int(3)],[int(1),X],Fields,Rest), |
170 | | Fields == [int(1),X], Rest == [int(3)])). |
171 | | :- assert_must_succeed((csp_tuples: get_constructor_arguments([dotTupleType([int(1),int(2)])],[int(1),int(2),int(3)],Fields,Rest), |
172 | | Fields == [int(1),int(2)], Rest == [int(3)])). |
173 | | :- assert_must_succeed((csp_tuples: get_constructor_arguments([int(1),int(2)],[int(1),int(2),int(3)],Fields,Rest), |
174 | | Fields == [int(1),int(2)], Rest == [int(3)])). |
175 | | |
176 | | get_constructor_arguments([],T,[],T). |
177 | | get_constructor_arguments([H|T],DotArgs,Fields,R) :- nonvar(H), H = dotTupleType(L), !, append(L,T,LL), get_constructor_arguments(LL,DotArgs,Fields,R). |
178 | | get_constructor_arguments([_Type|TT],DotArgs,Fields,R) :- |
179 | | (DotArgs = [H|DT] |
180 | | -> Fields = [H|T], get_constructor_arguments(TT,DT,T,R) |
181 | | ; % Have removed preference: incomplete records also arise in renamings; hard to distinguish proper from improper use |
182 | | %(preferences:preference(cspm_allow_incomplete_records,true) -> true |
183 | | % ; length([_Type|TT],Len),add_error(csp_tuples,'Incomplete record / missing arguments for record constructor (set CSP preference to turn off this message): ',ConstructorT:missing_args(Len))), |
184 | | /* Casper generated CSP files will trigger this; as will renaming of record names ?! !! */ |
185 | | DotArgs=[], R = [], |
186 | | Fields = [] /* to do check if we can work with this */ |
187 | | ). |
188 | | |
189 | | |
190 | | % -------------------------------------------------------------------- |
191 | | |
192 | | :- assert_must_succeed(( |
193 | | csp_tuples:unify_values([int(1)],[in(X)],R,a), |
194 | | R == [int(1)], X==int(1) )). |
195 | | :- assert_must_succeed(( |
196 | | csp_tuples:unify_values([int(1),int(2)],[int(1),in(X)],R,a), |
197 | | R == [int(1),int(2)], X==int(2) )). |
198 | | :- assert_must_succeed(( |
199 | | csp_tuples:unify_values([int(1),int(2)],[in(X)],R,a), |
200 | | R == [int(1),int(2)], X==tuple(R) )). |
201 | | :- assert_must_succeed(( |
202 | | csp_tuples:unify_values([int(1),int(2)],[in(dotTuple([X,Y]))],R,a), |
203 | | R == [int(1),int(2)], X==int(1), Y==int(2) )). |
204 | | :- assert_must_succeed(( |
205 | | csp_tuples:unify_values([in(dotTuple([X,Y]))],[int(1),int(2)],R,a), |
206 | | R == [int(1),int(2)], X==int(1), Y==int(2) )). |
207 | | :- assert_must_succeed(( |
208 | | csp_tuples:unify_values([in(dotTuple([X,Y]))],V2,R,a), |
209 | | V2 = [int(1),int(2)], |
210 | | R == [int(1),int(2)], X==int(1), Y==int(2) )). |
211 | | :- assert_must_succeed(( |
212 | | csp_tuples:unify_values([int(1),in(Y),int(3)],[int(1),in(X)],R,a), |
213 | | R == [int(1),in(Y),int(3)], X==tuple([in(Y),int(3)]) )). |
214 | | :- assert_must_succeed(( |
215 | | csp_tuples:unify_values([oranges],LHS,R,a), LHS = [H], H=in(X), |
216 | | R == [oranges], X==oranges )). |
217 | | :- assert_must_succeed(( |
218 | | csp_tuples:unify_values(LHS,RHS,R,a), LHS = [H|T], H=in(X), T=[], |
219 | | RHS = [oranges|RR], RR=[], |
220 | | R == [oranges], X==oranges )). |
221 | | :- assert_must_succeed(( |
222 | | csp_tuples:unify_values(LHS,RHS,R,a), LHS = [in(X)], |
223 | | RHS = [oranges|RR], RR=[apples|RR2],RR2=[], |
224 | | R == [oranges,apples], X==tuple([oranges,apples]) )). |
225 | | :- assert_must_succeed(( |
226 | | csp_tuples:unify_values(LHS,RHS,R,a), LHS = [dotTuple(ppp,[na_tuple([X,Y])])], RHS = [dotTuple(ppp,[na_tuple([v1,v2])])], |
227 | | R =[dotTuple(ppp,[na_tuple([v1,v2])])],X=v1,Y=v2 )). |
228 | | :- assert_must_succeed(( |
229 | | csp_tuples:unify_values(LHS,RHS,R,a), LHS = [record(ppp,[na_tuple([X,Y])])], RHS = [record(ppp,[na_tuple([v1,v2])])], |
230 | | R=[record(ppp,[na_tuple([v1,v2])])],X=v1,Y=v2 )). |
231 | | :- assert_must_succeed(( |
232 | | csp_tuples:unify_values(LHS,RHS,R,a), LHS = [list([int(2),int(3)])], RHS = [list(X)], |
233 | | R=[list([int(2),int(3)])], X=[int(2),int(3)] )). |
234 | | :- assert_must_succeed(( |
235 | | csp_tuples:unify_values(LHS,RHS,R,a), LHS = [tuple([int(2),int(3)])], RHS = [in(X)], |
236 | | R=[tuple([int(2),int(3)])], X=tuple([int(2),int(3)]) )). |
237 | | |
238 | | :- block pattern_match_function_argument(-,?,?). |
239 | | pattern_match_function_argument(Value1,Value2,Function) :- |
240 | | %% print(pat_match(Value1,Value2,Function)),nl, %% |
241 | | (Value1 = tuple(X) |
242 | | -> pattern_match_f2(Value2,X,Function) |
243 | | ; (Value1 = Value2) /* Probably DEAD CODE, first argument is always tuple(-) (see use in haskell_csp_analyzer module)*/ |
244 | | ). |
245 | | :- block pattern_match_f2(-,?,?). |
246 | | pattern_match_f2(Value2,X,Function) :- |
247 | | ((Value2 = tuple(Y); Value2 = dotTuple(Y)) -> unify_values(X,Y,_,Function,symbol(Function)) %use Function as span |
248 | | ; Value2 = record(Cons,Args) -> X=[Cons|TX], unify_values(TX,Args,_,Function,symbol(Function)) |
249 | | ; unify_values(X,[Value2],_,Function,symbol(Function))). |
250 | | |
251 | | unify_values(Values1,Values2,Res,Channel) :- |
252 | | unify_values(Values1,Values2,Res,Channel,no_loc_info_available). |
253 | | |
254 | | :- block unify_values(-,?,?,?,?), unify_values(?,-,?,?,?). |
255 | | unify_values(Values1,Values2,Res,Channel,Span) :- |
256 | | % print(unify_values(Values1,Values2,Channel,Span)),nl, |
257 | ? | unify_tuple_args(Values1,Values2,Res,Channel,Span). |
258 | | |
259 | | :- use_module(probsrc(translate),[translate_csp_value/2]). |
260 | | :- use_module(probsrc(tools_strings),[ajoin/2]). |
261 | | unify_tuple_args([],[],R,_,_) :- !, R=[]. |
262 | | unify_tuple_args([],[in(X)|T],R,Ch,Span) :- !, R=[], empty_tuple(X), unify_tuple_args([],T,_,Ch,Span). |
263 | | unify_tuple_args([],[H|T],_R,Ch,Span) :- !, |
264 | | translate_csp_value(dotTuple([H|T]),Xtra), |
265 | | ajoin(['Mismatch in number of arguments for synchronisation on channel ',Ch,' with extra argument(s): '],Msg), |
266 | | add_error_with_span(unify_tuple_args,Msg,Xtra,Span), |
267 | | fail. |
268 | | unify_tuple_args([H|T],[],R,Ch,Span) :- !, unify_tuple_args([],[H|T],R,Ch,Span). |
269 | | %unify_tuple_args([X],[Y],R,_Ch) :- !, unify_arg(X,Y,XY), R=[XY]. |
270 | | unify_tuple_args([in(X)|TAIL],V2,Res,Ch,Span) :- is_tuple(X,List),!, gen_ins(List,INList), |
271 | | append(INList,TAIL,NewV1), |
272 | | unify_tuple_args(NewV1,V2,Res,Ch,Span). |
273 | | unify_tuple_args([in(X)|TAIL],[H|T2],R,_Ch,Span) :- TAIL==[],!, R=[H|T2], |
274 | ? | unify_tuple_args2(T2,X,H,R,Span). |
275 | | unify_tuple_args(V1,[in(X)|TAIL],R,Ch,Span) :- is_tuple(X,List),!, gen_ins(List,INList), |
276 | | append(INList,TAIL,NewV2), |
277 | | unify_tuple_args(V1,NewV2,R,Ch,Span). |
278 | | unify_tuple_args([H|T2],[in(X)|TAIL],R,_Ch,Span) :- TAIL==[],!, |
279 | | /* only treat it as a tail_in(X) if it is definitely at the end of the list |
280 | | see example LetTestChannel -> TEST(2) process for complication if we do |
281 | | not check that TAIL==[] */ |
282 | | R=[H|T2], |
283 | ? | unify_tuple_args2(T2,X,H,R,Span). |
284 | | unify_tuple_args([X|T1],[Y|T2],R,Ch,Span) :- !, |
285 | ? | unify_arg(X,Y,XY,Span), R=[XY|RT], unify_values(T1,T2,RT,Ch,Span). |
286 | | unify_tuple_args(X,Y,R,Ch,Span) :- |
287 | | add_internal_error_with_span(csp_tuples,'Could not evaluate: ',unify_tuple_args(X,Y,R,Ch),Span), |
288 | | X=Y, R=X. |
289 | | |
290 | | is_tuple(X,List) :- nonvar(X), |
291 | | (X=tuple(List) -> true |
292 | | ; X = dotTuple(List) -> debug_println(9,unevaluated_dotTupleValue(List)) % can come from in(.) generated from inGuard |
293 | | ; X = dotpat(List)%, nl,print(unevaluated_dotpat(List)),nl % should't really happen |
294 | | ). |
295 | | |
296 | | :- block unify_tuple_args2(-,?,?,?,?). |
297 | ? | unify_tuple_args2(T2,X,H,R,Span) :- (T2=[] -> unify_arg(in(X),H,_,Span) ; X = tuple(R)). |
298 | | |
299 | | gen_ins([],[]). |
300 | | gen_ins([X|T],[in(X)|IT]) :- gen_ins(T,IT). |
301 | | |
302 | | /* DEAD CODE: unify_arg/3 will never be called, instead of that unify_arg/4 will be used. */ |
303 | | %unify_arg(A,B,R) :- unify_arg(A,B,R,no_loc_info_available). |
304 | | |
305 | | :- block unify_arg(-,?,?,?), unify_arg(?,-,?,?). |
306 | | unify_arg(in(X),in(Y),R,Span) :- !, direct_unify_values(X,Y,Span), R=in(X). |
307 | | unify_arg(in(X),Y,R,Span) :- !, |
308 | | valid_value(Y,unify_arg(in(X),Y),true,Span), |
309 | ? | direct_unify_values(Y,X,Span), R=X. |
310 | | unify_arg(X,in(Y),R,Span) :- !, |
311 | | valid_value(X,unify_arg(X,in(Y)),true,Span), |
312 | ? | direct_unify_values(X,Y,Span),R=Y. |
313 | ? | unify_arg(X,Y,R,Span) :- unify_arg2(X,Y,R,Span). |
314 | | |
315 | | unify_arg2(X,Y,Res,_Span) :- (var(X);var(Y)), !, X=Y,Res=X. |
316 | | unify_arg2(record(FX,XL),record(FY,YL),Res,Span) :- !, FX=FY, |
317 | ? | unify_values(XL,YL,RL,record(FX),Span),Res=record(FX,RL). |
318 | | unify_arg2(na_tuple(XL),na_tuple(YL),Res,Span) :- !, |
319 | | l_unify_arg(XL,YL,RL,Span), Res=na_tuple(RL). |
320 | | %unify_arg2(tuple(XL),tuple(YL),Res,Span) :- !, |
321 | | % l_unify_arg(XL,YL,RL,Span), Res=tuple(RL). |
322 | | %unify_arg(X,Y,X,Span) :- !,valid_value(X,unify_arg1(X,Y),false,Span),valid_value(Y,unify_arg2(X,Y),false,Span),X=Y. |
323 | | unify_arg2(X,Y,Res,Span) :- direct_unify_values(X,Y,Span),Res=X. |
324 | | %unify_arg(X,X,X,Span) :- valid_tuple_value(X,unify_arg(X,X),false,Span). |
325 | | |
326 | | |
327 | | direct_unify_values(X,Y,_Span) :- (var(X) ; var(Y)),!, X=Y. |
328 | | direct_unify_values(int(X),Y,Span) :- !,direct_unify_check(int(YY),Y,Span),X=YY. |
329 | | direct_unify_values(na_tuple(X),Y,Span) :- !,direct_unify_check(na_tuple(YY),Y,Span),X=YY. |
330 | | %direct_unify_values(tuple(X),Y,Span) :- !,direct_unify_check(tuple(YY),Y,Span),X=YY. |
331 | | direct_unify_values(list(X),Y,Span) :- !,direct_unify_check(list(YY),Y,Span),X=YY. |
332 | | direct_unify_values(X,X,_). |
333 | | |
334 | | direct_unify_check(Pattern,Value,Span) :- if(Pattern=Value,true, |
335 | | add_error_fail(direct_unify_check,'Unification type failure: ', '='(Value,Pattern, Span))). |
336 | | |
337 | | l_unify_arg([],[],R,_Span) :- !, R=[]. |
338 | | l_unify_arg([HX|TX],[HY|TY],R,Span) :- !, R = [HR|TR], |
339 | | unify_arg2(HX,HY,HR,Span), % calling unify_arg/4 here will not unify if one of the argments is variable |
340 | | l_unify_arg(TX,TY,TR,Span). |
341 | | l_unify_arg(X,Y,R,Span) :- add_internal_error_with_span(l_unify_arg,'Illegal lists to unify: ',l_unify_arg(X,Y,R),Span),fail. |
342 | | |
343 | | |
344 | | % check if we have a valid value |
345 | | :- block valid_value(-,?,?,?). |
346 | | valid_value(int(X),_,_,_) :- !, safe_number(X). |
347 | | valid_value(X,_,_,_) :- haskell_csp: valid_constant(X),!. |
348 | | valid_value(tuple(L),Value,AllowIn,Span) :- !,l_valid_tuple_value(L,Value,AllowIn,Span). |
349 | | valid_value(na_tuple(L),Value,AllowIn,Span) :- !, l_valid_value(L,Value,AllowIn,Span). |
350 | | valid_value(dotTuple(L),Value,AllowIn,Span) :- !, l_valid_value(L,Value,AllowIn,Span). |
351 | | valid_value(record(C,F),Value,AllowIn,Span) :- |
352 | ? | is_csp_constructor(C), !, l_valid_value(F,Value,AllowIn,Span). |
353 | | valid_value(true,_,_,_) :- !. |
354 | | valid_value(false,_,_,_) :- !. |
355 | | valid_value(list(List),OuterValue,AllowIn,Span) :- !, l_valid_value(List,OuterValue,AllowIn,Span). |
356 | | valid_value(setValue(List),OuterValue,AllowIn,Span) :- !, l_valid_value(List,OuterValue,AllowIn,Span). |
357 | | valid_value(setFrom(Low),OuterValue,AllowIn,Span) :- !, |
358 | | valid_value(Low,OuterValue,AllowIn,Span). |
359 | | valid_value(setFromTo(Low,Up),OuterValue,AllowIn,Span) :- !, |
360 | | valid_value(Low,OuterValue,AllowIn,Span), |
361 | | valid_value(Up,OuterValue,AllowIn,Span). |
362 | | valid_value(in(X),Value,AllowIn,Span) :- !, |
363 | | (AllowIn=true -> true % we allow the in/1 constructor |
364 | | ; add_internal_error(valid_value,'Input inside value: ',in(X):Value,Span) |
365 | | ). |
366 | | /* CSP-M constructors are asserted as valid constants. See second clause of valid_value/4 and |
367 | | the implementation of the valid_constant/1 predicate in the haskell_csp_analyzer module. |
368 | | Do we want to distinguish between valid_constants and csp constructors? */ |
369 | | %valid_value(C,OuterValue,_,Span) :- haskell_csp_analyzer: is_csp_constructor(C),!, |
370 | | % add_error_with_span(valid_value,'Warning: datatype constructor used as value: ',C:outer(OuterValue),Span). |
371 | | valid_value(Channel,OuterValue,_,Span) :- |
372 | | is_a_channel_name(Channel),!, % from haskell_csp_analyzer |
373 | | add_error_with_span(valid_value,'Warning: channel name used as value (should be wrapped in tuple): ',Channel:outer(OuterValue),Span). |
374 | | % should we generate a warning ? see e.g., angel2.csp |
375 | | |
376 | | /* This clause should call the add_internal_error_with_span/4 predicate. We have to complete the implementation of the valid_value/4 predicate. See TODO below. */ |
377 | | valid_value(X,OuterCall,_,Span) :- |
378 | | add_error_with_span(valid_value,'Warning: Illegal data value: ',X:outer(OuterCall),Span). |
379 | | /* to do: add sets,sequences,...*/ |
380 | | |
381 | | :- block valid_tuple_value(-,?,?,?). |
382 | | valid_tuple_value(C,_,_,_Span) :- |
383 | | is_csp_constructor(C),!. % from haskell_csp_analyzer; here it could be ok to use datatype constructor |
384 | | valid_tuple_value(X,V,A,Span) :- valid_value(X,V,A,Span). |
385 | | |
386 | | :- block safe_number(-). |
387 | | safe_number(X) :- number(X). |
388 | | |
389 | | :- block l_valid_value(-,?,?,?). |
390 | | l_valid_value([],_,_AllowIn,_Span). |
391 | | l_valid_value([H|T],Value,AllowIn,Span) :- valid_value(H,Value,AllowIn,Span), l_valid_value(T,Value,AllowIn,Span). |
392 | | |
393 | | :- block l_valid_tuple_value(-,?,?,?). |
394 | | l_valid_tuple_value([],_,_AllowIn,_Span). |
395 | | l_valid_tuple_value([H|T],Value,AllowIn,Span) :- valid_tuple_value(H,Value,AllowIn,Span), l_valid_tuple_value(T,Value,AllowIn,Span). |
396 | | |
397 | | % -------------------------------------------------------------------- |
398 | | |
399 | | :- block list_projection(-,?,?,?,?), list_projection(?,-,?,?,?), list_projection(?,?,-,?,?). |
400 | | list_projection(Nr,Len,list(List),Res,Span) :- !, list_projection2(Nr,Len,List,Res,Span). |
401 | | list_projection(Nr,Len,Tuple,_,Span) :- !, |
402 | | add_error_with_span(list_projection,'Could not match list pattern: ', Nr/Len/Tuple,Span),fail. |
403 | | :- block list_projection2(?,?,-,?,?). |
404 | | list_projection2(Nr,Len,List,Res,Span) :- |
405 | | (nth1(Nr,List,Res) -> |
406 | | (length(List,Len) -> |
407 | | true |
408 | | ; add_error_with_span(list_projection,'List is not of the right length for pattern: ',Len/list(List),Span) |
409 | | ) |
410 | | ; add_error_with_span(list_projection,'List is too short for pattern: ',Nr/list(List),Span),fail |
411 | | ). |
412 | | |
413 | | :- block na_tuple_projection(-,?,?,?), na_tuple_projection(?,-,?,?). |
414 | | na_tuple_projection(Nr,na_tuple(List),Res,Span) :- !, |
415 | | (nth1(Nr,List,Res) -> |
416 | | true |
417 | | ; add_error_with_span(csp_tuples,'NA Tuple is too small for pattern: ',Nr/na_tuple(List),Span),fail |
418 | | ). |
419 | | na_tuple_projection(Nr,Tuple,_,Span) :- !, |
420 | | add_error_with_span(csp_tuples,'Could not match na_tuple pattern: ', Nr/Tuple,Span),fail. |
421 | | |
422 | | :- block tuple_projection(-,?,?,?), tuple_projection(?,-,?,?). |
423 | | %tuple_projection(Nr,E,_,_) :- print(proj(Nr,E)),nl,fail. |
424 | | tuple_projection(Nr,tuple(List),Res,Span) :- !, |
425 | | (nth1(Nr,List,Res) -> |
426 | | true |
427 | | ; add_error_with_span(csp_tuples,'Tuple is too small for pattern: ',Nr/tuple(List),Span),fail |
428 | | ). |
429 | | %tuple_projection(Nr,list(List),Res,Span) :- !, |
430 | | % (nth1(Nr,List,Res) -> add_error_with_span(csp_tuples,'Warning: projecting on list: ',Nr/List,Span) |
431 | | % ; add_error_with_span(csp_tuples,'Could not project: ',Nr/list(List),Span),fail). |
432 | | tuple_projection(Nr,Tuple,_,Span) :- !, |
433 | | add_error_with_span(csp_tuples,'Could not match tuple pattern: ', Nr/Tuple,Span),fail. |
434 | | |