src/HOL/MicroJava/J/Term.thy
author wenzelm
Thu, 01 Sep 2016 16:05:22 +0200
changeset 63750 9c8a366778e1
parent 62042 6c6ccf573479
child 67443 3abf6a722518
permissions -rw-r--r--
more robust persistent storage; 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
61361
8b5f00202e1a isabelle update_cartouches;
wenzelm
parents: 58886
diff changeset
     5
section \<open>Expressions and Statements\<close>
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
62042
6c6ccf573479 isabelle update_cartouches -c -t;
wenzelm
parents: 61361
diff changeset
     9
datatype binop = Eq | Add    \<comment> "function codes for binary operation"
9240
f4d76cb26433 added BinOp
oheimb
parents: 8011
diff changeset
    10
58310
91ea607a34d8 updated news
blanchet
parents: 58263
diff changeset
    11
datatype expr
62042
6c6ccf573479 isabelle update_cartouches -c -t;
wenzelm
parents: 61361
diff changeset
    12
  = NewC cname               \<comment> "class instance creation"
6c6ccf573479 isabelle update_cartouches -c -t;
wenzelm
parents: 61361
diff changeset
    13
  | Cast cname expr          \<comment> "type cast"
6c6ccf573479 isabelle update_cartouches -c -t;
wenzelm
parents: 61361
diff changeset
    14
  | Lit val                  \<comment> "literal value, also references"
6c6ccf573479 isabelle update_cartouches -c -t;
wenzelm
parents: 61361
diff changeset
    15
  | BinOp binop expr expr    \<comment> "binary operation"
6c6ccf573479 isabelle update_cartouches -c -t;
wenzelm
parents: 61361
diff changeset
    16
  | LAcc vname               \<comment> "local (incl. parameter) access"
6c6ccf573479 isabelle update_cartouches -c -t;
wenzelm
parents: 61361
diff changeset
    17
  | LAss vname expr          ("_::=_" [90,90]90)      \<comment> "local assign"
6c6ccf573479 isabelle update_cartouches -c -t;
wenzelm
parents: 61361
diff changeset
    18
  | FAcc cname expr vname    ("{_}_.._" [10,90,99]90) \<comment> "field access"
10069
c7226e6f9625 untabified for HTML
kleing
parents: 10061
diff changeset
    19
  | FAss cname expr vname 
62042
6c6ccf573479 isabelle update_cartouches -c -t;
wenzelm
parents: 61361
diff changeset
    20
                    expr     ("{_}_.._:=_" [10,90,99,90]90) \<comment> "field ass."
10763
08e1610c1dcb added type annotation to Call
oheimb
parents: 10119
diff changeset
    21
  | Call cname expr mname 
62042
6c6ccf573479 isabelle update_cartouches -c -t;
wenzelm
parents: 61361
diff changeset
    22
    "ty list" "expr list"    ("{_}_.._'( {_}_')" [10,90,99,10,10] 90) \<comment> "method call"
58263
6c907aad90ba ported MicroJava to new datatypes
blanchet
parents: 58249
diff changeset
    23
6c907aad90ba ported MicroJava to new datatypes
blanchet
parents: 58249
diff changeset
    24
datatype_compat expr
10061
fe82134773dc added HTML syntax; added spaces in normal syntax for better documents
kleing
parents: 10042
diff changeset
    25
58310
91ea607a34d8 updated news
blanchet
parents: 58263
diff changeset
    26
datatype stmt
62042
6c6ccf573479 isabelle update_cartouches -c -t;
wenzelm
parents: 61361
diff changeset
    27
  = Skip                     \<comment> "empty statement"
6c6ccf573479 isabelle update_cartouches -c -t;
wenzelm
parents: 61361
diff changeset
    28
  | Expr expr                \<comment> "expression statement"
10061
fe82134773dc added HTML syntax; added spaces in normal syntax for better documents
kleing
parents: 10042
diff changeset
    29
  | Comp stmt stmt       ("_;; _"             [61,60]60)
fe82134773dc added HTML syntax; added spaces in normal syntax for better documents
kleing
parents: 10042
diff changeset
    30
  | 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
    31
  | Loop expr stmt       ("While '(_') _"     [80,79]70)
fe82134773dc added HTML syntax; added spaces in normal syntax for better documents
kleing
parents: 10042
diff changeset
    32
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    33
end
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10763
diff changeset
    34