src/HOL/MicroJava/JVM/JVMListExample.thy
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 24783 5a3e336a2e37
child 28408 e26aac53723d
permissions -rw-r--r--
Name.uu, Name.aT;
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
wenzelm@24340
     8
theory JVMListExample imports "../J/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")
wenzelm@24783
    94
  loc' ("int")
berghofe@12442
    95
berghofe@12442
    96
consts_code
berghofe@16770
    97
  "new_Addr" ("\<module>new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *}/ {* Loc *}")
berghofe@16770
    98
attach {*
berghofe@16770
    99
fun new_addr p none loc hp =
berghofe@16770
   100
  let fun nr i = if p (hp (loc i)) then (loc i, none) else nr (i+1);
berghofe@16770
   101
  in nr 0 end;
berghofe@16770
   102
*}
berghofe@12442
   103
wenzelm@18679
   104
  "arbitrary" ("(raise Match)")
haftmann@22921
   105
  "arbitrary :: val" ("{* Unit *}")
haftmann@22921
   106
  "arbitrary :: cname" ("{* Object *}")
berghofe@12442
   107
kleing@12951
   108
  "list_nam" ("\"list\"")
kleing@12951
   109
  "test_nam" ("\"test\"")
berghofe@12442
   110
  "append_name" ("\"append\"")
berghofe@12442
   111
  "makelist_name" ("\"makelist\"")
berghofe@12442
   112
  "val_nam" ("\"val\"")
berghofe@12442
   113
  "next_nam" ("\"next\"")
berghofe@12442
   114
haftmann@20971
   115
definition
haftmann@20971
   116
  "test = exec (E, start_state E test_name makelist_name)"
haftmann@20971
   117
haftmann@20971
   118
berghofe@12442
   119
subsection {* Single step execution *}
berghofe@12442
   120
berghofe@17145
   121
code_module JVM
berghofe@17145
   122
contains
haftmann@24225
   123
  exec = exec
haftmann@24225
   124
  test = test
berghofe@12442
   125
wenzelm@24074
   126
ML {*
wenzelm@24074
   127
JVM.test;
wenzelm@24074
   128
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   129
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   130
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   131
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   132
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   133
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   134
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   135
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   136
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   137
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   138
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   139
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   140
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   141
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   142
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   143
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   144
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   145
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   146
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   147
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   148
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   149
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   150
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   151
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   152
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   153
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   154
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   155
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   156
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   157
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   158
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   159
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   160
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   161
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   162
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   163
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   164
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   165
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   166
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   167
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   168
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   169
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   170
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   171
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   172
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   173
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   174
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   175
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   176
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   177
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   178
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   179
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   180
JVM.exec (JVM.E, JVM.the it);
wenzelm@24074
   181
*}
berghofe@12442
   182
kleing@12973
   183
end