######################################################################
                               SUBTYPING
######################################################################

Subtyping rules:

                        ---------- (top)
                         T <: Any
                         
                      ------------- (bottom)
                       Bottom <: T
            
                         -------- (refl)
                          T <: T
            
                         T1 <: T2
                  ---------------------- (list)
                   List[T1] <: List[T2]
            
                 {T2} <: {T1}      R1 <: R2
              --------------------------------- (func)
                ({T1}) => R1  <:  ({T2}) => R2


Definition of max:

                 T2 <: T1                   T1 <: T2
            ------------------         ------------------
             T1 = max(T1, T2)           T2 = max(T1, T2)


######################################################################
                           ATTRIBUTE GRAMMAR
######################################################################

P    = Program { D } B(tb)      Create a scope S for the function
                                declarations { D } and analyze B in S.

B(t) = Body { S } E(t)          Analyze { S } and E in a new scope
                                which is embedded in the current scope.

D    = FunDef ident { F }({ta}) T(tt) E(te)
                                Create a local scope S embedded in the
                                current scope R, analyze the formal
                                parameters in S, enter a new symbol
                                in R with name 'ident' and type 'tf',
                                and analyze the body E in scope S.
                                tf = ({ta}) => tt
                                te <: tt

F(t) = Formal ident T(t)        Enter a new symbol in the current scope
                                with name 'ident' and type 't'.

T(t) = BasicType Unit           t = Unit
     | BasicType Any            t = Any
     | BasicType Int            t = Int
     | ListType T(tt)           t = List[tt]
     | FunType {T}({ts}) T(tt)  t = ({ts}) => tt

S    = VarDef F(tf) E(te)       First analyze the expression E and then
                                F in the current scope.
                                te <: tf
     | While E(Int) E(te)
     | Exec E(te)

E(t) = If E(Int) E(t1) E(t2)    t = max(t1, t2)
     | Assign ident E(t)        sym = lookup(ident)
                                sym.isVariable
                                t <: sym.type
     | Binop Cons E(th) E(tt)   t = max(List[th], tt)
     | Binop O E(Int) E(Int)    O is not Cons
                                t = Int
     | Listop Head E(List[t])
     | Listop Tail E(t)         t <: List[Any]
     | Listop IsEmpty E(te)     te <: List[Any]
                                t = Int
     | Ident ident              t = lookup(ident).type
     | UnitLit                  t = Unit
     | NilLit                   t = List[Bottom]
     | IntLit int               t = Int
     | Apply E(tf) { E }({ta})  tf = ({ts}) => t
                                tf <: ({ta}) => Any
     | B(t)


######################################################################
$Id: attrib.txt,v 1.1 2004/02/24 16:10:55 schinz Exp $