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). |