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

AUTHOR: Gary T. Leavens

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

This module just translates the rules found in Chapter 1, Figure 1.4
into Haskell, with the addition of boolean literals and logical operators.

> module CoreSemantics where
> import CoreLangParser
> import CoreTyping
> import Domains

	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 have the number in the syntax 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.
Note that expressions here can't have side effects.
To achieve strictness, we ensure that the base cases
always evaluate their store argument.

> meaningE :: ATree Expression
>      -> DStore -> ExpressibleValue

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

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

> meaningE (( Deref l ::: Node (Aexp Aint) [atr] )) s =
>     InInt (lookupStore (meaningL((l ::: atr)), s))

> meaningE (( (e1 `Plus` e2) ::: Node (Aexp Aint) [at1, at2] )) s =
>   (case (meaningE((e1 ::: at1)) s, meaningE((e2 ::: at2)) s) of
>      (InInt i1, InInt i2) -> InInt (plus (i1,i2))
>      (_,_) -> error "type error")

> meaningE (( Not e ::: Node (Aexp Abool) [atr] )) s =
>   (case meaningE((e ::: atr)) s of
>      (InBool b) -> InBool (not b)
>      _ -> error "type error")

> meaningE (( (e1 `Equals` e2) 
>                ::: Node (Aexp Abool)
>                       [at1@(Node (Aexp t1) _),
>                        at2@(Node (Aexp t2) _)] )) s =
>   (case (t1, t2) of
>     (Abool, Abool) ->
>       (case (meaningE((e1 ::: at1)) s, meaningE((e2 ::: at2)) s) of
>         (InBool b1, InBool b2) -> InBool (equalbool (b1,b2))
>         (_,_) -> error "type error")
>     (Aint, Aint) ->
>       (case (meaningE((e1 ::: at1)) s, meaningE((e2 ::: at2)) s) of
>         (InInt i1, InInt i2) -> InBool (equalint (i1,i2))
>         (_,_) -> error "type error"))

> meaningE (( (e1 `Lt` e2) ::: Node (Aexp Abool) [at1, at2])) s =
>   (case (meaningE((e1 ::: at1)) s, meaningE((e2 ::: at2)) s) of
>         (InInt i1, InInt i2) -> InBool (i1 < i2)
>         (_,_) -> error "type error")

> meaningE (( (e1 `Gt` e2) ::: Node (Aexp Abool) [at1, at2])) s =
>   (case (meaningE((e1 ::: at1)) s, meaningE((e2 ::: at2)) s) of
>         (InInt i1, InInt i2) -> InBool (i1 > i2)
>         (_,_) -> error "type error")

> meaningE (( (e1 `Le` e2) ::: Node (Aexp Abool) [at1, at2])) s =
>   (case (meaningE((e1 ::: at1)) s, meaningE((e2 ::: at2)) s) of
>         (InInt i1, InInt i2) -> InBool (i1 <= i2)
>         (_,_) -> error "type error")

> meaningE (( (e1 `Ge` e2) ::: Node (Aexp Abool) [at1, at2])) s =
>   (case (meaningE((e1 ::: at1)) s, meaningE((e2 ::: at2)) s) of
>         (InInt i1, InInt i2) -> InBool (i1 >= i2)
>         (_,_) -> error "type error")

> meaningE (( (e1 `And` e2) ::: Node (Aexp Abool) [at1, at2])) s =
>   (case (meaningE((e1 ::: at1)) s, meaningE((e2 ::: at2)) s) of
>         (InBool b1, InBool b2) -> InBool (b1 && b2)
>         (_,_) -> error "type error")

> meaningE (( (e1 `Or` e2) ::: Node (Aexp Abool) [at1, at2])) s =
>   (case (meaningE((e1 ::: at1)) s, meaningE((e2 ::: at2)) s) of
>         (InBool b1, InBool b2) -> InBool (b1 || b2)
>         (_,_) -> error "type error")


          MEANINGS FOR COMMANDS

The meaning of a command is a transformation from one store to another.
Again, we modify the base cases to ensure strictness in the store argument.

> meaningC :: ATree Command -> DStore -> DStore

> meaningC ((Skip ::: Node Acomm _)) s = s `seq` s

> meaningC (( (l `Assign` e) ::: Node Acomm [atl, ate] )) s =
>   (case meaningE((e ::: ate)) s of
>     (InInt i) -> updateStore(meaningL((l ::: atl)), i, s)
>     _ -> error "type error")

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

> meaningC (( (If e c1 c2) ::: Node Acomm [ate, at1, at2] )) s =
>  (case meaningE((e ::: ate)) s of
>    (InBool b) ->
>      if b then meaningC((c1 ::: at1)) s
>           else meaningC((c2 ::: at2)) s
>    _ -> error "type error")

> meaningC (( (While e c) ::: Node Acomm [ate, atc] )) s =
>      w(s)
>      where w s' =
>             (case meaningE ((e:::ate)) s' of
>              (InBool b) -> 
>                if b
>                then w(meaningC((c:::atc)) s')
>                else s'
>              _ -> error "type error")