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

AUTHOR: Gary T. Leavens.

Part of a solution for chapter 1, problem 2.2 part a from
David Schmidt's "The Structure of Typed Programming Languages"
(MIT Press, 1994).

> module Problem_2_2_a_Typing(module Problem_2_2_a_Typing,
>                  module Problem_2_2_a_Parser, module Problem_2_2_a_Unparser,
>                  module CoreTypeAttributes, module CoreTypeHelpers) where
> import Problem_2_2_a_Parser
> import Problem_2_2_a_Unparser
> 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 (Avar tau),
>         Expr e ::: Aexp (Avar tau)]
>        ----------------------
>        (c ::: Acomm)
>                                   where tau = (0, "tau")

>  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 (Avar tau)]
>         ---------------------------
>         (e ::: Aexp (Avar tau))
>                                   where tau = (0, "tau")

>  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 tau i) is positive is enforced by the syntax.

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

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

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