$Id: CoreTyping.lhs,v 1.8 2004/10/18 23:47:48 leavens Exp leavens $

AUTHOR: Gary T. Leavens.

Type checking for the core language of Schmidt's
"The Structure of Typed Programming Languages" (MIT Press, 1994).
This module is essentially a translation into Haskell of the rules
chapter 1, figure 1.4, with the boolean literals added and some other
boolean-valued expressions added.

> module CoreTyping(module CoreTyping, module CoreLangParser,
>                   module CoreLangUnparser,
>                   module CoreTypeAttributes, module CoreTypeHelpers) where
> import CoreLangParser
> import CoreLangUnparser
> import CoreTypeAttributes
> import CoreTypeHelpers
> import Subst

This module uses the primitive type attributes defined
in the module CoreTypeAttributes.
It also uses the rule, axiom, and ruleIf functions of CoreTypeHelpers.


                     SYNTAX DOMAIN

To allow heterogenity of types of syntax in the lists of hypotheses,
we use the data type Syntax defined below.
It is the disjoint union of the domains of the abstract syntax.

> data Syntax =
>           Expr Expression
>         | Comm Command
>         | Loct Location
>         | Numr Integer
>         | Boole Bool

To dispatch annotate to the various domains from a hypothesis,
we make an instance for the type Syntax also.

> instance Annotatable Syntax where
>   annotate (Expr e) =
>         case annotate e of
>              (Tree_Subst (e:::a) substl) -> Tree_Subst (Expr e ::: a) substl
>   annotate (Comm c) = 
>         case annotate c of
>              (Tree_Subst (c:::a) substl) -> Tree_Subst (Comm c ::: a) substl
>   annotate (Loct l) =
>         case annotate l of
>              (Tree_Subst (c:::a) substl) -> Tree_Subst (Loct l ::: a) substl
>   annotate (Numr n) =
>         case annotate n of
>              (Tree_Subst (n:::a) substl) -> Tree_Subst (Numr n ::: a) substl
>   annotate (Boole b) =
>         case annotate b of
>              (Tree_Subst (b:::a) substl) -> Tree_Subst (Boole b ::: a) substl

To help in printing error messages, it is useful to make Syntax
also an instance of the class Show.

> instance Show Syntax where
>   showsPrec p (Expr e) = showsPrec p e
>   showsPrec p (Comm c) = showsPrec p c
>   showsPrec p (Loct l) = showsPrec p l
>   showsPrec p (Numr n) = showsPrec p n
>   showsPrec p (Boole b) = showsPrec p b


	TYPING RULES FOR COMMANDS

> instance Annotatable Command where

>  annotate c@(l `Assign` e) =
>   rule [Loct l ::: Aloc Aint,
>         Expr e ::: Aexp Aint]
>        ----------------------
>        (c ::: Acomm)

>  annotate Skip =
>   axiom (Skip ::: Acomm)

>  annotate c@(c1 `Semi` c2) =
>   rule [Comm c1 ::: Acomm,
>         Comm c2 ::: Acomm]
>        -------------------
>        (c ::: Acomm)


>  annotate c@(If e c1 c2) =
>   rule [Expr e ::: Aexp Abool,
>         Comm c1 ::: Acomm,
>         Comm c2 ::: Acomm]
>        -------------------
>        (c ::: Acomm)

>  annotate c@(While e body) =
>   rule [Expr e ::: Aexp Abool,
>         Comm body ::: Acomm]
>        ----------------------
>        (c ::: Acomm)


	TYPING RULES FOR EXPRESSIONS

> instance Annotatable Expression where

>  annotate e@(Deref l) =
>    rule [Loct l ::: Aloc Aint]
>         ------------------------
>         (e ::: Aexp Aint)

>  annotate e@(Num n) =
>    rule [Numr n ::: Aint]
>         -----------------
>         (e ::: Aexp Aint)

>  annotate e@(BoolLit b) =
>    rule [Boole b ::: Abool]
>         -----------------
>         (e ::: Aexp Abool)

>  annotate e@(e1 `Plus` e2) =
>    rule [Expr e1 ::: Aexp Aint,
>          Expr e2 ::: Aexp Aint]
>         -----------------------
>         (e ::: Aexp Aint)

>  annotate e@(Not e1) =
>    rule [Expr e1 ::: Aexp Abool]
>         ------------------------
>         (e ::: Aexp Abool)

>  annotate e@(e1 `Equals` e2) =
>    ruleIf [Expr e1 ::: Aexp (Avar tau),
>            Expr e2 ::: Aexp (Avar tau)] (\[Aexp tau, _] -> isAtomic tau)
>                                         (\_ -> nullSubst)
>           -----------------------------
>           (e ::: Aexp Abool)
>                                   where tau = (0, "tau")
>                                         isAtomic t = t `elem` [Aint,Abool]

>  annotate e@(e1 `Lt` e2) =
>    rule [Expr e1 ::: Aexp Aint,
>          Expr e2 ::: Aexp Aint]
>         -----------------------
>         (e ::: Aexp Abool)

>  annotate e@(e1 `Gt` e2) =
>    rule [Expr e1 ::: Aexp Aint,
>          Expr e2 ::: Aexp Aint]
>         -----------------------
>         (e ::: Aexp Abool)

>  annotate e@(e1 `Le` e2) =
>    rule [Expr e1 ::: Aexp Aint,
>          Expr e2 ::: Aexp Aint]
>         -----------------------
>         (e ::: Aexp Abool)

>  annotate e@(e1 `Ge` e2) =
>    rule [Expr e1 ::: Aexp Aint,
>          Expr e2 ::: Aexp Aint]
>         -----------------------
>         (e ::: Aexp Abool)

>  annotate e@(e1 `And` e2) =
>    rule [Expr e1 ::: Aexp Abool,
>          Expr e2 ::: Aexp Abool]
>         -----------------------
>         (e ::: Aexp Abool)

>  annotate e@(e1 `Or` e2) =
>    rule [Expr e1 ::: Aexp Abool,
>          Expr e2 ::: Aexp Abool]
>         -----------------------
>         (e ::: Aexp Abool)


	REMAINING RULES

The condition that the i in (Loc i) is positive is enforced by the syntax.

> instance Annotatable Location where
>  annotate l@(Loc i) =
>    axiom (l ::: Aloc Aint)

> instance Annotatable Integer where
>  annotate n =
>    axiom (n ::: Aint)

> instance Annotatable Bool where
>  annotate b =
>    axiom (b ::: Abool)