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