***********************************************************************
* A realization of the syntax and semantics of Reynolds' SIL:         *
* A "Simple Imperative Language", from Chapter 2 of the text.         *
***********************************************************************

Written by Paul Hudak, September 20, 2007

> 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
>   deriving (Eq, Show)

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 State = Var -> Integer

We can extend states using function variation:

> extend :: State -> Var -> Integer -> State
> 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.

SEMANTICS
=========

Semantic function for integer expressions:

> intExp :: IntExp -> State -> Integer

...

Semantic function for boolean expressions:

> boolExp :: BoolExp -> State -> Bool

...

Semantic function for commands:

> command :: Command -> State -> State

...

EXAMPLES
========

Initial state that maps all variables to zero:

> s0 :: State
> 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"

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

> test c = command c s0 "main"

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.

> sbot :: State
> sbot = undefined

> t1 = command ("main" := EInt 42) sbot "x"