csp_tuples

check_guard(Var,Guard,WF) :- %print(check_guard(Var,Guard)),nl,
    %(is_boolean_expression(Guard) -> check_boolean_expression(Guard) /* syntax in CIA-CSP but actually not allowed in CSP-M ! */
    haskell_csp:force_evaluate_argument_for_member_check(Guard,Set),
    /* already evaluate before Var is ground; avoid re-evaluation */
    try_get_cardinality_for_wait_flag(Set,Prio),
    get_wait_flag(Prio,check_guard,WF,LWF),
    % print(check_guard(Var,Guard,LWF)),nl,
    % TO DO: trigger earlier; Set must be a subset of the channel type; so we can always enumerate before full channel enumeration !
    when((ground(Var);nonvar(LWF)),(
    (ground(Var) -> evaluate_argument(Var,EVar) ; EVar=Var), % relevant for CorrectRouter.csp; TODO: investigate why
    %print(is_member_set(Var,Set)),nl,
    is_member_set_alsoPat(EVar,Set))).

construct_tuple([],tuple([])).

construct_tuple([H|T],R) :- construct_tuple2(H,T,R).

construct_tuple2(record(C,F),[],Res) :- !, Res= record(C,F). % this is not a dotTuple but a simple record

construct_tuple2(H,T,tuple([H|T])). % we have a real associative tuple

direct_unify_check(Pattern,Value,Span) :- if(Pattern=Value,true,
    add_error_fail(direct_unify_check,'Unification type failure: ', '='(Value,Pattern, Span))).

direct_unify_values(X,Y,_Span) :- (var(X) ; var(Y)),!, X=Y.

direct_unify_values(int(X),Y,Span) :- !,direct_unify_check(int(YY),Y,Span),X=YY.

direct_unify_values(na_tuple(X),Y,Span) :- !,direct_unify_check(na_tuple(YY),Y,Span),X=YY.

direct_unify_values(list(X),Y,Span) :- !,direct_unify_check(list(YY),Y,Span),X=YY.

direct_unify_values(X,X,_).

empty_tuple(tuple([])).

evaluate_channel_outputs(Values,ChannelExpr,EvaluatedValueList,Channel,Span,WF) :-
    % print(ev_channel(ChannelExpr,Values)),nl,
    evaluate_dot_tuple([ChannelExpr|Values],Res,WF), % print(Res),nl,
    %print(evaluated_dot_tuple(dotTuple([ChannelExpr|Values]),Res)),nl,
    (Res = tuple([Ch|VL])
    -> (EvaluatedValueList,Channel) = (VL,Ch) % if we unify VL without Ch we may get error messages !
    ; add_error_with_span(evaluate_channel_outputs,'Not a channel pattern: ', (ChannelExpr,Res),Span),fail
    ),
    (is_a_channel_name(Channel) -> true
    ; add_error_with_span(evaluate_channel_outputs,'Channel not declared: ',Channel,Span) ).

evaluate_cons_to_list(dotTuple(L),T,R,WF) :- !,
    append(L,T,LT), evaluate_dot_tuple_to_list(LT,R,WF).

evaluate_cons_to_list(tuple(L),T,R,WF) :- !,
    append(L,T,LT), evaluate_dot_tuple_to_list(LT,R,WF).

evaluate_cons_to_list(tupleExp(L),T,R,WF) :- !,
    haskell_csp: evaluate_argument2(tupleExp(L),Res),
    evaluate_dot_tuple_to_list(T,LT,WF),
    append([Res],LT,R).

evaluate_cons_to_list(X,T,R,WF) :- is_constructor(X,Constructor,SubTypes),!,
    % print(constructor(Constructor,SubTypes)),nl,
    evaluate_dot_tuple_to_list(T,ET,WF), %print(evalt(ET)),nl,
    get_constructor_arguments(SubTypes,ET,Fields,Rest),
    R=[record(Constructor,Fields)|Rest].

evaluate_cons_to_list(H,T,R,WF) :- !, evaluate_dot_argument(H,EH,WF),
    evaluate_cons_to_list_evhead(EH,T,R,WF).

evaluate_cons_to_list_evhead(tuple(L),T,R,WF) :- !, append(L,R2,R),
    evaluate_dot_tuple_to_list(T,R2,WF).

evaluate_cons_to_list_evhead(REC,T,R,WF) :-
    incomplete_record(REC,MissingFields,FullREC),!,
    %print(eval_cons_record(REC,MissingFields,FullREC)),nl,
    evaluate_dot_tuple_to_list(T,ET,WF), %print(evalt(ET)),nl,
    get_constructor_arguments(MissingFields,ET,MissingFields,Rest),
    %print(full_rec(FullREC,Rest)),nl,
    R=[FullREC|Rest].

evaluate_cons_to_list_evhead(EH,T,R,WF) :- R=[EH|ET], evaluate_dot_tuple_to_list(T,ET,WF).

evaluate_dot_argument(out(X),R,_) :- !, force_evaluate_argument(X,R).

evaluate_dot_argument(in(X),R,_) :- !, R=in(X).

evaluate_dot_argument(inGuard(X,Set),R,WF) :- !, R = in(X),
    %print(check_guard(X,Set)),nl,
    check_guard(X,Set,WF).

evaluate_dot_argument(H,EH,_) :- force_evaluate_argument(H,EH). %%% was evaluate_argument

evaluate_dot_tuple(List,Res) :-
    evaluate_dot_tuple(List,Res,_WF). %_WF not needed as inGuard cannot appear in normal tuples

evaluate_dot_tuple(L,Res,WF) :- evaluate_dot_tuple_to_list(L,R,WF),construct_tuple(R,Res).

evaluate_dot_tuple_to_list([],R,_WF) :- !,R=[].

evaluate_dot_tuple_to_list([H|T],R,WF) :- !, evaluate_cons_to_list(H,T,R,WF).

evaluate_dot_tuple_to_list(X,R,_WF) :- add_internal_error('Internal Error: Could not evaluate dotTuple List: ',X),R=X.

gen_ins([],[]).

gen_ins([X|T],[in(X)|IT]) :- gen_ins(T,IT).

get_constructor_arguments([],T,[],T).

get_constructor_arguments([H|T],DotArgs,Fields,R) :- nonvar(H), H = dotTupleType(L), !, append(L,T,LL), get_constructor_arguments(LL,DotArgs,Fields,R).

get_constructor_arguments([_Type|TT],DotArgs,Fields,R) :-
    (DotArgs = [H|DT]
    -> Fields = [H|T], get_constructor_arguments(TT,DT,T,R)
    ; % Have removed preference: incomplete records also arise in renamings; hard to distinguish proper from improper use
    %(preferences:preference(cspm_allow_incomplete_records,true) -> true
    % ; 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))),
    /* Casper generated CSP files will trigger this; as will renaming of record names ?! !! */
    DotArgs=[], R = [],
    Fields = [] /* to do check if we can work with this */
).

get_missing_fields([],[H|T],MissingFields,MissingFields) :- same_length([H|T],MissingFields).

get_missing_fields([Rec],[_TH],MissingFields,[FullRec]) :- % we could have incomplete record at end
    incomplete_record(Rec,MissingFields,FullRec),!.

get_missing_fields([FH|FT],[_TH|TT],MF,[FH|FFT]) :- get_missing_fields(FT,TT,MF,FFT).

incomplete_record(record(X,Fields), MissingFields, record(Constructor,FullFields)) :-
    is_constructor(X,Constructor,SubTypes),
    get_missing_fields(Fields,SubTypes,MissingFields,FullFields).

is_constructor(out(Constructor),Constructor,ArgSubTypes) :- atomic(Constructor),
    csp_full_type_constructor(Constructor,_Type,ArgSubTypes).

is_constructor(Constructor,Constructor,ArgSubTypes) :- atomic(Constructor),
    csp_full_type_constructor(Constructor,_Type,ArgSubTypes).

is_tuple(X,List) :- nonvar(X),
    (X=tuple(List) -> true
    ; X = dotTuple(List) -> debug_println(9,unevaluated_dotTupleValue(List)) % can come from in(.) generated from inGuard
    ; X = dotpat(List)%, nl,print(unevaluated_dotpat(List)),nl % should't really happen
).

l_unify_arg([],[],R,_Span) :- !, R=[].

l_unify_arg([HX|TX],[HY|TY],R,Span) :- !, R = [HR|TR],
    unify_arg2(HX,HY,HR,Span), % calling unify_arg/4 here will not unify if one of the argments is variable
    l_unify_arg(TX,TY,TR,Span).

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.

l_valid_tuple_value([],_,_AllowIn,_Span).

l_valid_tuple_value([H|T],Value,AllowIn,Span) :- valid_tuple_value(H,Value,AllowIn,Span), l_valid_tuple_value(T,Value,AllowIn,Span).

l_valid_value([],_,_AllowIn,_Span).

l_valid_value([H|T],Value,AllowIn,Span) :- valid_value(H,Value,AllowIn,Span), l_valid_value(T,Value,AllowIn,Span).

list_projection(Nr,Len,list(List),Res,Span) :- !, list_projection2(Nr,Len,List,Res,Span).

list_projection(Nr,Len,Tuple,_,Span) :- !,
    add_error_with_span(list_projection,'Could not match list pattern: ', Nr/Len/Tuple,Span),fail.

list_projection2(Nr,Len,List,Res,Span) :-
    (nth1(Nr,List,Res) ->
    (length(List,Len) ->
    true
    ; add_error_with_span(list_projection,'List is not of the right length for pattern: ',Len/list(List),Span)
    )
    ; add_error_with_span(list_projection,'List is too short for pattern: ',Nr/list(List),Span),fail
).

na_tuple_projection(Nr,na_tuple(List),Res,Span) :- !,
    (nth1(Nr,List,Res) ->
    true
    ; add_error_with_span(csp_tuples,'NA Tuple is too small for pattern: ',Nr/na_tuple(List),Span),fail
).

na_tuple_projection(Nr,Tuple,_,Span) :- !,
    add_error_with_span(csp_tuples,'Could not match na_tuple pattern: ', Nr/Tuple,Span),fail.

pattern_match_f2(Value2,X,Function) :-
    ((Value2 = tuple(Y); Value2 = dotTuple(Y)) -> unify_values(X,Y,_,Function,symbol(Function)) %use Function as span
    ; Value2 = record(Cons,Args) -> X=[Cons|TX], unify_values(TX,Args,_,Function,symbol(Function))
    ; unify_values(X,[Value2],_,Function,symbol(Function))).

pattern_match_function_argument(Value1,Value2,Function) :-
    %% print(pat_match(Value1,Value2,Function)),nl,
    (Value1 = tuple(X)
    -> pattern_match_f2(Value2,X,Function)
    ; (Value1 = Value2) /* Probably DEAD CODE, first argument is always tuple(-) (see use in haskell_csp_analyzer module)*/
).

safe_number(X) :- number(X).

tuple_projection(Nr,tuple(List),Res,Span) :- !,
    (nth1(Nr,List,Res) ->
    true
    ; add_error_with_span(csp_tuples,'Tuple is too small for pattern: ',Nr/tuple(List),Span),fail
).

tuple_projection(Nr,Tuple,_,Span) :- !,
    add_error_with_span(csp_tuples,'Could not match tuple pattern: ', Nr/Tuple,Span),fail.

unify_arg(in(X),in(Y),R,Span) :- !, direct_unify_values(X,Y,Span), R=in(X).

unify_arg(in(X),Y,R,Span) :- !,
    valid_value(Y,unify_arg(in(X),Y),true,Span),
    direct_unify_values(Y,X,Span), R=X.

unify_arg(X,in(Y),R,Span) :- !,
    valid_value(X,unify_arg(X,in(Y)),true,Span),
    direct_unify_values(X,Y,Span),R=Y.

unify_arg(X,Y,R,Span) :- unify_arg2(X,Y,R,Span).

unify_arg2(X,Y,Res,_Span) :- (var(X);var(Y)), !, X=Y,Res=X.

unify_arg2(record(FX,XL),record(FY,YL),Res,Span) :- !, FX=FY,
    unify_values(XL,YL,RL,record(FX),Span),Res=record(FX,RL).

unify_arg2(na_tuple(XL),na_tuple(YL),Res,Span) :- !,
    l_unify_arg(XL,YL,RL,Span), Res=na_tuple(RL).

unify_arg2(X,Y,Res,Span) :- direct_unify_values(X,Y,Span),Res=X.

unify_tuple_args([],[],R,_,_) :- !, R=[].

unify_tuple_args([],[in(X)|T],R,Ch,Span) :- !, R=[], empty_tuple(X), unify_tuple_args([],T,_,Ch,Span).

unify_tuple_args([],[H|T],_R,Ch,Span) :- !,
    translate_csp_value(dotTuple([H|T]),Xtra),
    ajoin(['Mismatch in number of arguments for synchronisation on channel ',Ch,' with extra argument(s): '],Msg),
    add_error_with_span(unify_tuple_args,Msg,Xtra,Span),
    fail.

unify_tuple_args([H|T],[],R,Ch,Span) :- !, unify_tuple_args([],[H|T],R,Ch,Span).

unify_tuple_args([in(X)|TAIL],V2,Res,Ch,Span) :- is_tuple(X,List),!, gen_ins(List,INList),
    append(INList,TAIL,NewV1),
    unify_tuple_args(NewV1,V2,Res,Ch,Span).

unify_tuple_args([in(X)|TAIL],[H|T2],R,_Ch,Span) :- TAIL==[],!, R=[H|T2],
    unify_tuple_args2(T2,X,H,R,Span).

unify_tuple_args(V1,[in(X)|TAIL],R,Ch,Span) :- is_tuple(X,List),!, gen_ins(List,INList),
    append(INList,TAIL,NewV2),
    unify_tuple_args(V1,NewV2,R,Ch,Span).

unify_tuple_args([H|T2],[in(X)|TAIL],R,_Ch,Span) :- TAIL==[],!,
    /* only treat it as a tail_in(X) if it is definitely at the end of the list
    see example LetTestChannel -> TEST(2) process for complication if we do
    not check that TAIL==[] */
    R=[H|T2],
    unify_tuple_args2(T2,X,H,R,Span).

unify_tuple_args([X|T1],[Y|T2],R,Ch,Span) :- !,
    unify_arg(X,Y,XY,Span), R=[XY|RT], unify_values(T1,T2,RT,Ch,Span).

unify_tuple_args(X,Y,R,Ch,Span) :-
    add_internal_error_with_span(csp_tuples,'Could not evaluate: ',unify_tuple_args(X,Y,R,Ch),Span),
    X=Y, R=X.

unify_tuple_args2(T2,X,H,R,Span) :- (T2=[] -> unify_arg(in(X),H,_,Span) ; X = tuple(R)).

unify_values(Values1,Values2,Res,Channel) :-
    unify_values(Values1,Values2,Res,Channel,no_loc_info_available).

unify_values(Values1,Values2,Res,Channel,Span) :-
    % print(unify_values(Values1,Values2,Channel,Span)),nl,
    unify_tuple_args(Values1,Values2,Res,Channel,Span).

valid_tuple_value(C,_,_,_Span) :-
    is_csp_constructor(C),!. % from haskell_csp_analyzer; here it could be ok to use datatype constructor

valid_tuple_value(X,V,A,Span) :- valid_value(X,V,A,Span).

valid_value(int(X),_,_,_) :- !, safe_number(X).

valid_value(X,_,_,_) :- haskell_csp: valid_constant(X),!.

valid_value(tuple(L),Value,AllowIn,Span) :- !,l_valid_tuple_value(L,Value,AllowIn,Span).

valid_value(na_tuple(L),Value,AllowIn,Span) :- !, l_valid_value(L,Value,AllowIn,Span).

valid_value(dotTuple(L),Value,AllowIn,Span) :- !, l_valid_value(L,Value,AllowIn,Span).

valid_value(record(C,F),Value,AllowIn,Span) :-
    is_csp_constructor(C), !, l_valid_value(F,Value,AllowIn,Span).

valid_value(true,_,_,_) :- !.

valid_value(false,_,_,_) :- !.

valid_value(list(List),OuterValue,AllowIn,Span) :- !, l_valid_value(List,OuterValue,AllowIn,Span).

valid_value(setValue(List),OuterValue,AllowIn,Span) :- !, l_valid_value(List,OuterValue,AllowIn,Span).

valid_value(setFrom(Low),OuterValue,AllowIn,Span) :- !,
    valid_value(Low,OuterValue,AllowIn,Span).

valid_value(setFromTo(Low,Up),OuterValue,AllowIn,Span) :- !,
    valid_value(Low,OuterValue,AllowIn,Span),
    valid_value(Up,OuterValue,AllowIn,Span).

valid_value(in(X),Value,AllowIn,Span) :- !,
    (AllowIn=true -> true % we allow the in/1 constructor
    ; add_internal_error(valid_value,'Input inside value: ',in(X):Value,Span)
).

valid_value(Channel,OuterValue,_,Span) :-
    is_a_channel_name(Channel),!, % from haskell_csp_analyzer
    add_error_with_span(valid_value,'Warning: channel name used as value (should be wrapped in tuple): ',Channel:outer(OuterValue),Span).

valid_value(X,OuterCall,_,Span) :-
    add_error_with_span(valid_value,'Warning: Illegal data value: ',X:outer(OuterCall),Span).