$Id: CoreTypeAttributes.lhs,v 1.3 1998/06/05 21:08:30 leavens Exp $

Type attributes rules for the core language of David A. Schmidt's
"The Structure of Typed Programming Languages" (MIT Press, 1994).
Translated into Haskell by Gary T. Leavens.

This module should be redefined for each language,
if the attributes are changed.
This module is used by the module CoreTypeHelpers.

> module CoreTypeAttributes where
> import Subst

The primitive type attributes used, following Reynolds, are:

type attribute		use
--------------------------------------
int                     integer values
bool                    boolean valuesloc   
comm                    commands
err                     type errors
tau loc                 locations holding taus
tau exp                 expressions evaluating to type tau
var X                   logical variables

This last is only present for use in unification.

These are modeled by the following Haskell definition.
We use the prefix "A" for "attribute".

> type Tau = PrimitiveAttrib

> data PrimitiveAttrib =
>        Aint | Abool | Acomm | Aerr
>      | Aloc Tau
>      | Aexp Tau
>      | Avar LogicalVar
>         deriving Eq

Making PrimitiveAttrib an instance of the Show class
is useful for debugging.

> instance Show PrimitiveAttrib where
>   showsPrec p Aint = showString "int"
>   showsPrec p Abool = showString "bool"
>   showsPrec p Acomm = showString "comm"
>   showsPrec p Aerr = showString "error"
>   showsPrec p (Aloc tau) = showsPrec p tau . showString " loc"
>   showsPrec p (Aexp tau) = showsPrec p tau . showString " exp"
>   showsPrec p (Avar lv) = showString "?" . showsPrec p lv

The Substitutable and Unifiable classes are needed to use the type helpers.

> instance Substitutable PrimitiveAttrib where
>   nullSubst = Avar

>   lv1 ->- t = \lv2 -> if lv1 == lv2 then t else Avar lv2

>   app s (Aloc tau) = Aloc (app s tau)
>   app s (Aexp tau) = Aexp (app s tau)
>   app s (Avar lv) = s lv
>   app s tau = tau  -- for the base cases

> instance Unifiable PrimitiveAttrib where
>   toTerm = Avar

>   getVar (Avar lv) = Just lv
>   getVar _         = Nothing

>   subterms (Aloc tau) = [tau]
>   subterms (Aexp tau) = [tau]
>   subterms _ = [] -- base cases, and logical variables

>   same_kind Aint Aint = True
>   same_kind Abool Abool = True
>   same_kind Acomm Acomm = True
>   same_kind Aerr Aerr = True
>   same_kind (Aloc tau1) (Aloc tau2) = True
>   same_kind (Aexp tau1) (Aexp tau2) = True
>   same_kind (Avar lv1) (Avar lv2) = True
>   same_kind t1 t2 = False