***********************************************************************
* A realization of the syntax and DIRECT denotational semantics for   *
* SIL: A "Simple Imperative Language", from Chapter 2 of the text.    *
* Also has "catch" command (labelled exceptions).                     *
***********************************************************************

Written by Paul Hudak, September 21, 2003.
Modified October 20, 2003 to include catch (labelled exceptions).

> module SIL where

SYNTAX
======

Syntax of integer expressions:

> data IntExp = 
>     EInt Integer		-- constants
>   | EVar Var			-- variables
>   | Neg IntExp		-- negation
>   | IntExp :+: IntExp		-- addition
>   | IntExp :-: IntExp		-- subtraction
>   | IntExp :*: IntExp		-- multiplication
>   | IntExp :/: IntExp		-- division
>   | IntExp `Rem` IntExp	-- remainder
>   deriving (Eq, Show)

Syntax of boolean expressions:

> data BoolExp =
>     TrueB | FalseB		-- constants
>   | IntExp :=:  IntExp	-- equality
>   | IntExp :/=: IntExp	-- inequality
>   | IntExp :<:  IntExp	-- less than
>   | IntExp :<=: IntExp	-- less than or equal
>   | IntExp :>:  IntExp	-- greater than
>   | IntExp :>=: IntExp	-- greater than or equal
>   | Not BoolExp		-- negation
>   | BoolExp :/\:  BoolExp	-- conjunction (and)
>   | BoolExp :\/:  BoolExp	-- disjunction (or)
>   | BoolExp :=>:  BoolExp	-- implication
>   | BoolExp :<=>: BoolExp	-- if and only if
>   deriving (Eq, Show)

Variables are just strings:

> type Var = String

Syntax of commands:

> data Command =
>     Var := IntExp
>   | Skip
>   | Command ::: Command
>   | If BoolExp Command Command
>   | While BoolExp Command
>   | Newvar Var IntExp Command
>   | For Var IntExp IntExp Command
>   | Fail Label
>   | Catch Label Command Command
>   deriving (Eq, Show)

Labels are just strings:

> type Label = String

Operator fixities (i.e. associativity and precedence):

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

The above is just as defined in Reynolds, except that:
(a) The prefix operators (Neg and Not) are not included because they
    are just functions in Haskell, and thus always have higher precedence
    than any infix operator.
(b) Reynolds says that each infix operator should be left associative, 
    but I don't like that, so I made the following changes:
    (i)  I did not give the relational operators (:=:, :<:, etc.) ANY
         associativity, since it doesn't make sense to write, for 
         example, x :>: y :>: z.  Similarly, assignment should have no
         associativity since it doesn't make sense to write x := y := z.
    (ii) I think that implication should be RIGHT asssociative; i.e.
         a => b => c should be parsed as a => (b => c).

States
======

States (really, environments) map variables to integers:

> type Sigma = Var -> Integer

We can extend states using function variation:

> extend :: Sigma -> Var -> Integer -> Sigma
> extend s v i v' = if v == v' then i else s v'

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

Answers either terminate or abort:

> data Omega = Term  Sigma
>            | Abort Label Sigma

SEMANTICS
=========

Semantic function for integer expressions:

> intExp :: IntExp -> Sigma -> Integer
>
> intExp (EInt i)      s = i
> intExp (EVar v)      s = s v
> intExp (Neg e)       s = - intExp e s
> intExp (e1 :+: e2)   s = intExp e1 s + intExp e2 s
> intExp (e1 :-: e2)   s = intExp e1 s - intExp e2 s
> intExp (e1 :*: e2)   s = intExp e1 s * intExp e2 s
> intExp (e1 :/: e2)   s = intExp e1 s `div` intExp e2 s
> intExp (e1 `Rem` e2) s = intExp e1 s `rem` intExp e2 s

Semantic function for boolean expressions:

> boolExp :: BoolExp -> Sigma -> Bool
>
> boolExp TrueB  s = True
> boolExp FalseB s = False
> boolExp (e1 :=:  e2)  s = intExp e1 s == intExp e2 s
> boolExp (e1 :/=: e2)  s = intExp e1 s /= intExp e2 s
> boolExp (e1 :<:  e2)  s = intExp e1 s <  intExp e2 s
> boolExp (e1 :<=: e2)  s = intExp e1 s <= intExp e2 s
> boolExp (e1 :>:  e2)  s = intExp e1 s >  intExp e2 s
> boolExp (e1 :>=: e2)  s = intExp e1 s >= intExp e2 s
> boolExp (Not p)       s = not (boolExp p s)
> boolExp (p1 :/\:  p2) s = boolExp p1 s && boolExp p2 s
> boolExp (p1 :\/:  p2) s = boolExp p1 s || boolExp p2 s
> boolExp (p1 :=>:  p2) s = if boolExp p1 s then boolExp p2 s else True
> boolExp (p1 :<=>: p2) s = if boolExp p1 s then boolExp p2 s
>                           else not (boolExp p2 s)

Semantic function for commands:

> command :: Command -> Sigma -> Omega
>
> command (v := e)        s = Term (extend s v (intExp e s))
> command (If b c1 c2)    s = if boolExp b s then command c1 s
>                                            else command c2 s
> command Skip            s = Term s
> command (c1 ::: c2)     s = command c2 *** (command c1 s)
> command (While b c)     s = y f s
>                             where f g s = if boolExp b s 
>                                           then g *** command c s
>                                           else Term s
> command (Newvar v e c)  s = (\s' -> extend s' v (s v)) +++
>                             (command c (extend s v (intExp e s)))
> command (For v e0 e1 c) s =
>   command (Newvar v e0 (While (EVar v :<=: e1) 
>                               (c ::: v := EVar v :+: EInt 1))) s
> command (Fail l)        s = Abort l s
> command (Catch l c0 c1) s = 
>         case (command c0 s) of
>           Term s'     -> Term s'
>           Abort l' s' -> if l==l' then command c1 s'
>                                   else Abort l' s'

> (***) :: (Sigma -> Omega) -> Omega -> Omega
>
> f *** (Term s)    = f s
> f *** (Abort l s) = Abort l s

> (+++) :: (Sigma -> Sigma) -> Omega -> Omega
>
> f +++ (Term s)    = Term (f s)
> f +++ (Abort l s) = Abort l (f s)

The fixpoint operator:

> y :: (a -> a) -> a
> y f = f (y f)

EXAMPLES
========

Initial state that maps all variables to zero:

> s0 :: Sigma
> s0 v = 0

Some test programs:

> fac :: Integer -> Command
> fac n = "v" := EInt n   :::
>         "r" := EInt 1   :::
>         While (EVar "v" :>: EInt 0)
>               ("r" := EVar "r" :*: EVar "v" :::
>                "v" := EVar "v" :-: EInt 1      ) :::
>         "main" := EVar "r"

Note that the above program has very few parentheses, due to the
fixities of the operators given earlier.

> p0,p1 :: Command
>
> p0 = While TrueB Skip
>
> p1 = "x" := EInt 0 :::
>      For "i" (EInt 1) (EInt 10) 
>          ("x" := EVar "x" :+: EVar "i") :::
>      "main" := EVar "x"

Exception examples from Reynolds:

> p2,p3 :: Command
>
> p2 = Catch "cold" 
>            (Catch "cold"
>                   ("x" := EInt 42 :::
>                    Fail "cold")
>                   ("y" := EInt 42)
>            )
>            ("z" := EInt 42)
>
> p3 = Catch "cold" 
>            (Catch "flu"
>                   ("x" := EInt 42 :::
>                    Fail "cold")
>                   ("y" := EInt 42)
>            )
>            ("z" := EInt 42)
>
> exceptionTest =
>   let Term s2 = command p2 s0
>       Term s3 = command p3 s0
>   in [s2 "x", s2 "y", s2 "z", s3 "x", s3 "y", s3 "z"]

A program testing function.  I use the convention that the result of a
program execution is the value of the variable "main":

> test c = case command c s0 of
>            Term s    -> show (s "main")
>            Abort l s -> "Abort with label " ++ l

Note that command p1 s0 "i" will test that Newvar is working properly
(the value 0 will be returned, instead of 10), because For is defined
in terms of Newvar.