src/HOL/NanoJava/Term.thy
changeset 11497 0e66e0114d9a
parent 11486 8f32860eac3a
child 11499 7a7bb59a05db
equal deleted inserted replaced
11496:fa8d12b789e1 11497:0e66e0114d9a
    12 typedecl vnam   (* variable or field name *)
    12 typedecl vnam   (* variable or field name *)
    13 typedecl mname  (* method name *)
    13 typedecl mname  (* method name *)
    14 arities  cname :: "term"
    14 arities  cname :: "term"
    15          vnam  :: "term"
    15          vnam  :: "term"
    16          mname :: "term"
    16          mname :: "term"
       
    17 types   imname = "cname \<times> mname"
    17 
    18 
    18 datatype vname  (* variable for special names *)
    19 datatype vname  (* variable for special names *)
    19   = This        (* This pointer *)
    20   = This        (* This pointer *)
    20   | Param       (* method parameter *)
    21   | Param       (* method parameter *)
    21   | Res         (* method result *)
    22   | Res         (* method result *)
    27   | Cond expr  stmt stmt   ("If '(_') _ Else _" [99,91,91] 91)
    28   | Cond expr  stmt stmt   ("If '(_') _ Else _" [99,91,91] 91)
    28   | Loop vname stmt        ("While '(_') _"     [99,91   ] 91)
    29   | Loop vname stmt        ("While '(_') _"     [99,91   ] 91)
    29   | LAss vname expr        ("_ :== _"           [99,   95] 94) (* local ass. *)
    30   | LAss vname expr        ("_ :== _"           [99,   95] 94) (* local ass. *)
    30   | FAss expr  vnam expr   ("_.._:==_"          [95,99,95] 94) (* field ass. *)
    31   | FAss expr  vnam expr   ("_.._:==_"          [95,99,95] 94) (* field ass. *)
    31   | Meth cname mname       (* virtual method *)
    32   | Meth cname mname       (* virtual method *)
    32   | Impl cname mname       (* method implementation *)
    33   | Impl      imname       (* method implementation *)
    33 and expr
    34 and expr
    34   = NewC cname       ("new _"        [   99] 95) (* object creation  *)
    35   = NewC cname       ("new _"        [   99] 95) (* object creation  *)
    35   | Cast cname expr                              (* type cast        *)
    36   | Cast cname expr                              (* type cast        *)
    36   | LAcc vname                                   (* local access     *)
    37   | LAcc vname                                   (* local access     *)
    37   | FAcc expr  vnam  ("_.._"         [95,99] 95) (* field access     *)
    38   | FAcc expr  vnam  ("_.._"         [95,99] 95) (* field access     *)