Here's the abstract syntax of while0, as discussed in class.

> -- helpful notationally
> infixr `Semi`

> type C = Command
> type E = Expression
> type L = Location
> type N = Numeral
>
> data Command = L `Assign` E | Skip
>	       | C `Semi` C | If E C C
>	       | While E C
> data Expression = Num N | Deref L
>	       | E `Plus` E
>	       | Not E | E `Equals` E
> data Location = Loc Integer
> type Numeral = Integer

The following is the Haskell code for the typing rules.

	MODELING ATTRIBUTES IN HASKELL

> data TypeAttrib = Aint | Abool
>	 | Aintloc
> 	 | Aexp TypeAttrib
>	 | Acomm             deriving Eq

> data AttribTree syntax attrib =
>    syntax ::: attrib
> type ATree syntax =
>     AttribTree syntax TypeAttrib

> infixr `ASemi`

> type AC = ACommand
> type AE = AExpression
> type AL = ALocation
> type AN = ANumeral

> type ACommand = ATree Command'
> data Command' = ASkip | AL `AAssign` AE
>	     | AC `ASemi` AC
>            | AIf AE AC AC
>	     | AWhile AE AC

> type AExpression = ATree Expression'
> data Expression' = ANum AN | ADeref AL
>	     | AE `APlus` AE
>	     | ANot AE | AE `AEquals` AE

> type ALocation = ATree Location
> type ANumeral = ATree Numeral

	MODELING THE TYPE RULES

> annotateC :: Command -> ACommand

> annotateC (l `Assign` e) =
>  (case (annotateL l, annotateE e) of
>    (al@(_::: Aintloc),
>     ae@(_::: Aexp Aint)) ->
>        (al `AAssign` ae) ::: Acomm)

> annotateC Skip =
>      ASkip:::Acomm

> annotateC (c1 `Semi` c2) =
>  (case (annotateC c1, annotateC c2) of
>    (ac1@(_::: Acomm),
>     ac2@(_::: Acomm)) ->
>       (ac1 `ASemi` ac2):::Acomm)

> annotateC (If e c1 c2) =
>  (case (annotateE e,
>         annotateC c1, annotateC c2) of
>    (ae@(_:::Aexp Abool),
>     ac1@(_:::Acomm),
>     ac2@(_:::Acomm)) ->
>       (AIf ae ac1 ac2):::Acomm)

> annotateC (While e c) =
>  (case (annotateE e, annotateC c) of
>    (ae@(_:::Aexp Abool),
>     ac@(_:::Acomm)) ->
>       (AWhile ae ac):::Acomm)

TYPING RULES FOR EXPRESSIONS

> annotateE (Deref l) =
>   (case (annotateL l) of
>     al@(_:::Aintloc) ->
>       (ADeref al):::Aexp Aint)

> annotateE (Num n) =
>   (case (annotateN n) of
>     an@(_:::Aint) ->
>      (ANum an):::Aexp Aint)

> annotateE (e1 `Plus` e2) =
>   (case (annotateE e1, annotateE e2) of
>     (ae1@(_:::Aexp Aint),
>      ae2@(_:::Aexp Aint)) ->
>       (ae1 `APlus` ae2):::Aexp Aint)

> annotateE (Not e) =
>   (case (annotateE e) of
>     ae@(_:::Aexp Abool) ->
>       (ANot ae):::Aexp Abool)

> annotateE (e1 `Equals` e2) =
>   (case (annotateE e1, annotateE e2) of
>     (ae1@(_:::Aexp at1),
>      ae2@(_:::Aexp at2))
>       | at1 == at2 ->
>      (ae1 `AEquals` ae2):::Aexp Abool)

	REMAINING RULES

> annotateL :: Location -> ALocation
> annotateL (Loc i) | i > 0 =
>      (Loc i):::Aintloc

> annotateN :: Numeral -> ANumeral
> annotateN n = n:::Aint

Here's the code for the semantics

   SEMANTIC DOMAINS MODELED IN HASKELL

The booleans

> type DBool = Bool
> true = True
> false = False

> -- Operations:
> -- not is already in Haskell
> equalbool :: (DBool, DBool) -> DBool
> equalbool(m, n) = (m == n)


The integers

> type DInt = Integer

> -- Operations:
> plus :: (DInt,DInt) -> DInt
> plus(m,n) = m + n
> equalint :: (DInt,DInt) -> DBool
> equalint(m,n) = (m == n)


Locations

> -- recall: data Location = Loc Integer
> type DLocation = Location


	MODELING STORES IN HASKELL

Stores

> type DStore = [DInt]

> -- Operations:
> lookup :: (DLocation,DStore) -> DInt
> lookup(Loc j, s) | (j <= genericLength s) =
>             s !! (j-1)
> lookup(Loc j, s) | (j > genericLength s) = 0

> update :: (DLocation,DInt,DStore)
>            -> DStore
> update(Loc j, n, s) | (j <= genericLength s) =
>      (take (j-1) s) ++ [n] ++ (drop j s)
> update(Loc j, n, s) | (j > genericLength s) = s

> -- if is already in Haskell


	SEMANTIC FUNCTIONS

> meaningN :: ANumeral -> DInt
> meaningN ((n ::: Aint)) = n

> meaningL :: ALocation -> DLocation
> meaningL (((Loc i) ::: Aintloc)) =
>           (Loc i)


         MEANINGS FOR EXPRESSIONS

> meaningE :: AExpression
>      -> DStore -> ExpressibleValue

> data ExpressibleValue = InInt DInt
>                       | InBool DBool

> meaningE ((ANum an ::: Aexp Aint)) s =
>     InInt (meaningN ((an)))
> meaningE ((ADeref al ::: Aexp Aint)) s =
>     InInt (lookup (meaningL((al)), s))
> meaningE (((ae1 `APlus` ae2) ::: Aexp Aint)) s =
>   (case (meaningE((ae1)) s, meaningE((ae2)) s) of
>      (InInt i1, InInt i2) -> InInt (plus (i1,i2)))
> meaningE ((ANot ae::: Aexp Abool)) s =
>   (case meaningE((ae)) s of
>      (InBool b) -> InBool (not b))
> meaningE (((ae1@(_:::Aexp Abool)
>              `AEquals`
>             ae2@(_:::Aexp Abool)))
>           ::: Aexp Abool) s =
>   (case (meaningE((ae1)) s, meaningE((ae2)) s) of
>     (InBool b1, InBool b2) -> InBool (equalbool (b1,b2)))
> meaningE (((ae1@(_:::Aexp Aint)
>              `AEquals`
>             ae2@(_:::Aexp Aint)))
>           ::: Aexp Abool) s =
>   (case (meaningE((ae1)) s, meaningE((ae2)) s) of
>     (InInt i1, InInt i2) -> InBool (equalint (i1,i2)))

The following we haven't done yet, but for completeness, here it is...

	MEANINGS FOR COMMANDS

> meaningC :: ACommand -> DStore -> DStore
> meaningC ((ASkip ::: Acomm)) s = s
> meaningC (((al `AAssign`
>             ae@(_:::Aexp Aint))
>      ::: Acomm)) s =
>   (case meaningE((ae)) s of
>     (InInt i) ->
>       update(meaningL(al), i, s))
> meaningC (((ac1 `ASemi` ac2) ::: Acomm))
>          s =
>   meaningC((ac2)) (meaningC((ac1)) s)
> meaningC (((AIf ae@(_:::Aexp Abool)
>                 ac1 ac2) ::: Acomm)) s =
>  (case meaningE((ae)) s of
>    (InBool b) ->
>      if b then meaningC((ac1)) s
>           else meaningC((ac2)) s)
> meaningC (((AWhile ae@(_:::Aexp Abool)
>                    ac) ::: Acomm)) s =
>      w(s)
>      where w s' =
>             (case meaningE ae s' of
>              (InBool b) -> 
>                if b
>                then w(meaningC((ac)) s')
>                else s')