weakest_preconditions

choice_wps([],_Pred,[]).

choice_wps([Choice|Choices],Pred,[ChoiceWP|WPs]) :-
    weakest_precondition(Choice,Pred,ChoiceWP),
    choice_wps(Choices,Pred,WPs).

create_member(Set,ID,Res) :-
    safe_create_texpr(member(ID,Set),pred,Res).

create_members(Set,IDs,MemberOf) :-
    maplist(create_member(Set),IDs,Preds),
    conjunct_predicates(Preds,MemberOf).

delete_reference_machine :-
    retractall(machine(_)).

empty_any_statement(any([],_Precond,b(parallel([]),subst,_))).

empty_assign_statement(assign([],[])).

function_assignment_to_overwrite([],[],[],[]).

function_assignment_to_overwrite([b(identifier(ID),Type,Infos)|IdOrFuns],[Expr|Exprs],[b(identifier(ID),Type,Infos)|IdOuts],[Expr|ExprOuts]) :-
    function_assignment_to_overwrite(IdOrFuns,Exprs,IdOuts,ExprOuts).

function_assignment_to_overwrite([b(function(Function,Argument),_Type,_Infos)|IdOrFuns],[Expr|Exprs],[Function|IdOuts],[ExprOut|ExprOuts]) :-
    get_texpr_type(Argument,ArgumentType), get_texpr_type(Expr,ExprType),
    get_texpr_type(Function,FunctionType),
    CoupleType = couple(ArgumentType,ExprType),
    safe_create_texpr(couple(Argument,Expr),CoupleType,OverwriteCouple),
    safe_create_texpr(set_extension([OverwriteCouple]),set(CoupleType),CoupleInSet),
    safe_create_texpr(overwrite(Function,CoupleInSet),FunctionType,ExprOut),
    function_assignment_to_overwrite(IdOrFuns,Exprs,IdOuts,ExprOuts).

get_non_represented_vars([],_PrimedVars,[]).

get_non_represented_vars([Var|Vars],PrimedVars,NonRepresented) :-
    prime_identifier(Var,VarPrimed),
    remove_all_infos(VarPrimed,VarPrimedNoInfos),
    (member(VarPrimedNoInfos,PrimedVars) ->
    NonRepresented = NonRepresented1
    ;
    NonRepresented = [Var|NonRepresented1]
    ),
    get_non_represented_vars(Vars,PrimedVars,NonRepresented1).

get_primed_ids([],[]).

get_primed_ids([ID|IDs],[ID|Rest]) :-
    get_texpr_id(ID,I),
    is_primed_id(I),!,
    get_primed_ids(IDs,Rest).

get_primed_ids([_ID|IDs],Rest) :-
    get_primed_ids(IDs,Rest).

if_wp([IF|IFs],Pred,WP) :-
    get_texpr_expr(IF,if_elsif(Test,Body)),
    % if-part
    weakest_precondition(Body,Pred,InnerWP),
    safe_create_texpr(implication(Test,InnerWP),pred,IfWP),
    % if there are further else/elseif parts, create pos
    (if_wp(IFs,Pred,SubWP)
    -> create_negation(Test,NegTest),
    safe_create_texpr(implication(NegTest,SubWP),pred,ElseWP),
    conjunct_predicates([IfWP,ElseWP],WP)
    ; WP = IfWP).

lookup_operation(Name,Results,Parameters,Body) :-
    ground(Name), % only for lookup of operations
    get_texpr_id(Name,op(OperationName)),
    (machine(M)
    -> get_section(operation_bodies,M,Ops),
    get_texpr_expr(Op,operation(TId,Results,Parameters,Body)),
    get_texpr_id(TId,op(Name)),
    member(Op,Ops)
    ; b_get_machine_operation(OperationName,Results,Parameters,Body)).

merge_assigns_and_anys(Assign,Any,Result) :-
    (empty_any_statement(Any),empty_assign_statement(Assign) ->
    add_error_fail(merge_assigns_and_anys,'merging of parallel executions failed (empty assignment and any statements): ', (Assign,Any))
    ; empty_any_statement(Any) ->
    Result = Assign
    ; empty_assign_statement(Assign) ->
    Result = Any
    ;
    Any = any(Par,PreCond,Body),
    get_texpr_expr(Body,parallel(Actions)),
    create_texpr(Assign,subst,[],BAssign),
    create_texpr(parallel([BAssign|Actions]),subst,[],NewBody),
    Result = any(Par,PreCond,NewBody)
).

merge_parallels(ParallelAssigns,Result) :-
    create_texpr(truth,pred,[],True),
    create_texpr(parallel([]),subst,[],Body),
    EmptyAny = any([],True,Body),
    EmptyAssign = assign([],[]),
    merge_parallels1(ParallelAssigns,EmptyAssign,EmptyAny,Assigns,Anys,Rest),
    (Rest == [] ->
    merge_assigns_and_anys(Assigns,Anys,Res),
    create_texpr(Res,subst,[],Result),
    (debug_mode(on) -> print_subst(Result),nl; true)
    ;
    add_error_fail(merge_parallels, 'merging of parallel executions failed (implementation missing?):', Rest)
).

merge_parallels1([],Assigns,Anys,Assigns,Anys,[]).

merge_parallels1([Subst|Substs],assign(IDs2,Exprs2),any(Par2,PreCond2,Body2),ResAssigns,ResAnys,Rest) :-
    get_texpr_expr(Subst,Expr),
    merge_parallels_normalize(Expr,ExprN),
    (ExprN = assign(IDs1,Exprs1) ->
    append(IDs2,IDs1,IDs3),
    append(Exprs2,Exprs1,Exprs3),
    NewAssign = assign(IDs3,Exprs3),
    NewAny = any(Par2,PreCond2,Body2),
    Rest = Rest1
    ; ExprN = any(Par1,PreCond1,Body1) ->
    append(Par2,Par1,Par3),
    conjunct_predicates([PreCond2,PreCond1],PreCond3),
    get_texpr_expr(Body2,parallel(AnySubsts2)),
    create_texpr(parallel([Body1|AnySubsts2]),subst,[],Body3),
    NewAny = any(Par3,PreCond3,Body3),
    NewAssign = assign(IDs2,Exprs2),
    Rest = Rest1
    ; ExprN = skip ->
    NewAssign = assign(IDs2,Exprs2),
    NewAny = any(Par2,PreCond2,Body2),
    Rest = Rest1
    ;
    NewAssign = assign(IDs2,Exprs2),
    NewAny = any(Par2,PreCond2,Body2),
    Rest = [Subst|Rest1]
    ), !, % do not backtrack once the a substitution is merged to the assignment or any generator
    merge_parallels1(Substs,NewAssign,NewAny,ResAssigns,ResAnys,Rest1).

merge_parallels_normalize(assign_single_id(ID,Expr),assign([ID],[Expr])) :- !.

merge_parallels_normalize(becomes_element_of(IDs,Set), any(Parameters,PreCond,Body)) :- !,
    prime_identifiers(IDs,Parameters), create_members(Set,Parameters,PreCond),
    create_texpr(assign(IDs,Parameters),subst,[],Body).

merge_parallels_normalize(becomes_such(Vars,Condition),any(PrimedIDs,Condition,Body)) :- !,
    find_typed_identifier_uses(Condition,UsedIDs),
    get_primed_ids(UsedIDs,PrimedIDs), % TO DO: check if we can reuse find_read_vars_for_becomes_such in b_read_write_info.pl
    get_non_represented_vars(Vars,PrimedIDs,NonRepresented),
    (NonRepresented\=[] ->
    get_texpr_ids(NonRepresented,VarsIDs),
    create_texpr(becomes_such(Vars,Condition),subst,[],TExpr),
    translate_substitution(TExpr,Subst),
    add_error_fail(merge_parallels_normalize,'Normalising becomes_such(...) costruct failed because the following variables were not reprsented by prime variables: ', (VarsIDs,Subst))
    ;
    create_texpr(assign(Vars,PrimedIDs),subst,[],Body)
).

merge_parallels_normalize(X,X).

select_whens_wps([],_Pred,[]).

select_whens_wps([When|Whens],Pred,[WP|WPs]) :-
    get_texpr_expr(When,select_when(PreCond, Body)),
    weakest_precondition(Body,Pred,InnerWP),
    safe_create_texpr(implication(PreCond,InnerWP),pred,WP),
    select_whens_wps(Whens,Pred,WPs).

sequence_wp(Actions,Pred,WP) :-
    reverse(Actions,ReversedActions),
    sequence_wp2(ReversedActions,Pred,WP).

sequence_wp2([],Pred,Pred).

sequence_wp2([Action|Actions],PredIn,PredOut) :-
    weakest_precondition(Action,PredIn,PredT),
    sequence_wp2(Actions,PredT,PredOut).

set_reference_machine(M) :-
    delete_reference_machine,
    assert_once(machine(M)).

weakest_precondition(Action,Pred,WP) :-
    get_texpr_expr(Action,Expr),
    weakest_precondition2(Expr,Pred,WP).

weakest_precondition2(any(Parameters,PreCond,Body),Pred,WP) :- !,
    weakest_precondition(Body,Pred,InnerWP),
    safe_create_texpr(implication(PreCond,InnerWP),pred,UnquantifiedWP),
    create_forall(Parameters,UnquantifiedWP,WP).

weakest_precondition2(assign(TIds,Exprs),Pred,WP) :- !,
    function_assignment_to_overwrite(TIds,Exprs,TIds2,Exprs2),
    get_texpr_ids(TIds2,StrippedIDs),
    replace_ids_by_exprs(Pred,StrippedIDs,Exprs2,WP).

weakest_precondition2(assign_single_id(TId,Expr),Pred,WP) :- !,
    function_assignment_to_overwrite([TId],[Expr],[TId2],[Expr2]),
    get_texpr_id(TId2,Id),
    replace_id_by_expr(Pred,Id,Expr2,WP).

weakest_precondition2(becomes_element_of(IDs,Set),Pred,WP) :- !,
    create_members(Set,IDs,MemberOf),
    safe_create_texpr(implication(MemberOf,Pred),pred,InnerWP),
    create_forall(IDs,InnerWP,WP).

weakest_precondition2(choice(Choices),Pred,WP) :- !,
    choice_wps(Choices,Pred,WPs),
    conjunct_predicates(WPs,WP).

weakest_precondition2(if(IfList),Pred,WP) :- !,
    if_wp(IfList,Pred,WP).

weakest_precondition2(let(Parameters,Defs,Body),Pred,WP) :- !,
    weakest_precondition(Body,Pred,InnerWP),
    safe_create_texpr(implication(Defs,InnerWP),pred,UnquantifiedWP),
    create_forall(Parameters,UnquantifiedWP,WP).

weakest_precondition2(operation_call(Operation,ResultsCall,ParametersCall),Pred,WP) :- !,
    lookup_operation(Operation,ResultsOperation,ParametersOperation,Body),
    % replace parameter/results identifiers
    append([ResultsOperation,ParametersOperation],IDs), append([ResultsCall,ParametersCall],Replacements),
    get_texpr_ids(IDs,StrippedIDs),
    replace_ids_by_exprs(Body,StrippedIDs,Replacements,NewBody),
    weakest_precondition(NewBody,Pred,WP).

weakest_precondition2(parallel(Actions),Pred,WP) :- !,
    merge_parallels(Actions,Action),
    weakest_precondition(Action,Pred,WP).

weakest_precondition2(precondition(Condition,Action),Pred,WP) :- !,
    weakest_precondition(Action,Pred,InnerWP),
    conjunct_predicates([Condition,InnerWP],WP).

weakest_precondition2(rlevent(_Name,_Section,_Stat,Parameters,Guard,_Thm,Act,_VWit,_PWit,_Unmod,_AbsEvents),Pred,WP) :- !,
    (is_list(Act)
    -> create_texpr(parallel(Act),subst,[],NewAct)
    ; NewAct=Act
    ),
    weakest_precondition2(any(Parameters,Guard,NewAct),Pred,WP).

weakest_precondition2(select(Whens),Pred,WP) :- !,
    select_whens_wps(Whens,Pred,WPs),
    conjunct_predicates(WPs,WP).

weakest_precondition2(select(Whens,Else),Pred,WP) :- !,
    select_whens_wps(Whens,Pred,WPs),
    conjunct_predicates(WPs,WhensWP),
    % collect all guards and negate them
    % => precondition for else-case
    findall(PC,(member(SW,Whens),get_texpr_expr(SW,select_when(PC,_))), AllPreconds),
    maplist(create_negation,AllPreconds,NegAllPreconds),
    conjunct_predicates(NegAllPreconds,ElsePrecond),
    % imply [T_n]S
    weakest_precondition(Else,Pred,InnerWP),
    safe_create_texpr(implication(ElsePrecond,InnerWP),pred,ElseWP),
    conjunct_predicates([WhensWP,ElseWP],WP).

weakest_precondition2(sequence(Actions),Pred,WP) :- !,
    sequence_wp(Actions,Pred,WP).

weakest_precondition2(skip,Pred,WP) :- !,WP=Pred.

weakest_precondition2(var(IDs,Subst),Pred,WP) :- !,
    weakest_precondition(Subst,Pred,InnerWP),
    create_forall(IDs,InnerWP,WP).

weakest_precondition2(while(P,S,I,V),R,WP) :- !,
    % [while P DO S INVARIANT I VARIANT V END] R
    % see abrial, b-book, p. 395:
    % there are five predicates. their conjunction is equal to the weakest precondition
    % first, create the list of all variables modified by the Stmt (used in forall)
    find_typed_identifier_uses(S,AllIdentifiersInStmt),
    get_accessed_vars(S,[],ModifiedVarsInStmt,_Reads),
    % the identifiers in ModifiedVarsInStmt are not typed. fetch the types from the list of all identifiers
    % TypedModifiedVarsInStmt = X
    get_texpr_ids(TypedModifiedVarsInStmt,ModifiedVarsInStmt),
    subset(TypedModifiedVarsInStmt,AllIdentifiersInStmt),
   
    ForAlls = TypedModifiedVarsInStmt,
   
    % first obligation: the invariant
    WP1 = I,
   
    % second obligation: forall x in X: (I & P => [S]I)
    conjunct_predicates([I,P],LHS2),
    weakest_precondition(S,I,RHS2),
    safe_create_texpr(implication(LHS2,RHS2),pred,Inner2),
    create_forall(ForAlls,Inner2,WP2),
   
    % third obligation: forall x in X: (I => v in N)
    safe_create_texpr(member(V,b(integer_set('NATURAL'),set(integer),[])),pred,RHS3),
    safe_create_texpr(implication(I,RHS3),pred,Inner3),
    create_forall(ForAlls,Inner3,WP3),
   
    % fourth obligation: forall x in X: I & P => [gamma:=V][S](V
    create_texpr(identifier('gamma\''),integer,[],Gamma),
    create_texpr(assign_single_id(Gamma,V),subst,[],AssignVariantToGamma),
    safe_create_texpr(less(V,Gamma),pred,VLessGamma),
    weakest_precondition(S,VLessGamma,RHS4T),
    weakest_precondition(AssignVariantToGamma,RHS4T,RHS4),
    LHS4 = LHS2,
    safe_create_texpr(implication(LHS4,RHS4),pred,Inner4),
    create_forall(ForAlls,Inner4,WP4),
   
    % fifth obligation: forall x in X: (I & not P) => R
    create_negation(P,NotP), conjunct_predicates([I,NotP],LHS5),
    safe_create_texpr(implication(LHS5,R),pred,Inner5),
    create_forall(ForAlls,Inner5,WP5),
   
    % conjunct them all together
    conjunct_predicates([WP1,WP2,WP3,WP4,WP5],WP).

weakest_precondition2(Action,Pred,_WeakestPrecondition) :- !,
    get_texpr_expr(Action,ActionExpr),
    add_error_fail(weakest_precondition,'weakest-precondition implementation missing: ',[ActionExpr,Pred]).