# HG changeset patch
# User haftmann
# Date 1246270737 -7200
# Node ID a16bb835e97d31d34559ff399cf780a69303084d
# Parent  c04f8c51d0aba04c03b32509f79b8e2cc3726448
explicit Set constructor for code generated for sets

diff -r c04f8c51d0ab -r a16bb835e97d src/HOL/MicroJava/BV/BVExample.thy
--- 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
 
diff -r c04f8c51d0ab -r a16bb835e97d src/HOL/Tools/inductive_codegen.ML
--- 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