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(schemaexpansion,[sexpansion/2,rename_variables/3]).
6
7		:- use_module(library(lists)).
8
9		:- use_module(probsrc(tools)).
10
11		:- use_module(prozsrc(subexpressions)).
12		:- use_module(prozsrc(z_tools)).
13		:- use_module(prozsrc(schemavars)).
14		:- use_module(prozsrc(zenvironment)).
15		:- use_module(prozsrc(zparameters)).
16
17		:- use_module(probsrc(module_information)).
18		:- module_info(group,proz).
19		:- module_info(description,'This module includes code for expanding Z schemas, i.e. removing references to other schemas by their content and evaluating schema calculus expressions').
20
21		sexpansion(In,Out) :-
22		create_initial_zenvironment(In,Env),
23		add_simple_types_info(Env,SEnv),
24		sexpansion(In,SEnv,Out).
25
26		sexpansion([],_,[]) :- !.
27		sexpansion([E|Rest],Env,[Exp|ERest]) :-
28		!,sexpansion(E,Env,Exp),
29		sexpansion(Rest,Env,ERest).
30
31		sexpansion(sref(Name,Deco,ParamValues,Renamings),Env,Result) :-
32		!,
33		lookup(Env,Name,Params,Expr),
34		sexpansion(Expr,Env,Expansion),
35		same_length(ParamValues,Params),
36		insert_parameter(Expansion,Params,ParamValues,PExp),
37		decorate(PExp,Deco,DExp),
38		rename_variables(DExp,Renamings,Result).
39		sexpansion(body(Decls,Where),Env,body(EDecl,EWhere)) :-
40		!,expand_decls(Decls,Env,ExpandedDeclsD,NWhere),
41		clean_decl(ExpandedDeclsD,EDecl),
42		append(NWhere,ExWhere,DWhere),
43		sexpansion(Where,Env,ExWhere),
44		clean_where(DWhere,EWhere).
45		sexpansion(text(S),Env,Expansion) :-
46		!,sexpansion(S,Env,Expansion).
47		sexpansion(sand(A,B),Env,Expanded) :-
48		!,sexpansion(body([sdecl(A),sdecl(B)],[]),Env,Expanded).
49		sexpansion(sor(A,B),Env,body(EDecl,EWhere)) :-
50		!,expand_and_split(A,Env,DA,WA),
51		expand_and_split(B,Env,DB,WB),
52		append_decls(DA,DB,EDecl),
53		find_common(WA,WB,UA,UB,Common),
54		z_conjunction(UA,AExpr),
55		z_conjunction(UB,BExpr),
56		z_disjunction([AExpr,BExpr],Or),
57		append(Common,[Or],EWhere).
58		sexpansion(simplies(A,B),Env,Expansion) :-
59		!,sexpansion_logic(implies,A,B,Env,Expansion).
60		sexpansion(sequiv(A,B),Env,Expansion) :-
61		!,sexpansion_logic(equiv,A,B,Env,Expansion).
62		sexpansion(snot(S),Env,body(Decls,[not(Condition)])) :-
63		!,expand_and_split(S,Env,Decls,Where),
64		z_conjunction(Where,Condition).
65
66		sexpansion(sforall(Body,S),Env,Expansion) :-
67		!,sexpansion_quantifier(forall,Body,S,Env,Expansion).
68		sexpansion(sexists(Body,S),Env,Expansion) :-
69		!,sexpansion_quantifier(exists,Body,S,Env,Expansion).
70		sexpansion(sexists1(Body,S),Env,Expansion) :-
71		!,sexpansion_quantifier(exists1,Body,S,Env,Expansion).
72
73		sexpansion(pre(S),Env,Expansion) :-
74		!,sexpansion(S,Env,SE),zsplit(SE,Decls,_),
75		find_vars_with_deco(Decls,['\'','!'],PostVars),
76		sexpansion(hide(SE,PostVars),Env,Expansion).
77
78		sexpansion(hide(S,VarsToHide),Env,body(NewDecls,[Exists])) :-
79		!,Exists = exists(body(ExistsDecls,Where),truth),
80		expand_and_split(S,Env,Decls,Where),
81		remove_vars_from_decls(Decls,VarsToHide,NewDecls,ExistsDecls).
82
83		sexpansion(project(A,B),Env,Expansion) :-
84		!,sexpansion(A,Env,AE),sexpansion(B,Env,BE),
85		zsplit(AE,AD,_),zsplit(BE,BD,_),
86		vars_of_decls(AD,VarsA),
87		vars_of_decls(BD,VarsB),
88		remove_all(VarsA,VarsB,VarsToRemove),
89		sexpansion(hide(sand(AE,BE),VarsToRemove),Env,Expansion).
90
91		sexpansion(fatsemi(A,B),Env,Expansion) :-
92		!,combine_schemas(A,B,'\'','',Env,Expansion).
93
94		sexpansion(pipe(A,B),Env,Expansion) :-
95		!,combine_schemas(A,B,'!','?',Env,Expansion).
96
97		sexpansion(spred(S),Env,Expansion) :-
98		!,expand_and_split(S,Env,_,Where),
99		z_conjunction(Where,Expansion).
100
101		sexpansion(comp(Body,nothing),Env,Expansion) :-
102		contains_sdecl(Body),!,
103		add_char_tuple(comp,Body,Env,Expansion).
104
105		sexpansion(mu(Body,nothing),Env,Expansion) :-
106		contains_sdecl(Body),!,
107		add_char_tuple(mu,Body,Env,Expansion).
108
109		sexpansion(lambda(Body,Result),Env,comp(ExpBody,just(Expression))) :-
110		Expression = tuple([Argument,ExpResult]),
111		contains_sdecl(Body),!,
112		sexpansion(Result,Env,ExpResult),
113		sexpansion(comp(Body,nothing),Env,comp(ExpBody,just(Argument))).
114
115		sexpansion(theta(Name,Deco,Renamings),Env,binding(Bindings)) :-
116		!,schema_vars(sref(Name,'',[],[]),Env,Vars),
117		generate_bindings(Vars,Deco,Renamings,Bindings).
118
119		sexpansion(Expr,Env,Expansion) :-
120		zexpr_conversion(Expr,Subs,ESubs,Expansion),
121		sexpansion(Subs,Env,ESubs).
122
123		sexpansion_quantifier(Quantifier,QBody,S,Env,body(NewSDecls,[Quant])) :-
124		functor(Quant,Quantifier,2),
125		arg(1,Quant,body(QDecls,QWhere)), arg(2,Quant,Expr),
126		%Quant =.. [Quantifier,body(QDecls,QWhere),Expr],
127		expand_and_split(QBody,Env,QDecls,QWhere),
128		expand_and_split(S,Env,SDecls,SWhere),
129		vars_of_decls(QDecls,QVars), remove_vars_from_decls(SDecls,QVars,NewSDecls,_),
130		z_conjunction(SWhere,Expr).
131
132		sexpansion_logic(Junctor,A,B,Env,body(Decl,[Condition])) :-
133		expand_and_split(A,Env,DA,WA),
134		expand_and_split(B,Env,DB,WB),
135		append_decls(DA,DB,Decl),
136		z_conjunction(WA,ExprA),
137		z_conjunction(WB,ExprB),
138		Condition =.. [Junctor,ExprA,ExprB].
139
140		expand_and_split(Expr,Env,Decl,Where) :-
141		sexpansion(Expr,Env,Expanded),
142		zsplit(Expanded,Decl,Where).
143		zsplit(body(Decl,Where),Decl,Where).
144
145
146		append_decls(A,B,R) :- append(A,B,M),clean_decl(M,R).
147		%append_where(A,B,R) :- append(A,B,M),clean_where(M,R).
148
149
150		%*******************************************************************************
151		% expand_decls removes all references to other schemas from a declaration
152		expand_decls([],_,[],[]).
153		expand_decls([D|DRest],Env,DExpanded,WExpanded) :-
154		expand_decls2(D,Env,DE,WE),
155		append(DE,DERest,DExpanded),
156		append(WE,WERest,WExpanded),
157		expand_decls(DRest,Env,DERest,WERest).
158		expand_decls2(decl(Vars,Type),Env,[decl(Vars,EType)],Where) :-
159		sexpansion(Type,Env,EType),
160		generate_membership(Vars,EType,Where).
161		expand_decls2(sdecl(S),Env,Decls,Where) :-
162		expand_and_split(S,Env,Decls,Where).
163
164		generate_membership([],_,[]).
165		generate_membership([Var|VRest],Set,[member(ref(Var,[]),Set)|MRest]) :-
166		generate_membership(VRest,Set,MRest).
167
168
169		%*******************************************************************************
170		% clean_decl removes double variable declarations
171		clean_decl(Decls,Cleaned) :-
172		clean_decl2(Decls,[],Cleaned).
173		clean_decl2([],_,[]).
174		clean_decl2([decl(Vars,Type)|Rest],Before,Cleaned) :-
175		filter_vars(Vars,Before,UniqueVars),
176		(UniqueVars = [] ->
177		Cleaned = RestCleaned;
178		Cleaned = [decl(UniqueVars,Type)|RestCleaned]),
179		append(UniqueVars,Before,NBefore),
180		clean_decl2(Rest,NBefore,RestCleaned).
181		filter_vars([],_,[]).
182		filter_vars([Var|Rest],Existing,Result) :-
183		(member(Var,Existing) -> Result = RestResult ; Result = [Var|RestResult]),
184		filter_vars(Rest,Existing,RestResult).
185
186
187		%*******************************************************************************
188		% find all vars with one of the given decorations
189		find_vars_with_deco(Decls,Decos,Postvars) :-
190		findall(name(N,D),
191		(member(decl(Vars,_),Decls),
192		member(name(N,D),Vars),
193		member(D,Decos)),
194		Postvars).
195
196		%*******************************************************************************
197		% combine two schemas: use pairs of matching vars which link both schemas
198		combine_schemas(A,B,DecoOut,DecoIn,Env,Expansion) :-
199		sexpansion(A,Env,AE),sexpansion(B,Env,BE),
200		zsplit(AE,AD,_),zsplit(BE,BD,_),
201
202		find_vars_with_deco(AD,[DecoOut],OutVars),
203		find_vars_with_deco(BD,[DecoIn],InVars),
204		find_matching_vars(OutVars,InVars,DecoOut,DecoIn,RenamingsA,RenamingsB,LocalVars),
205		rename_variables(AE,RenamingsA,AC),
206		rename_variables(BE,RenamingsB,BC),
207		sexpansion(hide(sand(AC,BC),LocalVars),Env,Expansion).
208
209		find_matching_vars([],_,_,_,[],[],[]).
210		find_matching_vars([name(Name,DecoOut)|OutRest],InVars,
211		DecoOut,DecoIn,
212		[rename(New,name(Name,DecoOut))|ARest],
213		[rename(New,name(Name,DecoIn))|BRest],
214		[New|NewRest]) :-
215		member(name(Name,DecoIn),InVars),!,
216		z_counter('match__',NewName),New=name(NewName,''),
217		find_matching_vars(OutRest,InVars,DecoOut,DecoIn,ARest,BRest,NewRest).
218
219		%*******************************************************************************
220		% find_common finds common terms in two lists
221		% find_common(ListA,ListB,UniqueA,UniqueB,Common).
222		find_common(ListA,ListB,UniqueA,UniqueB,Common) :-
223		find_common2(ListA,ListB,ListA,UniqueA,UniqueB,Common).
224		find_common2([A|Rest],ListB,ListA,UniqueA,UniqueB,Common) :-
225		( member(A,ListB) ->
226		(UniqueA = RUniqueA, Common = [A|RCommon])
227		;
228		(UniqueA = [A|RUniqueA], Common = RCommon)),
229		find_common2(Rest,ListB,ListA,RUniqueA,UniqueB,RCommon).
230		find_common2([],ListB,ListA,[],UniqueB,Common) :-
231		find_common3(ListB,ListA,UniqueB,Common).
232		find_common3([B|Rest],ListA,UniqueB,Common) :-
233		( member(B,ListA) ->
234		(UniqueB = RUniqueB, Common = [B|RCommon])
235		;
236		(UniqueB = [B|RUniqueB], Common = RCommon)),
237		find_common3(Rest,ListA,RUniqueB,RCommon).
238		find_common3([],_,[],[]).
239
240		%*******************************************************************************
241		rename_variables(Exprs,[],Exprs) :- !.
242		rename_variables(body(Decls,Where),Renamings,body(RDecls,RWhere)) :-
243		!,
244		rename_decls(Decls,Renamings,RDecls),
245		rename_variables2(Where,Renamings,RWhere).
246		rename_variables(Expr,Renamings,Result) :- rename_variables2(Expr,Renamings,Result).
247
248		rename_variables2([],_,[]) :- !.
249		rename_variables2([E|ERest],Renamings,[P|PRest]) :-
250		!,rename_variables2(E,Renamings,P),
251		rename_variables2(ERest,Renamings,PRest).
252		rename_variables2(ref(Name,P),Renamings,ref(New,P)) :-
253		!,
254		(member(rename(New,Name),Renamings) ->
255		!,true;
256		New = Name).
257		rename_variables2(Expr,Renamings,Result) :-
258		znamespace(Expr,Outer,Inner,Names,NOuter,NInner,Result),
259		!,
260		rename_variables2(Outer,Renamings,NOuter),
261		remove_renamings(Renamings,Names,NRenamings),
262		rename_variables2(Inner,NRenamings,NInner).
263		rename_variables2(Expr,Renamings,Result) :-
264		zexpr_conversion(Expr,Subs,PSubs,Result),
265		rename_variables2(Subs,Renamings,PSubs).
266
267		rename_decls([],_,[]).
268		rename_decls([sdecl(S)|DRest],Renamings,[sdecl(S)|RRest]) :-
269		!,rename_decls(DRest,Renamings,RRest).
270		rename_decls([decl(Vars,Type)|DRest],Renamings,[decl(RVars,Type)|RRest]) :-
271		!,rename_decl_vars(Vars,Renamings,RVars),
272		rename_decls(DRest,Renamings,RRest).
273		rename_decl_vars([],_,[]).
274		rename_decl_vars([Old|ORest],Renamings,[New|NRest]) :-
275		(memberchk(rename(New,Old),Renamings) -> true ; Old = New),
276		rename_decl_vars(ORest,Renamings,NRest).
277
278		remove_renamings([],_,[]).
279		remove_renamings([rename(New,Old)|RRest],Names,Renamings) :-
280		( member(Old,Names) ->
281		Renamings = ORenamings
282		;
283		Renamings = [rename(New,Old)|ORenamings]),
284		remove_renamings(RRest,Names,ORenamings).
285
286		%********************************************************************************
287		% decorates all variables of the given schema by renaming its variables
288		decorate(Expr,'',Expr) :- !.
289		decorate(Expr,Deco,Result) :-
290		zsplit(Expr,Decls,Where),
291		decorate_renamings(Decls,Deco,Renamings),
292		rename_variables(body(Decls,Where),Renamings,Result).
293		decorate_renamings([],_,[]).
294		decorate_renamings([decl(Vars,_)|DRest],Deco,Renamings) :-
295		findall(rename(name(Name,NewDeco),name(Name,OldDeco)),
296		(member(name(Name,OldDeco),Vars),atom_concat(OldDeco,Deco,NewDeco)),
297		LRenamings),
298		append(LRenamings,ORenamings,Renamings),
299		decorate_renamings(DRest,Deco,ORenamings).
300
301		%********************************************************************************
302		% returns all variables of a declaration as a list
303		vars_of_decls(Decls,Vars) :-
304		findall(V,(member(decl(Vs,_),Decls),member(V,Vs)),Vars).
305
306		remove_vars_from_decls([],_,[],[]).
307		remove_vars_from_decls([decl(Vars,Type)|Rest],ToRemove,RestDecls,RemovedDecls) :-
308		split_found_and_rest(Vars,ToRemove,RestVars,RemovedVars),
309		append_nonempty_decl(RestVars,Type,RRestDecls,RestDecls),
310		append_nonempty_decl(RemovedVars,Type,RRemovedDecls,RemovedDecls),
311		remove_vars_from_decls(Rest,ToRemove,RRestDecls,RRemovedDecls).
312		append_nonempty_decl(Vars,Type,Rest,Result) :-
313		(Vars = [] ->
314		Result = Rest;
315		Result = [decl(Vars,Type)|Rest]).
316		split_found_and_rest([],_,[],[]).
317		split_found_and_rest([Var|VRest],ToRemove,RRest,[Var|RRemoved]) :-
318		member(Var,ToRemove),!,
319		split_found_and_rest(VRest,ToRemove,RRest,RRemoved).
320		split_found_and_rest([Var|VRest],ToRemove,[Var|RRest],RRemoved) :-
321		split_found_and_rest(VRest,ToRemove,RRest,RRemoved).
322
323
324
325		%********************************************************************************
326		% generate bindings for a list of given variables
327		generate_bindings([],_,_,[]).
328		generate_bindings([Fieldname|FRest],Deco,Renamings,[bindfield(Fieldname,ref(Refname,[]))|BRest]) :-
329		Fieldname = name(OldName,OldDeco),
330		atom_concat(OldDeco,Deco,NewDeco),
331		(member(rename(Refname,name(OldName,NewDeco)),Renamings) ->
332		!,true;
333		Refname = name(OldName,NewDeco)),
334		generate_bindings(FRest,Deco,Renamings,BRest).
335
336		%********************************************************************************
337
338
339		add_simple_types_info(Env,env(Env,STypes)) :-
340		env_z_defs(Env,Def),
341		findall(Name,(member(given(L),Def),member(Name,L)),Givens),
342		findall(Name,member(namedset(Name,_),Def),Namedsets),
343		append(Givens,Namedsets,STypes).
344
345		lookup(env(Env,_),Name,Params,Expr) :- zlookup_schema(Env,Name,Params,Expr).
346
347		%**********************************************************************
348		% generation of characteristic tuple
349		contains_sdecl(body(Decl,_)) :-
350		contains_sdecl2(Decl).
351		contains_sdecl2([sdecl(_)|_]) :- !.
352		contains_sdecl2([_|R]) :- contains_sdecl(R).
353
354		add_char_tuple(Functor,Body,Env,Result) :-
355		Body=body(Decl,_),
356		characteristic_tuple(Decl,Env,Exprlist),
357		maybetuple(Exprlist,Expression),
358		functor(R,Functor,2),
359		arg(1,R,Body),
360		arg(2,R,just(Expression)),
361		sexpansion(R,Env,Result).
362		characteristic_tuple([],_,[]).
363		characteristic_tuple([D|Rest],Env,Exprlist) :-
364		characteristic_tuple2(D,Env,Exprs),
365		append(Exprs,Restlist,Exprlist),
366		characteristic_tuple(Rest,Env,Restlist).
367		characteristic_tuple2(decl(Vars,_),_,References) :-
368		names_to_references(Vars,References).
369		characteristic_tuple2(sdecl(sref(Name,Deco,Params,Renamings)),Env,[binding(Bindings)]) :-
370		sexpansion(sref(Name,'',Params,[]),Env,body(Decls,_)),
371		vars_of_decls(Decls,Vars),
372		generate_bindings(Vars,Deco,Renamings,Bindings).
373		maybetuple([E],E) :- !.
374		maybetuple([A,B|R],tuple([A,B|R])).
375
376		names_to_references([],[]).
377		names_to_references([Name|Nrest],[ref(Name,[])|Rrest]) :-
378		names_to_references(Nrest,Rrest).