closures

check_bdy_aux(conjunct(A,B),InConstrained,OutConstrained) :- !,
    check_inf_cl_body(A,InConstrained,OutConstrained1),
    check_inf_cl_body(B,OutConstrained1,OutConstrained).

check_bdy_aux(disjunct(A,B),InConstrained,OutConstrained) :- !,
    (check_inf_cl_body(A,InConstrained,OutConstrained) -> true
    ; check_inf_cl_body(B,InConstrained,OutConstrained)).

check_bdy_aux(equal(LHS,RHS), Constrained, OutConstrained) :- !,
    (check_bdy_equal(LHS,RHS,Constrained,OutConstrained) -> true
    ; check_bdy_equal(RHS,LHS,Constrained,OutConstrained)),!.

check_bdy_aux(member(b(identifier(ID),TYPE,_),SET),Constrained,[ID/INFINITE|Constrained]) :- !,
    \+ member(ID/_,Constrained),
    rhs_safe(Constrained,SET), % avoid ID : {ID+1, ID+2}
    (is_infinite_type(TYPE)
    -> %check that SET is infinite; otherwise remove from IDs
    (definitely_infinite(SET) -> INFINITE=infinite;
    definitely_not_empty_and_finite(SET) -> INFINITE = finite
    )
    ; definitely_not_empty_and_finite(SET), % otherwise we may have no solution and the entire closure is empty
    INFINITE = finite
).

check_bdy_aux(member(LHS,RHS),Constrained,[ID/infinite|Constrained]) :- !, % ID'Field : SET
    record_field_access_with_infinite_rest_type(LHS,RHS,Constrained,ID), % should we also cater for finite rest?
    definitely_not_empty_set(RHS).

check_bdy_aux(not_equal(A,B),Constrained,[ID/infinite|TC]) :- !,
    (get_texpr_id(A,ID)
    -> is_static_expr_of_infinite_type(B) % we have to be careful that B does not directly or indirectly reference A
    ; get_texpr_id(B,ID),
    is_static_expr_of_infinite_type(A)
    ),
    (select(ID/Kind,Constrained,TC)
    -> Kind=infinite % if it was infinite it will remain infinite, we only discard a single static value
    ; TC=Constrained).

check_bdy_aux(truth,Constrained,OutConstrained) :- !, OutConstrained=Constrained.

check_bdy_aux(external_pred_call(FunName,_Args),Constrained,Constrained) :- !,
    external_pred_always_true(FunName).

check_bdy_aux(EXPR,Constrained,[ID/infinite|Constrained]) :-
    %% TO DO: store bounds in ID/... list to check if the domain remains infinite!
    greater_typing(EXPR,ID,_UP),
    \+ member(ID/_,Constrained).

check_bdy_aux(EXPR,Constrained,[ID/infinite|Constrained]) :-
    less_typing(EXPR,ID,_UP),
    \+ member(ID/_,Constrained).

check_bdy_equal(LHS,RHS, Constrained, [ID/equal|Constrained]) :-
    get_texpr_id(LHS,ID),
    \+ member(ID/_,Constrained), % no constraints on ID so far
    does_not_occur_in(ID,RHS),
    rhs_safe(Constrained,RHS),
    !. % the equation must have a solution; assuming well-definedness

check_bdy_equal(LHS,RHS, Constrained, [ID/infinite|Constrained]) :- % ID'FieldName = RHS
    % detect closures like {x|x:struct(a:INTEGER,b:BOOL) & x'b=FALSE}, see test 2483
    record_field_access_with_infinite_rest_type(LHS,RHS,Constrained,ID),!.

check_inf_cl_body(b(B,pred,_),InConstrained,OutConstrained) :-
    check_bdy_aux(B,InConstrained,OutConstrained).

check_result_instantiation(X,_) :- var(X),!.

check_result_instantiation(closure(_,_,_),_PP) :- !.

check_result_instantiation(X,PP) :-
    add_internal_error('Result already instantiated in incompatible way: ',check_result_instantiation(X,PP)).

combine_names_and_types(ID,Type,b(identifier(ID),Type,[])).

construct_closure(Parameters, ParameterTypes, Body, Res) :-
    Res = closure(Parameters, ParameterTypes, Body).

construct_closure_if_necessary(_,_,b(falsity,pred,_),Res) :- !, Res=[].

construct_closure_if_necessary([ID], [T1], b(Pred,pred,_), Res) :-
    construct_unary_closure(Pred,ID,T1,SET),!,
    Res = SET.

construct_closure_if_necessary(Parameters, ParameterTypes, Body, Res) :-
    Res = closure(Parameters, ParameterTypes, Body).

construct_complement_closure(Delta,Type,Closure) :-
    % print(generating_complement_closure(GlobalSet,Delta,Type)),nl,
    construct_not_member_closure('_zzzz_unary',Type,[],value(Delta),Closure).

construct_greater_equal_closure(X,Res) :-
    construct_closure(['_zzzz_unary'],[integer],
    b(greater_equal(b(identifier('_zzzz_unary'),integer,[]),
    b(value(int(X)),integer,[])), pred,[]),Res).

construct_less_equal_closure(X,Res) :-
    construct_less_equal_closure('_zzzz_unary',X,[],Res).

construct_less_equal_closure(ID,X,Info,Res) :-
    construct_closure([ID],[integer],
    b(less_equal(b(identifier(ID),integer,[]),
    b(value(int(X)),integer,[])), pred,Info),Res).

construct_member_closure(ID,Type,Info,ClosureSetExpression,Result) :-
    check_result_instantiation(Result,construct_member_closure(ID)),
    create_texpr(identifier(ID),Type,[],TIdentifier), % used to be [generated]
    extract_pos_infos(Info,PosInfo), % Note: safe_create_texpr will copy WD info
    safe_create_texpr(ClosureSetExpression,set(Type),PosInfo,TClosureSet), % TODO: we could store whether sub_expression_contains_wd_condition for next call
    safe_create_texpr(member(TIdentifier,TClosureSet),pred,PosInfo,TPred),
    construct_closure([ID],[Type],TPred,Result).

construct_not_member_closure(ID,Type,Info,ClosureSetExpression,Result) :-
    check_result_instantiation(Result,construct_not_member_closure(ID)),
    Type==integer,
    interval_up_to_inf(ClosureSetExpression,Limit),
    !,
    construct_less_equal_closure(ID,Limit,Info,Result). % construct an interval closure; better support in kernel for it

construct_not_member_closure(ID,Type,Info,ClosureSetExpression,Result) :-
    create_texpr(identifier(ID),Type,[],TIdentifier), % used to be [generated]
    safe_create_texpr(ClosureSetExpression,set(Type),Info,TClosureSet),
    safe_create_texpr(not_member(TIdentifier,TClosureSet),pred,Info,TPred),
    construct_closure([ID],[Type],TPred,Result).

construct_unary_closure(member(b(identifier(ID),T1,_),b(value(SET),set(T1),_)),ID,T1,Res) :- Res=SET.

construct_unary_closure(truth,_,T1,Res) :- try_b_type2global_set(T1,Res).

construct_unary_closure(equal(b(identifier(ID),T1,_),b(value(SET),T1,_)),ID,T1,Res) :-
    try_expand_and_convert_to_avl([SET],Res).

contains_infinite_type([ID|IT],[H|T],OutConstrained) :-
    (is_infinite_type(H),
    \+ member(ID/_,OutConstrained)
    -> true ; contains_infinite_type(IT,T,OutConstrained)).

convert_type_to_value(integer,global_set('INTEGER')).

convert_type_to_value(global(G),global_set(G)).

convert_type_to_value(boolean,BS) :- BS=[pred_true /* bool_true */,pred_false /* bool_false */]. % TO DO: generate AVL ?

convert_type_to_value(string,global_set('STRING')). % :- all_strings_wf(S,WF).

does_not_occur_in(ID,EXPR) :- \+ occurs_in_expr(ID,EXPR).

get_bound('NATURAL',0).

get_bound('NATURAL1',1).

get_domain_range_for_closure_types(Types,Domain,Range) :-
    couplise_list(Types,couple(Domain,Range)).

get_names_and_types(b(identifier(ID),Type,_),ID,Type).

get_recursive_identifier_of_closure(V,RID) :- nonvar(V), V=closure(_P,_T,B),
    get_recursive_identifier_of_closure_body(B,RID).

get_recursive_identifier_of_closure_body(b(_,_,BodyInfo),RID) :- member(prob_annotation(recursive(RID)),BodyInfo).

greater_typing(greater(b(identifier(ID),integer,_),b(VUP,integer,_)),ID,UP) :- is_integer_val(VUP,UP).

greater_typing(greater_equal(b(identifier(ID),integer,_),b(VUP,integer,_)),ID,UP) :- is_integer_val(VUP,UP).

greater_typing(less(b(VUP,integer,_),b(identifier(ID),integer,_)),ID,UP) :- is_integer_val(VUP,UP).

greater_typing(less_equal(b(VUP,integer,_),b(identifier(ID),integer,_)),ID,UP) :- is_integer_val(VUP,UP).

identifier_equality(b(equal(b(LHS,Type,LHSInfo),b(RHS,_TypeRHS,RHSInfo)),pred,_),ID,Type,EXPR,EXPRINFO) :-
    % no need to unify with TypeRHS; actually Prolog unification could fail due to seq types ?
    identifier_equality_aux(LHS,LHSInfo,RHS,RHSInfo,ID,EXPR,EXPRINFO).

identifier_equality_aux(identifier(ID),_,EXPR,EXPRINFO,ID,EXPR,EXPRINFO) :- !.

identifier_equality_aux(EXPR,EXPRINFO,identifier(ID),_,ID,EXPR,EXPRINFO).

interval_up_to_inf(global_set('NATURAL'),-1).

interval_up_to_inf(global_set('NATURAL1'),0).

interval_up_to_inf(value(global_set('NATURAL')),-1).

interval_up_to_inf(value(global_set('NATURAL1')),0).

is_closure(closure(Parameters, ParameterTypes, Body), Parameters, ParameterTypes, Body).

is_closure_or_integer_set(closure(P,T,B),P,T,B).

is_closure_or_integer_set(global_set(INTSET),
    ['_zzzz_unary'],[integer],
    b(greater_equal(
    b(identifier('_zzzz_unary'),integer,[]),
    b(integer(BOUND),integer,[])
    ),
    pred,
    [prob_annotation('SYMBOLIC')])
    ) :-
    get_bound(INTSET,BOUND).

is_full_id_closure(P,T,B) :- is_id_closure_over(P,T,B,_,true).

is_id_closure_over([ID1,ID2], [TYPE,TYPE],Body, ID_Domain, Full) :- nonvar(Body),
    Body=b(equal(b(identifier(ID1),TYPE,_),b(identifier(ID2),TYPE,_)),pred,_),
    !,
    convert_type_to_value(TYPE,ID_Domain), Full=true.

is_id_closure_over(Par,Types,Body,ID_Domain,Full) :- nonvar(Par),nonvar(Body),
    is_member_closure(Par,Types,Body,_,Set), % print(member_closure(Set)),nl,
    nonvar(Set),
    Set = identity(b(VAL,set(_TYPE),_)),
    nonvar(VAL), VAL=value(ID_Domain),
    (custom_explicit_sets:is_definitely_maximal_set(ID_Domain) -> Full=true ; Full=false).

is_infinite_equality_closure(IDs, TYPES, Body) :-
    %IDs = [_,_|_], % we used to require at least at least two variables
    \+ Body = b(member(_,_),_,_), % simple member closure; we deal with it separately (and avoid blow-up of checks, cf test 2283)
    check_inf_cl_body(Body,[],OutConstrained),
    % if we arrive here, we know that the body constraint is satisfiable
    (member(_ID/infinite,OutConstrained) -> true
    ; contains_infinite_type(IDs,TYPES,OutConstrained)).

is_infinite_non_injective_closure(closure(P,T,Body)) :-
    %see also bsyntaxtree:get_lambda_equality(Body,LambdaID,RestBody,ResultExpr),
    Body = b(equal(LHS,RHS),pred,_),
    get_texpr_id(LHS,LambdaID),
    get_texpr_id(RHS,ProjID), % TODO: get used ids and see if the rest is infinite
    append(Args,[LambdaID],P), Args = [_,_|_],
    nth1(Nr,Args,ProjID),
    nth1(Nr2,T,NonProjectedType),
    Nr2 \= Nr,
    is_infinite_type(NonProjectedType).

is_integer_val(integer(UP),UP).

is_integer_val(value(V),UP) :- nonvar(V),V=int(UP).

is_lambda_closure(Args,Types,ClosurePred, OtherIDs, OtherTypes, DOMAINPRED,Res) :-
    % TO DO: do this more efficiently: if LambdaID occurs in any non-equal predicate : stop searching
    % TO DO: check if is_infinite_equality_closure is not a special case of lambda closure ?
    append(OtherTypes,[LambdaType],Types), OtherTypes \= [],
    append(OtherIDs,[LambdaID],Args),
    Res=b(EXPR,LambdaType,EXPRINFO),
    %used to call: b_interpreter:member_conjunct(EQ,ClosurePred,DOMAINPRED), ; but inlined below for efficiency
    select_equality(ClosurePred,LambdaID,EXPR,LambdaType,EXPRINFO,DOMAINPRED),
    !. % avoid backtracking member_conjunct

is_lambda_comprehension_set(b(comprehension_set(Parameters,Body),_,_),LambdaParas,DomainPred,EXPR) :-
    maplist(get_names_and_types,Parameters,Args,Types),
    is_lambda_closure(Args,Types,Body, OtherIDs,OtherTypes, DomainPred, EXPR),
    maplist(combine_names_and_types,OtherIDs,OtherTypes,LambdaParas).

is_lambda_value_domain_closure(P,T,Pred, DomainValue,Expr) :-
    is_lambda_value_domain_memoization_closure(P,T,Pred, DV,E),!,
    DV \= fail, E\= fail,
    DomainValue=DV, Expr=E.

is_lambda_value_domain_closure(Args,Types,B, DomainValue, EXPR) :-
    is_lambda_value_domain_normal_closure(Args,Types,B, DomainValue, EXPR).

is_lambda_value_domain_normal_closure(Args,Types,B, DomainValue, EXPR) :-
    % tools_printing:print_term_summary(try_is_lambda_domain(Args,Types,B)),
    is_lambda_closure(Args,Types,B, OtherIDs,OtherTypes, DomainPred, EXPR),!,
    %print(lambda_closure(OtherIDs)), translate:print_bexpr(EXPR),nl,
    construct_closure_if_necessary(OtherIDs,OtherTypes,DomainPred,DomClosure),
    (is_symbolic_closure(Args,Types,B)
    -> mark_closure_as_symbolic(DomClosure,DomainValue)
    ; DomainValue = DomClosure).

is_member_closure([ID],[TYPE],b(PRED,_Pred,_), TYPE,SET) :-
    is_member_closure_aux(PRED, ID,TYPE,SET).

is_member_closure_aux(member(TID,TSET), ID,TYPE,SET) :-
    TID = b(identifier(ID),TYPE,_),
    TSET = b(SET,SETTYPE,_),
    is_set_type(SETTYPE,TYPE).

is_member_closure_aux(subset(TID,BSET), ID,TYPE,SET) :-
    TID = b(identifier(ID),TYPE,_),
    SET = pow_subset(BSET).

is_member_closure_with_info([ID],[TYPE],b(PRED,_Pred,Info), TYPE,Info,SET) :-
    is_member_closure_aux(PRED, ID,TYPE,SET).

is_not_member_closure([ID],[TYPE],b(PRED,_Pred,_),TYPE,SET) :-
    is_not_member_closure_aux(PRED,ID,TYPE,SET).

is_not_member_closure_aux(not_member(b(identifier(ID),TYPE,_),b(SET,set(TYPE),_)),ID,TYPE,SET).

is_not_member_closure_aux(not_equal(b(identifier(ID),TYPE,_),ONE),ID,TYPE,SET) :-
    (ONE = b(value(Val),_,_),
    ground_value(Val)
    -> custom_explicit_sets:construct_one_element_custom_set(Val,SetVal), SET = value(SetVal)
    ; SET = set_extension([ONE])).

is_not_member_global_set('INTEGER',integer,[]).

is_not_member_global_set('NATURAL',integer,X) :-
    construct_less_equal_closure(-1,X). % {x|x<0}.

is_not_member_global_set('NATURAL1',integer,X) :-
    construct_less_equal_closure(0,X). %X = {x|x<1}.

is_not_member_value_closure(closure(Par,T,B),TYPE,SET) :-
    is_not_member_closure(Par,T,B,TYPE,value(SET)).

is_not_member_value_closure_or_integerset(global_set(X),TYPE,SET) :- !,
    is_not_member_global_set(X,TYPE,SET).

is_not_member_value_closure_or_integerset(C,TYPE,SET) :- is_not_member_value_closure(C,TYPE,SET).

is_recursive_closure(V) :- nonvar(V), V=closure(P,T,B),
    is_recursive_closure(P,T,B).

is_recursive_closure(_P,_T,b(_,_,INFO)) :-
    member(prob_annotation('RECURSIVE'),INFO).

is_special_infinite_closure(Par,T,Body) :-
    is_infinite_equality_closure(Par,T,Body),!.

is_special_infinite_closure(Par,T,Body) :-
    is_not_member_closure(Par,T,Body,Type,value(_)), is_infinite_type(Type).

is_static_expr_of_infinite_type(b(E,Type,_)) :- is_static_expr_of_infinite_type2(E,Type).

is_static_expr_of_infinite_type2(integer(_),_).

is_static_expr_of_infinite_type2(string(_),_).

is_static_expr_of_infinite_type2(real(_),_).

is_static_expr_of_infinite_type2(value(V),Type) :- is_val_of_infinite_type(V,Type).

is_static_expr_of_infinite_type2(empty_set,Type) :- is_infinite_type(Type).

is_static_expr_of_infinite_type2(empty_sequence,Type) :- is_infinite_type(Type).

is_symbolic_closure(V) :- nonvar(V), V=closure(P,T,B),
    is_symbolic_closure(P,T,B).

is_symbolic_closure(_P,_T,b(_,_,INFO)) :-
    member(prob_annotation('SYMBOLIC'),INFO).

is_val_of_infinite_type(V,_) :- var(V),!,fail.

is_val_of_infinite_type(int(_),_).

is_val_of_infinite_type(string(_),_).

is_val_of_infinite_type(term(floating(_)),_).

is_val_of_infinite_type((A,B),couple(TA,TB)) :- (is_val_of_infinite_type(A,TA) -> true ; is_val_of_infinite_type(B,TB)).

is_val_of_infinite_type([],Type) :- is_infinite_type(Type).

is_val_of_infinite_type(avl_set(_),Type) :- is_infinite_type(Type).

less_typing(less(b(identifier(ID),integer,_),b(VUP,integer,_)),ID,UP) :- is_integer_val(VUP,UP).

less_typing(less_equal(b(identifier(ID),integer,_),b(VUP,integer,_)),ID,UP) :- is_integer_val(VUP,UP).

less_typing(greater(b(VUP,integer,_),b(identifier(ID),integer,_)),ID,UP) :- is_integer_val(VUP,UP).

less_typing(greater_equal(b(VUP,integer,_),b(identifier(ID),integer,_)),ID,UP) :- is_integer_val(VUP,UP).

mark_aux(P,T,b(Pred,pred,INFO),ANN,Res) :-
    (ground(INFO)
    -> mark_info(ANN,INFO,RINFO)
    ; add_error(mark_aux,'Info field not set: ',closure(P,T,b(Pred,pred,INFO))),
    RINFO=INFO),
    Res = closure(P,T,b(Pred,pred,RINFO)).

mark_closure(closure(P,T,B),ANN,R) :- !, mark_aux(P,T,B,ANN,R).

mark_closure(A,_,Res) :- A=Res. % not a closure

mark_closure3(_,ANN,R) :- nonvar(R), % we could use equal_object
    add_internal_error('Result already instantiated: ',mark_closure3(_,ANN,R)),fail.

mark_closure3(C,ANN,R) :- var(C), % we could use equal_object
    !,
    debug_println(19,not_marking_var_closure(C,ANN)),
    R=C.

mark_closure3(C,ANN,R) :- mark_closure(C,ANN,R).

mark_closure_as_recursive(C,R) :-
    mark_closure3(C,['SYMBOLIC','RECURSIVE'],R).

mark_closure_as_symbolic(C,R) :-
    mark_closure3(C,['SYMBOLIC'],R).

mark_info([],INFO,INFO).

mark_info([ANN|T],INFO,Res) :-
    (member(prob_annotation(ANN),INFO) -> Res=TRes ; Res = [prob_annotation(ANN)|TRes]),
    mark_info(T,INFO,TRes).

record_field_access_with_infinite_rest_type(LHS,RHS,Constrained,ID) :-
    LHS = b(record_field(TID,FieldName),_,_),
    get_texpr_id(TID,ID),
    \+ member(ID/_,Constrained), % no constraints on ID so far
    get_texpr_type(TID,record(FieldTypes)),
    select(field(FieldName,_),FieldTypes,RestTypes),
    % we now have only a single value for field FieldName
    is_infinite_type(record(RestTypes)), % there are still infinitely many values left given the other fields
    does_not_occur_in(ID,RHS),
    rhs_safe(Constrained,RHS),!.

rhs_safe([],_).

rhs_safe([HID/Kind|TConstrained],RHS) :-
    (Kind=infinite -> true % CHECK!
    ; %HID could be bound to new ID, e.g., via HID=NewID+1 and equation NewID=HID would have no solution
    does_not_occur_in(HID,RHS)
    ),
    rhs_safe(TConstrained,RHS).

select_equality(ClosurePred,ID,RHSExpr,Type,Info,RestPred) :-
    conjunction_to_list(ClosurePred,List),
    select(EQ,List,RestList),
    identifier_equality(EQ,ID,Type,RHSExpr,Info),
    !, % once we find a first equality : no need to look for a second one as then does_not_occur in RestPred will always fail !
    (ID='_lambda_result_',EQ=b(_,_,I),
    member(prob_annotation('LAMBDA-EQUALITY'),I)
    -> true % no need to perform occurs check in RHS, but in RestPred, cf test 1874
    ; %format('Check occurs ~w : ',[ID]), translate:print_bexpr(b(RHSExpr,Type,Info)),nl,
    does_not_occur_in(ID,b(RHSExpr,Type,Info))
    ),
    conjunct_predicates(RestList,RestPred),
    does_not_occur_in(ID,RestPred).