$Id: CoreUntypedSemantics.lhs,v 1.3 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 translates the rules found in Chapter 1, Figure 1.4
into Haskell, with the addition of boolean literals and logical operators,
but without mentioning anything about types.

> module CoreUntypedSemantics where
> import CoreLangParser
> 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 :: Integer -> DInt
> meaningN (( n )) = n

Booleans are treated similarly

> meaningB :: Boolean -> DBool
> meaningB (( b )) = b

Locations have the number in the syntax as their meaning.

> meaningL :: Location -> DLocation
> meaningL (( Loc i )) = 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 :: Expression -> DStore -> ExpressibleValue

> meaningE (( Num n )) s =
>   s `seq` InInt (meaningN ((n)) )

> meaningE (( BoolLit b )) s =
>   s `seq` InBool (meaningB ((b)) )

> meaningE (( Deref l )) s =
>   InInt (lookupStore (meaningL((l)), s))

> meaningE (( e1 `Plus` e2 )) s =
>   (case (meaningE((e1)) s, meaningE((e2)) s) of
>      (InInt i1, InInt i2) -> InInt (plus (i1,i2))
>      (_,_) -> error "type error")

> meaningE (( Not e )) s =
>   (case meaningE((e)) s of
>      (InBool b) -> InBool (not b)
>      _ -> error "type error")

> meaningE (( e1 `Equals` e2 )) s =
>   (case (meaningE((e1)) s, meaningE((e2)) s) of
>      (InBool b1, InBool b2) -> InBool (equalbool (b1,b2))
>      (InInt i1, InInt i2) -> InBool (equalint (i1,i2))
>      (_,_) -> error "type error")

> meaningE (( e1 `Lt` e2 )) s =
>   (case (meaningE((e1)) s, meaningE((e2)) s) of
>         (InInt i1, InInt i2) -> InBool (i1 < i2)
>         (_,_) -> error "type error")

> meaningE (( e1 `Gt` e2 )) s =
>   (case (meaningE((e1)) s, meaningE((e2)) s) of
>         (InInt i1, InInt i2) -> InBool (i1 > i2)
>         (_,_) -> error "type error")

> meaningE (( e1 `Le` e2 )) s =
>   (case (meaningE((e1)) s, meaningE((e2)) s) of
>         (InInt i1, InInt i2) -> InBool (i1 <= i2)
>         (_,_) -> error "type error")

> meaningE (( e1 `Ge` e2 )) s =
>   (case (meaningE((e1)) s, meaningE((e2)) s) of
>         (InInt i1, InInt i2) -> InBool (i1 >= i2)
>         (_,_) -> error "type error")

> meaningE (( e1 `And` e2 )) s =
>   (case (meaningE((e1)) s, meaningE((e2)) s) of
>         (InBool b1, InBool b2) -> InBool (b1 && b2)
>         (_,_) -> error "type error")

> meaningE (( e1 `Or` e2 )) s =
>   (case (meaningE((e1)) s, meaningE((e2)) 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 :: Command -> DStore -> DStore

> meaningC ((Skip)) s = s `seq` s

> meaningC (( l `Assign` e )) s =
>   (case meaningE((e)) s of
>     (InInt i) -> updateStore(meaningL((l)), i, s)
>     _ -> error "type error")

> meaningC (( c1 `Semi` c2 )) s =
>   meaningC((c2)) (meaningC((c1)) s)

> meaningC (( If e c1 c2 )) s =
>  (case meaningE((e)) s of
>    (InBool b) ->
>      if b then meaningC((c1)) s
>           else meaningC((c2)) s
>    _ -> error "type error")

> meaningC (( While e c )) s =
>      w(s)
>      where w s' =
>             (case meaningE ((e)) s' of
>              (InBool b) -> 
>                if b
>                then w(meaningC((c)) s')
>                else s'
>              _ -> error "type error")