** Sample solution to SE304 Lab 5
** Author: Gareth Carter

** Question 1
** parse in SIMPLE-INT : M + M + M .
** Explain why you are offered two choices.
**
** CafeOBJ has no knowledge of the operator +.
** The system does not know if it is supposed parse the term from left to right,
** or from right to left. In traditional algebra, the + operator is associative on
** integers, so it would make no difference, but CafeOBJ has no knowledge of
** addition yet, so it cannot make that inference. Hence, two possible parses are
** presented.


module SIMPLE-NAT {

  [Zero NzNat < Nat]

** Define the signatures of the operations of the SIMPLE-NAT module
  op 0 : -> Zero
  op s : Nat -> Nat
  op _+_ : Nat Nat -> Nat
  op _*_ : Nat Nat -> Nat

** Define the meanings of the operations
  vars X, Y : Nat    ** using these variables

  ** Definition of +
  eq 0 + X = X .                     ** base case
  ** 0 + 6 = 6
  eq s(X) + Y = s(X + Y) .           ** recursive case
  ** s(4) + 5 = s(4 + 5)


  ** Definition of *
  eq 0 * X = 0 .                     ** base case
  ** 0 * 5 = 0
  eq s(X) * Y = Y + (X * Y) .        ** recusive case
  ** s(3) * 5 = 5 + (3 * 5)

}

** Run this through CafeOBJ to see the reduction of these terms

open SIMPLE-NAT .
  red s(s(0)) + s(s(s(s(0)))) .
  red s(s(s(0))) * s(s(s(s(s(0))))) .
close