link2_0.art

notation syntax rels runtime rstatics ;
import syntax wf wfenv statics1 cstatics runtime0 link2_0 ;



// Lemma 3.1. If a class inherits a method declaration with method type
// then it provides a method body that satisfies that method type.
//
// Both the static (MSigsC) search and the runtime (MethBody) search 
// begin at the same class (C).  We prove in wfenv.art that as we move 
// to subclasses the method is still found by the static MDecs search, 
// with a possible narrower return type.
//
// This first part says method bodies are always found.



thm inheritance-is-implemented
if TE wf_tyenv TE_wf 
    TE |- cprog cprog_hastype cprog_types
    MSigsC(TE,C)(m,mt) search
then  ?Xord body. MethBodyC(m,Args(mt),C,cprog)(Xord,body) g


proceed by rule induction on search with C variable;

  case Hit
    mt = MT(AT,rt) 
    Cdec(TE,C) = SOME(CLASS(Csupo,Is,fields,methods)) [rw,auto]
    (m,MT(AT,rt)) :: methods m_in_methods;

    consider cbody,Csupo',mbodies st
        (C,cbody) :: ELS(cprog) cbody_in_prog
        cbody =  (Csupo',mbodies) 
        (C,TE) |- cbody cclass_hastype (Csupo,Is,fields,methods) cbody_types 
      by CPROG_HASTYPE__classes_exist [cprog,TE,C],cprog_types,Cdec,PDOM,IN_ELIM,PFORALL_SPLIT;

    consider mbody,Xord,Xtys,body st
        Csupo = Csupo' 
        (m,mbody) :: ELS(mbodies)  
        mbody = ((Xord,Xtys),body) 
        (C,TE) |- mbody cmethod_hastype MT(AT,rt) a2
      by CCLASS_HASTYPE__methods_exist [TE,methods,fields,Is,Csupo/Csupo',Csupo'/Csupo],
         CCLASS_HASTYPE__subclasses_match [TE,methods,fields,Is,Csupo/Csupo',Csupo'/Csupo],
         cbody_types,m_in_methods,PEXISTS_SPLIT;

    then qed by MethBodyC__Hit,cbody_in_prog, g [Xord,body],Args, rule cases on a2;


  case Miss
    mt = MT(AT,rt) 
    Cdec(TE,C) = SOME(CLASS(SOME(Csup),Is,fields,methods)) [rw,auto]
    ?Xord body. MethBodyC(m,Args(mt),Csup,cprog)(Xord,body) ihyp
    MSigsC(TE,Csup)(m,mt)
    !AT' rt'. (m,MT(AT',rt')) :: methods --> AT <> AT' alldiff;

    consider Xord,body st 
       MethBodyC(m,AT,Csup,cprog)(Xord,body) recurse by ihyp,Args;

    consider cbody,mbodies,Csupo' st
        (C,cbody) :: ELS(cprog) cbody_in_prog
        cbody = (Csupo',mbodies) 
        (C,TE) |- cbody cclass_hastype (SOME(Csup),Is,fields,methods) cbody_types
      by CPROG_HASTYPE__classes_exist [cprog,TE,C],cprog_types,Cdec,PDOM,IN_ELIM,PFORALL_SPLIT;

    have Csupo' = SOME(Csup) 
        !m mbody. (m,mbody) :: ELS(mbodies) -->
         ?mt. (m,mt) :: methods &
             (C,TE) |- mbody cmethod_hastype mt t1 
             by CCLASS_HASTYPE__methoddecs_exist,CCLASS_HASTYPE__subclasses_match,cbody_types;

    // suffices to show the following condition
    sts !Xord Xtys body. (m,((Xord,Xtys),body)) :: ELS(mbodies) --> MAP(PAPPLY(Xtys))(Xord) <> AT
        by MethBodyC__Miss [cprog,mbodies,C/C,Csup/Csup],
           g [Xord,body],recurse,cbody_in_prog,Args;

    then consider Xord',Xtys',body',mbody' st
        + (m,mbody') :: ELS(mbodies) m_in_mbodies
        + mbody' = ((Xord',Xtys'),body') 
        - MAP(PAPPLY(Xtys'))(Xord') <> AT;

    consider mt' st 
         (m,mt') :: methods m_in_methods
         (C,TE) |- mbody' cmethod_hastype mt' t2 by t1 [mbody',m],m_in_mbodies ;

    let AT' = MAP(PAPPLY(Xtys'))(Xord') ;

    consider rt' st mt' =  MT(AT',rt') by rule cases on t2;
    then qed by alldiff [AT',rt'],m_in_methods;

  end;



// This second part says that if a method body is found for a 
// call to an object method, then it is well typed. 


thm implemented-object-inheritance-is-welltyped
if TE wf_tyenv TE_wf 
    TE |- cprog cprog_hastype cprog_types
    MSigsC(TE,C)(m,MT(AT,rt2)) search
    MethBodyC(m,AT,C,cprog)(Xord,body) fetch
then  ?Xtys C''. TE |- C subclass_of C'' &
                  (C'',TE) |- ((Xord,Xtys),body) cmethod_hastype MT(AT,rt2) g

proceed by rule induction on fetch with C variable;

  case Hit
    (C,(Csupo,mbodies)) :: ELS(cprog) cclass_in_prog
    (m,mbody) :: ELS(mbodies) mbody_in_mbodies
    mbody = ((Xord,Xtys),body) 
    MAP(PAPPLY(Xtys))(Xord) = AT ;

   let cclass = (Csupo,mbodies) ;

   consider ctyp,Is1,fields1,methods1,Csupo' st 
        Cdec(TE,C) = SOME(CLASS(ctyp)) [rw,auto]
        ctyp = (Csupo',Is1,fields1,methods1) 
        (C,TE) |- cclass cclass_hastype ctyp cclass_types
      by CPROG_HASTYPE__classdecs_exist [cprog,cclass,C,TE],cprog_types,cclass_in_prog;

   consider mt st 
        Csupo = Csupo' 
        (m,mt) :: methods1 m_in_methods1
        (C,TE) |- mbody cmethod_hastype mt mbody_types
      by CCLASS_HASTYPE__methoddecs_exist,
         CCLASS_HASTYPE__subclasses_match,cclass_types,mbody_in_mbodies;

   consider rt st mt = MT(AT,rt)  by rule cases on mbody_types;

   per cases
     case Cdec(TE,C) = SOME(CLASS(Csupo,Is2,fields2,methods2)) [rw,auto]
          (m,MT(AT,rt2)) :: methods2 m2;

      have ctyp = (Csupo,Is2,fields2,methods2) ;

      have mt = MT(AT,rt2) by 
               WF_TYENV__class_argtypes_unique [TE,mt/mt1,MT(AT,rt2)/mt2,C/C,m/m,methods1,Csupo/Csupo,Is1,fields1],
               TE_wf,PDOM,IN_ELIM,Cdec,m2,m_in_methods1,Args;
      then qed by mbody_types,g [C,Xtys];

     case Cdec(TE,C) = SOME(CLASS(SOME(Csup),Is2,fields2,methods2)) [rw,auto]
          MSigsC(TE,Csup)(m,MT(AT,rt2)) 
          !AT' rt'. (m,MT(AT',rt')) :: methods2 --> AT <> AT' no_match;

       have ctyp = (SOME(Csup),Is2,fields2,methods2) ;
       contradiction by m_in_methods1,no_match [AT,rt];

   end by rule cases on search;


  case Miss
    (C,(SOME(Csup),mbodies)) :: ELS(cprog) cclass_in_prog
    !Xord Xtys body. (m,((Xord,Xtys),body)) :: ELS(mbodies) --> MAP(PAPPLY(Xtys))(Xord) <> AT no_match
    MSigsC(TE,Csup)(m,MT(AT,rt2)) -->
     ?Xtys C''. TE |- Csup subclass_of C'' &
                (C'',TE) |- ((Xord,Xtys),body) cmethod_hastype MT(AT,rt2) ihyp
    MethBodyC(m,AT,Csup,cprog)(Xord,body)

   let cclass = (SOME(Csup),mbodies) ;

   consider ctyp, Is,fields,methods,Csupo' st 
        Cdec(TE,C) = SOME(CLASS(ctyp)) [rw,auto]
        ctyp = (Csupo',Is,fields,methods) [auto,rw]
        (C,TE) |- cclass cclass_hastype ctyp cclass_types
      by CPROG_HASTYPE__classdecs_exist [TE,cprog,cclass,C],cprog_types,cclass_in_prog;


   have Csupo' = SOME(Csup) 
        !m mt. (m,mt) :: methods -->
         ?mbody. (m,mbody) :: ELS(mbodies) & 
                (C,TE) |- mbody cmethod_hastype mt mbodies_exist
        by CCLASS_HASTYPE__methods_exist,CCLASS_HASTYPE__subclasses_match,cclass_types;

   per cases
     case Cdec(TE,C) = SOME(CLASS(Csupo,Is2,fields2,methods2)) [rw,auto]
          (m,MT(AT,rt2)) :: methods2 m2;

      have ctyp = (Csupo,Is2,fields2,methods2) ;

      consider mbody,Xord2,Xtys2,body2 st 
          (m,mbody) :: ELS(mbodies) m_in_mbodies
          mbody = ((Xord2,Xtys2),body2) 
          (C,TE) |- mbody cmethod_hastype MT(AT,rt2) mbody_types
        by mbodies_exist [m,MT(AT,rt2)],m2;
      have AT = MAP(PAPPLY(Xtys2))(Xord2) by rule cases on mbody_types;
      then contradiction by no_match,m_in_mbodies,Cdec;

     case Cdec(TE,C) = SOME(CLASS(SOME(Csup),Is2,fields2,methods2)) [rw,auto]
          MSigsC(TE,Csup)(m,MT(AT,rt2)) m1
          !AT' rt'. (m,MT(AT',rt')) :: methods2 --> AT <> AT' no_match;

       have ctyp = (SOME(Csup),Is2,fields2,methods2) ;
       consider Xtys',C'' st 
          TE  |- Csup subclass_of C'' 
          (C'',TE) |- ((Xord,Xtys'),body) cmethod_hastype MT(AT,rt2) by ihyp,m1;
       then qed by g [Xtys',C''], subclass_of__Step;

   end by rule cases on search;

end;


// Same thing for calling array methods...


thm implemented-array-inheritance-is-welltyped
 if TE wf_tyenv 
    TE |- cprog cprog_hastype
    0 < dim
    MSigsA(TE)(m,MT(AT,rt))
    MethBodyA(m,AT,VT(st,dim),cprog)(Xord,body)
then ?Xtys C'. TE |- VT(st,dim) varty_widens_to VT(Class(C'),0) &
                   (C',TE) |- ((Xord,Xtys),body) cmethod_hastype MT(AT,rt)
  then qed by MSigsA__elim,MethBodyA,
         implemented-object-inheritance-is-welltyped [TE,cprog,AT,Object/C,m/m,Xord,body,rt],
         varty_widens_to-trans [TE,VT(Class(Object),0)/vt2,VT(st,dim)/vt1],varty_widens_to__ArrayToObject [TE,st];


// And thus for any sort of heap object...


thm implemented-inheritance-is-welltyped
    TE wf_tyenv &
     TE |- cprog cprog_hastype &
     MSigs(TE,VT(st,dim))(m,MT(AT,rt)) &
     MethBody(m,AT,VT(st,dim),cprog)(Xord,body)
     --> ?Xtys C'. TE |- VT(st,dim) varty_widens_to VT(Class(C'),0) &
                   (C',TE) |- ((Xord,Xtys),body) cmethod_hastype MT(AT,rt)
qed by MSigs,MethBody,implemented-array-inheritance-is-welltyped [TE,cprog],
       implemented-object-inheritance-is-welltyped [TE,cprog],
       structural cases on st,ZERO_CASES [dim]