statics2.abs

notation syntax rels ;
import syntax wf statics1 ;

reserve TE for :tyenv;
reserve VE for :varenv;
reserve G for :tyenv × varenv;
reserve C for :id;
reserve id for :id;




//


lfp ApplMeths
A
        LEN(AT) = n &
         MSigs(TE,vt)(m,MT')  &  
         LEN(Args(MT')) = n &
         (!i. i < n --> TE |- EL(i)(AT) varty_widens_to EL(i)(Args(MT')))
      // --------------------------------------------------------------------
         ApplMethsC(TE,vt,m,AT)(MT')




lfp more_special_than
A
        LEN(AT) = n &
         LEN(AT') = n &
         (!j. j < n --> TE |- EL(j)(AT) varty_widens_to EL(j)(AT'))
    // ------------------------------------------------------
            TE |- (AT,res)) more_special_thanI (AT',res')


// find the minima of the more special partial order.  There
// may be more than one, though this is a type error.
lfp MostSpec
A
      ApplMeths(TE,vt,m,AT)(MT') &
       (!C'' MT''. ApplMeths(TE,vt,m,AT)(MT'') &
                   TE |- MT'' more_special_than MT'
                   --> MT' = MT'')
       // ---------------------------------------------------------
            MostSpec(TE,vt,m,AT)(MT')


// bug detected:  input/output analysis told me of a mistyped
// variable
//
// Expressions can type to void (== NONE) because a method
// call may not return a value, and a method call can be
// part of an expression.
lfp exp_hastype 
Id            PLOOKUP(VE)(x) = SOME(vt)
        // -----------------------------------------------
                (TE,VE) |- Id(x) var_hastype vt

Access  (TE,VE) |- arr exp_hastype SOME(VT(st,dim)) &
            0 < dim  &
            (TE,VE) |- e exp_hastype SOME(VT(PrimT(intT),0))
      // ----------------------------------------------------
            (TE,VE) |- Access(arr,e) var_hastype VT(st,dim-1)

Field   (TE,VE) |- obj exp_hastype SOME(VT(Class(C),0)) &
            FDec(TE,C,f)(C',vt')
      // ----------------------------------------------------
            (TE,VE) |- Field(obj,f) var_hastype vt'



Var     (TE,VE) |- v var_hastype vt
     // ---------------------------------------
            (TE,VE) |- Var(v) exp_hastype SOME(vt)

Void  
     // --------------------------------
           (TE,VE) |- Void exp_hastype NONE

Prim    p prim_hastype pt
     // ----------------------------------------
            (TE,VE) |- Prim(p) exp_hastype SOME(VT(PrimT(pt),0))

NewClass  TE |- C reachable_class &
             (!fld vt. (fld,vt) :: FDecs(TE,C) --> TE |- vt wf_vartype);
      // ----------------------------------------------
            (TE,VE) |- NewClass(C) exp_hastype SOME(VT(Class(C),0))

NewArray     0 < LEN(dims)+ext &
                TE |- st wf_simptype &
                (!j. j < LEN(dims) --> (TE,VE) |- EL(j)(dims) exp_hastype SOME(VT(PrimT(intT),0)))
      // ---------------------------------------------------------------------
            (TE,VE) |- NewArray(st,dims,ext) exp_hastype SOME(VT(st,LEN(dims)+ext))


// should rationalise these rules into one!
Call  LEN(Es) = n &
          LEN(Vts) = n &
          (!j. j < n --> (TE,VE) |- EL(j)(Es) exp_hastype SOME(EL(j)(Vts))) &
          (TE,VE) |- e exp_hastype SOME(vt) &
          MostSpecC(TE,vt,m,Vts)(mt) &
          (!y. MostSpecC(TE,vt,m,Vts)(y) --> mt = y)
      // ----------------------------------------------------
            (TE,VE) |- Call(e,m,Es) exp_hastype Res(mt)




// Execution:  The CCall and ICall rules are tricky, because the third
// line incrmentally creates an array Vts, i.e. we have < new
// pattern variables.  We need explicit support for variable
// sized collections of pattern variables, indexed by numbers.  This
// is like building in primitives for arrays in programming languages.
//
// We make LEN(pvar) = exp a declaration of an array of pattern
// variables, and EL(exp)(pvar) an acceptable declaration of
// a pattern variable.
//
// Nb. whether an array access is an instance of a pattern variable
// or an expression is statically undecidable: extra information
// needs to be provided by the user.
//
// Could broaden this to pattern vars indexed by any finite set??


// stmt_hastype
//
// env |- stmt stmt_hastype <varType option>
//
// options used for void types, which are not regular types.


// bug detected: redesigned stmt_hastype so it doesn't actually
// return a type.  Detected because of difficulty of evaluating
// the constructions used.
//
// BUG: For the moment I am forcing Expr() constructs to type to :void.
lfp stmt_hastype 
Assign         (TE,VE) |- v var_hastype vt &
                  (TE,VE) |- e exp_hastype SOME(vt') &
                  TE |- vt' varty_widens_to vt
     // -----------------------------------------------
                   (TE,VE) |- Assign(v,e) stmt_hastype

If          (TE,VE) |- stmt1 stmt_hastype &
               (TE,VE) |- stmt2 stmt_hastype &
               (TE,VE) |- e exp_hastype SOME(VT(PrimT(boolT),0))
     // ------------------------------------------------------------------
                (TE,VE) |- If(e,stmt1,stmt2) stmt_hastype

Block        !j. j < LEN(stmts) --> (TE,VE) |- EL(j)(stmts) stmt_hastype
     // ------------------------------------------------------------------
                (TE,VE) |- Block(stmts) stmt_hastype

Expr            (TE,VE) |- e exp_hastype NONE
      // ----------------------------------------
                  (TE,VE) |- Expr(e) stmt_hastype


// bug detected: case when no return statement was specifed was
// screwy
lfp body_hastype 
body 
        (TE,VE) |- stmt stmt_hastype &
         (TE,VE) |- exp exp_hastype vt
    // ---------------------------------------------------------------
              (TE,VE) |- (stmt,exp) body_hastype vt





// method_hastype
//
// 
// The complex FOLDL expression iterates through the bound variables,
// replacing each by a fresh variable, and adding the new variable
// to the environment.


//
// bug found: AT was undeclared.
//lfp method_hastype 
//(mbody)
//      LEN(Xs) = n &
//       (!j1. j1 < n -->
//        !j2. j2 < n --> 
//        EL(j1)(Xs) = EL(j2)(Xs) --> j1 = j2) &
//       FOLDL( LAM(G,body). LAM(Xname,Xty). 
//            ( LAMZname. (Vadd(G,Zname,Xty),
//                       body_subst(Xname,Zname) body))
//            (fresh(Bvars G))) (G,body) Xs = (G',body') &
//       G' |- body' body_hastype rt' &
//       G |- rt' expty_widens_to rt
//   // -------------------------------------------------------------------
//         G |- (Xs,body) method_hastype MT(MAP(SND)(Xs),rt)
//

       
lfp method_hastype 
mbody
      ELS(Xord) = PDOM(Xtys) &
       ORDERING(Xord) = T &
       (TE,Xtys <+ (this, VT(Class(C),0))) |- body body_hastype rt' &
       TE |- rt' expty_widens_to rt
   // -------------------------------------------------------------------
         (C,TE) |- ((Xord,Xtys),body) method_hastype MT(MAP(PAPPLY(Xtys))(Xord),rt)



// BUG: we don't check that everything in class has a decl.  We do
// check it the other way around.
//
// bug found by execution: this was getting assigned the wrong type.
lfp class_hastype 
cbody
      Cdec(TE,C) = SOME(CLASS(Csupo,Is,fields,methods)) &
       (!m mt. (m,mt) :: methods -->
        ?mbody. (m,mbody) :: ELS(mbodies) & 
                (C,TE) |- mbody method_hastype mt)
   // -------------------------------------------------------------------
         TE |- (C,(Csupo,mbodies)) class_hastype (Csupo,Is,fields,methods)


lfp prog_hastype 
prog
      (!C ctyp. C :: PDOM(FST(TE)) & Cdec(TE,C) = SOME(CLASS(ctyp)) -->
        ?cbody. cbody :: ELS(prog) &
            TE |- cbody class_hastype ctyp) &
       (!cbody. cbody :: ELS(prog) -->
        ?C ctyp. C :: PDOM(FST(TE)) & Cdec(TE,C) = SOME(CLASS(ctyp)) &
            TE |- cbody class_hastype ctyp)
   // -------------------------------------------------------------------
        TE |- (prog:prog) prog_hastype