let rec ------------------------------------------- semantic types ------------
    type Val = IntVal  Int +                 -- Int
               BoolVal Bool +                -- Bool
               ListVal Val Val + NilVal +    -- Lists
               FnVal   (Val -> Val) +        -- abstraction
               Wrong   String                -- error

and type Env == Ide -> Val              -- rho :Env, maps names to their values

and rho0 x = Wrong("undeclared: " @ x)            -- empty, initial environment

-------------------------------------------------------------------------------
and ShowVal (IntVal n)    = itos n ||                        -- : Val -> String
    ShowVal (BoolVal b)   = if b then "T" else "F" ||
    ShowVal (ListVal h t) = "(" @ (ShowVal h) @ "::" @ (ShowVal t) @ ")" ||
    ShowVal  NilVal       = "Nil" ||
    ShowVal (FnVal f)     = "function()" ||
    ShowVal (Wrong s)     = "Wrong: " @ s

and update f x v y = if x=y then v else f y

in let rec --------------------------------------------------------------------
--  E : Exp -> Env -> Val   -- evaluate an expression to a value, given an env'
    E (Ident x)   rho = rho x     ||
    E (Num n)     _   = IntVal n  ||
    E (Boolean b) _   = BoolVal b ||
    E NIL         _   = NilVal    ||

    E (Block isRec Local Body) rho = E Body (D isRec Local rho) ||

    E (Apply Fn Actual) rho = let  FnVal f = E Fn rho  in  f (E Actual rho) ||

    E (LambdaExp x Body) rho = let f v = E Body (update rho x v) in FnVal f ||

    E (IfExp Se Te Fe) rho =
       E (case E Se rho in BoolVal true: Te || BoolVal false: Fe end) rho ||

    E (UExp Opr Argh) rho = U Opr (E Argh rho) ||

    E (BExp Opr A1 A2) rho = B Opr (E A1 rho) (E A2 rho)

--  D : Bool -> Dec -> Env -> Env -------------------------------- Declarations
and D  isRec    L   oldRho =
    let rec
        newRho = DD L (if isRec then newRho else oldRho) oldRho
    and DD (Decs d1 ds) useRho grow = DD d1 useRho (DD ds useRho grow) ||
        DD (Bind x e)   useRho grow = update grow x (E e useRho)
    in newRho

--------------------------------------------------------------------- Operators
and U plusSy  (IntVal n)    = IntVal  n       ||
    U minusSy (IntVal n)    = IntVal  (-n)    ||

    U notSy   (BoolVal b)   = BoolVal (~b)    ||

    U nullSy  (ListVal _ _) = BoolVal false   ||
    U nullSy   NilVal       = BoolVal true    ||
    U hdSy    (ListVal h t) = h               ||
    U tlSy    (ListVal h t) = t

and B consSy h t = ListVal h t                ||

    B opr (IntVal m) (IntVal n) =
       case opr in plusSy  : IntVal( m+n )    ||
                   minusSy : IntVal( m-n )    ||
                   timesSy : IntVal( m*n )    ||
                   divSy   : IntVal( m%n )    ||

                   eqSy    : BoolVal( m=n)    ||
                   neSy    : BoolVal( m~=n )  ||
                   leSy    : BoolVal( m<=n )  ||
                   ltSy    : BoolVal( m<n )   ||
                   geSy    : BoolVal( m>=n )  ||
                   gtSy    : BoolVal( m>n )
       end                                    ||

    B opr (BoolVal p) (BoolVal q) =
       case opr in orSy  : BoolVal( p|q )     ||
                   andSy : BoolVal( p&q )
       end
-------------------------------------------------------------------------------
-- Executable Denotational Semantics of Lambda Calculus / FP
-- Direct style,  coded in Lazy ML (LML)
-- (c) 1994
-- L.Allison, Department of Computer Science, Monash University, Australia