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(z_tools,
6 [decorate_vars/3,
7 find_unchanged/3,
8 vars_of_decl/2,
9 z_conjunction/2,
10 z_conjunctiont/2,
11 z_disjunction/2,
12 z_counter/2,
13 z_translate_identifier/2,
14 z_translate_identifiers/2,
15 z_translate_typed_identifiers/4,
16 z_translate_typed_identifier/4,
17 z_translate_identifier_list/2,
18 append_not_duplicate/3,
19 create_z_let/6]).
20
21 :- use_module(library(lists)).
22
23 :- use_module(probsrc(tools)).
24 :- use_module(probsrc(self_check)).
25 :- use_module(probsrc(bsyntaxtree)).
26 :- use_module(probsrc(error_manager),[add_warning/3]).
27
28 :- use_module(probsrc(module_information)).
29 :- module_info(group,proz).
30 :- module_info(description,'This module provides several helper predicates for ProZ.').
31
32
33 %*******************************************************************************
34 % translates an Z identifier of the form "name(Name,Appendix)" to a B identifier
35 z_translate_identifier(name(ZName,Deco), BName) :-
36 atom_concat(ZName, Deco, BName).
37 z_translate_identifiers([],[]).
38 z_translate_identifiers([ZName|ZRest],[BName|BRest]) :-
39 z_translate_identifier(ZName,BName),
40 z_translate_identifiers(ZRest,BRest).
41
42 z_translate_identifier_list([],[]).
43 z_translate_identifier_list([ZName|ZRest],['Identifier'(BName)|BRest]) :-
44 z_translate_identifier(ZName,BName),
45 z_translate_identifier_list(ZRest,BRest).
46
47
48 z_translate_typed_identifier(name(ZName,Deco),Type,Infos,TExpr) :-
49 ajoin([ZName,Deco],Id),
50 create_texpr(identifier(Id),Type,[zname(ZName,Deco)|Infos],TExpr).
51
52 z_translate_typed_identifiers([],[],_,[]).
53 z_translate_typed_identifiers([ZName|Zrest],[Type|Trest],Infos,[TExpr|Brest]) :-
54 z_translate_typed_identifier(ZName,Type,Infos,TExpr),
55 z_translate_typed_identifiers(Zrest,Trest,Infos,Brest).
56
57 %*******************************************************************************
58 % Returns a term with a unique number appended
59 :- dynamic z_counter_db/1.
60 z_counter_db(1).
61
62 z_counter(Name,NewName) :-
63 retract(z_counter_db(C)),
64 C1 is C + 1,
65 assert(z_counter_db(C1)),
66 atom_codes(Name,NC), number_codes(C,CC),
67 append(NC,CC,NewC),
68 atom_codes(NewName,NewC).
69
70
71 %*******************************************************************************
72 % returns the list of variables that are declarated
73 vars_of_decl(Decls,Vars) :-
74 findall(V,
75 (member(decl(Vars,_Type),Decls),member(V,Vars)),
76 Vars).
77
78
79 %*******************************************************************************
80 % appends a list to another while ignoring duplicate entries
81 append_not_duplicate(A,B,Result) :-
82 remove_all(B,A,D),
83 append(A,D,Result).
84
85
86 %*******************************************************************************
87 % decorates variables
88 decorate_vars(In,Deco,Out) :- (Deco = '' -> In=Out ; decorate_vars2(In,Deco,Out)).
89 decorate_vars2([],_,[]).
90 decorate_vars2([name(Name,D1)|Rest],Deco,[name(Name,D2)|DRest]) :-
91 atom_concat(D1,Deco,D2),
92 decorate_vars2(Rest,Deco,DRest).
93
94
95 %********************************************************************************
96 % find unchanged variables
97
98 find_unchanged(ti(body(Decls,Where),Type),UnchangedVars,ti(body(Decls,RestWhere),Type)) :-
99 find_unchanged2(Where,UnchangedVars,RestWhere).
100 find_unchanged2([],[],[]) :- !.
101 find_unchanged2([ti(equal(ti(ref(name(Name,DecoA),[]),_),
102 ti(ref(name(Name,DecoB),[]),_)),bool)|ExprRest],
103 [name(Name,'')|UnchangedRest],Rest) :-
104 ( (DecoA = '', DecoB = '\'') % TODO: Use library(lists)
105 ; (DecoA = '\'', DecoB = '')),!,
106 find_unchanged2(ExprRest,UnchangedRest,Rest).
107 find_unchanged2([Pred|Rest],Unchanged,[Pred|FRest]) :- find_unchanged2(Rest,Unchanged,FRest).
108
109
110 %*******************************************************************************
111 % build the conjunction/disjunction of a list of predicates
112 % the result is a single predicate
113
114 z_conjunction(List,Result) :- lcombine(List,and,truth,Result).
115 z_disjunction(List,Result) :- lcombine(List,or,falsity,Result).
116
117 lcombine(List,Op,Neutral,Result) :-
118 lcombine2(List,Op,Neutral,Neutral,Result).
119 lcombine2([],_,_,Result,Result).
120 lcombine2([A|Rest],Op,Neutral,Acc,Result) :-
121 lcombine3(Acc,A,Op,Neutral,Inter),
122 lcombine2(Rest,Op,Neutral,Inter,Result).
123 lcombine3(Neutral,B,_,Neutral,B) :- !.
124 lcombine3(A,Neutral,_,Neutral,A) :- !.
125 lcombine3(A,B,Op,_,Result) :- Result =.. [Op,A,B].
126
127
128 z_conjunctiont(List,Result) :-
129 z_conjunctiont2(List,ti(truth,bool),Result).
130 z_conjunctiont2([],Result,Result).
131 z_conjunctiont2([A|Rest],Acc,Result) :-
132 z_conjunctiont3(Acc,A,Inter),
133 z_conjunctiont2(Rest,Inter,Result).
134 z_conjunctiont3(ti(truth,bool),B,B) :- !.
135 z_conjunctiont3(A,ti(truth,bool),A) :- !.
136 z_conjunctiont3(A,B,ti(and(A,B),bool)).
137
138
139 % ****************************************************
140
141
142
143 % create Z-style let; see page 59 of Spivey, identifiers are not in scope for Value expressions
144 create_z_let(ExPr,Ids,Values,Inner1,Infos,Result) :-
145 remove_unused_identifiers(Ids,Values,Inner1,RIds0,RValues0),
146 remove_unnecessary_lets(RIds0,RValues0,RIds1,RValues),
147 ( RIds1=[] -> Result = Inner1
148 ;
149 find_identifier_uses_l(RValues,[],RVars),
150 gen_fresh_typed_params(RIds1,Inner1,RVars,RIds,Inner),
151 (ExPr=expr ->
152 get_texpr_type(Inner,Type),
153 create_texpr(let_expression(RIds,RValues,Inner),Type,Infos,Result)
154 ; ExPr=pred ->
155 create_texpr(let_predicate(RIds,RValues,Inner),pred,Infos,Result)
156 ),
157 % extra check: but gen_fresh_typed_params should ensure everything ok
158 get_texpr_ids(RIds,S1), sort(S1,SortedIDs),
159 (ord_intersection(SortedIDs,RVars,Clash), Clash \= []
160 -> add_warning(create_let,'Variable clash in generated let:',Clash)
161 % can cause problems if we use let_predicate/let_expression which allows introducing multiple, dependent ids
162 ; true)
163 ).
164
165 :- use_module(library(lists)).
166 :- use_module(library(ordsets)).
167
168 %% rename parameters and direct definition body to use fresh ids
169 %% reason is that otherwise we repeatedly introduce the same variable and obtain nested lets with variable clashes
170 %% i.e., we may get lets of the form LET a ... LET a,b BE a=(a) & b=(a) ... where (a) is the outer value of a
171 %% Note: however, performance of test 1657 suffers if we systematically rename (hence we only rename VarsToAvoid)
172 gen_fresh_typed_params(TParams,TBody,VarsToAvoid,NewTParams,NewTBody) :-
173 maplist(alpha_typed_id_rename(VarsToAvoid),TParams,NewTParams,RenameList),
174 rename_bt(TBody,RenameList,NewTBody).
175
176 :- use_module(probsrc(gensym),[gensym/2]).
177 alpha_typed_id_rename(VarsToAvoid,b(identifier(OldID),T,I),b(identifier(FreshID),T,I),rename(OldID,FreshID)) :-
178 (ord_member(OldID,VarsToAvoid) -> gensym(OldID,FreshID) ; FreshID=OldID).
179
180 remove_unused_identifiers(TLetIds1,TLetValues1,TDef,TLetIds,TLetValues) :-
181 find_identifier_uses(TDef,[],UsedIds),
182 maplist(combine_with_minus,TLetIds1,TLetValues1,IdValuePairs),
183 include(id_is_used(UsedIds),IdValuePairs,NewIdValuePairs),
184 maplist(combine_with_minus,TLetIds,TLetValues,NewIdValuePairs).
185
186 % remove let a=a, ...
187 remove_unnecessary_lets([],[],[],[]).
188 remove_unnecessary_lets([TID|T1],[TRHS|T2],IDS,RHSS) :-
189 (unnecessary_let(TID,TRHS)
190 -> remove_unnecessary_lets(T1,T2,IDS,RHSS)
191 ; IDS=[TID|TIDS], RHSS = [TRHS|TRHSS], remove_unnecessary_lets(T1,T2,TIDS,TRHSS)
192 ).
193 unnecessary_let(b(identifier(ID),T,_),b(identifier(ID),T,_)).
194 combine_with_minus(A,B,A-B).
195 id_is_used(UsedIds,TId-_Value) :-
196 get_texpr_id(TId,Id),memberchk(Id,UsedIds).