% Computation semantics for the language
% of arithmetic expressions. Adapted
% from M. Hennessy: The Semantics of
% Programming Languages (Wiley, 1990).

module comput_arith.

  accumulate arith_abstract_syntax, rtc.
  
  % the reducesto relation
  
              (ap Oper V1 V2 N)
  => % ------------------------------------
      (reducesto (op Oper (num V1) (num V2))
                 (num N)).
  
            (reducesto E1 E1')
  => % ----------------------------
        (reducesto (op Oper E1 E2)
                   (op Oper E1' E2)).
  
            (reducesto E2 E2')
  => % --------------------------
       (reducesto (op Oper (num V1) E2)
                  (op Oper (num V1) E2')).

  % the output relation  
  (output_fun (num N) N).

  % auxilliary semantic relations
  local ap      operator -> int -> int
  			 -> int -> o.
  (ap add N1 N2 Ans) :- Ans is N1 + N2.
  (ap sub N1 N2 Ans) :- Ans is N1 - N2.
  (ap mult N1 N2 Ans) :- Ans is N1 * N2.