$Id: WhileNTyping.lhs,v 1.10 2004/10/18 21:36:17 leavens Exp $

AUTHOR: Gary T. Leavens.

Type checking for the language "WhileN" of Chapter 2 of Dave Schmidt's book
"The Structure of Typed Programming Languages" (MIT Press, 1994).
This module is essentially a translation into Haskell of the rules
in chapter 2, section 2.15, with the boolean literals added.
The only significant changes are in the rule for sequential declarations,
and the handling of const declartions, since invocations of const declarations
are parsed as expressions, not as numerals.

> module WhileNTyping where
> import WhileNParser
> import WhileNUnparser
> import Environments
> import TypeAttributes
> import TypeHelpers
> import Subst

This module uses the pritive type attributes defined
in the module TypeAttributes.
It also uses the rule, axiom, ruleIf, etc. functions of TypeHelpers.


                     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
(except for Identifier, which never seems to be needed as a hypothesis).

> data Syntax =
>           Prog Program
>         | Decl Declaration
>         | Type TypeStructure
>         | Comm Command
>         | Expr Expression
>         | Vari Variable
>         | Numr Integer
>         | Boole Bool
>         | IdEx IdentifierExpr

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

> instance Annotatable Syntax where
>   annotate pi (Prog p) = 
>         case annotate pi p of
>              (Tree_Subst (p:::a) substl) -> Tree_Subst (Prog p ::: a) substl
>   annotate pi (Decl d) = 
>         case annotate pi d of
>              (Tree_Subst (d:::a) substl) -> Tree_Subst (Decl d ::: a) substl
>   annotate pi (Type t) = 
>         case annotate pi t of
>              (Tree_Subst (t:::a) substl) -> Tree_Subst (Type t ::: a) substl
>   annotate pi (Comm c) = 
>         case annotate pi c of
>              (Tree_Subst (c:::a) substl) -> Tree_Subst (Comm c ::: a) substl
>   annotate pi (Expr e) =
>         case annotate pi e of
>              (Tree_Subst (e:::a) substl) -> Tree_Subst (Expr e ::: a) substl
>   annotate pi (Vari v) =
>         case annotate pi v of
>              (Tree_Subst (v:::a) substl) -> Tree_Subst (Vari v ::: a) substl
>   annotate pi (Numr n) =
>         case annotate pi n of
>              (Tree_Subst (n:::a) substl) -> Tree_Subst (Numr n ::: a) substl
>   annotate pi (Boole b) =
>         case annotate pi b of
>              (Tree_Subst (b:::a) substl) -> Tree_Subst (Boole b ::: a) substl
>   annotate pi (IdEx i) =
>         case annotate pi i of
>              (Tree_Subst (i:::a) substl) -> Tree_Subst (IdEx i ::: 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 (Prog pr) = showsPrec p pr
>   showsPrec p (Decl d) = showsPrec p d
>   showsPrec p (Type t) = showsPrec p t
>   showsPrec p (Comm c) = showsPrec p c
>   showsPrec p (Expr e) = showsPrec p e
>   showsPrec p (Vari v) = showsPrec p v
>   showsPrec p (Numr n) = showsPrec p n
>   showsPrec p (Boole b) = showsPrec p b
>   showsPrec p (IdEx i) = showsPrec p i

      
Declarations of logical variables.
The following are used in the rules as symbolic names.
They are collected here to get them out of the way.

> delta, tau, theta, pi1, pi2, pi3, pi4 :: LogicalVar
> delta = (0, "delta")
> tau = (0, "tau")
> theta = (1, "theta")
> pi1 = (1, "pi")
> pi2 = (2, "pi") 
> pi3 = (3, "pi")
> pi4 = (4, "pi")


	TYPING RULES FOR PROGRAMS

This is different than the text.  First, to be in the Annotatable class,
this has to take a type environment; but that's useful if we have any
built in abstractions in the inital environment (the pi would then give
the types of these).
Second, we allow declarations to override the names in the initial environment.
This is analogous to our choice for the sequential declaration rule (q.v.),
although it's not really necessary, and makes no difference if the initial
type environment is always empty.

> instance Annotatable Program where

>  annotate pi p@(d `In` c) =
>   ruleSeq
>     [Hyp (pi :- Decl d ::: Adec (Avar pi1)), Def (\[Adec (Api ff1)] ->
>                                                   (pi2 ->- Api
>                                                      (pi `unionMinus` ff1))),
>      Hyp (pi2 :?- Comm c ::: Acomm)]
>     --------------------------------------
>     (pi :- p ::: Acomm)



	    DECLARATIONS

The rule for sequential declarations is different than in the text.
We use unionMinus instead of unionDot to combine the assumed type environment
with the one produced by the first declaration.
This allows, for example, declarations in a module or record to
have names like those used outside, and is in general what is needed for
block structure.

The following are used in side conditions, such as the rule
for simultaneous declarations.

> isDisjoint (Adec (Api pi1)) (Adec (Api pi2)) = disjoint pi1 pi2

> uniondisjoint pi pi1 =
>    (case pi `unionDot` pi1 of
>       (Just pi2) -> pi2
>       Nothing -> error "duplicate declaration")


> instance Annotatable Declaration where

>  annotate pi d@(d1 `Also` d2) =
>   ruleIf [pi :- Decl d1 ::: Adec (Avar pi1),
>           pi :- Decl d2 ::: Adec (Avar pi2)]  (\[t1, t2] -> isDisjoint t1 t2)
>                                               (\[Adec (Api ff1),
>                                                  Adec (Api ff2)] ->
>                                                 (pi3 ->- Api
>                                                   (uniondisjoint ff1 ff2)))
>          ----------------------------------
>          (pi :- d ::: Adec (Avar pi3))

>  annotate pi d@(d1 `Then` d2) = 
>   ruleSeq
>     [Hyp (pi :- Decl d1 ::: Adec (Avar pi1)),  Def (\[Adec (Api ff1)] ->
>                                                     (pi4 ->- Api
>                                                      (pi `unionMinus` ff1))),
>      Hyp (pi4 :?- Decl d2 ::: Adec (Avar pi2)), When (\[t1, t2] ->
>                                                       isDisjoint t1 t2),
>                                                 Def (\[Adec (Api ff1),
>                                                        Adec (Api ff2)] ->
>                                                      (pi3 ->- Api
>                                                       (uniondisjoint ff1 ff2)
>                                                      ))]
>     ------------------------------------------
>     (pi :- d ::: Adec (Avar pi3))


The following cases for const declarations don't just use the rules for
expressions, because we want to flag expressions that don't look like
numerals or identifier expressions (the Numeral syntax in the book)
as syntax errors.

>  annotate pi d@(Const i (Num n)) =
>   rule [pi :- Numr n ::: Aint]
>        ----------------------------------
>        (pi :- d ::: Adec (Api [(i,Aint)]))

>  annotate pi d@(Const i (Ident x)) =
>   rule [pi :- IdEx x ::: Aint]
>        -----------------------------
>        (pi :- d ::: Adec (Api [(i,Aint)]))

>  annotate pi d@(Const i _) =
>   error "syntax error: can't use general exprs in const declarations"

>  annotate pi d@(Fun i e) =
>   rule [pi :- Expr e ::: Aexp (Avar tau)]
>        ----------------------------------------------
>        (pi :- d ::: Adec (Api [(i, Aexp (Avar tau))]))

>  annotate pi d@(Proc i c) =
>   rule [pi :- Comm c ::: Acomm]
>        ------------------------------------
>        (pi :- d ::: Adec (Api [(i,Acomm)]))

>  annotate pi d@(Var i t) =
>   rule [pi :- Type t ::: Aclass (Avar delta)]
>        -----------------------------------------
>        (pi :- d ::: Adec (Api [(i,Avar delta)]))

>  annotate pi d@(Alias i l) =
>   rule [pi :- Vari l ::: Aloc Aint]
>        -----------------------------------------
>        (pi :- d ::: Adec (Api [(i, Aloc Aint)]))

>  annotate pi d@(Class i t) =
>   rule [pi :- Type t ::: Aclass (Avar delta)]
>        -------------------------------------------------
>        (pi :- d ::: Adec (Api [(i,Aclass (Avar delta))]))

>  annotate pi d@(Module i d1) =
>   rule [pi :- Decl d1 ::: Adec (Avar pi1)]
>        -------------------------------------------------
>        (pi :- d ::: Adec (Api [(i,Amodule (Avar pi1))]))

>  annotate pi d@(Import x) =
>   rule [pi :- IdEx x ::: Amodule (Avar pi1)]
>        -------------------------------------
>        (pi :- d ::: Adec (Avar pi1))


	     TYPE STRUCTURES

> instance Annotatable TypeStructure where
>  annotate pi t@NewInt =
>   axiom (pi :- t ::: (Aclass (Aloc Aint)))

>  annotate pi t@(Record d) =
>   rule [pi :- Decl d ::: Adec (Avar pi1)]
>        ----------------------------------------
>        (pi :- t ::: Aclass (Amodule (Avar pi1)))

>  annotate pi t@(TId x) =
>   rule [pi :- IdEx x ::: Aclass (Avar delta)]
>        ------------------------------------
>        (pi :- t ::: Aclass (Avar delta))


            COMMANDS

> instance Annotatable Command where

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

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

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

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

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

>  annotate pi c@(Call x) =
>    rule [pi :- IdEx x ::: Acomm]
>         ------------------------
>         (pi :- c ::: Acomm)


	  EXPRESSIONS

> instance Annotatable Expression where

Note that the rule for identifier expressions is different
from the book, since here we could be dealing with either
a function name or a constant name
(in the book this second case is under Numeral).

>  annotate pi e@(Ident x) =
>    (rule [pi :- IdEx x ::: Aint]
>          ------------------------
>          (pi :- e ::: Aexp Aint))
>    `ruleOr`
>    (rule [pi :- IdEx x ::: Aexp (Avar tau)]
>          ----------------------------------
>          (pi :- e ::: Aexp (Avar tau)))

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

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

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

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

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

>  annotate pi e@(e1 `Equals` e2) =
>     (rule [pi :- e1 ::: Aexp Aint,
>            pi :- e2 ::: Aexp Aint]
>           --------------------------
>           (pi :- e ::: (Aexp Abool)))
>   `ruleOr`
>     (rule [pi :- e1 ::: Aexp Abool,
>            pi :- e2 ::: Aexp Abool]
>           --------------------------
>           (pi :- e ::: (Aexp Abool)))


              VARIABLES

> instance Annotatable Variable where

>  annotate pi v@(Varref x) =
>    rule [pi :- IdEx x ::: Aloc Aint]
>         ----------------------------
>         (pi :- v ::: Aloc Aint)

>  annotate pi v@(Loc i) =
>    axiom (pi :- v ::: Aloc Aint)


              NUMERALS

Note that the numeral rule does not contain identifier expressions,
as these are parsed as expressions.

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


              BOOLEAN LITERALS

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


             IDENTIFIER EXPRESSIONS


> instance Annotatable IdentifierExpr where
>  annotate pi id@(Name i) =
>    ruleIf nohyp                         (\_ -> i `elem` (dom pi))
>                                         (\_ -> (theta ->- justApply pi i))
>           ---------------------------
>           (pi :- id ::: (Avar theta))
>              where nohyp :: [Judgement
>                               (AttribTree IdentifierExpr PrimitiveAttrib)]
>                    nohyp = []

>  annotate pi id@(x `Dot` i) =
>    ruleIf [pi :- IdEx x ::: Amodule (Avar pi1)] (\[t] -> definedIn i t)
>                                                 (\[Amodule (Api ff)] ->
>                                                   (theta ->- justApply ff i))
>           -------------------------------------
>           (pi :- id ::: (Avar theta))
>                                        where definedIn i (Amodule (Api ff)) =
>                                                            i `elem` (dom ff)
>                                              definedIn i _ = False

> justApply pi i =
>   case applyEnv pi i of
>     (Just theta) -> theta
>     Nothing -> Aerr