***********************************************************
* A Monadic Semantics for the ISWIM Language              *
***********************************************************

Modified by Paul Liu.
Written by Paul Hudak.

> -- need glasgow extension to make function instances of Eq and Show
> {-# OPTIONS -fglasgow-exts #-}

> module ISWIM where

SYNTAX
======

Some type synonyms to use Reynolds names:

> type NatConst  = Int		-- but should not include negative numbers
> type BoolConst = Bool
> type Tag       = NatConst

> data Exp = 
> -- constants:
>     NatConst NatConst		-- integer literals
>   | BoolConst BoolConst	-- booleans
>   | Nil			-- nil
> -- arithmetic:
>   | Neg Exp			-- negation
>   | Exp :+: Exp		-- addition
>   | Exp :-: Exp		-- subtraction
>   | Exp :*: Exp		-- multiplication
>   | Exp :/: Exp		-- division
>   | Exp `Rem` Exp		-- remainder
> -- relational operators:
>   | Exp :=:  Exp		-- equality
>   | Exp :/=: Exp		-- inequality
>   | Exp :<:  Exp		-- less than
>   | Exp :<=: Exp		-- less than or equal
>   | Exp :>:  Exp		-- greater than
>   | Exp :>=: Exp		-- greater than or equal
> -- logical operators:
>   | Not Exp			-- negation
>   | Exp :/\:  Exp		-- conjunction (and)
>   | Exp :\/:  Exp		-- disjunction (or)
>   | Exp :=>:  Exp		-- implication
>   | Exp :<=>: Exp		-- if and only if
> -- conditional:
>   | If Exp Exp Exp            -- conditional
> -- variables, lambdas, and applications:
>   | Var Var			-- variables
>   | App Exp Exp		-- applications
>   | Lam Pat Exp		-- functions with pattern arguments
> -- tuples:
>   | Tup [Exp]			-- tuples
>   | Prj Exp Tag		-- tuple projection
> -- sums:
>   | Sum Tag Exp		-- sums (i.e. alternatives; tagged values)
>   | SumCase Exp [Exp]		-- sum discrimination (i.e. case)
> -- errors:
>   | Error			-- run-time error
> -- binding forms:
>   | Let    [(Pat,Exp)] Exp	-- let expression
>   | LetRec [(Var,Pat,Exp)] Exp-- recursive let expression
> -- reference
>   | NewRef Exp                -- new reference
>   | Exp ::= Exp               -- assignment
>   | Exp :==: Exp              -- test for reference equality
>   | Val Exp                   -- dereference
> -- sequencing
>   | Exp ::: Exp               -- sequencing
> -- exception
>   | Raise Label               -- raise exception
>   | Catch Label Exp Exp       -- catch and handle exception 
>   deriving (Eq, Show)
>
> data Pat = Pat1 Var
>          | Pat2 [Pat]
>   deriving (Eq, Show)

Variables are just strings:

> type Var = String

Label is just String

> type Label = String

FIXITIES
========

> infixl 9 :*:, :/:, `Rem`
> infixl 8 :-:, :+:
> infix  7 :=:, :/=:, :<:, :>:, :<=:, :>=:
> infixl 6 :/\:
> infixl 5 :\/:
> infixr 4 :=>:
> infixr 3 :<=>:
> infixr 2 ::=
> infixr 1 :::

SEMANTIC DOMAINS
================

> data Value a  = Norm a
>               | DynErr Label
>               | TypErr
>               deriving (Eq, Show)
>
> data V     = VInt  Int
>            | VBool Bool
>            | VNil
>            | VTup  [V]
>            | VSum  (Int, V)
>            | VFun  (V -> M V)
>            | VRef  Int
>            deriving (Eq, Show)
>
> nil   = Norm VNil

> instance Show (V -> M V) where
>   show f = "[Function]"
>
> instance Eq (V -> M V) where
>   f == g  =  False

AUXILIARY FUNCTIONS 
===================

Projections:

> i_norm = Norm
>
> i_int  = VInt
> i_bool = VBool
> i_tup  = VTup
> i_alt  = VSum
> i_fun  = VFun
> i_ref  = VRef

ENVIRONMENTS
============

> type Env = Var -> V
>
> extend :: Env -> Var -> V -> Env
> extend e v i v' = if v == v' then i else e v'

So "extend s v i" is equivalent to "s [v:i]" in Reynolds.

> emptyEnv x = error ("Unbound variable: " ++ x)

STATES
======

State stores values for references.

> type State = [V]

> emptyState = []

MONAD
=====

We'll make error handling and state into Monad.

> data M a = M (State -> (State, Value a))

> instance Monad M where
>    return v = M (\s -> (s, Norm v))
>    (M f) >>= g = M (\s ->
>       let (s', v) = f s
>       in case v of
>         Norm v' -> let M g' = g v'
>                    in g' s'
>         DynErr l -> (s', DynErr l)
>         TypErr -> (s', TypErr))

Monadic operations for State.

> newRef :: V -> M Int
> newRef v = M (\s -> let s' = s ++ [v] in (s', Norm (length s)))

> valRef :: Int -> M V
> valRef i = M (\s -> if i >= 0 && i < length s 
>                         then (s, Norm (s!!i))
>                         else (s, DynErr "Invalid reference"))

> assignRef :: Int -> V -> M V
> assignRef i v = M (\s -> if i >=0 && i < length s
>                         then (take i s ++ [v] ++ drop (i+1) s, Norm v)
>                         else (s, DynErr "Invalid reference"))
>                         

Monadic operation for Error.

> dynErr :: Label -> M a
> dynErr l = M (\s -> (s, DynErr l))

> typErr :: M a
> typErr = M (\s -> (s, TypErr))

> catchErr :: Label -> M a -> M a -> M a
> catchErr l (M f) (M g) = M h
>       where h s = case f s of
>                       (s', DynErr l') | l == l' -> g s'
>                       v -> v

Type checking are now Monadic operation

> t_int ::  V -> M Int
> t_int (VInt v) = M (\s -> (s, Norm v))
> t_int  _       = typErr
>
> t_bool :: V -> M Bool
> t_bool (VBool v) = M (\s -> (s, Norm v))
> t_bool  _        = typErr
>
> t_tup :: V -> M [V]
> t_tup (VTup v) = M (\s -> (s, Norm v))
> t_tup _        = typErr

> t_alt :: V -> M (Int,V)
> t_alt (VSum v) = M (\s -> (s, Norm v))
> t_alt _        = typErr
>
> t_fun :: V -> M (V -> M V)
> t_fun (VFun v) = M (\s -> (s, Norm v))
> t_fun _        = typErr
>
> t_ref ::  V -> M Int
> t_ref (VRef v) = M (\s -> (s, Norm v))
> t_ref  _       = typErr
>

Syntax Expansion
================

An infinite supply of fresh variabes, using the convention that no
variable name in the program begins with "_":

> names = map (("_"++).show) [0..]

SEMANTICS
=========

After desugaring:

> mean :: Exp -> Env -> M V
> -- constants:
> mean Nil          eta  = return VNil
> mean Error        eta  = dynErr "Error"
> mean (NatConst k) eta  = return (i_int  k)
> mean (BoolConst b) eta = return (i_bool b)
>
> -- unops:
> mean (Neg e) eta = mean e eta >>= t_int >>= return . i_int . negate
> mean (Not e) eta = mean e eta >>= t_bool >>= return . i_bool . not
>
> mean (e :+:  e') eta  = binop e e' t_int i_int (+) eta 
> mean (e :-:  e') eta  = binop e e' t_int i_int (-) eta 
> mean (e :*:  e') eta  = binop e e' t_int i_int (*) eta 
> mean (e :/=: e') eta  = binop e e' t_int i_bool (/=) eta 
> mean (e :<:  e') eta  = binop e e' t_int i_bool (<) eta 
> mean (e :>:  e') eta  = binop e e' t_int i_bool (>) eta 
> mean (e :<=: e') eta  = binop e e' t_int i_bool (<=) eta 
> mean (e :>=: e') eta  = binop e e' t_int i_bool (>=) eta 
> mean (e :/\: e') eta  = binop e e' t_bool i_bool (&&) eta 
> mean (e :\/: e') eta  = binop e e' t_bool i_bool (>) eta 
> mean (e :=>: e') eta  = binop e e' t_bool i_bool f eta 
>   where f b b' = if b then b' else True   -- not b || b'
> mean (e :<=>: e') eta = binop e e' t_bool i_bool f eta 
>   where f b b' = if b then b' else not b' -- (b&&b')||(not (b||b'))
> mean (e :=:  e') eta  = binop e e' return i_bool (==) eta 

> -- division and remainder:
> mean (e :/: e') eta = mean e eta >>= t_int >>= \i ->
>                       mean e' eta >>= t_int >>= \i' ->
>                       if (i' == 0) then dynErr "Division by zero"
>                                    else return (i_int (i `div` i'))
>
> mean (e `Rem` e') eta = mean e eta >>= t_int >>= \i ->
>                         mean e' eta >>= t_int >>= \i' ->
>                         if (i' == 0) then dynErr "Rem by zero"
>                                      else return (i_int (i `rem` i'))

> -- conditional
> mean (If b c a)  eta = mean b eta >>= t_bool >>= \t ->
>                        if t then mean c eta else mean a eta
>
> -- vars, apps, and lambdas:
> mean (Var v) eta = return (eta v)
>
> mean (App e e') eta = mean e eta >>= t_fun >>= \f ->
>                       mean e' eta >>= f
>
> mean (Lam (Pat1  v) e) eta = return (i_fun (\z -> (mean e) (extend eta v z)))
>
> mean (Lam (Pat2 ps) e) eta = 
>   error "Lambda patterns should be desugared."
>
> -- tuples
> mean (Tup es) eta = aux es >>= \vs ->
>                     return (i_tup vs)
>   where aux [] = return []
>         aux (e:es) = mean e eta >>= \v ->
>                      aux es >>= \vs ->
>                      return (v:vs)
>
> mean (Prj e k) eta = mean e eta >>= t_tup >>= \ts ->
>                      if k < length ts
>                        then return (ts !! k)
>                        else dynErr "Out of bound"
>
> -- sums:
> mean (Sum k e) eta = mean e eta >>= \v ->
>                      return (i_alt (k, v))
>
> mean (SumCase e fs) eta = mean e eta >>= t_alt >>= \(k,z) -> 
>                           if k < length fs 
>                             then mean (fs!!k) eta >>= t_fun >>= \f -> f z
>                             else dynErr "Out of bound"
>
> -- let expression:
> mean (Let eqns e) eta = error "Let expression should be desugared."
>
> -- recursive let:
> mean (LetRec eqns e) eta = 
>   let eta' = foldr f eta eqns
>       f (v,Pat1 u,e) eta = extend eta v 
>                              (i_fun (\z -> mean e (extend eta' u z)))
>   in mean e eta'

> -- extensions:
> mean (Raise l) eta = dynErr l
> mean (Catch l e e') eta = catchErr l (mean e eta) (mean e' eta)
> mean (e ::: e') eta = mean e eta >> mean e' eta
> mean (e ::= e') eta = mean e eta >>= t_ref >>= \i ->
>                   mean e' eta >>= \v -> assignRef i v
> mean (e :==: e') eta = mean e eta >>= t_ref >>= \i ->
>                    mean e' eta >>= t_ref >>= \i' -> return (i_bool (i == i'))
> mean (NewRef e) eta = mean e eta >>= newRef >>= return . i_ref
> mean (Val e) eta = mean e eta >>= t_ref >>= valRef

> -- binops:
> binop :: Exp -> Exp -> (V -> M a) -> (b -> V) -> (a -> a -> b) -> Env -> M V
> binop e e' t_v i_v f eta
>     = mean e eta  >>= t_v >>= \i -> 
>       mean e' eta >>= t_v >>= \i' -> 
>       return (i_v (f i i'))


DESUGARING
==========

Top-level desugaring:

> desugar :: Exp -> Exp
> desugar e = desug e [] names

Main desugaring function:

> desug :: Exp -> [(Var,Exp)] -> [Var] -> Exp
> -- constants:
> desug Nil           as vs = Nil
> desug Error         as vs = Error
> desug (NatConst k)  as vs = NatConst k
> desug (BoolConst b) as vs = BoolConst b
>
> -- unops:
> desug (Neg e) as vs   = Neg (desug e as vs)
> desug (Not e) as vs   = Not (desug e as vs)
> desug (Prj e k) as vs = Prj (desug e as vs) k
> desug (Sum k e) as vs = Sum k (desug e as vs)
>
> -- binops:
> desug (e :+:   e') as vs = bDesug e e' (:+:)  as vs
> desug (e :-:   e') as vs = bDesug e e' (:-:)  as vs
> desug (e :*:   e') as vs = bDesug e e' (:*:)  as vs
> desug (e :=:   e') as vs = bDesug e e' (:=:)  as vs
> desug (e :/=:  e') as vs = bDesug e e' (:/=:) as vs
> desug (e :<:   e') as vs = bDesug e e' (:<:)  as vs
> desug (e :>:   e') as vs = bDesug e e' (:>:)  as vs
> desug (e :<=:  e') as vs = bDesug e e' (:<=:) as vs
> desug (e :>=:  e') as vs = bDesug e e' (:>=:) as vs
> desug (e :/\:  e') as vs = bDesug e e' (:/\:) as vs
> desug (e :\/:  e') as vs = bDesug e e' (:\/:) as vs
> desug (e :=>:  e') as vs = bDesug e e' (:=>:) as vs
> desug (e :<=>: e') as vs = bDesug e e' (:<=>:)as vs
> desug (e :/:   e') as vs = bDesug e e' (:/:)  as vs
> desug (e `Rem` e') as vs = bDesug e e'  Rem   as vs
> desug (App  e  e') as vs = bDesug e e'  App   as vs
>
> -- ternary op:
> desug (If b c a) as vs =
>   If (desug b as vs) (desug c as vs) (desug a as vs)
>
> -- n-ary ops:
> desug (Tup es)       as vs = 
>   Tup (map (\e -> desug e as vs) es)
> desug (SumCase e fs) as vs = 
>   SumCase (desug e as vs) (map (\e -> desug e as vs) fs)
>
> -- variables:
> desug (Var v) as vs = lookUp v as
>
> -- lambda:
> desug (Lam (Pat1  v) e) as    vs  = Lam (Pat1 v) (desug e as vs)
> desug (Lam (Pat2 ps) e) as (v:vs) =
>   let as' = depat ps (Var v) 0
>   in Lam (Pat1 v) (desug e (as'++as) vs)
>
> -- let expression:
> desug (Let eqns exp) as vs = 
>   desug (expand eqns) as vs
>   where expand  []          = exp
>         expand ((p,e):eqns) = App (Lam p (expand eqns)) e
>
> -- recursive let:
> desug (LetRec eqns e) as vs =
>   LetRec (map f eqns) (desug e as vs)
>   where f (v,p,e) =
>              let Lam p' e' = desug (Lam p e) as vs
>              in (v,p',e')

> -- extensions
> desug (e ::: e') as vs = bDesug e e' (:::) as vs
> desug (e ::= e') as vs = bDesug e e' (::=) as vs
> desug (NewRef e) as vs = NewRef (desug e as vs)
> desug (Val e) as vs = Val (desug e as vs)
> desug (Catch l e e') as vs = bDesug e e' (Catch l) as vs
> desug (Raise l) as vs = Raise l

Auxilary functions for desugaring:

Binary operators:

> bDesug e1 e2 op as vs = desug e1 as vs `op` desug e2 as vs

Variable lookup:

> lookUp v as = case lookup v as of
>                 Just e  -> e
>                 Nothing -> Var v
>                         -- error ("Unknown variable: " ++ v)

Compiling patterns:

> depat []     e n = []
> depat (p:ps) e n = dep1 p e n ++ depat ps e (n+1)

> dep1 (Pat1 v)  e n = [(v, Prj e n)]
> dep1 (Pat2 ps) e n = depat ps (Prj e n) 0

RUN PROGRAM
===========

> test :: Exp -> Value V
> test e = let M f = mean (desugar e) emptyEnv
>              (_, v) = f emptyState
>          in v

TESTS
=====

> tpats = [Pat1 "a", Pat2 [Pat1 "b", Pat1 "c"], Pat1 "d"]
> t1 = depat tpats (Var "v") 0

t1 ==> [("a", Prj (Var "v") 0),
        ("b", Prj (Prj (Var "v") 1) 0),
        ("c", Prj (Prj (Var "v") 1) 1),
        ("d", Prj (Var "v") 2)]

> tlam = Lam (Pat2 tpats) (Var "b" :+: Var "d")
> t2 = desugar tlam

t2 ==> Lam (Pat1 "v0") (Prj (Prj (Var "v0") 1) 0 :+: Prj (Var "v0") 2)

Complete programs:
------------------

 test p = meaning p emptyE

Factorial:

> p1 = LetRec [("fac", Pat1 "n", 
>               If (Var "n" :=: NatConst 0)
>                  (NatConst 1)
>                  (Var "n" :*: App (Var "fac") (Var "n" :-: NatConst 1))
>              )]
>        (App (Var "fac") (NatConst 5))

test p1 ==> Norm (VInt 120)

Lists:

> listFns = [(Pat1 "cons",
>            Lam (Pat2 [Pat1 "x", Pat1 "xs"]) (Tup [Var "x", Var "xs"])),
>           (Pat1 "car",
>            Lam (Pat1 "xs") (Prj (Var "xs") 0)),
>           (Pat1 "cdr",
>            Lam (Pat1 "xs") (Prj (Var "xs") 1)),
>           (Pat1 "null",
>            Lam (Pat1 "xs") (Var "xs" :=: Nil))]

> alist = [(Pat1 "l1",
>           App (Var "cons") 
>               (Tup [NatConst 1,
>                     (App (Var "cons")
>                          (Tup [NatConst 2, Nil]))]))]

> p2 = Let (listFns++alist)
>          (App (Var "cdr") (Var "l1"))

test p2 ==> Norm (VTup [VInt 2,VNil])

These are from Reynolds: reduce (fold) and append (defined using reduce):

> red = ("reduce",
>        Pat2 [Pat1 "x", Pat1 "f", Pat1 "a"],
>        If (App (Var "null") (Var "x"))
>           (Var "a")
>           (App (App (Var "f") (App (Var "car") (Var "x")))
>                (App (Var "reduce") (Tup [App (Var "cdr") (Var "x"),
>                                          Var "f",
>                                          Var "a"]))))

> app = (Pat1 "append",
>        Lam (Pat2 [Pat1 "x", Pat1 "y"])
>            (App (Var "reduce")
>                 (Tup [Var "x",
>                       Lam (Pat1 "i")
>                           (Lam (Pat1 "z")
>                                (App (Var "cons") 
>                                     (Tup [Var "i",Var "z"]))),
>                       Var "y"])))

Test of append:

> p3 = Let (listFns++alist)
>          (LetRec [red]
>                  (Let [app]
>                       (App (Var "append")
>                            (Tup [Var "l1", Var "l1"]))))

test p3 ==> Norm (VTup [VInt 1,VTup [VInt 2,VTup [VInt 1,VTup [VInt 2,VNil]]]])

> -- test for Catch and Raise

> p4  = Let [(Pat1 "x", NewRef (NatConst 1))] 
>       (Catch "cold" (Catch "cold" (Var "x" ::= NatConst 42 ::: Raise "cold")
>                                   (Var "x" ::= NatConst 24))
>                     (Var "x" ::= NatConst 0) :::
>                     (Val (Var "x"))) -- Norm (VInt 24)
> p4' = Let [(Pat1 "x", NewRef (NatConst 1))]
>       (Catch "cold" (Catch "flu"  (Var "x" ::= NatConst 42 ::: Raise "cold")
>                                   (Var "x" ::= NatConst 24))
>                     (Var "x" ::= NatConst 0) :::
>                     (Val (Var "x"))) -- Norm (VInt 0)

More test cases (copied from Eric Cheng's PS7 submission)

> test0 = Prj (Tup [NatConst 1, NatConst 2]) 1 -- Norm (VInt 2)
> test1 = Prj (Tup [NatConst 1, NatConst 2]) 0 -- Norm (VInt 1)
> test2 = Prj (Tup [NatConst 1, NatConst 2]) 2 -- Err DynErr
> test4 = App (Lam (Pat1 "x") (Var "x" :+: NatConst 1)) (NatConst 1) -- Norm (VInt 2)
> test5 = App (Lam (Pat2 [Pat1 "x"]) (Var "x" :+: NatConst 1)) (Tup [NatConst 1]) -- Norm (VInt 2)

> -- tests for references
> test6 = Let [(Pat1 "r1", NewRef (NatConst 1))] (Val (Var "r1")) -- Norm (VInt 1)
> test7 = Let [(Pat1 "r1", NewRef (NatConst 1)),
>              (Pat1 "v1", Val (Var "r1")),
>              (Pat1 "v2", Var "r1" ::= NatConst 2),
>              (Pat1 "v3", Val (Var "r1"))] (Tup [Var "v1", Var "v2", Var "v3"]) -- Norm (VTup [VInt 1,VInt 2,VInt 2])
> test8 = Let [(Pat1 "r1", NewRef (NatConst 1)),
>              (Pat1 "r2", Var "r1"),
>              (Pat1 "v1", Var "r1" ::= NatConst 2),
>              (Pat1 "v2", Val (Var "r2")),
>              (Pat1 "v3", Var "r1" :=: Var "r2"),
>              (Pat1 "v4", Var "r1" :=: Var "r2")] (Tup [Var "v1", Var "v2", Var "v3", Var "v4"]) -- Norm (VTup [VInt 2,VInt 2,VBool True,VBool True])
>
> -- test if newref preserves semantics
> test9 = Let [(Pat1 "r1", NewRef (NatConst 1)),
>              (Pat1 "r2", NewRef (NatConst 2)),
>              (Pat1 "_", Var "r1" ::= NatConst 3),
>              (Pat1 "r4", NewRef (NatConst 4))]
>             (Tup [Val (Var "r1"), Val (Var "r2"), Val (Var "r4")]) -- Norm (VTup [VInt 3,VInt 2,VInt 4])
>
> incr = (Pat1 "incr", Lam (Pat1 "r") (Var "r" ::= Val (Var "r") :+: (NatConst 1)))
>
> -- test for sequencing operator
> test10 = Let [(Pat1 "r1", NewRef (NatConst 1)), incr]
>              (App (Var "incr") (Var "r1") :::
>               App (Var "incr") (Var "r1") :::
>               App (Var "incr") (Var "r1") :::
>               Val (Var "r1")) -- Norm (VInt 4)