src/HOL/MicroJava/JVM/JVMListExample.thy
author kleing
Thu Feb 21 09:54:08 2002 +0100 (2002-02-21)
changeset 12911 704713ca07ea
parent 12559 7fb12775ce98
child 12951 a9fdcb71d252
permissions -rw-r--r--
new document
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@12911
     6
header {* \isaheader{Example for generating executable code from JVM semantics} *}
berghofe@12442
     7
berghofe@12442
     8
theory JVMListExample = JVMExec:
berghofe@12442
     9
berghofe@12442
    10
consts
berghofe@12442
    11
  list_name :: cname
berghofe@12442
    12
  test_name :: cname
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
berghofe@12442
    19
  val_name :: vname
berghofe@12442
    20
  "val_name == VName val_nam"
berghofe@12442
    21
berghofe@12442
    22
  next_name :: vname
berghofe@12442
    23
  "next_name == VName next_nam"
berghofe@12442
    24
kleing@12518
    25
  list_class :: "jvm_method class"
berghofe@12442
    26
  "list_class ==
berghofe@12442
    27
    (Object,
berghofe@12442
    28
     [(val_name, PrimT Integer), (next_name, RefT (ClassT list_name))],
berghofe@12442
    29
     [((append_name, [RefT (ClassT list_name)]), PrimT Integer,
berghofe@12442
    30
      (0, 0,
berghofe@12442
    31
       [Load 0,
berghofe@12442
    32
        Getfield next_name list_name,
berghofe@12442
    33
        Dup,
berghofe@12442
    34
        LitPush Null,
berghofe@12442
    35
        Ifcmpeq 4,
berghofe@12442
    36
        Load 1,
berghofe@12442
    37
        Invoke list_name append_name [RefT (ClassT list_name)],
berghofe@12442
    38
        Return,
berghofe@12442
    39
        Pop,
berghofe@12442
    40
        Load 0,
berghofe@12442
    41
        Load 1,
berghofe@12442
    42
        Putfield next_name list_name,
berghofe@12442
    43
        LitPush Unit,
kleing@12518
    44
        Return],[]))])"
berghofe@12442
    45
kleing@12518
    46
  test_class :: "jvm_method class"
berghofe@12442
    47
  "test_class ==
berghofe@12442
    48
    (Object, [],
berghofe@12442
    49
     [((makelist_name, []), PrimT Integer,
berghofe@12442
    50
      (0, 3,
berghofe@12442
    51
       [New list_name,
berghofe@12442
    52
        Dup,
berghofe@12442
    53
        Store 0,
berghofe@12442
    54
        LitPush (Intg 1),
berghofe@12442
    55
        Putfield val_name list_name,
berghofe@12442
    56
        New list_name,
berghofe@12442
    57
        Dup,
berghofe@12442
    58
        Store 1,
berghofe@12442
    59
        LitPush (Intg 2),
berghofe@12442
    60
        Putfield val_name list_name,
berghofe@12442
    61
        New list_name,
berghofe@12442
    62
        Dup,
berghofe@12442
    63
        Store 2,
berghofe@12442
    64
        LitPush (Intg 3),
berghofe@12442
    65
        Putfield val_name list_name,
berghofe@12442
    66
        Load 0,
berghofe@12442
    67
        Load 1,
berghofe@12442
    68
        Invoke list_name append_name [RefT (ClassT list_name)],
berghofe@12442
    69
        Load 0,
berghofe@12442
    70
        Load 2,
berghofe@12442
    71
        Invoke list_name append_name [RefT (ClassT list_name)],
berghofe@12442
    72
        LitPush Unit,
kleing@12518
    73
        Return],[]))])"
berghofe@12442
    74
berghofe@12442
    75
  example_prg :: jvm_prog
berghofe@12442
    76
  "example_prg == [ObjectC, (list_name, list_class), (test_name, test_class)]"
berghofe@12442
    77
berghofe@12442
    78
  start_state :: jvm_state
berghofe@12442
    79
  "start_state ==
berghofe@12442
    80
    (None, empty, [([], Unit # Unit # Unit # [], test_name, (makelist_name, []), 0)])"
berghofe@12442
    81
berghofe@12442
    82
types_code
berghofe@12442
    83
  cname ("string")
berghofe@12442
    84
  vnam ("string")
berghofe@12442
    85
  mname ("string")
kleing@12522
    86
  loc_ ("int")
berghofe@12442
    87
berghofe@12442
    88
consts_code
kleing@12522
    89
  "new_Addr" ("new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *}/ {* Loc *}")
berghofe@12442
    90
berghofe@12442
    91
  "wf" ("true?")
berghofe@12442
    92
berghofe@12442
    93
  "arbitrary" ("(raise ERROR)")
berghofe@12442
    94
  "arbitrary" :: "val" ("{* Unit *}")
berghofe@12442
    95
  "arbitrary" :: "cname" ("\"\"")
berghofe@12442
    96
berghofe@12442
    97
  "Object" ("\"Object\"")
berghofe@12442
    98
  "list_name" ("\"list\"")
berghofe@12442
    99
  "test_name" ("\"test\"")
berghofe@12442
   100
  "append_name" ("\"append\"")
berghofe@12442
   101
  "makelist_name" ("\"makelist\"")
berghofe@12442
   102
  "val_nam" ("\"val\"")
berghofe@12442
   103
  "next_nam" ("\"next\"")
berghofe@12442
   104
berghofe@12442
   105
ML {*
kleing@12522
   106
fun new_addr p none loc hp =
kleing@12522
   107
  let fun nr i = if p (hp (loc i)) then (loc i, none) else nr (i+1);
berghofe@12442
   108
  in nr 0 end;
berghofe@12442
   109
*}
berghofe@12442
   110
berghofe@12442
   111
subsection {* Single step execution *}
berghofe@12442
   112
berghofe@12442
   113
generate_code
berghofe@12442
   114
  test = "exec (example_prg, start_state)"
berghofe@12442
   115
berghofe@12442
   116
ML {* test *}
berghofe@12442
   117
ML {* exec (example_prg, the it) *}
berghofe@12442
   118
ML {* exec (example_prg, the it) *}
berghofe@12442
   119
ML {* exec (example_prg, the it) *}
berghofe@12442
   120
ML {* exec (example_prg, the it) *}
berghofe@12442
   121
ML {* exec (example_prg, the it) *}
berghofe@12442
   122
ML {* exec (example_prg, the it) *}
berghofe@12442
   123
ML {* exec (example_prg, the it) *}
berghofe@12442
   124
ML {* exec (example_prg, the it) *}
berghofe@12442
   125
ML {* exec (example_prg, the it) *}
berghofe@12442
   126
ML {* exec (example_prg, the it) *}
berghofe@12442
   127
ML {* exec (example_prg, the it) *}
berghofe@12442
   128
ML {* exec (example_prg, the it) *}
berghofe@12442
   129
ML {* exec (example_prg, the it) *}
berghofe@12442
   130
ML {* exec (example_prg, the it) *}
berghofe@12442
   131
ML {* exec (example_prg, the it) *}
berghofe@12442
   132
ML {* exec (example_prg, the it) *}
berghofe@12442
   133
ML {* exec (example_prg, the it) *}
berghofe@12442
   134
ML {* exec (example_prg, the it) *}
berghofe@12442
   135
ML {* exec (example_prg, the it) *}
berghofe@12442
   136
ML {* exec (example_prg, the it) *}
berghofe@12442
   137
ML {* exec (example_prg, the it) *}
berghofe@12442
   138
ML {* exec (example_prg, the it) *}
berghofe@12442
   139
ML {* exec (example_prg, the it) *}
berghofe@12442
   140
ML {* exec (example_prg, the it) *}
berghofe@12442
   141
ML {* exec (example_prg, the it) *}
berghofe@12442
   142
ML {* exec (example_prg, the it) *}
berghofe@12442
   143
ML {* exec (example_prg, the it) *}
berghofe@12442
   144
ML {* exec (example_prg, the it) *}
berghofe@12442
   145
ML {* exec (example_prg, the it) *}
berghofe@12442
   146
ML {* exec (example_prg, the it) *}
berghofe@12442
   147
ML {* exec (example_prg, the it) *}
berghofe@12442
   148
ML {* exec (example_prg, the it) *}
berghofe@12442
   149
ML {* exec (example_prg, the it) *}
berghofe@12442
   150
ML {* exec (example_prg, the it) *}
berghofe@12442
   151
ML {* exec (example_prg, the it) *}
berghofe@12442
   152
ML {* exec (example_prg, the it) *}
berghofe@12442
   153
ML {* exec (example_prg, the it) *}
berghofe@12442
   154
ML {* exec (example_prg, the it) *}
berghofe@12442
   155
ML {* exec (example_prg, the it) *}
berghofe@12442
   156
ML {* exec (example_prg, the it) *}
berghofe@12442
   157
ML {* exec (example_prg, the it) *}
berghofe@12442
   158
ML {* exec (example_prg, the it) *}
berghofe@12442
   159
ML {* exec (example_prg, the it) *}
berghofe@12442
   160
ML {* exec (example_prg, the it) *}
berghofe@12442
   161
ML {* exec (example_prg, the it) *}
berghofe@12442
   162
ML {* exec (example_prg, the it) *}
berghofe@12442
   163
ML {* exec (example_prg, the it) *}
berghofe@12442
   164
ML {* exec (example_prg, the it) *}
berghofe@12442
   165
ML {* exec (example_prg, the it) *}
berghofe@12442
   166
ML {* exec (example_prg, the it) *}
berghofe@12442
   167
ML {* exec (example_prg, the it) *}
berghofe@12442
   168
ML {* exec (example_prg, the it) *}
berghofe@12442
   169
ML {* exec (example_prg, the it) *}
berghofe@12442
   170
kleing@12522
   171
end