wf.abs

// This file defines environments and the well-formedness
// constraints upon them, and other interesting things
// like searching through class hierarchies for nearest
// fields/methods.


notation syntax rels ;
import syntax ;



// The environment.
//
// Contains both the subclass and interface hierachies
// and variable type declarations.  Also contains the type definitions
// of all variables and methods of a class and its interface.
// Declarations consist of class declarations, interface declarations 
// and identifier declarations.



datatype MT:varType list × varType option -> methType;


datatype CLASS: (id option × 
                  id set × 
                  (id -> varType option) × 
                  (id × methType) set) -> classDecl

datatype INTERFACE:id set × 
                    (id × methType) set -> interfaceDecl

//type tyenv == (id,classDecl) pfun × 
//              (id,interfaceDecl) pfun;

reserve TE for :tyenv;
reserve C for :id;
reserve i for :id;

def Cdec Cdec((CE,IE):tyenv,C) = PLOOKUP(CE)(C)
def Idec Idec((CE,IE):tyenv,i) = PLOOKUP(IE)(i)


// This relation is useful for characterising the inductive property
// of interfaces induced by the well-formedness conditions
// for environments.  It says that an interface is wellfounded
// if it has no superinterfaces or if some superinterface is
// well founded.  The equivalent for classes is to say that
// the class is a subclass of Object.


lfp wellfounded_interface 
Base [ ]
           Idec(TE,i) = SOME(INTERFACE(EMPTY,x1))
         // ---------------------------------------------
            TE |- i wellfounded_interface

Step [ ]
           Idec(TE,i) = SOME(INTERFACE(Is,x1)) &
            i' :: Is &
            TE |- i' wellfounded_interface
         // ---------------------------------------------
            TE |- i wellfounded_interface




// Well-formed types - not really used


def Args Args(MT(AT,rt)) = AT
def Res Res(MT(AT,rt)) = rt

lfp wf_simptype 
Class [simp,prolog,auto]

         // ------------------------------------
             TE |- (Class(C)) wf_simptype

Interface [simp,prolog,auto]

         // ------------------------------------
            TE |- (Interface(i)) wf_simptype

Prim  [simp,prolog,auto]     

         // ------------------------------------
            TE |- (PrimT(p)) wf_simptype



def wf_vartype
   TE |- VT(st,n) wf_vartype <=> TE |- st wf_simptype

def wf_exptype
   TE |- expty wf_exptype <=> 
         (!vt. expty = SOME(vt) --> TE |- vt wf_vartype);

lfp wf_argtype 
argtype [prolog,auto]
       (!j. j < LEN(AT) --> TE |- EL(j)(AT) wf_vartype)
       // -----------------------------------------
              TE |- AT wf_argtype


lfp wf_methtype 
methtype 
      TE |- AT wf_argtype &
       (!x. R = SOME(x) --> TE |- x wf_vartype)
      // ----------------------------------------
            TE |- (MT(AT,R)) wf_methtype





// The subclass relationship.  
//
// nb. executable version does not terminate for circular class
// structures.


lfp subclass_of 
Refl [simp,auto,prolog]

         // ------------------------------------
            TE |- C subclass_of C

Step 
             Cdec(TE,C) = SOME(CLASS(SOME(Csup),x1,x2,x3)) & TE |- Csup subclass_of C''
        // -----------------------------------------------------------
             TE |- C subclass_of C''





// The implements relationship


lfp implements 
Step  [simp,auto]
             Cdec(TE,C) = SOME(CLASS(x1,Is,x2,x3)) & i :: Is
         // -------------------------------------------------------
             TE |- C implements i




// The subinterface relationship
//
// nb. executable version does not terminate for circular class
// structures.


lfp subinterface_of
Refl [simp,prolog,auto]

         // ------------------------------------
             TE |- i subinterface_of i

Step [ ]
           Idec(TE,i) = SOME(INTERFACE(Is,x1)) &
            i' :: Is & 
            TE |- i' subinterface_of i''
         // ---------------------------------------------
            TE |- i subinterface_of i''



thm subclass-trans 
 TE |- C0 subclass_of C1 & TE |- C1 subclass_of C2 
  --> TE |- C0 subclass_of C2

thm subinterface-trans 
 TE |- C0 subinterface_of C1 & TE |- C1 subinterface_of C2 
  --> TE |- C0 subinterface_of C2

thm wellfounded_interface-trans 
 TE |- C0 subinterface_of C1 & TE |- C1 wellfounded_interface 
  --> TE |- C0 wellfounded_interface





// Widening/Narrowing
//
// The purpose of the wellfounded_interface and subclass_of Object
// constraints is to ensure that any narrower type remains 
// firmly grounded in the environment (if the wider type
// is).  This ensures that transitivity holds when we complete the
// confluent paths down our graph (e.g. C <= I <= Object gives
// C <= Object, and i1 <= i2 <= Object gives i1 <= Object).
//
// This was nasty to figure out...


lfp simpty_widens_to 
Prim      [prolog,auto,simp]

         // ------------------------------------
             TE |- PrimT(pt) simpty_widens_to PrimT(pt)

ClassToClass  [prolog,auto,simp] 
             TE |- C subclass_of C'
         // -------------------------------------------------
             TE |- Class(C) simpty_widens_to Class(C')

InterfaceToInterface [prolog,auto,simp]
             TE |- i subinterface_of i'
         // ---------------------------------------------------
             TE |- Interface(i) simpty_widens_to Interface(i')

InterfaceToObject   [prolog,auto,simp]
           TE |- i wellfounded_interface
       // -----------------------------------------------------
        TE |- Interface(i) simpty_widens_to Class(Object)

ClassToInterface  [prolog,auto]
               TE |- C subclass_of Object &
                TE |- C subclass_of C' & 
                TE |- C' implements i &
                TE |- i subinterface_of i'
        // ---------------------------------------------------------------
           TE |- Class(C) simpty_widens_to Interface(i')



lfp varty_widens_to
ArrayToObject  [prolog,auto,simp]
             0 < n
       // --------------------------------------
             TE |- VT(st,n) varty_widens_to VT(Class Object,0)

Simple  [prolog,auto,simp]
             TE |- st simpty_widens_to st'
       // ---------------------------------------------------------
             TE |- VT(st,n) varty_widens_to VT(st',n)




// Widening for return types - NONE indicates a void return type.
// nb. voids and nulls are different
//
// bug found: prime missing off vt, making it undefined.


lfp expty_widens_to
Some  [prolog,auto,simp]
             TE |- vt varty_widens_to vt'
         // ------------------------------------
             TE |- SOME(vt) expty_widens_to SOME(vt')

None [prolog,auto,simp]

         // ------------------------------------
             TE |- NONE expty_widens_to NONE





// Search for declarations and methods.  Sensibly defined
// for well formed hierarchies of interfaces and classes.
//
// FDec(TE,C,v) indicates the nearest superclass of C (possibly C itself)
// which contains a declaration of the instance variable v, and
// its declared type.


lfp FDec
Hit
          Cdec(TE,C) = SOME(CLASS(Csupo,Is,fields,methods)) &
           PLOOKUP(fields)(v) = SOME(vt)
         // ------------------------------------
             FDec(TE,C,v)(C,vt)

Miss
          Cdec(TE,C) = SOME(CLASS(SOME(Csup),Is,fields,methods)) &
           PLOOKUP(fields)(v) = NONE &
           FDec(TE,Csup,v)(res)
         // ------------------------------------
             FDec(TE,C,v)(res)





// FDecs(TE,C) indicates all the fields in C & all the superclasses of C
// including hidden fields.
//
// For non-cyclic hierarchies, vt is unique for a given (f,C).


lfp FDecs
Hit
          Cdec(TE,C) = SOME(CLASS(Csupo,Is,fields,methods)) &
           f :: PDOM(fields) &
           PLOOKUP(fields)(f) = SOME(vt)
         // ------------------------------------
             FDecs(TE,C)((C,f),vt)

Super
           Cdec(TE,C) = SOME(CLASS(SOME(Csup),Is,fields,methods)) &
            FDecs(TE,Csup)((Cf,f),vt)
         // ------------------------------------
            FDecs(TE,C)((Cf,f),vt)






// MSigs(TE,C,m) indicates all the method declarations (i.e. both the class of
// the declaration and the signature) for method m in class C, or inherited
// from one of its superclasses, and not hidden by any of its superclasses.


lfp MSigsC
Hit
          Cdec(TE,C) = SOME(CLASS(Csupo,Is,fields,methods)) &
           (m,MT(AT,rt)) :: methods
         // ------------------------------------
             MSigsC(TE,C)(m,MT(AT,rt))

Miss
          Cdec(TE,C) = SOME(CLASS(SOME(Csup),Is,fields,methods)) &
           MSigsC(TE,Csup)(m,MT(AT,rt)) &
           (!AT' rt'. (m,MT(AT',rt')) :: methods --> AT <> AT')
         // ------------------------------------
             MSigsC(TE,C)(m,MT(AT,rt))




// When the same methods gets inherited from
// several superinterfaces, there must be a common
// most narrow return type.  The well-formedness rule for environments uses 
// this.
lfp MSigsI

Hit
          Idec(TE,i) = SOME(INTERFACE(Is,methods)) &
           (m,mt) :: methods
         // ------------------------------------
             MSigsI(TE,i)(m,mt)

Miss
          Idec(TE,i) = SOME(INTERFACE(Is,methods)) &
           ((?i'. MSigsI(TE,i')(m,MT(at,rt)) &
             !i''. i'' :: Is & MSigsI(TE,i'')(m,MT(at,rt')) --> TE |- rt expty_widens_to rt')  | 

            (Is = EMPTY & MSigsC(TE,Object)(m,MT(at,rt)))) &

           (!at' rt'. (m,MT(at',rt')) :: methods --> at' <> at)
         // ------------------------------------------------------
             MSigsI(TE,i)(m,MT(at,rt))




// This indicates all the method declarations visible from an array
//
// Arrays always support all methods found in Object, unless they are overridden.
// I haven't yet got arrays supporting methods and fields generic to all arrays,
// i.e. size and clone.


lfp MSigsA
Object
          MSigsC(TE,Object)(m,mt)
         // ------------------------------------
             MSigsA(TE)(m,mt)


def MSigs 
   MSigs(TE, VT(st,dim))(m,mt) <=> 
       MATCH res.
          (    0 < dim                     andalso res = MSigsA(TE)(m,mt)) |
          (?i. dim = 0 & st = Interface(i) andalso res = MSigsI(TE,i)(m,mt)) |
          (?C. dim = 0 & st = Class(C)     andalso res = MSigsC(TE,C)(m,mt)) |
          (?p. dim = 0 & st = PrimT(p)     andalso res = F)