before_after_predicates

add_else_if_missing([],[DefaultElse]) :-
    safe_create_texpr(if_elsif(b(truth,pred,[]),b(skip,subst,[])),subst,DefaultElse).

add_else_if_missing([If|Ifs],[If|Ifs]) :-
    get_texpr_expr(If,if_elsif(Test,_)),
    is_truth(Test), !.

add_else_if_missing([If|Ifs],[If|MoreIfs]) :-
    add_else_if_missing(Ifs,MoreIfs).

add_missing_equalities([],PredWithoutEqualities,Res) :- !, Res=PredWithoutEqualities.

add_missing_equalities(AllVariables,PredWithoutEqualities,PredWithEqualities) :-
    find_typed_identifier_uses(PredWithoutEqualities,UsedIdentifiers),
    exclude(primed_var_is_used(UsedIdentifiers),AllVariables,VariablesNotOccuringPrimed),
    maplist(ba_predicate_equal,VariablesNotOccuringPrimed,VariablesNotOccuringPrimed,EqualityPredicates),
    conjunct_predicates([PredWithoutEqualities|EqualityPredicates],PredWithEqualities).

ba_predicate_becomes_such(Ids,Pred,Predicate) :-
    list_renamings_to_primed_vars(Ids,RenamingList),
    rename_bt(Pred,RenamingList,Predicate).

ba_predicate_equal(LHS,RHS,Res) :-
    % LHS := RHS
    get_override(LHS,RHS,TPred), !,
    %nl,translate:print_bexpr(TPred),nl,
    Res=TPred.

ba_predicate_if(IF,BA,AllChangedIDs) :-
    add_else_if_missing(IF,IFWithElse),
    maplist(ba_predicate_if_aux,IFWithElse,BAPreds,ChangedIDs),
    append(ChangedIDs,AllChangedIDs),
    ba_predicate_if(IFWithElse,BAPreds,AllChangedIDs,BA).

ba_predicate_if([IF|IFs],[BAPred|BAPreds],IDs,BA) :-
    get_texpr_expr(IF,if_elsif(Test,_)),
    % if-part
    add_missing_equalities(IDs,BAPred,InnerBAPredIf),
    (is_truth(Test)
    -> InnerBAPredIf = BAPredIf
    ; safe_create_texpr(implication(Test,InnerBAPredIf),pred,BAPredIf)),
    % if there are further else/elseif parts, create pos
    (ba_predicate_if(IFs,BAPreds,IDs,ElsePred)
    -> create_negation(Test,NegTest),
    safe_create_texpr(implication(NegTest,ElsePred),pred,BAPredElse),
    conjunct_predicates([BAPredIf,BAPredElse],BA)
    ; BA = BAPredIf).

ba_predicate_if_aux(IF,BAPred,ChangedIDs) :-
    get_texpr_expr(IF,if_elsif(_,Body)),
    before_after_predicate_no_equalities(Body,BAPred,ChangedIDs).

ba_predicate_member(Set,Id,TPred) :-
    % prime identifiers on the lhs
    prime_typed_identifier(Id,PrimedId),
    safe_create_texpr(member(PrimedId,Set),pred,TPred).

ba_predicate_sequence([Last],Predicate,ChangedIDs) :- !,
    before_after_predicate_no_equalities(Last,Predicate,ChangedIDs).

ba_predicate_sequence([First|SomeMore],Predicate,ChangedIDs) :-
    before_after_predicate_no_equalities(First,FirstPred,ChangesFirst),
    find_typed_identifier_uses(FirstPred,TypedIdsOfFirst),
    % get primed typed identifiers
    include(is_primed_typed_identifier,TypedIdsOfFirst,PrimedTypedIdsOfFirst),
    % rename them if they are already used in SomeMore
    ba_predicate_sequence(SomeMore,SecondPred,FurtherChanges),
    maplist(find_free_id_by_priming(SecondPred),PrimedTypedIdsOfFirst,UnusedPrimedTypedIds),
    maplist(create_id_renaming,PrimedTypedIdsOfFirst,UnusedPrimedTypedIds,RenamingOfFirst),
    rename_bt(FirstPred,RenamingOfFirst,FirstPredAfterReplacement),
    % rename unprimed ids in SecondPred, which are written by FirstPred
    maplist(remove_prime_typed_identifier,PrimedTypedIdsOfFirst,UnprimedTypedIds),
    maplist(create_id_renaming,UnprimedTypedIds,UnusedPrimedTypedIds,RenamingOfSecond),
    rename_bt(SecondPred,RenamingOfSecond,SecondPredAfterReplacement),
   
    conjunct_predicates([FirstPredAfterReplacement,SecondPredAfterReplacement],FullPred),
    % create exists for typed identifiers, which are primed more than once
    include(is_primed_more_than_once,UnusedPrimedTypedIds,TwoOrMorePrimedTypedIds),
    conjunction_to_list(FullPred,FullPredList),
    split_list(contains_some_typed_id(TwoOrMorePrimedTypedIds),FullPredList,ExistsPredList,RemainingPredList),
    conjunct_predicates(ExistsPredList,ExistsPred),
    create_exists(TwoOrMorePrimedTypedIds,ExistsPred,Exists),
    conjunct_predicates([Exists|RemainingPredList],Predicate),
    append(ChangesFirst,FurtherChanges,ChangedIDs).

before_after_predicate_for_operation(OpName,BAPredicate) :-
    b_get_machine_operation(OpName,_Results,_Parameters,OpBody),
    %print(op(OpName)),nl,
    b_get_machine_variables(Variables),
    %b_get_machine_constants(Constants), append(Variables,Constants,VarsAndConsts),
    before_after_predicate_with_equalities(OpBody,Variables,BAPredicate).

before_after_predicate_for_operation_no_equalities(OpName,Parameters,Results,BAPredicate,ChangedIds) :-
    b_get_machine_operation(OpName,Results,Parameters,OpBody),
    % TO DO: rename parameters if clashing
    generate_typing_predicates(Parameters,Typings1),
    generate_typing_predicates(Results,Typings2),
    before_after_predicate_no_equalities_tl4(top_level,OpBody,BAPred,ChangedIds),
    append([Typings1,Typings2,[BAPred]],LP),
    conjunct_predicates(LP,BAPredicate).

before_after_predicate_list_conjunct_with_equalities(Actions,AllIdentifiers,BAPredicateWithEq) :-
    maplist(before_after_predicate_no_equalities_tl3(top_level),Actions,AllPredicates),
    conjunct_predicates(AllPredicates,BAPredicate),
    add_missing_equalities(AllIdentifiers,BAPredicate,BAPredicateWithEq).

before_after_predicate_list_disjunct_with_equalities(Actions,AllIdentifiers,BAPredicate) :-
    maplist(before_after_predicate_no_equalities_tl3(top_level),Actions,AllPredicates),
    maplist(add_missing_equalities(AllIdentifiers),AllPredicates,BAPredicates),
    disjunct_predicates(BAPredicates,BAPredicate).

before_after_predicate_no_equalities(Action,Predicate,ChangedIDs) :-
    get_texpr_expr(Action,Expr),
    before_after_predicate_no_equalities_aux(Expr,Predicate,ChangedIDs).

before_after_predicate_no_equalities_aux(assign_single_id(Id,Pred),Predicate,ChangedIDs) :- !,
    before_after_predicate_no_equalities_aux(assign([Id],[Pred]),Predicate,ChangedIDs).

before_after_predicate_no_equalities_aux(assign(Ids,Preds),Predicate,ChangedIds) :- !,
    maplist(get_changed_id,Ids,ChangedIds),
    maplist(ba_predicate_equal,Ids,Preds,Predicates),
    conjunct_predicates(Predicates,Predicate).

before_after_predicate_no_equalities_aux(becomes_element_of(Ids,Set),Predicate,Ids) :- !,
    maplist(ba_predicate_member(Set),Ids,Predicates),
    % THIS IS WRONG: it asserts that each Id is an element of Set, but the tuple Ids is an element!
    conjunct_predicates(Predicates,Predicate). % should we generate Set /= {} => Predicate

before_after_predicate_no_equalities_aux(becomes_such(Ids,Pred),Predicate,Ids) :- !,
    ba_predicate_becomes_such(Ids,Pred,Predicate).

before_after_predicate_no_equalities_aux(choice(Choices),Predicate,ChangedIDs) :- !,
    maplist(before_after_predicate_no_equalities,Choices,BAChoices,Changes),
    append(Changes,ChangedIDs),
    maplist(add_missing_equalities(ChangedIDs),BAChoices,BAChoicesWithEqualities),
    disjunct_predicates(BAChoicesWithEqualities,Predicate).

before_after_predicate_no_equalities_aux(precondition(Pre,Body),Predicate,ChangedIDs) :- !,
    before_after_predicate_no_equalities(Body,BABody,ChangedIDs),
    create_implication(Pre,BABody,Predicate).

before_after_predicate_no_equalities_aux(witness_then(Pre,Body),Predicate,ChangedIDs) :- !,
    before_after_predicate_no_equalities_aux(assertion(Pre,Body),Predicate,ChangedIDs). % TODO: check if ok, or if we should use SELECT

before_after_predicate_no_equalities_aux(assertion(Pre,Body),Predicate,ChangedIDs) :-
    !,
    before_after_predicate_no_equalities(Body,BABody,ChangedIDs),
    create_implication(Pre,BABody,Predicate1),
    create_negation(Pre,NotPre),
    add_missing_equalities(ChangedIDs,b(truth,pred,[]),NotPrePredicate),
    create_implication(NotPre,NotPrePredicate,Predicate2),
    conjunct_predicates([Predicate1,Predicate2],Predicate).

before_after_predicate_no_equalities_aux(select_when(Pre,Body),Predicate,ChangedIDs) :- !,
    before_after_predicate_no_equalities(Body,BABody,ChangedIDs),
    conjunct_predicates([Pre,BABody],Predicate).

before_after_predicate_no_equalities_aux(select(Whens),Predicate,ChangedIDs) :- !,
    maplist(before_after_predicate_no_equalities,Whens,WhensPredicates,Changes),
    append(Changes,ChangedIDs),
    maplist(add_missing_equalities(ChangedIDs),WhensPredicates,WhensPredicatesWithEqualities),
    disjunct_predicates(WhensPredicatesWithEqualities,Predicate).

before_after_predicate_no_equalities_aux(select(Whens,Else),Predicate,ChangedIDs) :- !,
    maplist(before_after_predicate_no_equalities,Whens,WhensPredicates,Changes),
    maplist(add_missing_equalities(ChangedIDs),WhensPredicates,WhensPredicatesWithEqualities),
    maplist(get_select_conditions,Whens,SelectConditions),
    disjunct_predicates(SelectConditions,ElseTemp),
    create_negation(ElseTemp,ElseLHS),
    before_after_predicate_no_equalities(Else,ElseRHS,ElseChangedIDs),
    append([ElseChangedIDs|Changes],ChangedIDs),
    conjunct_predicates([ElseLHS,ElseRHS],ElsePred),
    add_missing_equalities(ChangedIDs,ElsePred,ElsePredWithEqualities),
    disjunct_predicates([ElsePredWithEqualities|WhensPredicatesWithEqualities],Predicate).

before_after_predicate_no_equalities_aux(sequence(ListOfSteps),Predicate,ChangedIDs) :- !,
    ba_predicate_sequence(ListOfSteps,Predicate,ChangedIDs).

before_after_predicate_no_equalities_aux(if(IfList),Predicate,ChangedIDs) :- !,
    ba_predicate_if(IfList,Predicate,ChangedIDs).

before_after_predicate_no_equalities_aux(let(P,D,B),Predicate,ChangedIDs) :- !,
    before_after_predicate_no_equalities_aux(any(P,D,B),Predicate,ChangedIDs). % TO DO: create let_predicate

before_after_predicate_no_equalities_aux(any(Parameters,PreCond,Body),Predicate,ChangedIDs) :- !,
    before_after_predicate_no_equalities(Body,BABody,ChangedIDs),
    conjunct_predicates([PreCond,BABody],Inner),
    create_or_merge_exists(Parameters,Inner,Predicate).

before_after_predicate_no_equalities_aux(parallel(P),Predicate,ChangedIDs) :- !,
    maplist(before_after_predicate_no_equalities,P,Preds,Changes),
    append(Changes,ChangedIDs),
    conjunct_predicates(Preds,Predicate).

before_after_predicate_no_equalities_aux(skip,Predicate,[]) :- !,
    Predicate = b(truth,pred,[]).

before_after_predicate_no_equalities_aux(var(Parameters,Body),Predicate,ChangedIDs) :- !,
    before_after_predicate_no_equalities(Body,BABody,ChangedIDs),
    create_or_merge_exists(Parameters,BABody,Predicate).

before_after_predicate_no_equalities_aux(rlevent(_Name,_Section,_Stat,_Parameters,Guards,_Thm,Actions,_VWit,_PWit,_Unmod,_AbsEvents),Predicate,ChangedIDs) :- !,
    maplist(before_after_predicate_no_equalities,Actions,BAActions,Changes),
    append(Changes,ChangedIDs),
    conjunct_predicates([Guards|BAActions],Predicate). % should probably be an implication? see precondition.

before_after_predicate_no_equalities_aux(operation_call(OpId,[],[]),Predicate,ChangedIDs) :- !,
    get_texpr_id(OpId,op(OpName)),
    b_get_machine_operation(OpName,[],[],OpBody),
    before_after_predicate_no_equalities(OpBody,Predicate,ChangedIDs).

before_after_predicate_no_equalities_aux(Expr,Predicate,ChangedIDs) :-
    add_error_fail(before_after_predicate,'before-after-predicate implementation missing: ',[Expr,Predicate,ChangedIDs]).

before_after_predicate_no_equalities_tl3(TopLevel,Action,Predicate) :-
    before_after_predicate_no_equalities_tl4(TopLevel,Action,Predicate,_).

before_after_predicate_no_equalities_tl4(TopLevel,Action,Predicate,ChangedIDs) :-
    get_texpr_expr(Action,Expr),
    before_after_predicate_no_equalities_top_level_aux(Expr,Predicate,ChangedIDs,TopLevel).

before_after_predicate_no_equalities_top_level_aux(precondition(Pre,Body),Predicate,ChangedIDs,top_level) :-
    get_preference(treat_outermost_pre_as_select,true),
    !,
    before_after_predicate_no_equalities(Body,BABody,ChangedIDs),
    conjunct_predicates([Pre,BABody],Predicate). % May sometimes have to be an implication (depending on how BA-predicate is used) !

before_after_predicate_no_equalities_top_level_aux(Expr,Pred,ChangedIDs,_) :-
    before_after_predicate_no_equalities_aux(Expr,Pred,ChangedIDs).

before_after_predicate_with_equalities(Action,AllIdentifiers,Predicate) :-
    before_after_predicate_list_conjunct_with_equalities([Action],AllIdentifiers,Predicate).

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

contains_some_typed_id(TypedIds,Pred) :-
    some(contains_typed_id(Pred),TypedIds).

contains_typed_id(Pred,TypedId) :-
    find_typed_identifier_uses(Pred,TypedIds),
    member(TypedId,TypedIds).

create_id_renaming(Var,RenamedVar,rename(Id,RenamedId)) :-
    get_texpr_id(Var,Id),
    get_texpr_id(RenamedVar,RenamedId).

find_free_id_by_priming(Pred,TypedId,FreePrimedTypedId) :-
    find_typed_identifier_uses(Pred,TypedIds),
    (member(TypedId,TypedIds) ->
    prime_typed_identifier(TypedId,PrimedTypedId),
    find_free_id_by_priming(Pred,PrimedTypedId,FreePrimedTypedId)
    ; FreePrimedTypedId = TypedId).

get_changed_id(b(function(FUN,_),_,_),ID) :- !, get_changed_id(FUN,ID).

get_changed_id(ID,ID).

get_override(b(function(FUN,ARG),_Type,_Info),ExprSoFar,Res) :- !, % FUN(ARG) := RHS
    %print(fun(FUN)),nl, translate:print_bexpr(ExprSoFar),nl,
    get_texpr_type(FUN,FType),
    create_couple(ARG,ExprSoFar,Update), % ARG|-> ExprSoFar
    safe_create_texpr(set_extension([Update]),FType,UpdateSET), % {ARG|->ExprSoFar}
    construct_override(FUN,UpdateSET,Override), % FUN <+ {ARG |-> {...}}
    get_override(FUN,Override,Res). % Pass Override as new RHS in case FUN itself is a function application

get_override(FUNID,OverrideExpr,TPred) :-
    get_texpr_id(FUNID,_ID), %print(base(ID)),nl,
    prime_typed_identifier(FUNID,FUNPrimeId),
    safe_create_texpr(equal(FUNPrimeId,OverrideExpr),pred,TPred). % FUN' = FUN <+ {ARG |-> RHS}

get_override(FUNID,OverrideExpr,TPred) :-
    add_internal_error('Cannot compute override: ',get_override(FUNID,OverrideExpr,TPred)),fail.

get_select_conditions(b(select_when(Condition,_),_,_),Condition).

is_primed_more_than_once(TExpr) :-
    get_texpr_id(TExpr,ID),
    remove_prime_id_atom(ID,ID2),
    is_primed_id_atom(ID2).

list_renamings_to_primed_vars([],[]).

list_renamings_to_primed_vars([Var|Vars],[rename(VarId,PrimedId)|T]) :-
    get_texpr_id(Var,VarId),
    prime_id_atom(VarId,PrimedId),
    list_renamings_to_primed_vars(Vars,T).

prime_bexpr_for_ids(TExpr,ChangedIds,PrimedTExpr,ChangesPerformed) :-
    sort(ChangedIds,SortedCIds),
    transform_bexpr_with_scoping(before_after_predicates:prime_changed_id(SortedCIds,Changed),TExpr,PrimedTExpr),
    (var(Changed) -> ChangesPerformed=false ; ChangesPerformed=true).

prime_changed_id(ChangedIds,Changed,b(identifier(ID),Type,Info),Result,LocalIds) :-
    ord_member(ID,ChangedIds),
    ord_nonmember(ID,LocalIds), % The ID is not overriden by a locally quantified variable
    prime_id(ID,PrimedID),
    Changed=true, % change was performed
    Result = b(identifier(PrimedID),Type,Info).

prime_identifiers(TExprs,Primed) :-
    maplist(prime_typed_identifier,TExprs,Primed).

primed_var_is_used(UsedIdentifiers,Identifier) :-
    prime_typed_identifier(Identifier,PrimedIdentifier),
    remove_infos_and_norm(PrimedIdentifier,PrimedIdentifierWithoutInfos),
    member(PrimedIdentifierWithoutInfos,UsedIdentifiers).

remove_infos_and_norm(b(E,Type,_),b(E,NType,_)) :- normalize_type(Type,NType).

tcltk_before_after_predicate_for_operation(OpName,list(Res)) :-
    before_after_predicate_for_operation(OpName,BAPredicate),
    %translate:print_bexpr(BAPredicate),nl,
    conjunction_to_list(BAPredicate,LP),
    maplist(translate_bexpression,LP,Res).