store

add_var_to_localstate(Var,Val,InState,[bind(Var,Val)|InState]).

can_be_computed(domain(X)) :- is_known_set_or_int_value(X).

can_be_computed(range(X)) :- is_known_set_or_int_value(X).

can_be_computed(plus(X,Y)) :- is_known_set_or_int_value(X),is_known_set_or_int_value(Y).

can_be_computed(minus(X,Y)) :- is_known_set_or_int_value(X),is_known_set_or_int_value(Y).

can_be_computed(times(X,Y)) :- is_known_set_or_int_value(X),is_known_set_or_int_value(Y).

cannot_be_normalised_in_avl((A,B)) :- !,
    (cannot_be_normalised_in_avl(A) -> true ; cannot_be_normalised_in_avl(B) -> true).

cannot_be_normalised_in_avl([H|_]) :- cannot_be_normalised_in_avl(H).

cannot_be_normalised_in_avl(C) :- is_symbolic_closure(C).

cannot_be_normalised_in_avl(rec(Fields)) :- !, member(field(_,A),Fields), cannot_be_normalised_in_avl(A).

check_val(X,V,_State) :-
    (X==term(undefined) ->
    add_state_error_wf(reading_undefined_variable,'Trying to read undefined variable: ',V,unknown,no_wf_available)
    % do not fail
    ; true).

check_val_with_span_wf(X,V,_State,Span,WF) :-
    (X==term(undefined) ->
    add_state_error_wf(reading_undefined_variable,'Trying to read undefined variable: ',V,Span,WF) % do not fail; otherwise we will look elsewhere and generate another error message, see test 1660
    ; true).

check_valid_store([],_PP).

check_valid_store([bind(Var,Value)|T],PP) :- member(bind(Var,Val2),T),
    add_internal_error('Multiple occurences of variable: ',bind(Var,Value,Val2,PP)),
    fail.

check_valid_store([_|T],PP) :- check_valid_store(T,PP).

construct_normalised_closure(P,T,B1,closure(P,T,NB)) :-
    %print(normalising(P)),nl,
    %b_compile(B1,P,[],[],B2,no_wf_available), % probably much more expensive than simple code with can_be_computed below
    normalise_closure_body(B1,NB).

copy_store(In,Out,_,_) :- var(Out),!, Out=In.

copy_store(In,Out,PP,_) :- var(In),!, add_warning(store,'In store skeleton not set up:',In,PP), Out=In.

copy_store([],[],_PP,_) :- !.

copy_store([bind(Var1,InVal)|T1],[bind(Var2,OutVal)|T2],PP,WF) :- !,
    (Var1=Var2
    -> equal_object_wf(InVal,OutVal,copy_store,WF)
    % usually InVal==OutVal, but in test 1043 became false after WF0 was no longer grounded inside SELECT/PRE
    ; add_error(copy_store,'Variable mismatch:',Var1:Var2,PP), fail),
    copy_store(T1,T2,PP,WF).

copy_store(S1,S2,PP,_) :-
    check_valid_store(S1,PP), check_valid_store(S2,PP),
    add_error(copy_store,'Illegal stores:',S1:S2,PP),fail.

copy_variable_store(InState,SortedChanges,Updates,NewFullState) :-
    (SortedChanges=[] -> Updates = [],NewFullState=InState % Query Operation/Event ,print(no_upd),nl
    ; copy_variable_store2(InState,SortedChanges,Updates,NewFullState)).

copy_variable_store2([],_,[],[]).

copy_variable_store2([bind(Var,Old)|T],SortedChanges,Updates,NewFullState) :-
    ( b_is_constant(Var) ->
    Updates = CT, NewFullState = [bind(Var,Old)|FT]
    %; safe_member(Var,SortedChanges,copy_variable_store) ->
    ; ord_member(Var,SortedChanges) ->
    %; ord_delete(SortedChanges,Var,SortedChanges2) -> % in principle better than ord_member; but seems slightly slower on examples/EventBPrologPackages/Advance_WP2/v6_Sep2014/ex_mch.eventb
    Updates = [bind(Var,New)|CT], NewFullState = [bind(Var,New)|FT]
    ;
    Updates = CT, NewFullState = [bind(Var,Old)|FT]
    ), copy_variable_store2(T,SortedChanges,CT,FT).

delete_variable([],_,[]).

delete_variable([bind(V,Val)|T],Var,Res) :-
    (Var==V
    -> Res = T
    ; Res = [bind(V,Val)|DT], delete_variable(T,Var,DT)
).

delete_variables_from_state([],S,R) :- !, R=S.

delete_variables_from_state([Var|T],InState,OutState) :- !,
    delete_variable(InState, Var, S2),
    delete_variables_from_state(T,S2,OutState).

delete_variables_from_state(Vs,I,O) :-
    add_internal_error('Illegal call to:',delete_variables_from_state(Vs,I,O)),fail.

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

dont_expand_for_norm(limit(Limit),C,_,_) :- !,
    (dont_normalise_this_explicit_set(C) ;
    dont_expand_this_explicit_set(C,Limit)).

dont_expand_for_norm(_,C,VarName,Span) :-
    constant_variable_marked_as_expand(VarName),!, % we have a user annotation, e.g., /*@desc expand */
    % see also b_add_constant_definition for constants in b_interpreter
    (is_recursive_closure(C)
    -> add_warning(store,'Cannot expand recursive constant or variable: ',VarName,Span)
    ; is_infinite_explicit_set(C)
    -> add_warning(store,'Cannot expand infinite constant or variable: ',VarName,Span)
).

dont_expand_for_norm(true,C,_,_) :-
    dont_normalise_this_explicit_set(C) ;
    dont_expand_this_explicit_set(C). % detects e.g. symbolic closures or large intervals

dont_expand_for_norm(force,C,_,_) :-
    (is_recursive_closure(C) -> true ; is_infinite_or_very_large_explicit_set(C)).

dont_normalise_this_explicit_set(closure(P,T,B)) :- is_memoization_closure(P,T,B,_).

empty_state([]).

eq_obj(Val1,Val2) :- (var(Val1);var(Val2)),!,Val1=Val2.

eq_obj(Val1,Val2) :- equal_object(Val1,Val2,search_and_delete_value).

expand_closure_value2(P,T,B,EXPAND,VarName,ExpandedValue) :- !,
    % print(expand_closure_value2(VarName,EXPAND,P)),debug:nl_time,
    (dont_expand_for_norm(EXPAND,closure(P,T,B),VarName,B)
    -> construct_normalised_closure(P,T,B,ExpandedValue) %, print(not_expanding(closure(P,T,B))),nl
    ; %format('Expanding closure value of ~w for normalisation (expand:~w)~n',[VarName,EXPAND]),
    % translate:print_bvalue(closure(P,T,B)),nl,
    (EXPAND=force, is_symbolic_closure(closure(P,T,B))
    -> Factor = 0.1 % more likely that expansion is not possible
    ; Factor = 0.3),
    catch_clpfd_overflow_call2(
    time_out_with_factor_call(
    call_with_enumeration_warning( /* ensure we generate enumeration_warning exceptions */
    store:expand_closure_value3(P,T,B,VarName,ExpandedValue)
    ),
    Factor,
    store:time_out_expand_backup(VarName,P,T,B,ExpandedValue))
    , (format('% CLP(FD) overflow during closure expansion: ~w~n',[VarName]),
    construct_normalised_closure(P,T,B,ExpandedValue)))
%, tools_printing:print_term_summary(expanded(VarName,ExpandedValue)),debug:nl_time
).

expand_closure_value3(P,T,B,VarName,ExpandedValue) :-
    init_wait_flags_with_call_stack(WF,[prob_command_context(expanding_value_for_normalisation(VarName),unknown)]),
    custom_explicit_sets:expand_closure_to_avl_or_list(P,T,B,ExpandedValue,no_check,WF),
    ground_wait_flags(WF).

expand_closure_value_for_normalisation(Var,_,_,R) :- var(Var),!,R=Var.

expand_closure_value_for_normalisation(closure(P,T,B),EXPAND,VarName,ExpandedValue) :- !, %print(expand_closure_value_for_normalisation(P,T,B)),nl,
    expand_closure_value2(P,T,B,EXPAND,VarName,ExpandedValue).

expand_closure_value_for_normalisation(Val,_Expand,_VarName,Val).

extract_vars(const_and_vars(ConstID,IV),IV,OV,const_and_vars(ConstID,OV)) :- !.

extract_vars(IV,IV,OV,OV).

filter_info(truth,_,Res) :- !, % we have a maximal set
    Res=[]. % we could check preference(provide_trace_information,false)

filter_info(falsity,_,Res) :- !, Res=[].

filter_info(_,V,R) :- filter_info2(V,R).

filter_info2(V,R) :- var(V),!,R=V.

filter_info2([],[]).

filter_info2([H|T],Res) :-
    (important_info(H) -> Res=[H|TR] ; Res=TR), filter_info2(T,TR).

get_id_value(Id,State,Val) :- safe_member(bind(Id,Val),State,get_id_value). /* can be backtracked over */

get_ids_from_store(Store,Ids,SIds) :- findall(Id,member(bind(Id,_),Store),Ids), sort(Ids,SIds).

important_info(contains_wd_condition).

important_info(prob_annotation(_)).

important_info(used_ids(_)).

important_info(reads(_)). % operation_call_in_expr, modifies(.), non_det_modifies(.) only appear in subst

important_info(was(_)).

important_info(nodeid(_)).

important_info(allow_to_lift_exists).

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

is_known_aux([]).

is_known_aux(avl_set(_)).

is_known_aux(int(Nr)) :- number(Nr).

is_known_set_or_int_value(b(value(V),_,_)) :- is_known_aux(V).

l_expand_and_normalise_values([],[],_).

l_expand_and_normalise_values([H|T],[NH|NT],[VarName|VT]) :-
    %% print(normalising(VarName)),nl,
    normalise_value_for_var(VarName,true,H,NH),
    l_expand_and_normalise_values(T,NT,VT).

l_expand_and_normalise_values([],[]).

l_expand_and_normalise_values([H|T],[NH|NT]) :-
    normalise_value_for_var('$unkown',true,H,NH),
    l_expand_and_normalise_values(T,NT).

l_normalise_values([],[]).

l_normalise_values([H|T],[NH|NT]) :- normalise_value(H,NH), l_normalise_values(T,NT).

lookup_and_delete_value(Var,Value,T,UT,ReportError,WF,Finished) :-
    lookup_and_delete_value1(T,Var,Value,UT,ReportError,WF,Finished).

lookup_and_delete_value1([],Var,Value,[],ReportError,WF,Finished) :-
    (ReportError=report_error(WF)
    -> add_abort_error_span(missing_assignment_error,'Statement did not assign to variable: ',Var,unknown,WF)
    /* lookup_and_delete is called only from get_results */
    ; true
    ), no_value_for_variable(Value,Var),
    Finished=true.

lookup_and_delete_value1([bind(Var2,Value2)|T],Var,Value,Res,ReportError,WF,Finished) :-
    lookup_and_delete_value2(Var2,Value2,T,Var,Value,Res,ReportError,WF,Finished).

lookup_and_delete_value2(Var2,Value2,T,Var,Value,Res,ReportError,WF,Finished) :-
    (Var=Var2
    -> Value=Value2, T=Res, Finished=true
    ; Res=[bind(Var2,Value2)|UT],
    lookup_and_delete_value1(T,Var,Value,UT,ReportError,WF,Finished)
).

lookup_value(Id,State,Val) :-
    (member_bind(Id,Val,State) %safe_member(bind(Id,Val),State,lookup_value)
    -> check_val(Val,Id,State)
).

lookup_value(Id,LocalState,State,Val) :-
    (member_bind(Id,Val,LocalState) %safe_member(bind(Id,Val),LocalState,lookup_value__4)
    -> check_val(Val,Id,LocalState)
    ; member_bind(Id,Val,State) -> check_val(Val,Id,State)).

lookup_value_for_existing_id(Id,State,Res) :-
    (member_bind(Id,Val,State) % safe_member(bind(Id,Val),State,lookup_value_for_existing_id)
    -> check_val(Val,Id,State),Res=Val
    ; add_internal_error('Call Failed: ',lookup_value_for_existing_id(Id,State,Res)),
    Res=term(undefined)
).

lookup_value_for_existing_id(Id,LocalState,State,Val) :-
    (member_bind(Id,Val,LocalState) %safe_member(bind(Id,Val),LocalState,lookup_value_for_existing_id__4)
    -> check_val(Val,Id,LocalState)
    ; lookup_value_for_existing_id(Id,State,Val)).

lookup_value_for_existing_id_wf(Id,State,Val,WF) :-
    (member_bind(Id,Val,State) %safe_member(bind(Id,Val),LocalState,lookup_value_for_existing_id__4)
    -> check_val_with_span_wf(Val,Id,State,unknown,WF)
    ; add_state_error_wf(lookup_value_for_existing_id_wf,'Cannot find identifier: ',Id,unknown,WF),
    fail
).

lookup_value_for_existing_id_wf(Id,LocalState,State,Val,WF) :-
    (member_bind(Id,Val,LocalState) %safe_member(bind(Id,Val),LocalState,lookup_value_for_existing_id__4)
    -> check_val_with_span_wf(Val,Id,LocalState,unknown,WF)
    ; lookup_value_for_existing_id_wf(Id,State,Val,WF)).

lookup_value_with_span_wf(Id,LocalState,State,Val,Span,WF) :-
    (member_bind(Id,Val,LocalState) %safe_member(bind(Id,Val),LocalState,lookup_value__4)
    -> check_val_with_span_wf(Val,Id,LocalState,Span,WF)
    ; member_bind(Id,Val,State) -> check_val_with_span_wf(Val,Id,State,Span,WF)).

lookup_value_without_check(Id,LocalState,State,Val) :- % does not check if value is undefined
    (member_bind(Id,Val,LocalState) %safe_member(bind(Id,Val),LocalState,lookup_value__4)
    -> true
    ; member_bind(Id,Val,State) -> true).

member_bind(Id,Val,[H|T]) :-
    arg(1,H,Id) -> arg(2,H,Val) ; member_bind(Id,Val,T).

merge_remove([],Var,NewVal,[bind(Var,NewVal)]).

merge_remove([bind(Var2,Val2)|T2],Var1,Val1,[bind(Var2,Val2)|NewT2]) :-
    merge_remove_aux(Var2,T2,Var1,Val1,NewT2).

merge_remove_aux(Var2,T2,Var1,Val1,NewT2) :-
    (Var1=Var2
    -> NewT2=T2 /* binding in second updates overrides first update */
    ; merge_remove(T2,Var1,Val1,NewT2)
).

merge_updates([],RHSUpdates,RHSUpdates).

merge_updates([Bind|LHT],RHSUpdates,Rest) :-
    merge_updates2( Bind,LHT,RHSUpdates,Rest).

merge_updates2(bind(Var,NewVal),LHT,RHSUpdates,Rest) :-
    merge_remove(RHSUpdates,Var,NewVal,RHSUpdates2),
    merge_updates(LHT,RHSUpdates2,Rest).

ncb(V,R) :- var(V),!, R=V.

ncb(bool_set,R) :- !, R=bool_set.

ncb(truth,R) :- !, R=truth.

ncb(event_b_identity,R) :- !, R=event_b_identity.

ncb(falsity,R) :- !, R=falsity.

ncb(max_int,R) :- !, R=max_int.

ncb(min_int,R) :- !, R=min_int.

ncb(value(V),value(NV)) :- !,normalise_value_for_var('$closure_body',V,NV).

ncb(integer(X),integer(NX)) :- !, X=NX.

ncb(identifier(X),identifier(NX)) :- !, X=NX.

ncb(float_set,R) :- !, R=float_set.

ncb(real(X),real(NX)) :- !, X=NX.

ncb(real_set,R) :- !, R=real_set.

ncb(string(X),string(NX)) :- !, X=NX.

ncb(string_set,R) :- !, R=string_set.

ncb(integer_set(X),integer_set(NX)) :- !, X=NX.

ncb(set_extension(X),set_extension(NX)) :- !, X=NX.

ncb(partition(S,L),partition(NS,NL)) :- !, normalise_closure_body(S,NS),
    maplist(normalise_closure_body,L,NL).

ncb(general_sum(Ids,Condition,Expression),general_sum(Ids,NC,NE)) :- !,
    normalise_closure_body(Condition,NC),normalise_closure_body(Expression,NE).

ncb(general_product(Ids,Condition,Expression),general_product(Ids,NC,NE)) :- !,
    normalise_closure_body(Condition,NC),normalise_closure_body(Expression,NE).

ncb(sequence_extension(X),sequence_extension(NX)) :- !, X=NX.

ncb(external_function_call(F,L),external_function_call(F,LL)) :- !, L=LL.

ncb(external_pred_call(F,L),external_pred_call(F,LL)) :- !, L=LL.

ncb(equal(A,B),equal(NA,NB)) :- !, normalise_closure_body(A,NA), normalise_closure_body(B,NB).

ncb(couple(A,B),couple(NA,NB)) :- !, normalise_closure_body(A,NA), normalise_closure_body(B,NB).

ncb(interval(A,B),interval(NA,NB)) :- !, normalise_closure_body(A,NA), normalise_closure_body(B,NB).

ncb(function(A,B),function(NA,NB)) :- !, normalise_closure_body(A,NA), normalise_closure_body(B,NB).

ncb(operation_call_in_expr(A,B),operation_call_in_expr(NA,B)) :- !,
    normalise_closure_body(A,NA).

ncb(relations(A,B),relations(NA,NB)) :- !, normalise_closure_body(A,NA), normalise_closure_body(B,NB).

ncb(member(A,B),member(NA,NB)) :- !, normalise_closure_body(A,NA), normalise_closure_body(B,NB).

ncb(not_member(A,B),not_member(NA,NB)) :- !, normalise_closure_body(A,NA), normalise_closure_body(B,NB).

ncb(negation(B),negation(NB)) :- !, normalise_closure_body(B,NB).

ncb(conjunct(A,B),conjunct(NA,NB)) :- !, normalise_closure_body(A,NA), normalise_closure_body(B,NB).

ncb(disjunct(A,B),disjunct(NA,NB)) :- !, normalise_closure_body(A,NA), normalise_closure_body(B,NB).

ncb(equivalence(A,B),equivalence(NA,NB)) :- !, normalise_closure_body(A,NA), normalise_closure_body(B,NB).

ncb(if_then_else(A,B,C),if_then_else(NA,NB,NC)) :- !,
    normalise_closure_body(A,NA), normalise_closure_body(B,NB), normalise_closure_body(C,NC).

ncb(implication(A,B),implication(NA,NB)) :- !, normalise_closure_body(A,NA), normalise_closure_body(B,NB).

ncb(comprehension_set(V,B),comprehension_set(V,NB)) :- !, normalise_closure_body(B,NB).

ncb(convert_bool(B),convert_bool(NB)) :- !, normalise_closure_body(B,NB).

ncb(convert_real(B),convert_real(NB)) :- !, normalise_closure_body(B,NB).

ncb(convert_int_floor(B),convert_int_floor(NB)) :- !, normalise_closure_body(B,NB).

ncb(convert_int_ceiling(B),convert_int_ceiling(NB)) :- !, normalise_closure_body(B,NB).

ncb(exists(IDs,B),exists(IDs,NB)) :- !, normalise_closure_body(B,NB).

ncb(forall(IDs,A,B),forall(IDs,NA,NB)) :- !, normalise_closure_body(A,NA), normalise_closure_body(B,NB).

ncb(assertion_expression(Cond,ErrMsg,Expr),assertion_expression(NA,ErrMsg,NB)) :- !,
    normalise_closure_body(Cond,NA), normalise_closure_body(Expr,NB).

ncb(freetype_case(FT,IsCase,Expr),freetype_case(FT,IsCase,NB)) :- !,
    normalise_closure_body(Expr,NB).

ncb(freetype_constructor(Id,Case,Expr),freetype_constructor(Id,Case,NB)) :- !,
    normalise_closure_body(Expr,NB).

ncb(freetype_destructor(Id,Case,Expr),freetype_destructor(Id,Case,NB)) :- !,
    normalise_closure_body(Expr,NB).

ncb(record_field(R,Name),record_field(NR,Name)) :- !,
    normalise_closure_body(R,NR).

ncb(rec(Fields),rec(NFields)) :- !,
    ncb_fields(Fields,NFields).

ncb(recursive_let(ID,R),recursive_let(ID,NR)) :- !,
    normalise_closure_body(R,NR).

ncb(kodkod(Id,Ids),R) :- !, R=kodkod(Id,Ids).

ncb(lazy_let_expr(Id,E,Expr),lazy_let_expr(Id,NE,NExpr)) :- !, normalise_closure_body(E,NE),
    normalise_closure_body(Expr,NExpr).

ncb(lazy_let_pred(Id,E,Pred),lazy_let_pred(Id,NE,NPred)) :- !, normalise_closure_body(E,NE),
    normalise_closure_body(Pred,NPred).

ncb(lazy_lookup_expr(X),lazy_lookup_expr(NX)) :- !, X=NX.

ncb(lazy_lookup_pred(X),lazy_lookup_pred(NX)) :- !, X=NX.

ncb(let_predicate(Ids,AssignmentExprs,Pred),let_predicate(Ids,AssignmentExprs,NPred)) :- !,
    normalise_closure_body(Pred,NPred).

ncb(let_expression(Ids,AssignmentExprs,Expr),let_expression(Ids,AssignmentExprs,NExpr)) :- !,
    normalise_closure_body(Expr,NExpr).

ncb(let_expression_global(Ids,AssignmentExprs,Expr),let_expression_global(Ids,AssignmentExprs,NExpr)) :- !,
    normalise_closure_body(Expr,NExpr).

ncb(F,NF) :- functor(F,Op,1),
    (unary_function(Op,_,_) ; unary_in_boolean_type(Op,_)), !,
    arg(1,F,Arg1), functor(NF,Op,1), arg(1,NF,NormArg1),
    normalise_closure_body(Arg1,NormArg1).

ncb(F,NF) :- functor(F,Op,2),
    (binary_function(Op,_,_) ; kernel_mappings:binary_boolean_operator(Op,_,_) ; binary_in_boolean_type(Op,_)), !,
    arg(1,F,Arg1),arg(2,F,Arg2), functor(NF,Op,2), arg(1,NF,NormArg1), arg(2,NF,NormArg2),
    normalise_closure_body(Arg1,NormArg1),
    normalise_closure_body(Arg2,NormArg2).

ncb(X,X) :- print(ncb(X)),nl.

ncb_fields([],[]).

ncb_fields([field(Name,Expr)|T], [field(Name,NExpr)|NT]) :-
    normalise_closure_body(Expr,NExpr),
    ncb_fields(T,NT).

no_value_for_variable(term(no_value_for(Var)),Var).

normalise2([H|T],Res) :- !,
    normalise_list([H|T],Res).

normalise2((A,B),(NA,NB)) :- !, normalise_value(A,NA), normalise_value(B,NB).

normalise2(global_set(GS),N) :- !,
    (b_integer_or_real_or_string_set(GS)
    -> N = global_set(GS) /* can be very large or infinite, so don't expand */
    ; all_elements_of_type(GS,Res),
    normalise2(Res,N)).

normalise2(freetype(ID),N) :- is_enumerated_set_freetype(ID), !, % triggers in test 2439
    % TODO: also treat freetypes like setX = el1, el23(BOOL)
    expand_freetype(ID,List,no_wf_available),
    normalise_value(List,N).

normalise2(avl_set(A),R) :- !,
    (%empty_avl(A)
    A=empty
    -> R=[] ;
    %A = node(_,_,_,empty,_) -> R = avl_set(A) ; % avoid normalising certain one and two element sets; does not seem to bring any improvement
    avl_to_list(A,L), ord_list_to_avl(L,B), R=avl_set(B)).

normalise2(string(S),R) :- !, R=string(S).

normalise2(int(S),R) :- !, R=int(S).

normalise2(fd(N,T),R) :- !, R=fd(N,T).

normalise2(rec(Fields),R) :- !, R=rec(NFields), normalise_fields(Fields,NFields).

normalise2(V,V).

normalise3((A,B),(NA,NB)) :- !, normalise_value(A,NA), normalise_value(B,NB).

normalise3(V,Res) :- equal_object(V,Res,normalise3).

normalise_closure_body(b(OP,T,I),b(NOP,T,FI)) :-
    (var(I) -> print(b(OP,T,I)),nl , when(nonvar(OP),(print(b(OP,T,I)),nl)) ; true),
    filter_info(OP,I,FI),
    ncb(OP,OP2),
    (can_be_computed(OP2) % when compiling not all information was available for computation, now it is
    -> b_interpreter:b_compute_expression_nowf(b(OP,T,I),[],[],Val,'normalising closure body',0),
    %print(comp(Val)),nl,
    ncb(value(Val),NOP) % TO DO: better apply the can_be_computed check after ncb, if performance ok
    ; NOP=OP2).

normalise_fields([],[]).

normalise_fields([field(Name,Val)|T], [field(Name,NVal)|NT]) :- normalise_value(Val,NVal),
    normalise_fields(T,NT).

normalise_list(List,Res) :-
    ground_value_check(List,ListGround), % this is slightly slower than ground() for long lists not containing avl_set values
    normalise_list_aux(ListGround,List,Res).

normalise_list_aux(_,[H|T],Res) :- % used to check T==[]; for test 2420 T ist not [] and we get a time-out
    cannot_be_normalised_in_avl(H),!,
    % do not expand this; would lead to enumeration warning; cf test 2157,
    sort([H|T],Sorted),
    kernel_objects:equal_object(Res,Sorted,normalise_list).

normalise_list_aux(_,List,Res) :-
    % catch enumeration warnings in case infinite set is later in list
    on_enumeration_warning(
    construct_avl_from_lists(List,Avl),
    Avl=List),
    kernel_objects:equal_object(Res,Avl,normalise_list).

normalise_state(I,O) :-
    extract_vars(I,VI,VO,O),
    normalise_store(VI,VO).

normalise_states([],[]).

normalise_states([I|Irest],[O|Orest]) :-
    normalise_state(I,O),
    normalise_states(Irest,Orest).

normalise_store(T,NT) :-
    preferences:get_computed_preference(convert_closures_into_explicit_form_for_store,EXPAND),
    normalise_store1(T,EXPAND,NT).

normalise_store1([],_Expand,Res) :- !, Res=[].

normalise_store1([bind(Var,Val)|T],EXPAND,Res) :- !, Res = [bind(Var,NVal)|NT],
    %print(normalise(Val)),nl,print(Var),nl,
    normalise_value_for_var(Var,EXPAND,Val,NVal),
    normalise_store1(T,EXPAND,NT).

normalise_store1(Store,E,Res) :-
    add_internal_error('Illegal store: ',normalise_store1(Store,E,Res)),
    Res=Store.

normalise_value(V,Res) :-
    (nonvar(V),var(Res) -> normalise2(V,ResR),Res=ResR ; normalise3(V,Res)).

normalise_value_for_var(Var,Val,NormVal) :-
    preferences:get_computed_preference(convert_closures_into_explicit_form_for_store,EXPAND),
    normalise_value_for_var(Var,EXPAND,Val,NormVal).

normalise_value_for_var(Var,EXPAND,Val,NormVal) :-
    % print(check_var(Var)),nl, b_interpreter:check_value(Val,Var), print(ok(Var)),nl,
    expand_closure_value_for_normalisation(Val,EXPAND,Var,ENewVal), % also normalises values inside closure if not expanded
    normalise_value(ENewVal,NormVal). % , tools_printing:print_term_summary(normalised(ENewVal,NormVal)).

safe_member(_,[],_) :- !,fail.

safe_member(X,[H|T],Loc) :- !, (X=H ; safe_member(X,T,Loc)).

safe_member(X,T,Loc) :- add_internal_error('Argument not a list: ',safe_member(X,T,Loc)),fail.

save_updates_in_existing_store([],_Store).

save_updates_in_existing_store([bind(Var,Value)|Urest],Store) :-
    save_updates_in_existing_store2(Var,Value,Store),
    save_updates_in_existing_store(Urest,Store).