src/HOL/MicroJava/J/Term.thy
changeset 10061 fe82134773dc
parent 10042 7164dc0d24d8
child 10069 c7226e6f9625
equal deleted inserted replaced
10060:4522e59b7d84 10061:fe82134773dc
     9 Term = Value + 
     9 Term = Value + 
    10 
    10 
    11 datatype binop = Eq | Add	   (* function codes for binary operation *)
    11 datatype binop = Eq | Add	   (* function codes for binary operation *)
    12 
    12 
    13 datatype expr
    13 datatype expr
    14 	= NewC	cname		   (* class instance creation *)
    14 	= NewC	cname              (* class instance creation *)
    15 	| Cast	cname expr	   (* type cast *)
    15 	| Cast	cname expr         (* type cast *)
    16 	| Lit	val		   (* literal value, also references *)
    16 	| Lit	val                  (* literal value, also references *)
    17         | BinOp binop  expr expr   (* binary operation *)
    17   | BinOp binop  expr expr   (* binary operation *)
    18 	| LAcc vname		   (* local (incl. parameter) access *)
    18 	| LAcc vname               (* local (incl. parameter) access *)
    19 	| LAss vname expr          (* local assign *) ("_::=_"  [      90,90]90)
    19 	| LAss vname expr          (* local assign *) ("_::=_"   [      90,90]90)
    20 	| FAcc cname expr vname    (* field access *) ("{_}_.._"[10,90,99   ]90)
    20 	| FAcc cname expr vname    (* field access *) ("{_}_.._" [10,90,99   ]90)
    21 	| FAss cname expr vname 
    21 	| FAss cname expr vname 
    22 	                  expr     (* field ass. *)("{_}_.._:=_"[10,90,99,90]90)
    22                     expr     (* field ass. *) ("{_}_.._:=_" [10,90,99,90]90)
    23 	| Call expr mname (ty list) (expr list)(* method call*)
    23 	| Call expr mname 
    24                                     ("_.._'({_}_')" [90,99,10,10] 90)
    24     (ty list) (expr list)    (* method call*) ("_.._'({_}_')" [90,99,10,10] 90)
       
    25 
    25 and stmt
    26 and stmt
    26 	= Skip			   (* empty      statement *)
    27 	= Skip                     (* empty statement *)
    27 	| Expr expr		   (* expression statement *)
    28   | Expr expr                (* expression statement *)
    28 	| Comp stmt stmt	   ("_;; _"			[      61,60]60)
    29   | Comp stmt stmt       ("_;; _"             [61,60]60)
    29 	| Cond expr stmt stmt      ("If'(_') _ Else _"		[   80,79,79]70)
    30   | Cond expr stmt stmt  ("If '(_') _ Else _" [80,79,79]70)
    30 	| Loop expr stmt	   ("While'(_') _"		[      80,79]70)
    31   | Loop expr stmt       ("While '(_') _"     [80,79]70)
       
    32 
    31 end
    33 end