csp_sets

add_element(El,S,Res) :- Res = setValue(R), expand_symbolic_set(S,setValue(ES),add_element),
    (is_a_set(El) -> expand_symbolic_set(El,ExEl,add_element) ; ExEl=El), % normalise element before storing in set
    when(ground(ExEl),add_element1(ES,ExEl,R)).

add_element1([],El,[El]).

add_element1([H|T],El,Res) :- when(?=(El,H),(El @=<H -> (El=H -> Res = [El|T] ; Res = [El,H|T])
    ; (Res=[H|R2],add_element1(T,El,R2)))).

add_variables([],TVar,TVar,_).

add_variables([Var|T],TVar,Res,Set) :-
    (exact_member(Var,TVar)
    -> (add_error(csp_sets,'Variable appears twice in Generator list:',
    (Var,[comprehensionGenerator(Var,Set)|T])),
    /* TODO: FIX; this is actually allowed ?? !! */
    TVar1 = TVar)
    ; TVar1 = [Var|TVar]),
    add_variables(T,TVar1,Res,Set).

big_inter(S1,Res) :-
    expand_symbolic_set(S1,setValue(ES1),big_inter),
    (ES1 = [H|T]
    -> big_inter_del(T,H,Res)
    ; (add_error(csp_sets,'At least one set needed for Inter: ','Inter'(S1)),
    fail)
).

big_inter_del([],R,R).

big_inter_del([H|T],S2,Res) :- inter_set(H,S2,S3),
    big_inter_del(T,S3,Res).

big_union(S1,Res) :- %print(big_union(S1,Res)),nl,
    expand_symbolic_set(S1,setValue(ES1),big_union),
    %%print(big2(ES1)),nl,
    big_union_add(ES1,setValue([]),Res). %, print(big_res(Res)),nl.

big_union_add([],R,R).

big_union_add([H|T],S2,Res) :- union_set(H,S2,S3),
    big_union_add(T,S3,Res).

binary_set_op(builtin_call(X),A,B) :- binary_set_op(X,A,B).

binary_set_op(union(A,B),A,B).

binary_set_op(diff(A,B),A,B).

binary_set_op(inter(A,B),A,B).

blocking_member(X,[H|T]) :-
    (equal_element(X,H) ; blocking_member(X,T)).

cardinality(setValue(S),R) :- my_length(S,C),!,R=int(C).

cardinality(setFromTo(Low,Up),R) :- !,
    R=int(C), when((ground(Low),ground(Up)),compute_from_to_cardinality(Low,Up,C)).

cardinality(setFrom(Low),_) :- !,
    add_error(csp_sets,'Trying to compute cardinality of infinite set: ',set_from(Low)),fail.

cardinality(closure(ChannelList),R) :- !,my_length(Closure,C), R=int(C), when(ground(ChannelList),
    expand_symbolic_set(closure(ChannelList),setValue(Closure),closure_cardinality)).

cardinality(dataType(DT),R) :- !,R=int(C),my_length(DTSet,C),expand_symbolic_set(dataType(DT),setValue(DTSet),datatype_set_cardinality).

cardinality(X,_R) :- add_error(csp_sets,'Could not compute card of: ',X),fail.

check_sorted(Src,PrevH,H) :- ((PrevH=none;PrevH @< H) -> true ; add_error(Src,'CSP set not sorted: ',[PrevH,H])).

check_variable(V) :- atomic(V), channel(V,_),!,
    add_error(csp_sets,'Channel name used for local variable: ',V).

check_variable(_).

clever_bool_and(true,X,R) :- !,R=X.

clever_bool_and(X,true,R) :- !,R=X.

clever_bool_and(G1,G2,bool_and(G1,G2)).

closure_expand(ListOfEls,setValue(ExpandedList)) :-
    %print(closure_expand(ListOfEls)),nl,
    when(ground(ListOfEls),
    (findall(EEl,(member(El,ListOfEls),
    closure_expand_single_element(El,EEl)),EEls),
    %print(expanded(EEls)),nl,
    sort(EEls,ExpandedList) /* is sort ok wrt to @< used by various set operations?? */
)).

closure_expand_single_element(tuple([Ch|List]),R) :-
    channel_type_list(Ch,ChannelTypeList),!, R = tuple([Ch|NewList]),
    %print(tuple([Ch|NewList],ChannelTypeList)),nl,
    %% print(gen_expanded_list(ChannelTypeList,List,NewList,Ch)),nl,
    gen_expanded_list(ChannelTypeList,List,NewList,Ch).

closure_expand_single_element(Cons,C) :-
    is_csp_constructor(Cons),!,
    csp_constructor(Cons,DT,_ArgSubTypes),
    %print(csp_constructor(Cons,DT,_ArgSubTypes)),nl,
    C=record(Cons,_Fields),
    enumerate_datatype_el(DT,C,_Ch,2,no_loc_information).

closure_expand_single_element(tuple([Ch|_]),_R) :- !,
    add_error(csp_sets,'Cannot compute closure: This is not a defined channel: ',Ch),
    fail.

closure_expand_single_element(X,_R) :-
    add_error(csp_sets,'Cannot expand closure: ',X),
    fail.

compute_from_to_cardinality(Low,Up,C) :-
    (Up<Low ->
    C is 0
    ; C is Up-Low+1
).

deconstruct_setValue([H|T],H,T).

deconstruct_set_of_sets(setExp(rangeEnum([H|T])),H,setExp(rangeEnum(T))).

deconstruct_set_of_sets(setValue(V),H,setValue(T)) :- deconstruct_setValue(V,H,T).

diff_elements([],_,[]).

diff_elements([H|T],S2,Res) :-
    (remove_element(H,S2,S3)
    -> diff_elements(T,S3,Res)
    ; (Res=[H|R2], diff_elements(T,S2,R2))
).

diff_set(S1,S2,Res) :- Res = setValue(R), expand_symbolic_set(S1,setValue(ES1),diff_set1),
    expand_symbolic_set(S2,setValue(ES2),diff_set2),
    when(ground((ES1,ES2)),diff_elements(ES1,ES2,R)).

empty_set_of_sets(setExp(rangeEnum([]))).

empty_set_of_sets(setValue(X)) :- is_empty_list(X,true).

enum_sub2([],[]).

enum_sub2([El|T],Res) :-
    (Res = [El|T2], enum_sub2(T,T2))
    ; enum_sub2(T,Res).

enum_subset(S,setValue(Subset)) :- expand_symbolic_set(S,setValue(ES),enum_subset),
    enum_sub2(ES,Subset).

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

equal_element(true,X) :- !,
    ( X=true -> true
    ; X=false -> fail
    ; add_error_fail(haskell_csp,'Type error in equality: ',true=X)
).

equal_element(false,X) :- !,
    ( X=false -> true
    ; X=true -> fail
    ; add_error_fail(haskell_csp,'Type error in equality: ',false=X)
).

equal_element(int(X),R) :- !,
    (R=int(Y) -> X=Y
    ; add_error_fail(haskell_csp,'Type error in equality: ',int(X)=R)
).

equal_element(setFrom(X),R) :- !,
    (R=setFrom(Y) -> X=Y
    ; is_a_set(R) -> fail
    ; add_error_fail(haskell_csp,'Type error in equality: ',setFrom(X)=R)
).

equal_element(setFromTo(X,Y),R) :- !,
    (R=setFromTo(X2,Y2) -> X=X2,Y=Y2
    ; (R=setValue(_) ;R=setExp(_,_)) -> equal_sets(setFromTo(X,Y),R)
    ; is_a_set(R) -> fail % Set different for setValue and setExp
    ; add_error_fail(haskell_csp,'Type error in equality: ',setFromTo(X,Y)=R)
).

equal_element(setValue(X),R) :- !,
    (R=setValue(Y) -> equal_setValue(X,Y)
    ; R=setFrom(_) -> fail % infinite set cannot be equal to finite one
    ; is_a_set(R) -> expand_symbolic_set(R,setValue(ER),equal_element), equal_setValue(X,ER)
    ; add_error_fail(haskell_csp,'Type error in equality: ',setValue(X)=R)
).

equal_element(list(X),R) :- !,
    (R=list(Y) -> X=Y
    ;add_error_fail(haskell_csp,'Type error in equality: ',list(X)=R)
).

equal_element(na_tuple(X),R) :- !,
    (R=na_tuple(Y) -> X=Y
    ;add_error_fail(haskell_csp,'Type error in equality: ',na_tuple(X)=R)
).

equal_element(tuple(X),R) :- !,
    ( R=tuple(Y) -> (X=Y ; equal_interleaved_dot_tuples(X,Y))
    ; R=record(C,A) -> X=[H|T], C=H, (T=A ; equal_interleaved_dot_tuples(T,A))
    ; add_error_fail(haskell_csp,'Type error in equality: ',tuple(X)=R)
).

equal_element(dotTuple(X),R) :- !,
    ( R=tuple(Y) -> (X=Y ; equal_interleaved_dot_tuples(X,Y))
    ; R=record(C,A) -> X=[H|T], C=H, (T=A ; equal_interleaved_dot_tuples(T,A))
    ; add_error_fail(haskell_csp,'Type error in equality: ',dotTuple(X)=R)
).

equal_element(record(C,A),R) :-
    get_constructor_type(C,Type),!,
    ((R=record(C2,A2),get_constructor_type(C2,Type)) -> C=C2,(A=A2 ; equal_interleaved_dot_tuples(A,A2)) % missing subtype checks
    ; R=tuple([H|T]) -> (H=C,(T=A ; equal_interleaved_dot_tuples(A,T)))
    ; (atomic(R),get_constant_type(R,Type)) -> fail
    ; R=agent_call(_,_,_) -> force_evaluate_argument(R,Res),equal_element(record(C,A),Res)
    ; add_error_fail(haskell_csp,'Type error in equality: ',record(C,A)=R)
).

equal_element(X,R) :-
    atomic(X),get_constant_type(X,Type),!,
    ((atomic(R),get_constant_type(R,Type)) -> X=R
    ;(R=record(C,_Args),get_constructor_type(C,Type)) -> fail
    ; add_error_fail(haskell_csp,'Type error in equality: ',X=R)
).

equal_element(Set,R) :-
    is_a_set(Set),!,
    expand_symbolic_set(Set,ES,equal_element),
    equal_element(ES,R).

equal_element(X,Y) :- print(equal_element(X,Y)),nl,X=Y.

equal_interleaved_dot_tuples(X,Y) :-
    unify_tuple_elements(X,Y,R,tuple),
    (X=R -> true; unfold_dot_tuples(X,XR),XR=R).

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

equal_setValue(L1,L2) :-
    maplist(equal_element,L1,L2).

equal_sets(setFromTo(X,Y),R) :-
    ((R=setValue(S),ground((X,Y,S))) ->
    cardinality(setFromTo(X,Y),int(N)),
    length(S,N),
    expand_from_to(X,Y,XYSet),
    diff_elements(XYSet,S,[])
    ;
    expand_symbolic_set(setFromTo(X,Y),ES,equal_element),
    equal_element(ES,R)
).

evaluate_closure(X,closure(RS)) :- (X=tuple(XList) -> true ; X=XList),
    evaluate_set(XList,setValue(RS)).%evaluate_set(XList,setValue(RS),evaluate_argument).

evaluate_set([],R) :- !, R=setValue([]).

evaluate_set([H|T],R) :- !, haskell_csp:evaluate_argument(H,EH), evaluate_set(T,ET),
    add_element(EH,ET,R).

evaluate_set(X,_) :- add_internal_error('Internal Error: Could not evaluate: ',evaluate_set(X,_)),fail.

expand_constructor_to_record(Cons,DT,MaxRec,Res) :-
    Res=record(Cons,_L),
    enumerate_datatype_el(DT,Res,_Channel,MaxRec,no_loc_info_available).

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

expand_datatypedefbody([constructor(C)|T],DT,R,Context) :- !, R=[C|ET],
    expand_datatypedefbody(T,DT,ET,Context).

expand_datatypedefbody([constructorC(Cons,Type)|T],DT,R,Context) :- !,
    (haskell_csp:channel_type_is_finite(Type,2) ->
    findall(Record,csp_sets:expand_constructor_to_record(Cons,DT,2,Record),L),
    append(L,RT,R),
    expand_datatypedefbody(T,DT,RT,Context)
    ; add_error(csp_sets, 'Could not expand infinite datatype body: ',constructorC(Cons,Type):context(Context)),fail
).

expand_datatypedefbody(L,_DT,R,Context) :-
    add_internal_error('Internal Error: Could not expand datatype body (potentially infinite): ',L:context(Context)),
    R=[].

expand_from_to(X,Y,R) :- expand_from_to2(X,Y,R).

expand_from_to2(X,Y,R) :- X>Y,!, R=[].

expand_from_to2(X,Y,[int(X)|T]) :- X1 is X+1, expand_from_to2(X1,Y,T).

expand_set_comprehension(RangeExpr,GeneratorList,Res) :-
    %%%% print(expand_set_comprehension(RangeExpr,GeneratorList,Res)),nl,
    get_waitvars_for_generator_list(GeneratorList,WaitVars),
    %print(get_waitvars_for_generator_list(GeneratorList,WaitVars)),nl,
    when(ground(WaitVars), generate_set_comprehension_solutions(RangeExpr,GeneratorList,Res)).

expand_symbolic_set(X,R,Context) :- var(X),!,
    add_error(expand_symbolic_set,'Variable argument for expand_symbolic_set, Context: ',Context),
    R=X.

expand_symbolic_set(dataType(T),R,Context) :- !, R=setValue(SET),
    (dataTypeDef(T,Def)
    -> %print(dt(T,Def,SET)),nl,
    expand_datatypedefbody(Def,T,SET,Context)
    ; add_error(csp_sets,'Could not expand dataType. No datatype definition for: ',T:context(Context)),
    SET=[]
).

expand_symbolic_set(closure(X),R,_Context) :- !, closure_expand(X,R).

expand_symbolic_set(setValue(X),R,_Context) :- !, R=setValue(X).

expand_symbolic_set(setFrom(X),R,Context) :- !, add_warning(expand_symbolic_set,'Warning: Tried to expand infinite set: ',setFrom(X):context(Context)),R=setFrom(X).

expand_symbolic_set(setFromTo(Low,Up),R,_Context) :- !,R=setValue(RS),expand_from_to(Low,Up,RS).

expand_symbolic_set(setExp(RangeExpr,GeneratorList),R,_Context) :- !,
    expand_set_comprehension(RangeExpr,GeneratorList,R).

expand_symbolic_set(listFromTo(X,Y),_,Context) :-
    add_error(expand_symbolic_set,'Type error; expected set: ',listFromTo(X,Y):context(Context)),fail.

expand_symbolic_set(agent_call(Span,F,Par),R,Context) :- !,
    force_evaluate_argument(agent_call(Span,F,Par),RF),
    expand_symbolic_set(RF,R,Context).

expand_symbolic_set(boolType,R,_Context) :- !, R = setValue([true,false]).

expand_symbolic_set(dotTupleType(L),R,_Context) :- !, % we want to expand some more complicated Types like {0..2}.({0..2},{0..2})
    %print(expand_symbolic_set(dotTupleType(L))),nl,
    l_unfold_datatype_dot_tuple([dotTupleType(L)],RL),
    findall(Val,haskell_csp: enumerate_channel_input_value2(dotTupleType(RL),Val,_Ch,2,no_loc_info_available),Set),
    R = setValue(Set).

expand_symbolic_set(typeTuple(L),R,_Context) :- !,
    haskell_csp: evaluate_type_list(L,LR),
    findall(Val,haskell_csp: enumerate_channel_input_value2(typeTuple(LR),Val,_Ch,2,no_loc_info_available),Set),
    R = setValue(Set).

expand_symbolic_set(Set,R,Context) :-
    add_error(expand_symbolic_set,'Could not expand set: ',Set:context(Context)),R=Set.

extract_local_variables_from_generator_list([],R) :- !,R=[].

extract_local_variables_from_generator_list([comprehensionGuard(_)|T],Res) :- !,
    extract_local_variables_from_generator_list(T,Res).

extract_local_variables_from_generator_list([comprehensionGenerator(Var,Set)|T],Res) :- !,
    check_variable(Var),
    extract_local_variables_from_generator_list(T,TVar),
    term_variables(Var,Vars),
    add_variables(Vars,TVar,Res1,Set),
    extract_local_variables_from_set_expression(Set,Res1,Res).

extract_local_variables_from_generator_list(X,R) :-
    add_internal_error('Not a generator list: ', X),
    R=[].

extract_local_variables_from_set_expression(X,I,O) :- var(X),!,
    %add_error(extract_local_variables_from_set_expression,'Variable expr. :',X),
    I=O.

extract_local_variables_from_set_expression(Set,InVar,OutVar) :- unary_set_op(Set,A),!,
    extract_local_variables_from_set_expression(A,InVar,OutVar).

extract_local_variables_from_set_expression(Set,InVar,OutVar) :- binary_set_op(Set,A,B),!,
    extract_local_variables_from_set_expression(A,InVar,V1),
    extract_local_variables_from_set_expression(B,V1,OutVar).

extract_local_variables_from_set_expression(setEnum(List),InVar,OutVar) :- !,
    l_extract_local_variables_from_set_expression(List,InVar,OutVar).

extract_local_variables_from_set_expression(closureComp(Generators,Set),In,Out) :- !,
    extract_local_variables_from_generator_list(Generators,GV),
    add_variables(GV,In,Out,Set).

extract_local_variables_from_set_expression(setExp(RangeExpr,Generators),In,Out) :- !,
    extract_local_variables_from_generator_list(Generators,GV),
    add_variables(GV,In,Out,RangeExpr).

extract_local_variables_from_set_expression(_Set,In,Out) :-
    %print(uncovered_set_extract(_Set)),nl,
    Out=In.

extract_variables_from_generator_list([],R) :- !,R=[].

extract_variables_from_generator_list([comprehensionGuard(_)|T],Res) :- !,
    extract_variables_from_generator_list(T,Res).

extract_variables_from_generator_list([comprehensionGenerator(Var,Set)|T],Res) :- !,
    check_variable(Var),
    extract_variables_from_generator_list(T,TVar),
    term_variables(Var,Vars),
    add_variables(Vars,TVar,Res,Set).

extract_variables_from_generator_list(X,R) :-
    add_internal_error('Not a generator list: ', X),
    R=[].

force_evaluate_set([],R) :- !, R=setValue([]).

force_evaluate_set([H|T],R) :- !, haskell_csp:force_evaluate_argument(H,EH),
    force_evaluate_set(T,ET),
    add_element(EH,ET,R).

force_evaluate_set(X,_) :- add_internal_error('Interal Error: Could not evaluate: ',force_evaluate_set(X,_)),fail.

gen_expanded_list([],List,[],Channel) :-
    (List=[] ->
    true
    ; add_error(csp_sets,'Pattern list too long for channel: ',(List,Channel))
).

gen_expanded_list([Type|TT],List,Res,Channel) :-
    (List=[H|LT]
    -> (is_incomplete_record(H,CompletedH,RecType)
    -> ((LT==[] ->
    true
    ; add_error(gen_expanded_list,'Incomplete Record at non-tail position:',Channel:H)
    ),
    enumerate_channel_input_value(dataType(RecType),CompletedH,Channel,no_loc_info_available),
    %%print(enum(Type,CompletedH,Channel)),nl,
    Res = [CompletedH|RT]
    )
    ; Res=[H|RT]
    )
    ; Res=[NewEl|RT],LT=List, /* is it ok not to put dot(NewEl) here ? */
    enumerate_channel_input_value(Type,NewEl,Channel,no_loc_info_available)
    ),
    gen_expanded_list(TT,LT,RT,Channel).

generate_replicate_set_comprehension_solutions(ExprList,GeneratorList,Res) :-
    treat_generators(GeneratorList,GenVars,Sets,Guard),
    findall(EExpr,get_replicate_generators_solution(Guard,GenVars,ExprList,Sets,EExpr),Expressions),
    evaluate_set(Expressions,Res).%evaluate_set(Expressions,Res,evaluate_argument).

generate_set_comprehension_solutions(RangeExpr,GeneratorList,Res) :-
    treat_generators(GeneratorList,GenVars,Sets,Guard),
    findall(EExpr,get_generators_solution(Guard,GenVars,RangeExpr,Sets,EExpr),Expressions),
    %print(force_evaluate_set(Expressions,Res)),nl,
    force_evaluate_set(Expressions,Res).%evaluate_set(Expressions,Res,force_evaluate_argument).

generator_sol([],[],_Context).

generator_sol([Pattern|VT],[Set|ST],Context) :-
    (ground(Set) -> true ; print(generator_sol_set_non_ground(Set)),nl), % for nested set comprehension this could actually be non-ground
    translate_pattern(Pattern,TranslPattern),
    % print(evaluated_pattern(TranslPattern,Pattern,Set)),nl,
    (ground(TranslPattern) -> /* we do not need to enumerate; generator variable already ground */
    force_evaluate_argument_for_member_check(Set,ESet),
    is_member_set_alsoPat(TranslPattern,ESet)
    ; force_evaluate_argument(Set,EvSet),
    is_member_clpfd(TranslPattern,EvSet,Context)
    ),
    % print(gen_is_member(TranslPattern,Pattern,Set)),nl,
    generator_sol(VT,ST,Context).

geq(X,Low) :- X>=Low.

get_constant_type(C,Type) :- csp_full_type_constant(C,DataType),!,Type=DataType.

get_constant_type(C,Type) :- csp_full_type_constructor(C,DataType,_ArgTypes),!,
    % a type constructor is passed as an atomic value; some CSP specs do this (stc.csp of Kharmeh PhD spec)
    Type=constructor(DataType).

get_constant_type(C,_) :- add_internal_error(/*get_constant_type,*/'Internal Error: Unknown constant: ',C),fail.

get_constructor_type(C,Type) :- csp_full_type_constructor(C,DT,_ArgTypes),!,Type=DT.

get_constructor_type(C,_) :- add_internal_error(/*get_constructor_type,*/'Internal Error: Unknown record constructor: ',C),fail.

get_generators_solution(Guard,GenVars,RangeExpr,Sets,EExpr) :-
    check_boolean_expression(Guard),
    %print(generator_sol(guard(Guard),GenVars,Sets)),nl,
    generator_sol(GenVars,Sets,set), % unifies the variables of the comprehension generator expressions (e.g. x <- {0..10})
    %print(checking_range),nl,
    member_range_expr(RangeExpr,EExpr).

get_replicate_generators_solution(Guard,GenVars,ExprList,Sets,EExpr) :-
    check_boolean_expression(Guard),
    generator_sol(GenVars,Sets,replicated), % unifies the variables of the comprehension generator expressions (e.g. x <- {0..10})
    member(Expr,ExprList),
    evaluate_argument(Expr,EExpr).

get_waitvars_for_generator_list(GeneratorList,WaitVars) :-
    extract_local_variables_from_generator_list(GeneratorList,LocalVars),
    term_variables(GeneratorList,GVars),
    % Do not wait on local variables, they will never be grounded:
    remove_variables(GVars,LocalVars,WaitVars).

inter_merge_elements([],_R,[]).

inter_merge_elements([_|_],[],[]).

inter_merge_elements([H1|T1],[H2|T2],Res) :-
    (equal_element(H1,H2)
    -> (Res = [H1|TR], inter_merge_elements(T1,T2,TR))
    ; (H1@<H2 -> inter_merge_elements(T1,[H2|T2],Res)
    ; inter_merge_elements([H1|T1],T2,Res)
)
).

inter_merge_elements_from([],_Low,[]).

inter_merge_elements_from([int(H)|T],Low,Res) :-
    ((Low =< H) ->
    Res = [int(H)|TR], inter_merge_elements_from(T,Low,TR)
    ;
    inter_merge_elements_from(T,Low,Res)
).

inter_set(S1,S2,Res) :- Res = setValue(R),
    (S1=setFrom(Low) ->
    expand_symbolic_set(S2,setValue(ES2),inter_set1),
    when(ground((Low,ES2)),inter_merge_elements_from(ES2,Low,R))
    ;S2=setFrom(Low) ->
    expand_symbolic_set(S1,setValue(ES1),inter_set2),
    when(ground((ES1,Low)),inter_merge_elements_from(ES1,Low,R))
    ;
    expand_symbolic_set(S1,setValue(ES1),inter_set1),
    expand_symbolic_set(S2,setValue(ES2),inter_set2),
    when(ground((ES1,ES2)),inter_merge_elements(ES1,ES2,R))
).

is_a_set(setValue(_)).

is_a_set(closure(_)).

is_a_set(setFromTo(_,_)).

is_a_set(setFrom(_)).

is_a_set(intType).

is_a_set(boolType).

is_a_set(dataType(_)).

is_a_set(dotTupleType(_)).

is_a_set(setExp(_,_)).

is_a_set(closureComp(_,_)). % right?

is_a_set('Seq'(_)).

is_empty_set(setValue(X),R) :- !, is_empty_list(X,R).

is_empty_set(closure(X),R) :- !, is_empty_list(X,R).

is_empty_set(setFromTo(Low,Up),R) :- !, safe_less_than(Up,Low,R).

is_empty_set(setFrom(_),R) :- !, R=false.

is_empty_set(X,_) :- add_error(csp_sets,'Could not evaluate: ',is_empty_set(X)),fail.

is_incomplete_record(record(Constructor,Fields),record(Constructor,FullFields),Type) :-
    csp_full_type_constructor(Constructor,Type,SubTypes),
    length(SubTypes,NrReqArgs),
    length(Fields,NrFields),
    (NrReqArgs > NrFields
    -> ( %print(record_incomplete(Constructor,Fields,SubTypes)),nl,
    length(FullFields,NrReqArgs),
    append(Fields,_,FullFields)
    %print(completed(record(Constructor,FullFields))),nl
    )
    ; ((NrReqArgs<NrFields -> add_error(csp_sets,'Too many arguments for record: ',Constructor:Fields) ; true),
    fail)
).

is_member_clpfd(Pat,EvSet,_Context) :-
    expand_symbolic_set(EvSet,ESet,generator_sol),
    is_member_set_alsoPat(Pat,ESet).

is_member_comprehension_set(X,rangeEnum(ExprList),GeneratorList) :- ExprList=[Expr|TT],TT==[],var(Expr),!,
    get_waitvars_for_generator_list(GeneratorList,WaitVars),
    when(ground(WaitVars),
    (treat_generators(GeneratorList,Vars,Sets,Guard),
    % print(treat_generators(for(X,ExprList),Vars,Sets,Guard)),nl,
    Expr=X,
    check_boolean_expression(Guard),
    % print(checked(Guard,Vars,Sets)),nl,
    generator_sol(Vars,Sets,set))).

is_member_comprehension_set(X,ExprList,GeneratorList) :- !, %ExprList = [_,_|_],fail,!,
    /* if more than one element in ExprList:
    we need to expand it; we cannot instantiate the single variable and just check the generators,guards
    otherwise pending co-routines can occur (e.g., { x , x1 | x<-{1..4}, x1 <-{x+2..x+3} } )
    Also: currently we cannot check it symbolically if the elment of ExprList is not a variable */
    % print(expanding_comprehension_set(ExprList,GeneratorList)),nl,
    expand_set_comprehension(ExprList,GeneratorList,ExpandedSet),
    is_member_set(X,ExpandedSet).

is_member_comprehension_set(X,T,G) :-
    add_error_fail(is_member_comprehension_set,'Could not evaluate: ', is_member_comprehension_set(X,T,G)).

is_member_from(X,Low) :- X >= Low.

is_member_from_to(X,Low,Up) :- ground(X),!,geq(X,Low), leq(X,Up).

is_member_from_to(X,Low,Up) :- enumerate_csp_int(X,Low,Up).

is_member_inter(LS,El) :-
    (deconstruct_set_of_sets(LS,H,T) ->
    is_member_set2(H,El),
    (empty_set_of_sets(T) -> true ; is_member_set2('Inter'(T),El))
    ; empty_set_of_sets(T) -> add_error(is_member_set2,'Empty set not allowed for Inter(-): ',T)
    ; add_error_fail(is_member_set,'Illegal argument: ','Inter'(LS))).

is_member_set(El,S) :- is_member_set2(S,El).

is_member_set2(setValue(Set),El) :- !, blocking_member(El,Set).

is_member_set2(boolType,X) :- !, (X=true;X=false).

is_member_set2(intType,R) :- !, R=int(_).

is_member_set2(setFromTo(Low,Up),R) :- !, R=int(X),
    is_member_from_to(X,Low,Up).

is_member_set2(setFrom(Low),int(X)) :- !, is_member_from(X,Low).

is_member_set2('Seq'(X),C) :- expand_sequence(C,list(EC)), !, list_elements_member_set(EC,X).

is_member_set2('dotTupleType'(X),T) :- !,(T=tuple(TT) ; T=dotTuple(TT)), l_dot_is_member_set(TT,X). %%%%%% see trace output

is_member_set2('typeTuple'(X),T) :- !, T=na_tuple(TT), l_is_member_set(TT,X).

is_member_set2(dataType(DT),C) :- is_a_datatype(DT,L),!, % to do: precompute this
    ( (atomic(C),member(constructor(C),L)) ; ( C=record(Cons,Fields),
    csp_constructor(Cons,DT,ArgSubTypes),
    maplist(haskell_csp:get_value_alsoPat,Fields,Fields1), % could be possible that some of the elements are wrapped in in(.) or alsoPat(.,.)
    l_dot_is_member_set(Fields1,ArgSubTypes) )
).

is_member_set2(setExp(RangeExpr),C) :- !, is_member_set2(setExp(RangeExpr,[]),C).

is_member_set2(setExp(RangeExpr,GeneratorSet),C) :- !,
    is_member_comprehension_set(C,RangeExpr,GeneratorSet).

is_member_set2('Union'(LS),El) :- ground(El),!,is_member_union(LS,El).

is_member_set2('Union'(LS),El) :- !,force_evaluate_argument('Union'(LS),ES), is_member_set2(ES,El).

is_member_set2('Inter'(LS),El) :- !,is_member_inter(LS,El).

is_member_set2(agent_call(Span,F,Par),El) :- !, haskell_csp: unfold_function_call_once(F,Par,Body,Span),
    force_evaluate_argument_for_member_check(Body,R), is_member_set(El,R).

is_member_set2(closure(Cl),El) :- !, closure_expand(Cl,R),is_member_set(El,R).

is_member_set2(S,El) :- haskell_csp: name_type(S,Type),!,is_member_set2(Type,El).

is_member_set2(R,X) :- add_error(csp_sets,'Could not evaluate: ',is_member_set(X,R)),fail.