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