1 | % (c) 2009-2019 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(ztransformations,[freetype2namedsets/2, | |
6 | remove_ignore_decl/2, | |
7 | removeabbreviations/2, | |
8 | ggsimplify/2, | |
9 | removesexpr/2, | |
10 | clearsrefs/2]). | |
11 | ||
12 | :- use_module(library(lists)). | |
13 | :- use_module(library(ordsets)). | |
14 | ||
15 | :- use_module(probsrc(tools)). | |
16 | :- use_module(probsrc(error_manager)). | |
17 | ||
18 | :- use_module(subexpressions). | |
19 | :- use_module(z_typechecker). | |
20 | :- use_module(z_tools). | |
21 | :- use_module(zparameters). | |
22 | ||
23 | :- use_module(probsrc(module_information)). | |
24 | :- module_info(group,proz). | |
25 | :- module_info(description,'This module provides several transformations on the Z syntax tree in order to prepare the translation to B.'). | |
26 | ||
27 | ||
28 | %******************************************************************************* | |
29 | % convert free types to named sets | |
30 | freetype2namedsets([],[]) :- !. | |
31 | freetype2namedsets([E|ERest],[C|CRest]) :- | |
32 | !,freetype2namedsets(E,C), | |
33 | freetype2namedsets(ERest,CRest). | |
34 | freetype2namedsets(data(Name,Arms),namedset(Name,Members)) :- | |
35 | % a freetype can be converted if it elements are just constants, no constructors | |
36 | \+ member(arm(_,just(_)),Arms), | |
37 | !, findall(M,member(arm(M,nothing),Arms),Members). | |
38 | freetype2namedsets(E,E). | |
39 | ||
40 | ||
41 | %******************************************************************************* | |
42 | % remove the declaration of prozignore, if present | |
43 | remove_ignore_decl([],[]). | |
44 | remove_ignore_decl([define(Sets,body(Decls,Wheres))|Rest],Result) :- | |
45 | !,remove_ignore_decl2(Decls,NewDecls), | |
46 | (NewDecls = [], Wheres = [] -> | |
47 | Result = IRest; | |
48 | Result = [define(Sets,body(NewDecls,Wheres))|IRest]), | |
49 | remove_ignore_decl(Rest,IRest). | |
50 | remove_ignore_decl([Def|Rest],[Def|IRest]) :- | |
51 | remove_ignore_decl(Rest,IRest). | |
52 | remove_ignore_decl2([],[]). | |
53 | remove_ignore_decl2([decl(Vars,Type)|Rest],Result) :- | |
54 | ignore(Ignore), | |
55 | remove_all(Vars,[Ignore],NewVars), | |
56 | (NewVars = [] -> | |
57 | Result = IRest; | |
58 | Result = [decl(NewVars,Type)|IRest]), | |
59 | remove_ignore_decl2(Rest,IRest). | |
60 | ||
61 | ||
62 | %******************************************************************************* | |
63 | % handling of recursive free types | |
64 | ||
65 | ||
66 | split_recursive_freetypes(Defs,Recursives,NonRec) :- | |
67 | find_freetype_refs(Defs,Refs), | |
68 | split_list(is_cyclic_freetype(Refs),Defs,Recursives,NonRec). | |
69 | ||
70 | is_cyclic_freetype(Refs,FreetypeDefinition) :- | |
71 | ti_expr(FreetypeDefinition,data(FreetypeName,_Arms)), | |
72 | is_cyclic(FreetypeName,FreetypeName,Refs,[]). | |
73 | is_cyclic(Node,Freetype,Refs,_) :- | |
74 | member(ref(Node,Freetype),Refs),!. | |
75 | is_cyclic(Node,Freetype,Refs,Old) :- | |
76 | member(ref(Node,Next),Refs), | |
77 | \+ member(Next,Old), | |
78 | is_cyclic(Next,Freetype,Refs,[Next|Old]),!. | |
79 | ||
80 | find_freetype_refs(FreeTypeDefinitions,References) :- | |
81 | maplist(find_freetype_refs2,FreeTypeDefinitions,ReferencesL), | |
82 | append(ReferencesL,References). | |
83 | % find_freetype_refs2(+FreeTypeDefinition,-References): | |
84 | % For a freetype, find references in it definition to other types | |
85 | % FreeTypeDefinition: The definition of the freetype (data(Name,Arms) + type) | |
86 | % References: A list of ref(NameA,NameB) where NameA and NameB are both names of freetypes | |
87 | % and in the definition of NameA is a reference to NameB. | |
88 | find_freetype_refs2(FreeTypeDefinition,References) :- | |
89 | ti_expr(FreeTypeDefinition,data(FreetypeName,Arms)), | |
90 | % extract the domains of the constructor arms (skip the constants) | |
91 | convlist(extract_freetype_arm_domain_type,Arms,ArmDomainTypes), | |
92 | foldl(extract_fr,ArmDomainTypes,[],ReferencedFreetypes), | |
93 | maplist(construct_reference(FreetypeName),ReferencedFreetypes,References). | |
94 | extract_freetype_arm_domain_type(ArmTi,ArmDomainType) :- | |
95 | ti_expr(ArmTi,arm(_Name,ArmDef)), | |
96 | ti_expr(ArmDef,just(ArmDomain)), | |
97 | ti_type(ArmDomain,ArmDomainType). | |
98 | construct_reference(FreetypeName,ReferencedFreetype,ref(FreetypeName,ReferencedFreetype)). | |
99 | ||
100 | % extract_fr(Type,In,Out): Extract all referenced freetypes in a type. | |
101 | % Type: The Z type | |
102 | % In: An ordered set (-> library(ordset)) | |
103 | % Out: An ordered set with in Type referenced types added | |
104 | extract_fr(freetype(Name),In,Out) :- !,ord_add_element(In,Name,Out). | |
105 | extract_fr(set(X),In,Out) :- !,extract_fr(X,In,Out). | |
106 | extract_fr(tuple(Types),In,Out) :- !,foldl(extract_fr,Types,In,Out). | |
107 | extract_fr(schema(Fields),In,Out) :- | |
108 | !,maplist(extract_field_type,Fields,Types), | |
109 | foldl(extract_fr,Types,In,Out). %% FIXED: extract_fr should probably be the first argument, but clause is not tested | |
110 | extract_fr(_,Refs,Refs). | |
111 | ||
112 | % get the type from a field of a schema type (removing the name of the field) | |
113 | extract_field_type(field(_,Type),Type). | |
114 | ||
115 | ||
116 | ||
117 | %******************************************************************************* | |
118 | % Some general simplifications | |
119 | ||
120 | ggsimplify(In,Out) :- | |
121 | prepare_given_env(In,GivenEnv), | |
122 | prepare_freetype_env(In,FreetypeEnv,I2), | |
123 | Env = [given(GivenEnv),freetype(FreetypeEnv)], | |
124 | ggsimplify1(I2,Env,Out). | |
125 | ||
126 | prepare_given_env(TypedDef,GivenEnv) :- | |
127 | findall(G, | |
128 | (member(ti(given(Ns),none),TypedDef),member(G,Ns)), | |
129 | Given), | |
130 | findall(N,member(ti(namedset(N,_),none),TypedDef),NamedSets), | |
131 | append(Given,NamedSets,GivenEnv). | |
132 | ||
133 | prepare_freetype_env(TypedDef,FreetypeEnv,NewDefs) :- | |
134 | findall(ti(data(Freetype,Arms),Type), | |
135 | member(ti(data(Freetype,Arms),Type),TypedDef), | |
136 | DataEnv), | |
137 | ( DataEnv = [] -> | |
138 | FreetypeEnv = [],NewDefs = TypedDef | |
139 | ; otherwise -> | |
140 | ||
141 | split_recursive_freetypes(DataEnv,Recursive,NonRecursive), | |
142 | ||
143 | findall(ft(F,rec),member(F,Recursive),FRec), | |
144 | findall(ft(F,simpl),member(F,NonRecursive),FNRec), | |
145 | append(FRec,FNRec,FreetypeEnv), | |
146 | ||
147 | maplist(create_axdef_for_recfreetype,Recursive,Axdefs), | |
148 | append(Axdefs,TypedDef,NewDefs) | |
149 | ). | |
150 | ||
151 | ggsimplify1([],_,[]) :- !. | |
152 | ggsimplify1([Expr|Rest],Env,[SimplExpr|SimplRest]) :- | |
153 | !,ggsimplify1(Expr,Env,SimplExpr), | |
154 | ggsimplify1(Rest,Env,SimplRest). | |
155 | ggsimplify1(ti(Expr,T),Env,ti(Simpl,T)) :- | |
156 | presimplify_fixpoint(Expr,T,Env,Step1), | |
157 | zexpr_conversiont(ti(Step1,T),Subs,SSubs,ti(S,T)), | |
158 | ggsimplify1(Subs,Env,SSubs), | |
159 | ggsimplify_fixpoint(S,T,Env,Simpl). | |
160 | ||
161 | ggsimplify_fixpoint(Expr,T,Env,Result) :- | |
162 | ggsimplify2(Expr,T,Env,Inter), | |
163 | Expr \= Inter, | |
164 | !,ggsimplify_fixpoint(Inter,T,Env,Result). | |
165 | ggsimplify_fixpoint(Expr,_,_,Expr). | |
166 | ||
167 | presimplify_fixpoint(Expr,T,Env,Result) :- | |
168 | presimplify(Expr,T,Env,Inter), | |
169 | Expr \= Inter, | |
170 | !,presimplify_fixpoint(Inter,T,Env,Result). | |
171 | presimplify_fixpoint(Expr,_,_,Expr). | |
172 | ||
173 | % remove all expressions except types from declarations | |
174 | presimplify(decl(Vars,ti(_,Type)),_,_,decl(Vars,ti(basetype(Type),Type))) :- !. | |
175 | ||
176 | % just use the type, if a prozignore annotation is found | |
177 | presimplify(pregen(Name,_),Type,_,basetype(Type)) :- ignore(Name). | |
178 | ||
179 | % testing: direct call to ftconstant | |
180 | presimplify(apply(ti(ref(name('\\proztestftconstant',''),[]),_),Arg), | |
181 | freetype(FT),_,ftconstant(FT,Case)) :- | |
182 | !, | |
183 | (Arg = ti(tuple([ti(ref(FT,[]),set(freetype(FT))), | |
184 | ti(ref(Case,[]),freetype(FT))]),_) | |
185 | -> true | |
186 | ; add_error(ztransformations,'wrong arguments for \\proztestftconstant')). | |
187 | ||
188 | % testing: direct call to ftconstructor | |
189 | presimplify(apply(ti(ref(name('\\proztestftconstructor',''),[]),_),Arg), | |
190 | freetype(FT),_,ftconstructor(FT,Case,Inner)) :- | |
191 | !, | |
192 | (Arg = ti(tuple([ti(ref(FT,[]),set(freetype(FT))), | |
193 | ti(ref(Case,[]),set(tuple([_,freetype(FT)]))), | |
194 | Inner]),_) | |
195 | -> true | |
196 | ; add_error(ztransformations,'wrong arguments for \\proztestftconstructor')). | |
197 | ||
198 | % testing: direct call to ftdestructor | |
199 | presimplify(apply(ti(ref(name('\\proztestftdestructor',''),[]),_),Arg), | |
200 | _,_,ftdestructor(FT,Case,ti(Inner,freetype(FT)))) :- | |
201 | !, | |
202 | (Arg = ti(tuple([ti(ref(FT,[]),set(freetype(FT))), | |
203 | ti(ref(Case,[]),set(tuple([_,freetype(FT)]))), | |
204 | ti(Inner,freetype(FT))]),_) | |
205 | -> true | |
206 | ; add_error(ztransformations,'wrong arguments for \\proztestftdestructor')). | |
207 | ||
208 | % testing: direct usage of ftcase | |
209 | presimplify(prerel(name('\\proztestftcase',''),Arg),_,_,ftcase(FT,Case,ti(Expr,freetype(FT)))) :- | |
210 | !, | |
211 | ((Arg = ti(tuple([ti(ref(FT,[]),set(freetype(FT))), | |
212 | ti(ref(Case,[]),CaseType), | |
213 | ti(Expr,freetype(FT))]),_), | |
214 | (CaseType=freetype(FT);CaseType=set(tuple([_,freetype(FT)])))) | |
215 | -> !,true | |
216 | ; add_error(ztransformations,'wrong arguments for \\proztestftcase')). | |
217 | ||
218 | % freetype destructor call | |
219 | presimplify(apply(FunTi,ArgTi),IType,Env,ftdestructor(FT,CName,ArgTi)) :- | |
220 | is_ftdestructor_expression(FunTi,Env,FT,CName,IType). | |
221 | ||
222 | % freetype constructor range membership | |
223 | presimplify(member(Expr,ti(apply(ti(ref(name('\\ran',''),[]),_),Constructor),set(freetype(FT)))), | |
224 | bool,Env,ftcase(FT,CName,Expr)) :- | |
225 | is_ftconstructor_expression(Constructor,Env,FT,CName,_). | |
226 | ||
227 | % freetype destructor domain membership | |
228 | presimplify(member(Expr,ti(apply(ti(ref(name('\\dom',''),[]),_),Destructor),set(freetype(FT)))), | |
229 | bool,Env,ftcase(FT,CName,Expr)) :- | |
230 | is_ftdestructor_expression(Destructor,Env,FT,CName,_). | |
231 | ||
232 | % freetype constructor range not membership | |
233 | presimplify(inrel(name('\\notin',''),Expr, | |
234 | ti(apply(ti(ref(name('\\ran',''),[]),_),Constructor),set(freetype(FT)))), | |
235 | bool,Env,not(ti(ftcase(FT,CName,Expr),bool))) :- | |
236 | is_ftconstructor_expression(Constructor,Env,FT,CName,_). | |
237 | ||
238 | % freetype destructor domain not membership | |
239 | presimplify(inrel(name('\\notin',''),Expr, | |
240 | ti(apply(ti(ref(name('\\dom',''),[]),_),Destructor),set(freetype(FT)))), | |
241 | bool,Env,not(ti(ftcase(FT,CName,Expr),bool))) :- | |
242 | is_ftdestructor_expression(Destructor,Env,FT,CName,_). | |
243 | ||
244 | ignore(name('\\prozignore','')). | |
245 | ||
246 | % some simple optimizations of boolean expressions, that can be generated | |
247 | ggsimplify2(and(ti(truth,bool),ti(X,bool)),_,_,X) :- !. | |
248 | ggsimplify2(and(ti(X,bool),ti(truth,bool)),_,_,X) :- !. | |
249 | ggsimplify2(implies(_,ti(truth,bool)),_,_,truth) :- !. | |
250 | ||
251 | ||
252 | % handling of basetypes | |
253 | ggsimplify2(ref(name('\\num',''),[]),_,_,basetype(set(num))) :- !. | |
254 | ggsimplify2(power(ti(basetype(T),T)),_,_,basetype(set(T))) :- !. | |
255 | ggsimplify2(pregen(name('\\finset',''),ti(basetype(T),T)),_,_,basetype(set(T))) :- !. | |
256 | ggsimplify2(cross(List),_,_,basetype(set(tuple(Types)))) :- | |
257 | all_basetypes(List,Types),!. | |
258 | ggsimplify2(ingen(name('\\rel',''),ti(basetype(set(A)),_),ti(basetype(set(B)),_)),_,_, | |
259 | basetype(set(tuple([A,B])))) :- !. | |
260 | ggsimplify2(ref(Name,[]),set(given(Name)),Env,basetype(set(given(Name)))) :- | |
261 | member(given(GivenEnv),Env),member(Name,GivenEnv),!. | |
262 | ggsimplify2(comp(ti(body(_,[]),_),ti(nothing,none)),Type,_,basetype(Type)) :- !. | |
263 | ||
264 | ||
265 | % Comprehension sets with expressions are replaced by comprehensions sets | |
266 | % without expressions by using an "Exists" operator | |
267 | ggsimplify2(comp(BodyTi, ti(just(ResultTi),_)), _,_, comp(NewBody,ti(nothing,none))) :- | |
268 | !, simplify_compset(BodyTi,ResultTi,NewBody). | |
269 | ||
270 | % Same for Mu-Operators with expressions | |
271 | ggsimplify2(mu(BodyTi, ti(just(ResultTi),_)), _,_, mu(NewBody,ti(nothing,none))) :- | |
272 | !,simplify_compset(BodyTi,ResultTi,NewBody). | |
273 | ||
274 | % Equallity of two bindings can be substituted by a conjunction of | |
275 | % equalities. | |
276 | % E.g. < a=>m, b=>n > = < a=>k, b=>l > | |
277 | % can be simplified to m=k /\ n=l | |
278 | ggsimplify2(equal(ti(binding(B1),_),ti(binding(B2),_)), _,_, Result) :- | |
279 | !, equal_bindings(B1,B2,ti(Result,bool)). | |
280 | ||
281 | % EXISTS1 is replaced by checking the cardinality of a comprehension set | |
282 | ggsimplify2(exists1(ti(body(Decl,Where),BType),Condition), _, Env, equal(Card,ti(number(1),num))) :- | |
283 | !, | |
284 | Card1 = ti(apply(Ref,Comp),num), | |
285 | Ref = ti(ref(name('\\#',''),[]),set(tuple([SetType,num]))), | |
286 | Comp = ti(comp(ti(body(Decl,NewWhere),BType),ti(nothing,none)),SetType), | |
287 | compset_type_convert(BType,SetType), | |
288 | append(Where,[Condition],NewWhere), | |
289 | ggsimplify1(Card1,Env,Card). | |
290 | ||
291 | % the backward relational composition is replaced by the (forward) relational composition | |
292 | ggsimplify2(inop(name('\\circ',''), A, B), _,_, inop(name('\\comp',''), B, A)) :- !. | |
293 | ||
294 | % the application of the successor function is rewritten to "...+1" | |
295 | % E.g. "succ a" -> "a+1" | |
296 | ggsimplify2(apply(ti(ref(name('succ',''),[]),_), Arg), _,_, | |
297 | inop(name('+',''),Arg, ti(number(1),num))) :- !. | |
298 | ||
299 | % remove double entries, trues, etc. in the where part of a body | |
300 | ggsimplify2(body(Decls,Where), _,_, body(Decls,NewWhere)) :- | |
301 | !,clean_wheret(Where,NewWhere). | |
302 | ||
303 | % simplify set membership tests for comprehension sets | |
304 | ggsimplify2(member(Expr, ti(comp(Body,ti(nothing,none)),_)), _,_, Condition) :- | |
305 | Body = ti(body([ti(decl([Var],_),_)],Wheres),_), | |
306 | !,simplify_member(Expr,Var,Wheres,ti(Condition,bool)). | |
307 | ||
308 | % the check of membership is trivial for basetypes because typechecking already | |
309 | % ensures that the property is true. | |
310 | ggsimplify2(member(_,ti(basetype(_),_)), _,_, truth) :- !. | |
311 | ||
312 | % the reflexive-transitive closure can be expressed by a union of the | |
313 | % transitive closure and the inferred type | |
314 | ggsimplify2(postop(name('\\star',''),ExprTi), RelType, _, inop(name('\\cup',''),TransCls,Id)) :- | |
315 | RelType = set(tuple([T,T])),!, | |
316 | TransCls = ti(postop(name('\\plus',''),ExprTi),RelType), | |
317 | Id = ti(pregen(name('\\id',''),ti(basetype(set(T)),set(T))),RelType). | |
318 | ||
319 | % simplify the direct application of a lambda expression without preconditions | |
320 | ggsimplify2(apply(ti(lambda(ti(body([ti(decl([Param],_),_)],[]),_),ExprTi),_), | |
321 | ArgTi),_,_, | |
322 | NewExpr) :- | |
323 | !,replace_expression(ExprTi,Param,ArgTi,ti(NewExpr,_)). | |
324 | ||
325 | % rewrite the bag display to the application of the items function to the sequence of elements | |
326 | ggsimplify2(bag(Expressions), BagType, _Env, apply(ItemsFun,Seq)) :- !, | |
327 | BagType = set(tuple([X,num])), SeqType = set(tuple([num,X])), | |
328 | ItemsFun = ti(ref(name('items',''),[]),set(tuple([BagType,SeqType]))), | |
329 | Seq = ti(seq(Expressions),set(SeqType)). | |
330 | ggsimplify2(pregen(name('\\bag',''),Set), _Type, _Env, ingen(name('\\pfun',''), Set, Nat1)) :- | |
331 | ti_expr(Nat1,ref(name('\\nat','_1'),[])), | |
332 | ti_type(Nat1,set(num)). | |
333 | ggsimplify2(inop(name('\\bcount',''),Bag,Elem),Type,Env,IfThenElse) :- | |
334 | !,create_bag_count(Bag,Elem,IfThenElse1), ggsimplify1(ti(IfThenElse1,Type),Env,ti(IfThenElse,_)). | |
335 | ggsimplify2(apply(Count,Bag), _Type, _Env, lambda(Body,Expr)) :- | |
336 | ti_expr(Count,ref(name('count',''),[])),!, | |
337 | ti_type(Bag,BagType), | |
338 | BagType = set(tuple([ArgType,num])), | |
339 | z_counter('param__',P),Param=name(P,''), | |
340 | Body = ti(body([ti(decl([Param],ti(basetype(set(ArgType)),set(ArgType))),none)],[]), | |
341 | set(schema([field(Param,ArgType)]))), | |
342 | ti_expr(RefParam,ref(Param,[])), ti_type(RefParam,ArgType), | |
343 | create_bag_count(Bag,RefParam,IfThenElse), | |
344 | ti_expr(Expr,IfThenElse), ti_type(Expr,num). | |
345 | ggsimplify2(inop(name('\\otimes',''),Factor,Bag),Type,Env,Comp) :- | |
346 | !,create_bag_otimes(Factor,Bag,Comp1), ggsimplify1(ti(Comp1,Type),Env,ti(Comp,_)). | |
347 | ggsimplify2(inop(name('\\uminus',''),A,B),Type,Env,Comp) :- | |
348 | !,create_bag_minus(A,B,Comp1), ggsimplify1(ti(Comp1,Type),Env,ti(Comp,_)). | |
349 | ggsimplify2(inop(name('\\uplus',''),A,B),Type,Env,Comp) :- | |
350 | !,create_bag_plus(A,B,Comp1), ggsimplify1(ti(Comp1,Type),Env,ti(Comp,_)). | |
351 | ggsimplify2(inrel(name('\\inbag',''),Elem,Bag),_Type,_Env,member(Elem,Domain)) :- | |
352 | !,make_z_domain(Bag,Domain). | |
353 | ggsimplify2(inrel(name('\\subbageq',''),BagA,BagB),_Type,_Env,Pred) :- | |
354 | !,create_subbag(BagA,BagB,Pred). | |
355 | ||
356 | ||
357 | % handling of free types | |
358 | ||
359 | % free type constants | |
360 | ggsimplify2(ref(CName,[]),freetype(FT),Env,ftconstant(FT,CName)) :- | |
361 | is_ftconstant2(Env,FT,CName),!. | |
362 | ||
363 | % free type constructor | |
364 | ggsimplify2(ref(CName,[]),set(tuple([ArgType,freetype(FT)])),Env,Lambda) :- | |
365 | is_ftconstructor2(Env,FT,CName,DomSet),!, | |
366 | Lambda1 = lambda(ti(body([ti(decl([Param],ti(basetype(set(ArgType)),set(ArgType))),none)], | |
367 | [ti(member(ti(ref(Param,[]),ArgType),DomSet),bool)]), | |
368 | set(schema([field(Param,ArgType)]))), | |
369 | ti(ftconstructor(FT,CName,ti(ref(Param,[]),ArgType)),freetype(FT))), | |
370 | z_counter('param__',P),Param=name(P,''), | |
371 | ggsimplify1(ti(Lambda1,set(tuple([ArgType,freetype(FT)]))),Env,ti(Lambda,_)). | |
372 | ||
373 | % free type set -> comprehension set for non-recursive free types | |
374 | ggsimplify2(ref(FT,[]),set(freetype(FT)),Env,Result) :- | |
375 | ftget(Env,FT,Arms,simpl),!, | |
376 | z_counter('param__',P),Param=name(P,''), | |
377 | Result1 = comp(ti(body([ti(decl([Param],ti(basetype(set(freetype(FT))),set(freetype(FT)))),none)], | |
378 | Constraints),BType),ti(nothing,none)), | |
379 | BType = set(schema([field(Param,freetype(FT))])), | |
380 | create_constraints(Arms,FT,ti(ref(Param,[]),freetype(FT)),Constraints), | |
381 | ggsimplify1(ti(Result1,set(freetype(FT))),Env,ti(Result,_)). | |
382 | ||
383 | % recursive free type set -> reference to global constant | |
384 | ggsimplify2(ref(FT,[]),set(freetype(FT)),Env,ref(Global,[])) :- | |
385 | ftget(Env,FT,_,rec),!, | |
386 | global_ft_constant(FT,Global). | |
387 | ||
388 | global_ft_constant(name(S,Deco),name(Global,Deco)) :- | |
389 | atom_concat(S,'__rec',Global). | |
390 | ||
391 | create_constraints([],_,_,[]). | |
392 | create_constraints([ti(arm(CName,ti(just(DomSet),none)),_)|Rest],FT,Expr, | |
393 | [ti(implies(A,B),bool)|CRest]) :- | |
394 | !,ti_type(DomSet,set(CType)), | |
395 | A = ti(ftcase(FT,CName,Expr),bool), | |
396 | B = ti(member(Destr,DomSet),bool), | |
397 | Destr = ti(ftdestructor(FT,CName,Expr),CType), | |
398 | create_constraints(Rest,FT,Expr,CRest). | |
399 | create_constraints([ti(arm(_,ti(nothing,none)),_)|Rest],FT,Expr,CRest) :- | |
400 | create_constraints(Rest,FT,Expr,CRest). | |
401 | ||
402 | is_ftconstructor_expression(ti(ref(CName,[]),set(tuple([IType,freetype(FT)]))),Env,FT,CName,IType) :- | |
403 | is_ftconstructor2(Env,FT,CName,_). | |
404 | is_ftconstructor_expression(ti(postop(name('\\inv',''),Arg),set(tuple([IType,freetype(FT)]))), | |
405 | Env,FT,CName,IType) :- | |
406 | is_ftdestructor_expression(Arg,Env,FT,CName,IType). | |
407 | is_ftdestructor_expression(ti(postop(name('\\inv',''),Arg),set(tuple([freetype(FT),_]))),Env,FT,CName,IType) :- | |
408 | is_ftconstructor_expression(Arg,Env,FT,CName,IType). | |
409 | ||
410 | is_ftconstant2(Env,FT,Name) :- | |
411 | ftget(Env,FT,Arms,_), | |
412 | member(ti(arm(Name,ti(nothing,none)),_),Arms),!. | |
413 | ||
414 | is_ftconstructor2(Env,FT,CName,DomSet) :- | |
415 | ftget(Env,FT,Arms,_), | |
416 | member(ti(arm(CName,ti(just(DomSet),none)),_),Arms),!. | |
417 | ||
418 | ftget(Env,FT,Arms,FtType) :- ftenv(Env,FtEnv),member(ft(ti(data(FT,Arms),_),FtType),FtEnv). | |
419 | ftenv(Env,FtEnv) :- member(freetype(FtEnv),Env),!. | |
420 | ||
421 | create_axdef_for_recfreetype(Ti,ti(axdef(Body),none)) :- | |
422 | ti_expr(Ti,data(FT,Arms)), | |
423 | ||
424 | FTSET = set(freetype(FT)), | |
425 | ||
426 | global_ft_constant(FT,Global), | |
427 | Equation = ti(equal(ti(ref(Global,[]),FTSET),RecLet),bool), | |
428 | create_typed_body([Global],[FTSET],[Equation],Body), | |
429 | ||
430 | ||
431 | RecLet = ti(reclet(ti(ref(Global,[]),FTSET),Compset),FTSET), | |
432 | Compset = ti(comp(CompsetBody,ti(nothing,none)),FTSET), | |
433 | z_counter('param__',P),Param=name(P,''), | |
434 | create_typed_body([Param],[freetype(FT)],Constraints,CompsetBody), | |
435 | create_constraints(Arms,FT,ti(ref(Param,[]),freetype(FT)),Constraints). | |
436 | ||
437 | compset_type_convert(set(schema([field(_,Type)])),set(Type)) :- !. | |
438 | compset_type_convert(set(schema(Fields)),set(tuple([Types]))) :- | |
439 | maplist(extract_field_type,Fields,Types). | |
440 | ||
441 | equal_bindings([],_,ti(truth,bool)). | |
442 | equal_bindings([ti(bindfield(Name,ExprA),_)],Bindings2,ti(equal(ExprA,ExprB),bool)) :- | |
443 | !,member(ti(bindfield(Name,ExprB),_),Bindings2),!. | |
444 | equal_bindings([ti(bindfield(Name,ExprA),_)|BRest],Bindings2, | |
445 | ti(and(ti(equal(ExprA,ExprB),bool),ERest),bool)) :- | |
446 | member(ti(bindfield(Name,ExprB),_),Bindings2),!, | |
447 | equal_bindings(BRest,Bindings2,ERest). | |
448 | ||
449 | simplify_member(ti(ref(Name,Params),Type), Var, Wheres, Condition) :- | |
450 | !,replace_cleanup(Wheres,Var,ti(ref(Name,Params),Type),Condition). | |
451 | ||
452 | simplify_member(Expr,Var,Wheres,Condition) :- | |
453 | count_occurences(Wheres,Var,Count), | |
454 | (Count > 1 -> | |
455 | z_counter('lettmp',Tmp), | |
456 | Condition = ti(letpred([ti(letdef(name(Tmp,''),Expr),none)],Pred),bool), | |
457 | ti_type(Expr,Type), | |
458 | replace_cleanup(Wheres,Var,ti(ref(name(Tmp,''),[]),Type),Pred); | |
459 | ||
460 | replace_cleanup(Wheres,Var,Expr,Condition)). | |
461 | ||
462 | replace_cleanup(Wheres,Var,New,Condition) :- | |
463 | replace_expression(Wheres,Var,New,Conditions), | |
464 | clean_wheret(Conditions,CConditions), | |
465 | z_conjunctiont(CConditions,Condition). | |
466 | ||
467 | ||
468 | % count the number of occurences of references to the variable "Search" | |
469 | % in the given expression | |
470 | count_occurences(Expr,Search,Count) :- | |
471 | count_occurences2(Expr,Search,0,Count). | |
472 | count_occurences2(ti(ref(Search,[]),_),Search,In,Out) :- !,Out is In + 1. | |
473 | count_occurences2([],_,Count,Count) :- !. | |
474 | count_occurences2([Expr|ERest],Search,In,Out) :- | |
475 | !,count_occurences2(Expr,Search,In,I2), | |
476 | count_occurences2(ERest,Search,I2,Out). | |
477 | count_occurences2(Expr,Search,In,Out) :- | |
478 | znamespacet(Expr,Outer,Inner,Names),!, | |
479 | count_occurences2(Outer,Search,In,I2), | |
480 | % if a variable of the same name has been introduced by an quantifier, | |
481 | % we do not look further into the inner expression | |
482 | ( memberchk(Search,Names) -> | |
483 | I2 = Out | |
484 | ; otherwise -> | |
485 | count_occurences2(Inner,Search,I2,Out)). | |
486 | count_occurences2(Expr,Search,In,Out) :- | |
487 | zsubexpressionst(Expr,Subs), | |
488 | count_occurences2(Subs,Search,In,Out). | |
489 | ||
490 | replace_expression(ti(ref(Expr,[]),_),Expr,New,New) :- !. | |
491 | replace_expression([],_,_,[]) :- !. | |
492 | replace_expression([E|Rest],Old,New,[RE|RRest]) :- | |
493 | !,replace_expression(E,Old,New,RE), | |
494 | replace_expression(Rest,Old,New,RRest). | |
495 | replace_expression(Expr,Old,New,RExpr) :- | |
496 | znamespacet(Expr,Outer,Inner,Names,NOuter,NInner,RExpr),!, | |
497 | replace_expression(Outer,Old,New,NOuter), | |
498 | (member(Old,Names) -> | |
499 | Inner = NInner; | |
500 | replace_expression(Inner,Old,New,NInner)). | |
501 | replace_expression(Expr,Old,New,RExpr) :- | |
502 | zexpr_conversiont(Expr,OldSubs,NewSubs,RExpr), | |
503 | replace_expression(OldSubs,Old,New,NewSubs). | |
504 | ||
505 | ||
506 | simplify_compset(ti(body(Decl,Wheres),OldBodyType),ResultTi,ti(NewBody,NewBodyType)) :- | |
507 | z_counter('cmpset__',Name), Var = name(Name,''), | |
508 | ti_type(ResultTi,Type), | |
509 | ||
510 | NewBodyType = set(schema([field(Var,Type)])), | |
511 | ||
512 | NewBody = body([ti(decl([Var],ti(basetype(set(Type)),set(Type))),none)], | |
513 | [ti(exists(ti(body(Decl,[]),OldBodyType), Condition),bool)]), | |
514 | ||
515 | z_conjunctiont([ti(equal(ti(ref(Var,[]),Type),ResultTi),bool)|Wheres],Condition). | |
516 | ||
517 | all_basetypes([ti(basetype(set(T)),_)],[T]). | |
518 | all_basetypes([ti(basetype(set(A)),_),B|Rest], [A|TRest]) :- | |
519 | all_basetypes([B|Rest],TRest). | |
520 | ||
521 | %******************************************************************************* | |
522 | % Remove abbreviations | |
523 | ||
524 | removeabbreviations(In,Out) :- | |
525 | findeqeq(In,NonEqeqs,EqEqs), | |
526 | (EqEqs = [] -> | |
527 | In = Out ; | |
528 | removeabbr2(NonEqeqs,EqEqs,Out)). | |
529 | ||
530 | findeqeq([],[],[]). | |
531 | findeqeq([S|Rest],NonEqeqs,Eqeqs) :- | |
532 | (S=eqeq(_,_) -> | |
533 | (NonEqeqs,Eqeqs) = (NeRest,[S|EqRest]); | |
534 | (NonEqeqs,Eqeqs) = ([S|NeRest],EqRest)), | |
535 | findeqeq(Rest,NeRest,EqRest). | |
536 | ||
537 | removeabbr2([],_,[]) :- !. | |
538 | removeabbr2([Expr|ERest],Eqeqs,[Result|RRest]) :- | |
539 | !,removeabbr2(Expr,Eqeqs,Result), | |
540 | removeabbr2(ERest,Eqeqs,RRest). | |
541 | removeabbr2(ref(Name,Values),Eqeqs,Result) :- | |
542 | member(eqeq(lhs(Name,Params),EqExpr),Eqeqs), | |
543 | !,insert_parameter(EqExpr,Params,Values,Result1), | |
544 | % If the inserted expression has the form body(_,_), it | |
545 | % is an schema expression and will be marked with sexpr. | |
546 | (EqExpr = body(_,_) -> | |
547 | Result2 = sexpr(EqExpr); | |
548 | Result2 = Result1), | |
549 | % Check if the inserted expression makes use of another abbreviation. | |
550 | removeabbr2(Result2,Eqeqs,Result). | |
551 | removeabbr2(Expr,Eqeqs,Result) :- | |
552 | zexpr_conversion(Expr,Old,New,Result), | |
553 | removeabbr2(Old,Eqeqs,New). | |
554 | ||
555 | %******************************************************************************* | |
556 | % replace references to schemas with SEXPR(sref(...)) | |
557 | ||
558 | clearsrefs(In,Out) :- | |
559 | findschemas(In,Schemas), | |
560 | clearsrefs2(In,Schemas,Out). | |
561 | clearsrefs2([],_,[]) :- !. | |
562 | clearsrefs2([Expr|Rest],Schemas,[CExpr|CRest]) :- | |
563 | !, clearsrefs2(Expr,Schemas,CExpr), | |
564 | clearsrefs2(Rest,Schemas,CRest). | |
565 | clearsrefs2(ref(name(Name,Deco),Params),Schemas,sexpr(sref(Name,Deco,Params,[]))) :- | |
566 | member(Name,Schemas),!. | |
567 | clearsrefs2(Expr,Schemas,CExpr) :- | |
568 | zexpr_conversion(Expr,Old,New,CExpr), | |
569 | clearsrefs2(Old,Schemas,New). | |
570 | ||
571 | findschemas([],[]). | |
572 | findschemas([D|Rest],Schemas) :- | |
573 | (findschema(D,Name) -> | |
574 | Schemas = [Name|SRest]; | |
575 | Schemas = SRest), | |
576 | findschemas(Rest,SRest). | |
577 | findschema(sdef(shead(Name,[]),_),Name). | |
578 | findschema(defeq(shead(Name,[]),_),Name). | |
579 | ||
580 | ||
581 | %******************************************************************************* | |
582 | % Remove schema expressions | |
583 | ||
584 | removesexpr(In,Out) :- removesexpr2(In,Out). | |
585 | ||
586 | removesexpr2([],[]) :- !. | |
587 | removesexpr2([Expr|Rest],[RExpr|RRest]) :- | |
588 | !,removesexpr2(Expr,RExpr), | |
589 | removesexpr2(Rest,RRest). | |
590 | removesexpr2(ti(sexpr(SexprTi),SType),ti(comp(Body,ti(nothing,none)),SType)) :- | |
591 | !, | |
592 | SType = set(Type),Type=schema(Fields), | |
593 | z_counter('rec__',Name),Var = name(Name,''), | |
594 | ||
595 | Body = ti(body([Decl],NewWheres),set(schema([field(Var,Type)]))), | |
596 | Decl = ti(decl([Var],ti(basetype(SType),SType)),none), | |
597 | removesexpr2(SexprTi,ti(body(_,Wheres),_)), | |
598 | insert_selects(Wheres,ti(ref(Var,[]),Type),Fields,NewWheres). | |
599 | ||
600 | removesexpr2(Expr,Result) :- | |
601 | zexpr_conversiont(Expr,OldSubs,NewSubs,Result), | |
602 | removesexpr2(OldSubs,NewSubs). | |
603 | ||
604 | % replaces occurences of the given field names by record selects. | |
605 | insert_selects([],_,_,[]) :- !. | |
606 | insert_selects([Expr|Rest],Var,Fields,[IExpr|IRest]) :- | |
607 | !,insert_selects(Expr,Var,Fields,IExpr), | |
608 | insert_selects(Rest,Var,Fields,IRest). | |
609 | insert_selects(ti(ref(Name,[]),Type),Var,Fields,ti(select(Var,Name),Type)) :- | |
610 | member(field(Name,_),Fields),!. | |
611 | insert_selects(Expr,Var,Fields,Result) :- | |
612 | znamespacet(Expr,Outer,Inner,Names,NOuter,NInner,Result), | |
613 | !,insert_selects(Outer,Var,Fields,NOuter), | |
614 | remove_fields_by_name(Fields,Names,NewFields), | |
615 | insert_selects(Inner,Var,NewFields,NInner). | |
616 | insert_selects(Expr,Var,Fields,Result) :- | |
617 | zexpr_conversiont(Expr,OldSubs,NewSubs,Result), | |
618 | insert_selects(OldSubs,Var,Fields,NewSubs). | |
619 | ||
620 | % create if-then-else for counting bag elements | |
621 | create_bag_count(Bag,RefParam,if(If,Then,Else)) :- | |
622 | make_z_member(RefParam,BagDom,If), | |
623 | make_z_domain(Bag,BagDom), | |
624 | make_z_expr(apply(Bag,RefParam),num,Then), | |
625 | make_z_number(0,Else). | |
626 | ||
627 | create_bag_otimes(Factor,Bag,comp(Body,Just)) :- | |
628 | ti_type(Bag,BagType), BagType = set(tuple([Type,num])), | |
629 | make_z_expr(just(Expr),BagType,Just), | |
630 | unique_reference('i__',num,Iname,I), | |
631 | unique_reference('e__',Type,Ename,E), | |
632 | create_typed_body([Ename,Iname],[Type,num],[Where],Body), | |
633 | make_z_member(Pair,Bag,Where), | |
634 | make_z_tuple([E,I],[Type,num],Pair), | |
635 | make_z_tuple([E,Mult],[Type,num],Expr), | |
636 | make_z_inop('*',num,Factor,I,Mult). | |
637 | ||
638 | create_bag_plus(BagA,BagB,comp(Body,Just)) :- | |
639 | ti_type(BagA,BagType), BagType = set(tuple([Type,num])), | |
640 | make_z_expr(just(Expr),BagType,Just), | |
641 | unique_reference('e__',Type,Ename,E), | |
642 | create_typed_body([Ename],[Type],[Where],Body), | |
643 | make_z_member(E,DomUnion,Where), | |
644 | make_z_inop('\\cup',set(Type),DomA,DomB,DomUnion), | |
645 | make_z_domain(BagA,DomA), make_z_domain(BagB,DomB), | |
646 | make_z_inop('+',num,CountA,CountB,Sum), | |
647 | make_z_bag_count(BagA,E,CountA), make_z_bag_count(BagB,E,CountB), | |
648 | make_z_tuple([E,Sum],[Type,num],Expr). | |
649 | ||
650 | create_bag_minus(Bag,NegBag,comp(Body,Just)) :- | |
651 | ti_type(Bag,BagType), BagType = set(tuple([Type,num])), | |
652 | make_z_expr(just(Expr),BagType,Just), | |
653 | unique_reference('i__',num,Iname,I), | |
654 | unique_reference('e__',Type,Ename,E), | |
655 | unique_reference('d__',num,Dname,D), | |
656 | create_typed_body([Ename,Iname,Dname],[Type,num,num],[Membership,Equal,Pos],Body), | |
657 | make_z_member(Pair,Bag,Membership), | |
658 | make_z_tuple([E,I],[Type,num],Pair), | |
659 | make_z_tuple([E,D],[Type,num],Expr), | |
660 | make_z_expr(equal(D,Diff),bool,Equal), | |
661 | make_z_inrel('<',Zero,D,Pos), | |
662 | make_z_number(0,Zero), | |
663 | make_z_inop('-',num,I,Count,Diff), | |
664 | make_z_bag_count(NegBag,E,Count). | |
665 | ||
666 | create_subbag(BagA,BagB,forall(Body,Pred)) :- | |
667 | ti_type(BagA,BagType), BagType = set(tuple([Type,num])), | |
668 | unique_reference('i__',num,Iname,I), | |
669 | unique_reference('e__',Type,Ename,E), | |
670 | create_typed_body([Ename,Iname],[Type,num],[Membership],Body), | |
671 | make_z_member(Pair,BagA,Membership), | |
672 | make_z_tuple([E,I],[Type,num],Pair), | |
673 | make_z_domain(BagB,DomainB), | |
674 | make_z_member(E,DomainB,CheckMember), | |
675 | make_z_expr(apply(BagB,E),num,CountB), | |
676 | make_z_inrel('\\leq',I,CountB,LessEqual), | |
677 | make_z_expr(and(CheckMember,LessEqual),bool,Pred). | |
678 | ||
679 | create_typed_body(Params,Types,Wheres,Body) :- | |
680 | ti_expr(Body,body(Decls,Wheres)), ti_type(Body,set(schema(Fields))), | |
681 | create_typed_decl_fields(Params,Types,Decls,Fields). | |
682 | create_typed_decl_fields([],[],[],[]). | |
683 | create_typed_decl_fields([N|Nrest],[Type|Trest],[D|Drest],[field(N,Type)|Frest]) :- | |
684 | ti_expr(D,decl([N],Basetype)), ti_type(D,none), | |
685 | ti_expr(Basetype,basetype(set(Type))), ti_type(Basetype,set(Type)), | |
686 | create_typed_decl_fields(Nrest,Trest,Drest,Frest). | |
687 | ||
688 | unique_reference(Prefix,Type,Name,Reference) :- | |
689 | z_counter(Prefix,Id),Name=name(Id,''), | |
690 | make_z_expr(ref(Name,[]),Type,Reference). | |
691 | ||
692 | make_z_domain(Relation,Domain) :- | |
693 | ti_type(Relation,RelType), | |
694 | RelType = set(tuple([A,_])), | |
695 | make_z_expr(apply(DomOp,Relation),set(A),Domain), | |
696 | make_z_expr(ref(name('\\dom',''),[]),set(tuple([RelType,set(A)])),DomOp). | |
697 | ||
698 | make_z_bag_count(Bag,Element,Count) :- | |
699 | make_z_inop('\\bcount',num,Bag,Element,Count). | |
700 | ||
701 | make_z_member(Elem,Set,Member) :- | |
702 | make_z_expr(member(Elem,Set),bool,Member). | |
703 | ||
704 | make_z_tuple(Elements,Types,Expr) :- | |
705 | make_z_expr(tuple(Elements),tuple(Types),Expr). | |
706 | ||
707 | make_z_inop(Op,Type,A,B,Expr) :- | |
708 | make_z_expr(inop(name(Op,''),A,B),Type,Expr). | |
709 | ||
710 | make_z_inrel(Op,A,B,Expr) :- | |
711 | make_z_expr(inrel(name(Op,''),A,B),bool,Expr). | |
712 | ||
713 | make_z_number(Number,Expr) :- | |
714 | make_z_expr(number(Number),num,Expr). | |
715 | ||
716 | make_z_expr(Expr,Type,Z) :- | |
717 | ti_expr(Z,Expr), ti_type(Z,Type). |