kernel_mappings

all_but_one([],_H,true).

all_but_one([H2|T],H1,KNOWN) :- known_value(H2,K2), known_value(H1,K1), all_but_one_wait(K1,K2,T,KNOWN).

all_but_one_set_known([],true).

all_but_one_set_known([H|T],KNOWN) :-
    (T==[] -> KNOWN=true
    ; all_but_one(T,H,KNOWN)).

all_but_one_wait(K1,K2,[],true) :- K1=true,K2=true.

all_but_one_wait(K1,K2,[H3|T],KNOWN) :- known_value(H3,K3),
    (var(K2) -> all_but_one_wait(K2,K3,T,KNOWN) ; all_but_one_wait(K1,K3,T,KNOWN)).

binary_arg1_determines_value(multiplication,A1,int(0)) :- zero(A1).

binary_arg1_determines_value(intersection,A1,[]) :- A1==[].

binary_arg1_determines_value(set_subtraction,A1,[]) :- A1==[].

binary_arg1_determines_value(domain_restriction,A1,[]) :- A1==[]. % first arg is set

binary_arg1_determines_value(range_subtraction,A1,[]) :- A1==[]. % first arg is rel

binary_arg1_determines_value(range_restriction,A1,[]) :- A1==[]. % first arg is rel

binary_arg1_determines_value(cartesian_product,A1,[]) :- A1==[].

binary_arg1_determines_value(composition,A1,[]) :- A1==[].

binary_arg1_determines_value(direct_product,A1,[]) :- A1==[].

binary_arg1_determines_value(parallel_product,A1,[]) :- A1==[].

binary_boolean_operator(not_equal,kernel_objects:not_equal_object_wf,yes).

binary_boolean_operator(equal,kernel_objects:equal_object_optimized,no).

binary_boolean_operator(less,kernel_objects:less_than,no).

binary_boolean_operator(less_equal,kernel_objects:less_than_equal,no).

binary_boolean_operator(less_real,kernel_reals:real_less_than_wf,yes).

binary_boolean_operator(less_equal_real,kernel_reals:real_less_than_equal_wf,yes).

binary_boolean_operator(greater,kernel_objects:greater_than,no).

binary_boolean_operator(greater_equal,kernel_objects:greater_than_equal,no).

binary_boolean_operator(subset,kernel_objects:check_subset_of_wf,yes).

binary_boolean_operator(subset_strict,kernel_objects:strict_subset_of_wf,yes).

binary_boolean_operator(not_subset_strict,kernel_objects:not_strict_subset_of_wf,yes).

binary_boolean_operator(not_subset,kernel_objects:not_subset_of_wf,yes).

binary_definitely_true_based_on_element_value(partial_function,[]). % {} : A +-> B

binary_definitely_true_based_on_element_value(partial_injection,[]). % {} : A >+> B

binary_definitely_true_based_on_element_value(relations,[]). % {} : A <-> B

binary_function(concat,bsets_clp,concat_sequence). % ^

binary_function(insert_front,bsets_clp,prepend_sequence).

binary_function(insert_tail,bsets_clp,append_sequence).

binary_function(restrict_front,bsets_clp,prefix_sequence_wf). % s /|\ n

binary_function(restrict_tail,bsets_clp,suffix_sequence). % WF

binary_function(union,kernel_objects,union_wf).

binary_function(intersection,kernel_objects,intersection).

binary_function(set_subtraction,kernel_objects,difference_set_wf).

binary_function(cartesian_product,kernel_objects,cartesian_product_wf). % always converted into closure

binary_function(add,kernel_objects,int_plus).

binary_function(add_real,kernel_reals,real_addition_wf).

binary_function(multiplication,kernel_objects,times).

binary_function(multiplication_real,kernel_reals,real_multiplication_wf).

binary_function(minus,kernel_objects,int_minus).

binary_function(minus_real,kernel_reals,real_subtraction_wf).

binary_function(modulo,kernel_objects,modulo).

binary_function(power_of,kernel_objects,int_power).

binary_function(power_of_real,kernel_reals,real_power_of_wf).

binary_function(div,kernel_objects,division).

binary_function(div_real,kernel_reals,real_division_wf).

binary_function(floored_div,kernel_objects,floored_division).

binary_function(image,bsets_clp,image_wf).

binary_function(domain_restriction,bsets_clp,domain_restriction_wf).

binary_function(domain_subtraction,bsets_clp,domain_subtraction_wf).

binary_function(range_subtraction,bsets_clp,range_subtraction_wf).

binary_function(range_restriction,bsets_clp,range_restriction_wf).

binary_function(overwrite,bsets_clp,override_relation).

binary_function(composition,bsets_clp,rel_composition_wf).

binary_function(iteration,bsets_clp,rel_iterate_wf).

binary_function(direct_product,bsets_clp,direct_product_wf).

binary_function(parallel_product,bsets_clp,parallel_product_wf).

binary_in_boolean_type(partial_function,bsets_clp:partial_function_wf).

binary_in_boolean_type(total_function,bsets_clp:total_function_wf).

binary_in_boolean_type(cartesian_product,kernel_objects:is_cartesian_pair_wf).

binary_in_boolean_type(partial_surjection,bsets_clp:partial_surjection_wf).

binary_in_boolean_type(partial_injection,bsets_clp:partial_injection_wf).

binary_in_boolean_type(total_injection,bsets_clp:total_injection_wf). % >->

binary_in_boolean_type(partial_bijection,bsets_clp:partial_bijection_wf).

binary_in_boolean_type(total_surjection,bsets_clp:total_surjection_wf). % -->>

binary_in_boolean_type(total_bijection,bsets_clp:total_bijection_wf). % >->>

binary_in_boolean_type(relations,bsets_clp:relation_over_wf).

binary_in_boolean_type(total_relation,bsets_clp:total_relation_wf).

binary_in_boolean_type(surjection_relation,bsets_clp:surjection_relation_wf).

binary_in_boolean_type(total_surjection_relation,bsets_clp:total_surjection_relation_wf).

binary_in_boolean_type(interval,kernel_objects:in_nat_range_wf).

binary_in_boolean_type(parallel_product,bsets_clp:in_parallel_product_wf).

binary_in_boolean_type(set_subtraction,kernel_objects:in_difference_set_wf).

binary_in_boolean_type(intersection,kernel_objects:in_intersection_set_wf).

binary_in_boolean_type(range_subtraction,bsets_clp:in_range_subtraction_wf).

binary_in_boolean_type(range_restriction,bsets_clp:in_range_restriction_wf).

binary_in_boolean_type(domain_subtraction,bsets_clp:in_domain_subtraction_wf).

binary_in_boolean_type(domain_restriction,bsets_clp:in_domain_restriction_wf).

binary_in_boolean_type(composition,bsets_clp:in_composition_wf).

binary_in_definitely_true(BOP,ValueOfEl) :- nonvar(ValueOfEl),
    binary_definitely_true_based_on_element_value(BOP,ValueOfEl).

binary_in_kernel_call(Module,Kernel_predicate,ElValue,SV1,SV2,WF,_Expr) :-
    get_wait_flag0(WF,WF0),
    binary_in_kernel_call2(Module,Kernel_predicate,ElValue,SV1,SV2,WF,WF0).

binary_in_kernel_call2(Module,Kernel_predicate,ElValue,SV1,SV2,WF,WF0) :- nonvar(WF0),!,
    call(Module:Kernel_predicate,ElValue,SV1,SV2,WF).

binary_in_kernel_call2(Module,Kernel_predicate,ElValue,SV1,SV2,WF,WF0) :-
    not_symbolic_when_var(ElValue,WF0,EWait),
    % ensure that we do not call this in case ElValue is a closure which may need expanding
    binary_in_kernel_call3(Module,Kernel_predicate,ElValue,SV1,SV2,WF,WF0,EWait).

binary_in_kernel_call3(Module,Kernel_predicate,ElValue,SV1,SV2,WF,WF0,_EWait) :- nonvar(WF0),!,
    call(Module:Kernel_predicate,ElValue,SV1,SV2,WF).

binary_in_kernel_call3(Module,Kernel_predicate,ElValue,SV1,SV2,WF,WF0,EWait) :-
    ground_value_check(SV1,G1),
    ground_value_check(SV2,G2),
    % when((nonvar(WF0) ; ground(EWait), nonvar(G1), nonvar(G2)),
    call_nv4(Module:Kernel_predicate,ElValue,SV1,SV2,WF, WF0,EWait,G1,G2).

binary_kernel_call(_,KernelFunction,ESV1,ESV2,Value,WF,_Expr,_Type,Span) :-
    determined_binary_integer_function(KernelFunction),
    !,
    get_wait_flag0(WF,WF0),
    call_determined_integer_function(KernelFunction,ESV1,ESV2,Value,WF0,WF,Span).

binary_kernel_call(Module,KernelFunction,ESV1,ESV2,Value,WF,Expr,Type,Span) :-
    (expects_waitflag_and_span(KernelFunction)
    -> KernelCall =.. [KernelFunction,ESV1,ESV2,Value,Span,WF]
    ; expects_waitflag(KernelFunction)
    -> KernelCall =.. [KernelFunction,ESV1,ESV2,Value,WF]
    ; expects_waitflag_and_type(KernelFunction)
    -> KernelCall =.. [KernelFunction,ESV1,ESV2,Value,Type,WF]
    ; KernelCall =.. [KernelFunction,ESV1,ESV2,Value]
    ),
    special_propagate_binary_function(KernelFunction,ESV1,ESV2,Value,WF),
    must_succ_kernel_call(Module:KernelCall,(ESV1,ESV2),WF,Expr).

binary_not_in_boolean_type(interval,kernel_objects:not_in_nat_range_wf).

binary_not_in_boolean_type(partial_function,bsets_clp:not_partial_function).

binary_not_in_boolean_type(partial_surjection,bsets_clp:not_partial_surjection_wf).

binary_not_in_boolean_type(total_surjection,bsets_clp:not_total_surjection_wf).

binary_not_in_boolean_type(partial_injection,bsets_clp:not_partial_injection).

binary_not_in_boolean_type(total_injection,bsets_clp:not_total_injection).

binary_not_in_boolean_type(partial_bijection,bsets_clp:not_partial_bijection).

binary_not_in_boolean_type(cartesian_product,kernel_objects:not_is_cartesian_pair).

binary_not_in_boolean_type(relations,bsets_clp:not_relation_over).

binary_not_in_boolean_type(total_function,bsets_clp:not_total_function).

binary_not_in_boolean_type(total_bijection,bsets_clp:not_total_bijection).

binary_not_in_boolean_type(total_relation,bsets_clp:not_total_relation_wf).

binary_not_in_boolean_type(surjection_relation,bsets_clp:not_surjection_relation_wf).

binary_not_in_boolean_type(total_surjection_relation,bsets_clp:not_total_surjection_relation_wf).

binary_not_in_boolean_type(parallel_product,bsets_clp:not_in_parallel_product_wf).

binary_not_in_boolean_type(set_subtraction,kernel_objects:not_in_difference_set_wf).

binary_not_in_boolean_type(intersection,kernel_objects:not_in_intersection_set_wf).

binary_not_in_boolean_type(range_subtraction,bsets_clp:not_in_range_subtraction_wf).

binary_not_in_boolean_type(range_restriction,bsets_clp:not_in_range_restriction_wf).

binary_not_in_boolean_type(domain_subtraction,bsets_clp:not_in_domain_subtraction_wf).

binary_not_in_boolean_type(domain_restriction,bsets_clp:not_in_domain_restriction_wf).

binary_not_in_boolean_type(composition,bsets_clp:not_in_composition_wf).

call_apply_to(FValue,ArgValue,Res,FunctionType,Span,WF,_,_Gr) :-
    %discard_ground_value_check(Gr),
    bsets_clp:apply_to(FValue,ArgValue,Res,FunctionType,Span,WF).

call_determined_integer_function(KF,V1,V2,Val,WF0,WF,Span) :-
    determined(V1,V2,Val,Determined,WF0),
    call_determined_integer_function2(KF,V1,V2,Val,WF0,Determined,WF,Span).

call_determined_integer_function2(division,V1,V2,Val,_,_,WF,Span) :-
    kernel_objects:division(V1,V2,Val,Span,WF).

call_determined_integer_function2(floored_division,V1,V2,Val,_,_,WF,Span) :-
    kernel_objects:floored_division(V1,V2,Val,Span,WF).

call_determined_integer_function2(int_minus,V1,V2,Val,_,_,_WF,_Span) :-
    kernel_objects:int_minus(V1,V2,Val).

call_determined_integer_function2(int_plus,V1,V2,Val,_,_,_WF,_Span) :-
    % kernel_call_determined(kernel_objects:int_plus(V1,V2,Val),V1,V2,Val,WF,integer).
    kernel_objects:int_plus(V1,V2,Val).

call_determined_integer_function2(int_power,V1,V2,Val,_,_,WF,Span) :-
    kernel_objects:int_power(V1,V2,Val,Span,WF).

call_determined_integer_function2(modulo,V1,V2,Val,_,_,WF,Span) :-
    kernel_objects:modulo(V1,V2,Val,Span,WF).

call_determined_integer_function2(times,V1,V2,Val,_,_,_WF,_Span) :-
    kernel_objects:times(V1,V2,Val).

call_nv(Call,_,_) :-
    % ( (var(WF0) -> print('enter :'),tools_printing:print_term_summary(Call) ; true),
    call(Call).

call_nv3(Call,A,B,C,_WF0,_,_) :-
    call(Call,A,B,C).

call_nv4(Call,A,B,C,D,_WF0,_,_G1,_G2) :-
    call(Call,A,B,C,D).

call_nv_or3(Call,_,_,_) :-
    call(Call).

call_wf0(Call,_) :- call(Call).

call_wf0_2(Call,A1,A2,WF,_) :- call(Call,A1,A2,WF).

call_wf0_3(Call,A1,A2,A3,WF,_) :- call(Call,A1,A2,A3,WF).

can_construct_complement_closure(Set1,Set2) :-
    nonvar(Set1), nonvar(Set2), Set2 = avl_set(_),
    custom_explicit_sets:is_very_large_maximal_global_set(Set1,_).

check_element_of_wf0(A,B,WF,_WF0,_) :- var(B),!, % means nonvar(WF0)
    kernel_objects:check_element_of_wf(A,B,WF).

check_element_of_wf0(_A,B,_WF,_,_) :- B=[],!,fail. % nothing can be element of empty set; CAN PREVENT WD-ERRORS from being detected !

check_element_of_wf0(A,B,WF,_WF0,_) :-
    singleton_set(B,B1),!, /* also does var check */
    equal_object_optimized_wf(A,B1,check_element_of_wf0,WF). %was equal_obj(A,B1,WF0) but as B1 is ground value will always call equal_object_optimized directly

check_element_of_wf0(A,global_set(GS),WF,_,Span) :- nonvar(A),
    !, % be sure that we check something like int(-1) : NATURAL
    %kernel_objects:check_element_of_wf(A,global_set(GS),WF).
    kernel_objects:element_of_global_set_wf(A,GS,WF,Span). % Span for enumeration warnings

check_element_of_wf0(A,avl_set(AVL),WF,_,_) :- simple_ground_value(A),
    !, % we can already check this efficiently in phase 0
    custom_explicit_sets:element_of_avl_set_wf(AVL,A,WF). % we could even call avl_fetch directly

check_element_of_wf0(A,B,WF,WF0,Span) :-
    check_element_of_wf0_aux(A,B,WF,WF0,Span).

check_element_of_wf0_aux(A,global_set(GS),WF,_WF0,Span) :- !,
    kernel_objects:element_of_global_set_wf(A,GS,WF,Span). % Span for enumeration warnings

check_element_of_wf0_aux(A,avl_set(AVL),_WF,_WF0,b(EE,TT,Span)) :-
    member(prob_annotation('ENUM'),Span),!, % force early enumeration via 'ENUM' external function annotation
    (debug:debug_mode(on) -> add_message(enum,'Early enumeration of: ',b(EE,TT,Span),Span) ; true),
    custom_explicit_sets:safe_avl_member(A,AVL). % TO DO: use avl_fetch if A known? + cover ENUM annotation also if set is known later

check_element_of_wf0_aux(A,B,WF,_WF0,_Span) :- kernel_objects:check_element_of_wf(A,B,WF).

check_valid_kernel_call(X,unary) :- unary_function(_,_,X).

check_valid_kernel_call(X,binary) :- binary_function(_,_,X).

check_valid_kernel_call(X,_) :- add_error(check_valid_kernel_call,'Illegal Kernel Call: ',X),fail.

cst_in_boolean_type(string_set,kernel_objects:is_string).

cst_in_boolean_type(real_set,kernel_reals:is_real_wf).

cst_in_boolean_type(float_set,kernel_reals:is_float_wf).

cst_in_boolean_type(integer_set(IntSet),Call) :- integerset_in_boolean_type(IntSet,Call).

cst_not_in_boolean_type(string_set,kernel_objects:is_not_string).

cst_not_in_boolean_type(real_set,kernel_reals:is_not_real).

cst_not_in_boolean_type(float_set,kernel_reals:is_not_float).

cst_not_in_boolean_type(integer_set(IntSet),Call) :- integerset_not_in_boolean_type(IntSet,Call).

definitely_not_empty(X) :- nonvar(X), definitely_not_empty_aux(X).

definitely_not_empty_aux([_|_]).

definitely_not_empty_aux(avl_set(_)).

definitely_not_empty_aux(global_set(_)).

definitely_not_empty_aux(freetype(ID)) :- is_non_empty_freetype(ID).

determined(_X,_Y,_Z,Det,WF0) :- nonvar(WF0),!,Det=determined.

determined(X,Y,V,Det,_) :- var(X),!, Y=int(YY),V=int(VV), %(YY=0 -> X=V ; true),
    determined2(X,YY,VV,Det).

determined(Y,X,V,Det,_) :- var(X),!, Y=int(YY),V=int(VV), %(YY=0 -> X=V ; true),
    determined2(X,YY,VV,Det).

determined(Y,V,X,Det,_) :- Y=int(YY),V=int(VV), %(YY=0 -> X=V ; VV=0 -> X=Y),
    determined2(X,YY,VV,Det).

determined2(X,_,_,Det) :- var(X),!,Det=determined.

determined2(int(XX),YY,VV,Det) :- determined3(XX,YY,VV,Det).

determined3(_,_,_,determined).

determined_binary_integer_function(division). % isn't really determined X / 10 = 2 --> many possible values

determined_binary_integer_function(int_minus).

determined_binary_integer_function(int_plus).

determined_binary_integer_function(int_power).

determined_binary_integer_function(modulo). % isn't really determined; X mod 10 = 0 --> many possible values

determined_binary_integer_function(times).

do_not_keep_symbolic(cartesian_product,Set1,Set2,Res,WF) :- %print(cart(Set1,Set2)),nl,
    (singleton_set(Set1,_) -> small_known_set(Set2)
    ; singleton_set(Set2,_) -> small_known_set(Set1)
    ),
    kernel_objects:cartesian_product_wf(Set1,Set2,Res,WF).

do_not_keep_symbolic(interval,int(A),int(B),Res,_WF) :-
    (integer(A),nonvar(B),A=B % or B-A < some limit
    -> custom_explicit_sets:convert_to_avl([int(A)],Res)).

do_not_keep_symbolic(parallel_product,Rel1,Rel2,Res,WF) :-
    not_closure(Rel1), not_closure(Rel2),
    bsets_clp:parallel_product_wf(Rel1,Rel2,Res,WF).

do_not_keep_symbolic(intersection,Set1,Set2,Res,_WF) :- nonvar(Set1), nonvar(Set2),
    % only keep symbolic if at least one non-interval closure
    nonvar_non_interval_closure(Set1,Set2,R12),
    (R12=1 ->
    \+ small_known_set(Set2) % intersection with singleton set can always be computed
    ; R12=2 -> \+ small_known_set(Set1)),
    !,
    (same_closure(Set1,Set2) -> Res = Set1 % Set1 /\ Set1 = Set1
    ; %% print(symbolic_intersection),nl, translate:print_bvalue(Set1),nl, translate:print_bvalue(Set2),nl,nl,
    fail).

do_not_keep_symbolic(intersection,Set1,Set2,Res,WF) :- % otherwise: compute intersection normally
    Call=kernel_objects:intersection(Set1,Set2,Res,WF),
    must_succ_kernel_call(Call,[Set1,Set2],WF,Call).

do_not_keep_symbolic(set_subtraction,Set1,Set2,Res,_WF) :- Set2 == [],!,
    Res = Set1.

do_not_keep_symbolic(set_subtraction,Set1,Set2,Res,_WF) :- nonvar(Set1),
    % only keep symbolic if at least one non-interval closure
    nonvar_non_interval_closure(Set1,Set2,_),
    % check if we cannot construct a complement closure:
    \+ can_construct_complement_closure(Set1,Set2),
    \+ small_known_set(Set1),
    !,
    (same_closure(Set1,Set2) -> Res = [] % Set \ Set = {}
    ; %nl,print(symbolic_set_subtr(Set1,Set2)),nl,nl,
    fail).

do_not_keep_symbolic(set_subtraction,Set1,Set2,Res,WF) :- % otherwise: compute difference normally
    Call=kernel_objects:difference_set_wf(Set1,Set2,Res,WF), % print(diff_set(Set1,Set2,Res)),nl,
    must_succ_kernel_call(Call,[Set1,Set2],WF,Call).

do_not_keep_symbolic_unary(_,ArgValue) :- ArgValue==[],!.

do_not_keep_symbolic_unary(closure,Set1) :- % this is closure1
    very_small_known_avl_set(Set1).

do_not_keep_symbolic_unary(pow_subset,Set1) :- singleton_set(Set1,_).

do_not_keep_symbolic_unary(fin_subset,Set1) :- singleton_set(Set1,_).

do_not_keep_symbolic_unary(pow1_subset,Set1) :- singleton_set(Set1,_).

do_not_keep_symbolic_unary(fin1_subset,Set1) :- singleton_set(Set1,_).

efficient_value(X) :- var(X),!,fail.

efficient_value(int(_)).

efficient_value(avl_set(_)).

efficient_value([]).

efficient_value(fd(_,_)).

efficient_value(string(_)).

efficient_value((A,B)) :- nonvar(A),nonvar(B),efficient_value(A), efficient_value(B).

efficient_value(pred_true). efficient_value(pred_false).

efficient_value(pred_true). efficient_value(pred_false).

efficient_value(term(_)). % will usually be floating: :- nonvar(X),X=floating(_).

equal_obj(A,B,WF0,WF) :- nonvar(WF0),!,
    equal_object_optimized_wf(A,B,equal_obj1,WF).

equal_obj(A,B,WF0,WF) :- %hit_profiler:add_profile_hit(eq(A,B)),
    non_simple_ground_value_check(A,VA),
    (nonvar(VA) -> equal_object_optimized_wf(A,B,equal_obj2,WF)
    ; non_simple_ground_value_check(B,VB),
    (nonvar(VB) -> equal_object_optimized_wf(A,B,equal_obj3,WF)
    ; equal_obj_block(A,B,WF,WF0,VA,VB)
)
).

equal_obj_block(A,B,WF,_,_,_) :-
    equal_object_optimized_wf(A,B,equal_obj4,WF).

expects_waitflag(append_sequence).

expects_waitflag(bag_items).

expects_waitflag(cartesian_product_wf).

expects_waitflag(compaction).

expects_waitflag(concat_sequence).

expects_waitflag(concatentation_of_sequences).

expects_waitflag(difference_set_wf).

expects_waitflag(direct_product_wf).

expects_waitflag(parallel_product_wf).

expects_waitflag(domain_restriction_wf).

expects_waitflag(domain_subtraction_wf).

expects_waitflag(domain_wf).

expects_waitflag(finite_cardinality_as_int_wf).

expects_waitflag(identity_relation_over_wf).

expects_waitflag(image_wf).

expects_waitflag(intersection).

expects_waitflag(invert_relation_wf).

expects_waitflag(relational_trans_closure_wf).

expects_waitflag(override_relation).

expects_waitflag(prefix_sequence_wf).

expects_waitflag(prepend_sequence).

expects_waitflag(range_restriction_wf).

expects_waitflag(range_subtraction_wf).

expects_waitflag(range_wf).

expects_waitflag(real_addition_wf).

expects_waitflag(real_multiplication_wf).

expects_waitflag(real_subtraction_wf).

expects_waitflag(real_unary_minus_wf).

expects_waitflag(rev_sequence).

expects_waitflag(size_of_sequence).

expects_waitflag(square).

expects_waitflag(suffix_sequence).

expects_waitflag(unary_minus_wf).

expects_waitflag(union_generalized_wf).

expects_waitflag(union_wf).

expects_waitflag_and_span(first_sequence).

expects_waitflag_and_span(last_sequence).

expects_waitflag_and_span(tail_sequence).

expects_waitflag_and_span(front_sequence).

expects_waitflag_and_span(minimum_of_set).

expects_waitflag_and_span(maximum_of_set).

expects_waitflag_and_span(intersection_generalized_wf).

expects_waitflag_and_span(division).

expects_waitflag_and_span(floored_division).

expects_waitflag_and_span(modulo).

expects_waitflag_and_span(int_power).

expects_waitflag_and_span(real_power_of_wf).

expects_waitflag_and_span(singleton_set_element).

expects_waitflag_and_span(real_division_wf).

expects_waitflag_and_span(real_maximum_of_set).

expects_waitflag_and_span(real_minimum_of_set).

expects_waitflag_and_type(rel_iterate_wf).

expects_waitflag_and_type(rel_composition_wf).

generate_documentation :-
    kernel_predicate(M,P,_T,ARITY,BAST,BOP,_WF),
    ( symbolic_closure_unary_operator(BOP) -> Sym=' (symbolic_unary)'
    ; symbolic_closure_binary_operator(BOP) -> Sym=' (symbolic_binary)' % these not printed as binary_function does not include them
    ; Sym= ''),
    format(' ~w (~w/~w) --> ~w:~w ~w~n',[BOP,BAST,ARITY,M,P,Sym]),
    fail.

generate_documentation.

get_waitflag_info(P,WF) :-
    (expects_waitflag_and_span(P) -> WF = wf_span ;
    expects_waitflag_and_span(P) -> WF = yes ;
    WF = no).

integerset_in_boolean_type('INTEGER',kernel_objects:is_integer).

integerset_in_boolean_type('NATURAL',kernel_objects:is_natural).

integerset_in_boolean_type('NATURAL1',kernel_objects:is_natural1).

integerset_in_boolean_type('INT',kernel_objects:is_implementable_int).

integerset_in_boolean_type('NAT',kernel_objects:is_implementable_nat).

integerset_in_boolean_type('NAT1',kernel_objects:is_implementable_nat1).

integerset_not_in_boolean_type('INTEGER',kernel_objects:is_not_integer).

integerset_not_in_boolean_type('NATURAL',kernel_objects:is_not_natural).

integerset_not_in_boolean_type('NATURAL1',kernel_objects:is_not_natural1).

integerset_not_in_boolean_type('INT',kernel_objects:is_not_implementable_int).

integerset_not_in_boolean_type('NAT',kernel_objects:is_not_implementable_nat).

integerset_not_in_boolean_type('NAT1',kernel_objects:is_not_implementable_nat1).

invalid_call(X) :- \+ check_valid_kernel_call(X,_).

is_definitely_empty(interval,int(A),int(B)) :- number(A),number(B), A>B.

is_definitely_empty(cartesian_product,A,B) :- (B==[]->true ; A==[]). % A==[] actually already checked in binary_arg1_determines_value

is_definitely_empty(parallel_product,A,B) :- (A==[]->true ; B==[]).

is_definitely_empty(total_relation,A,B) :- B==[], definitely_not_empty(A).

is_definitely_empty(total_function,A,B) :- B==[], definitely_not_empty(A). % {} --> {} = {{}}

is_definitely_empty(total_injection,A,B) :- B==[], definitely_not_empty(A).

is_definitely_empty(total_surjection,A,B) :- B==[], definitely_not_empty(A).

is_definitely_empty(total_bijection,A,B) :- B==[], definitely_not_empty(A).

is_definitely_empty(intersection,A,B) :- (A==[] ; B==[]).

is_definitely_empty(set_subtraction,A,B) :-
    (A==[] ; nonvar(B), custom_explicit_sets:is_definitely_maximal_set(B)).

kernel_call(Call,HasToBeGround,WF,_Expr) :-
    get_wait_flag0(WF,WF0),
    %hit_profiler:add_profile_hit(kernel_call(Call,WF),2),
    %print(kc(WF0,Call)),nl,
    (nonvar(WF0)
    -> call(Call)
    ; ground_value_opt_check(HasToBeGround,WF0,G1),
    call_nv(Call,WF0,G1)
).

kernel_call_apply_to(FValue,ArgValue,Res,FunctionType,Span,WF) :-
    %hit_profiler:add_profile_hit(kernel_call_apply_to(FValue,ArgValue,Res,WF)),
    get_wait_flag0(WF,WF0),
    (var(WF0) %(var(WF0), \+ ground(ArgValue), \+ ground(FValue))
    -> ground_value_check((FValue,ArgValue),WF1), % often FValue is an avl_set, avoid pending co-routines later by checking it first for groundness
    call_apply_to(FValue,ArgValue,Res,FunctionType,Span,WF,WF0,WF1)
    ; apply_to(FValue,ArgValue,Res,FunctionType,Span,WF)
).

kernel_call_or(Call,HasToBeGround1,HasToBeGround2,WF,_Expr) :-
    get_wait_flag0(WF,WF0),
    (nonvar(WF0) -> call(Call)
    ; ground_value_check(HasToBeGround1,G1),
    (nonvar(G1) -> call(Call)
    ; ground_value_check(HasToBeGround2,G2),
    %hit_profiler:add_profile_hit(kernel_call_or(Call,WF0),2),
    call_nv_or3(Call,WF0,G1,G2)
)
).

kernel_call_predicate(equal_object_optimized(A,B),kernel_objects,WF,_) :- !,
    get_wait_flag0(WF,WF0),
    equal_obj(A,B,WF0,WF).

kernel_call_predicate(not_equal_object_wf(A,B,WF),kernel_objects,WF,Expr) :- !,
    get_wait_flag0(WF,WF0),not_eq_wf(A,B,WF,WF0,Expr).

kernel_call_predicate(partition_wf(A,B,PWF),kernel_objects,WF,Expr) :- !,
    (nonvar(B),B=[B1|T],T==[] % just one set
    -> kernel_call_predicate(equal_object_optimized(A,B1),kernel_objects,WF,Expr)
    ; all_but_one_set_known([A|B],Known),
    kernel_call(kernel_objects:partition_wf(A,B,PWF),Known,WF,Expr)).

kernel_call_predicate(less_than(A,B),kernel_objects,_WF,_Expr) :- !, kernel_objects:less_than(A,B).

kernel_call_predicate(less_than_equal(A,B),kernel_objects,_WF,_Expr) :- !, kernel_objects:less_than_equal(A,B).

kernel_call_predicate(greater_than(A,B),kernel_objects,_WF,_Expr) :- !, kernel_objects:less_than(B,A).

kernel_call_predicate(greater_than_equal(A,B),kernel_objects,_WF,_Expr) :- !, kernel_objects:less_than_equal(B,A).

kernel_call_predicate(check_element_of_wf(A,B,PWF),kernel_objects,WF,Expr) :- !,
    get_wait_flag0(WF,WF0), check_element_of_wf0(A,B,PWF,WF0,Expr).

kernel_call_predicate(is_natural(A,WF),kernel_objects,WF,_Expr) :- !, kernel_objects:is_natural(A,WF). % see test 2092

kernel_call_predicate(is_natural1(A,WF),kernel_objects,WF,_Expr) :- !, kernel_objects:is_natural1(A,WF).

kernel_call_predicate(is_not_natural(A),kernel_objects,_WF,_Expr) :- !, kernel_objects:is_not_natural(A).

kernel_call_predicate(is_not_natural1(A),kernel_objects,_WF,_Expr) :- !, kernel_objects:is_not_natural1(A).

kernel_call_predicate(Call,Module,WF,_Expr) :- get_wait_flag0(WF,WF0),
    %hit_profiler:add_profile_hit(kernel_call_predicate(Call,WF0),2),
    call_wf0(Module:Call,WF0).

kernel_call_predicate2(KernelCall,Arg1,Arg2,Module,WF,_Expression) :-
    get_wait_flag0(WF,WF0),
    call_wf0_2(Module:KernelCall,Arg1,Arg2,WF,WF0).

kernel_call_predicate3(KernelCall,Arg1,Arg2,Arg3,Module,WF,_Expression) :-
    get_wait_flag0(WF,WF0),
    call_wf0_3(Module:KernelCall,Arg1,Arg2,Arg3,WF,WF0).

kernel_call_predicate_check_element_of_wf(A,B,WF,Span) :-
    get_wait_flag0(WF,WF0), check_element_of_wf0(A,B,WF,WF0,Span).

kernel_call_predicate_equal_object_optimized(A,B,WF) :-
    get_wait_flag0(WF,WF0),equal_obj(A,B,WF0,WF).

kernel_call_predicate_not_element_of_wf(A,B,WF) :-
    get_wait_flag0(WF,WF0),not_element_of_wf0(A,B,WF,WF0).

kernel_call_predicate_not_equal_object(A,B,WF,Expr) :-
    get_wait_flag0(WF,WF0),not_eq_wf(A,B,WF,WF0,Expr).

kernel_predicate(M,P,expression,1,BAST,BOP,WF) :-
    unary_function(BAST,M,P), get_waitflag_info(P,WF),
    (translate:unary_prefix(BAST,BOP,_) -> true
    ; translate:unary_postfix(BAST,BOP,_) -> true
    ; translate:function_like(BAST,BOP) -> true
    ; BOP = '??').

kernel_predicate(M,P,expression,2,BAST,BOP,WF) :-
    binary_function(BAST,M,P), get_waitflag_info(P,WF),
    (translate:binary_infix(BAST,BOP,_,_) -> true
    ; translate:function_like(BAST,BOP) -> true ; BOP = '??').

kernel_predicate(M,P,predicate,2,BAST,BOP,WF) :-
    binary_boolean_operator(BAST,M:P,WF),
    (translate:binary_infix(BAST,BOP,_,_) -> true
    ; translate:function_like(BAST,BOP) -> true ; BOP = '??').

known_atomic(_,true).

known_value(_,T) :- T==true,!.

known_value(int(X),K) :- !, known_atomic(X,K).

known_value(pred_true /* bool_true */,K) :- !, K=true.

known_value(pred_false /* bool_false */,K) :- !, K=true.

known_value(string(X),K) :- !, known_atomic(X,K).

known_value([],K) :- !, K=true.

known_value(avl_set(_A),K) :- !, K=true.

known_value(global_set(X),K) :- !,known_atomic(X,K).

known_value(freetype(X),K) :- !,known_atomic(X,K).

known_value(A,K) :- when(ground(A),K=true).

must_succ_kernel_call(Call,HasToBeGround,WF,_Expr) :-
    get_wait_flag0(WF,WF0),
    (nonvar(WF0)
    -> call(Call)
    ; %hit_profiler:add_profile_hit(must_succ_kernel_call(Call,WF0),3),
    %ground_value_check(HasToBeGround,G1), % using this made test 1562 fail; probably because co-routines remain active after WF0 has been set, leading un bound variables preventing optimisations in kernel_objects
    ground_value_opt_check(HasToBeGround,WF0,VG1),
    call_nv(Call,WF0,VG1)
).

negate_binary_boolean_operator(X,Y) :-
    ( negate_binary_boolean_operator2(X,Y) -> true
    ; negate_binary_boolean_operator2(Y,X)).

negate_binary_boolean_operator2(member,not_member).

negate_binary_boolean_operator2(subset,not_subset).

negate_binary_boolean_operator2(subset_strict,not_subset_strict).

negate_binary_boolean_operator2(equal,not_equal).

negate_binary_boolean_operator2(less,greater_equal).

negate_binary_boolean_operator2(less_equal,greater).

negate_binary_boolean_operator_swap(less_equal_real,less_real).

negate_binary_boolean_operator_swap(less_real,less_equal_real).

non_simple_ground_value_check(V,Vars) :- var(V),!, Vars=[V].

non_simple_ground_value_check(pred_false,Vars) :- !, Vars=[].

non_simple_ground_value_check(pred_true,Vars) :- !, Vars=[].

non_simple_ground_value_check(int(_),Vars) :- !, Vars=[]. % may contain var; but we can unify nonetheless

non_simple_ground_value_check(string(_),Vars) :- !, Vars=[]. % ditto

non_simple_ground_value_check(fd(_,_),Vars) :- !, Vars=[]. % ditto

non_simple_ground_value_check(A,Vars) :- !, ground_value_check(A,Vars).

nonvar_non_interval_closure(A) :- nonvar(A), A=closure(_,_,_),
    \+ custom_explicit_sets:is_interval_closure_or_integerset(A,_,_),
    \+ custom_explicit_sets:is_not_member_value_closure(A,_Type,_MS2). % there isn't full support for this for intersection yet ! TODO fix