# HG changeset patch
# User haftmann
# Date 1160556569 -7200
# Node ID 1e7df197b8b818f581e7d6bf3a84bd4fda26920f
# Parent  c2a342e548a9281a1847b11a4d8acbf6733fd917
added code generator setup

diff -r c2a342e548a9 -r 1e7df197b8b8 src/HOL/MicroJava/JVM/JVMListExample.thy
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Wed Oct 11 10:49:28 2006 +0200
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Wed Oct 11 10:49:29 2006 +0200
@@ -112,6 +112,66 @@
   "val_nam" ("\"val\"")
   "next_nam" ("\"next\"")
 
+code_type cnam and vnam and mname and loc_
+  (SML target_atom "string" and target_atom "string" and target_atom "string" and target_atom "IntInf.int")
+
+instance cnam :: eq
+  and cname :: eq
+  and vname :: eq
+  and mname :: eq
+  and ty :: eq
+  and instr :: eq ..
+
+definition
+  arbitrary_val :: val
+  "arbitrary_val = arbitrary"
+  arbitrary_cname :: cname
+  "arbitrary_cname = arbitrary"
+
+declare arbitrary_val_def [symmetric, code inline]
+declare arbitrary_cname_def [symmetric, code inline]
+
+definition
+  "unit' = Unit"
+  "object' = Object"
+
+code_constsubst
+  arbitrary_val \<equiv> unit'
+  arbitrary_cname \<equiv> object'
+
+code_const list_nam and test_nam and append_name and makelist_name and val_nam and next_nam
+  (SML target_atom "\"list\"" and target_atom "\"test\"" and target_atom "\"append\""
+    and target_atom "\"makelist\"" and target_atom "\"val\"" and target_atom "\"next\"")
+
+axiomatization
+  incr_loc :: "loc_ \<Rightarrow> loc_"
+  and zero_loc :: "loc_"
+
+code_const incr_loc and zero_loc
+  (SML target_atom "(_ + 1)" and target_atom "0")
+
+axiomatization
+  test_loc :: "(loc_ \<Rightarrow> bool) \<Rightarrow> (loc_ \<Rightarrow> 'a) \<Rightarrow> loc_ \<Rightarrow> 'a" where
+  "test_loc p v l = (if p l then v l else test_loc p v (incr l))"
+
+definition
+  new_addr' :: "(loc \<Rightarrow> (cname \<times> (vname \<times> cname \<Rightarrow> val option)) option) \<Rightarrow> loc \<times> val option"
+  "new_addr' hp =
+    test_loc (\<lambda>i. is_none (hp (Loc i) )) (\<lambda>i. (Loc i, None)) zero_loc"
+
+lemma [code func]:
+  "wf_class = wf_class" ..
+
+code_const
+  wf_class (SML target_atom "(fn _ => true)")
+
+code_constsubst
+  new_Addr \<equiv> new_addr'
+
+definition
+  "test = exec (E, start_state E test_name makelist_name)"
+
+
 subsection {* Single step execution *}
 
 code_module JVM