******************************************
* Problem Set #2 for CS 430              *
* Code modified by Paul Liu              *
******************************************

***********************************************************************
* 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

FIXED POINT OPERATOR
====================

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

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
>   | (Var, Var) ::= (IntExp, 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
>
> 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 -> State -> 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 -> State -> State
>
> command (v := e)       s = extend s v (intExp e s)
> command (Skip)         s = s
> command (c1 ::: c2)    s = command c2 $! (command c1 s)
> command (If p c1 c2)   s = if boolExp p s then command c1 s else command c2 s
> command (While p c)    s = (y bigF) s
>     where bigF f s = if boolExp p s then f $! (command c s) else s
> command (Newvar v e c) s = extend (command c (extend s v (intExp e s))) v (s v)
> command (For v e1 e2 c) s = command (Newvar v e1 (While (EVar v :<=: e2) (c ::: v := EVar v :+: EInt 1))) s

Double assignment

> command ((v0,v1) ::= (e0,e1)) s = extend (extend s v0 e0') v1 e1'
>    where e0' = intExp e0 s
>          e1' = intExp e1 s

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"

===================================================================
2.4. Prove that the function F in the semantic equation below
     for the while command is continuous

    [[while b do c]] = Y F
         where F f s = if ( [[b]] s ) then f'' ( [[c]] s ) else s

    Note: f'' is the lifted function of f
===================================================================

Proof:

F is of type (State -> State') -> (State -> State')

Let P = State -> State', the pointwise ordering [= over P is

        f [= g <=> forall s (- State, f(s) = _|_ or  f(s) = g(s)
        
2.4.1) We'll first show that F is monotone, i.e., to prove 

        f [= g => F(f) [= F(g)

For any s (- State, we have

        (F(f))(s) = if [[b]] s then ((f)'')([[c]] s) else s
        (F(g))(s) = if [[b]] s then ((g)'')([[c]] s) else s

There are two cases:

2.4.1.1) suppose [[b]] s = true

        (F(f))(s) = ((f)'')([[c]] s)
        (F(g))(s) = ((g)'')([[c]] s)

    because f [= g <=> forall s (- State, f(s) = _|_ or  f(s) = g(s)
    we have

        f [= g
    =>  f([[c]] s) = _|_ or f([[c]] s) = g([[c]] s)
    =>  ((f)'')([[c]] s) = _|_ or
        ((f)'')([[c]] s) = f([[c]] s) = g([[c]] s) = ((g)'')([[c]] s)

    therefore 

        (F(f))(s) = _|_ or (F(f))(s) = (F(g))(s)
    <=> F(f) [= F(g)
   
2.4.1.2) suppose [[b]] s = false

        (F(f))(s) = s = (F(g))(s)
    <=> F(f) [= F(g)

Hence, in both cases we have F(f) [= F(g), i.e.

     for any f and g, f [= g => F(f) [= F(g)
     
So F is monotone. 

2.4.2) Next we want to prove F is contiuous. 

Let lub denote the least upper bound function on P, 
    lub' denote the least upper bound function on State'

For any interesting chain f0 [= f1 [= ... in P, we want to show

        F(lub(fi)) = lub(F(fi))

According to the definition of F, for any s (- State, we have

        F(lub(fi))(s)
      = if [[b]] s then ((lub(fi))'')([[c]] s) else s

        (lub(F(fi)))(s)
      = lub'(F(fi)(s))                  by proposition 2.2
      = lub'(if [[b]] s then (fi'')([[c s]]) else s)

there are two cases

2.4.2.1) suppose [[b]] s = true

        (F(lub(fi)))(s)
      = ((lub(fi))'')([[c]] s)
      = lub'((fi'')([[c]] s))           by proposition 2.2

        (lub(F(fi)))(s)
      = lub'((fi'')([[c]] s))
      = (F(lub(fi)))(s)

2.4.2.2) suppose [[b]] s = false

        (F(lub(fi)))(s) = s
        lub(F((fi)))(s) = lub'(s) = s

Hence, for all s (- State, we have

        (F(lub(fi)))(s) = lub(F((fi)))(s)

Therefore F(lub(fi)) = lub(F(fi)) for all interesting
chains fi in P. So F is a continuous function from P to P'.

Q.E.D.

===================================================================
2.6. Given: FV(c0) ^ FA(c1) = FV(c0) ^ FA(c1) = {}               (a)
     Prove: [[c0 ; c1]] = [[c1 ; c0]]
===================================================================

We want to show that for any s in State

        [[c1]]'' ([[c0]] s) = [[c0]]'' ([[c1]] s)

Let s0 = [[c0]] s, s1 = [[c1]] s, we'll prove by case analysis.

2.6.1) if s0 = _|_, we have two sub cases

2.6.1.1) if s1 = _|_ then it's trivial. 

2.6.1.2) if s1 /= _|_

For all u in FV(c0), we have

     u in FV(c0)
  => u not-in FA(c1)                            by (a)
  => s1 u = [[c1]] s u = s u                    by proposition 2.6(b)

Then by proposition 2.6(a), we have [[c0]] s1 = [[c0]] s = _|_, so

[[c1]]'' ([[c0]] s) = [[c1]]'' _|_ = _|_ = [[c0]] s1 = [[c0]]'' ([[c1]] s)

End of proof for case 2.6.1.

2.6.2) if s1 = _|_

This can proved similarly to 2.6.1, by the symmetry of the problem.

2.6.3) if s0 /= _|_ and s1 /= _|_, then we can drop the source lifting. 
Instead, we want to prove

      [[c1]] s0 u = [[c0]] s1 u, for all variable u.

First we'll show that

      [[c1]] s0 /= _|_. 

This is is proved by contradiction. Suppose [[c1]] s0 = _|_, 
then forall v in FV(c1)

      v in FV(c1)
   => v not-in FA(c0)
   => [[c0]] s v = s0 v = s v                   by proposition 2.6(b)
   => [[c1]] s0 v = _|_ = [[c1]] s v            by proposition 2.6(a)

But it's a contradiction to [[c1]] s v /= _|_. Therefore
[[c1]] s0 can't be _|_. Similarly, [[c0]] s1 can't be
_|_. Therefore, neither [[c1;c0]] s nor [[c0;c1]] s is _|_.

Then we'll do a case analysis on variable u. There are
three cases:

2.6.3.1) if u in FA(c0)

      u in FA(c0)
   => u not-in FV(c1)                           by (a)
   => u not-in FA(c1)                           FV(c) is superset of FA(c)

If [[c1]] s0 /= _|_, then by proposition 2.6(b)

      [[c1]] ([[c0]] s) u = [[c1]] s0 u = s0 u.

and also because [[c1]] s /= _|_, we have

      [[c1]] s v = s1 v = s v, for all v not-in FA(c1)

Because v not-in FA(c1) <=> v in FV(c0), we then have
s1 v = s v, for all v in FV(c0). Then by proposition 2.6(a):

      [[c0]] s1 = [[c0]] s /= _|_ and
      for all v in FV(c0), [[c0]] s1 v = [[c0]] s v

Because u in FA(c0) => u in FV(c0), we then have

[[c0]] ([[c1]] s) u = [[c0]] s1 u = [[c0]] s u = s0 u = [[c1]] ([[c0]] s) u

Case proved.

2.6.3.2) if u in FA(c1)

This can proved similarly to 2.6.3.1, by the symmetry of the problem.

2.6.3.3) if u not-in FA(c0) and u not-in FA(c1), this implies:

      u not-in FA(c0;c1)
   => [[c0;c1]] s u = s u                       by proposition 2.6(b)

because [[c0;c1]] s is not _|_ as proved above in 2.6.3. Similarly, 
we have [[ c1;c0 ]] s u = s u = [[c0;c1]] s u.

All cases proved. Q.E.D.