units_domain

add_constraint_marker(A,B) :-
    (var(A) -> put_atts(A, constraint) ; true),
    (var(B) -> put_atts(B, constraint) ; true).

check_factor([],[],X,X).

check_factor([[Factor1,_,_]|T1], [[Factor2,_,_]|T2],X,Y) :-
    !, X2 is X + Factor1, Y2 is Y + Factor2, check_factor(T1,T2,X2,Y2).

division_reverse_signs([],[]).

division_reverse_signs([[Factor,Unit,Pow]|T],[[Factor2,Unit,Pow2]|T2]) :-
    Factor2 is -Factor, Pow2 is -Pow,
    division_reverse_signs(T,T2).

involved_in_constraint(X) :- var(X), !, get_atts(X, constraint).

involved_in_constraint([H|T]) :-
    !, (involved_in_constraint(H) ; involved_in_constraint(T)).

involved_in_constraint(Pred) :-
    !, Pred =.. [Head|Tail],
    Tail = [_|_],
    (involved_in_constraint(Head) ; involved_in_constraint(Tail)).

lub(A,B,C) :- A=B, !, B=C.

lub(A,B,C) :- lub_domain_level(A,B,C), !.

lub(top(A),top(B),top(C)) :-
    !, union(A,B,C).

lub(top(A),B,top(C)) :-
    !, union(A,[B],C).

lub(A,top(B),top(C)) :-
    !, union([A],B,C).

lub(A,B,C) :-
    \+ is_list(A), \+ is_list(B), \+ is_list(C),
    A =.. [Type|ArgsA],
    B =.. [Type|ArgsB],
    lub_list(ArgsA,ArgsB,ArgsC), !,
    C =.. [Type|ArgsC].

lub(A,B,top([A,B])) :- !.

lub_domain_level(U1,U2,U3) :-
    check_factor(U1,U2,0,0),
    lub_domain_level2(U1,U2,U3).

lub_domain_level2([],[],[]) :- !.

lub_domain_level2([[Factor1,Unit1,Pow1]|Units], UnitsOp2,[[Factor1,Unit1,Pow1]|ResUnits]) :-
    selectchk([_Factor1,Unit1,Pow1],UnitsOp2,UnitsOp22), !,
    lub_domain_level2(Units,UnitsOp22,ResUnits).

lub_list([],[],[]).

lub_list([H1|T1],[H2|T2],[H3|T3]) :-
    lub(H1,H2,H3), !,
    lub_list(T1,T2,T3).

one_is_var(A,B) :- var(A) ; var(B).

power_of_multiply_units(_,[],[]).

repeat_conversion_add(X,_,_) :- X < 0, !, fail.

repeat_conversion_add(0,Unit,Unit).

repeat_conversion_add(Factor,Unit,UnitOut) :-
    var(UnitOut)
    -> conversion_add(Unit2,Factor2,Unit),
    FactorOut is Factor - Factor2,
    repeat_conversion_add(FactorOut,Unit2,UnitOut)
    ; conversion_add(UnitOut,Factor2,Unit2),
    FactorOut is Factor - Factor2,
    repeat_conversion_add(FactorOut, Unit, Unit2).

repeat_conversion_factor(X,_,_) :- X < 1, !, fail.

repeat_conversion_factor(1.0,Unit,Unit).

repeat_conversion_factor(Factor,Unit,UnitOut) :-
    var(UnitOut)
    -> conversion_factor(Unit2,Factor2,Unit),
    FactorOut is Factor / Factor2,
    repeat_conversion_factor(FactorOut,Unit2,UnitOut)
    ; conversion_factor(UnitOut,Factor2,Unit2),
    FactorOut is Factor / Factor2,
    repeat_conversion_factor(FactorOut, Unit, Unit2).

same_units([]).

same_units([_]).

same_units([A,B|T]) :- same_units(A,B), same_units([B|T]).

same_units(A,B) :- lub(A,B,C), !, (A=C ; B=C).

units_domain_addition_conversion(_, X, _) :- var(X), !.

units_domain_addition_conversion(b(integer(X),_,_), [Unit|Units], [Unit2|Units]) :-
    repeat_conversion_add(X,Unit2,Unit).

units_domain_addition_conversion(BInt,[Unit|Units],[Unit|Units2]) :-
    units_domain_addition_conversion(BInt,Units,Units2).

units_domain_division(A,B,C) :- var(A), A==B, !, C=[].

units_domain_division(A,B,C) :- one_is_var(A,B), !, add_constraint_marker(A,B), put_atts(C, dfactors(A,B)).

units_domain_division(top(A),top(B),top(C)) :-
    !, map_product(units_domain_division,A,B,C).

units_domain_division(top(A),B,top(C)) :-
    !, maplist(units_domain_division_reversed_arguments(B),A,C).

units_domain_division(A,top(B),top(C)) :-
    !, maplist(units_domain_division(A),B,C).

units_domain_division(Op1,[],Op1) :- !.

units_domain_division([],Op2,Op3) :- !,
    division_reverse_signs(Op2,Op3).

units_domain_division([[Factor1,Unit1,Pow1]|Units], UnitsOp2, Res2) :- !,
    (selectchk([Factor2,Unit1,Pow2],UnitsOp2,UnitsOp22)
    -> Factor3 is Factor1-Factor2, Pow3 is Pow1-Pow2,
    Res1 = [Factor3,Unit1,Pow3], units_domain_division(Units,UnitsOp22,UnitsResult)
    ; Res1 = [Factor1,Unit1,Pow1], units_domain_division(Units,UnitsOp2,UnitsResult)
    ),
    (Res1 = [0,_,0] -> Res2 = UnitsResult ; Res2 = [Res1|UnitsResult]).

units_domain_division_conversion(_, X, _) :- var(X), !.

units_domain_division_conversion(b(integer(X),_,_), [Unit|Units], [Unit2|Units]) :-
    repeat_conversion_factor(X,Unit2,Unit).

units_domain_division_conversion(BInt,[Unit|Units],[Unit|Units2]) :-
    units_domain_division_conversion(BInt,Units,Units2).

units_domain_division_reversed_arguments(A,B,C) :-
    units_domain_division(B,A,C).

units_domain_member(A,B) :- set(A) = B, !.

units_domain_member(rec(FieldsA),set(rec(FieldsB))) :- !,
    maplist(units_domain_member,FieldsA,FieldsB).

units_domain_member(field(Name,A),field(Name,B)) :- !,
    units_domain_member(A,B).

units_domain_multiplication(A,B,C) :- one_is_var(A,B), !, add_constraint_marker(A,B), put_atts(C, mfactors(A,B)).

units_domain_multiplication(top(A),top(B),top(C)) :- !,
    map_product(units_domain_multiplication,A,B,C).

units_domain_multiplication(top(A),B,top(C)) :- !,
    maplist(units_domain_multiplication(B),A,C).

units_domain_multiplication(A,top(B),top(C)) :- !,
    maplist(units_domain_multiplication(A),B,C).

units_domain_multiplication(Op1,[],Op1) :- !.

units_domain_multiplication([],Op2,Op2) :- !.

units_domain_multiplication([[Factor1,Unit1,Pow1]|Units], UnitsOp2, Res2) :- !,
    (selectchk([Factor2,Unit1,Pow2],UnitsOp2,UnitsOp22)
    -> Factor3 is Factor1+Factor2, Pow3 is Pow1+Pow2,
    Res1 = [Factor3,Unit1,Pow3], units_domain_multiplication(Units,UnitsOp22,UnitsResult)
    ; Res1 = [Factor1,Unit1,Pow1], units_domain_multiplication(Units,UnitsOp2,UnitsResult)
    ),
    (Res1 = [0,_,0] -> Res2 = UnitsResult ; Res2 = [Res1|UnitsResult]).

units_domain_multiplication_conversion(_, X, _) :- var(X), !.

units_domain_multiplication_conversion(b(integer(X),_,_), [Unit|Units], [Unit2|Units]) :-
    repeat_conversion_factor(X,Unit,Unit2).

units_domain_multiplication_conversion(BInt,[Unit|Units],[Unit|Units2]) :-
    units_domain_multiplication_conversion(BInt,Units,Units2).

units_domain_power_of(A,b(integer(B,_,_)),C) :- var(A), put_atts(A,constraint), put_atts(C, pfactors(A,B)), !.

units_domain_power_of(A, b(integer(X),_,_),C) :-
    power_of_multiply_units(X,A,C), !.

units_domain_power_of(top(A), b(integer(X),_,_),top(C)) :-
    maplist(power_of_multiply_units(X),A,C), !.

units_domain_power_of(_A,_B,top([])) :- !.

units_domain_relation(set(A),set(B),set(set(couple(A,B)))).

units_domain_subtraction_conversion(_, X, _) :- var(X), !.

units_domain_subtraction_conversion(b(integer(X),_,_), [Unit|Units], [Unit2|Units]) :-
    repeat_conversion_add(X,Unit,Unit2).

units_domain_subtraction_conversion(BInt,[Unit|Units],[Unit|Units2]) :-
    units_domain_subtraction_conversion(BInt,Units,Units2).

verify_attributes(Var, Value, Goal) :-
    % the variable might be the result of a multiplication
    % -> propagate inwards
    get_atts(Var, mfactors(A,B)), !,
    (var(Value) -> Goal = [] ;
    (A==B, var(A)) -> Goal=[power_of_multiply_units(2,A,Value)] ;
    (var(A), nonvar(B)) -> Goal=[units_domain_division(Value,B,A)] ;
    (var(B), nonvar(A)) -> Goal=[units_domain_division(Value,A,B)] ;
    Goal=[]).

verify_attributes(Var, Value, Goal) :-
    % the variable might be the result of a division
    % -> propagate inwards
    get_atts(Var, dfactors(A,B)), !,
    (var(Value) -> Goal=[] ;
    (var(A), nonvar(B)) -> Goal=[units_domain_multiplication(Value,B,A)] ;
    (var(B), nonvar(A)) -> Goal=[units_domain_division(A,Value,B)] ;
    Goal=[]).

verify_attributes(Var, Value, Goal) :-
    % the variable might be the result of a exponentiation
    % -> propagate inwards
    get_atts(Var, pfactors(A,B)), !,
    (var(Value) -> Goal=[] ;
    (var(A), nonvar(B)) -> Goal=[power_of_multiply_units(B,A,Value)] ;
    Goal=[]).

verify_attributes(Var, Value, []) :-
    get_atts(Var, constraint), !,
    (var(Value) -> put_atts(Value, constraint) ; true).