b_normal_form

bool_choice(TrueValue,FalseValue,ChoiceBool, ResultExpression) :-
    %{x,r|x:BOOL & (ChoiceBool=TRUE => r=TrueValue) & (ChoiceBool=False => r=FalseValue)}(TRUE)
    boolean_true(BTRUE),
    EQ = b(equal(ChoiceBool,BTRUE),pred,[]),
    get_texpr_type(TrueValue,Type),
    ResultExpression = b(if_then_else(EQ,TrueValue,FalseValue),Type,[]).

boolean_false(b(boolean_false,boolean,[])).

boolean_true(b(boolean_true,boolean,[])).

check(C) :- (C -> true ; print('CALL FAILED: '), nl, print(C),nl, trace, C).

complete_partial_updates(b(parallel(List),subst,I),b(New,subst,I),Pre,NewPre,Info) :- !,
    get_fun_modifies(Info,FunMod),
    complete_partial_updates_list(List,NewList,NewPreds,FunMod),
    construct_par(NewList,New),
    conjunct_predicates([Pre|NewPreds],NewPre).

complete_partial_updates(Body,Body,Pre,Pre,_).

complete_partial_updates_list([PartialUpdate|T], [NewInstruction|TT],RestPreds,FunMod) :-
    function_update3(PartialUpdate,_FID,LHS,UpdateFunction), %print(generate_pre(_FID)),nl,
    get_texpr_info(UpdateFunction,Infos), %print(Infos),nl,
    findall(merge(UF1,UF2),member(merge(UF1,UF2),Infos),Merges), Merges = [_|_],
    !,
    maplist(gen_merge_pred(LHS),Merges,PL),
    conjunct_predicates(PL,NewPred),
    NewInstruction = b(precondition(NewPred,PartialUpdate),subst,[]), % In Event-B we could translate this into a theorem guard
    complete_partial_updates_list(T,TT,RestPreds,FunMod).

complete_partial_updates_list(L,L,[],_FunMod).

construct_any(Par,Pre,Body,Info,b(any(Par,Pre,Body),subst,Info)).

construct_complement(Set,b(set_subtraction(FullType,Set),Type,[])) :-
    get_texpr_type(Set,set(Type)),
    translate:type_set(Type,FullType).

construct_domain_subtraction(DEL,FunID,DomRes) :-
    get_texpr_type(FunID,Type),
    DomRes = b(domain_subtraction(DEL,FunID),Type,[]).

construct_full_update(TypedID,RHS,b(assign_single_id(TypedID,RHS),subst,[])).

construct_function_application(FunID,Arg,Res) :-
    get_texpr_type(FunID,set(couple(_AT,ET))),
    Res = b(function(FunID,Arg),ET,[]).

construct_function_update3(FunID,UpdateFunction,Info, Body) :-
    Body = b(assign([FunID],[NewFunID]),subst,Info),
    construct_function_application(UpdateFunction,FunID,NewFunID).

construct_override(FunID,Update,Override) :-
    get_texpr_type(Update,Type),
    Override = b(overwrite(FunID,Update),Type,[]).

construct_par([],skip).

construct_par([A],E) :- get_texpr_expr(A,E).

construct_par([A,B|T],parallel([A,B|T])).

construct_set_subtraction(DEL,FunID,DomRes) :-
    get_texpr_type(FunID,Type),
    DomRes = b(set_subtraction(DEL,FunID),Type,[]).

construct_skip_eq(ModifiedID,b(equal(IDBT,BFALSE),pred,[])) :- normalizing_mode(asm),!,
    % generate x@=FALSE
    boolean_false(BFALSE),
    update_bool_id(ModifiedID,IDB),
    IDBT = b(identifier(IDB),boolean,[]).

construct_skip_eq(ModifiedID,b(equal(TID,TIDP),pred,[])) :-
    % generate x=x'
    TID = b(identifier(ModifiedID),Type,[]),
    prime_id(ModifiedID,IDP),
    TIDP = b(identifier(IDP),Type,[]).

construct_skip_fun_eq(update(_FID,IDB),b(equal(IDBT,BFALSE),pred,[])) :- !,
    % generate x@=FALSE for function updates
    boolean_false(BFALSE),
    IDBT = b(identifier(IDB),boolean,[]).

construct_union(b(empty_set,_,_),U,R) :- !, R=U.

construct_union(U,b(empty_set,_,_),R) :- !, R=U.

construct_union(Update1,Update2,Res) :-
    get_texpr_type(Update1,UT),
    Res = b(union(Update1,Update2),UT,[]).

create_or([A],A).

create_or([A,B|T],b(convert_bool(DISJ),boolean,[])) :-
    % create bool(A=TRUE or B=TRUE ...)
    maplist(eqtrue,[A,B|T],EqList),
    disjunct_predicates(EqList,DISJ).

eqtrue(A,b(equal(A,BTRUE),pred,[])) :- boolean_true(BTRUE).

fresh_update_bool_id(ID,IDB) :-
    (retract(gensym_count(ID,C)) -> true ; C=0),
    C1 is C+1,
    assertz(gensym_count(ID,C1)),
    %ajoin([ID,'@',C1],IDB).
    ajoin([ID,'__upd_',C1],IDB).

fresh_update_fun_id(ID,IDB) :-
    (retract(gensym_countf(ID,C)) -> true ; C=0),
    C1 is C+1,
    assertz(gensym_countf(ID,C1)),
    %ajoin([ID,'@',C1],IDB).
    ajoin([ID,'_uf_',C1],IDB).

full_update(b(assign_single_id(TypedID,RHS),subst,_),ID,TypedID,RHS) :-
    get_texpr_id(TypedID,ID). % RHS should be of form {TRUE|->x', FALSE |->x}(x@)

function_update3(b(assign([FunID],[FunApp]),subst,_),FID,FunID,UpdateFunction) :-
    get_texpr_id(FunID,FID),
    is_update_function_application(FunApp,FunID,UpdateFunction). % we have FunID := UF(FunID)

function_update3(b(assign_single_id(FunID,RHS),subst,_),FID,FunID,UpdateFunction) :-
    get_texpr_id(FunID,FID),
    get_texpr_type(FunID,Type), Type = set(couple(_,_)), % only makes sense for functions/relations
    bool_choice(TrueValue,FalseValue,ChoiceBool, RHS),
    same_texpr(FalseValue,FunID), % no modification if ChoiceBool is FALSE
    fresh_update_fun_id(FID,UFID),
    UpdID = b(identifier(UFID),Type,[]),
    bool_choice(TrueValue,UpdID,ChoiceBool, UpdatedRHS), % in case no modification: return lambda identifier not FunID !
    UpdateFunction = b(lambda([UpdID],b(truth,pred,[]),UpdatedRHS),Type,[is_update_function]).

function_update3(b(assign_single_id(FunID,RHS),subst,_),FID,FunID,UpdateFunction) :-
    get_texpr_id(FunID,FID),
    get_texpr_type(FunID,Type), Type = set(couple(_,_)), % only makes sense for functions/relations
    fresh_update_fun_id(FID,UFID),
    UpdID = b(identifier(UFID),Type,[]),
    UpdateFunction = b(lambda([UpdID],b(truth,pred,[]),RHS),Type,[is_update_function]).

gen_merge_pred(LHS,merge(UF1,UF2),NewPred1) :-
    construct_function_application(UF1,LHS,U1),
    construct_function_application(UF2,U1,U12),
    construct_function_application(UF2,LHS,U2),
    construct_function_application(UF1,U2,U21),
    NewPred1 = b(equal(U12,U21),pred,[]).

gen_update_eq([],P1,P1,P2,P2,[],[]).

gen_update_eq([ModifiedID|TID],InPred1,OutPred1,InPred2,OutPred2,[TID1,TID2|NewIDs],[EQV|NewPreds]) :- % should only occur in asm mode
    % we introduce two new update variables x@1, x@2 and rename accordingly and
    % add predicate (x@=TRUE <=> (x@1=TRUE or x@2=TRUE)
    fresh_update_bool_id(ModifiedID,ID1), TID1 = b(identifier(ID1),boolean,[]),
    fresh_update_bool_id(ModifiedID,ID2), TID2 = b(identifier(ID2),boolean,[]),
    update_bool_id(ModifiedID,IDB),
    rename_bt(InPred1,[rename(IDB,ID1)],IntPred1),
    rename_bt(InPred2,[rename(IDB,ID2)],IntPred2),
    boolean_true(BTRUE),
    EQV = b(equivalence(
    b(equal(b(identifier(IDB),boolean,[]),BTRUE),pred,[]),
    b(disjunct(
    b(equal(TID1,BTRUE),pred,[]),
    b(equal(TID2,BTRUE),pred,[])
    ),pred,[])
    ),pred,[]),
    gen_update_eq(TID,IntPred1,OutPred1,IntPred2,OutPred2,NewIDs,NewPreds).

generate_update_function(Arg,EXPR,Type,IDBT,UF) :-
    fresh_update_fun_id('UU',UFID),
    UpdID = b(identifier(UFID),Type,[]),
    UpdateSET = b(set_extension([Update]),Type,[]),
    get_texpr_type(Arg,AT),
    get_texpr_type(EXPR,ET),
    Update = b(couple(Arg,EXPR),couple(AT,ET),[]),
    construct_override(UpdID,UpdateSET,OVER), % UU<+ {Arg |-> Expr}
    bool_choice(OVER,UpdID,IDBT,LAMBDARES),
    UF = b(lambda([UpdID],b(truth,pred,[]),LAMBDARES),Type,[is_update_function]).

get_fun_modifies(Info,Mod) :- member(fun_modifies(M),Info),!, Mod=M.

get_fun_modifies(_,[]).

get_fun_modifies(Info1,Info2,M12) :-
    get_fun_modifies(Info1,M1),
    get_fun_modifies(Info2,M2),
    append(M1,M2,M12).

get_modifies(Info,Mod) :- member(modifies(M),Info),!, Mod=M.

get_modifies(Info,[]) :- add_error(get_modifies,'No modifies info: ',Info).

if_then_else(if([b(if_elsif(Cond,THEN),subst,_)|ELSE]),
    Cond, THEN, ELSE).

is_update_function_application(b(function(UpdateFunction,Arg1),_,_), Arg2, UpdateFunction) :-
    same_texpr(Arg1,Arg2),
    get_texpr_info(UpdateFunction,Infos),
    member(is_update_function,Infos).

join_parameters([],R,R,_).

join_parameters([ID1|T],ID2,Res,RaiseError) :-
    get_texpr_id(ID1,ID),
    get_texpr_id(IDTemplate,ID),
    member(IDTemplate,ID2),
    !,
    (RaiseError=raise_error ->
    add_error(join_parameters,'Identifier clash when joining parameters: ',ID)
    ; print_message(merging_parameter(ID))),
    join_parameters(T,ID2,Res,RaiseError).

join_parameters([ID|T],ID2,[ID|Res],RE) :- join_parameters(T,ID2,Res,RE).

merge_function_updates([],[]).

merge_function_updates([H|T],[NH|NT]) :-
    function_update3(H,FID,FunID,UF1),
    select(H2,T,T2),
    function_update3(H2,FID,_,UF2), print(merge_fun_update2(FID)),nl,
    !,
    merge_update_functions(UF1,UF2,UF12),
    % TO DO: check UF1(UF2(FunID)) = UF2(UF1(FunID))
    construct_function_update3(FunID,UF12,[],NH),
    merge_function_updates(T2,NT).

merge_function_updates([H|T],[H|NT]) :- merge_function_updates(T,NT).

merge_update_functions(UF1, UF2,
    b(lambda([ID1],Pred,FUNAPP),Type,[merge(UF1,UF2)|Info])) :-
    UF1 = b(lambda([ID1],Pred,RES1),Type,Info1),
    get_texpr_info(UF2,Info2),
    append(Info1,Info2,Info),
    construct_function_application(UF2,RES1,FUNAPP).

normalize_body(Body,Res) :-
    retractall(gensym_count(_,_)),
    % TO DO: rename all local variables (ANY) so that they are distinct
    normalize_body_aux(Body,Par,Pre,NewBody,Info),
    % to do: now merge all partial function updates (at various levels) with full updates
    % i.e. merge f := f' and f := f <+ Updates into f := f' with condition Updates <: f'
    check(complete_partial_updates(NewBody,NewBody2,Pre,Pre2,Info)),
    construct_any(Par,Pre2,NewBody2,Info,Res).

normalize_body2(assign_single_id(LHS,EXPR),I,Par,Pre,Body,Info) :- normalizing_mode(asm),
    LHS = b(function(FunID,Arg),_,_), % f(Arg) := EXPR
    get_texpr_id(FunID,FID), get_texpr_type(FunID,FunType),
    print(update_fun(FID,FunType,Arg)),nl,
    !,
    fresh_update_bool_id(FID,IDB),
    IDBT = b(identifier(IDB),boolean,[]), % boolean variable : TRUE if update performed
    Par = [IDBT],
    generate_update_function(Arg,EXPR,FunType,IDBT,UpdateFunction),
    construct_function_update3(FunID,UpdateFunction,Info, Body), % TO DO: add UpdateFunction as parameter
    Info = [fun_modifies([update(FID,IDB)]),modifies([])|I],
    boolean_true(BTRUE),
    Pre = b(equal(IDBT, BTRUE),pred,[]).

normalize_body2(assign_single_id(LHS,EXPR),I,Par,Pre,Body,Info) :-
    LHS = b(function(FunID,Arg),ET,_),
    !,
    % rewrite f(A) := E into f := f <+ {A|->E}
    get_texpr_type(Arg,AT),
    Override = b(overwrite(FunID,CSET),set(couple(AT,ET)),[]),
    CSET = b(set_extension([Update]),set(couple(AT,ET)),[]),
    Update = b(couple(Arg,EXPR),couple(AT,ET),[]),
    normalize_body2(assign_single_id(FunID,Override),I,Par,Pre,Body,Info).

normalize_body2(assign_single_id(LHS,EXPR),I,Par,Pre,Body,Info) :- normalizing_mode(asm),
    !,
    %get_texpr_id(LHS,ID),
    LHS = b(identifier(ID),Type,IDInfo),
    prime_id(ID,IDP), update_bool_id(ID,IDB),
    IDPT = b(identifier(IDP),Type,IDInfo), % new potential value for Identifier
    IDBT = b(identifier(IDB),boolean,IDInfo), % boolean variable : TRUE if update performed
    Par = [IDPT,IDBT],
    boolean_true(BTRUE),
    conjunct_predicates([b(equal(IDPT, EXPR),pred,[]),
    b(equal(IDBT, BTRUE),pred,[])], Pre),
    Info = [modifies([ID])|I],
    bool_choice(IDPT,LHS,IDBT,RHS),
    % Body = x := {TRUE|->x', FALSE |->x}(x@)
    Body = b(assign_single_id(LHS,RHS),subst,I).

normalize_body2(assign_single_id(LHS,EXPR),I,Par,Pre,Body,Info) :- !,
    %get_texpr_id(LHS,ID),
    LHS = b(identifier(ID),Type,IDInfo),
    prime_id(ID,IDP),
    IDPT = b(identifier(IDP),Type,IDInfo),
    Par = [IDPT],
    Pre = b(equal(IDPT, EXPR),pred,[]),
    Info = [modifies([ID])|I],
    Body = b(assign_single_id(LHS,IDPT),subst,I).

normalize_body2(assign([LHS],[EXPR]),I,Par,Pre,Body,Info) :- !,
    normalize_body2(assign_single_id(LHS,EXPR),I,Par,Pre,Body,Info).

normalize_body2(assign([LHS|ET],[EXPR|LT]),I,Par,Pre,Body,Info) :-
    normalize_body2(assign_single_id(LHS,EXPR),I,Par1,Pre1,Body1,Info1),
    normalize_body2(assign(ET,LT),I,Par2,Pre2,Body2,Info2),
    !,
    join_parameters(Par1,Par2,Par,no_errors), % to do: rename apart
    conjunct_predicates([Pre1,Pre2],Pre),
    get_modifies(Info1,M1),
    get_modifies(Info2,M2),
    union(M1,M2,M12),
    % TO DO: check intersection
    par_subst(Body1,Body2,Body),
    get_fun_modifies(Info1,Info2,U12), % always distinct variables; nothing needs to be done
    Info = [modifies(M12),fun_modifies(U12)|I].

normalize_body2(parallel([A]),_I,Par,Pre,Body,Info) :- !,
    normalize_body_aux(A,Par,Pre,Body,Info).

normalize_body2(parallel([A|B]),I,Par,Pre,Body,Info) :-
    normalize_body_aux(A,Par1,Pre1,Body1,Info1),
    normalize_body2(parallel(B),I,Par2,Pre2,Body2,Info2),
    !,
    join_parameters(Par1,Par2,Par12,no_errors),
    get_modifies(Info1,M1),
    get_modifies(Info2,M2),
    union(M1,M2,M12),
    % TO DO: check intersection ?
    get_fun_modifies(Info1,Info2,U12), % always distinct variables; nothing needs to be done
    Info = [modifies(M12),fun_modifies(U12)|I],
    intersection(M1,M2,Both),
    gen_update_eq(Both,Pre1,NewPre1,Pre2,NewPre2,NewIDs,NewPreds),
    append(Par12,NewIDs,Par),
    conjunct_predicates([NewPre1,NewPre2|NewPreds],Pre),
    par_subst(Body1,Body2,Body).

normalize_body2(if([]),I,Par,Pre,Body,Info) :-
    normalize_body2(skip,I,Par,Pre,Body,Info).

normalize_body2(IF,_I,Par,Pre,Body,Info) :-
    if_then_else(IF,TRUTH,Body0,_),
    is_truth(TRUTH),!,
    normalize_body_aux(Body0,Par,Pre,Body,Info).

normalize_body2(IF,I,Par,Pre,Body,Info) :-
    if_then_else(IF,Cond,Body0,ELSE),!,
    % if with else:
    normalize_body_aux(Body0,Par1,Pre1,Body1,Info1),
    normalize_body2(if(ELSE),I,Par2,Pre2,Body2,Info2),
    join_parameters(Par1,Par2,Par,no_errors), % to do: rename apart
    get_modifies(Info1,M1),
    get_fun_modifies(Info1,U1),
    get_modifies(Info2,M2),
    get_fun_modifies(Info2,U2),
    subtract(M1,M2,M1only),
    maplist(construct_skip_eq,M1only,SkipM1EQList),
    maplist(construct_skip_fun_eq,U1,SkipU1EQList), % U1 and U2 necessarily distinct
    append(SkipM1EQList,SkipU1EQList,Skip1),
    conjunct_predicates([Pre2|Skip1],NewPre2),
    subtract(M2,M1,M2only),
    maplist(construct_skip_eq,M2only,SkipM2EQList),
    maplist(construct_skip_fun_eq,U2,SkipU2EQList), % U1 and U2 necessarily distinct
    append(SkipM2EQList,SkipU2EQList,Skip2),
    conjunct_predicates([Pre1|Skip2],NewPre1),
    create_implication(Cond,NewPre1,IMP1),
    create_negation(Cond,NCond),
    create_implication(NCond,NewPre2,IMP2),
    conjunct_predicates([IMP1,IMP2],Pre),
    par_subst(Body1,Body2,Body),
    %print(if(U1,U2,M1,M2)),nl,translate:print_subst(Body),nl,
    union(M1,M2,M12),
    get_fun_modifies(Info1,Info2,U12),
    Info=[modifies(M12),fun_modifies(U12)|I].

normalize_body2(if(IfList),_I,_Par,_Pre,_Body,_Info) :-
    print(uncovered_if(IfList)),nl,fail.

normalize_body2(let(Parameters,Defs,Body1),I,Par,Pre,Body,Info) :-
    conjunct_predicates(Defs,Pre1),
    normalize_body2(any(Parameters,Pre1,Body1),I,Par,Pre,Body,Info).

normalize_body2(any(Par1,Pre1,Body1),I,Par,Pre,Body,Info) :-
    normalize_body_aux(Body1,Par2,Pre2,Body2,Info2),
    join_parameters(Par1,Par2,Par,raise_error), % to do: rename apart
    conjunct_predicates([Pre1,Pre2],Pre),
    Body=Body2, append(I,Info2,Info).

normalize_body2(skip,Info,[],Truth,Body,[modifies([])|Info]) :-
    Truth=b(truth,pred,[]),
    Body=b(skip,subst,[]).

normalize_body_aux(BE,Par,Pre,Body,Info) :-
    ((BE = b(E,subst,I),
    normalize_body2(E,I,Par,Pre,Body,Info))
    -> true
    %, print(normalised(Par,Pre,Body,Info)),nl
    ; print('Could not normalize: '),
    translate:print_subst(BE),nl,
    tools_printing:trace_print(BE,5),
    BE = b(_,subst,I),
    Pre=b(truth,pred,[]), Body=BE, Info=I
).

normalizing_mode(asm).

old_bool_choice(TrueValue,FalseValue,ChoiceBool, ResultExpression) :-
    % ResultExpression = {TRUE|->TrueValue, FALSE |->FalseValue}(ChoiceBool)
    boolean_true(BTRUE),
    boolean_false(BFALSE),
    get_texpr_type(TrueValue,Type),
    FUN = [b(couple(BTRUE,TrueValue),couple(boolean,Type),[]),
    b(couple(BFALSE,FalseValue),couple(boolean,Type),[])],
    % FUNC = {TRUE |-> x', FALSE |-> x}
    FUNC = b(set_extension(FUN),set(couple(boolean,Type)),[]),
    ResultExpression = b(function(FUNC,ChoiceBool),Type,[]).

par_subst(A,B,Res) :- par_subst_aux(A,B,AB),
    ((AB=b(parallel(U),subst,I),
    check(merge_function_updates(U,MU)))
    -> Res = b(parallel(MU),subst,I)
    ; Res = AB). % , nl,print('PARALLEL: '), print(Res),nl,nl.

par_subst_aux(b(skip,_,_),S2,R) :- !, R=S2.

par_subst_aux(S1,b(skip,_,_),R) :- !, R=S1.

par_subst_aux(S1,S2,R) :- same_subst(S1,S2),!,R=S1.

par_subst_aux(b(parallel([]),subst,_I1),S2,Res) :- !, Res=S2.

par_subst_aux(b(parallel([S1|T1]),subst,I1),S2,Res) :- !,
    par_subst_aux(S1,S2,S12),
    par_subst_aux(b(parallel(T1),subst,I1),S12,Res).

par_subst_aux(S1,b(parallel(S2),subst,I),Res) :- !,
    (same_member(S1,S2) -> Res = b(parallel(S2),subst,I)
    ; Res= b(parallel([S1|S2]),subst,I)).

par_subst_aux(S1,S2,b(parallel([S1,S2]),subst,[])).

prime_id(ID,IDP) :- % generate the identifier representing the value of ID after the operation
    %ajoin([ID,''''],IDP).
    ajoin([ID,'__'],IDP).

print_normal_forms :-
    b_get_machine_operation_for_animation(Name,_Results,_Parameters,Body,_OType,_TopLevel),
    format('/* ORIGINAL FORM for ~w~n',[Name]),
    translate:print_subst(Body),nl,
    normalize_body(Body,NBody),
    format(' NORMAL FORM: */~n ~w = ',[Name]),
    translate:print_subst(NBody),nl,nl,
    fail.

print_normal_forms.

same_member(X,L) :- member(XX,L), same_subst(XX,X).

same_subst(S1,S2) :- same_texpr(S1,S2).

update_bool_id(ID,IDB) :- % generate the boolean identfier which is TRUE if an update is performed
    ajoin([ID,'__upd_'], IDB).

update_occurs_pred(ID,b(equal(IDBT, BTRUE),pred,[])) :-
    boolean_true(BTRUE),
    update_bool_id(ID,IDB),
    IDBT = b(identifier(IDB),boolean,[]). % boolean variable : TRUE if update performed