| 1 | % (c) 2014-2025 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, | |
| 2 | % Heinrich Heine Universitaet Duesseldorf | |
| 3 | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) | |
| 4 | ||
| 5 | :- module(before_after_predicates, [tcltk_before_after_predicate_for_operation/2, | |
| 6 | before_after_predicate_for_operation/2, | |
| 7 | before_after_predicate_for_operation_no_equalities/5, | |
| 8 | before_after_predicate_with_equalities/3, | |
| 9 | before_after_predicate_list_conjunct_with_equalities/3, | |
| 10 | before_after_predicate_list_disjunct_with_equalities/3, | |
| 11 | before_after_predicate_no_equalities/3, | |
| 12 | add_missing_equalities/3, | |
| 13 | prime_bexpr_for_ids/4, prime_dollar0_bexpr_for_ids/3, | |
| 14 | list_renamings_to_primed_vars/2]). | |
| 15 | ||
| 16 | :- use_module(probsrc(module_information),[module_info/2]). | |
| 17 | :- module_info(group,cbc). | |
| 18 | :- module_info(description,'This module computes before-after-predicates of B and Event-B actions.'). | |
| 19 | % NOTE: for the moment it assumes no clashes between operation parameters and variables, constants, ... | |
| 20 | ||
| 21 | :- use_module(library(lists)). | |
| 22 | ||
| 23 | :- use_module(probsrc(bsyntaxtree), [get_texpr_expr/2, | |
| 24 | get_texpr_id/2, | |
| 25 | is_truth/1, | |
| 26 | safe_create_texpr/3, | |
| 27 | get_texpr_type/2, | |
| 28 | conjunct_predicates/2, | |
| 29 | conjunction_to_list/2, | |
| 30 | create_implication/3, | |
| 31 | create_couple/3, | |
| 32 | disjunct_predicates/2, | |
| 33 | find_typed_identifier_uses/2, | |
| 34 | rename_bt/3, | |
| 35 | create_exists/3, create_or_merge_exists/3, | |
| 36 | create_negation/2]). | |
| 37 | :- use_module(probsrc(error_manager), [add_error_fail/3]). | |
| 38 | :- use_module(probsrc(bmachine),[b_get_machine_operation/4, | |
| 39 | b_get_machine_variables/1, | |
| 40 | b_get_machine_constants/1]). | |
| 41 | %:- use_module(probsrc(specfile,[animation_minor_mode/1]). | |
| 42 | :- use_module(probsrc(tools),[split_list/4]). | |
| 43 | :- use_module(probsrc(translate),[translate_bexpression/2]). | |
| 44 | :- use_module(symbolic_model_checker(predicate_handling), | |
| 45 | [prime_id_atom/2, remove_prime_id_atom/2, is_primed_id_atom/1, | |
| 46 | prime_typed_identifier/2,remove_prime_typed_identifier/2, | |
| 47 | is_primed_typed_identifier/1]). | |
| 48 | ||
| 49 | ||
| 50 | tcltk_before_after_predicate_for_operation(OpName,list(Res)) :- | |
| 51 | before_after_predicate_for_operation(OpName,BAPredicate), | |
| 52 | %translate:print_bexpr(BAPredicate),nl, | |
| 53 | conjunction_to_list(BAPredicate,LP), | |
| 54 | maplist(translate_bexpression,LP,Res). | |
| 55 | ||
| 56 | before_after_predicate_for_operation(OpName,BAPredicate) :- | |
| 57 | b_get_machine_operation(OpName,_Results,_Parameters,OpBody), | |
| 58 | %print(op(OpName)),nl, | |
| 59 | b_get_machine_variables(Variables), | |
| 60 | %b_get_machine_constants(Constants), append(Variables,Constants,VarsAndConsts), | |
| 61 | before_after_predicate_with_equalities(OpBody,Variables,BAPredicate). | |
| 62 | ||
| 63 | % ---------------- | |
| 64 | ||
| 65 | :- use_module(probsrc(translate), [generate_typing_predicates/2]). | |
| 66 | ||
| 67 | % without equalities for UNCHANGED vars | |
| 68 | before_after_predicate_for_operation_no_equalities(OpName,Parameters,Results,BAPredicate,ChangedIds) :- | |
| 69 | b_get_machine_operation(OpName,Results,Parameters,OpBody), | |
| 70 | % TO DO: rename parameters if clashing | |
| 71 | generate_typing_predicates(Parameters,Typings1), | |
| 72 | generate_typing_predicates(Results,Typings2), | |
| 73 | before_after_predicate_no_equalities_tl4(top_level,OpBody,BAPred,ChangedIds), | |
| 74 | append([Typings1,Typings2,[BAPred]],LP), | |
| 75 | conjunct_predicates(LP,BAPredicate). | |
| 76 | % predicate contains new open identifiers: Results and Parameters | |
| 77 | ||
| 78 | % :- before_after_predicates:before_after_predicate_for_operation_no_equalities(Op,_,_,P,C), format('Op ~w (writing ~w):~n',[Op,C]), translate:print_bexpr(P),nl,nl,fail. | |
| 79 | ||
| 80 | ||
| 81 | ||
| 82 | :- use_module(probsrc(bsyntaxtree),[transform_bexpr_with_scoping/3]). | |
| 83 | % prime those variables inside a formula which are in the ChangedIds list | |
| 84 | prime_bexpr_for_ids(TExpr,ChangedIds,PrimedTExpr,ChangesPerformed) :- | |
| 85 | prime_bexpr_for_ids(TExpr,prime_with_quote,ChangedIds,PrimedTExpr,ChangesPerformed). | |
| 86 | prime_dollar0_bexpr_for_ids(TExpr,ChangedIds,PrimedTExpr) :- | |
| 87 | prime_bexpr_for_ids(TExpr,prime_with_dollar0,ChangedIds,PrimedTExpr,_ChangesPerformed). | |
| 88 | ||
| 89 | prime_bexpr_for_ids(TExpr,Kind,ChangedIds,PrimedTExpr,ChangesPerformed) :- | |
| 90 | sort(ChangedIds,SortedCIds), | |
| 91 | transform_bexpr_with_scoping(before_after_predicates:prime_changed_id(Kind,SortedCIds,Changed),TExpr,PrimedTExpr), | |
| 92 | (var(Changed) -> ChangesPerformed=false ; ChangesPerformed=true). | |
| 93 | ||
| 94 | :- use_module(library(ordsets),[ord_member/2,ord_nonmember/2]). | |
| 95 | prime_changed_id(Kind,ChangedIds,Changed,b(identifier(ID),Type,Info),Result,LocalIds) :- | |
| 96 | ord_member(ID,ChangedIds), | |
| 97 | ord_nonmember(ID,LocalIds), % The ID is not overriden by a locally quantified variable | |
| 98 | my_prime_id(Kind,ID,PrimedID), | |
| 99 | Changed=true, % change was performed | |
| 100 | Result = b(identifier(PrimedID),Type,Info). | |
| 101 | ||
| 102 | ||
| 103 | :- use_module(probsrc(btypechecker),[prime_id/2, prime_atom0/2]). | |
| 104 | my_prime_id(prime_with_dollar0,ID,PrimedID0) :- !, prime_atom0(ID,PrimedID0). % x -> x$0 | |
| 105 | my_prime_id(_,ID,PrimedID) :- !, prime_id(ID,PrimedID). % prime_with_quote: x -> x' | |
| 106 | ||
| 107 | ||
| 108 | % ---------------- | |
| 109 | ||
| 110 | %! before_after_predicate_with_equalities(+Action,+AllIdentifiers,-Predicate) | |
| 111 | % these add missing y' = y equalities for unchanged variables | |
| 112 | before_after_predicate_with_equalities(Action,AllIdentifiers,Predicate) :- | |
| 113 | before_after_predicate_list_conjunct_with_equalities([Action],AllIdentifiers,Predicate). | |
| 114 | before_after_predicate_list_conjunct_with_equalities(Actions,AllIdentifiers,BAPredicateWithEq) :- | |
| 115 | maplist(before_after_predicate_no_equalities_tl3(top_level),Actions,AllPredicates), | |
| 116 | conjunct_predicates(AllPredicates,BAPredicate), | |
| 117 | add_missing_equalities(AllIdentifiers,BAPredicate,BAPredicateWithEq). | |
| 118 | before_after_predicate_list_disjunct_with_equalities(Actions,AllIdentifiers,BAPredicate) :- | |
| 119 | maplist(before_after_predicate_no_equalities_tl3(top_level),Actions,AllPredicates), | |
| 120 | maplist(add_missing_equalities(AllIdentifiers),AllPredicates,BAPredicates), | |
| 121 | disjunct_predicates(BAPredicates,BAPredicate). | |
| 122 | ||
| 123 | % ---------------- | |
| 124 | ||
| 125 | % does not add missing y' = y equalities for unchanged variables | |
| 126 | % top-level version: has a special rule for PRE | |
| 127 | before_after_predicate_no_equalities_tl3(TopLevel,Action,Predicate) :- | |
| 128 | before_after_predicate_no_equalities_tl4(TopLevel,Action,Predicate,_). | |
| 129 | before_after_predicate_no_equalities_tl4(TopLevel,Action,Predicate,ChangedIDs) :- | |
| 130 | get_texpr_expr(Action,Expr), | |
| 131 | before_after_predicate_no_equalities_top_level_aux(Expr,Predicate,ChangedIDs,TopLevel). | |
| 132 | ||
| 133 | :- use_module(probsrc(preferences),[get_preference/2]). | |
| 134 | before_after_predicate_no_equalities_top_level_aux(precondition(Pre,Body),Predicate,ChangedIDs,top_level) :- | |
| 135 | get_preference(treat_outermost_pre_as_select,true), | |
| 136 | !, | |
| 137 | before_after_predicate_no_equalities(Body,BABody,ChangedIDs), | |
| 138 | conjunct_predicates([Pre,BABody],Predicate). % May sometimes have to be an implication (depending on how BA-predicate is used) ! | |
| 139 | before_after_predicate_no_equalities_top_level_aux(Expr,Pred,ChangedIDs,_) :- | |
| 140 | before_after_predicate_no_equalities_aux(Expr,Pred,ChangedIDs). | |
| 141 | ||
| 142 | % ---------------- | |
| 143 | ||
| 144 | % does not add missing y' = y equalities for unchanged variables | |
| 145 | before_after_predicate_no_equalities(Action,Predicate,ChangedIDs) :- | |
| 146 | get_texpr_expr(Action,Expr), | |
| 147 | before_after_predicate_no_equalities_aux(Expr,Predicate,ChangedIDs). | |
| 148 | ||
| 149 | get_changed_id(b(function(FUN,_),_,_),ID) :- !, get_changed_id(FUN,ID). | |
| 150 | get_changed_id(ID,ID). | |
| 151 | ||
| 152 | % TO DO: return list of Predicates rather than single predicate; avoid conjunct_predicates and create flat conj at end | |
| 153 | before_after_predicate_no_equalities_aux(assign_single_id(Id,Pred),Predicate,ChangedIDs) :- !, | |
| 154 | before_after_predicate_no_equalities_aux(assign([Id],[Pred]),Predicate,ChangedIDs). | |
| 155 | before_after_predicate_no_equalities_aux(assign(Ids,Preds),Predicate,ChangedIds) :- !, | |
| 156 | maplist(get_changed_id,Ids,ChangedIds), | |
| 157 | maplist(ba_predicate_equal,Ids,Preds,Predicates), | |
| 158 | conjunct_predicates(Predicates,Predicate). | |
| 159 | before_after_predicate_no_equalities_aux(becomes_element_of(Ids,Set),Predicate,Ids) :- !, | |
| 160 | maplist(ba_predicate_member(Set),Ids,Predicates), | |
| 161 | % THIS IS WRONG: it asserts that each Id is an element of Set, but the tuple Ids is an element! | |
| 162 | conjunct_predicates(Predicates,Predicate). % should we generate Set /= {} => Predicate | |
| 163 | before_after_predicate_no_equalities_aux(becomes_such(Ids,Pred),Predicate,Ids) :- !, | |
| 164 | ba_predicate_becomes_such(Ids,Pred,Predicate). | |
| 165 | before_after_predicate_no_equalities_aux(choice(Choices),Predicate,ChangedIDs) :- !, | |
| 166 | maplist(before_after_predicate_no_equalities,Choices,BAChoices,Changes), | |
| 167 | append(Changes,ChangedIDs), | |
| 168 | maplist(add_missing_equalities(ChangedIDs),BAChoices,BAChoicesWithEqualities), | |
| 169 | disjunct_predicates(BAChoicesWithEqualities,Predicate). | |
| 170 | before_after_predicate_no_equalities_aux(precondition(Pre,Body),Predicate,ChangedIDs) :- !, | |
| 171 | before_after_predicate_no_equalities(Body,BABody,ChangedIDs), | |
| 172 | create_implication(Pre,BABody,Predicate). | |
| 173 | before_after_predicate_no_equalities_aux(witness_then(Pre,Body),Predicate,ChangedIDs) :- !, | |
| 174 | before_after_predicate_no_equalities_aux(assertion(Pre,Body),Predicate,ChangedIDs). % TODO: check if ok, or if we should use SELECT | |
| 175 | before_after_predicate_no_equalities_aux(assertion(Pre,Body),Predicate,ChangedIDs) :- | |
| 176 | !, | |
| 177 | before_after_predicate_no_equalities(Body,BABody,ChangedIDs), | |
| 178 | create_implication(Pre,BABody,Predicate1), | |
| 179 | create_negation(Pre,NotPre), | |
| 180 | add_missing_equalities(ChangedIDs,b(truth,pred,[]),NotPrePredicate), | |
| 181 | create_implication(NotPre,NotPrePredicate,Predicate2), | |
| 182 | conjunct_predicates([Predicate1,Predicate2],Predicate). | |
| 183 | before_after_predicate_no_equalities_aux(select_when(Pre,Body),Predicate,ChangedIDs) :- !, | |
| 184 | before_after_predicate_no_equalities(Body,BABody,ChangedIDs), | |
| 185 | conjunct_predicates([Pre,BABody],Predicate). | |
| 186 | before_after_predicate_no_equalities_aux(select(Whens),Predicate,ChangedIDs) :- !, | |
| 187 | maplist(before_after_predicate_no_equalities,Whens,WhensPredicates,Changes), | |
| 188 | append(Changes,ChangedIDs), | |
| 189 | maplist(add_missing_equalities(ChangedIDs),WhensPredicates,WhensPredicatesWithEqualities), | |
| 190 | disjunct_predicates(WhensPredicatesWithEqualities,Predicate). | |
| 191 | before_after_predicate_no_equalities_aux(select(Whens,Else),Predicate,ChangedIDs) :- !, | |
| 192 | maplist(before_after_predicate_no_equalities,Whens,WhensPredicates,Changes), | |
| 193 | maplist(add_missing_equalities(ChangedIDs),WhensPredicates,WhensPredicatesWithEqualities), | |
| 194 | maplist(get_select_conditions,Whens,SelectConditions), | |
| 195 | disjunct_predicates(SelectConditions,ElseTemp), | |
| 196 | create_negation(ElseTemp,ElseLHS), | |
| 197 | before_after_predicate_no_equalities(Else,ElseRHS,ElseChangedIDs), | |
| 198 | append([ElseChangedIDs|Changes],ChangedIDs), | |
| 199 | conjunct_predicates([ElseLHS,ElseRHS],ElsePred), | |
| 200 | add_missing_equalities(ChangedIDs,ElsePred,ElsePredWithEqualities), | |
| 201 | disjunct_predicates([ElsePredWithEqualities|WhensPredicatesWithEqualities],Predicate). | |
| 202 | % TODO: case, handle while | |
| 203 | before_after_predicate_no_equalities_aux(sequence(ListOfSteps),Predicate,ChangedIDs) :- !, | |
| 204 | ba_predicate_sequence(ListOfSteps,Predicate,ChangedIDs). | |
| 205 | before_after_predicate_no_equalities_aux(if(IfList),Predicate,ChangedIDs) :- !, | |
| 206 | ba_predicate_if(IfList,Predicate,ChangedIDs). | |
| 207 | before_after_predicate_no_equalities_aux(let(P,D,B),Predicate,ChangedIDs) :- !, | |
| 208 | before_after_predicate_no_equalities_aux(any(P,D,B),Predicate,ChangedIDs). % TO DO: create let_predicate | |
| 209 | before_after_predicate_no_equalities_aux(any(Parameters,PreCond,Body),Predicate,ChangedIDs) :- !, | |
| 210 | before_after_predicate_no_equalities(Body,BABody,ChangedIDs), | |
| 211 | conjunct_predicates([PreCond,BABody],Inner), | |
| 212 | create_or_merge_exists(Parameters,Inner,Predicate). | |
| 213 | before_after_predicate_no_equalities_aux(parallel(P),Predicate,ChangedIDs) :- !, | |
| 214 | maplist(before_after_predicate_no_equalities,P,Preds,Changes), | |
| 215 | append(Changes,ChangedIDs), | |
| 216 | conjunct_predicates(Preds,Predicate). | |
| 217 | before_after_predicate_no_equalities_aux(skip,Predicate,[]) :- !, | |
| 218 | Predicate = b(truth,pred,[]). | |
| 219 | before_after_predicate_no_equalities_aux(var(Parameters,Body),Predicate,ChangedIDs) :- !, | |
| 220 | before_after_predicate_no_equalities(Body,BABody,ChangedIDs), | |
| 221 | create_or_merge_exists(Parameters,BABody,Predicate). | |
| 222 | before_after_predicate_no_equalities_aux(rlevent(_Name,_Section,_Stat,_Parameters,Guards,_Thm,Actions,_VWit,_PWit,_Unmod,_AbsEvents),Predicate,ChangedIDs) :- !, | |
| 223 | maplist(before_after_predicate_no_equalities,Actions,BAActions,Changes), | |
| 224 | append(Changes,ChangedIDs), | |
| 225 | conjunct_predicates([Guards|BAActions],Predicate). % should probably be an implication? see precondition. | |
| 226 | before_after_predicate_no_equalities_aux(operation_call(OpId,[],[]),Predicate,ChangedIDs) :- !, | |
| 227 | get_texpr_id(OpId,op(OpName)), | |
| 228 | b_get_machine_operation(OpName,[],[],OpBody), | |
| 229 | before_after_predicate_no_equalities(OpBody,Predicate,ChangedIDs). | |
| 230 | before_after_predicate_no_equalities_aux(Expr,Predicate,ChangedIDs) :- | |
| 231 | add_error_fail(before_after_predicate,'before-after-predicate implementation missing: ',[Expr,Predicate,ChangedIDs]). | |
| 232 | ||
| 233 | get_select_conditions(b(select_when(Condition,_),_,_),Condition). | |
| 234 | ||
| 235 | ba_predicate_equal(LHS,RHS,Res) :- | |
| 236 | % LHS := RHS | |
| 237 | get_override(LHS,RHS,TPred), !, | |
| 238 | %nl,translate:print_bexpr(TPred),nl, | |
| 239 | Res=TPred. | |
| 240 | ||
| 241 | :- use_module(probsrc(error_manager),[add_internal_error/2]). | |
| 242 | % get override Term for f(X)(Y)... := RHS | |
| 243 | get_override(b(function(FUN,ARG),_Type,_Info),ExprSoFar,Res) :- !, % FUN(ARG) := RHS | |
| 244 | %print(fun(FUN)),nl, translate:print_bexpr(ExprSoFar),nl, | |
| 245 | get_texpr_type(FUN,FType), | |
| 246 | create_couple(ARG,ExprSoFar,Update), % ARG|-> ExprSoFar | |
| 247 | safe_create_texpr(set_extension([Update]),FType,UpdateSET), % {ARG|->ExprSoFar} | |
| 248 | construct_override(FUN,UpdateSET,Override), % FUN <+ {ARG |-> {...}} | |
| 249 | get_override(FUN,Override,Res). % Pass Override as new RHS in case FUN itself is a function application | |
| 250 | get_override(FUNID,OverrideExpr,TPred) :- | |
| 251 | get_texpr_id(FUNID,_ID), %print(base(ID)),nl, | |
| 252 | prime_typed_identifier(FUNID,FUNPrimeId), | |
| 253 | safe_create_texpr(equal(FUNPrimeId,OverrideExpr),pred,TPred). % FUN' = FUN <+ {ARG |-> RHS} | |
| 254 | get_override(FUNID,OverrideExpr,TPred) :- | |
| 255 | add_internal_error('Cannot compute override: ',get_override(FUNID,OverrideExpr,TPred)),fail. | |
| 256 | ||
| 257 | construct_override(FunID,Update,Override) :- | |
| 258 | get_texpr_type(Update,Type), | |
| 259 | Override = b(overwrite(FunID,Update),Type,[]). | |
| 260 | ||
| 261 | ba_predicate_member(Set,Id,TPred) :- | |
| 262 | % prime identifiers on the lhs | |
| 263 | prime_typed_identifier(Id,PrimedId), | |
| 264 | safe_create_texpr(member(PrimedId,Set),pred,TPred). | |
| 265 | ||
| 266 | ba_predicate_becomes_such(Ids,Pred,Predicate) :- | |
| 267 | list_renamings_to_primed_vars(Ids,RenamingList), | |
| 268 | rename_bt(Pred,RenamingList,Predicate). | |
| 269 | ||
| 270 | list_renamings_to_primed_vars([],[]). | |
| 271 | list_renamings_to_primed_vars([Var|Vars],[rename(VarId,PrimedId)|T]) :- | |
| 272 | get_texpr_id(Var,VarId), | |
| 273 | prime_id_atom(VarId,PrimedId), | |
| 274 | list_renamings_to_primed_vars(Vars,T). | |
| 275 | ||
| 276 | % add missing UNCHANGED equalities (x'=x for all variables that are unchanged) | |
| 277 | add_missing_equalities([],PredWithoutEqualities,Res) :- !, Res=PredWithoutEqualities. | |
| 278 | add_missing_equalities(AllVariables,PredWithoutEqualities,PredWithEqualities) :- | |
| 279 | find_typed_identifier_uses(PredWithoutEqualities,UsedIdentifiers), | |
| 280 | exclude(primed_var_is_used(UsedIdentifiers),AllVariables,VariablesNotOccuringPrimed), | |
| 281 | maplist(ba_predicate_equal,VariablesNotOccuringPrimed,VariablesNotOccuringPrimed,EqualityPredicates), | |
| 282 | conjunct_predicates([PredWithoutEqualities|EqualityPredicates],PredWithEqualities). | |
| 283 | ||
| 284 | :- use_module(probsrc(typing_tools),[normalize_type/2]). | |
| 285 | primed_var_is_used(UsedIdentifiers,Identifier) :- | |
| 286 | prime_typed_identifier(Identifier,PrimedIdentifier), | |
| 287 | remove_infos_and_norm(PrimedIdentifier,PrimedIdentifierWithoutInfos), | |
| 288 | member(PrimedIdentifierWithoutInfos,UsedIdentifiers). | |
| 289 | ||
| 290 | remove_infos_and_norm(b(E,Type,_),b(E,NType,_)) :- normalize_type(Type,NType). | |
| 291 | ||
| 292 | add_else_if_missing([],[DefaultElse]) :- | |
| 293 | safe_create_texpr(if_elsif(b(truth,pred,[]),b(skip,subst,[])),subst,DefaultElse). | |
| 294 | add_else_if_missing([If|Ifs],[If|Ifs]) :- | |
| 295 | get_texpr_expr(If,if_elsif(Test,_)), | |
| 296 | is_truth(Test), !. | |
| 297 | add_else_if_missing([If|Ifs],[If|MoreIfs]) :- | |
| 298 | add_else_if_missing(Ifs,MoreIfs). | |
| 299 | ||
| 300 | ba_predicate_if(IF,BA,AllChangedIDs) :- | |
| 301 | add_else_if_missing(IF,IFWithElse), | |
| 302 | maplist(ba_predicate_if_aux,IFWithElse,BAPreds,ChangedIDs), | |
| 303 | append(ChangedIDs,AllChangedIDs), | |
| 304 | ba_predicate_if(IFWithElse,BAPreds,AllChangedIDs,BA). | |
| 305 | ||
| 306 | ba_predicate_if([IF|IFs],[BAPred|BAPreds],IDs,BA) :- | |
| 307 | get_texpr_expr(IF,if_elsif(Test,_)), | |
| 308 | % if-part | |
| 309 | add_missing_equalities(IDs,BAPred,InnerBAPredIf), | |
| 310 | (is_truth(Test) | |
| 311 | -> InnerBAPredIf = BAPredIf | |
| 312 | ; safe_create_texpr(implication(Test,InnerBAPredIf),pred,BAPredIf)), | |
| 313 | % if there are further else/elseif parts, create pos | |
| 314 | (ba_predicate_if(IFs,BAPreds,IDs,ElsePred) | |
| 315 | -> create_negation(Test,NegTest), | |
| 316 | safe_create_texpr(implication(NegTest,ElsePred),pred,BAPredElse), | |
| 317 | conjunct_predicates([BAPredIf,BAPredElse],BA) | |
| 318 | ; BA = BAPredIf). | |
| 319 | ||
| 320 | ba_predicate_if_aux(IF,BAPred,ChangedIDs) :- | |
| 321 | get_texpr_expr(IF,if_elsif(_,Body)), | |
| 322 | before_after_predicate_no_equalities(Body,BAPred,ChangedIDs). | |
| 323 | ||
| 324 | ba_predicate_sequence([Last],Predicate,ChangedIDs) :- !, | |
| 325 | before_after_predicate_no_equalities(Last,Predicate,ChangedIDs). | |
| 326 | ba_predicate_sequence([First|SomeMore],Predicate,ChangedIDs) :- | |
| 327 | before_after_predicate_no_equalities(First,FirstPred,ChangesFirst), | |
| 328 | find_typed_identifier_uses(FirstPred,TypedIdsOfFirst), | |
| 329 | % get primed typed identifiers | |
| 330 | include(is_primed_typed_identifier,TypedIdsOfFirst,PrimedTypedIdsOfFirst), | |
| 331 | % rename them if they are already used in SomeMore | |
| 332 | ba_predicate_sequence(SomeMore,SecondPred,FurtherChanges), | |
| 333 | maplist(find_free_id_by_priming(SecondPred),PrimedTypedIdsOfFirst,UnusedPrimedTypedIds), | |
| 334 | maplist(create_id_renaming,PrimedTypedIdsOfFirst,UnusedPrimedTypedIds,RenamingOfFirst), | |
| 335 | rename_bt(FirstPred,RenamingOfFirst,FirstPredAfterReplacement), | |
| 336 | % rename unprimed ids in SecondPred, which are written by FirstPred | |
| 337 | maplist(remove_prime_typed_identifier,PrimedTypedIdsOfFirst,UnprimedTypedIds), | |
| 338 | maplist(create_id_renaming,UnprimedTypedIds,UnusedPrimedTypedIds,RenamingOfSecond), | |
| 339 | rename_bt(SecondPred,RenamingOfSecond,SecondPredAfterReplacement), | |
| 340 | ||
| 341 | conjunct_predicates([FirstPredAfterReplacement,SecondPredAfterReplacement],FullPred), | |
| 342 | % create exists for typed identifiers, which are primed more than once | |
| 343 | include(is_primed_more_than_once,UnusedPrimedTypedIds,TwoOrMorePrimedTypedIds), | |
| 344 | conjunction_to_list(FullPred,FullPredList), | |
| 345 | split_list(contains_some_typed_id(TwoOrMorePrimedTypedIds),FullPredList,ExistsPredList,RemainingPredList), | |
| 346 | conjunct_predicates(ExistsPredList,ExistsPred), | |
| 347 | create_exists(TwoOrMorePrimedTypedIds,ExistsPred,Exists), | |
| 348 | conjunct_predicates([Exists|RemainingPredList],Predicate), | |
| 349 | append(ChangesFirst,FurtherChanges,ChangedIDs). | |
| 350 | ||
| 351 | ||
| 352 | find_free_id_by_priming(Pred,TypedId,FreePrimedTypedId) :- | |
| 353 | find_typed_identifier_uses(Pred,TypedIds), | |
| 354 | (member(TypedId,TypedIds) -> | |
| 355 | prime_typed_identifier(TypedId,PrimedTypedId), | |
| 356 | find_free_id_by_priming(Pred,PrimedTypedId,FreePrimedTypedId) | |
| 357 | ; FreePrimedTypedId = TypedId). | |
| 358 | ||
| 359 | contains_some_typed_id(TypedIds,Pred) :- | |
| 360 | some(contains_typed_id(Pred),TypedIds). | |
| 361 | ||
| 362 | contains_typed_id(Pred,TypedId) :- | |
| 363 | find_typed_identifier_uses(Pred,TypedIds), | |
| 364 | member(TypedId,TypedIds). | |
| 365 | ||
| 366 | prime_identifiers(TExprs,Primed) :- | |
| 367 | maplist(prime_typed_identifier,TExprs,Primed). | |
| 368 | ||
| 369 | is_primed_more_than_once(TExpr) :- | |
| 370 | get_texpr_id(TExpr,ID), | |
| 371 | remove_prime_id_atom(ID,ID2), | |
| 372 | is_primed_id_atom(ID2). | |
| 373 | ||
| 374 | create_id_renaming(Var,RenamedVar,rename(Id,RenamedId)) :- | |
| 375 | get_texpr_id(Var,Id), | |
| 376 | get_texpr_id(RenamedVar,RenamedId). | |
| 377 | ||
| 378 |