% File 'additive-cr'
 
:- include 'arithmetic'.

:- variables
  V_A,V_A1,V_A2,V_A3,V_A4            :: action;
  V_X,V_I,V_I1                           :: integer;
  V_NNI                              :: nnInteger.

% parsing propositions involving 'increments' and 'decrements'

:- op(1010,xfx,increments).
:- op(1010,xfx,decrements).
:- op(1015,xfx,by).

% definitions of 'increments' and 'decrements'

:- macros 
  #1 increments #2 by #3 if #4 
    -> caused contribution(#1,#2) = #3 if #1 & #4 ;

%  #1 increments #2 by #3 if #4 
%    -> caused contribution(#1,#2) = #3 if #1 & #4 ;

  #1 increments #2 by #3
    -> #1 increments #2 by #3 if true;

  #1 decrements #2 by #3 if #4
    -> caused contribution(#1,#2) = -(#3) if #1 & #4 ;

  #1 decrements #2 by #3 
    -> #1 decrements #2 by #3 if true .

% total order on actions induced by @<

:- macros 
  next(#1,#2) -> (#1 @< #2 & 
                     -([\/V_A2 | (#1 @< V_A2 & V_A2 @< #2)]));
  first(#1) -> -([\/V_A3 | (V_A3 @< #1)]);
  last(#1) ->  -([\/V_A4 | (#1 @< V_A4)]).

% definitions of '<-op-'
:- variables
  V_N1,V_N2,V_N3                     :: integer.

:- op(1010,xfx,<-+-).
:- op(1010,xfx,<---).
:- op(1010,xfx,<-++-).
:- op(1010,xfx,<-+--).
:- op(1010,xfx,<--+-).
:- op(1010,xfx,<----).

:- macros

% when \cal E is (\lambda x. k*x)

  #2 <-+- multiply(#3,#1)
    -> ( caused iContr(#2) = (#3)*(V_N1+V_N2-V_N3)
          if iContr(#1)=V_N1 & dContr(#1)=V_N2 & tContr(#1)=V_N3
           & (#3)*(V_N1+V_N2-V_N3)>=minInt & 
		(#3)*(V_N1+V_N2-V_N3)=<maxInt; 
	 considerRange(#1) );

  #2 <--- multiply(#3,#1)
    -> ( caused iContr(#2) = (#3)*(V_N3-V_N1-V_N2)
          if iContr(#1)=V_N1 & dContr(#1)=V_N2 & tContr(#1)=V_N3
           & (#3)*(V_N1+V_N2-V_N3) >= minInt & 
		(#3)*(V_N1+V_N2-V_N3) =< maxInt;
	 considerRange(#1) );

  #2 <-++- multiply(#3,#1)
    -> caused iContr(#2)= (#3)*V_N3
	 if tContr(#1) = V_N3 & V_N3 >0 & 
		(#3)*V_N3 >= minInt & (#3)*V_N3 =< maxInt;

  #2 <-+-- multiply(#3,#1)
    -> caused iContr(#2)= (#3)*V_N3
         if tContr(#1)=V_N3 & V_N3 <0 & (#3)*V_N3 >= minInt & (#3)*V_N3 =< maxInt;

  #2 <--+- multiply(#3,#1)
    -> caused iContr(#2) = (#3)*(-V_N3)
         if tContr(#1)=V_N3 & V_N3 >0 & (#3)*V_N3 >= minInt & (#3)*V_N3 =< maxInt;

  #2 <---- multiply(#3,#1)
    -> caused iContr(#2) = (#3)*(-V_N3)
        if tContr(#1) = V_N3 & V_N3 <0 & 
		(#3) * V_N3 >= minInt & (#3) * V_N3 =< maxInt.