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