--- a/src/HOL/MicroJava/BV/BVExample.thy Mon Jun 29 12:18:57 2009 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy Mon Jun 29 12:18:57 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/MicroJava/BV/BVExample.thy
- ID: $Id$
Author: Gerwin Klein
*)
@@ -94,7 +93,7 @@
text {* Method and field lookup: *}
lemma method_Object [simp]:
- "method (E, Object) = empty"
+ "method (E, Object) = Map.empty"
by (simp add: method_rec_lemma [OF class_Object wf_subcls1_E])
lemma method_append [simp]:
@@ -436,7 +435,7 @@
"some_elem = (%S. SOME x. x : S)"
consts_code
- "some_elem" ("hd")
+ "some_elem" ("(case/ _ of/ {*Set*}/ xs/ =>/ hd/ xs)")
text {* This code setup is just a demonstration and \emph{not} sound! *}
@@ -455,7 +454,7 @@
(\<lambda>(ss, w).
let p = some_elem w in propa f (step p (ss ! p)) ss (w - {p}))
(ss, w)"
- unfolding iter_def is_empty_def some_elem_def ..
+ unfolding iter_def List_Set.is_empty_def some_elem_def ..
lemma JVM_sup_unfold [code]:
"JVMType.sup S m n = lift2 (Opt.sup
@@ -475,7 +474,6 @@
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
--- a/src/HOL/Tools/inductive_codegen.ML Mon Jun 29 12:18:57 2009 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Mon Jun 29 12:18:57 2009 +0200
@@ -378,7 +378,7 @@
end
| compile_prems out_ts vs names ps gr =
let
- val vs' = distinct (op =) (List.concat (vs :: map term_vs out_ts));
+ val vs' = distinct (op =) (flat (vs :: map term_vs out_ts));
val SOME (p, mode as SOME (Mode (_, js, _))) =
select_mode_prem thy modes' vs' ps;
val ps' = filter_out (equal p) ps;
@@ -404,7 +404,9 @@
(compile_expr thy defs dep module false modes
(mode, t) gr2)
else
- apfst (fn p => [str "DSeq.of_list", Pretty.brk 1, p])
+ apfst (fn p => Pretty.breaks [str "DSeq.of_list", str "(case", p,
+ str "of", str "Set", str "xs", str "=>", str "xs)"])
+ (*this is a very strong assumption about the generated code!*)
(invoke_codegen thy defs dep module true t gr2);
val (rest, gr4) = compile_prems out_ts''' vs' (fst nvs) ps' gr3;
in
@@ -661,8 +663,10 @@
let val (call_p, gr') = mk_ind_call thy defs dep module true
s T (ts1 @ ts2') names thyname k intrs gr
in SOME ((if brack then parens else I) (Pretty.block
- [str "DSeq.list_of", Pretty.brk 1, str "(",
- conv_ntuple fs ots call_p, str ")"]), gr')
+ [str "Set", Pretty.brk 1, str "(DSeq.list_of", Pretty.brk 1, str "(",
+ conv_ntuple fs ots call_p, str "))"]),
+ (*this is a very strong assumption about the generated code!*)
+ gr')
end
else NONE
end