||*************************************************************************||
|| Semantics with Applications: A formal introduction                      ||
|| --- Appendix B: Introduction to Miranda Implementations (appB.m)        ||
|| Hanne Riis Nielson & Flemming Nielson                                   ||
||*************************************************************************||

||-------------------------------------------------------------------------||
|| Abstract Syntax                                                         ||
||-------------------------------------------------------------------------||

var == [char]

aexp ::= N num | V var | Add aexp aexp |
         Mult aexp aexp | Sub aexp aexp

bexp ::= TRUE | FALSE | Eq aexp aexp | Le aexp aexp | 
         Neg bexp | And bexp bexp

stm  ::= Ass var aexp | Skip | Comp stm stm | 
         If bexp stm stm | While bexp stm

factorial = Comp (Ass "y" (N 1)) 
                 (While (Neg (Eq (V "x") (N 1)))
                        (Comp (Ass "y" (Mult (V "y") (V "x")))
                              (Ass "x" (Sub (V "x") (N 1)))))

||-------------------------------------------------------------------------||
|| Evaluation of expressions                                               ||
||-------------------------------------------------------------------------||

z == num
t == bool

state == var -> z

s_init "x" = 3
s_init y   = 0

a_val :: aexp -> state -> z
b_val :: bexp -> state -> t

a_val (N n) s        = n
a_val (V x) s        = s x
a_val (Add a1 a2) s  = (a_val a1 s) + (a_val a2 s)
a_val (Mult a1 a2) s = (a_val a1 s) * (a_val a2 s)
a_val (Sub a1 a2) s  = (a_val a1 s) - (a_val a2 s)

b_val TRUE s        = True
b_val FALSE s       = False
b_val (Eq a1 a2) s  = True,  if a_val a1 s = a_val a2 s
                    = False, otherwise
b_val (Le a1 a2) s  = True,  if a_val a1 s <= a_val a2 s
                    = False, otherwise
b_val (Neg b) s     = True,  if b_val b s = False
                    = False, if b_val b s = True
b_val (And b1 b2) s = True,  if b_val b1 s = True & b_val b2 s = True
                    = False, otherwise