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 |