$Id: WhileNSemantics.lhs,v 1.4 1998/05/19 16:26:44 leavens Exp $

AUTHOR: Gary T. Leavens

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

This module just translates the semantics found in Chapter 2, Section 2.15
into Haskell.  However, unlike our translation of chapter 1,
we write this in a way that is independent of the type system,
and so give semantics just to the syntax, without regard to the type
environment and types of phrases.
We also add boolean literals.

> module WhileNSemantics where
> import WhileNParser
> import WhileNDomains


	SEMANTIC FUNCTIONS

The semantic functions are meaningP, meaningD, meaningC, etc.
We present the semantic functions top down, following the book.

You will notice that the base cases of the semantic functions
have been modified to ensure strictness in the store and enviornment arguments.

          PROGRAMS

Although not necessary, it matches the typing rules to let the program
also be given an initial environment.  This could contain bindings for
built-in names for the language.

> meaningP :: Program -> DEnvironment -> DStore -> DStore
> meaningP (( d `In` c )) env s = meaningC((c)) env1 s1
>    where (env1, s1) = meaningD((d)) emptyEnv s


          DECLARATIONS

The main difference here is the use of unionMinus in the treatment
of sequential declarations; this is necessary for modules and records to work.

> meaningD :: Declaration -> DEnvironment -> DStore -> (DEnvironment, DStore)

> meaningD (( d1 `Also` d2 )) env s =
>   if disjoint e1 e2 then (e1 ++ e2, s2) else error "type error"
>     where (e1, s1) = meaningD((d1)) env s
>           (e2, s2) = meaningD((d2)) env s1

> meaningD (( d1 `Then` d2 )) env s =
>   if disjoint e1 e2 then (e1 ++ e2, s2) else error "type error"
>     where (e1, s1) = meaningD((d1)) env s
>           (e2, s2) = meaningD((d2)) (env `unionMinus` e1) s1

> meaningD (( Fun i e )) env s = env `seq` s `seq` ([(i, DVFun f)], s)
>    where f s' = meaningE((e)) env s'

We have separate cases for const because the syntax recognized by
the parser is wider than it would be ideally.

> meaningD (( Const i (Num n) )) env s =
>    env `seq` s `seq`
>    ([(i, DVInt (meaningN((n))))], s)
> meaningD (( Const i (Ident x) )) env s =
>    s `seq`
>    (case meaningX((x)) env of
>      dvi@(DVInt n) -> ([(i, dvi)], s)
>      _ -> error "type error")
> meaningD (( Const i _ )) env s = error "syntax error"

> meaningD (( Proc i c )) env s = env `seq` s `seq` ([(i, DVProc p)], s)
>    where p s' = meaningC((c)) env s'

> meaningD (( Var i t )) env s = ([(i, v)], s')
>    where (v,s') = meaningT((t)) env s

> meaningD (( Alias i l )) env s = s `seq` ([(i, DVLoc v)], s)
>    where v = meaningL((l)) env

> meaningD (( Class i t )) env s = env `seq` s `seq` ([(i, DVClass p)], s)
>    where p s' = meaningT((t)) env s'

> meaningD (( Module i d )) env s = ([(i, DVModule env1)], s1)
>    where (env1,s1) = meaningD((d)) env s

> meaningD (( Import x )) env s =
>    s `seq`
>    (case meaningX((x)) env of
>       (DVModule env1) -> (env1, s)
>       _ -> error "type error")


         
          TYPE STRUCTURE

> meaningT :: TypeStructure -> DEnvironment
>                           -> DStore
>                           -> (DenotableValue, DStore)

> meaningT (( NewInt )) env s =
>   env `seq`
>   let (l,s') = allocateStore s
>   in  (DVLoc l, s')

> meaningT (( Record d )) env s =
>   let (env', s') = meaningD (( d )) env s
>   in  (DVModule env', s')

> meaningT (( TId x )) env s =
>   (case meaningX((x)) env of
>      (DVClass p) -> p(s)
>      _ -> error "type error")



          COMMANDS

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

> meaningC :: Command -> DEnvironment -> DStore -> DStore

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

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

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

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

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

> meaningC (( Call x )) env s =
>   (case meaningX((x)) env of
>      (DVProc p) -> p(s)
>      _ -> error "type error")


        EXPRESSIONS

The ExpressibleValue domain is defined in the module Domains.
Note that expressions here can't have side effects.

The main change from the book is that the meaning of identifiers as
expressions has to handle two cases: the names of functions and the
names of constants.  The latter appear in the book under Numerals.

> meaningE :: Expression -> DEnvironment -> DStore -> ExpressibleValue

> meaningE (( Ident x )) env s =
>   s `seq`
>   (case meaningX((x)) env of
>      (DVFun f) -> f(s)
>      (DVInt i) -> InInt i
>      _ -> error "type error")

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

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

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

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

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

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


           VARIABLES

Variables are defined using identifier expressions.
Although it's not obvious in the book why there's a
separate domain and meaning function for variables,
it's clear here that an extra check happens.

> meaningL :: Variable -> DEnvironment -> DLocation

> meaningL (( Varref x )) env =
>   (case (meaningX((x)) env) of
>      (DVLoc l) -> l
>      _ -> error "type error")

> meaningL (( Loc i )) env = env `seq` i

           NUMERALS

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.  Also, we don't handle identifier
expressions here, as they don't parse as numerals, but as expressions.

> meaningN :: Integer -> DInt
> meaningN (( n )) = n

           BOOLEANS

Booleans are treated similarly

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


     IDENTIFIER EXPRESSIONS

> meaningX :: IdentifierExpr -> DEnvironment -> DenotableValue

> meaningX (( Name i )) env =
>   env `dot` i                     -- gives a type error if i is not in env

> meaningX (( x `Dot` i )) env =
>    (case meaningX((x)) env of
>       (DVModule r) ->  r `dot` i  -- can also give a type error
>       _ -> error "type error")