%%% Evaluating arithmetic expressions
%%% Author: Roberto Virga

%use equality/rationals.

eval_digit : digit X -> rational -> type.

ev_d0 : eval_digit d0 0.
ev_d1 : eval_digit d1 1.
ev_d2 : eval_digit d2 2.
ev_d3 : eval_digit d3 3.
ev_d4 : eval_digit d4 4.
ev_d5 : eval_digit d5 5.
ev_d6 : eval_digit d6 6.
ev_d7 : eval_digit d7 7.
ev_d8 : eval_digit d8 8.
ev_d9 : eval_digit d9 9.

eval_number : number X -> rational -> type.

ev_nd  : eval_number (nd D) Q
           <- eval_digit D Q.

ev_n++ : eval_number (n++ N D) (10 * Q1 + Q2)
           <- eval_digit D Q1
           <- eval_number N Q2.

eval : expression X -> rational -> type.

ev_en : eval (en N) Q
          <- eval_number N Q.

ev_e~ : eval (e~ E) (~ Q)
          <- eval E Q.

ev_e* : eval (e* E2 E1) (Q1 * Q2)
          <- eval E2 Q2
          <- eval E1 Q1.

ev_e+ : eval (e+ E2 E1) (Q1 + Q2)
          <- eval E2 Q2
          <- eval E1 Q1.

ev_e- : eval (e- E2 E1) (Q1 - Q2)
          <- eval E2 Q2
          <- eval E1 Q1.

ev_e/ : eval (e/ E2 E1) Q
          <- eval E2 Q2
          <- eval E1 (Q * Q2).

ev_ep : eval (ep E) Q
          <- eval E Q.