src/HOL/MicroJava/J/Term.thy
author kleing
Thu Sep 21 10:42:49 2000 +0200 (2000-09-21)
changeset 10042 7164dc0d24d8
parent 9348 f495dba0cb07
child 10061 fe82134773dc
permissions -rw-r--r--
unsymbolized
     1 (*  Title:      HOL/MicroJava/J/Term.thy
     2     ID:         $Id$
     3     Author:     David von Oheimb
     4     Copyright   1999 Technische Universitaet Muenchen
     5 
     6 Java expressions and statements
     7 *)
     8 
     9 Term = Value + 
    10 
    11 datatype binop = Eq | Add	   (* function codes for binary operation *)
    12 
    13 datatype expr
    14 	= NewC	cname		   (* class instance creation *)
    15 	| Cast	cname expr	   (* type cast *)
    16 	| Lit	val		   (* literal value, also references *)
    17         | BinOp binop  expr expr   (* binary operation *)
    18 	| LAcc vname		   (* local (incl. parameter) access *)
    19 	| LAss vname expr          (* local assign *) ("_::=_"  [      90,90]90)
    20 	| FAcc cname expr vname    (* field access *) ("{_}_.._"[10,90,99   ]90)
    21 	| FAss cname expr vname 
    22 	                  expr     (* field ass. *)("{_}_.._:=_"[10,90,99,90]90)
    23 	| Call expr mname (ty list) (expr list)(* method call*)
    24                                     ("_.._'({_}_')" [90,99,10,10] 90)
    25 and stmt
    26 	= Skip			   (* empty      statement *)
    27 	| Expr expr		   (* expression statement *)
    28 	| Comp stmt stmt	   ("_;; _"			[      61,60]60)
    29 	| Cond expr stmt stmt      ("If'(_') _ Else _"		[   80,79,79]70)
    30 	| Loop expr stmt	   ("While'(_') _"		[      80,79]70)
    31 end