$Id: CoreMonadSemantics.lhs,v 1.6 1998/03/19 07:18:13 leavens Exp $

AUTHOR: Gary T. Leavens.

Semantic rules in monadic style for the core language of
David A. Schmidt's "The Structure of Typed Programming Languages"
(MIT Press, 1994).

> module CoreMonadSemantics where
> import CoreLangParser
> import CoreTyping
> import Domains
> import MonadStore

	SEMANTIC FUNCTIONS

The semantic functions are meaningN, meaningL, meaningE, meaningC.
(I don't see how to avoid different names for the
meaning functions, since they aren't parametric.)
We present the semantic functions bottom up, following the book.


For numbers, we really don't convert from syntax to semantics
going from numerals to numbers, because the "syntax"
is already coded as an integer

> meaningN :: ATree Integer -> DInt
> meaningN (( n ::: Node Aint _ )) = n

Booleans are treated similarly

> meaningB :: ATree Boolean -> DBool
> meaningB (( b ::: Node Abool _ )) = b

Locations essentially have themselves as their meaning.

> meaningL :: ATree Location -> DLocation
> meaningL (( (Loc i) ::: Node (Aloc Aint) _ )) = i


        MEANINGS FOR EXPRESSIONS

The ExpressibleValue domain is defined in the module Domains.
This version of the semantics, since it uses the store monad,
would allow side effects in expressions, although in this
particular semantics none are possible.

> meaningE :: ATree Expression
>      -> MStore ExpressibleValue

> meaningE (( Num n ::: Node (Aexp Aint) [atr] )) =
>   return (InInt (meaningN ((n ::: atr)) ) )

> meaningE (( BoolLit b ::: Node (Aexp Abool) [atr] )) =
>   return (InBool (meaningB ((b ::: atr )) ) )

> meaningE (( Deref l ::: Node (Aexp Aint) [atr] )) =
>   do i <- lookupS (meaningL((l ::: atr)) )
>      return (InInt i)

> meaningE (( (e1 `Plus` e2) ::: Node (Aexp Aint) [at1, at2] )) =
>   do (InInt i1) <- (meaningE ((e1 ::: at1)))
>      (InInt i2) <- (meaningE ((e2 ::: at2)))
>      return (InInt (plus (i1,i2)))

> meaningE (( Not e ::: Node (Aexp Abool) [atr] )) =
>   do (InBool b) <- meaningE ((e ::: atr))
>      return (InBool (not b))

> meaningE (( (e1 `Equals` e2) 
>                ::: Node (Aexp Abool)
>                       [at1@(Node (Aexp t1) _),
>                        at2@(Node (Aexp t2) _)] )) =
>   (case (t1, t2) of
>     (Abool, Abool) ->
>       do (InBool b1) <- meaningE((e1 ::: at1))
>          (InBool b2) <- meaningE((e2 ::: at2))
>          return (InBool (equalbool (b1,b2)))
>     (Aint, Aint) ->
>       do (InInt b1) <- meaningE((e1 ::: at1))
>          (InInt b2) <- meaningE((e2 ::: at2))
>          return (InBool (equalint (b1,b2))) )

> meaningE (( (e1 `Lt` e2) ::: Node (Aexp Abool) [at1, at2] )) =
>   do (InInt i1) <- meaningE ((e1 ::: at1))
>      (InInt i2) <- meaningE ((e2 ::: at2))
>      return (InBool (i1 < i2))

> meaningE (( (e1 `Gt` e2) ::: Node (Aexp Abool) [at1, at2] )) =
>   do (InInt i1) <- meaningE ((e1 ::: at1))
>      (InInt i2) <- meaningE ((e2 ::: at2))
>      return (InBool (i1 > i2))

> meaningE (( (e1 `Le` e2) ::: Node (Aexp Abool) [at1, at2] )) =
>   do (InInt i1) <- meaningE ((e1 ::: at1))
>      (InInt i2) <- meaningE ((e2 ::: at2))
>      return (InBool (i1 <= i2))

> meaningE (( (e1 `Ge` e2) ::: Node (Aexp Abool) [at1, at2] )) =
>   do (InInt i1) <- meaningE ((e1 ::: at1))
>      (InInt i2) <- meaningE ((e2 ::: at2))
>      return (InBool (i1 >= i2))

> meaningE (( (e1 `And` e2) ::: Node (Aexp Abool) [at1, at2] )) =
>   do (InBool b1) <- meaningE ((e1 ::: at1))
>      (InBool b2) <- meaningE ((e2 ::: at2))
>      return (InBool (b1 && b2))

> meaningE (( (e1 `Or` e2) ::: Node (Aexp Abool) [at1, at2] )) =
>   do (InBool b1) <- meaningE ((e1 ::: at1))
>      (InBool b2) <- meaningE ((e2 ::: at2))
>      return (InBool (b1 || b2))

          MEANINGS FOR COMMANDS

The meaning of a command is a transformation from one store to another.

> meaningC :: ATree Command -> MStore ()

> meaningC ((Skip ::: Node Acomm _)) =
>   return ()

> meaningC (( (l `Assign` e) ::: Node Acomm [atl, ate] )) =
>   do (InInt i) <- meaningE ((e ::: ate))
>      updateS (meaningL ((l ::: atl))) i

> meaningC (( (c1 `Semi` c2) ::: Node Acomm [at1, at2] )) =
>   do meaningC ((c1 ::: at1))
>      meaningC ((c2 ::: at2))

> meaningC (( (If e c1 c2) ::: Node Acomm [ate, at1, at2] )) =
>   do (InBool b) <- meaningE ((e ::: ate))
>      if b then do meaningC ((c1 ::: at1))
>           else do meaningC ((c2 ::: at2))

> meaningC (( (While e c) ::: Node Acomm [ate, atc] )) =
>   w
>   where w = do (InBool b) <- meaningE ((e:::ate))
>                if b
>                 then do meaningC ((c:::atc))
>                         w
>                 else do meaningC ((Skip ::: Node Acomm []))