--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sat Oct 24 16:55:42 2009 +0200
@@ -89,6 +89,13 @@
[]
else [intro]
+
+fun print_intross thy msg intross =
+ tracing (msg ^
+ (space_implode "; " (map
+ (fn intros => commas (map (Display.string_of_thm_global thy) intros)) intross)))
+
+
fun preprocess_strong_conn_constnames gr constnames thy =
let
val get_specs = map (fn k => (k, Graph.get_node gr k))
@@ -103,8 +110,7 @@
val _ = priority "Compiling predicates to flat introrules..."
val (intross1, thy'') = apfst flat (fold_map Predicate_Compile_Pred.preprocess
(get_specs prednames) thy')
- val _ = tracing ("Flattened introduction rules: " ^
- commas (map (Display.string_of_thm_global thy'') (flat intross1)))
+ val _ = print_intross thy'' "Flattened introduction rules: " intross1
val _ = priority "Replacing functions in introrules..."
(* val _ = burrow (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross *)
val intross2 =
@@ -113,11 +119,12 @@
SOME intross => intross
| NONE => let val _ = warning "Function replacement failed!" in intross1 end
else burrow (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross1
- val _ = tracing ("Introduction rules with replaced functions: " ^
- commas (map (Display.string_of_thm_global thy'') (flat intross2)))
- val intross3 = burrow (maps remove_pointless_clauses) intross2
+ val _ = print_intross thy'' "Introduction rules with replaced functions: " intross2
+ val intross3 = map (maps remove_pointless_clauses) intross2
+ val _ = print_intross thy'' "After removing pointless clauses: " intross3
val intross4 = burrow (map (AxClass.overload thy'')) intross3
val intross5 = burrow (map (simplify_fst_snd o expand_tuples thy'')) intross4
+ val _ = print_intross thy'' "introduction rules before registering: " intross5
val _ = priority "Registering intro rules..."
val thy''' = fold Predicate_Compile_Core.register_intros intross5 thy''
in
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Oct 24 16:55:42 2009 +0200
@@ -697,6 +697,9 @@
fun register_intros pre_intros thy =
let
val (c, T) = dest_Const (fst (strip_intro_concl 0 (prop_of (hd pre_intros))))
+ fun constname_of_intro intr = fst (dest_Const (fst (strip_intro_concl 0 (prop_of intr))))
+ val _ = if not (forall (fn intr => constname_of_intro intr = c) pre_intros) then
+ error "register_intros: Introduction rules of different constants are used" else ()
val _ = Output.tracing ("Registering introduction rules of " ^ c)
val _ = Output.tracing (commas (map (Display.string_of_thm_global thy) pre_intros))
val nparams = guess_nparams T
--- a/src/HOL/ex/Predicate_Compile_ex.thy Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy Sat Oct 24 16:55:42 2009 +0200
@@ -1,5 +1,5 @@
theory Predicate_Compile_ex
-imports Main Predicate_Compile
+imports Main Predicate_Compile_Alternative_Defs
begin
inductive even :: "nat \<Rightarrow> bool" and odd :: "nat \<Rightarrow> bool" where
@@ -122,7 +122,7 @@
"map_ofP ((a, b)#xs) a b"
| "map_ofP xs a b \<Longrightarrow> map_ofP (x#xs) a b"
-code_pred map_ofP .
+code_pred (mode: [1], [1, 2], [1, 2, 3], [1, 3]) map_ofP .
thm map_ofP.equation
section {* reverse *}
@@ -371,10 +371,7 @@
code_pred (inductify_all) avl .
thm avl.equation
-(*
-lemma [code_pred_inline]: "bot_fun_inst.bot_fun == (\<lambda>(y::'a::type). False)"
-unfolding bot_fun_inst.bot_fun[symmetric] bot_bool_eq[symmetric] bot_fun_eq by simp
-*)
+
fun set_of
where
"set_of ET = {}"
@@ -385,33 +382,10 @@
"is_ord ET = True"
| "is_ord (MKT n l r h) =
((\<forall>n' \<in> set_of l. n' < n) \<and> (\<forall>n' \<in> set_of r. n < n') \<and> is_ord l \<and> is_ord r)"
-(*
-lemma empty_set[code_pred_def]: "{} = (\<lambda>x. False)" unfolding empty_def by simp
-thm set_of.simps[unfolded empty_set Un_def]
-*)
-(*
-declare empty_def[code_pred_def]
-*)
-ML {* prop_of (@{thm set_of.simps(1)}) *}
-thm Un_def
-thm eq_refl
-declare eq_reflection[OF empty_def, code_pred_inline]
-thm Un_def
-definition Un' where "Un' A B == A Un B"
-lemma [code_pred_intros]: "A x ==> Un' A B x"
-and [code_pred_intros] : "B x ==> Un' A B x"
-sorry
-
-code_pred Un' sorry
-
-lemmas a = Un'_def[symmetric]
-declare a[code_pred_inline]
-declare set_of.simps
-ML {* prop_of @{thm Un_def} *}
-ML {* tap *}
code_pred (inductify_all) set_of .
thm set_of.equation
+text {* expected mode: [1], [1, 2] *}
(* FIXME *)
(*
code_pred (inductify_all) is_ord .