src/HOL/MicroJava/J/Term.thy

more transfer rules

(*  Title:      HOL/MicroJava/J/Term.thy
    Author:     David von Oheimb, Technische Universitaet Muenchen
*)

section {* Expressions and Statements *}

theory Term imports Value begin

datatype binop = Eq | Add    -- "function codes for binary operation"

datatype expr
  = NewC cname               -- "class instance creation"
  | Cast cname expr          -- "type cast"
  | Lit val                  -- "literal value, also references"
  | BinOp binop expr expr    -- "binary operation"
  | LAcc vname               -- "local (incl. parameter) access"
  | LAss vname expr          ("_::=_" [90,90]90)      -- "local assign"
  | FAcc cname expr vname    ("{_}_.._" [10,90,99]90) -- "field access"
  | FAss cname expr vname 
                    expr     ("{_}_.._:=_" [10,90,99,90]90) -- "field ass."
  | Call cname expr mname 
    "ty list" "expr list"    ("{_}_.._'( {_}_')" [10,90,99,10,10] 90) -- "method call"

datatype_compat expr

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

end