src/HOL/MicroJava/JVM/JVMListExample.thy
changeset 12442 0ecba8660de7
child 12518 521f2da133be
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Mon Dec 10 15:24:48 2001 +0100
     1.3 @@ -0,0 +1,173 @@
     1.4 +(*  Title:      HOL/MicroJava/JVM/JVMListExample.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Stefan Berghofer
     1.7 +*)
     1.8 +
     1.9 +header {* Example for generating executable code from JVM semantics *}
    1.10 +
    1.11 +theory JVMListExample = JVMExec:
    1.12 +
    1.13 +consts
    1.14 +  list_name :: cname
    1.15 +  test_name :: cname
    1.16 +  append_name :: mname
    1.17 +  makelist_name :: mname
    1.18 +  val_nam :: vnam
    1.19 +  next_nam :: vnam
    1.20 +
    1.21 +constdefs
    1.22 +  val_name :: vname
    1.23 +  "val_name == VName val_nam"
    1.24 +
    1.25 +  next_name :: vname
    1.26 +  "next_name == VName next_nam"
    1.27 +
    1.28 +  list_class :: "(nat * nat * bytecode) class"
    1.29 +  "list_class ==
    1.30 +    (Object,
    1.31 +     [(val_name, PrimT Integer), (next_name, RefT (ClassT list_name))],
    1.32 +     [((append_name, [RefT (ClassT list_name)]), PrimT Integer,
    1.33 +      (0, 0,
    1.34 +       [Load 0,
    1.35 +        Getfield next_name list_name,
    1.36 +        Dup,
    1.37 +        LitPush Null,
    1.38 +        Ifcmpeq 4,
    1.39 +        Load 1,
    1.40 +        Invoke list_name append_name [RefT (ClassT list_name)],
    1.41 +        Return,
    1.42 +        Pop,
    1.43 +        Load 0,
    1.44 +        Load 1,
    1.45 +        Putfield next_name list_name,
    1.46 +        LitPush Unit,
    1.47 +        Return]))])"
    1.48 +
    1.49 +  test_class :: "(nat * nat * bytecode) class"
    1.50 +  "test_class ==
    1.51 +    (Object, [],
    1.52 +     [((makelist_name, []), PrimT Integer,
    1.53 +      (0, 3,
    1.54 +       [New list_name,
    1.55 +        Dup,
    1.56 +        Store 0,
    1.57 +        LitPush (Intg 1),
    1.58 +        Putfield val_name list_name,
    1.59 +        New list_name,
    1.60 +        Dup,
    1.61 +        Store 1,
    1.62 +        LitPush (Intg 2),
    1.63 +        Putfield val_name list_name,
    1.64 +        New list_name,
    1.65 +        Dup,
    1.66 +        Store 2,
    1.67 +        LitPush (Intg 3),
    1.68 +        Putfield val_name list_name,
    1.69 +        Load 0,
    1.70 +        Load 1,
    1.71 +        Invoke list_name append_name [RefT (ClassT list_name)],
    1.72 +        Load 0,
    1.73 +        Load 2,
    1.74 +        Invoke list_name append_name [RefT (ClassT list_name)],
    1.75 +        LitPush Unit,
    1.76 +        Return]))])"
    1.77 +
    1.78 +  example_prg :: jvm_prog
    1.79 +  "example_prg == [ObjectC, (list_name, list_class), (test_name, test_class)]"
    1.80 +
    1.81 +  start_state :: jvm_state
    1.82 +  "start_state ==
    1.83 +    (None, empty, [([], Unit # Unit # Unit # [], test_name, (makelist_name, []), 0)])"
    1.84 +
    1.85 +types_code
    1.86 +  cname ("string")
    1.87 +  vnam ("string")
    1.88 +  mname ("string")
    1.89 +  loc ("int")
    1.90 +
    1.91 +consts_code
    1.92 +  "new_Addr" ("new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *}")
    1.93 +  "cast_ok" ("true????")
    1.94 +
    1.95 +  "wf" ("true?")
    1.96 +
    1.97 +  "arbitrary" ("(raise ERROR)")
    1.98 +  "arbitrary" :: "val" ("{* Unit *}")
    1.99 +  "arbitrary" :: "cname" ("\"\"")
   1.100 +
   1.101 +  "Object" ("\"Object\"")
   1.102 +  "list_name" ("\"list\"")
   1.103 +  "test_name" ("\"test\"")
   1.104 +  "append_name" ("\"append\"")
   1.105 +  "makelist_name" ("\"makelist\"")
   1.106 +  "val_nam" ("\"val\"")
   1.107 +  "next_nam" ("\"next\"")
   1.108 +
   1.109 +ML {*
   1.110 +fun new_addr p none hp =
   1.111 +  let fun nr i = if p (hp i) then (i, none) else nr (i+1);
   1.112 +  in nr 0 end;
   1.113 +*}
   1.114 +
   1.115 +subsection {* Single step execution *}
   1.116 +
   1.117 +generate_code
   1.118 +  test = "exec (example_prg, start_state)"
   1.119 +
   1.120 +ML {* test *}
   1.121 +ML {* exec (example_prg, the it) *}
   1.122 +ML {* exec (example_prg, the it) *}
   1.123 +ML {* exec (example_prg, the it) *}
   1.124 +ML {* exec (example_prg, the it) *}
   1.125 +ML {* exec (example_prg, the it) *}
   1.126 +ML {* exec (example_prg, the it) *}
   1.127 +ML {* exec (example_prg, the it) *}
   1.128 +ML {* exec (example_prg, the it) *}
   1.129 +ML {* exec (example_prg, the it) *}
   1.130 +ML {* exec (example_prg, the it) *}
   1.131 +ML {* exec (example_prg, the it) *}
   1.132 +ML {* exec (example_prg, the it) *}
   1.133 +ML {* exec (example_prg, the it) *}
   1.134 +ML {* exec (example_prg, the it) *}
   1.135 +ML {* exec (example_prg, the it) *}
   1.136 +ML {* exec (example_prg, the it) *}
   1.137 +ML {* exec (example_prg, the it) *}
   1.138 +ML {* exec (example_prg, the it) *}
   1.139 +ML {* exec (example_prg, the it) *}
   1.140 +ML {* exec (example_prg, the it) *}
   1.141 +ML {* exec (example_prg, the it) *}
   1.142 +ML {* exec (example_prg, the it) *}
   1.143 +ML {* exec (example_prg, the it) *}
   1.144 +ML {* exec (example_prg, the it) *}
   1.145 +ML {* exec (example_prg, the it) *}
   1.146 +ML {* exec (example_prg, the it) *}
   1.147 +ML {* exec (example_prg, the it) *}
   1.148 +ML {* exec (example_prg, the it) *}
   1.149 +ML {* exec (example_prg, the it) *}
   1.150 +ML {* exec (example_prg, the it) *}
   1.151 +ML {* exec (example_prg, the it) *}
   1.152 +ML {* exec (example_prg, the it) *}
   1.153 +ML {* exec (example_prg, the it) *}
   1.154 +ML {* exec (example_prg, the it) *}
   1.155 +ML {* exec (example_prg, the it) *}
   1.156 +ML {* exec (example_prg, the it) *}
   1.157 +ML {* exec (example_prg, the it) *}
   1.158 +ML {* exec (example_prg, the it) *}
   1.159 +ML {* exec (example_prg, the it) *}
   1.160 +ML {* exec (example_prg, the it) *}
   1.161 +ML {* exec (example_prg, the it) *}
   1.162 +ML {* exec (example_prg, the it) *}
   1.163 +ML {* exec (example_prg, the it) *}
   1.164 +ML {* exec (example_prg, the it) *}
   1.165 +ML {* exec (example_prg, the it) *}
   1.166 +ML {* exec (example_prg, the it) *}
   1.167 +ML {* exec (example_prg, the it) *}
   1.168 +ML {* exec (example_prg, the it) *}
   1.169 +ML {* exec (example_prg, the it) *}
   1.170 +ML {* exec (example_prg, the it) *}
   1.171 +ML {* exec (example_prg, the it) *}
   1.172 +ML {* exec (example_prg, the it) *}
   1.173 +ML {* exec (example_prg, the it) *}
   1.174 +
   1.175 +end
   1.176 +