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