src/HOL/MicroJava/J/Term.thy
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 16417 9bc16273c2d4
child 41589 bbd861837ebc
permissions -rw-r--r--
Name.uu, Name.aT;
     1 (*  Title:      HOL/MicroJava/J/Term.thy
     2     ID:         $Id$
     3     Author:     David von Oheimb
     4     Copyright   1999 Technische Universitaet Muenchen
     5 *)
     6 
     7 header {* \isaheader{Expressions and Statements} *}
     8 
     9 theory Term imports Value begin
    10 
    11 datatype binop = Eq | Add    -- "function codes for binary operation"
    12 
    13 datatype expr
    14   = NewC cname               -- "class instance creation"
    15   | Cast cname expr          -- "type cast"
    16   | Lit val                  -- "literal value, also references"
    17   | BinOp binop expr expr    -- "binary operation"
    18   | LAcc vname               -- "local (incl. parameter) access"
    19   | LAss vname expr          ("_::=_" [90,90]90)      -- "local assign"
    20   | FAcc cname expr vname    ("{_}_.._" [10,90,99]90) -- "field access"
    21   | FAss cname expr vname 
    22                     expr     ("{_}_.._:=_" [10,90,99,90]90) -- "field ass."
    23   | Call cname expr mname 
    24     "ty list" "expr list"    ("{_}_.._'( {_}_')" [10,90,99,10,10] 90) -- "method call" 
    25 
    26 datatype stmt
    27   = Skip                     -- "empty statement"
    28   | Expr expr                -- "expression statement"
    29   | Comp stmt stmt       ("_;; _"             [61,60]60)
    30   | Cond expr stmt stmt  ("If '(_') _ Else _" [80,79,79]70)
    31   | Loop expr stmt       ("While '(_') _"     [80,79]70)
    32 
    33 end
    34