$Id: TypeAttributes.lhs,v 1.7 1998/06/05 21:01:49 leavens Exp $

Type attributes rules for various languages in 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 TypeHelpers.

> module TypeAttributes where
> import FinFun
> import Subst

The primitive type attributes used, following Reynolds, are:

type attribute		use
--------------------------------------
int                     integer values
bool                    boolean values   
comm                    commands
err                     type errors
tau loc                 locations holding taus
tau exp                 expressions evaluating to type tau
delta class             allocators of type delta
pi dec                  declarations yielding a type environment pi
pi module               module containing declarations that yield pi
theta1 -> theta2        functions from theta1 to theta2
var X                   logical variables
pi                      type environment

The last two above are really just there for use in unification.

These are modeled by the following Haskell definitions.
We use the prefix "A" for "attribute".
Note: if you change these, you *must* also change the instances of
the classes Substitutable and Unifiable below.  (You should also change
the Show instance.)

> type Theta = PrimitiveAttrib

> data PrimitiveAttrib =
>        Aint | Abool | Acomm | Aerr
>      | Aloc Tau
>      | Aexp Tau
>      | Aclass Delta
>      | Adec Pi
>      | Amodule Pi
>      | Theta :-> Theta
>      | Avar LogicalVar
>      | Api (FiniteFun String Theta)
>            deriving Eq

Although Schmidt breaks type attributes into various subdomains,
to prevent, for example, command locations, this is inconvenient
in a program.  In particular, to do unification, all of these have
to be collected into one domain. Hence we use the following synonyms.

> type Tau = PrimitiveAttrib
> type Delta = PrimitiveAttrib
> type Pi = PrimitiveAttrib

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 (Aclass delta) = showsPrec p delta . showString " class"
>   showsPrec p (Adec pi) = showsPrec p pi . showString " dec"
>   showsPrec p (Amodule pi) = showsPrec p pi . showString " module"
>   showsPrec p (theta1 :-> theta2) =
>      showString "("
>       . showsPrec p theta1 . showString " -> " . showsPrec p theta2
>       . showString ")"
>   showsPrec p (Avar lv) = showString "?" . showsPrec p lv
>   showsPrec p (Api pi) = showsPrec p pi


The Substitutable and Unifiable classes are needed to use the type helpers.
The Substitutable class tells how to substitute for logical variables in terms.

> 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 (Aclass delta) = Aclass (app s delta)
>   app s (Adec pi) = Adec (app s pi)
>   app s (Amodule pi) = Amodule (app s pi) 
>   app s (theta1 :-> theta2) = (app s theta1) :-> (app s theta2)
>   app s (Avar lv) = s lv
>   app s (Api pi) = Api (map (\(i,tau) -> (i,(app s tau))) pi)
>   app s tau = tau  -- for the base cases
>   -- Note: the previous line matches all patterns,
>   -- anything you add below this point won't affect app!

The Unifiable instance gives the capabilities needed to do unification
on type attributes.

> instance Unifiable PrimitiveAttrib where
>   toTerm = Avar

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

>   subterms (Aloc tau) = [tau]
>   subterms (Aexp tau) = [tau]
>   subterms (Aclass delta) = [delta]
>   subterms (Adec pi) = [pi]
>   subterms (Amodule pi) = [pi]
>   subterms (theta1 :-> theta2) = [theta1, theta2]
>   subterms (Api pi) = [tau | (i,tau) <- pi]
>   subterms _ = [] -- base cases, and logical variables
>   -- Note: the previous line matches all patterns,
>   -- anything you add below this point won't affect subterms!

>   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 (Aclass delta1) (Aclass delta2) = True
>   same_kind (Adec pi1) (Adec pi2) = True
>   same_kind (Amodule pi1) (Amodule pi2) = True
>   same_kind (theta11 :-> theta12) (theta21 :-> theta22) = True
>   same_kind (Avar lv1) (Avar lv2) = True
>   same_kind (Api pi1) (Api pi2) =
>                and (zipWith (\(i1,t1) -> \(i2,t2) -> i1 == i2) pi1 pi2)
>   same_kind t1 t2 = False
>   -- Note: the previous line matches all patterns,
>   -- anything you add below this point won't affect same_kind!