Term.thy

(*  Title:      isabelle/Bali/Term.thy
    ID:         $Id: Term.thy,v 1.2 1997/10/22 12:00:11 oheimb Exp $
    Author:     David von Oheimb
    Copyright   1997 Technische Universitaet Muenchen

Java expressions and statements

design concerns:
* all variables may alternatively be handled in a very uniform way, by 
  representing arrays as special sort of class instances, and by 
  representing the current invocation frame as an instance of a special pseudo
  class (one per method definition) and identifying a special location called
  StackTop (as opposed to Heap) pointing to it. The semantic memory model would
  then be closer to the uniform memory of an usual machine implementation.
  'this' could then be represented as a special field within that object.
  Instead, use a different approach for each kind of variable because: 
  +  it is closer to the language and therefore easier to read
  +  there is no extra handling (e.g. invariants) for special constructs 
     like StackTop needed
  -  there is more redundancy in the syntax and some semantic aspects 
     of variable access and assignment

simplifications:
* no super yet
* no unary, binary, ..., operators
* access to field x in current class via this.x
* NewA creates just one-dimensional arrays;
  initialization of further subarrays may be simulated with nested NewAs
* no constructors, initializers and finalizers yet
* for the transition semantics, the 'Lit' constructor is allowed to contain a
  reference value. this is assumed to be prohibited in the input language and
  is checked during type-checking.

* no throw and try yet
* no synchronized
* result expression instead of return statement (see Decl.thy)
* no secondary forms of if, while (e.g. no for) (may be easily simulated)
* no switch, break, continue, no labels (may be simulated with while)
* for the transition semantice, the 'while' constructor needs an extra copy
  of the loop condition. Both expressions are assumed to be initially identical.
* for the transition semantice, the method call produces an intermediate method
  body construct that enables the restoration of the previous 'stack' contents.

* the compiler is supposed to add the annotations {_} during type-checking. this
  transformation is left out as its result is checked by the type rules anyway

*)

Term = Type + 

types   loc		(* locations, i.e. abstract references on objects *)
arities loc :: term




datatype val_		(* name non 'val' because of clash with ML token *)
	= Unit		(* dummy result value of void methods *)
	| Null		(* null reference *)
	| Bool bool	(* Boolean value *)
	| Intg int	(* integer value *) (* Name Intg instead of Int because
					       of clash with HOL/Set.thy *)
	| Addr loc	(* addresses, i.e. locations of objects *)
types	val = val_
(*translations "val" == (type) "val_"*)

datatype 'a e
	= This
	| NewC	tname		   (* class instance creation *)
	| NewA	ty ('a e)		   (* array creation *)
	| Cast	ty ('a e)		   (* type cast *)
	| Lit	val		   (* literal value, also references *)
	| LAcc			   (* local (incl. parameter) access *)
	| LAss		     ('a e)(* local (incl. parameter) assignment *)
	| FAcc ('a e) ref_ty ename (* field access *) ("_{_}._"	[90,10,99   ]90)
	| FAss ('a e) ref_ty ename 
	                     ('a e)(* field ass. *)("_{_}._:=_" [80,10,99,80]70)
	| AAcc ('a e)('a e)	   (* array access *) ("_[_]"	[90,10      ]90)
	| AAss ('a e)('a e)  ('a e)(* array ass. *)   ("_[_]:=_"[80,10,   80]70)
	| Call ('a e)mname ty('a e)(* method call*)("_.._{_}'(_')" [80,10,99]80)
	| Body  'a ('a e) val loc  (* method body*)

datatype stmt
	= Skip			   (* empty      statement *)
	| Expr (stmt e)		   (* expression statement *)
	| Comp	stmt    stmt	   ("_;; _"			[      61,60]60)
	| Cond (stmt e) stmt stmt  ("If'(_') _ Else _"		[   80,79,79]70)
	| Loop (stmt e) stmt	   ("While'(_') _"		[      80,79]70)

types expr = stmt e

end