src/HOL/MicroJava/J/Term.thy
changeset 10069 c7226e6f9625
parent 10061 fe82134773dc
child 10119 20c9590bb5f5
equal deleted inserted replaced
10068:46db6fde4ee3 10069:c7226e6f9625
     6 Java expressions and statements
     6 Java expressions and statements
     7 *)
     7 *)
     8 
     8 
     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 
    23   | Call expr mname 
    24     (ty list) (expr list)    (* method call*) ("_.._'({_}_')" [90,99,10,10] 90)
    24     (ty list) (expr list)    (* method call*) ("_.._'({_}_')" [90,99,10,10] 90)
    25 
    25 
    26 and stmt
    26 and stmt
    27 	= Skip                     (* empty statement *)
    27   = Skip                     (* empty statement *)
    28   | Expr expr                (* expression statement *)
    28   | Expr expr                (* expression statement *)
    29   | Comp stmt stmt       ("_;; _"             [61,60]60)
    29   | Comp stmt stmt       ("_;; _"             [61,60]60)
    30   | Cond expr stmt stmt  ("If '(_') _ Else _" [80,79,79]70)
    30   | Cond expr stmt stmt  ("If '(_') _ Else _" [80,79,79]70)
    31   | Loop expr stmt       ("While '(_') _"     [80,79]70)
    31   | Loop expr stmt       ("While '(_') _"     [80,79]70)
    32 
    32