--- a/src/HOL/MicroJava/BV/BVExample.thy Fri Aug 05 00:14:08 2011 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy Fri Aug 05 14:16:44 2011 +0200
@@ -21,13 +21,6 @@
*}
section "Setup"
-text {*
- Since the types @{typ cnam}, @{text vnam}, and @{text mname} are
- anonymous, we describe distinctness of names in the example by axioms:
-*}
-axioms
- distinct_classes: "list_nam \<noteq> test_nam"
- distinct_fields: "val_nam \<noteq> next_nam"
text {* Abbreviations for definitions we will have to use often in the
proofs below: *}
@@ -415,35 +408,45 @@
in kiljvm G mxs (1+size pTs+mxl) rT et instr start)"
lemma [code]:
- "unstables r step ss = (UN p:{..<size ss}. if \<not>stable r step ss p then {p} else {})"
- apply (unfold unstables_def)
- apply (rule equalityI)
- apply (rule subsetI)
- apply (erule CollectE)
- apply (erule conjE)
- apply (rule UN_I)
- apply simp
- apply simp
- apply (rule subsetI)
- apply (erule UN_E)
- apply (case_tac "\<not> stable r step ss p")
- apply simp+
- done
+ "unstables r step ss =
+ foldr (\<lambda>p A. if \<not>stable r step ss p then insert p A else A) [0..<size ss] {}"
+proof -
+ have "unstables r step ss = (UN p:{..<size ss}. if \<not>stable r step ss p then {p} else {})"
+ apply (unfold unstables_def)
+ apply (rule equalityI)
+ apply (rule subsetI)
+ apply (erule CollectE)
+ apply (erule conjE)
+ apply (rule UN_I)
+ apply simp
+ apply simp
+ apply (rule subsetI)
+ apply (erule UN_E)
+ apply (case_tac "\<not> stable r step ss p")
+ apply simp+
+ done
+ also have "\<And>f. (UN p:{..<size ss}. f p) = Union (set (map f [0..<size ss]))" by auto
+ also note Sup_set_foldr also note foldr_map
+ also have "op \<union> \<circ> (\<lambda>p. if \<not> stable r step ss p then {p} else {}) =
+ (\<lambda>p A. if \<not>stable r step ss p then insert p A else A)"
+ by(auto simp add: fun_eq_iff)
+ finally show ?thesis .
+qed
-definition some_elem :: "'a set \<Rightarrow> 'a" where
+definition some_elem :: "'a set \<Rightarrow> 'a" where [code del]:
"some_elem = (%S. SOME x. x : S)"
-
-consts_code
- "some_elem" ("(case/ _ of/ {*Set*}/ xs/ =>/ hd/ xs)")
+code_const some_elem
+ (SML "(case/ _ of/ Set/ xs/ =>/ hd/ xs)")
+setup {* Code.add_signature_cmd ("some_elem", "'a set \<Rightarrow> 'a") *}
text {* This code setup is just a demonstration and \emph{not} sound! *}
lemma False
proof -
have "some_elem (set [False, True]) = False"
- by evaluation
+ by eval
moreover have "some_elem (set [True, False]) = True"
- by evaluation
+ by eval
ultimately show False
by (simp add: some_elem_def)
qed
@@ -465,15 +468,35 @@
by simp
lemmas [code] = JType.sup_def [unfolded exec_lub_def] JVM_le_unfold
+lemmas [code] = lesub_def plussub_def
-lemmas [code_ind] = rtranclp.rtrancl_refl converse_rtranclp_into_rtranclp
+setup {*
+ Code.add_signature_cmd ("More_Set.is_empty", "'a set \<Rightarrow> bool")
+ #> Code.add_signature_cmd ("propa", "('s \<Rightarrow> 's \<Rightarrow> 's) \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's list \<Rightarrow> nat set \<Rightarrow> 's list * nat set")
+ #> Code.add_signature_cmd
+ ("iter", "('s \<Rightarrow> 's \<Rightarrow> 's) \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> (nat \<times> 's) list) \<Rightarrow> 's list \<Rightarrow> nat set \<Rightarrow> 's list * nat set")
+ #> Code.add_signature_cmd ("unstables", "('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> (nat \<times> 's) list) \<Rightarrow> 's list \<Rightarrow> nat set")
+*}
+
+definition [code del]: "mem2 = op :"
+lemma [code]: "mem2 x A = A x"
+ by(simp add: mem2_def mem_def)
-code_module BV
-contains
- test1 = "test_kil E list_name [Class list_name] (PrimT Void) 3 0
+lemmas [folded mem2_def, code] =
+ JType.sup_def[unfolded exec_lub_def]
+ wf_class_code
+ widen.equation
+ match_exception_entry_def
+
+definition test1 where
+ "test1 = test_kil E list_name [Class list_name] (PrimT Void) 3 0
[(Suc 0, 2, 8, Xcpt NullPointer)] append_ins"
- test2 = "test_kil E test_name [] (PrimT Void) 3 2 [] make_list_ins"
-ML BV.test1
-ML BV.test2
+definition test2 where
+ "test2 = test_kil E test_name [] (PrimT Void) 3 2 [] make_list_ins"
+
+ML {*
+ @{code test1};
+ @{code test2};
+*}
end
--- a/src/HOL/MicroJava/J/JBasis.thy Fri Aug 05 00:14:08 2011 +0200
+++ b/src/HOL/MicroJava/J/JBasis.thy Fri Aug 05 14:16:44 2011 +0200
@@ -7,7 +7,7 @@
\isaheader{Some Auxiliary Definitions}
*}
-theory JBasis imports Main begin
+theory JBasis imports Main "~~/src/HOL/Library/Transitive_Closure_Table" begin
lemmas [simp] = Let_def
--- a/src/HOL/MicroJava/J/State.thy Fri Aug 05 00:14:08 2011 +0200
+++ b/src/HOL/MicroJava/J/State.thy Fri Aug 05 14:16:44 2011 +0200
@@ -52,8 +52,18 @@
definition raise_if :: "bool \<Rightarrow> xcpt \<Rightarrow> val option \<Rightarrow> val option" where
"raise_if b x xo \<equiv> if b \<and> (xo = None) then Some (Addr (XcptRef x)) else xo"
+text {* Make new_Addr completely specified (at least for the code generator) *}
+(*
definition new_Addr :: "aheap => loc \<times> val option" where
"new_Addr h \<equiv> SOME (a,x). (h a = None \<and> x = None) | x = Some (Addr (XcptRef OutOfMemory))"
+*)
+consts nat_to_loc' :: "nat => loc'"
+code_datatype nat_to_loc'
+definition new_Addr :: "aheap => loc \<times> val option" where
+ "new_Addr h \<equiv>
+ if \<exists>n. h (Loc (nat_to_loc' n)) = None
+ then (Loc (nat_to_loc' (LEAST n. h (Loc (nat_to_loc' n)) = None)), None)
+ else (Loc (nat_to_loc' 0), Some (Addr (XcptRef OutOfMemory)))"
definition np :: "val => val option => val option" where
"np v == raise_if (v = Null) NullPointer"
@@ -74,11 +84,8 @@
hp ref = None \<and> xcp = None \<or> xcp = Some (Addr (XcptRef OutOfMemory))"
apply (drule sym)
apply (unfold new_Addr_def)
-apply(simp add: Pair_fst_snd_eq Eps_split)
-apply(rule someI)
-apply(rule disjI2)
-apply(rule_tac r = "snd (?a,Some (Addr (XcptRef OutOfMemory)))" in trans)
-apply auto
+apply (simp split: split_if_asm)
+apply (erule LeastI)
done
lemma raise_if_True [simp]: "raise_if True x y \<noteq> None"
@@ -150,4 +157,42 @@
lemma c_hupd_fst [simp]: "fst (c_hupd h (x, s)) = x"
by (simp add: c_hupd_def split_beta)
+text {* Naive implementation for @{term "new_Addr"} by exhaustive search *}
+
+definition gen_new_Addr :: "aheap => nat \<Rightarrow> loc \<times> val option" where
+ "gen_new_Addr h n \<equiv>
+ if \<exists>a. a \<ge> n \<and> h (Loc (nat_to_loc' a)) = None
+ then (Loc (nat_to_loc' (LEAST a. a \<ge> n \<and> h (Loc (nat_to_loc' a)) = None)), None)
+ else (Loc (nat_to_loc' 0), Some (Addr (XcptRef OutOfMemory)))"
+
+lemma new_Addr_code_code [code]:
+ "new_Addr h = gen_new_Addr h 0"
+by(simp only: new_Addr_def gen_new_Addr_def split: split_if) simp
+
+lemma gen_new_Addr_code [code]:
+ "gen_new_Addr h n = (if h (Loc (nat_to_loc' n)) = None then (Loc (nat_to_loc' n), None) else gen_new_Addr h (Suc n))"
+apply(simp add: gen_new_Addr_def)
+apply(rule impI)
+apply(rule conjI)
+ apply safe[1]
+ apply(auto intro: arg_cong[where f=nat_to_loc'] Least_equality)[1]
+ apply(rule arg_cong[where f=nat_to_loc'])
+ apply(rule arg_cong[where f=Least])
+ apply(rule ext)
+ apply(safe, simp_all)[1]
+ apply(rename_tac "n'")
+ apply(case_tac "n = n'", simp_all)[1]
+apply clarify
+apply(subgoal_tac "a = n")
+ apply(auto intro: Least_equality arg_cong[where f=nat_to_loc'])[1]
+apply(rule ccontr)
+apply(erule_tac x="a" in allE)
+apply simp
+done
+
+instantiation loc' :: equal begin
+definition "HOL.equal (l :: loc') l' \<longleftrightarrow> l = l'"
+instance proof qed(simp add: equal_loc'_def)
end
+
+end
--- a/src/HOL/MicroJava/J/SystemClasses.thy Fri Aug 05 00:14:08 2011 +0200
+++ b/src/HOL/MicroJava/J/SystemClasses.thy Fri Aug 05 14:16:44 2011 +0200
@@ -13,18 +13,18 @@
*}
definition ObjectC :: "'c cdecl" where
- "ObjectC \<equiv> (Object, (undefined,[],[]))"
+ [code_inline]: "ObjectC \<equiv> (Object, (undefined,[],[]))"
definition NullPointerC :: "'c cdecl" where
- "NullPointerC \<equiv> (Xcpt NullPointer, (Object,[],[]))"
+ [code_inline]: "NullPointerC \<equiv> (Xcpt NullPointer, (Object,[],[]))"
definition ClassCastC :: "'c cdecl" where
- "ClassCastC \<equiv> (Xcpt ClassCast, (Object,[],[]))"
+ [code_inline]: "ClassCastC \<equiv> (Xcpt ClassCast, (Object,[],[]))"
definition OutOfMemoryC :: "'c cdecl" where
- "OutOfMemoryC \<equiv> (Xcpt OutOfMemory, (Object,[],[]))"
+ [code_inline]: "OutOfMemoryC \<equiv> (Xcpt OutOfMemory, (Object,[],[]))"
definition SystemClasses :: "'c cdecl list" where
- "SystemClasses \<equiv> [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]"
+ [code_inline]: "SystemClasses \<equiv> [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]"
end
--- a/src/HOL/MicroJava/J/Type.thy Fri Aug 05 00:14:08 2011 +0200
+++ b/src/HOL/MicroJava/J/Type.thy Fri Aug 05 14:16:44 2011 +0200
@@ -8,6 +8,10 @@
theory Type imports JBasis begin
typedecl cnam
+instantiation cnam :: equal begin
+definition "HOL.equal (cn :: cnam) cn' \<longleftrightarrow> cn = cn'"
+instance proof qed(simp add: equal_cnam_def)
+end
-- "exceptions"
datatype
@@ -23,7 +27,16 @@
| Cname cnam
typedecl vnam -- "variable or field name"
+instantiation vnam :: equal begin
+definition "HOL.equal (vn :: vnam) vn' \<longleftrightarrow> vn = vn'"
+instance proof qed(simp add: equal_vnam_def)
+end
+
typedecl mname -- "method name"
+instantiation mname :: equal begin
+definition "HOL.equal (M :: mname) M' \<longleftrightarrow> M = M'"
+instance proof qed(simp add: equal_mname_def)
+end
-- "names for @{text This} pointer and local/field variables"
datatype vname
--- a/src/HOL/MicroJava/J/TypeRel.thy Fri Aug 05 00:14:08 2011 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy Fri Aug 05 14:16:44 2011 +0200
@@ -77,22 +77,112 @@
"wf_class G = wf ((subcls1 G)^-1)"
-text {* Code generator setup (FIXME!) *}
+
+text {* Code generator setup *}
+
+code_pred
+ (modes: i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool, i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool)
+ subcls1p
+ .
+declare subcls1_def[unfolded Collect_def, code_pred_def]
+code_pred
+ (modes: i \<Rightarrow> i \<times> o \<Rightarrow> bool, i \<Rightarrow> i \<times> i \<Rightarrow> bool)
+ [inductify]
+ subcls1
+ .
+
+definition subcls' where "subcls' G = (subcls1p G)^**"
+code_pred
+ (modes: i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool, i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool)
+ [inductify]
+ subcls'
+.
+lemma subcls_conv_subcls' [code_inline]:
+ "(subcls1 G)^* = (\<lambda>(C, D). subcls' G C D)"
+by(simp add: subcls'_def subcls1_def rtrancl_def)(simp add: Collect_def)
+
+lemma class_rec_code [code]:
+ "class_rec G C t f =
+ (if wf_class G then
+ (case class G C of
+ None \<Rightarrow> class_rec G C t f
+ | Some (D, fs, ms) \<Rightarrow>
+ if C = Object then f Object fs ms t else f C fs ms (class_rec G D t f))
+ else class_rec G C t f)"
+apply(cases "wf_class G")
+ apply(unfold class_rec_def wf_class_def)
+ apply(subst wfrec, assumption)
+ apply(cases "class G C")
+ apply(simp add: wfrec)
+ apply clarsimp
+ apply(rename_tac D fs ms)
+ apply(rule_tac f="f C fs ms" in arg_cong)
+ apply(clarsimp simp add: cut_def)
+ apply(blast intro: subcls1I)
+apply simp
+done
-consts_code
- "wfrec" ("\<module>wfrec?")
-attach {*
-fun wfrec f x = f (wfrec f) x;
-*}
+lemma wf_class_code [code]:
+ "wf_class G \<longleftrightarrow> (\<forall>(C, rest) \<in> set G. C \<noteq> Object \<longrightarrow> \<not> G \<turnstile> fst (the (class G C)) \<preceq>C C)"
+proof
+ assume "wf_class G"
+ hence wf: "wf (((subcls1 G)^+)^-1)" unfolding wf_class_def by(rule wf_converse_trancl)
+ hence acyc: "acyclic ((subcls1 G)^+)" by(auto dest: wf_acyclic)
+ show "\<forall>(C, rest) \<in> set G. C \<noteq> Object \<longrightarrow> \<not> G \<turnstile> fst (the (class G C)) \<preceq>C C"
+ proof(safe)
+ fix C D fs ms
+ assume "(C, D, fs, ms) \<in> set G"
+ and "C \<noteq> Object"
+ and subcls: "G \<turnstile> fst (the (class G C)) \<preceq>C C"
+ from `(C, D, fs, ms) \<in> set G` obtain D' fs' ms'
+ where "class": "class G C = Some (D', fs', ms')"
+ unfolding class_def by(auto dest!: weak_map_of_SomeI)
+ hence "G \<turnstile> C \<prec>C1 D'" using `C \<noteq> Object` ..
+ hence "(C, D') \<in> (subcls1 G)^+" ..
+ also with acyc have "C \<noteq> D'" by(auto simp add: acyclic_def)
+ with subcls "class" have "(D', C) \<in> (subcls1 G)^+" by(auto dest: rtranclD)
+ finally show False using acyc by(auto simp add: acyclic_def)
+ qed
+next
+ assume rhs[rule_format]: "\<forall>(C, rest) \<in> set G. C \<noteq> Object \<longrightarrow> \<not> G \<turnstile> fst (the (class G C)) \<preceq>C C"
+ have "acyclic (subcls1 G)"
+ proof(intro acyclicI strip notI)
+ fix C
+ assume "(C, C) \<in> (subcls1 G)\<^sup>+"
+ thus False
+ proof(cases)
+ case base
+ then obtain rest where "class G C = Some (C, rest)"
+ and "C \<noteq> Object" by cases
+ from `class G C = Some (C, rest)` have "(C, C, rest) \<in> set G"
+ unfolding class_def by(rule map_of_SomeD)
+ with `C \<noteq> Object` `class G C = Some (C, rest)`
+ have "\<not> G \<turnstile> C \<preceq>C C" by(auto dest: rhs)
+ thus False by simp
+ next
+ case (step D)
+ from `G \<turnstile> D \<prec>C1 C` obtain rest where "class G D = Some (C, rest)"
+ and "D \<noteq> Object" by cases
+ from `class G D = Some (C, rest)` have "(D, C, rest) \<in> set G"
+ unfolding class_def by(rule map_of_SomeD)
+ with `D \<noteq> Object` `class G D = Some (C, rest)`
+ have "\<not> G \<turnstile> C \<preceq>C D" by(auto dest: rhs)
+ moreover from `(C, D) \<in> (subcls1 G)\<^sup>+`
+ have "G \<turnstile> C \<preceq>C D" by(rule trancl_into_rtrancl)
+ ultimately show False by contradiction
+ qed
+ qed
+ thus "wf_class G" unfolding wf_class_def
+ by(rule finite_acyclic_wf_converse[OF finite_subcls1])
+qed
consts
-
method :: "'c prog \<times> cname => ( sig \<rightharpoonup> cname \<times> ty \<times> 'c)" (* ###curry *)
field :: "'c prog \<times> cname => ( vname \<rightharpoonup> cname \<times> ty )" (* ###curry *)
fields :: "'c prog \<times> cname => ((vname \<times> cname) \<times> ty) list" (* ###curry *)
-- "methods of a class, with inheritance, overriding and hiding, cf. 8.4.6"
-defs method_def: "method \<equiv> \<lambda>(G,C). class_rec G C empty (\<lambda>C fs ms ts.
+defs method_def [code]: "method \<equiv> \<lambda>(G,C). class_rec G C empty (\<lambda>C fs ms ts.
ts ++ map_of (map (\<lambda>(s,m). (s,(C,m))) ms))"
lemma method_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==>
@@ -106,7 +196,7 @@
-- "list of fields of a class, including inherited and hidden ones"
-defs fields_def: "fields \<equiv> \<lambda>(G,C). class_rec G C [] (\<lambda>C fs ms ts.
+defs fields_def [code]: "fields \<equiv> \<lambda>(G,C). class_rec G C [] (\<lambda>C fs ms ts.
map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ ts)"
lemma fields_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==>
@@ -119,7 +209,7 @@
done
-defs field_def: "field == map_of o (map (\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
+defs field_def [code]: "field == map_of o (map (\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
lemma field_fields:
"field (G,C) fn = Some (fd, fT) \<Longrightarrow> map_of (fields (G,C)) (fn, fd) = Some fT"
@@ -138,6 +228,8 @@
| subcls : "G\<turnstile>C\<preceq>C D ==> G\<turnstile>Class C \<preceq> Class D"
| null [intro!]: "G\<turnstile> NT \<preceq> RefT R"
+code_pred widen .
+
lemmas refl = HOL.refl
-- "casting conversion, cf. 5.5 / 5.1.5"
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy Fri Aug 05 00:14:08 2011 +0200
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy Fri Aug 05 14:16:44 2011 +0200
@@ -8,13 +8,20 @@
imports "../J/SystemClasses" JVMExec
begin
-consts
- list_nam :: cnam
- test_nam :: cnam
- append_name :: mname
- makelist_name :: mname
- val_nam :: vnam
- next_nam :: vnam
+text {*
+ Since the types @{typ cnam}, @{text vnam}, and @{text mname} are
+ anonymous, we describe distinctness of names in the example by axioms:
+*}
+axiomatization list_nam test_nam :: cnam
+where distinct_classes: "list_nam \<noteq> test_nam"
+
+axiomatization append_name makelist_name :: mname
+where distinct_methods: "append_name \<noteq> makelist_name"
+
+axiomatization val_nam next_nam :: vnam
+where distinct_fields: "val_nam \<noteq> next_nam"
+
+axioms nat_to_loc'_inject: "nat_to_loc' l = nat_to_loc' l' \<longleftrightarrow> l = l'"
definition list_name :: cname where
"list_name == Cname list_nam"
@@ -86,96 +93,103 @@
definition E :: jvm_prog where
"E == SystemClasses @ [(list_name, list_class), (test_name, test_class)]"
+code_datatype list_nam test_nam
+lemma equal_cnam_code [code]:
+ "HOL.equal list_nam list_nam \<longleftrightarrow> True"
+ "HOL.equal test_nam test_nam \<longleftrightarrow> True"
+ "HOL.equal list_nam test_nam \<longleftrightarrow> False"
+ "HOL.equal test_nam list_nam \<longleftrightarrow> False"
+ by(simp_all add: distinct_classes distinct_classes[symmetric] equal_cnam_def)
-types_code
- cnam ("string")
- vnam ("string")
- mname ("string")
- loc' ("int")
+code_datatype append_name makelist_name
+lemma equal_mname_code [code]:
+ "HOL.equal append_name append_name \<longleftrightarrow> True"
+ "HOL.equal makelist_name makelist_name \<longleftrightarrow> True"
+ "HOL.equal append_name makelist_name \<longleftrightarrow> False"
+ "HOL.equal makelist_name append_name \<longleftrightarrow> False"
+ by(simp_all add: distinct_methods distinct_methods[symmetric] equal_mname_def)
-consts_code
- "new_Addr" ("\<module>new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *}/ {* Loc *}")
-attach {*
-fun new_addr p none loc hp =
- let fun nr i = if p (hp (loc i)) then (loc i, none) else nr (i+1);
- in nr 0 end;
-*}
+code_datatype val_nam next_nam
+lemma equal_vnam_code [code]:
+ "HOL.equal val_nam val_nam \<longleftrightarrow> True"
+ "HOL.equal next_nam next_nam \<longleftrightarrow> True"
+ "HOL.equal val_nam next_nam \<longleftrightarrow> False"
+ "HOL.equal next_nam val_nam \<longleftrightarrow> False"
+ by(simp_all add: distinct_fields distinct_fields[symmetric] equal_vnam_def)
+
- "undefined" ("(raise Match)")
- "undefined :: val" ("{* Unit *}")
- "undefined :: cname" ("{* Object *}")
+lemma equal_loc'_code [code]:
+ "HOL.equal (nat_to_loc' l) (nat_to_loc' l') \<longleftrightarrow> l = l'"
+ by(simp add: equal_loc'_def nat_to_loc'_inject)
- "list_nam" ("\"list\"")
- "test_nam" ("\"test\"")
- "append_name" ("\"append\"")
- "makelist_name" ("\"makelist\"")
- "val_nam" ("\"val\"")
- "next_nam" ("\"next\"")
+definition undefined_cname :: cname
+ where [code del]: "undefined_cname = undefined"
+code_datatype Object Xcpt Cname undefined_cname
+declare undefined_cname_def[symmetric, code_inline]
+
+definition undefined_val :: val
+ where [code del]: "undefined_val = undefined"
+declare undefined_val_def[symmetric, code_inline]
+code_datatype Unit Null Bool Intg Addr undefined_val
definition
"test = exec (E, start_state E test_name makelist_name)"
-
-subsection {* Single step execution *}
-
-code_module JVM
-contains
- exec = exec
- test = test
-
-ML {* JVM.test *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {*
+ @{code test};
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+ @{code exec} (@{code E}, @{code the} it);
+*}
end