$Id: CoreDomains.lhs,v 1.3 2004/09/20 21:03:46 leavens Exp $

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

AUTHOR: Gary T. Leavens.

> module CoreDomains(module CoreDomains, Location) where
> import CoreLangParser
> import List -- from the Haskell library

   SEMANTIC DOMAINS MODELED IN HASKELL

See Schmidt's figure 1.6 for the usual formatting.

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

There are no operations on locations.

Note that there are 3 DBool values: true, false, and bottom.
This is unavoidable when using a programming lang,
but it is an approximation.


Stores

> type DStore = [StorableValue]

> -- Operations:
> lookupStore :: Storable storable =>
>    (DLocation, [storable]) -> storable
> lookupStore(Loc j, s)
>         | (0 < j) && (j <= genericLength s) = s !! (fromInteger (j-1))
>         | otherwise = defaultContents

> updateStore :: 
>   (DLocation, storable, [storable]) -> [storable]
> updateStore(Loc j, n, s)
>        | (0 < j) && (j <= genericLength s) =
>                  (genericTake (j-1) s) ++ [n] ++ (genericDrop j s)
>        | otherwise = s

> -- if is already in Haskell

Note: we need to use genericLength because j is a Haskell Integer,
and length returns a Haskell Int (:-|)


Storable Values

The type synonym StorableValue is intended to make reuse of this
module a bit easier.  In particular, if, for example, you need to
store Booleans, then you'll need to change this into a data definition.

> type StorableValue = DInt

The assumptions on StorableValue used above
are captured in the class Storable, of which DInt (= Integer)
is an instance.

> class Storable t where
>   defaultContents :: t

> instance Storable Integer where
>   defaultContents = 0


The meaning of an expession in a given store is an expressible value.
Expressible values are either integers or booleans.

> data ExpressibleValue = InInt DInt
>                       | InBool DBool
>                         deriving Eq

It's useful for ExpressibleValue to be an instance of the class Show,
for output of expression values.

> instance Show ExpressibleValue where
>   showsPrec p (InInt i) = showsPrec p i
>   showsPrec p (InBool b) = showsPrec p b