rsyntax.abs

// Syntax of JavaR - runtime terms in the abstract machine
//
// Ids are just place holders and are replaced by stack references when 
// a procedure is called.  A stack reference contains a frame number 
// and an id.  (actually
// Ids are StackVars with any frame number - a bit of conflation that I may get
// rid of but it makes the typing rules simpler).


notation syntax rsyntax ;
import syntax ;

datatype RPrim: prim -> rval       
       | RExn: string -> rval
       | RAddr: int option -> rval

datatype RStackVar: nat × id -> rvar
       | RAccess: rexp × rexp -> rvar
       | RField: rexp × id × id -> rvar

       | RValue: rval -> rexp
       | RVar: rvar -> rexp
       | RNewClass: id × ((id × id) -> varType option) -> rexp
       | RNewArray: simpType × rexp list × nat -> rexp
       | RCall: rexp × argType × id × rexp list -> rexp
       | RVoid: rexp
       | RBody: (rstmt × rexp) -> rexp

       | RBlock: rstmt list -> rstmt

       | RIf: rexp × rstmt × rstmt -> rstmt
       | RAssign: rvar × rexp -> rstmt
       | RExpr: rexp -> rstmt;