improved handling of alternative rules; added test cases for alternative rules; normalized tracing in the predicate compiler
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Oct 28 00:24:38 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Oct 28 12:29:00 2009 +0100
@@ -67,8 +67,6 @@
(* debug stuff *)
-fun tracing s = (if ! Toplevel.debug then Output.tracing s else ());
-
fun print_tac s = Seq.single;
fun print_tac' options s =
@@ -333,7 +331,7 @@
fun print_modes options modes =
if show_modes options then
- Output.tracing ("Inferred modes:\n" ^
+ tracing ("Inferred modes:\n" ^
cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
string_of_mode ms)) modes))
else ()
@@ -344,7 +342,7 @@
^ (string_of_entry pred mode entry)
fun print_pred (pred, modes) =
"predicate " ^ pred ^ ": " ^ cat_lines (map (print_mode pred) modes)
- val _ = Output.tracing (cat_lines (map print_pred pred_mode_table))
+ val _ = tracing (cat_lines (map print_pred pred_mode_table))
in () end;
fun string_of_prem thy (Prem (ts, p)) =
@@ -661,7 +659,7 @@
fun cons_intro gr =
case try (Graph.get_node gr) name of
SOME pred_data => Graph.map_node name (map_pred_data
- (apfst (fn (intros, elim, nparams) => (thm::intros, elim, nparams)))) gr
+ (apfst (fn (intros, elim, nparams) => (intros @ [thm], elim, nparams)))) gr
| NONE =>
let
val nparams = the_default (guess_nparams T) (try (#nparams o rep_pred_data o (fetch_pred_data thy)) name)
@@ -1052,9 +1050,9 @@
fun print_failed_mode options thy modes p m rs i =
if show_mode_inference options then
let
- val _ = Output.tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^
+ val _ = tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^
p ^ " violates mode " ^ string_of_mode m)
- val _ = Output.tracing (string_of_clause thy p (nth rs i))
+ val _ = tracing (string_of_clause thy p (nth rs i))
in () end
else ()
@@ -2142,7 +2140,6 @@
fun add_equations_of steps options prednames thy =
let
val _ = print_step options ("Starting predicate compiler for predicates " ^ commas prednames ^ "...")
- val _ = tracing (commas (map (Display.string_of_thm_global thy) (maps (intros_of thy) prednames)))
(*val _ = check_intros_elim_match thy prednames*)
(*val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames)*)
val (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) =
@@ -2181,7 +2178,7 @@
SOME v => (G, v)
| NONE => (Graph.new_node (key, value_of key) G, value_of key)
val (G'', visited') = fold (extend' value_of edges_of) (subtract (op =) visited (edges_of (key, v)))
- (G', key :: visited)
+ (G', key :: visited)
in
(fold (Graph.add_edge o (pair key)) (edges_of (key, v)) G'', visited')
end;
@@ -2307,7 +2304,7 @@
(extend (fetch_pred_data thy) (depending_preds_of thy) const)) lthy
|> LocalTheory.checkpoint
val thy' = ProofContext.theory_of lthy'
- val preds = Graph.all_preds (PredData.get thy') [const] |> filter_out (has_elim thy')
+ val preds = Graph.all_succs (PredData.get thy') [const] |> filter_out (has_elim thy')
fun mk_cases const =
let
val T = Sign.the_const_type thy const
--- a/src/HOL/ex/Predicate_Compile_Alternative_Defs.thy Wed Oct 28 00:24:38 2009 +0100
+++ b/src/HOL/ex/Predicate_Compile_Alternative_Defs.thy Wed Oct 28 12:29:00 2009 +0100
@@ -45,7 +45,7 @@
unfolding mem_def[symmetric, of _ a2]
apply auto
unfolding mem_def
- apply auto
+ apply fastsimp
done
qed
--- a/src/HOL/ex/Predicate_Compile_ex.thy Wed Oct 28 00:24:38 2009 +0100
+++ b/src/HOL/ex/Predicate_Compile_ex.thy Wed Oct 28 12:29:00 2009 +0100
@@ -17,7 +17,7 @@
definition EmptySet' :: "'a \<Rightarrow> bool"
where "EmptySet' = {}"
-code_pred (mode: [], [1]) [inductify, show_intermediate_results] EmptySet' .
+code_pred (mode: [], [1]) [inductify] EmptySet' .
inductive EmptyRel :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
@@ -61,7 +61,87 @@
"zerozero (0, 0)"
code_pred zerozero .
-code_pred [rpred, show_compilation] zerozero .
+code_pred [rpred] zerozero .
+
+subsection {* Alternative Rules *}
+
+datatype char = C | D | E | F | G
+
+inductive is_C_or_D
+where
+ "(x = C) \<or> (x = D) ==> is_C_or_D x"
+
+code_pred (mode: [1]) is_C_or_D .
+thm is_C_or_D.equation
+
+inductive is_D_or_E
+where
+ "(x = D) \<or> (x = E) ==> is_D_or_E x"
+
+lemma [code_pred_intros]:
+ "is_D_or_E D"
+by (auto intro: is_D_or_E.intros)
+
+lemma [code_pred_intros]:
+ "is_D_or_E E"
+by (auto intro: is_D_or_E.intros)
+
+code_pred (mode: [], [1]) is_D_or_E
+proof -
+ case is_D_or_E
+ from this(1) show thesis
+ proof
+ fix x
+ assume x: "a1 = x"
+ assume "x = D \<or> x = E"
+ from this show thesis
+ proof
+ assume "x = D" from this x is_D_or_E(2) show thesis by simp
+ next
+ assume "x = E" from this x is_D_or_E(3) show thesis by simp
+ qed
+ qed
+qed
+
+thm is_D_or_E.equation
+
+inductive is_F_or_G
+where
+ "x = F \<or> x = G ==> is_F_or_G x"
+
+lemma [code_pred_intros]:
+ "is_F_or_G F"
+by (auto intro: is_F_or_G.intros)
+
+lemma [code_pred_intros]:
+ "is_F_or_G G"
+by (auto intro: is_F_or_G.intros)
+
+inductive is_FGH
+where
+ "is_F_or_G x ==> is_FGH x"
+| "is_FGH H"
+
+text {* Compilation of is_FGH requires elimination rule for is_F_or_G *}
+
+code_pred is_FGH
+proof -
+ case is_F_or_G
+ from this(1) show thesis
+ proof
+ fix x
+ assume x: "a1 = x"
+ assume "x = F \<or> x = G"
+ from this show thesis
+ proof
+ assume "x = F"
+ from this x is_F_or_G(2) show thesis by simp
+ next
+ assume "x = G"
+ from this x is_F_or_G(3) show thesis by simp
+ qed
+ qed
+qed
subsection {* Preprocessor Inlining *}
@@ -175,7 +255,16 @@
code_pred append2
proof -
case append2
- from append2.cases[OF append2(1)] append2(2-3) show thesis by blast
+ from append2(1) show thesis
+ proof
+ fix xs
+ assume "a1 = []" "a2 = xs" "a3 = xs"
+ from this append2(2) show thesis by simp
+ next
+ fix xs ys zs x
+ assume "a1 = x # xs" "a2 = ys" "a3 = x # zs" "append2 xs ys zs"
+ from this append2(3) show thesis by fastsimp
+ qed
qed
inductive tupled_append :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
@@ -658,6 +747,8 @@
| "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
| "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
+code_pred (mode: [], [1]) S\<^isub>4p .
+
subsection {* Lambda *}
datatype type =
@@ -708,4 +799,10 @@
| appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t"
| abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs T s \<rightarrow>\<^sub>\<beta> Abs T t"
+code_pred (mode: [1, 2], [1, 2, 3]) typing .
+thm typing.equation
+
+code_pred (mode: [1], [1, 2]) beta .
+thm beta.equation
+
end
\ No newline at end of file