1 | % (c) 2009-2013 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(units_domain, [ same_units/1, | |
6 | same_units/2, | |
7 | lub/3, | |
8 | units_domain_multiplication/3, | |
9 | units_domain_multiplication_conversion/3, | |
10 | units_domain_division/3, | |
11 | units_domain_division_conversion/3, | |
12 | units_domain_subtraction_conversion/3, | |
13 | units_domain_addition_conversion/3, | |
14 | units_domain_power_of/3, | |
15 | units_domain_member/2, | |
16 | units_domain_relation/3, | |
17 | involved_in_constraint/1, | |
18 | power_of_multiply_units/3 | |
19 | ]). | |
20 | ||
21 | :- use_module(library(lists)). | |
22 | :- use_module(library(clpfd)). | |
23 | :- use_module(library(sets)). | |
24 | :- use_module(library(atts)). | |
25 | ||
26 | ||
27 | :- use_module(probsrc(self_check)). | |
28 | ||
29 | :- use_module(units_conversions). | |
30 | ||
31 | :- use_module(probsrc(module_information)). | |
32 | :- module_info(group,plugin_units). | |
33 | :- module_info(description,'Units Plugin: The abstract Domain.'). | |
34 | ||
35 | :- attribute mfactors/2, dfactors/2, pfactors/2, constraint/0. | |
36 | ||
37 | involved_in_constraint(X) :- var(X), !, get_atts(X, constraint). | |
38 | involved_in_constraint([H|T]) :- | |
39 | !, (involved_in_constraint(H) ; involved_in_constraint(T)). | |
40 | involved_in_constraint(Pred) :- | |
41 | !, Pred =.. [Head|Tail], | |
42 | Tail = [_|_], | |
43 | (involved_in_constraint(Head) ; involved_in_constraint(Tail)). | |
44 | ||
45 | add_constraint_marker(A,B) :- | |
46 | (var(A) -> put_atts(A, constraint) ; true), | |
47 | (var(B) -> put_atts(B, constraint) ; true). | |
48 | ||
49 | verify_attributes(Var, Value, Goal) :- | |
50 | % the variable might be the result of a multiplication | |
51 | % -> propagate inwards | |
52 | get_atts(Var, mfactors(A,B)), !, | |
53 | (var(Value) -> Goal = [] ; | |
54 | (A==B, var(A)) -> Goal=[power_of_multiply_units(2,A,Value)] ; | |
55 | (var(A), nonvar(B)) -> Goal=[units_domain_division(Value,B,A)] ; | |
56 | (var(B), nonvar(A)) -> Goal=[units_domain_division(Value,A,B)] ; | |
57 | otherwise -> Goal=[]). | |
58 | verify_attributes(Var, Value, Goal) :- | |
59 | % the variable might be the result of a division | |
60 | % -> propagate inwards | |
61 | get_atts(Var, dfactors(A,B)), !, | |
62 | (var(Value) -> Goal=[] ; | |
63 | (var(A), nonvar(B)) -> Goal=[units_domain_multiplication(Value,B,A)] ; | |
64 | (var(B), nonvar(A)) -> Goal=[units_domain_division(A,Value,B)] ; | |
65 | otherwise -> Goal=[]). | |
66 | verify_attributes(Var, Value, Goal) :- | |
67 | % the variable might be the result of a exponentiation | |
68 | % -> propagate inwards | |
69 | get_atts(Var, pfactors(A,B)), !, | |
70 | (var(Value) -> Goal=[] ; | |
71 | (var(A), nonvar(B)) -> Goal=[power_of_multiply_units(B,A,Value)] ; | |
72 | otherwise -> Goal=[]). | |
73 | % rescue constraint attribute when unifying | |
74 | verify_attributes(Var, Value, []) :- | |
75 | get_atts(Var, constraint), !, | |
76 | (var(Value) -> put_atts(Value, constraint) ; true). | |
77 | %verify_attributes(Var, Value, []) :- | |
78 | % not a result of multiplication or division | |
79 | % true. | |
80 | ||
81 | one_is_var(A,B) :- var(A) ; var(B). | |
82 | ||
83 | % special case "power_of": | |
84 | % A is the unit part of an integer. This might be a variable. | |
85 | units_domain_power_of(A,b(integer(B,_,_)),C) :- var(A), put_atts(A,constraint), put_atts(C, pfactors(A,B)), !. | |
86 | % B is a raw syntax element. if it is a known integer literal, compute exponent | |
87 | units_domain_power_of(A, b(integer(X),_,_),C) :- | |
88 | power_of_multiply_units(X,A,C), !. | |
89 | % A might be top containing a list of known units | |
90 | units_domain_power_of(top(A), b(integer(X),_,_),top(C)) :- | |
91 | maplist(power_of_multiply_units(X),A,C), !. | |
92 | % otherwise, we can not infer the unit anymore | |
93 | units_domain_power_of(_A,_B,top([])) :- !. | |
94 | ||
95 | power_of_multiply_units(_,[],[]). | |
96 | power_of_multiply_units(X,[[Factor1,Unit,Pow1]|T1],[[Factor2,Unit,Pow2]|T2]) :- | |
97 | Factor2 #= Factor1 * X, Pow2 #= Pow1 * X, | |
98 | power_of_multiply_units(X,T1,T2). | |
99 | ||
100 | % Conversions between units. Conversion_factor and conversion_add is supplied in its own module. | |
101 | ||
102 | units_domain_addition_conversion(_, X, _) :- var(X), !. | |
103 | units_domain_addition_conversion(b(integer(X),_,_), [Unit|Units], [Unit2|Units]) :- | |
104 | repeat_conversion_add(X,Unit2,Unit). | |
105 | units_domain_addition_conversion(BInt,[Unit|Units],[Unit|Units2]) :- | |
106 | units_domain_addition_conversion(BInt,Units,Units2). | |
107 | ||
108 | units_domain_subtraction_conversion(_, X, _) :- var(X), !. | |
109 | units_domain_subtraction_conversion(b(integer(X),_,_), [Unit|Units], [Unit2|Units]) :- | |
110 | repeat_conversion_add(X,Unit,Unit2). | |
111 | units_domain_subtraction_conversion(BInt,[Unit|Units],[Unit|Units2]) :- | |
112 | units_domain_subtraction_conversion(BInt,Units,Units2). | |
113 | ||
114 | :- assert_must_succeed((units_domain_multiplication_conversion(b(integer(10),_,_), | |
115 | _,X),var(X))). | |
116 | :- assert_must_succeed((units_domain_multiplication_conversion(b(integer(10),_,_), | |
117 | [[1,m,1]],X),X=[[0,m,1]])). | |
118 | :- assert_must_succeed((units_domain_multiplication_conversion(b(integer(60),_,_), | |
119 | [[1,mins,1]],X),X=[[1,s,1]])). | |
120 | :- assert_must_succeed((units_domain_multiplication_conversion(b(integer(10),_,_), | |
121 | [[1,m,1],[1,s,1]],X),X=[[0,m,1],[1,s,1]])). | |
122 | :- assert_must_succeed((units_domain_multiplication_conversion(b(integer(10),_,_), | |
123 | [[1,s,1],[1,m,1]],X),X=[[1,s,1],[0,m,1]])). | |
124 | :- assert_must_succeed((units_domain_multiplication_conversion(b(integer(60),_,_), | |
125 | [[1,m,1],[1,mins,1]],X),X=[[1,m,1],[1,s,1]])). | |
126 | :- assert_must_succeed((units_domain_multiplication_conversion(b(integer(60),_,_), | |
127 | [[1,mins,1],[1,m,1]],X),X=[[1,s,1],[1,m,1]])). | |
128 | units_domain_multiplication_conversion(_, X, _) :- var(X), !. | |
129 | units_domain_multiplication_conversion(b(integer(X),_,_), [Unit|Units], [Unit2|Units]) :- | |
130 | repeat_conversion_factor(X,Unit,Unit2). | |
131 | units_domain_multiplication_conversion(BInt,[Unit|Units],[Unit|Units2]) :- | |
132 | units_domain_multiplication_conversion(BInt,Units,Units2). | |
133 | ||
134 | :- assert_must_succeed((units_domain_division_conversion(b(integer(10),_,_), | |
135 | _,X),var(X))). | |
136 | :- assert_must_succeed((units_domain_division_conversion(b(integer(10),_,_), | |
137 | [[1,m,1]],X),X=[[2,m,1]])). | |
138 | units_domain_division_conversion(_, X, _) :- var(X), !. | |
139 | units_domain_division_conversion(b(integer(X),_,_), [Unit|Units], [Unit2|Units]) :- | |
140 | repeat_conversion_factor(X,Unit2,Unit). | |
141 | units_domain_division_conversion(BInt,[Unit|Units],[Unit|Units2]) :- | |
142 | units_domain_division_conversion(BInt,Units,Units2). | |
143 | ||
144 | repeat_conversion_factor(X,_,_) :- X < 1, !, fail. | |
145 | repeat_conversion_factor(1.0,Unit,Unit). | |
146 | repeat_conversion_factor(Factor,Unit,UnitOut) :- | |
147 | var(UnitOut) | |
148 | -> conversion_factor(Unit2,Factor2,Unit), | |
149 | FactorOut is Factor / Factor2, | |
150 | repeat_conversion_factor(FactorOut,Unit2,UnitOut) | |
151 | ; conversion_factor(UnitOut,Factor2,Unit2), | |
152 | FactorOut is Factor / Factor2, | |
153 | repeat_conversion_factor(FactorOut, Unit, Unit2). | |
154 | ||
155 | repeat_conversion_add(X,_,_) :- X < 0, !, fail. | |
156 | repeat_conversion_add(0,Unit,Unit). | |
157 | repeat_conversion_add(Factor,Unit,UnitOut) :- | |
158 | var(UnitOut) | |
159 | -> conversion_add(Unit2,Factor2,Unit), | |
160 | FactorOut is Factor - Factor2, | |
161 | repeat_conversion_add(FactorOut,Unit2,UnitOut) | |
162 | ; conversion_add(UnitOut,Factor2,Unit2), | |
163 | FactorOut is Factor - Factor2, | |
164 | repeat_conversion_add(FactorOut, Unit, Unit2). | |
165 | ||
166 | ||
167 | % Operations on Integers | |
168 | :- assert_must_succeed(units_domain_multiplication(top([]),[[1,m,1]],top([]))). | |
169 | :- assert_must_succeed(units_domain_multiplication(top([[[1,m,1]],[[2,m,1]]]),[[1,m,1]],top([[[2,m,2]],[[3,m,2]]]))). | |
170 | :- assert_must_succeed(units_domain_multiplication(top([[[1,m,1]],[[2,m,1]]]),top([[[1,m,1]],[[2,m,1]]]), | |
171 | top([[[2,m,2]],[[3,m,2]],[[3,m,2]],[[4,m,2]]]))). | |
172 | :- assert_must_succeed(units_domain_multiplication([[1,m,1]],[[1,m,1]],[[2,m,2]])). | |
173 | :- assert_must_succeed((units_domain_multiplication(A,B,C),var(A),var(B),var(C))). | |
174 | :- assert_must_succeed((units_domain_multiplication(_,[[1,m,1]],Y), var(Y))). | |
175 | :- assert_must_succeed((units_domain_multiplication([[1,m,1]],_,Y), var(Y))). | |
176 | :- assert_must_succeed(units_domain_multiplication([[1,m,1],[1,a,2]],[[1,m,1]],[[2,m,2],[1,a,2]])). | |
177 | :- assert_must_succeed((units_domain_multiplication([[0,m,1],[0,s,-1]],[[0,s,1]],Res), Res = [[0,m,1]])). | |
178 | units_domain_multiplication(A,B,C) :- one_is_var(A,B), !, add_constraint_marker(A,B), put_atts(C, mfactors(A,B)). | |
179 | units_domain_multiplication(top(A),top(B),top(C)) :- !, | |
180 | map_product(units_domain_multiplication,A,B,C). | |
181 | units_domain_multiplication(top(A),B,top(C)) :- !, | |
182 | maplist(units_domain_multiplication(B),A,C). | |
183 | units_domain_multiplication(A,top(B),top(C)) :- !, | |
184 | maplist(units_domain_multiplication(A),B,C). | |
185 | units_domain_multiplication(Op1,[],Op1) :- !. | |
186 | units_domain_multiplication([],Op2,Op2) :- !. | |
187 | units_domain_multiplication([[Factor1,Unit1,Pow1]|Units], UnitsOp2, Res2) :- !, | |
188 | (selectchk([Factor2,Unit1,Pow2],UnitsOp2,UnitsOp22) | |
189 | -> Factor3 is Factor1+Factor2, Pow3 is Pow1+Pow2, | |
190 | Res1 = [Factor3,Unit1,Pow3], units_domain_multiplication(Units,UnitsOp22,UnitsResult) | |
191 | ; Res1 = [Factor1,Unit1,Pow1], units_domain_multiplication(Units,UnitsOp2,UnitsResult) | |
192 | ), | |
193 | (Res1 = [0,_,0] -> Res2 = UnitsResult ; Res2 = [Res1|UnitsResult]). | |
194 | ||
195 | :- assert_must_succeed(units_domain_division(top([]),[[1,m,1]],top([]))). | |
196 | :- assert_must_succeed(units_domain_division([[1,m,1]],top([]),top([]))). | |
197 | :- assert_must_succeed(units_domain_division(top([[[1,m,1],[1,a,2]],[[1,m,1],[2,a,2]]]),[[1,m,1]],top([[[1,a,2]],[[2,a,2]]]))). | |
198 | :- assert_must_succeed(units_domain_division([[1,m,1]],top([[[1,m,2]],[[1,m,3]]]),top([[[0,m,-1]],[[0,m,-2]]]))). | |
199 | :- assert_must_succeed(units_domain_division(top([[[1,m,1]],[[2,m,1]]]),top([[[1,m,2]],[[1,m,3]]]), | |
200 | top([[[0,m,-1]],[[0,m,-2]],[[1,m,-1]],[[1,m,-2]]]))). | |
201 | :- assert_must_succeed(units_domain_division([[1,m,1]],[[1,m,1]],[])). | |
202 | :- assert_must_succeed(units_domain_division([[1,m,1],[1,a,2]],[[1,m,1]],[[1,a,2]])). | |
203 | :- assert_must_succeed(units_domain_division([[1,m,1]],[[1,m,1],[1,a,2]],[[-1,a,-2]])). | |
204 | :- assert_must_succeed((units_domain_division(A,B,C),var(A),var(B),var(C))). | |
205 | :- assert_must_succeed((units_domain_division(A,A,C),var(A),C==[])). | |
206 | :- assert_must_succeed((units_domain_division(_,[[1,m,1]],Y), var(Y))). | |
207 | :- assert_must_succeed((units_domain_division([[1,m,1]],_,Y), var(Y))). | |
208 | :- assert_must_succeed((units_domain_division([[0,m,1],[0,s,1]],[[0,s,1]],Res), Res = [[0,m,1]])). | |
209 | units_domain_division(A,B,C) :- var(A), A==B, !, C=[]. | |
210 | units_domain_division(A,B,C) :- one_is_var(A,B), !, add_constraint_marker(A,B), put_atts(C, dfactors(A,B)). | |
211 | units_domain_division(top(A),top(B),top(C)) :- | |
212 | !, map_product(units_domain_division,A,B,C). | |
213 | units_domain_division(top(A),B,top(C)) :- | |
214 | !, maplist(units_domain_division_reversed_arguments(B),A,C). | |
215 | units_domain_division(A,top(B),top(C)) :- | |
216 | !, maplist(units_domain_division(A),B,C). | |
217 | units_domain_division(Op1,[],Op1) :- !. | |
218 | units_domain_division([],Op2,Op3) :- !, | |
219 | division_reverse_signs(Op2,Op3). | |
220 | units_domain_division([[Factor1,Unit1,Pow1]|Units], UnitsOp2, Res2) :- !, | |
221 | (selectchk([Factor2,Unit1,Pow2],UnitsOp2,UnitsOp22) | |
222 | -> Factor3 is Factor1-Factor2, Pow3 is Pow1-Pow2, | |
223 | Res1 = [Factor3,Unit1,Pow3], units_domain_division(Units,UnitsOp22,UnitsResult) | |
224 | ; Res1 = [Factor1,Unit1,Pow1], units_domain_division(Units,UnitsOp2,UnitsResult) | |
225 | ), | |
226 | (Res1 = [0,_,0] -> Res2 = UnitsResult ; Res2 = [Res1|UnitsResult]). | |
227 | ||
228 | division_reverse_signs([],[]). | |
229 | division_reverse_signs([[Factor,Unit,Pow]|T],[[Factor2,Unit,Pow2]|T2]) :- | |
230 | Factor2 is -Factor, Pow2 is -Pow, | |
231 | division_reverse_signs(T,T2). | |
232 | ||
233 | % reverse argument order - for maplist | |
234 | units_domain_division_reversed_arguments(A,B,C) :- | |
235 | units_domain_division(B,A,C). | |
236 | ||
237 | % Operations on Sets | |
238 | :- assert_must_succeed(units_domain_member(type,set(type))). | |
239 | :- assert_must_fail(units_domain_member(integer([[1,m,1]]), set(integer([[2,m,1]])))). | |
240 | units_domain_member(A,B) :- set(A) = B, !. | |
241 | units_domain_member(rec(FieldsA),set(rec(FieldsB))) :- !, | |
242 | maplist(units_domain_member,FieldsA,FieldsB). | |
243 | units_domain_member(field(Name,A),field(Name,B)) :- !, | |
244 | units_domain_member(A,B). | |
245 | ||
246 | :- assert_must_succeed(units_domain_relation(set(type),set(type2),set(set(couple(type,type2))))). | |
247 | units_domain_relation(set(A),set(B),set(set(couple(A,B)))). | |
248 | ||
249 | ||
250 | ||
251 | % COMPARISON OF UNITS | |
252 | % same_units/1 checks if a list of units are equal | |
253 | % same_units/2 checks if two units are equal | |
254 | % lub/3 infers least upper bound - a common unit higher in the lattice than the first ones | |
255 | ||
256 | % same_units/2 - test cases | |
257 | :- assert_must_fail(same_units(type(_), other_type)). | |
258 | :- assert_must_fail(same_units(type(type2(_)), type(type3(_)))). | |
259 | :- assert_must_succeed(same_units(type([[1,m,1],[1,s,2]]), type([[1,s,2],[1,m,1]]))). | |
260 | :- assert_must_succeed(same_units(type([[-1,m,1],[1,s,2]]), type([[-1,s,2],[1,m,1]]))). | |
261 | :- assert_must_succeed(same_units(type([[2,m,1],[1,s,2]]), type([[2,s,2],[1,m,1]]))). | |
262 | :- assert_must_succeed(same_units(type([[-1,m,1],[0,s,2]]), type([[-2,s,2],[1,m,1]]))). | |
263 | :- assert_must_succeed(same_units(type(top([])), type(top([])))). | |
264 | :- assert_must_succeed(same_units(type(X), type(X))). | |
265 | ||
266 | % lub/3 - test cases | |
267 | :- assert_must_succeed(lub(type([[1,m,1],[1,s,2]]), type([[1,s,2],[1,m,1]]), type([[1,m,1],[1,s,2]]))). | |
268 | :- assert_must_succeed(lub(type([[-1,m,1],[1,s,2]]), type([[-1,s,2],[1,m,1]]), type([[-1,m,1],[1,s,2]]))). | |
269 | :- assert_must_succeed(lub(type(top([])), type([[1,m,1]]), type(top([[[1,m,1]]])))). | |
270 | :- assert_must_succeed(lub(type(top([])), type([[1,s,2],[1,m,1]]), type(top([[[1,s,2],[1,m,1]]])))). | |
271 | :- assert_must_succeed(lub(type([[1,m,1],[5,s,2]]), type(top([[[1,m,1]]])), type(top([[[1,m,1],[5,s,2]],[[1,m,1]]])))). | |
272 | :- assert_must_succeed(lub(type(X), type(X), type(X))). | |
273 | :- assert_must_succeed(lub([[3,m,1]],[[3,m,1],[0,h,-1]],top([[[3,m,1]],[[3,m,1],[0,h,-1]]]))). | |
274 | :- assert_must_succeed(lub(integer(_),integer(top([[[0,m,1]],[[0,m,1],[0,s,-1]],[[0,m,1]]])), | |
275 | integer(top([[[0,m,1]],[[0,m,1],[0,s,-1]],[[0,m,1]]])))). | |
276 | :- assert_must_succeed(lub(integer(top([[[0,m,1]],[[0,m,1],[0,s,-1]],[[0,m,1]]])),integer(_), | |
277 | integer(top([[[0,m,1]],[[0,m,1],[0,s,-1]],[[0,m,1]]])))). | |
278 | :- assert_must_succeed(lub(top([[[0,m,1]],[[0,m,1],[0,s,-1]]]),[[0,m,1],[0,s,-1]], | |
279 | top([[[0,m,1]],[[0,m,1],[0,s,-1]]]))). | |
280 | :- assert_must_succeed(lub([[0,m,1],[0,s,-1]],top([[[0,m,1]],[[0,m,1],[0,s,-1]]]), | |
281 | top([[[0,m,1]],[[0,m,1],[0,s,-1]]]))). | |
282 | :- assert_must_succeed(lub(top([[[0,m,1]],[[0,m,1],[0,s,-1]]]),top([[[0,m,1],[0,s,-1]],[[0,m,1]]]), | |
283 | top([[[0,m,1],[0,s,-1]],[[0,m,1]]]))). | |
284 | ||
285 | same_units([]). | |
286 | same_units([_]). | |
287 | same_units([A,B|T]) :- same_units(A,B), same_units([B|T]). | |
288 | % two units are identical, if the lub is again one of the two units | |
289 | same_units(A,B) :- lub(A,B,C), !, (A=C ; B=C). | |
290 | ||
291 | % lub/3 - implementation | |
292 | lub(A,B,C) :- A=B, !, B=C. | |
293 | lub(A,B,C) :- lub_domain_level(A,B,C), !. | |
294 | lub(top(A),top(B),top(C)) :- | |
295 | !, union(A,B,C). | |
296 | lub(top(A),B,top(C)) :- | |
297 | !, union(A,[B],C). | |
298 | lub(A,top(B),top(C)) :- | |
299 | !, union([A],B,C). | |
300 | lub(A,B,C) :- | |
301 | \+ is_list(A), \+ is_list(B), \+ is_list(C), | |
302 | A =.. [Type|ArgsA], | |
303 | B =.. [Type|ArgsB], | |
304 | lub_list(ArgsA,ArgsB,ArgsC), !, | |
305 | C =.. [Type|ArgsC]. | |
306 | lub(A,B,top([A,B])) :- !. | |
307 | ||
308 | lub_list([],[],[]). | |
309 | lub_list([H1|T1],[H2|T2],[H3|T3]) :- | |
310 | lub(H1,H2,H3), !, | |
311 | lub_list(T1,T2,T3). | |
312 | ||
313 | lub_domain_level(U1,U2,U3) :- | |
314 | check_factor(U1,U2,0,0), | |
315 | lub_domain_level2(U1,U2,U3). | |
316 | ||
317 | lub_domain_level2([],[],[]) :- !. | |
318 | lub_domain_level2([[Factor1,Unit1,Pow1]|Units], UnitsOp2,[[Factor1,Unit1,Pow1]|ResUnits]) :- | |
319 | selectchk([_Factor1,Unit1,Pow1],UnitsOp2,UnitsOp22), !, | |
320 | lub_domain_level2(Units,UnitsOp22,ResUnits). | |
321 | ||
322 | check_factor([],[],X,X). | |
323 | check_factor([[Factor1,_,_]|T1], [[Factor2,_,_]|T2],X,Y) :- | |
324 | !, X2 is X + Factor1, Y2 is Y + Factor2, check_factor(T1,T2,X2,Y2). |