src/HOL/MicroJava/J/Term.thy
changeset 12517 360e3215f029
parent 11070 cc421547e744
child 12911 704713ca07ea
equal deleted inserted replaced
12516:d09d0f160888 12517:360e3215f029
     6 
     6 
     7 header "Expressions and Statements"
     7 header "Expressions and Statements"
     8 
     8 
     9 theory Term = Value:
     9 theory 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          ("_::=_" [90,90]90)      -- "local assign"
    20   | FAcc cname expr vname    (* field access *) ("{_}_.._" [10,90,99   ]90)
    20   | FAcc cname expr vname    ("{_}_.._" [10,90,99]90) -- "field access"
    21   | FAss cname expr vname 
    21   | FAss cname expr vname 
    22                     expr     (* field ass. *) ("{_}_.._:=_" [10,90,99,90]90)
    22                     expr     ("{_}_.._:=_" [10,90,99,90]90) -- "field ass."
    23   | Call cname expr mname 
    23   | Call cname expr mname 
    24     "ty list" "expr list"    (* method call*) ("{_}_.._'( {_}_')"
    24     "ty list" "expr list"    ("{_}_.._'( {_}_')" [10,90,99,10,10] 90) -- "method call" 
    25                                                             [10,90,99,10,10] 90)
       
    26 
    25 
    27 datatype stmt
    26 datatype stmt
    28   = Skip                     (* empty statement *)
    27   = Skip                     -- "empty statement"
    29   | Expr expr                (* expression statement *)
    28   | Expr expr                -- "expression statement"
    30   | Comp stmt stmt       ("_;; _"             [61,60]60)
    29   | Comp stmt stmt       ("_;; _"             [61,60]60)
    31   | Cond expr stmt stmt  ("If '(_') _ Else _" [80,79,79]70)
    30   | Cond expr stmt stmt  ("If '(_') _ Else _" [80,79,79]70)
    32   | Loop expr stmt       ("While '(_') _"     [80,79]70)
    31   | Loop expr stmt       ("While '(_') _"     [80,79]70)
    33 
    32 
    34 end
    33 end