explicit Set constructor for code generated for sets
authorhaftmann
Mon Jun 29 12:18:57 2009 +0200 (2009-06-29)
changeset 31852a16bb835e97d
parent 31851 c04f8c51d0ab
child 31853 f079b174e56a
explicit Set constructor for code generated for sets
src/HOL/MicroJava/BV/BVExample.thy
src/HOL/Tools/inductive_codegen.ML
     1.1 --- a/src/HOL/MicroJava/BV/BVExample.thy	Mon Jun 29 12:18:57 2009 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/BVExample.thy	Mon Jun 29 12:18:57 2009 +0200
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/MicroJava/BV/BVExample.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Gerwin Klein
     1.7  *)
     1.8  
     1.9 @@ -94,7 +93,7 @@
    1.10  
    1.11  text {* Method and field lookup: *}
    1.12  lemma method_Object [simp]:
    1.13 -  "method (E, Object) = empty"
    1.14 +  "method (E, Object) = Map.empty"
    1.15    by (simp add: method_rec_lemma [OF class_Object wf_subcls1_E])
    1.16  
    1.17  lemma method_append [simp]:
    1.18 @@ -436,7 +435,7 @@
    1.19    "some_elem = (%S. SOME x. x : S)"
    1.20  
    1.21  consts_code
    1.22 -  "some_elem" ("hd")
    1.23 +  "some_elem" ("(case/ _ of/ {*Set*}/ xs/ =>/ hd/ xs)")
    1.24  
    1.25  text {* This code setup is just a demonstration and \emph{not} sound! *}
    1.26  
    1.27 @@ -455,7 +454,7 @@
    1.28      (\<lambda>(ss, w).
    1.29          let p = some_elem w in propa f (step p (ss ! p)) ss (w - {p}))
    1.30      (ss, w)"
    1.31 -  unfolding iter_def is_empty_def some_elem_def ..
    1.32 +  unfolding iter_def List_Set.is_empty_def some_elem_def ..
    1.33  
    1.34  lemma JVM_sup_unfold [code]:
    1.35   "JVMType.sup S m n = lift2 (Opt.sup
    1.36 @@ -475,7 +474,6 @@
    1.37    test1 = "test_kil E list_name [Class list_name] (PrimT Void) 3 0
    1.38      [(Suc 0, 2, 8, Xcpt NullPointer)] append_ins"
    1.39    test2 = "test_kil E test_name [] (PrimT Void) 3 2 [] make_list_ins"
    1.40 -
    1.41  ML BV.test1
    1.42  ML BV.test2
    1.43  
     2.1 --- a/src/HOL/Tools/inductive_codegen.ML	Mon Jun 29 12:18:57 2009 +0200
     2.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Mon Jun 29 12:18:57 2009 +0200
     2.3 @@ -378,7 +378,7 @@
     2.4            end
     2.5        | compile_prems out_ts vs names ps gr =
     2.6            let
     2.7 -            val vs' = distinct (op =) (List.concat (vs :: map term_vs out_ts));
     2.8 +            val vs' = distinct (op =) (flat (vs :: map term_vs out_ts));
     2.9              val SOME (p, mode as SOME (Mode (_, js, _))) =
    2.10                select_mode_prem thy modes' vs' ps;
    2.11              val ps' = filter_out (equal p) ps;
    2.12 @@ -404,7 +404,9 @@
    2.13                           (compile_expr thy defs dep module false modes
    2.14                             (mode, t) gr2)
    2.15                       else
    2.16 -                       apfst (fn p => [str "DSeq.of_list", Pretty.brk 1, p])
    2.17 +                       apfst (fn p => Pretty.breaks [str "DSeq.of_list", str "(case", p,
    2.18 +                         str "of", str "Set", str "xs", str "=>", str "xs)"])
    2.19 +                         (*this is a very strong assumption about the generated code!*)
    2.20                             (invoke_codegen thy defs dep module true t gr2);
    2.21                     val (rest, gr4) = compile_prems out_ts''' vs' (fst nvs) ps' gr3;
    2.22                   in
    2.23 @@ -661,8 +663,10 @@
    2.24                      let val (call_p, gr') = mk_ind_call thy defs dep module true
    2.25                        s T (ts1 @ ts2') names thyname k intrs gr 
    2.26                      in SOME ((if brack then parens else I) (Pretty.block
    2.27 -                      [str "DSeq.list_of", Pretty.brk 1, str "(",
    2.28 -                       conv_ntuple fs ots call_p, str ")"]), gr')
    2.29 +                      [str "Set", Pretty.brk 1, str "(DSeq.list_of", Pretty.brk 1, str "(",
    2.30 +                       conv_ntuple fs ots call_p, str "))"]),
    2.31 +                       (*this is a very strong assumption about the generated code!*)
    2.32 +                       gr')
    2.33                      end
    2.34                    else NONE
    2.35                  end