cstatics.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;

// 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 cexp_hastype 
Id            PLOOKUP(VE)(x) = SOME(vt)
        // -----------------------------------------------
                (TE,VE) |- IdA(x) cvar_hastype vt

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


Var     (TE,VE) |- v cvar_hastype vt
     // ---------------------------------------
            (TE,VE) |- VarA(v) cexp_hastype SOME(vt)

Void  
     // --------------------------------
           (TE,VE) |- VoidA cexp_hastype NONE

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


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


FieldA 
         (TE,VE) |- obj cexp_hastype SOME(VT(Class(C),0)) &
           ((C',f),vt) :: FDecs(TE,C)
      // ----------------------------------------------------
            (TE,VE) |- FieldA(obj,C',f) cvar_hastype vt

NewClassA 
            TE |- C wf_class &
             (!fld vt. (fld,vt) :: FDecs(TE,C) --> TE |- vt wf_vartype) &
             flds = PGRAPH {fspec | FDecs(TE,C)(fspec)}
      // -----------------------------------------------------------------
            (TE,VE) |- NewClassA(C,flds) cexp_hastype SOME(VT(Class(C),0))

CallA 
         LEN(args) = nargs &
          LEN(AT) = nargs &
          (TE,VE) |- e cexp_hastype SOME(vt) &
          MSigs(TE,vt)(m,MT(AT,rt))
      // ----------------------------------------------------
         (TE,VE) |- CallA(e,AT,m,args) cexp_hastype rt




// 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??


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


// bug detected: redesigned cstmt_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 cstmt_hastype 
Assign         (TE,VE) |- v cvar_hastype vt &
                  (TE,VE) |- e cexp_hastype SOME(vt') &
                  TE |- vt' varty_widens_to vt
     // -----------------------------------------------
                   (TE,VE) |- AssignA(v,e) cstmt_hastype

If          (TE,VE) |- stmt1 cstmt_hastype &
               (TE,VE) |- stmt2 cstmt_hastype &
               (TE,VE) |- e cexp_hastype SOME(VT(PrimT(boolT),0))
     // ------------------------------------------------------------------
                (TE,VE) |- IfA(e,stmt1,stmt2) cstmt_hastype

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

Expr            (TE,VE) |- e cexp_hastype NONE
      // ----------------------------------------
                  (TE,VE) |- ExprA(e) cstmt_hastype


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





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


       
lfp cmethod_hastype 
mbody
      ELS(Xord) = PDOM(Xtys) &
       ORDERING(Xord) = T &
       (TE,(Xtys <+ (this, VT(Class(C),0)))) |- body cbody_hastype rt' &
       TE |- rt' expty_widens_to rt
   // -------------------------------------------------------------------
         (C,TE) |- ((Xord,Xtys),body) cmethod_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.
def cclass_hastype
   (C,TE) |- (Csupo,mbodies) cclass_hastype (Csupo',Is,fields,methods) <=>
       (Csupo = Csupo')  &
       Cdec(TE,C) = SOME(CLASS(Csupo,Is,fields,methods)) &

       (!m mt. (m,mt) :: methods -->
        (?mbody. (m,mbody) :: ELS(mbodies) & 
                (C,TE) |- mbody cmethod_hastype mt) ) &

       (!m mbody. (m,mbody) :: ELS(mbodies) -->
        (?mt. (m,mt) :: methods & 
             (C,TE) |- mbody cmethod_hastype mt) )

def cprog_hastype
  TE |- (cprog:cprog) cprog_hastype <=>
       (!C ctyp. C :: PDOM(FST(TE)) & Cdec(TE,C) = SOME(CLASS(ctyp)) -->
       (?cclass. (C,cclass) :: ELS(cprog) &
            (C,TE) |- cclass cclass_hastype ctyp) ) &

       (!C cclass. (C,cclass) :: ELS(cprog) -->
       (?ctyp. Cdec(TE,C) = SOME(CLASS(ctyp)) &
            (C,TE) |- cclass cclass_hastype ctyp) )