1 | % (c) 2009-2015 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). |