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

%use equality/integers.

eval_digit : digit X -> integer -> 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 -> integer -> 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 -> integer -> 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).

%abbrev >< : expression "10*9+35"
   = e* (e+ (en (n++ (nd d5) d3)) (en (nd d9))) (en (n++ (nd d0) d1)).

%solve
exp : expression "10*9+35".

%query 1 *
eval exp Q.