units_interpreter

units_check_boolean_expression(b(Expr,Type,Infos),LS,S) :- !,
    % if units_check_boolean_expression2 fails, there was a wrong usage of units
    %statistics(walltime,[Start,_]),
    %format('Start checking ~w~n', [Expr]),
    (units_check_boolean_expression2(Expr,Infos,LS,S,NoInnerError)
    -> ( NoInnerError = false
    -> %trace, units_check_boolean_expression2(Expr,Infos,LS,S,NoInnerError), notrace,
    current_state_id(ID),
    member(nodeid(Position),Infos),
    translate_bexpression(b(Expr,Type,Infos), PPExpr),
    units:units_error_context(Context),
    store_state_error(ID,abort_error(well_definedness_error,
    'Wrong usage of units in expression',PPExpr,
    span_context(Position,Context)),_)
    ; true%, format('Boolean Expression computed: ~w~n', [Expr])
    )
    ; % computational error, not unit error!
    add_error_fail(units_check_boolean_expression, 'Boolean Expression Check Failed: ', [Expr,Infos,LS,S])).

units_check_boolean_expression2(truth,_Infos,_LocalState,_InState,true) :- !.

units_check_boolean_expression2(falsity,_Infos,_LocalState,_InState,true) :- !.

units_check_boolean_expression2(partition(Arg1,Arg2),_Infos,LocalState,State,Result) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    units_compute_expressions(Arg2,LocalState,State,SV2),
    (same_units([SV1|SV2]) -> Result = true ; Result = false).

units_check_boolean_expression2(conjunct(LHS,RHS),_Infos,LocalState,State,true) :-
    !,units_check_boolean_expression(LHS,LocalState,State),
    units_check_boolean_expression(RHS,LocalState,State).

units_check_boolean_expression2(negation(Val),_Infos,LocalState,State,true) :-
    !,units_check_boolean_expression(Val,LocalState,State).

units_check_boolean_expression2(disjunct(LHS,RHS),_Infos,LocalState,State,true) :-
    !,units_check_boolean_expression(LHS,LocalState,State),
    units_check_boolean_expression(RHS,LocalState,State).

units_check_boolean_expression2(implication(LHS,RHS),_Infos,LocalState,State,true) :-
    !,units_check_boolean_expression(LHS,LocalState,State),
    units_check_boolean_expression(RHS,LocalState,State).

units_check_boolean_expression2(equivalence(LHS,RHS),_Infos,LocalState,State,true) :-
    !,units_check_boolean_expression(LHS,LocalState,State),
    units_check_boolean_expression(RHS,LocalState,State).

units_check_boolean_expression2(equal(Arg1,Arg2),_Info,LocalState,State,Result) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    units_compute_expression(Arg2,LocalState,State,SV2),
    (same_units(SV1,SV2) -> Result = true ; Result = false).

units_check_boolean_expression2(not_equal(Arg1,Arg2),_Info,LocalState,State,Result) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    units_compute_expression(Arg2,LocalState,State,SV2),
    (same_units(SV1,SV2) -> Result = true ; Result = false).

units_check_boolean_expression2(member(Arg1,Arg2),_Info,LocalState,State,Result) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    units_compute_expression(Arg2,LocalState,State,SV2),
    (units_domain_member(SV1,SV2) -> Result = true ; Result = false).

units_check_boolean_expression2(not_member(Arg1,Arg2),_Info,LocalState,State,Result) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    units_compute_expression(Arg2,LocalState,State,SV2),
    (units_domain_member(SV1,SV2) -> Result = true ; Result = false).

units_check_boolean_expression2(subset(Arg1,Arg2),_Info,LocalState,State,Result) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    units_compute_expression(Arg2,LocalState,State,SV2),
    (same_units(SV1,SV2) -> Result = true ; Result = false).

units_check_boolean_expression2(subset_strict(Arg1,Arg2),_Info,LocalState,State,Result) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    units_compute_expression(Arg2,LocalState,State,SV2),
    (same_units(SV1,SV2) -> Result = true ; Result = false).

units_check_boolean_expression2(not_subset(Arg1,Arg2),_Info,LocalState,State,Result) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    units_compute_expression(Arg2,LocalState,State,SV2),
    (same_units(SV1,SV2) -> Result = true ; Result = false).

units_check_boolean_expression2(not_subset_strict(Arg1,Arg2),_Info,LocalState,State,Result) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    units_compute_expression(Arg2,LocalState,State,SV2),
    (same_units(SV1,SV2) -> Result = true ; Result = false).

units_check_boolean_expression2(less_equal(Arg1,Arg2),_Infos,LocalState,InState,Result) :-
    !, units_compute_expression(Arg1,LocalState,InState,SV1),
    units_compute_expression(Arg2,LocalState,InState,SV2),
    (same_units(SV1,SV2) -> Result = true ; Result = false).

units_check_boolean_expression2(less(Arg1,Arg2),_Infos,LocalState,InState,Result) :-
    !, units_compute_expression(Arg1,LocalState,InState,SV1),
    units_compute_expression(Arg2,LocalState,InState,SV2),
    (same_units(SV1,SV2) -> Result = true ; Result = false).

units_check_boolean_expression2(greater_equal(Arg1,Arg2),_Infos,LocalState,InState,Result) :-
    !, units_compute_expression(Arg1,LocalState,InState,SV1),
    units_compute_expression(Arg2,LocalState,InState,SV2),
    (same_units(SV1,SV2) -> Result = true ; Result = false).

units_check_boolean_expression2(greater(Arg1,Arg2),_Infos,LocalState,InState,Result) :-
    !, units_compute_expression(Arg1,LocalState,InState,SV1),
    units_compute_expression(Arg2,LocalState,InState,SV2),
    (same_units(SV1,SV2) -> Result = true ; Result = false).

units_check_boolean_expression2(exists(Parameters,RHS),_Infos,LocalState,InState,true) :-
    !, units_set_up_localstate(Parameters,_ParaValues,InnerLocalState),
    append(InnerLocalState,LocalState,CompleteLocalState),
    units_check_boolean_expression(RHS,CompleteLocalState,InState).

units_check_boolean_expression2(forall(Parameters,LHS,RHS),_Infos,LocalState,InState,true) :-
    !, units_set_up_localstate(Parameters,_ParaValues,InnerLocalState),
    append(InnerLocalState,LocalState,CompleteLocalState),
    units_check_boolean_expression(LHS,CompleteLocalState,InState),
    units_check_boolean_expression(RHS,CompleteLocalState,InState).

units_check_boolean_expression2(let_predicate(Ids,Assignments,Expr),_Infos,LocalState,State,true) :-
    !, units_compute_expressions(Assignments,LocalState,State,Assignments2),
    assign_vars(Ids,Assignments2,LocalState,State, NewVars, NewVals),
    assign_vals_to_vars(NewVars, NewVals, StoreList),
    append(StoreList,LocalState,LetState),
    units_check_boolean_expression(Expr,LetState,State).

units_check_boolean_expression2(Test,_Infos,LocalState,InState,_Res) :-
    !, add_error_fail(units_check_boolean_expression, 'Boolean Expression not implemented: ', [Test,LocalState,InState]).

units_check_list_of_boolean_expressions([],_LocalState,_InState).

units_check_list_of_boolean_expressions([Expr|T],LocalState,InState) :-
    units_check_boolean_expression(Expr,LocalState,InState),
    units_check_list_of_boolean_expressions(T,LocalState,InState).

units_compute_expression(b(Expr,Type,Info),LS,S,R) :- !,
    units_compute_expression2(Expr,Type,Info,LS,S,R),
    (contains_top(R)
    -> current_state_id(ID),
    member(nodeid(Position),Info),
    translate_bexpression(b(Expr,Type,Info), PPExpr),
    units:units_error_context(Context),
    store_state_error(ID,abort_error(well_definedness_error,
    'Wrong usage of units in expression',PPExpr,
    span_context(Position,Context)),_)
    ; true).

units_compute_expression2(boolean_true,_Type,_Info,_LocalState,_State,boolean(_)) :- !.

units_compute_expression2(boolean_false,_Type,_Info,_LocalState,_State,boolean(_)) :- !.

units_compute_expression2(min_int,_Type,_Info,_LocalState,_State,integer(_)) :- !.

units_compute_expression2(max_int,_Type,_Info,_LocalState,_State,integer(_)) :- !.

units_compute_expression2(empty_set,Type,Info,_LocalState,_State,Result) :-
    !, b_type_to_internal_type(Type,Info,Result).

units_compute_expression2(bool_set,_Type,_Info,_LocalState,_State,set(boolean(_))) :- !.

units_compute_expression2(string_set,_Type,_Info,_LocalState,_State,set(string(_))) :- !.

units_compute_expression2(convert_bool(Arg1),_Type,_Info,LocalState,State,boolean(_)) :-
    !, units_check_boolean_expression(Arg1,LocalState,State).

units_compute_expression2(add(Arg1,Arg2),integer,Info,LocalState,State,integer(Value)) :-
    !, units_compute_expression(Arg1,LocalState,State,integer(SV1)),
    units_compute_expression(Arg2,LocalState,State,integer(SV2)),
    units_compute_expression(Arg2,LocalState,State,integer(SV2)),
    (
    member(conversion,Info)
    -> (
    (var(SV1)
    -> units_domain_addition_conversion(Arg1,SV2,Value), !
    ; units_domain_addition_conversion(Arg2,SV1,Value), !
    )
    ; !, member(nodeid(Position),Info),
    current_state_id(ID),
    translate_bexpression(b(add(Arg1,Arg2),integer,Info), PPExpr),
    units:units_error_context(Context),
    store_state_error(ID,abort_error(well_definedness_error,
    'Wrong usage of conversion',PPExpr,
    span_context(Position,Context)),_)
    )
    ; lub(SV1,SV2,Value)
).

units_compute_expression2(minus(Arg1,Arg2),integer,Info,LocalState,State,integer(Value)) :-
    !, units_compute_expression(Arg1,LocalState,State,integer(SV1)),
    units_compute_expression(Arg2,LocalState,State,integer(SV2)),
    (
    member(conversion,Info)
    -> (
    (var(SV1)
    -> units_domain_subtraction_conversion(Arg1,SV2,Value), !
    ; units_domain_subtraction_conversion(Arg2,SV1,Value), !
    )
    ; !, member(nodeid(Position),Info),
    current_state_id(ID),
    translate_bexpression(b(minus(Arg1,Arg2),integer,Info), PPExpr),
    units:units_error_context(Context),
    store_state_error(ID,abort_error(well_definedness_error,
    'Wrong usage of conversion',PPExpr,
    span_context(Position,Context)),_)
    )
    ; lub(SV1,SV2,Value)
).

units_compute_expression2(unary_minus(Arg1),integer,_Info,LocalState,State,Arg2) :-
    !, units_compute_expression(Arg1,LocalState,State,Arg2).

units_compute_expression2(multiplication(Arg1,Arg2),integer,Info,LocalState,State,integer(Value)) :-
    !,
    units_compute_expression(Arg1,LocalState,State,integer(SV1)),
    units_compute_expression(Arg2,LocalState,State,integer(SV2)),
    (
    member(conversion,Info)
    -> (
    (var(SV1)
    -> units_domain_multiplication_conversion(Arg1,SV2,Value), !
    ; units_domain_multiplication_conversion(Arg2,SV1,Value), !
    )
    ; !, member(nodeid(Position),Info),
    current_state_id(ID),
    translate_bexpression(b(multiplication(Arg1,Arg2),integer,Info), PPExpr),
    units:units_error_context(Context),
    store_state_error(ID,abort_error(well_definedness_error,
    'Wrong usage of conversion',PPExpr,
    span_context(Position,Context)),_)
    )
    ; units_domain_multiplication(SV1,SV2,Value)
).

units_compute_expression2(cartesian_product(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    units_compute_expression(Arg2,LocalState,State,SV2),
    SV1 = set(C1), SV2 = set(C2), Value = set(couple(C1,C2)).

units_compute_expression2(div(Arg1,Arg2),integer,Info,LocalState,State,integer(Value)) :-
    !,
    units_compute_expression(Arg1,LocalState,State,integer(SV1)),
    units_compute_expression(Arg2,LocalState,State,integer(SV2)),
    (
    member(conversion,Info)
    -> (
    (var(SV1)
    -> units_domain_division_conversion(Arg1,SV2,Value), !
    ; units_domain_division_conversion(Arg2,SV1,Value), !
    )
    ; !, member(nodeid(Position),Info),
    current_state_id(ID),
    translate_bexpression(b(div(Arg1,Arg2),integer,Info), PPExpr),
    units:units_error_context(Context),
    store_state_error(ID,abort_error(well_definedness_error,
    'Wrong usage of conversion',PPExpr,
    span_context(Position,Context)),_)
    )
    ; units_domain_division(SV1,SV2,Value)
).

units_compute_expression2(modulo(Arg1,_Arg2),integer,_Info,LocalState,State,SV1) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1).

units_compute_expression2(power_of(Arg1,Arg2),integer,_Info,LocalState,State,integer(Value)) :-
    !, units_compute_expression(Arg1,LocalState,State,integer(SV1)),
    units_domain_power_of(SV1,Arg2,Value).

units_compute_expression2(min(Arg1),_Type,_Info,LocalState,State,Value) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    SV1 = set(Value).

units_compute_expression2(max(Arg1),_Type,_Info,LocalState,State,Value) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    SV1 = set(Value).

units_compute_expression2(card(_Arg1),integer,_Info,_LocalState,_State,integer([])) :- !.

units_compute_expression2(couple(Arg1,Arg2),_Type,_Info,LocalState,State,couple(SV1,SV2)) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    units_compute_expression(Arg2,LocalState,State,SV2).

units_compute_expression2(pow_subset(Arg1),_X,_Info,LocalState,State,set(SV1)) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1).

units_compute_expression2(pow1_subset(Arg1),_X,_Info,LocalState,State,set(SV1)) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1).

units_compute_expression2(fin_subset(Arg1),_X,_Info,LocalState,State,set(SV1)) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1).

units_compute_expression2(fin1_subset(Arg1),_X,_Info,LocalState,State,set(SV1)) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1).

units_compute_expression2(interval(Arg1,Arg2),set(integer),_Info,LocalState,State,set(Value)) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    units_compute_expression(Arg2,LocalState,State,SV2),
    lub(SV1,SV2,Value).

units_compute_expression2(union(Arg1,Arg2),set(_X),_Info,LocalState,State,set(Value)) :-
    !, units_compute_expression(Arg1,LocalState,State,set(SV1)),
    units_compute_expression(Arg2,LocalState,State,set(SV2)),
    lub(SV1,SV2,Value).

units_compute_expression2(intersection(Arg1,Arg2),set(_X),_Info,LocalState,State,set(Value)) :-
    !, units_compute_expression(Arg1,LocalState,State,set(SV1)),
    units_compute_expression(Arg2,LocalState,State,set(SV2)),
    lub(SV1,SV2,Value).

units_compute_expression2(set_subtraction(Arg1,Arg2),_X,_Info,LocalState,State,Value) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    units_compute_expression(Arg2,LocalState,State,SV2),
    lub(SV1,SV2,Value).

units_compute_expression2(general_union(Arg1),_X,_Info,LocalState,State,Value) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    SV1 = set(set(A)), Value = set(A).

units_compute_expression2(general_intersection(Arg1),_X,_Info,LocalState,State,Value) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    SV1 = set(set(A)), Value = set(A).

units_compute_expression2(relations(Arg1,Arg2),_X,_Info,LocalState,State,Value) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    units_compute_expression(Arg2,LocalState,State,SV2),
    units_domain_relation(SV1,SV2,Value).

units_compute_expression2(reverse(Arg1),_X,_Info,LocalState,State,Value) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    SV1 = set(couple(A,B)),
    Value = set(couple(B,A)).

units_compute_expression2(concat(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    units_compute_expression(Arg2,LocalState,State,SV2),
    lub(SV1,SV2,Value).

units_compute_expression2(insert_front(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    units_compute_expression(Arg2,LocalState,State,SV2),
    lub(set(couple(integer(_),SV1)),SV2,Value).

units_compute_expression2(insert_tail(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    units_compute_expression(Arg2,LocalState,State,SV2),
    lub(SV1,set(couple(integer(_),SV2)),Value).

units_compute_expression2(general_concat(Arg1),_X,_Info,LocalState,State,Value) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    SV1 = set(couple(integer(_),set(couple(integer(_),A)))), Value = set(couple(integer(_),A)).

units_compute_expression2(composition(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    units_compute_expression(Arg2,LocalState,State,SV2),
    SV1 = set(couple(A,B1)), SV2 = set(couple(B2,C)),
    same_units(B1,B2), Value = set(couple(A,C)).

units_compute_expression2(direct_product(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    units_compute_expression(Arg2,LocalState,State,SV2),
    SV1 = set(couple(A1,B)), SV2 = set(couple(A2,C)),
    lub(A1,A2,A3),
    Value = set(couple(A3,couple(B,C))).

units_compute_expression2(parallel_product(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    units_compute_expression(Arg2,LocalState,State,SV2),
    SV1 = set(couple(A,B)), SV2 = set(couple(C,D)),
    Value = set(couple(couple(A,C),couple(B,D))).

units_compute_expression2(domain(Arg1),_Type,_Info,LocalState,State,set(Value)) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    SV1 = set(couple(Value,_X)).

units_compute_expression2(range(Arg1),_Type,_Info,LocalState,State,set(Value)) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    SV1 = set(couple(_X,Value)).

units_compute_expression2(image(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    units_compute_expression(Arg2,LocalState,State,SV2),
    SV1 = set(couple(A1,Image)), SV2 = set(A2),
    same_units(A1,A2), Value=set(Image).

units_compute_expression2(domain_restriction(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    units_compute_expression(Arg2,LocalState,State,SV2),
    SV1 = set(A1), SV2 = set(couple(A2,B)),
    lub(A1,A2,A3), Value=set(couple(A3,B)).

units_compute_expression2(domain_subtraction(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    units_compute_expression(Arg2,LocalState,State,SV2),
    SV1 = set(A1), SV2 = set(couple(A2,B)),
    lub(A1,A2,A3), Value=set(couple(A3,B)).

units_compute_expression2(range_restriction(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    units_compute_expression(Arg2,LocalState,State,SV2),
    SV1 = set(couple(A,B1)), SV2 = set(B2),
    lub(B1,B2,B3), Value=set(couple(A,B3)).

units_compute_expression2(range_subtraction(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    units_compute_expression(Arg2,LocalState,State,SV2),
    SV1 = set(couple(A,B1)), SV2 = set(B2),
    lub(B1,B2,B3), Value=set(couple(A,B3)).

units_compute_expression2(overwrite(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    units_compute_expression(Arg2,LocalState,State,SV2),
    lub(SV1,SV2,Value).

units_compute_expression2(partial_function(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    units_compute_expression(Arg2,LocalState,State,SV2),
    units_domain_relation(SV1,SV2,Value).

units_compute_expression2(total_function(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    units_compute_expression(Arg2,LocalState,State,SV2),
    units_domain_relation(SV1,SV2,Value).

units_compute_expression2(partial_injection(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    units_compute_expression(Arg2,LocalState,State,SV2),
    units_domain_relation(SV1,SV2,Value).

units_compute_expression2(total_injection(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    units_compute_expression(Arg2,LocalState,State,SV2),
    units_domain_relation(SV1,SV2,Value).

units_compute_expression2(partial_surjection(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    units_compute_expression(Arg2,LocalState,State,SV2),
    units_domain_relation(SV1,SV2,Value).

units_compute_expression2(total_surjection(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    units_compute_expression(Arg2,LocalState,State,SV2),
    units_domain_relation(SV1,SV2,Value).

units_compute_expression2(total_bijection(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    units_compute_expression(Arg2,LocalState,State,SV2),
    units_domain_relation(SV1,SV2,Value).

units_compute_expression2(partial_bijection(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    units_compute_expression(Arg2,LocalState,State,SV2),
    units_domain_relation(SV1,SV2,Value).

units_compute_expression2(total_relation(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    units_compute_expression(Arg2,LocalState,State,SV2),
    units_domain_relation(SV1,SV2,Value).

units_compute_expression2(surjection_relation(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    units_compute_expression(Arg2,LocalState,State,SV2),
    units_domain_relation(SV1,SV2,Value).

units_compute_expression2(total_surjection_relation(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    units_compute_expression(Arg2,LocalState,State,SV2),
    units_domain_relation(SV1,SV2,Value).

units_compute_expression2(seq(Arg1),_Type,_Info,LocalState,State,set(set(couple(integer(_),V)))) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    SV1 = set(V).

units_compute_expression2(seq1(Arg1),_Type,_Info,LocalState,State,set(set(couple(integer(_),V)))) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    SV1 = set(V).

units_compute_expression2(iset(couple(integer(_),Arg1)),_Type,_Info,LocalState,State,set(set(couple(integer(_),V)))) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    SV1 = set(V).

units_compute_expression2(iseq(Arg1),_Type,_Info,LocalState,State,set(set(couple(integer(_),V)))) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    SV1 = set(V).

units_compute_expression2(iseq1(Arg1),_Type,_Info,LocalState,State,set(set(couple(integer(_),V)))) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    SV1 = set(V).

units_compute_expression2(perm(Arg1),_Type,_Info,LocalState,State,set(set(couple(integer(_),V)))) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    SV1 = set(V).

units_compute_expression2(empty_sequence,Type,Info,_LocalState,_State,Result) :-
    !, b_type_to_internal_type(Type,Info,Result).

units_compute_expression2(size(_Arg1),_Type,_Info,_LocalState,_State,integer([])) :- !.

units_compute_expression2(first(Arg1),_Type,_Info,LocalState,State,V) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    SV1 = set(couple(integer(_),V)).

units_compute_expression2(last(Arg1),_Type,_Info,LocalState,State,V) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    SV1 = set(couple(integer(_),V)).

units_compute_expression2(front(Arg1),_Type,_Info,LocalState,State,SV1) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1).

units_compute_expression2(tail(Arg1),_Type,_Info,LocalState,State,SV1) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1).

units_compute_expression2(rev(Arg1),_Type,_Info,LocalState,State,SV1) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1).

units_compute_expression2(concat(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    units_compute_expression(Arg2,LocalState,State,SV2),
    lub(SV1,SV2,Value).

units_compute_expression2(function(Function,Arg),_Type,_Info,LocalState,State,Value) :-
    !, units_compute_expression(Function,LocalState,State,FValue),
    units_compute_expression(Arg,LocalState,State,ArgValue),
    FValue = set(couple(ArgValue,Value)).

units_compute_expression2(set_extension(Ex),set(_X),_Info,LocalState,State,set(Merged)) :-
    !, units_compute_expressions(Ex,LocalState,State,ExValue),
    merge_expression_list(ExValue,Merged).

units_compute_expression2(sequence_extension(Ex),_X,_Info,LocalState,State,set(couple(integer(_),Merged))) :-
    !, units_compute_expressions(Ex,LocalState,State,ExValue),
    merge_expression_list(ExValue,Merged).

units_compute_expression2(comprehension_set(ListOfIDs,Pred),_Type,_Info,LocalState,State,set(Merged)) :-
    !,
    units_set_up_localstate(ListOfIDs,_Bindings,ParameterState),
    append(ParameterState,LocalState,NewLocalState),
    units_check_boolean_expression(Pred,NewLocalState,State),
    units_compute_expressions(ListOfIDs,NewLocalState,State,ExValues),
    %format('#### ExValues in Comprehension Set: ~w~n', [ExValues]),
    couplise_list(ExValues, Merged).

units_compute_expression2(general_sum(ListOfIDs,Pred,Stmt),_Type,_Info,LocalState,State,Value) :-
    !,
    units_set_up_localstate(ListOfIDs,_Bindings,ParameterState),
    append(ParameterState,LocalState,NewLocalState),
    units_check_boolean_expression(Pred,NewLocalState,State),
    units_compute_expression(Stmt,NewLocalState,State,Value).

units_compute_expression2(general_product(ListOfIDs,Pred,Stmt),_Type,_Info,LocalState,State,Value) :-
    !,
    units_set_up_localstate(ListOfIDs,_Bindings,ParameterState),
    append(ParameterState,LocalState,NewLocalState),
    units_check_boolean_expression(Pred,NewLocalState,State),
    units_compute_expression(Stmt,NewLocalState,State,Value).

units_compute_expression2(closure(Arg1),_X,_Info,LocalState,State,SV1) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1).

units_compute_expression2(closure1(Arg1),_X,_Info,LocalState,State,SV1) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1).

units_compute_expression2(reflexive_closure(Arg1),_X,_Info,LocalState,State,SV1) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1).

units_compute_expression2(integer(_Int),_T,Info,_LS,_S,Res) :- !,
    (member(unit(Unit),Info) -> unit_args_to_list(Unit, V), Res=integer(V); Res=integer(_)).

units_compute_expression2(identifier(Id),_Type,_Info,LocalState,State,Value) :-
    !, units_lookup_value(Id,LocalState,State,Value).

units_compute_expression2(first_of_pair(Pair),_Type,_Info,LocalState,State,Value) :-
    !, units_compute_expression(Pair,LocalState,State,SV1),
    SV1 = couple(Value,_Second).

units_compute_expression2(second_of_pair(Pair),_Type,_Info,LocalState,State,Value) :-
    !, units_compute_expression(Pair,LocalState,State,SV1),
    SV1 = couple(_First,Value).

units_compute_expression2(iteration(Arg1,_Arg2),_Type,_Info,LocalState,State,Value) :-
    !, units_compute_expression(Arg1,LocalState,State,SV1),
    Value = SV1.

units_compute_expression2(integer_set(_),Type,Info,_LocalState,_State,Result) :-
    !, b_type_to_internal_type(Type,Info,Result).

units_compute_expression2(string(_),_Type,_Info,_LocalState,_State,string(_)) :- !.

units_compute_expression2(external_function_call(_FunName,Arguments),Type,Info,LocalState,State,Result) :-
    %format('Function: ~w~nArguments: ~w~nType: ~w~nInfo:~w~n', [FunName,Arguments,Type,Info]),
    !, units_compute_expressions(Arguments,LocalState,State,_EvaluatedArgs),
    b_type_to_internal_type(Type,Info,Result).

units_compute_expression2(identity(X),_Type,_Info,LocalState,State,Result) :-
    !, units_compute_expression(X,LocalState,State,set(XExpr)),
    Result = set(couple(XExpr,XExpr)).

units_compute_expression2(value(_),Type,Info,_LocalState,_State,Result) :-
    !, b_type_to_internal_type(Type,Info,Result).

units_compute_expression2(let_expression(Ids,Assignments,Expr),_Type,_Infos,LocalState,State,Result) :-
    !, units_compute_expressions(Assignments,LocalState,State,Assignments2),
    assign_vars(Ids,Assignments2,LocalState,State,NewVars,NewVals),
    assign_vals_to_vars(NewVars,NewVals,StoreList),
    append(StoreList,LocalState,LetState),
    units_compute_expression(Expr,LetState,State,Result).

units_compute_expression2(rec(Fields),_Type,_Infos,LocalState,State,rec(Result)) :-
    !, units_compute_record_fields(Fields,LocalState,State,Result).

units_compute_expression2(record_field(Record,Field),_Type,_Infos,LocalState,State,Result) :-
    !, units_compute_expression(Record,LocalState,State,rec(Fields)),
    member(field(Field,Result),Fields).

units_compute_expression2(struct(Rec),_Type,_Infos,LocalState,State,set(Result)) :-
    !, units_compute_expression(Rec,LocalState,State,Result).

units_compute_expression2(X,T,I,LS,S,_V) :-
    !, add_error_fail(units_compute_expression2, 'Expression not implemented: ', [X,T,I,LS,S]).

units_compute_expressions([], _, _, []).

units_compute_expressions([EXPRsHd|EXPRsTl],LocalState,InState,[ValHd|ValTl]) :-
    units_compute_expression(EXPRsHd,LocalState,InState,ValHd),
    units_compute_expressions(EXPRsTl,LocalState,InState,ValTl).

units_compute_record_fields([],_,_,[]).

units_compute_record_fields([field(Name,Val)|Fields],LocalState,State,[field(Name,UVal)|UFields]) :-
    units_compute_expression(Val,LocalState,State,UVal),
    units_compute_record_fields(Fields,LocalState,State,UFields).

units_execute_operation(Name,Operation,InState,NewOutState,ParaValues,ResultValues,TopLevel,Path) :-
    b_interpreter:b_get_machine_operation_for_animation(Name,Results,Parameters,Body,_OType,TopLevel),
    units_execute_operation(Name,Operation,InState,NewOutState,Body,Parameters,ParaValues,Results,ResultValues,TopLevel,Path).

units_execute_operation(Name,RealFullOperation,InState,SortedStateFinish,Body,Parameters,ParameterValues,Results,ResultValues,TopLevel,Path) :-
    units_set_up_localstate(Parameters,ParameterValues,LocalState),
    units_set_up_undefined_localstate(Results,InState,NewInState),
    (
    TopLevel==true
    -> units_execute_top_level_statement(Body,LocalState,NewInState,OutState,Path)
    ; units_execute_statement(Body,LocalState,NewInState,OutState,Path)
    ),
    l_expand_and_normalise_values(ParameterValues,NormalisedParameterValues,Parameters),
    Operation =.. [Name|NormalisedParameterValues],
    (
    Results == []
    -> RealFullOperation = Operation
    ; RealFullOperation = '-->'(Operation,ResultValues)
    ),
    units_get_results(Results,OutState,ResultValues,StateFinish),
    units_get_results(Parameters,LocalState,ParameterValues,_StateFinish),
    samsort(StateFinish,SortedStateFinish),
    % check if either the parameters or the results contain top and add error
    (contains_top(ResultValues)
    -> %member(nodeid(Position),Info),
    current_state_id(ID), get_texpr_info(Body,Info),
    member(nodeid(Position),Info),
    %translate_bexpression(b(minus(Arg1,Arg2),integer,Info), PPExpr),
    units:units_error_context(Context),
    store_state_error(ID,abort_error(well_definedness_error,
    'Result value has multiple units',Name,
    span_context(Position,Context)),_),
    assert_once(top_in_results(Name))
    ; true),
    (contains_top(ParameterValues)
    -> %member(nodeid(Position),Info),
    current_state_id(ID), get_texpr_info(Body,Info),
    member(nodeid(Position),Info),
    %translate_bexpression(b(minus(Arg1,Arg2),integer,Info), PPExpr),
    units:units_error_context(Context),
    store_state_error(ID,abort_error(well_definedness_error,
    'Parameter value has multiple units',Name,
    span_context(Position,Context)),_),
    assert_once(top_in_parameters(Name))
    ; true).

units_execute_operation_with_parameters(Name,InState,Parameters,OutState,ResultValues,Path) :-
    (b_get_machine_operation(Name,_,_,_)
    -> units_execute_operation(Name,_,InState,OutState,Parameters,ResultValues,false,Path)
    ; add_error_fail(units_interpreter,'Unknown operation, cannot call: ',Name)
).

units_execute_statement(b(Stmt,_,Infos),LocalState,InState,OutState,Path) :-
    units_execute_statement2(Stmt, Infos, LocalState,InState, OutState, Path).

units_execute_statement2(rlevent(_Name,_Section,_Status,_Params,_Guard,_Theorems,Actions,_VWitnesses,_PWitnesses,_Unmod,_AbstractEvents),
    _Infos,LocalState,InState,OutState,eventb(Path)) :- !,
    execute_eventb_list(Actions,LocalState,InState,OutState,Path).

units_execute_statement2(assign_single_id(IDE,Expr),_Infos,LocalState,InState,OutState,assign) :-
    get_texpr_id(IDE,ID),!,
    units_compute_expression(Expr,LocalState,InState,Value),
    state_store(bind(ID,Value),InState,OutState).

units_execute_statement2(assign(VarExprs, ValExprs), _Infos,LocalState,InState,OutState,assign) :-
    !, units_compute_expressions(ValExprs, LocalState, InState, ValExprs2),
    assign_vars(VarExprs, ValExprs2, LocalState, InState, NewVars, NewVals),
    assign_vals_to_vars(NewVars, NewVals, StoreList),
    state_store_list(StoreList, InState, OutState).

units_execute_statement2(parallel(Statements),_Infos,LocalState,InState,OutState,parallel(Paths)) :-
    !, execute_statements_in_parallel(Statements, LocalState, InState, OutState, Paths).

units_execute_statement2(skip,_Infos,_LocalState,InState,InState,skip) :- !.

units_execute_statement2(any(Parameters,PreCond,Body),_Infos,LocalState,InState,OutState,any(Bindings,Path)) :-
    !, units_set_up_localstate(Parameters,Bindings,ParameterState),
    append(ParameterState,LocalState,NewLocalState),
    units_check_boolean_expression(PreCond,NewLocalState,InState),
    units_execute_statement(Body,NewLocalState,InState,OutState,Path).

units_execute_statement2(if(IfList),_Infos,LocalState,InState,OutState,if) :-
    !, execute_else_list(IfList,LocalState,InState,OutState).

units_execute_statement2(select(SelectList),_Infos,LocalState,InState,OutState,select) :-
    !, execute_select_list(SelectList,LocalState,InState,OutState).

units_execute_statement2(select(Whens,Else),Infos,LocalState,InState,OutState,select(PathWhens,PathElse)) :- !,
    units_execute_statement2(select(Whens),Infos,LocalState,InState,IntermediateState,PathWhens),
    findall(PC,(member(SW,Whens),get_texpr_expr(SW,select_when(PC,_))), AllPreconds),
    units_check_list_of_boolean_expressions(AllPreconds,LocalState,InState),
    units_execute_statement(Else,LocalState,IntermediateState,OutState,PathElse).

units_execute_statement2(becomes_element_of(Element,Expression),_Infos,LocalState,InState,OutState,becomes_element_of) :-
    !, Element=[b(identifier(ID),_,_)],
    units_compute_expression(Expression,LocalState,InState,Value),
    Value = set(Inner),
    state_store(bind(ID,Inner),InState,OutState).

units_execute_statement2(becomes_such(Vars,Condition),_,LocalState,InState,OutState,becomes_such) :- !,
    units_set_up_localstate(Vars,_Bindings,VarsState),
    state_store_list(VarsState, InState, OutState),
    insert_before_substitution_variables(Vars,LocalState,InState,OutState,TempLocalState),
    units_check_boolean_expression(Condition,TempLocalState,OutState).

units_execute_statement2(operation_call(Operation,Results,Parameters),_,LocalState,InState,OutState,
    operation_call(OperationName,ParamValues,ResultValues,InnerPath)) :- !,
    def_get_texpr_id(Operation,op(OperationName)),
    units_compute_expressions(Parameters,LocalState,InState,ParamValues),
    units_execute_operation_with_parameters(OperationName,InState,ParamValues,OpOutState,ResultValues,InnerPath),
    b_interpreter:split_names_and_types(Results,ResultingIDs,_),
    assign_vals_to_vars(ResultingIDs, ResultValues, ResultsOutState),
    merge_non_overriding_states(ResultsOutState,OpOutState,OutState).

units_execute_statement2(precondition(PreCond,Body),_,LocalState,InState,OutState,Path) :- !,
    units_check_boolean_expression(PreCond,LocalState,InState),
    Path=pre(IPath),
    units_execute_statement(Body,LocalState,InState,OutState,IPath).

units_execute_statement2(case(Expression,Cases,Else),_,LocalState,InState,OutState,case) :- !,
    units_compute_expression(Expression,LocalState,InState,EValue),
    execute_cases_list(EValue,Cases,LocalState,InState,OutStateTmp),
    units_execute_statement(Else,LocalState,OutStateTmp,OutState,_Path).

units_execute_statement2(var(Parameters,Body),_Infos,LocalState,InState,NewOutState,var(Path)) :- !,
    units_set_up_undefined_localstate(Parameters,InState,NewInState),
    b_interpreter:split_names_and_types(Parameters,Names,_),
    store:delete_variables_from_state(Names,LocalState,NewLocalState),
    units_execute_statement(Body,NewLocalState,NewInState,OutState,Path),
    units_get_results(Parameters,OutState,_ResultValues,NewOutState).

units_execute_statement2(choice(ChoiceList),_,LocalState,InState,OutState,choice) :- !,
    execute_choice_list(ChoiceList,LocalState,InState,OutState).

units_execute_statement2(let(Parameters,Defs,Body),_Infos,LocalState,InState,OutState,let(Path)) :- !,
    units_set_up_localstate(Parameters,_ParaValues,LetLocalState),
    append(LetLocalState,LocalState,ExtendedLocalState),
    units_check_boolean_expression(Defs,ExtendedLocalState,InState),
    units_execute_statement(Body,ExtendedLocalState,InState,OutState,Path).

units_execute_statement2(sequence(Seq),_Infos,LocalState,InState,OutUpdates,Path) :- !,
    ( Seq = [First|Rest] ->
    (Rest == [] -> units_execute_statement(First,LocalState,InState,OutUpdates,Path)
    ; execute_sequence(First,sequence(Rest),LocalState,InState,OutUpdates,Path)
    )
    ; Seq = [] -> OutUpdates = [], Path=[]
    ; add_error_fail(units_execute_statement2,'Illegal argument to sequence: ',Seq)).

units_execute_statement2(while(Cond,Stmt,_Inv,_Variant),_,LocalState,InState,OutState,while) :- !,
    execute_while(Cond,Stmt,LocalState,InState,OutState).

units_execute_statement2(Stmt,_Infos,LocalState,InState,_OutState,_Path) :-
    !, add_error_fail(units_execute_statement2, 'Statement not implemented: ', [Stmt,LocalState,InState]).

units_execute_top_level_operation(Name,FullOperation,InState,NewState,Parameters,Results,Path) :-
    b_interpreter:try_get_op_name(FullOperation, Name),
    units_execute_operation(Name,FullOperation,InState,NewState,Parameters,Results,true,Path).

units_execute_top_level_statement(TExpr,LocalState,InState,OutState,Path) :-
    get_texpr_expr(TExpr,Stmt),
    units_execute_top_level_statement2(Stmt,TExpr,LocalState,InState,OutState,Path).

units_execute_top_level_statement2(precondition(PreCond,Body),_,LocalState,InState,OutState,Path) :-
    !, units_check_boolean_expression(PreCond,LocalState,InState),
    units_execute_statement(Body,LocalState,InState,OutState,Path).

units_execute_top_level_statement2(_,TExpr,LocalState,InState,OutState,Path) :-
    units_execute_statement(TExpr,LocalState,InState,OutState,Path).

units_find_transition(Operation, StateBegin, StateTrans, Paras, Results) :-
    units_execute_top_level_operation(Operation, _, StateBegin, StateTransInter, Paras, Results, Path),
    Path \= precond(false),
    StateTransInter = StateTrans.

units_get_results([],OutState,[],OutState).

units_get_results([R|Results],OutState,[NRV|ResultValues],NewOutState) :-
    def_get_texpr_id(R,ResultId),
    selectchk(bind(ResultId,NRV),OutState,OutState2),
    units_get_results(Results,OutState2,ResultValues,NewOutState).