src/HOL/MicroJava/JVM/JVMListExample.thy
author berghofe
Mon Dec 10 15:24:48 2001 +0100 (2001-12-10)
changeset 12442 0ecba8660de7
child 12518 521f2da133be
permissions -rw-r--r--
Example for code generator.
     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 :: "(nat * nat * bytecode) 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 :: "(nat * nat * bytecode) 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 *}")
    90   "cast_ok" ("true????")
    91 
    92   "wf" ("true?")
    93 
    94   "arbitrary" ("(raise ERROR)")
    95   "arbitrary" :: "val" ("{* Unit *}")
    96   "arbitrary" :: "cname" ("\"\"")
    97 
    98   "Object" ("\"Object\"")
    99   "list_name" ("\"list\"")
   100   "test_name" ("\"test\"")
   101   "append_name" ("\"append\"")
   102   "makelist_name" ("\"makelist\"")
   103   "val_nam" ("\"val\"")
   104   "next_nam" ("\"next\"")
   105 
   106 ML {*
   107 fun new_addr p none hp =
   108   let fun nr i = if p (hp i) then (i, none) else nr (i+1);
   109   in nr 0 end;
   110 *}
   111 
   112 subsection {* Single step execution *}
   113 
   114 generate_code
   115   test = "exec (example_prg, start_state)"
   116 
   117 ML {* test *}
   118 ML {* exec (example_prg, the it) *}
   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 
   172 end
   173