# HG changeset patch # User bulwahn # Date 1256729340 -3600 # Node ID 7d0288d90535fe2cd9fb18e8dda13954c96a2363 # Parent 02de0317f66fb7509c0e48b5c99f4175a3ed9df6 improved handling of alternative rules; added test cases for alternative rules; normalized tracing in the predicate compiler diff -r 02de0317f66f -r 7d0288d90535 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- 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 diff -r 02de0317f66f -r 7d0288d90535 src/HOL/ex/Predicate_Compile_Alternative_Defs.thy --- 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 diff -r 02de0317f66f -r 7d0288d90535 src/HOL/ex/Predicate_Compile_ex.thy --- 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 \ bool" where "EmptySet' = {}" -code_pred (mode: [], [1]) [inductify, show_intermediate_results] EmptySet' . +code_pred (mode: [], [1]) [inductify] EmptySet' . inductive EmptyRel :: "'a \ 'b \ 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) \ (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) \ (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 \ 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 \ 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 \ 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 \ 'a list \ 'a list \ bool" @@ -658,6 +747,8 @@ | "w \ S\<^isub>4 \ b # w \ B\<^isub>4" | "\v \ B\<^isub>4; w \ B\<^isub>4\ \ a # v @ w \ B\<^isub>4" +code_pred (mode: [], [1]) S\<^isub>4p . + subsection {* Lambda *} datatype type = @@ -708,4 +799,10 @@ | appR [simp, intro!]: "s \\<^sub>\ t ==> u \ s \\<^sub>\ u \ t" | abs [simp, intro!]: "s \\<^sub>\ t ==> Abs T s \\<^sub>\ 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