syntax.abs

// Syntax for a subset of Java


notation syntax ;

//type id == string;



// Types.
//
// We distinguish variable types, which correspond to sets of possible runtime
// values for variables, and method types.
//
// Simple variable types are variable types excluding arrays, but
// including objects and interfaces.
//
// Primitive types are simple types excluding objects and interfaces


// enum primType = {bool,char,int,byte,short,long,float,double};
datatype boolT: primType | charT: primType | intT: primType | 
          byteT: primType | shortT: primType | 
          longT: primType | floatT: primType | doubleT: primType

datatype PrimT: primType -> simpType
       | Class: id -> simpType 
       | Interface: id ->simpType


// varType are simpTypes arrayed' to a certain power (normally 0)


datatype VT: simpType × nat -> varType


//type argType == varType list
//type methType == varType list × expType;




// values
// enum val = Bool of bool | Long of long | Char of char 
//          | Byte of byte | Float of iee32 | Double of iee64
//
// Addr and Exn are artifacts of the operational semantics.  They
// could be removed by having a separate syntax for Java SE.
// No well-typed program may contain them.


datatype Bool: bool -> prim
       | Char: uchar -> prim
       | Byte: int8 -> prim
       | Short: int16 -> prim
       | Int: int32 -> prim
       | Long: int64 -> prim
       | Float: ieee32 -> prim
       | Double: ieee64 -> prim


// JavaS
//
// Variables (= lvalues), expressions and statements
//
// Supposedly expressions can't contain statements (e.g. assignments): 
// have to check up on this, though it doesn't make much difference.
//
// Void types to :void and does nothing, like an zero-efect method
// call.  Used for return statements that return Void.
// Note that the type rules preclude expressions that 
// have type :void being subexpressions
// of other expressions.
//


datatype Id: id -> var
       | Field: exp × id -> var
       | Access: exp × exp -> var

       | Prim: prim -> exp
       | Var: var -> exp
       | Call: exp × id × exp list -> exp
       | NewClass: id -> exp
       | NewArray: simpType × exp list × nat -> exp
       | Void: exp

       | Block: stmt list -> stmt
       | If: exp × stmt × stmt -> stmt
       | Assign: var × exp -> stmt
       | Expr: exp -> stmt;


//type methodbody == id × (id list × (id -> varType option)) × stmt list × exp option;
//type classbody == id × id × methodbody list;
//type prog == classbody list;



// JavaA


datatype IdA: id -> cvar
       | FieldA: cexp × id × id -> cvar
       | AccessA: cexp × cexp -> cvar

       | PrimA: prim -> cexp
       | VarA: cvar -> cexp
       | CallA: cexp × argType × id × cexp list -> cexp
       | NewClassA: id × ((id × id) -> varType option) -> cexp
       | NewArrayA: simpType × cexp list × nat -> cexp
       | VoidA: cexp

       | BlockA: cstmt list -> cstmt
       | IfA: cexp × cstmt × cstmt -> cstmt
       | AssignA: cvar × cexp -> cstmt
       | ExprA: cexp -> cstmt;