| 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 | /* 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) :- !, valid_value(Y,unify_arg(in(X),Y),true,Span), | |
| 308 | direct_unify_values(Y,X,Span), R=X. | |
| 309 | unify_arg(X,in(Y),R,Span) :- !, valid_value(X,unify_arg(X,in(Y)),true,Span), | |
| 310 | direct_unify_values(X,Y,Span),R=Y. | |
| 311 | unify_arg(X,Y,R,Span) :- unify_arg2(X,Y,R,Span). | |
| 312 | ||
| 313 | unify_arg2(X,Y,Res,_Span) :- (var(X);var(Y)), !, X=Y,Res=X. | |
| 314 | unify_arg2(record(FX,XL),record(FY,YL),Res,Span) :- !, FX=FY, | |
| 315 | unify_values(XL,YL,RL,record(FX),Span),Res=record(FX,RL). | |
| 316 | unify_arg2(na_tuple(XL),na_tuple(YL),Res,Span) :- !, | |
| 317 | l_unify_arg(XL,YL,RL,Span), Res=na_tuple(RL). | |
| 318 | %unify_arg2(tuple(XL),tuple(YL),Res,Span) :- !, | |
| 319 | % l_unify_arg(XL,YL,RL,Span), Res=tuple(RL). | |
| 320 | %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. | |
| 321 | unify_arg2(X,Y,Res,Span) :- direct_unify_values(X,Y,Span),Res=X. | |
| 322 | %unify_arg(X,X,X,Span) :- valid_tuple_value(X,unify_arg(X,X),false,Span). | |
| 323 | ||
| 324 | ||
| 325 | direct_unify_values(X,Y,_Span) :- (var(X) ; var(Y)),!, X=Y. | |
| 326 | direct_unify_values(int(X),Y,Span) :- !,direct_unify_check(int(YY),Y,Span),X=YY. | |
| 327 | direct_unify_values(na_tuple(X),Y,Span) :- !,direct_unify_check(na_tuple(YY),Y,Span),X=YY. | |
| 328 | %direct_unify_values(tuple(X),Y,Span) :- !,direct_unify_check(tuple(YY),Y,Span),X=YY. | |
| 329 | direct_unify_values(list(X),Y,Span) :- !,direct_unify_check(list(YY),Y,Span),X=YY. | |
| 330 | direct_unify_values(X,X,_). | |
| 331 | ||
| 332 | direct_unify_check(Pattern,Value,Span) :- if(Pattern=Value,true, | |
| 333 | add_error_fail(direct_unify_check,'Unification type failure: ', '='(Value,Pattern, Span))). | |
| 334 | ||
| 335 | l_unify_arg([],[],R,_Span) :- !, R=[]. | |
| 336 | l_unify_arg([HX|TX],[HY|TY],R,Span) :- !, R = [HR|TR], | |
| 337 | unify_arg2(HX,HY,HR,Span), % calling unify_arg/4 here will not unify if one of the argments is variable | |
| 338 | l_unify_arg(TX,TY,TR,Span). | |
| 339 | 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. | |
| 340 | ||
| 341 | %:- block valid_value(-,?). | |
| 342 | /* DEAD CODE: valid_value/2 will never be called, instead of this predicate valid_value/4 is used. */ | |
| 343 | %valid_value(X,AllowIn) :- valid_value(X,X,AllowIn,no_loc_info_available). | |
| 344 | ||
| 345 | % check if we have a valid value | |
| 346 | :- block valid_value(-,?,?,?). | |
| 347 | valid_value(int(X),_,_,_) :- !, safe_number(X). | |
| 348 | valid_value(X,_,_,_) :- haskell_csp: valid_constant(X),!. | |
| 349 | valid_value(tuple(L),Value,AllowIn,Span) :- !,l_valid_tuple_value(L,Value,AllowIn,Span). | |
| 350 | valid_value(na_tuple(L),Value,AllowIn,Span) :- !, l_valid_value(L,Value,AllowIn,Span). | |
| 351 | valid_value(dotTuple(L),Value,AllowIn,Span) :- !, l_valid_value(L,Value,AllowIn,Span). | |
| 352 | valid_value(record(C,F),Value,AllowIn,Span) :- | |
| 353 | is_csp_constructor(C), !, l_valid_value(F,Value,AllowIn,Span). | |
| 354 | valid_value(true,_,_,_) :- !. | |
| 355 | valid_value(false,_,_,_) :- !. | |
| 356 | valid_value(list(List),OuterValue,AllowIn,Span) :- !, l_valid_value(List,OuterValue,AllowIn,Span). | |
| 357 | valid_value(in(X),Value,AllowIn,Span) :- !, | |
| 358 | (AllowIn=true -> | |
| 359 | true | |
| 360 | ; add_internal_error(valid_value,'Input inside value: ',in(X):Value,Span) | |
| 361 | ). | |
| 362 | %%%%%%%%%%%%%%%%%%%%%%% DEAD CODE %%%%%%%%%%%%%%%%%%%%%%%%% | |
| 363 | /* CSP-M constructors are asserted as valid constants. See second clause of valid_value/4 and | |
| 364 | the implementation of the valid_constant/1 predicate in the haskell_csp_analyzer module. | |
| 365 | Do we want to distinguish between valid_constants and csp constructors? */ | |
| 366 | %valid_value(C,OuterValue,_,Span) :- haskell_csp_analyzer: is_csp_constructor(C),!, | |
| 367 | % add_error_with_span(valid_value,'Warning: datatype constructor used as value: ',C:outer(OuterValue),Span). | |
| 368 | valid_value(Channel,OuterValue,_,Span) :- | |
| 369 | is_a_channel_name(Channel),!, % from haskell_csp_analyzer | |
| 370 | add_error_with_span(valid_value,'Warning: channel name used as value (should be wrapped in tuple): ',Channel:outer(OuterValue),Span). | |
| 371 | % should we generate a warning ? see e.g., angel2.csp | |
| 372 | ||
| 373 | /* 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. */ | |
| 374 | valid_value(X,OuterValue,_,Span) :- add_error_with_span(valid_value,'Warning: Illegal data value: ',X:outer(OuterValue),Span). | |
| 375 | /* to do: add sets,sequences,...*/ | |
| 376 | ||
| 377 | :- block valid_tuple_value(-,?,?,?). | |
| 378 | valid_tuple_value(C,_,_,_Span) :- | |
| 379 | is_csp_constructor(C),!. % from haskell_csp_analyzer; here it could be ok to use datatype constructor | |
| 380 | valid_tuple_value(X,V,A,Span) :- valid_value(X,V,A,Span). | |
| 381 | ||
| 382 | :- block safe_number(-). | |
| 383 | safe_number(X) :- number(X). | |
| 384 | ||
| 385 | :- block l_valid_value(-,?,?,?). | |
| 386 | l_valid_value([],_,_AllowIn,_Span). | |
| 387 | l_valid_value([H|T],Value,AllowIn,Span) :- valid_value(H,Value,AllowIn,Span), l_valid_value(T,Value,AllowIn,Span). | |
| 388 | ||
| 389 | :- block l_valid_tuple_value(-,?,?,?). | |
| 390 | l_valid_tuple_value([],_,_AllowIn,_Span). | |
| 391 | l_valid_tuple_value([H|T],Value,AllowIn,Span) :- valid_tuple_value(H,Value,AllowIn,Span), l_valid_tuple_value(T,Value,AllowIn,Span). | |
| 392 | ||
| 393 | % -------------------------------------------------------------------- | |
| 394 | ||
| 395 | :- block list_projection(-,?,?,?,?), list_projection(?,-,?,?,?), list_projection(?,?,-,?,?). | |
| 396 | list_projection(Nr,Len,list(List),Res,Span) :- !, list_projection2(Nr,Len,List,Res,Span). | |
| 397 | list_projection(Nr,Len,Tuple,_,Span) :- !, | |
| 398 | add_error_with_span(list_projection,'Could not match list pattern: ', Nr/Len/Tuple,Span),fail. | |
| 399 | :- block list_projection2(?,?,-,?,?). | |
| 400 | list_projection2(Nr,Len,List,Res,Span) :- | |
| 401 | (nth1(Nr,List,Res) -> | |
| 402 | (length(List,Len) -> | |
| 403 | true | |
| 404 | ; add_error_with_span(list_projection,'List is not of the right length for pattern: ',Len/list(List),Span) | |
| 405 | ) | |
| 406 | ; add_error_with_span(list_projection,'List is too short for pattern: ',Nr/list(List),Span),fail | |
| 407 | ). | |
| 408 | ||
| 409 | :- block na_tuple_projection(-,?,?,?), na_tuple_projection(?,-,?,?). | |
| 410 | na_tuple_projection(Nr,na_tuple(List),Res,Span) :- !, | |
| 411 | (nth1(Nr,List,Res) -> | |
| 412 | true | |
| 413 | ; add_error_with_span(csp_tuples,'NA Tuple is too small for pattern: ',Nr/na_tuple(List),Span),fail | |
| 414 | ). | |
| 415 | na_tuple_projection(Nr,Tuple,_,Span) :- !, | |
| 416 | add_error_with_span(csp_tuples,'Could not match na_tuple pattern: ', Nr/Tuple,Span),fail. | |
| 417 | ||
| 418 | :- block tuple_projection(-,?,?,?), tuple_projection(?,-,?,?). | |
| 419 | %tuple_projection(Nr,E,_,_) :- print(proj(Nr,E)),nl,fail. | |
| 420 | tuple_projection(Nr,tuple(List),Res,Span) :- !, | |
| 421 | (nth1(Nr,List,Res) -> | |
| 422 | true | |
| 423 | ; add_error_with_span(csp_tuples,'Tuple is too small for pattern: ',Nr/tuple(List),Span),fail | |
| 424 | ). | |
| 425 | %tuple_projection(Nr,list(List),Res,Span) :- !, | |
| 426 | % (nth1(Nr,List,Res) -> add_error_with_span(csp_tuples,'Warning: projecting on list: ',Nr/List,Span) | |
| 427 | % ; add_error_with_span(csp_tuples,'Could not project: ',Nr/list(List),Span),fail). | |
| 428 | tuple_projection(Nr,Tuple,_,Span) :- !, | |
| 429 | add_error_with_span(csp_tuples,'Could not match tuple pattern: ', Nr/Tuple,Span),fail. | |
| 430 |