1		% (c) 2009-2022 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(subexpressions,[%zsubexpressions/2,
6		zexpr_conversion/4,
7		znamespace/7,
8		znamespace/4,
9		zsubexpressionst/2,
10		zexpr_conversiont/4,
11		znamespacet/7,
12		znamespacet/4,
13		equal_expression/2,
14		clean_where/2,
15		equal_expressiont/2,
16		clean_wheret/2,
17		/* check_z_structure/1,
18		check_z_structuret/1, */
19		rename_variablest/3,
20		exists_equalt/2]).
21
22		:- use_module(library(lists)).
23		:- use_module(library(terms)).
24
25		:- use_module(probsrc(tools)).
26		:- use_module(probsrc(self_check)).
27
28		:- use_module(z_tools).
29
30		:- use_module(probsrc(module_information)).
31		:- module_info(group,proz).
32		:- module_info(description,'This module contains predicates to decompose and operate on Z expressions').
33
34		% not used :
35		%zsubexpressions(Expr,Subexpressions) :-
36		% zexpr_conversion(Expr,Subexpressions,_,_).
37
38		zexpr_conversion(ref(N,P),[],[],ref(N,P)).
39		zexpr_conversion(number(N),[],[],number(N)).
40		zexpr_conversion(apply(F,A),[F,A],[F2,A2],apply(F2,A2)).
41		zexpr_conversion(inop(N,A,B),[A,B],[A2,B2],inop(N,A2,B2)).
42		zexpr_conversion(ingen(N,A,B),[A,B],[A2,B2],ingen(N,A2,B2)).
43		zexpr_conversion(postop(N,A),[A],[A2],postop(N,A2)).
44		zexpr_conversion(pregen(N,A),[A],[A2],pregen(N,A2)).
45		zexpr_conversion(inrel(N,A,B),[A,B],[A2,B2],inrel(N,A2,B2)).
46		zexpr_conversion(prerel(N,A),[A],[A2],prerel(N,A2)).
47		zexpr_conversion(equal(A,B),[A,B],[A2,B2],equal(A2,B2)).
48		zexpr_conversion(member(A,B),[A,B],[A2,B2],member(A2,B2)).
49		zexpr_conversion(power(A),[A],[A2],power(A2)).
50		zexpr_conversion(cross(A),[A],[A2],cross(A2)).
51		zexpr_conversion(tuple(A),[A],[A2],tuple(A2)).
52		zexpr_conversion(if(I,T,E),[I,T,E],[I2,T2,E2],if(I2,T2,E2)).
53		zexpr_conversion(ext(A),[A],[A2],ext(A2)).
54		zexpr_conversion(seq(A),[A],[A2],seq(A2)).
55		zexpr_conversion(bag(A),[A],[A2],bag(A2)).
56		zexpr_conversion(theta(N,D,R),[],[],theta(N,D,R)).
57		zexpr_conversion(sexpr(A),[A],[A2],sexpr(A2)).
58		zexpr_conversion(select(A,N),[A],[A2],select(A2,N)).
59		zexpr_conversion(lambda(A,B),[A,B],[A2,B2],lambda(A2,B2)).
60		zexpr_conversion(comp(A,B),[A,B],[A2,B2],comp(A2,B2)).
61		zexpr_conversion(reclet(A,B),[A,B],[A2,B2],reclet(A2,B2)).
62		zexpr_conversion(just(A),[A],[A2],just(A2)).
63		zexpr_conversion(nothing,[],[],nothing).
64		zexpr_conversion(mu(A,B),[A,B],[A2,B2],mu(A2,B2)).
65		zexpr_conversion(falsity,[],[],falsity).
66		zexpr_conversion(truth,[],[],truth).
67		zexpr_conversion(forall(A,B),[A,B],[A2,B2],forall(A2,B2)).
68		zexpr_conversion(exists(A,B),[A,B],[A2,B2],exists(A2,B2)).
69		zexpr_conversion(exists1(A,B),[A,B],[A2,B2],exists1(A2,B2)).
70		zexpr_conversion(and(A,B),[A,B],[A2,B2],and(A2,B2)).
71		zexpr_conversion(or(A,B),[A,B],[A2,B2],or(A2,B2)).
72		zexpr_conversion(implies(A,B),[A,B],[A2,B2],implies(A2,B2)).
73		zexpr_conversion(equiv(A,B),[A,B],[A2,B2],equiv(A2,B2)).
74		zexpr_conversion(not(A),[A],[A2],not(A2)).
75		zexpr_conversion(spred(S),[S],[S2],spred(S2)).
76		zexpr_conversion(letexpr(A,B),[A,B],[A2,B2],letexpr(A2,B2)).
77		zexpr_conversion(letpred(A,B),[A,B],[A2,B2],letpred(A2,B2)).
78		zexpr_conversion(letdef(N,A),[A],[A2],letdef(N,A2)).
79		zexpr_conversion(sref(N,D,P,R),[],[],sref(N,D,P,R)).
80		zexpr_conversion(sand(A,B),[A,B],[A2,B2],sand(A2,B2)).
81		zexpr_conversion(sor(A,B),[A,B],[A2,B2],sor(A2,B2)).
82		zexpr_conversion(simplies(A,B),[A,B],[A2,B2],simplies(A2,B2)).
83		zexpr_conversion(sequiv(A,B),[A,B],[A2,B2],sequiv(A2,B2)).
84		zexpr_conversion(snot(A),[A],[A2],snot(A2)).
85		zexpr_conversion(sforall(A,B),[A,B],[A2,B2],sforall(A2,B2)).
86		zexpr_conversion(sexists(A,B),[A,B],[A2,B2],sexists(A2,B2)).
87		zexpr_conversion(sexists1(A,B),[A,B],[A2,B2],sexists1(A2,B2)).
88		zexpr_conversion(hide(A,H),[A],[A2],hide(A2,H)).
89		zexpr_conversion(fatsemi(A,B),[A,B],[A2,B2],fatsemi(A2,B2)).
90		zexpr_conversion(project(A,B),[A,B],[A2,B2],project(A2,B2)).
91		zexpr_conversion(pre(A),[A],[A2],pre(A2)).
92		zexpr_conversion(pipe(A,B),[A,B],[A2,B2],pipe(A2,B2)).
93		zexpr_conversion(text(A),[A],[A2],text(A2)).
94
95		zexpr_conversion(sdef(N,D),[D],[D2],sdef(N,D2)).
96		zexpr_conversion(defeq(N,D),[D],[D2],defeq(N,D2)).
97		zexpr_conversion(eqeq(N,D),[D],[D2],eqeq(N,D2)).
98		zexpr_conversion(define(N,D),[D],[D2],define(N,D2)).
99		zexpr_conversion(axdef(D),[D],[D2],axdef(D2)).
100		zexpr_conversion(pred(P),[P],[P2],pred(P2)).
101		zexpr_conversion(given(Ns),[],[],given(Ns)).
102		zexpr_conversion(data(N,Arms),[Arms],[Arms2],data(N,Arms2)).
103		zexpr_conversion(arm(N,A),[A],[A2],arm(N,A2)).
104
105		zexpr_conversion(body(D,W),[D,W],[D2,W2],body(D2,W2)).
106		zexpr_conversion(decl(Ns,T),[T],[T2],decl(Ns,T2)).
107		zexpr_conversion(sdecl(S),[S],[S2],sdecl(S2)).
108
109		% internal constructs
110		zexpr_conversion(namedset(N,Ms),[],[],namedset(N,Ms)).
111		zexpr_conversion(binding(Fs),[Fs],[Fs2],binding(Fs2)).
112		zexpr_conversion(bindfield(N,E),[E],[E2],bindfield(N,E2)).
113
114		zexpr_conversion(basetype(T),[],[],basetype(T)).
115
116		zexpr_conversion(ftconstant(F,C),[],[],ftconstant(F,C)).
117		zexpr_conversion(ftconstructor(F,C,E),[E],[E2],ftconstructor(F,C,E2)).
118		zexpr_conversion(ftdestructor(F,C,E),[E],[E2],ftdestructor(F,C,E2)).
119		zexpr_conversion(ftcase(F,C,E),[E],[E2],ftcase(F,C,E2)).
120
121
122		% the same as znamespace/4 but with additional arguments:
123		% +NOuter: the list of new inner subexpressions
124		% +NInner: the list of new outer subexpressions
125		% -Result: the original expression with exchanged subexpressions
126		znamespace(Expr,Outer,Inner,Names,NOuter,NInner,Result) :-
127		has_body(Expr),!,
128		extract_body_structure(Expr,Outer,Inner,Names,Decls,Exprs,Where),
129
130		same_functor(Expr,Term),
131		zns_body(Term,body(XDecls,XWhere),XExprs),
132		anon_decls(Decls,XDecls,NOuter),
133		same_length(Where,XWhere),
134		same_length(Exprs,XExprs),
135		append(XWhere,XExprs,NInner),
136		Term = Result.
137		znamespace(Expr,Outer,Inner,Names,NOuter,NInner,Result) :-
138		extract_let_structure(Expr,Outer,Inner,Names,Defs),
139
140		same_functor(Expr,Term),
141		zns_let(Term,XDefs,XExpr),
142		anon_decls(Defs,XDefs,NOuter),
143		NInner = XExpr,
144		Result = Term.
145
146		% znamespace returns the subcomponents of an expression
147		% An expression might introduce new variables (like in forall,
148		% lexists, let, etc.
149		% znamespace(+Expr,-Outer,-Inner,-Names)
150		% Expr: the expressionto decompose
151		% Outer: the list of subexpression outside the newly introduced scope
152		% (e.g. in the declaration part of an universal quantification)
153		% Inner: the list of subexpression inside the newly introduced scope
154		% (e.g. the predicate of an universal quantification)
155		% Names: the list of newly introduced names
156		znamespace(Expr,Outer,Inner,Names) :-
157		has_body(Expr),!,
158		extract_body_structure(Expr,Outer,Inner,Names,_Decls,_Exprs,_Where).
159		znamespace(Expr,Outer,Inner,Names) :-
160		extract_let_structure(Expr,Outer,Inner,Names,_Defs).
161
162		has_body(Expr) :- zns_body(Expr,body(_,_),_),!.
163
164		extract_body_structure(Expr,Outer,Inner,Names,Decls,Exprs,Where) :-
165		zns_body(Expr,body(Decls,Where),Exprs),
166		append(Where,Exprs,Inner),
167		findall(Type,member(decl(_,Type),Decls),Outer),
168		findall(Vars,member(decl(Vars,_),Decls),VarLists),
169		append(VarLists,Names).
170
171		extract_let_structure(Expr,Outer,Inner,Names,Defs) :-
172		zns_let(Expr,Defs,Inner),
173		findall(Name,member(letdef(Name,_),Defs),Names),
174		findall(LExpr,member(letdef(_,LExpr),Defs),Outer).
175
176
177		zsubnamespace(Expr,Outer,[Where,Exprs],Names) :-
178		zns_body(Expr,body(Decls,Where),Exprs),
179		!,
180		vars_and_types_of_decls(Decls,Names,Outer).
181		zsubnamespace(Expr,Outer,Inner,Names) :-
182		zns_let(Expr,Defs,Inner),
183		vars_and_types_of_letdefs(Defs,Names,Outer).
184		vars_and_types_of_decls([],[],[]).
185		vars_and_types_of_decls([decl(Vars,Type)|Rest],[Vars|NRest],[Type|TRest]) :-
186		!,vars_and_types_of_decls(Rest,NRest,TRest).
187		vars_and_types_of_decls([sdecl(S)|Rest],NRest,[S|TRest]) :-
188		vars_and_types_of_decls(Rest,NRest,TRest).
189		vars_and_types_of_letdefs([],[],[]).
190		vars_and_types_of_letdefs([letdef(Name,Expr)|Rest],[Name|NRest],[Expr|ERest]) :-
191		vars_and_types_of_letdefs(Rest,NRest,ERest).
192
193
194
195		anon_decls([],[],[]).
196		anon_decls([sdecl(S)|DRest],[sdecl(S)|ARest],ERest) :-
197		!,anon_decls(DRest,ARest,ERest).
198		anon_decls([D|DRest],[A|ARest],[E|ERest]) :- anon_decls2(D,A,E),anon_decls(DRest,ARest,ERest).
199		anon_decls2(decl(Vars,_),decl(Vars,E),E).
200		anon_decls2(letdef(Name,_),letdef(Name,E),E).
201
202
203		zns_body(body(Decl,Where),body(Decl,Where),[]) :- !.
204		zns_body(Expr,Body,Res) :- zns_body2(Expr,Body,Res).
205
206		zns_body2(forall(Body,Expr),Body,[Expr]).
207		zns_body2(exists(Body,Expr),Body,[Expr]).
208		zns_body2(exists1(Body,Expr),Body,[Expr]).
209		zns_body2(sforall(Body,Expr),Body,[Expr]).
210		zns_body2(sexists(Body,Expr),Body,[Expr]).
211		zns_body2(sexists1(Body,Expr),Body,[Expr]).
212		zns_body2(mu(Body,Expr),Body,[Expr]).
213		zns_body2(comp(Body,Expr),Body,[Expr]).
214		zns_body2(lambda(Body,Expr),Body,[Expr]).
215
216		zns_let(letexpr(Defs,Expr),Defs,Expr).
217		zns_let(letpred(Defs,Pred),Defs,Pred).
218
219
220		%*******************************************************************************
221		% expression equivalence
222
223		equal_expression(A,B) :- equal_expression2(A,B,[]).
224
225		equal_expression2(Expr,Expr,_) :- !.
226		equal_expression2([AExpr|ARest],[BExpr|BRest],Mapping) :-
227		!,equal_expression2(AExpr,BExpr,Mapping),
228		equal_expression2(ARest,BRest,Mapping).
229		equal_expression2(A,B,Mapping) :-
230		same_functor(A,B),
231		equal_expression3(A,B,Mapping).
232
233		equal_expression3(ref(AName,[]),ref(BName,[]),Mapping) :-
234	?	member(mapping(AName,AMap),Mapping),!,AMap=BName.
235		equal_expression3(A,B,Mapping) :-
236		zsubnamespace(A,AOuter,AInner,ANames),
237		!,
238		zsubnamespace(B,BOuter,BInner,BNames),
239		equal_expression2(AOuter,BOuter,Mapping),
240		extend_mapping(ANames,BNames,Mapping,NewMapping),
241		equal_expression2(AInner,BInner,NewMapping).
242		equal_expression3(A,B,Mapping) :-
243		zexpr_conversion(A,ASubs,BSubs,B),
244		equal_expression2(ASubs,BSubs,Mapping).
245
246		extend_mapping([],[],Mapping,Mapping) :- !.
247		extend_mapping([A|ARest],[B|BRest],Mapping,NewMapping) :-
248		!,extend_mapping(A,B,Mapping,InterMapping),
249		extend_mapping(ARest,BRest,InterMapping,NewMapping).
250		extend_mapping(A,B,Mapping,[mapping(A,B)|Mapping]).
251
252
253		%*******************************************************************************
254		% clean_where removes double constraints
255		clean_where(Where,Cleaned) :-
256		normalise_ands(Where,NWhere),
257		clean_where2(NWhere,[],Cleaned).
258		clean_where2([],_,[]).
259		clean_where2([W|Rest],Before,Cleaned) :-
260		(exists_equal(Before,W) -> Cleaned = RestCleaned ; Cleaned = [W|RestCleaned]),
261		clean_where2(Rest,[W|Before],RestCleaned).
262
263		exists_equal([ExprA|_],ExprB) :- equal_expression(ExprA,ExprB),!.
264		exists_equal([_|Rest],Expr) :- exists_equal(Rest,Expr).
265
266		%*******************************************************************************
267		% normalise conjunctions
268		normalise_ands(Ands,Normalised) :-
269		normalise_ands2(Ands,Normalised,[]).
270		normalise_ands2([]) --> !,[].
271		normalise_ands2([A|Rest]) -->
272		!,normalise_ands2(A),normalise_ands2(Rest).
273		normalise_ands2(and(A,B)) -->
274		!,normalise_ands2(A), normalise_ands2(B).
275		normalise_ands2(truth) --> !,[].
276		normalise_ands2(Expr) --> [Expr].
277
278
279
280		%*******************************************************************************
281		% typed versions
282
283		zsubexpressionst(ti(Expr,_),Subs) :-
284		zexpr_conversion(Expr,Subs,_,_).
285		zexpr_conversiont(ti(E,Type),ESubs,CSubs,ti(C,Type)) :-
286		zexpr_conversion(E,ESubs,CSubs,C).
287
288		znamespacet(ti(E,Type),Outer,[Exprs,Where],Names,NOuter,[NExprs,NWhere],ti(N,Type)) :-
289		zns_body2(E,ti(body(Decls,Where),BType),Exprs),!,
290		extract_t_vars_outer(Decls,DeclVars,Outer,NOuter,NDecls),
291		functor(E,Functor,Arity),functor(N,Functor,Arity),
292		zns_body2(N,ti(body(NDecls,NWhere),BType),NExprs),
293		same_length(Where,NWhere),
294		same_length(Exprs,NExprs),
295		append(DeclVars,Names).
296		znamespacet(ti(E,Type),Outer,Inner,Names,NOuter,NInner,ti(N,Type)) :-
297		zns_let(E,Defs,Inner),!,
298		subexpressions:extract_t_vars_outerl(Defs,Names,Outer,NOuter,NDefs),
299		functor(E,Functor,Arity),functor(N,Functor,Arity),
300		zns_let(N,NDefs,NInner).
301
302		znamespacet(ti(E,_),Outer,Inner,Names) :-
303		zns_body2(E,ti(body(Decls,Where),_),Exprs),!,
304		extract_t_vars_outer(Decls,DeclVars,Outer),
305		append(DeclVars,Names),
306		append(Where,Exprs,Inner).
307		znamespacet(ti(E,_),Outer,Inner,Names) :-
308		zns_let(E,Defs,Inner),!,
309		extract_t_vars_outerl(Defs,Names,Outer).
310
311		zsubnamespacet(ti(E,Type),Outer,[Where,Exprs],Names,[Type,BType]) :-
312		zns_body2(E,ti(body(Decls,Where),BType),Exprs),!,
313		extract_t_vars_outer(Decls,Names,Outer).
314		zsubnamespacet(ti(E,Type),Outer,Inner,Names,[Type]) :-
315		zns_let(E,Defs,Inner),!,
316		extract_t_vars_outerl(Defs,Names,Outer).
317
318
319
320		extract_t_vars_outer([],[],[],[],[]).
321		extract_t_vars_outer([ti(decl(Vars,TypeExpr),DT)|DRest],
322		[Vars|VRest],
323		[TypeExpr|TRest],
324		[NTypeExpr|NTRest],
325		[ti(decl(Vars,NTypeExpr),DT)|NDRest]) :-
326		extract_t_vars_outer(DRest,VRest,TRest,NTRest,NDRest).
327		extract_t_vars_outer([],[],[]).
328		extract_t_vars_outer([ti(decl(Vars,TypeExpr),none)|DRest],[Vars|VRest],[TypeExpr|TRest]) :-
329		extract_t_vars_outer(DRest,VRest,TRest).
330
331		extract_t_vars_outerl([],[],[],[],[]).
332		extract_t_vars_outerl([ti(letdef(Name,Expr),DT)|DRest],
333		[Name|NRest],
334		[Expr|ERest],
335		[NExpr|NERest],
336		[ti(letdef(Name,NExpr),DT)|NDRest]) :-
337		extract_t_vars_outerl(DRest,NRest,ERest,NERest,NDRest).
338		extract_t_vars_outerl([],[],[]).
339		extract_t_vars_outerl([ti(letdef(Name,Expr),none)|DRest],[Name|NRest],[Expr|ERest]) :-
340		extract_t_vars_outerl(DRest,NRest,ERest).
341
342
343
344		%*******************************************************************************
345		% expression equivalence -- typed
346
347		equal_expressiont(A,B) :- equal_expression2t(A,B,[]).
348
349		equal_expression2t(Expr,Expr,_) :- !.
350		equal_expression2t([AExpr|ARest],[BExpr|BRest],Mapping) :-
351		!,equal_expression2t(AExpr,BExpr,Mapping),
352		equal_expression2t(ARest,BRest,Mapping).
353		equal_expression2t(ti(A,TA),ti(B,TB),Mapping) :-
354		functor(A,Functor,Arit),
355		functor(B,Functor,Arit),
356		similiar_type(TA,TB),
357		equal_expression3t(ti(A,T),ti(B,T),Mapping).
358
359		equal_expression3t(ti(ref(AName,[]),T),ti(ref(BName,[]),T),Mapping) :-
360	?	member(mapping(AName,AMap),Mapping),!,AMap=BName.
361		equal_expression3t(A,B,Mapping) :-
362		zsubnamespacet(A,AOuter,AInner,ANames,ATypes),
363		!,
364		zsubnamespacet(B,BOuter,BInner,BNames,BTypes),
365		equal_expression2t(AOuter,BOuter,Mapping),
366		similiar_type_l(ATypes,BTypes),
367		extend_mapping(ANames,BNames,Mapping,NewMapping),
368		equal_expression2t(AInner,BInner,NewMapping).
369		equal_expression3t(A,B,Mapping) :-
370		zexpr_conversiont(A,ASubs,BSubs,B),
371		equal_expression2t(ASubs,BSubs,Mapping).
372
373		% we do not only check if the types are exactly the same, because
374		% some bodies have different types, even if they are equal.
375		similiar_type(T,T) :- !.
376		similiar_type(set(A),set(B)) :- similiar_type(A,B).
377		similiar_type(tuple(A),tuple(B)) :- similiar_type_l(A,B).
378		similiar_type(schema(A),schema(B)) :- same_length(A,B).
379		similiar_type_l([],[]).
380		similiar_type_l([A|Arest],[B|Brest]) :-
381		similiar_type(A,B),
382		similiar_type_l(Arest,Brest).
383
384		%*******************************************************************************
385		% clean_where removes double constraints
386		clean_wheret(Where,Cleaned) :-
387		normalise_andst(Where,NWhere),
388		clean_where2t(NWhere,[],Cleaned).
389		clean_where2t([],_,[]).
390		clean_where2t([ti(truth,bool)|Rest],Before,Cleaned) :-
391		!,clean_where2t(Rest,Before,Cleaned).
392		clean_where2t([W|Rest],Before,Cleaned) :-
393		(exists_equalt(Before,W) -> Cleaned = RestCleaned ; Cleaned = [W|RestCleaned]),
394		clean_where2t(Rest,[W|Before],RestCleaned).
395
396		exists_equalt([ExprA|_],ExprB) :- equal_expressiont(ExprA,ExprB),!.
397		exists_equalt([_|Rest],Expr) :- exists_equalt(Rest,Expr).
398
399		%*******************************************************************************
400		% normalise conjunctions -- typed
401		normalise_andst(Ands,Normalised) :-
402		normalise_ands2t(Ands,Normalised,[]).
403		normalise_ands2t([]) --> !,[].
404		normalise_ands2t([A|Rest]) -->
405		!,normalise_ands2t(A),normalise_ands2t(Rest).
406		normalise_ands2t(ti(and(A,B),bool)) -->
407		!,normalise_ands2t(A), normalise_ands2t(B).
408		normalise_ands2t(ti(truth,bool)) --> !,[].
409		normalise_ands2t(Expr) --> [Expr].
410
411
412
413		%*******************************************************************************
414		% rename variables -- typed version
415
416		rename_variablest(Exprs,[],Exprs) :- !.
417		rename_variablest(ti(body(Decls,Where),set(schema(Fields))),Renamings,
418		ti(body(RDecls,RWhere),set(schema(RFields)))) :-
419		!,
420		rename_declst(Decls,Renamings,RDecls),
421		rename_fieldst(Fields,Renamings,RFields),
422		rename_variablest2(Where,Renamings,RWhere).
423		rename_variablest(Expr,Renamings,Result) :- rename_variablest2(Expr,Renamings,Result).
424
425		rename_variablest2([],_,[]) :- !.
426		rename_variablest2([E|ERest],Renamings,[P|PRest]) :-
427		!,rename_variablest2(E,Renamings,P),
428		rename_variablest2(ERest,Renamings,PRest).
429		rename_variablest2(ti(ref(Name,P),Type),Renamings,ti(ref(New,P),Type)) :-
430		!,
431	?	(member(rename(New,Name),Renamings) ->
432		!,true;
433		New = Name).
434		rename_variablest2(Expr,Renamings,Result) :-
435		znamespacet(Expr,Outer,Inner,Names,NOuter,NInner,Result),
436		!,
437		rename_variablest2(Outer,Renamings,NOuter),
438		remove_renamings(Renamings,Names,NRenamings),
439		rename_variablest2(Inner,NRenamings,NInner).
440		rename_variablest2(Expr,Renamings,Result) :-
441		zexpr_conversiont(Expr,Subs,PSubs,Result),
442		rename_variablest2(Subs,Renamings,PSubs).
443
444		rename_declst([],_,[]).
445		rename_declst([ti(decl(Vars,Type),none)|DRest],Renamings,[ti(decl(RVars,Type),none)|RRest]) :-
446		!,rename_decl_varst(Vars,Renamings,RVars),
447		rename_declst(DRest,Renamings,RRest).
448		rename_decl_varst([],_,[]).
449		rename_decl_varst([Old|ORest],Renamings,[New|NRest]) :-
450	?	(member(rename(New,Old),Renamings) ->
451		!,true;
452		Old = New),
453		rename_decl_varst(ORest,Renamings,NRest).
454
455		rename_fieldst([],_,[]).
456		rename_fieldst([field(Old,Type)|ORest],Renamings,[field(New,Type)|NRest]) :-
457	?	(member(rename(New,Old),Renamings) ->
458		!,true;
459		Old = New),
460		rename_fieldst(ORest,Renamings,NRest).
461
462		remove_renamings([],_,[]).
463		remove_renamings([rename(New,Old)|RRest],Names,Renamings) :-
464	?	(member(Old,Names) ->
465		Renamings = ORenamings;
466		Renamings = [rename(New,Old)|ORenamings]),
467		remove_renamings(RRest,Names,ORenamings).