src/HOL/MicroJava/JVM/JVMListExample.thy
author haftmann
Fri Jun 17 16:12:49 2005 +0200 (2005-06-17)
changeset 16417 9bc16273c2d4
parent 13101 90b31354fe15
child 16644 701218c1301c
permissions -rw-r--r--
migrated theory headers to new format
berghofe@12442
     1
(*  Title:      HOL/MicroJava/JVM/JVMListExample.thy
berghofe@12442
     2
    ID:         $Id$
berghofe@12442
     3
    Author:     Stefan Berghofer
berghofe@12442
     4
*)
berghofe@12442
     5
kleing@12973
     6
header {* \isaheader{Example for generating executable code from JVM semantics}\label{sec:JVMListExample} *}
berghofe@12442
     7
haftmann@16417
     8
theory JVMListExample imports SystemClasses JVMExec begin
berghofe@12442
     9
berghofe@12442
    10
consts
kleing@12951
    11
  list_nam :: cnam
kleing@12951
    12
  test_nam :: cnam
berghofe@12442
    13
  append_name :: mname
berghofe@12442
    14
  makelist_name :: mname
berghofe@12442
    15
  val_nam :: vnam
berghofe@12442
    16
  next_nam :: vnam
berghofe@12442
    17
berghofe@12442
    18
constdefs
kleing@12951
    19
  list_name :: cname
kleing@12951
    20
  "list_name == Cname list_nam"
kleing@12951
    21
  
kleing@12951
    22
  test_name :: cname
kleing@12951
    23
  "test_name == Cname test_nam"
kleing@12951
    24
berghofe@12442
    25
  val_name :: vname
berghofe@12442
    26
  "val_name == VName val_nam"
berghofe@12442
    27
berghofe@12442
    28
  next_name :: vname
berghofe@12442
    29
  "next_name == VName next_nam"
berghofe@12442
    30
kleing@12951
    31
  append_ins :: bytecode
kleing@12951
    32
  "append_ins == 
berghofe@12442
    33
       [Load 0,
berghofe@12442
    34
        Getfield next_name list_name,
berghofe@12442
    35
        Dup,
berghofe@12442
    36
        LitPush Null,
berghofe@12442
    37
        Ifcmpeq 4,
kleing@12951
    38
        Load 1,       
kleing@12951
    39
        Invoke list_name append_name [Class list_name],
berghofe@12442
    40
        Return,
berghofe@12442
    41
        Pop,
berghofe@12442
    42
        Load 0,
berghofe@12442
    43
        Load 1,
berghofe@12442
    44
        Putfield next_name list_name,
berghofe@12442
    45
        LitPush Unit,
kleing@12951
    46
        Return]"
berghofe@12442
    47
kleing@12951
    48
  list_class :: "jvm_method class"
kleing@12951
    49
  "list_class ==
kleing@12951
    50
    (Object,
kleing@12951
    51
     [(val_name, PrimT Integer), (next_name, Class list_name)],
kleing@12951
    52
     [((append_name, [Class list_name]), PrimT Void,
kleing@12951
    53
        (3, 0, append_ins,[(1,2,8,Xcpt NullPointer)]))])"
kleing@12951
    54
kleing@12951
    55
  make_list_ins :: bytecode
kleing@12951
    56
  "make_list_ins ==
berghofe@12442
    57
       [New list_name,
berghofe@12442
    58
        Dup,
berghofe@12442
    59
        Store 0,
berghofe@12442
    60
        LitPush (Intg 1),
berghofe@12442
    61
        Putfield val_name list_name,
berghofe@12442
    62
        New list_name,
berghofe@12442
    63
        Dup,
berghofe@12442
    64
        Store 1,
berghofe@12442
    65
        LitPush (Intg 2),
berghofe@12442
    66
        Putfield val_name list_name,
berghofe@12442
    67
        New list_name,
berghofe@12442
    68
        Dup,
berghofe@12442
    69
        Store 2,
berghofe@12442
    70
        LitPush (Intg 3),
berghofe@12442
    71
        Putfield val_name list_name,
berghofe@12442
    72
        Load 0,
berghofe@12442
    73
        Load 1,
kleing@12951
    74
        Invoke list_name append_name [Class list_name],
kleing@13101
    75
        Pop,
berghofe@12442
    76
        Load 0,
berghofe@12442
    77
        Load 2,
kleing@12951
    78
        Invoke list_name append_name [Class list_name],
kleing@12951
    79
        Return]"
kleing@12951
    80
kleing@12951
    81
  test_class :: "jvm_method class"
kleing@12951
    82
  "test_class ==
kleing@12951
    83
    (Object, [],
kleing@12951
    84
     [((makelist_name, []), PrimT Void, (3, 2, make_list_ins,[]))])"
berghofe@12442
    85
kleing@12951
    86
  E :: jvm_prog
kleing@12951
    87
  "E == SystemClasses @ [(list_name, list_class), (test_name, test_class)]"
kleing@12951
    88
berghofe@12442
    89
berghofe@12442
    90
types_code
kleing@12951
    91
  cnam ("string")
berghofe@12442
    92
  vnam ("string")
berghofe@12442
    93
  mname ("string")
kleing@12522
    94
  loc_ ("int")
berghofe@12442
    95
berghofe@12442
    96
consts_code
kleing@12522
    97
  "new_Addr" ("new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *}/ {* Loc *}")
berghofe@12442
    98
berghofe@12442
    99
  "arbitrary" ("(raise ERROR)")
berghofe@12442
   100
  "arbitrary" :: "val" ("{* Unit *}")
kleing@12951
   101
  "arbitrary" :: "cname" ("Object")
berghofe@12442
   102
kleing@12951
   103
  "list_nam" ("\"list\"")
kleing@12951
   104
  "test_nam" ("\"test\"")
berghofe@12442
   105
  "append_name" ("\"append\"")
berghofe@12442
   106
  "makelist_name" ("\"makelist\"")
berghofe@12442
   107
  "val_nam" ("\"val\"")
berghofe@12442
   108
  "next_nam" ("\"next\"")
berghofe@12442
   109
berghofe@12442
   110
ML {*
kleing@12522
   111
fun new_addr p none loc hp =
kleing@12522
   112
  let fun nr i = if p (hp (loc i)) then (loc i, none) else nr (i+1);
berghofe@12442
   113
  in nr 0 end;
berghofe@12442
   114
*}
berghofe@12442
   115
berghofe@12442
   116
subsection {* Single step execution *}
berghofe@12442
   117
kleing@12951
   118
generate_code 
kleing@13052
   119
  test = "exec (E, start_state E test_name makelist_name)"
berghofe@12442
   120
berghofe@12442
   121
ML {* test *}
kleing@12951
   122
ML {* exec (E, the it) *}
kleing@12951
   123
ML {* exec (E, the it) *}
kleing@12951
   124
ML {* exec (E, the it) *}
kleing@12951
   125
ML {* exec (E, the it) *}
kleing@12951
   126
ML {* exec (E, the it) *}
kleing@12951
   127
ML {* exec (E, the it) *}
kleing@12951
   128
ML {* exec (E, the it) *}
kleing@12951
   129
ML {* exec (E, the it) *}
kleing@12951
   130
ML {* exec (E, the it) *}
kleing@12951
   131
ML {* exec (E, the it) *}
kleing@12951
   132
ML {* exec (E, the it) *}
kleing@12951
   133
ML {* exec (E, the it) *}
kleing@12951
   134
ML {* exec (E, the it) *}
kleing@12951
   135
ML {* exec (E, the it) *}
kleing@12951
   136
ML {* exec (E, the it) *}
kleing@12951
   137
ML {* exec (E, the it) *}
kleing@12951
   138
ML {* exec (E, the it) *}
kleing@12951
   139
ML {* exec (E, the it) *}
kleing@12951
   140
ML {* exec (E, the it) *}
kleing@12951
   141
ML {* exec (E, the it) *}
kleing@12951
   142
ML {* exec (E, the it) *}
kleing@12951
   143
ML {* exec (E, the it) *}
kleing@12951
   144
ML {* exec (E, the it) *}
kleing@12951
   145
ML {* exec (E, the it) *}
kleing@12951
   146
ML {* exec (E, the it) *}
kleing@12951
   147
ML {* exec (E, the it) *}
kleing@12951
   148
ML {* exec (E, the it) *}
kleing@12951
   149
ML {* exec (E, the it) *}
kleing@12951
   150
ML {* exec (E, the it) *}
kleing@12951
   151
ML {* exec (E, the it) *}
kleing@12951
   152
ML {* exec (E, the it) *}
kleing@12951
   153
ML {* exec (E, the it) *}
kleing@12951
   154
ML {* exec (E, the it) *}
kleing@12951
   155
ML {* exec (E, the it) *}
kleing@12951
   156
ML {* exec (E, the it) *}
kleing@12951
   157
ML {* exec (E, the it) *}
kleing@12951
   158
ML {* exec (E, the it) *}
kleing@12951
   159
ML {* exec (E, the it) *}
kleing@12951
   160
ML {* exec (E, the it) *}
kleing@12951
   161
ML {* exec (E, the it) *}
kleing@12951
   162
ML {* exec (E, the it) *}
kleing@12951
   163
ML {* exec (E, the it) *}
kleing@12951
   164
ML {* exec (E, the it) *}
kleing@12951
   165
ML {* exec (E, the it) *}
kleing@12951
   166
ML {* exec (E, the it) *}
kleing@12951
   167
ML {* exec (E, the it) *}
kleing@12951
   168
ML {* exec (E, the it) *}
kleing@12951
   169
ML {* exec (E, the it) *}
kleing@12951
   170
ML {* exec (E, the it) *}
kleing@12951
   171
ML {* exec (E, the it) *}
kleing@12951
   172
ML {* exec (E, the it) *}
kleing@12951
   173
ML {* exec (E, the it) *}
kleing@12951
   174
ML {* exec (E, the it) *}
berghofe@12442
   175
kleing@12973
   176
end