haskell_csp_analyzer

add_extra_input_tuple_variable(Expr,XA,NXA,Res,_Span) :- % allow record constructors
    %print(addi(Expr)),nl,
    nonvar(Expr), is_csp_constructor(Expr),!, XA=NXA, Res=Expr. % TO DO: should we check the args ?!

add_extra_input_tuple_variable(Expr,XA,NXA,Res,Span) :- add_extra_input_variable(Expr,XA,NXA,Res,Span).

add_extra_input_tuple_variables([],XA,XA,[],_).

add_extra_input_tuple_variables([V|T],XA,NXA,[CV|CT],Span) :-
    add_extra_input_tuple_variable(V,XA,XA1,CV,Span),
    add_extra_input_tuple_variables(T,XA1,NXA,CT,Span).

add_extra_input_variable(Var,XA,NXA,Res,Span) :- %print(add(Var,XA,NXA)),nl,
    var(Var),!,
    (exact_member(Var,XA) %% case will be catched from the CSP-M parser (e.g. c?x?x => Error message: Redefinition of x)
    -> (add_internal_error(haskell_csp_analyzer,'Internal Error: Channel input variable already used: ',Var,Span),NXA=XA)
    ; NXA=[Var|XA]
    ),Res=Var.

add_extra_input_variable(listPat(List),XA,NXA,Res,Span) :- !, Res = list(RList),
    add_extra_input_variables(List,XA,NXA,RList,Span).

add_extra_input_variable(singleSetPat(List),XA,NXA,Res,Span) :- !, Res = setValue(RList),
    add_extra_input_variables(List,XA,NXA,RList,Span).

add_extra_input_variable(tuplePat(List),XA,NXA,Res,Span) :- !, Res = na_tuple(RList),
    add_extra_input_variables(List,XA,NXA,RList,Span).

add_extra_input_variable(dotpat(List),XA,NXA,Res,Span) :- !, Res = dotTuple(RList),
    /* dotTuple or dotpat because it still needs to be evaluated */
    /* TODO: CHECK if we don't have to detect records here ?? */
    add_extra_input_tuple_variables(List,XA,NXA,RList,Span).

add_extra_input_variable(alsoPattern([X,Y]),XA,NXA,Res,Span) :- !, Res = alsoPat(RX,RY),
    add_extra_input_variable(X,XA,NXX,RX,Span),
    add_extra_input_variable(Y,XA,NXY,RY,Span), append(NXX,NXY,NXA). % was NXA=NXX.

add_extra_input_variable(appendPattern(List),_XA,_NXA,Res,Span) :- !,
    compile_append_pat(appendPattern(List),LRes,Constr),
    get_append_agent_result('AppPatFun',LRes,Constr,Res,Span).

add_extra_input_variable(Expr,XA,NXA,Res,_Span) :-
    (Expr = int(_); valid_constant(Expr)),!, XA=NXA, Res=Expr.

add_extra_input_variable(Expr,XA,NXA,Res,Span) :-
    add_error(haskell_csp_analyzer,'Channel input not recognized: ',Expr,Span),
    NXA=XA, Res=Expr.

add_extra_input_variables([],XA,XA,[],_).

add_extra_input_variables([V|T],XA,NXA,[CV|CT],Span) :-
    add_extra_input_variable(V,XA,XA1,CV,Span),
    add_extra_input_variables(T,XA1,NXA,CT,Span).

add_new_parameters(X,Vars,NewVars) :- var(X),!,Vars=NewVars.

add_new_parameters(comprehensionGenerator(VAR,_SET),Vars,NewVars) :- !,
    (var(VAR) -> NewVars=[VAR|Vars]
    ; %nl,print(comprehensionGenerator(VAR,_SET)),nl,
    NewVars=Vars)
. %, check_var(VAR,_SET).

add_new_parameters(_,V,V).

agent_compiled_with_constraints(Head,Body,Span,Constr) :-
    clause(agent_compiled(Head,Body,Span),Constr).

agent_compiled_without_constraints(Head,Body,Span) :-
    clause(agent_compiled(Head,Body,Span),_Constr).

analyze :- reset_csp_analyzer,
    precompile_datatypes(init),% initialiazing constructors before starting to check the process bodies
    debug_stats(precompile_constants),
    precompile_constants,
    debug_stats(compile_nested_let_expressions),
    compile_nested_let_expressions,
    opt_csp_listing,
    debug_stats(find_csp_processes),
    debug_print(19,'% Finding Definite CSP Processes:'),
    analyze_recursively,
    debug_nl(19),debug_print(19,'% Finding Possible CSP Processes: '),
    analyze_recursively_possible,
    check,
    debug_stats(precompile_nametypes),
    precompile_nametypes, /* must be put before datatypes */
    precompile_datatypes(eval),
    generate_channel_type_lists,
    precompile_cspPrint,
    debug_stats(precompile_finished).

analyze_recursively :-
    retractall(change_happened),
    agent_compiled_without_constraints(X,Body,_Span),
    functor(X,F,N),functor(X2,F,N),
    \+ is_csp_process(X2),
    (is_function(X2) -> true ; assertz(is_function(X2))),
    definite_cspm_process_expression(Body),
    assertz(is_csp_process(X2)),
    assertz(change_happened),
    debug_mode(on),print(' '),print_agent(X2),
    fail.

analyze_recursively :- debug_print(19,';'),
    (change_happened -> analyze_recursively ; debug_nl(19)).

analyze_recursively_possible :-
    retractall(change_happened),
    is_function(X2),
    \+ is_csp_process(X2), \+ is_possible_csp_process(X2),
    findall(Body,agent_compiled_without_constraints(X2,Body,_Span),AllBodies),
    maplist(possible_cspm_process_expression,AllBodies),
    assertz(is_possible_csp_process(X2)),
    assertz(change_happened),
    debug_mode(on),print(' '),print_agent(X2),
    fail.

analyze_recursively_possible :- debug_print(19,';'),
    (change_happened -> analyze_recursively_possible ; debug_nl(19)).

assert_agent(Head,Body,Span) :-
    compile_head(Head,NewHead,Constraints,Span),
    assert_agent_compiled_head(NewHead,Body,Span,Constraints).

assert_agent_compiled_head(Head,OrigBody,Span,Constr) :-
    (preferences:get_preference(cspm_strip_source_location,true)
    -> clear_span(OrigBody,Body) %,print(clear_span(Res,CRes)),nl
    ; Body=OrigBody),
    lift(Head,LHead,(Body,Constr),(LBody,LConstr)),
    assertz((agent_compiled(LHead,LBody,Span) :- LConstr)),
    LHead =.. [Functor|Args],
    length(Args,Arity),
    compute_lazy_strict_types(Args,TL),
    (retract(agent_parameters(Functor,Arity,OldTL))
    -> merge_lazy_strict_types(TL,OldTL,NewTL) ; NewTL = TL ),
    %% print(agent_parameters(Functor,Arity,NewTL)),nl,
    assertz(agent_parameters(Functor,Arity,NewTL)),
    (agent_functor(Functor,Arity) -> true ; assertz(agent_functor(Functor,Arity))).

blocking_append(L1,L2,L3) :- append(L1,L2,L3).

builtin_functor('tuplePat',1).

builtin_functor(dotpat,1).

builtin_functor(Nr,0) :- number(Nr).

channel_type_list(left,[dataType('FRUIT')]).

channel_type_list(right,[dataType('FRUIT')]).

channel_type_list(mid,[dataType('FRUIT')]).

channel_type_list(ack,[]).

channel_type_list(a,[intType]). /* for test cases */

channel_type_list(b,[intType]). /* for test cases */

channel_type_list(c,[intType]). /* for test cases */

channel_type_list(gen1,[intType,intType]). /* for test cases */

channel_type_list(gen2,[intType,intType]). /* for test cases */

channel_type_list(receive,[dataType('SubMsg')]).

channel_type_list(contact,[dataType('SubSubMsg'),intType,boolType]).

channel_type_list(infinite,[dataType('Inf')]).

check :- debug_println(15,'% Checking Definitions:'),
    findall(V,bindval(V,_,_),LBV),
    check_for_multiples(LBV),
    findall(W,(agent(W,_,_);agent_curry(W,_,_)),LAG),
    check_for_contig(LAG),
    % Note: we cannot detect if a function definition is interrupted by a bindval or channel def
    debug_nl(15),
    debug_println(9,'% Checking Definition bodies:'),
    agent_compiled_without_constraints(X,Body,Span),
    (debug_mode(on) -> print(' '),print_agent(X) ; true),
    check_definition_body(Body,X,Span),
    fail.

check :- debug_nl(15).

check_definite_cspm_body_construct(X,D,S) :-
    check_definition_body(X,D,S),!.

check_definite_cspm_body_construct(X,_Def,Span) :-
    add_internal_error(haskell_csp_analyzer,'Unknown CSP construct: ',X,Span).

check_definition_body(X,_,_) :- var(X),!,true.

check_definition_body('$VAR'(X),_,_) :- !, cur_numbervars_index(Idx), X =< Idx.

check_definition_body(lambda(_,E),Def,Span) :- !,
    check_definition_body(E,Def,Span).

check_definition_body(agent_call(CallSpan,F,Par),_Def,_Span) :- atomic(F),!, X=..[F|Par],
    ((is_defined_agent(X); is_builtin_agent(X)) -> true ; add_error(haskell_csp_analyzer,'Undefined Agent Call: ',X,CallSpan)).

check_definition_body(agent_call(CallSpan,X,Par),_Def,_Span) :-
    nonvar(X), X=lambda(Var,Body),!,
    length(Par,PL), length(Var,VL),
    (PL=VL -> true
    ; add_error(haskell_csp_analyzer,'Lambda parameters and arguments do not match: ',(Par,Var,Body),CallSpan)).

check_definition_body(agent_call(CallSpan,F,Par),Def,_Span) :- !,
    (var(F) -> true ;
    (F=agent_call(Span2,F2,Par2)
    -> check_definition_body(agent_call(Span2,F2,Par2),Def,CallSpan)
    ; add_error(haskell_csp_analyzer,'Complicated LHS not yet supported in agent_call: ',
    agent_call(F,Par),CallSpan)
)
).

check_definition_body(X,Def,Span) :-
    definite_cspm_process_construct(X,Spans,OtherSubExprs,List),!,
    l_check_spans(Spans,Span), l_check_non_csp_args(OtherSubExprs,Span),
    l_check_definite_csp_args(List,Def,Span).

check_definition_body(X,Def,Span) :-
    potential_cspm_process_construct(X,Spans,OtherSubExprs,List),
    l_check_spans(Spans,Span), l_check_non_csp_args(OtherSubExprs,Span),
    l_check_possible_csp_args(List,Def,Span).

check_for_contig([]).

check_for_contig([H,H2|T]) :- functor(H,F,N), functor(H2,F,N), !, check_for_contig(T).

check_for_contig([H|T]) :-
    (member(H,T) -> add_symbol_error(haskell_csp,'Definition not contiguous: ',H,H) ; true),
    check_for_contig(T).

check_for_multiples(S) :- samsort(S,SS),check_for_multiples2(SS).

check_for_multiples2([]).

check_for_multiples2([H|T]) :-
    (T=[H|T2] -> add_symbol_error(haskell_csp,'Multiple Definitions of: ',H,H) ; T2=T),
    check_for_multiples2(T2).

check_var(V,SET) :- nl, print(not_var(V)),nl,print(SET),nl.

clear_span(X,R) :- var(X),!,R=X.

clear_span('|~|'(X,Y,SrcSpan),R) :- R='|~|'(CX,CY,SrcSpan),
    % keep span for internal choice; it is currently being used for tau-priority partial order reduction
    clear_span(X,CX), clear_span(Y,CY).

clear_span(X,R) :- csp_span(X),!,R=no_loc_info_available.

clear_span(X,R) :- atomic(X),!,R=X.

clear_span(X,R) :- X=..[F|A], maplist(clear_span,A,CA), R=..[F|CA].

compile_append_pat(appendPattern([Pat1]),NewPara,Constraint1) :- !,
    compile_head_para(Pat1,NewPara,Constraint1,_Head,_Span).

compile_append_pat(appendPattern([H|T]),NewPara,ConstraintsT) :-
    nonvar(H), H=listPat(HList),is_list_skeleton(HList),!,
    NewPara = list(NewList),
    compile_append_pat(appendPattern(T),NewT,ConstraintsT),
    NewT = list(TList), append(HList,TList,NewList).

compile_append_pat(appendPattern(Pat),NewPara,Constraint) :-
    is_list_skeleton(Pat),
    append(T,[H],Pat),
    nonvar(H), H=listPat(HList),is_list_skeleton(HList),!,
    compile_append_pat(appendPattern(T),NewT,_ConstraintsT),
    NewPara = list(NewList), NewT = list(TList),
    Constraint=blocking_append(TList,HList,NewList).

compile_append_pat(Pat,_NewPara,_Constraint) :-
    add_internal_error('Internal Error: Expected append pattern instead of ', Pat),fail.

compile_body(X,_F,_XARGS,_DEFS,_DC,Res) :- var(X),!, Res=X.

compile_body(lambda(Args,Body),F,XARGS,DEFS,DC,Res) :- !, %nl,print(lambda1(Args,Body)),nl,
    l_compile_head_para(Args,CArgs,Constraints,lambda(Args,Body),unknown_span),
    (Constraints=true -> true
    ; add_error(compile_body,'ProB does not (yet) support complicated patterns inside lambda: ',lambda(Args,Body))),
    mynumbervars(CArgs), % note: important that compilation of body does detect $VAR
    % otherwise will fail to add necessary parameters
    Res = lambda(CArgs,ResBody),
    append(Args,XARGS,NewXARGS),
    compile_body(Body,F,NewXARGS,DEFS,DC,ResBody).

compile_body(val_of(X,Span),_F,_XARGS,DEFS,_DC,Res) :- !, /* we do not need to compile X itself !? */
    % haskell_csp:get_symbol_span(X,Span), % does this work for local lets ???
    (is_local_let2(X,0,[],DEFS,NX,NPar,_)
    -> Res = agent_call(Span,NX,NPar)
    ; Res=agent_call(Span,X,[])).

compile_body(agent_call(_Span,TFun,[Arg]),F,XARGS,DEFS,DC,Res) :-
    cspTransparent([TFun]), !,
    compile_body(Arg,F,XARGS,DEFS,DC,Res).

compile_body(agent_call_curry(X,Paras),F,XARGS,DEFS,DC,Res) :- !,
    /* translate agent_call_curry into nested agent_calls : */
    (Paras=[Paras1|RestParas]
    -> compile_body(agent_call_curry(agent_call(no_loc_info_available,X,Paras1),RestParas),F,XARGS,DEFS,DC,Res)
    ; compile_body(X,F,XARGS,DEFS,DC,Res)
).

compile_body(agent_call(_Span,X,Para),F,XARGS,DEFS,DC,Res) :- atomic(X),
    Term=..[X|Para], length(Para,N), length(NPara,N), Fun=..[X|NPara],
    (\+ agent(Fun,_Body,_Src), is_builtin_agent(Term), \+is_local_let(Fun,DEFS,_NewFun,_FXArgs,_)),!,
    compile_body(builtin_call(Term),F,XARGS,DEFS,DC,Res).

compile_body(agent_call(Span,X,Para),F,XARGS,DEFS,_DC,Res) :- atomic(X),
    CX=X, %%%%compile_body(X,F,XARGS,DEFS,true,CX),
    l_compile_body(Para,F,XARGS,DEFS,true,CPara),
    (is_local_let2(CX,_Arity,CPara,DEFS,NX,NPara,_) -> Res = agent_call(Span,NX,NPara) ; Res=agent_call(Span,CX,CPara)).

compile_body(prefix(Span,Values,ChannelExpr,CSP,Span2),F,XARGS,DEFS,DC,Res) :- !,
    compile_body(ChannelExpr,F,XARGS,DEFS,DC,NewChExpr),
    l_compile_channel_value(Values,F,XARGS,DEFS,NewVals,NewXARGS,Span),
    %print(comp_channel(Values,NewVals)),nl,
    compile_body(CSP,F,NewXARGS,DEFS,DC,NewCSP),
    ResBody = prefix(Span,NewVals,NewChExpr,NewCSP,Span2),
    (NewXARGS \= XARGS %,DC = true always lift out so that states are ground and that we need no variant/instance checks !
    -> /* need to lift prefix */
    gensym('->',GSF), debug_println(5,generating_agent_for_prefix(F,GSF, ResBody)),
    string_concatenate(F,GSF,PrefixName),
    Call =.. [PrefixName|XARGS],
    Res = agent_call(Span,PrefixName,XARGS),
    % portray_clause( prefix_agent(Call,ResBody) ),
    assert_agent(Call, ResBody,Span),
    functor(Call,CF,CN), functor(CallSkel,CF,CN),
    assertz( is_csp_process(CallSkel) )
    ; %print(not_lifting_prefix(Values,F,XARGS,DC, NewXARGS),nl,
    Res = ResBody
).

compile_body(X,F,XARGS,DEFS,DC,Res) :-
    replicated_or_comprehension(X,Op,Vars,OutsideOfScope,InScope,NewDC,ISCSP,Span),!,
    % print(repl(X,Op,Vars)),nl,print(inscope(InScope)),nl, print(outofscope(OutsideOfScope)),nl,
    (var(Vars)
    -> add_error(haskell_csp_analyzer,'Replicated variables var: ',X),fail ; true),
    %%print(compiling_set(OutsideOfScope,XARGS)),nl,
    % This part does not need the extra variables Vars as parameters
    compile_body(OutsideOfScope,F,XARGS,DEFS,DC,NewOutsideOfScope),
    % print(done_outside(NewOutsideOfScope)),nl,
    append(Vars,XARGS,NewXARGS), % add the variables of the comprehension as additional parameters to nested calls
    %%print(compiling_csp(InScope,NewXARGS)),nl,
    compile_body(InScope,F,NewXARGS,DEFS,NewDC,NewInScope),
    % print(done_csp(InScope,NewInScope)),nl,
    replicated_or_comprehension(ResBody,Op,Vars,NewOutsideOfScope,NewInScope,_,ISCSP,Span),
    (true %DC = true always lift out so that states are ground and that we need no variant/instance checks !
    -> gensym('@',GSF), debug_println(5,generating_agent_for_repOp(F,GSF, ResBody)),
    string_concatenate(F,GSF,PrefixName),
    Call =.. [PrefixName|XARGS],
    Res = agent_call(Span,PrefixName,XARGS), % use Span ?? or no_loc_info_available
    % portray_clause( replicated(Call,ResBody) ),
    assert_agent(Call, ResBody, unknown_span),
    functor(Call,CF,CN), functor(CallSkel,CF,CN),
    (ISCSP=true -> assertz( is_csp_process(CallSkel) ) ; true)
    ; Res = ResBody
).

compile_body(let(LIST,Body),F,XARGS,DEFS,DC,Res) :- !, %print(let(LIST)),nl,
    expand_let_definitions(LIST,ExpLIST), %print(extracting(ExpLIST)),nl,
    extract_new_funs_from_lets(ExpLIST,F,XARGS,[],LetDefs),
    append(LetDefs,DEFS,NDEFS),
    debug_println(5,new_funs(NDEFS)),
    compile_lets(ExpLIST,F,XARGS,NDEFS,DC),
    debug_println(5,nested_let_compile(Body,NDEFS)),
    compile_body(Body,F,XARGS,NDEFS,DC,Res). % check builtin calls in let declarations list

compile_body(builtin_call(X),F,XARGS,DEFS,DC,Res) :- !,
    translate_builtin_call(X,TX),
    %(translate_builtin_call(X,TX) -> true ; TX=X),
    compile_body(TX,F,XARGS,DEFS,DC,Res).

compile_body([H|T],F,XARGS,DEFS,DC,Res) :- !, l_compile_body([H|T],F,XARGS,DEFS,DC,Res).

compile_body(FunName,_F,_XARGS,DEFS,_DC,Res) :- atomic(FunName),
    %(FunName=getPrio -> print(compile(FunName,DEFS)),nl ; true),
    is_local_let2(FunName,OriginalArity,[],DEFS,NewF,_,LLXARGS) ,!, %% append(LLXARGS,_,_XARGS) ??
    %print(replacing(FunName,NewF,LLXARGS)),nl,
    % We have a local function whose function name is used: replace by a lambda closure which hides
    % the additional parameters required to call the lifted version NewF
    length(OrigArgs,OriginalArity),
    mynumbervars(OrigArgs),
    (LLXARGS=[]
    -> Res = NewF
    ; (append(OrigArgs,LLXARGS,FullArgs),
    haskell_csp:get_symbol_span(FunName,Span),
    Res = lambda(OrigArgs,agent_call(Span,NewF,FullArgs))
% ,print(generated(Res)),nl
)
). %% ,print(res(Res)),nl.

compile_body(NV,F,XARGS,DEFS,DC,Res) :- nonvar(NV), NV=..[FN|Args], !, /* TO DO: IMPROVE ! */
    l_compile_body(Args,F,XARGS,DEFS,DC,ResArgs),
    Res =.. [FN|ResArgs] %%,print(compiled(NV,Res)),nl
.

compile_body(X,_F,_X,_D,_DC,X).

compile_body(Body,F,XARGS,NDEFS,Res) :- compile_body(Body,F,XARGS,NDEFS,false,Res).

compile_channel_value(VAR,F,XA,_DEFS,Res,NXA,Span) :- var(VAR),!,
    add_internal_error(compile_channel_value,'Variable as channel value: ',F,Span),NXA=XA, Res=[VAR].

compile_channel_value(out(Expr),F,XA,DEFS,Res,NXA,_Span) :- !,
    Res=[out(CE)],NXA=XA,compile_body(Expr,F,XA,DEFS,CE).

compile_channel_value(dot(Expr),F,XA,DEFS,Res,NXA,_Span) :- !,
    Res=[out(CE)],NXA=XA,compile_body(Expr,F,XA,DEFS,CE).

compile_channel_value(in(Expr),F,XA,DEFS,Res,NXA,Span) :- ground(Expr), !,
    add_message(haskell_csp_analyzer,'CSP Warning: Channel input contains no variable: ',Expr,Span),
    Res=[out(CE)],NXA=XA,compile_body(Expr,F,XA,DEFS,CE).

compile_channel_value(in(Expr),F,XA,DEFS,Res,NXA,Span) :-
    compile_top_level_in_channel_value(Expr,F,XA,DEFS,Res,NXA,Span,warn),!.

compile_channel_value(inGuard(Var,Guard),F,XA,DEFS,Res,NXA,Span) :- Res = [inGuard(VarNew,NewGuard)],
    compile_in_channel_value(Var,XA,VarRes,NXA,Span,warn),
    %print(compile_inGuard(Var,Guard,Res)),nl,
    VarRes=[in(VarNew)],!,
    compile_body(Guard,F,XA,DEFS,NewGuard). % XA instead of NXA: the input value cannot be used in the set expression

compile_channel_value(E,F,XA,_,Res,NXA,Span) :-
    add_internal_error(haskell_csp_analyzer,'Illegal channel value or guard: ',E:F,Span), Res=[E],NXA=XA.

compile_head(Head,NewHead,Constraints,SPAN) :-
    Head =.. [Func|Args],
    l_compile_head_para(Args,NewArgs,Constraints,Head,SPAN),
    NewHead =.. [Func|NewArgs].

compile_head_para(Var,NewPara,Constraint,_Head,_Span) :- var(Var),!, NewPara=Var, Constraint=true.

compile_head_para(emptySet,NewPara,Constraint,_Head,_Span) :- !, Constraint=true, NewPara = setValue([]).

compile_head_para(listPat(List),NewPara,RestConstr,Head,Span) :- !, NewPara=list(NList),
    l_compile_head_para(List,NList,RestConstr,Head,Span).

compile_head_para(singleSetPat(List),NewPara,RestConstr,Head,Span) :- !, NewPara=setValue(NList),
    l_compile_head_para(List,NList,RestConstr,Head,Span).

compile_head_para(dotpat(List),NewPara,Constraint,Head,Span) :- !,
    % TO DO: check if we have a record constructor and can construct a record pattern: we would need no constraint
    Constraint = (pattern_match_function_argument(tuple(WNList),NewPara,Head),RestConstr),
    l_compile_head_para(List,NList,RestConstr,Head,Span),
    wrap_free_vars(NList,WNList). % wrap free vars with in(.)

compile_head_para(tuplePat(List),NewPara,Constraint,Head,Span) :- !, NewPara = na_tuple(NList),
    l_compile_head_para(List,NList,Constraint,Head,Span).

compile_head_para(alsoPattern([Pat1]),NewPara,Constraint1,Head,Span) :- !,
    compile_head_para(Pat1,NewPara,Constraint1,Head,Span).

compile_head_para(alsoPattern([Pat1|Tail]),NewPara,Constr,Head,Span) :- !,
    compile_head_para(Pat1,NewPara,Constraint1,Head,Span),
    compile_head_para(alsoPattern(Tail),NewPara2,Constraint2,Head,Span),
    Constr = (NewPara=NewPara2,Constraint1,Constraint2).

compile_head_para(appendPattern([Pat1]),NewPara,Constraint1,Head,Span) :- !,
    compile_head_para(Pat1,NewPara,Constraint1,Head,Span).

compile_head_para(appendPattern([H|T]),NewPara,Constraints,Head,Span) :-
    nonvar(H), H=listPat(HList),is_list_skeleton(HList),!,
    compile_head_para(H,NH,ConstraintH,Head,_), NH=list(NHList),
    NewPara = list(NewList),
    compile_head_para(appendPattern(T),NewT,ConstraintsT,Head,Span),
    Constraints = ','(ConstraintH,ConstraintsT),
    NewT = list(TList), append(NHList,TList,NewList).

compile_head_para(appendPattern(Pat),NewPara,Constraint,Head,Span) :-
    is_list_skeleton(Pat),
    append(T,[H],Pat),
    nonvar(H), H=listPat(HList),is_list_skeleton(HList),!,
    compile_head_para(H,NH,ConstraintH,Head,_), NH=list(NHList),
    compile_head_para(appendPattern(T),NewT,ConstraintsT,Head,Span),
    NewPara = list(NewList), NewT = list(TList),
    Constraint=','(ConstraintH,','(append(TList,NHList,NewList),ConstraintsT)).

compile_head_para(appendPattern(Pat),_,_,_Head,Span) :-
    %haskell_csp:get_symbol_span(Head,HeadSpan),
    add_error(compile_head_para,'Unsupported Append Pattern: ',Pat,Span),fail.

compile_head_para(X,_,_,Head,Span) :-
    atomic(X),
    channel(X,_), %print(Head),nl,
    (multiple_definitions(Head)
    -> add_message(compile_head_para,'Warning: Channel name used as Function/Process argument: ',X)
    ; % haskell_csp:get_symbol_span(Head,HeadSpan),
    add_error(compile_head_para,'Warning: Channel name used as Function/Process argument: ',X, Span)
    ),
    fail.

compile_head_para(X,NewPara,Constraint,_Head,_Span) :-
    atomic(X), evaluate_argument(X,NewPara), !,
    %% print(compiled_head_para(X,NewPara)),nl,
    Constraint=true.

compile_head_para(P,P,true,_Head,_Span).

compile_in_channel_value(Expr,XA,[ResTerm],NXA,Span,Warn) :- !,
    add_extra_input_variable(Expr,XA,NXA,Res,Span),
    (XA==NXA ->
    %add_error(haskell_csp_analyzer,'Channel input contains no variable: ',Expr,Span)
    (Warn=nowarn -> true
    ; add_message(haskell_csp_analyzer,'CSP Warning: Channel input contains no variable: ',Expr,Span)),
    ResTerm = out(Res)
    ; ResTerm=in(Res)).

compile_let(agent_curry(Fun,Body,SRCSPAN),F,XARGS,DEFS,DC) :- !,
    translate_agent_curry(Fun,Body,TFun,TBody,SRCSPAN),
    compile_let(agent(TFun,TBody,SRCSPAN),F,XARGS,DEFS,DC).

compile_let(agent(Fun,Body,SRCSPAN),F,XARGS,DEFS,DC) :-
    /* TO DO: treat multiple agent facts for same fun ;; DONE ?? */
    ( is_local_let(Fun,DEFS,NewFun,_FXArgs,_)
    -> term_variables(Fun,ArgumentsToFun),
    append(XARGS,ArgumentsToFun,NewXARGS),
    debug_println(5,compile_within_let(Fun,NewXARGS)),
    compile_body(Body,F,NewXARGS,DEFS,DC,Res), /* one could pass NewF instead of F */
    % portray_clause( let_agent(NewFun,Res) ),
    assert_agent(NewFun,Res,SRCSPAN)
    %print(assert_agent(NewFun,Res,SRCSPAN)),nl
    ; add_internal_error(haskell_csp,'Could not find let function in defs: ',(Fun,DEFS),SRCSPAN)
).

compile_lets([],_F,_XA,_D,_DC).

compile_lets([L1|T],F,XA,D,DC) :-
    compile_let(L1,F,XA,D,DC), compile_lets(T,F,XA,D,DC).

compile_nested_let_expressions :- debug_println(5,'% Compiling nested let expressions:'),
    retractall(agent_compiled(_,_,_)),
    retractall(agent_parameters(_,_,_)),
    init_agent_functor, reset_cur_numbervars_index,
    get_agent(X,Body,SRCSPAN),
    (var(X) ->
    add_internal_error(haskell_csp,'Error in compiled .pl File: Uninstantiated LHS in bindval or agent',(X,Body),SRCSPAN),fail
    ; true),
    compile_head(X,NX,Constraints,SRCSPAN),
    debug_println(5,compiled_head(X,NX,Constraints)),
   
    NX=..[F|_N_XARGS],
    (debug_mode(on) -> print(' '),print_agent(X),nl ; true),
    term_variables(X,InnerVariables), XARGS=InnerVariables, % these are the variables before extracting pattern matches into Constraints
    %debug_println(9,compiling_body(Body,F,_N_XARGS,XARGS)),
    (compile_body(Body,F,XARGS,[],Res)
    -> true
    ; add_internal_error(haskell_csp,'Unable to compile body of agent: ',agent(X,Body),SRCSPAN), fail
    ),
    assert_agent_compiled_head(NX,Res,SRCSPAN,Constraints),
    % (Constraints = true -> assert_agent_compiled(NX,Res,SRCSPAN) ; assert_agent_compiled(NX,Res,SRCSPAN,Constraints)),
    %portray_clause( (agent_compiled(NX,Res) :- Constraints)),
    fail.

compile_nested_let_expressions :- (debug_mode(on) -> nl ; true).

compile_top_level_in_channel_value(Expr,F,XA,DEFS,Res,NXA,Span,_) :- % print(compile(Expr,XA,Res,NXA)),nl,
    nonvar(Expr),Expr = dotpat(List),
    List=[H|T], \+ is_csp_constructor(H),!, % we have a ?(x.y) --> treate like ?x?y
    compile_top_level_in_channel_value(H,F,XA,DEFS,R1,NXA1,Span,nowarn),append(R1,R2,Res),
    compile_top_level_in_channel_value(dotpat(T),F,NXA1,DEFS,R2,NXA,Span,nowarn).

compile_top_level_in_channel_value(Expr,F,XA,DEFS,Res,NXA,Span,_) :-
    nonvar(Expr),Expr = dotpat(List),
    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))]),
    l_compile_channel_value(LL,F,XA,DEFS,Res,NXA,Span).

compile_top_level_in_channel_value(Expr,_F,XA,_DEFS,Res,NXA,_Span,_) :- % print(compile(Expr,XA,Res,NXA)),nl,
    nonvar(Expr),Expr = dotpat(List),List=[],!, % we have a ?(x.y) --> treate like ?x.?y
    Res = [],NXA=XA.

compile_top_level_in_channel_value(Expr,_F,XtraArgs,_DEFS,Res,NewXtraArgs,Span,WarnIfNoVariables) :-
    compile_in_channel_value(Expr,XtraArgs,Res,NewXtraArgs,Span,WarnIfNoVariables).

comprehension_aux(listExp(rangeEnum(Tuples),Generators),listComp, Vars , Generators, InScope) :-
    InScope = Tuples,
    extract_variables_from_generator_list(Generators,Vars).

comprehension_aux(setExp(rangeEnum(Tuples),Generators), setComp, Vars , Generators, InScope) :-
    InScope = Tuples,
    extract_variables_from_generator_list(Generators,Vars).

comprehension_aux(procRenamingComp(A,Generators,RenameList),procRenamingComp,Vars,OutsideOfScope,InScope) :-
    OutsideOfScope = [A|Generators],
    InScope = RenameList,
    extract_variables_from_generator_list(Generators,Vars).

compute_lazy_strict_types([],[]).

compute_lazy_strict_types([H|T],[HT|TT]) :-
    (var(H) -> HT=lazy ; HT=strict),
    compute_lazy_strict_types(T,TT).

csp_clause(Clause) :- channel_type_list(C,T),
    format_to_codes('~q.~N',[channel_type_list(C,T)],Clause).

csp_clause(Clause) :- name_type(C,T),
    format_to_codes('~q.~N',[name_type(C,T)],Clause).

csp_clause(Clause) :-
    haskell_csp_analyzer:agent_compiled_with_constraints(Head,Body,_Span,Constr),
    functor(Head,F,A),
    (agent_parameters(F,A,List) -> true ; List = no_agent_parameter_fact),
    numbervars((Head,Body,Constr),0,_),
    %portray_clause((Head :- Body)),
    ((List=[],Constr=true) -> format_to_codes('~q :-~N ~q.~N',[Head,Body],Clause)
    ; List=[] -> format_to_codes('~q :- ~q, /* Constraints */~N ~q.~N',[Head,Constr,Body],Clause)
    ; Constr\=true -> format_to_codes('~q :- /* ~p */~N ~q, /* Constraints */~N ~q.~N',[Head,List,Constr,Body],Clause)
    ; format_to_codes('~q :- /* ~p */~N ~q.~N',[Head,List,Body],Clause)).

csp_constant(C,T) :- csp_full_type_constant(C,T).

csp_constant(C,T) :- csp_sub_type_constant(C,T).

csp_constructor(C,T,A) :- csp_full_type_constructor(C,T,A).

csp_constructor(C,T,A) :- csp_sub_type_constructor(C,T,A).

csp_full_type_constant(apples,'FRUIT'). csp_full_type_constant(oranges,'FRUIT'). csp_full_type_constant(pears,'FRUIT'). % complementary to default CSP-M spec

csp_full_type_constant(apples,'FRUIT'). csp_full_type_constant(oranges,'FRUIT'). csp_full_type_constant(pears,'FRUIT'). % complementary to default CSP-M spec

csp_full_type_constant(apples,'FRUIT'). csp_full_type_constant(oranges,'FRUIT'). csp_full_type_constant(pears,'FRUIT'). % complementary to default CSP-M spec

csp_listing :-
    nl,
    agent_compiled_without_constraints(Head,Body,_Span),
    portray_clause((Head :- Body)),
    functor(Head,F,A),
    (agent_parameters(F,A,List)
    -> (List=[] -> true ; (print(' /* '), print(List), print('*/')))
    ; print(' **** NO agent_parameter fact ! ****')
    ),nl,
    fail.

csp_listing.

csp_span(no_loc_info_available).

csp_span(src_span(_,_,_,_,_,_)).

csp_span(src_position(_,_,_,_)).

csp_span(span_info(_,_)).

csp_span(multi_span(_,_,_,_,_,_,_)).

csp_span(src_span_operator(_,_)).