let rec                                                       -- Semantic Types
    type Locn == Int

and type Sv = SvInt Int + SvBool Bool               -- Storable Values
and type Ev = EvInt Int + EvBool Bool + EvLocn Locn -- Expressible Values
and type Dv = DvLocn Locn                           -- Denotable Values
and type Bv = BvInt Int + BvBool Bool               -- Basic Values

and type Store == Locn -> Sv
and type State = st Store Int (List Bv) -- Store, Locn counter, Answer

and type Env == Ide -> Dv

in let                                                      -- utility routines
    update f x v y = if x=y then v else f y

and SvtoEv (SvInt n)  = EvInt n

and EvtoSv (EvInt n)  = SvInt n  || EvtoSv (EvBool b)  = SvBool b
and EvtoDv (EvLocn l) = DvLocn l
and EvtoBv (EvInt n)  = BvInt n  || EvtoBv (EvBool b)  = BvBool b

and DvtoEv (DvLocn l) = EvLocn l

and rec
    show [] = [] ||
    show (BvInt n  . t) = itos n @ " " @ show t  ||
    show (BvBool b . t) = (if b then "T" else "F") @ " " @ show t

in let rec                                                                 -- C
    C (Cmds g1 g2)    env s = C g2 env (C g1 env s)  ||

    C (Assign e1 e2)  env s =
       let EvLocn l, s2 = L e1 env s
       in  let v, st s f a = R e2 env s2
           in  st (update s l (EvtoSv v)) f a  ||

    C (IfCmd be gt gf) env s = let EvBool v, s2 = R be env s
                               in  C (if v then gt else gf) env s2  ||

    C (WhileCmd be g)  env s = let EvBool v, s2 = R be env s
                               in if v then C (WhileCmd be g) env (C g env s2)
                                          else s2  ||

    C (Block d g)     env s = uncurry (C g) (D d env s)  ||

    C (Write e)       env s = let v, st s f a = R e env s
                              in  st s f (a @ [EvtoBv v])


and E (Ident x) env s = DvtoEv(env x), s  ||                               -- E

    E (Num n)   env s = EvInt n, s ||

    E (UExp op e) env s = let v, s2 = R e env s
                          in  U op v, s2  ||

    E (BExp op e1 e2) env s =
       let v1, s2 = R e1 env s
       in  let v2, s3 = R e2 env s2
           in  O op v1 v2, s3


and L e env s = let EvLocn l, s2 = E e env s                               -- L
                in  EvLocn l, s2

and R e env s = case E e env s in                                          -- R
                EvLocn l, st s f a: SvtoEv(s l), st s f a ||
                v, s2             : v, s2
                end


and D (VarDec x) env (st s f a) = update env x (DvLocn f), st s (f+1) a  ||-- D

    D (Decs d1 d2) env s = uncurry (D d2) (D d1 env s)


and U plusSy  (EvInt n) = EvInt n    ||                                    -- U
    U minusSy (EvInt n) = EvInt(-n)  ||
    U not     (EvBool true) = EvBool false    ||
    U not     (EvBool false) = EvBool true


and O plusSy  (EvInt n1) (EvInt n2) = EvInt (n1+n2)  ||                    -- O
    O minusSy (EvInt n1) (EvInt n2) = EvInt (n1-n2)  ||
    O timesSy (EvInt n1) (EvInt n2) = EvInt (n1*n2)  ||
    O divSy   (EvInt n1) (EvInt n2) = EvInt (n1/n2)  ||

    O eqSy    v1 v2 = EvBool(v1=v2)  ||
    O neSy    v1 v2 = EvBool(v1~=v2) ||
    O gtSy    (EvInt n1) (EvInt n2) = EvBool (n1 >  n2)  ||
    O geSy    (EvInt n1) (EvInt n2) = EvBool (n1 >= n2)  ||
    O ltSy    (EvInt n1) (EvInt n2) = EvBool (n1 <  n2)  ||
    O leSy    (EvInt n1) (EvInt n2) = EvBool (n1 <= n2)  ||

    O andSy   (EvBool b1) (EvBool b2) = EvBool (b1 & b2) ||
    O orSy    (EvBool b1) (EvBool b2) = EvBool (b1 | b2)


--\fB Direct Semantics in LML. \fP
-- L.Allison, Department of Computer Science, Monash University, Australia