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