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