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