src/HOL/MicroJava/J/Term.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 41589 bbd861837ebc
child 58249 180f1b3508ed
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/MicroJava/J/Term.thy
41589
bbd861837ebc tuned headers;
wenzelm
parents: 16417
diff changeset
     2
    Author:     David von Oheimb, Technische Universitaet Muenchen
11070
cc421547e744 improved document (added headers etc)
oheimb
parents: 11026
diff changeset
     3
*)
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     4
12911
704713ca07ea new document
kleing
parents: 12517
diff changeset
     5
header {* \isaheader{Expressions and Statements} *}
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     6
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 12911
diff changeset
     7
theory Term imports Value begin
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     8
12517
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11070
diff changeset
     9
datatype binop = Eq | Add    -- "function codes for binary operation"
9240
f4d76cb26433 added BinOp
oheimb
parents: 8011
diff changeset
    10
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    11
datatype expr
12517
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11070
diff changeset
    12
  = NewC cname               -- "class instance creation"
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11070
diff changeset
    13
  | Cast cname expr          -- "type cast"
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11070
diff changeset
    14
  | Lit val                  -- "literal value, also references"
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11070
diff changeset
    15
  | BinOp binop expr expr    -- "binary operation"
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11070
diff changeset
    16
  | LAcc vname               -- "local (incl. parameter) access"
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11070
diff changeset
    17
  | LAss vname expr          ("_::=_" [90,90]90)      -- "local assign"
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11070
diff changeset
    18
  | FAcc cname expr vname    ("{_}_.._" [10,90,99]90) -- "field access"
10069
c7226e6f9625 untabified for HTML
kleing
parents: 10061
diff changeset
    19
  | FAss cname expr vname 
12517
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11070
diff changeset
    20
                    expr     ("{_}_.._:=_" [10,90,99,90]90) -- "field ass."
10763
08e1610c1dcb added type annotation to Call
oheimb
parents: 10119
diff changeset
    21
  | Call cname expr mname 
12517
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11070
diff changeset
    22
    "ty list" "expr list"    ("{_}_.._'( {_}_')" [10,90,99,10,10] 90) -- "method call" 
10061
fe82134773dc added HTML syntax; added spaces in normal syntax for better documents
kleing
parents: 10042
diff changeset
    23
10119
20c9590bb5f5 separated expr and stmt
nipkow
parents: 10069
diff changeset
    24
datatype stmt
12517
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11070
diff changeset
    25
  = Skip                     -- "empty statement"
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11070
diff changeset
    26
  | Expr expr                -- "expression statement"
10061
fe82134773dc added HTML syntax; added spaces in normal syntax for better documents
kleing
parents: 10042
diff changeset
    27
  | Comp stmt stmt       ("_;; _"             [61,60]60)
fe82134773dc added HTML syntax; added spaces in normal syntax for better documents
kleing
parents: 10042
diff changeset
    28
  | Cond expr stmt stmt  ("If '(_') _ Else _" [80,79,79]70)
fe82134773dc added HTML syntax; added spaces in normal syntax for better documents
kleing
parents: 10042
diff changeset
    29
  | Loop expr stmt       ("While '(_') _"     [80,79]70)
fe82134773dc added HTML syntax; added spaces in normal syntax for better documents
kleing
parents: 10042
diff changeset
    30
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    31
end
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10763
diff changeset
    32