--- a/doc-src/Codegen/Thy/Program.thy Wed Apr 21 11:23:04 2010 +0200
+++ b/doc-src/Codegen/Thy/Program.thy Wed Apr 21 12:11:48 2010 +0200
@@ -571,21 +571,20 @@
code_pred %quote lexord
(*<*)
proof -
- fix r a1
- assume lexord: "lexord r a1"
- assume 1: "\<And> xs ys a v. a1 = (xs, ys) \<Longrightarrow> append xs (a # v) ys \<Longrightarrow> thesis"
- assume 2: "\<And> xs ys u a v b w. a1 = (xs, ys) \<Longrightarrow> append u (a # v) xs \<Longrightarrow> append u (b # w) ys \<Longrightarrow> r (a, b) \<Longrightarrow> thesis"
- obtain xs ys where a1: "a1 = (xs, ys)" by fastsimp
+ fix r xs ys
+ assume lexord: "lexord r (xs, ys)"
+ assume 1: "\<And> r' xs' ys' a v. r = r' \<Longrightarrow> (xs, ys) = (xs', ys') \<Longrightarrow> append xs' (a # v) ys' \<Longrightarrow> thesis"
+ assume 2: "\<And> r' xs' ys' u a v b w. r = r' \<Longrightarrow> (xs, ys) = (xs', ys') \<Longrightarrow> append u (a # v) xs' \<Longrightarrow> append u (b # w) ys' \<Longrightarrow> r' (a, b) \<Longrightarrow> thesis"
{
assume "\<exists>a v. ys = xs @ a # v"
- from this 1 a1 have thesis
+ from this 1 have thesis
by (fastsimp simp add: append)
} moreover
{
assume "\<exists>u a b v w. (a, b) \<in> r \<and> xs = u @ a # v \<and> ys = u @ b # w"
- from this 2 a1 have thesis by (fastsimp simp add: append mem_def)
+ from this 2 have thesis by (fastsimp simp add: append mem_def)
} moreover
- note lexord[simplified a1]
+ note lexord
ultimately show thesis
unfolding lexord_def
by (fastsimp simp add: Collect_def)
--- a/src/HOL/HOL.thy Wed Apr 21 11:23:04 2010 +0200
+++ b/src/HOL/HOL.thy Wed Apr 21 12:11:48 2010 +0200
@@ -2061,19 +2061,22 @@
val name = "code_pred_def"
val description = "alternative definitions of constants for the Predicate Compiler"
)
-*}
-
-ML {*
structure Predicate_Compile_Inline_Defs = Named_Thms
(
val name = "code_pred_inline"
val description = "inlining definitions for the Predicate Compiler"
)
+structure Predicate_Compile_Simps = Named_Thms
+(
+ val name = "code_pred_simp"
+ val description = "simplification rules for the optimisations in the Predicate Compiler"
+)
*}
setup {*
Predicate_Compile_Alternative_Defs.setup
#> Predicate_Compile_Inline_Defs.setup
+ #> Predicate_Compile_Simps.setup
*}
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Wed Apr 21 11:23:04 2010 +0200
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Wed Apr 21 12:11:48 2010 +0200
@@ -6,6 +6,14 @@
declare HOL.if_bool_eq_disj[code_pred_inline]
+declare bool_diff_def[code_pred_inline]
+declare inf_bool_eq_raw[code_pred_inline]
+declare less_bool_def_raw[code_pred_inline]
+declare le_bool_def_raw[code_pred_inline]
+
+lemma min_bool_eq [code_pred_inline]: "(min :: bool => bool => bool) == (op &)"
+by (rule eq_reflection) (auto simp add: expand_fun_eq min_def le_bool_def)
+
setup {* Predicate_Compile_Data.ignore_consts [@{const_name Let}] *}
section {* Pairs *}
@@ -35,6 +43,10 @@
"(A - B) = (%x. A x \<and> \<not> B x)"
by (auto simp add: mem_def)
+lemma subset_eq[code_pred_inline]:
+ "(P :: 'a => bool) < (Q :: 'a => bool) == ((\<exists>x. Q x \<and> (\<not> P x)) \<and> (\<forall> x. P x --> Q x))"
+by (rule eq_reflection) (fastsimp simp add: mem_def)
+
lemma set_equality[code_pred_inline]:
"(A = B) = ((\<forall>x. A x \<longrightarrow> B x) \<and> (\<forall>x. B x \<longrightarrow> A x))"
by (fastsimp simp add: mem_def)
@@ -141,7 +153,7 @@
"less_nat 0 (Suc y)"
| "less_nat x y ==> less_nat (Suc x) (Suc y)"
-lemma [code_pred_inline]:
+lemma less_nat[code_pred_inline]:
"x < y = less_nat x y"
apply (rule iffI)
apply (induct x arbitrary: y)
@@ -228,6 +240,16 @@
done
qed
+section {* Simplification rules for optimisation *}
+
+lemma [code_pred_simp]: "\<not> False == True"
+by auto
+
+lemma [code_pred_simp]: "\<not> True == False"
+by auto
+
+lemma less_nat_k_0 [code_pred_simp]: "less_nat k 0 == False"
+unfolding less_nat[symmetric] by auto
end
\ No newline at end of file
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Wed Apr 21 11:23:04 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Wed Apr 21 12:11:48 2010 +0200
@@ -49,8 +49,8 @@
val max_mutants = 4
val num_mutations = 1
(* soundness check: *)
-val max_mutants = 1
-val num_mutations = 0
+(*val max_mutants = 1
+val num_mutations = 0*)
(* quickcheck options *)
(*val quickcheck_generator = "SML"*)
@@ -197,7 +197,14 @@
(@{const_name induct_conj}, "'a"),*)
(@{const_name "undefined"}, "'a"),
(@{const_name "default"}, "'a"),
- (@{const_name "dummy_pattern"}, "'a::{}") (*,
+ (@{const_name "dummy_pattern"}, "'a::{}"),
+ (@{const_name "HOL.simp_implies"}, "prop => prop => prop"),
+ (@{const_name "bot_fun_inst.bot_fun"}, "'a"),
+ (@{const_name "top_fun_inst.top_fun"}, "'a"),
+ (@{const_name "Pure.term"}, "'a"),
+ (@{const_name "top_class.top"}, "'a"),
+ (@{const_name "eq_class.eq"}, "'a"),
+ (@{const_name "Quotient.Quot_True"}, "'a")(*,
(@{const_name "uminus"}, "'a"),
(@{const_name "Nat.size"}, "'a"),
(@{const_name "Groups.abs"}, "'a") *)]
@@ -219,10 +226,28 @@
String.isSuffix "_raw" s
end
+val forbidden_mutant_constnames =
+ ["HOL.induct_equal",
+ "HOL.induct_implies",
+ "HOL.induct_conj",
+ @{const_name undefined},
+ @{const_name default},
+ @{const_name dummy_pattern},
+ @{const_name "HOL.simp_implies"},
+ @{const_name "bot_fun_inst.bot_fun"},
+ @{const_name "top_fun_inst.top_fun"},
+ @{const_name "Pure.term"},
+ @{const_name "top_class.top"},
+ @{const_name "eq_class.eq"},
+ @{const_name "Quotient.Quot_True"}]
+
fun is_forbidden_mutant t =
- let val consts = Term.add_const_names t [] in
+ let
+ val consts = Term.add_const_names t []
+ in
exists (String.isPrefix "Nitpick") consts orelse
- exists (String.isSubstring "_sumC") consts (* internal function *)
+ exists (String.isSubstring "_sumC") consts orelse
+ exists (member (op =) forbidden_mutant_constnames) consts
end
fun is_executable_term thy t = can (TimeLimit.timeLimit (Time.fromMilliseconds 2000) (Quickcheck.test_term
@@ -340,6 +365,12 @@
(map (fn (mtd_name, (outcome, timing)) => mtd_name ^ ": " ^ string_of_outcome outcome) results) ^
"\n"
+(* XML.tree -> string *)
+fun plain_string_from_xml_tree t =
+ Buffer.empty |> XML.add_content t |> Buffer.content
+(* string -> string *)
+val unyxml = plain_string_from_xml_tree o YXML.parse
+
fun string_of_mutant_subentry' thy thm_name (t, results) =
let
fun string_of_report (Quickcheck.Report {iterations = i, raised_match_errors = e,
@@ -352,16 +383,28 @@
fun string_of_mtd_result (mtd_name, (outcome, (timing, reports))) =
mtd_name ^ ": " ^ string_of_outcome outcome ^ "; " ^
space_implode "; " (map (fn (s, t) => (s ^ ": " ^ string_of_int t)) timing)
- ^ "\n" ^ string_of_reports reports
+ (*^ "\n" ^ string_of_reports reports*)
in
- "mutant of " ^ thm_name ^ ":\n" ^ cat_lines (map string_of_mtd_result results)
+ "mutant of " ^ thm_name ^ ":\n"
+ ^ unyxml (Syntax.string_of_term_global thy t) ^ "\n" ^ cat_lines (map string_of_mtd_result results)
end
fun string_of_detailed_entry thy (thm_name, exec, t, mutant_subentries) =
thm_name ^ " " ^ (if exec then "[exe]" else "[noexe]") ^ ": " ^
- Syntax.string_of_term_global thy t ^ "\n" ^
+ Syntax.string_of_term_global thy t ^ "\n" ^
cat_lines (map (string_of_mutant_subentry' thy thm_name) mutant_subentries) ^ "\n"
+fun theoryfile_string_of_mutant_subentry thy thm_name (i, (t, results)) =
+ "lemma " ^ thm_name ^ "_" ^ string_of_int (i + 1) ^ ":\n" ^
+ "\"" ^ unyxml (Syntax.string_of_term_global thy t) ^
+ "\" \nquickcheck[generator = SML]\nquickcheck[generator = predicate_compile_wo_ff]\n" ^
+ "quickcheck[generator = predicate_compile_ff_nofs]\noops\n"
+
+fun theoryfile_string_of_detailed_entry thy (thm_name, exec, t, mutant_subentries) =
+ "subsubsection {* mutants of " ^ thm_name ^ " *}\n\n" ^
+ cat_lines (map_index
+ (theoryfile_string_of_mutant_subentry thy thm_name) mutant_subentries) ^ "\n"
+
(* subentry -> string *)
fun string_for_subentry (mtd_name, genuine_cex, potential_cex, no_cex, donno,
timeout, error) =
@@ -390,6 +433,8 @@
(*for detailled report: *)
val (gen_create_entry, gen_string_for_entry) =
(create_detailed_entry, string_of_detailed_entry thy)
+ val (gen_create_entry, gen_string_for_entry) =
+ (create_detailed_entry, theoryfile_string_of_detailed_entry thy)
in
File.write path (
"Mutation options = " ^
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Wed Apr 21 11:23:04 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Wed Apr 21 12:11:48 2010 +0200
@@ -789,7 +789,6 @@
code_pred [inductify, skip_proof] case_f .
thm case_fP.equation
-thm case_fP.intros
fun fold_map_idx where
"fold_map_idx f i y [] = (y, [])"
@@ -935,10 +934,10 @@
code_pred [inductify] avl .
thm avl.equation*)
-code_pred [random_dseq inductify] avl .
-thm avl.random_dseq_equation
+code_pred [new_random_dseq inductify] avl .
+thm avl.new_random_dseq_equation
-values [random_dseq 2, 1, 7] 5 "{t:: int tree. avl t}"
+values [new_random_dseq 2, 1, 7] 5 "{t:: int tree. avl t}"
fun set_of
where
@@ -1392,6 +1391,100 @@
values [expected "{9::int}"] "{a. minus_int_test a 4 5}"
values [expected "{- 1::int}"] "{b. minus_int_test 4 b 5}"
+subsection {* minus on bool *}
+
+inductive All :: "nat => bool"
+where
+ "All x"
+
+inductive None :: "nat => bool"
+
+definition "test_minus_bool x = (None x - All x)"
+
+code_pred [inductify] test_minus_bool .
+thm test_minus_bool.equation
+
+values "{x. test_minus_bool x}"
+
+subsection {* Examples for detecting switches *}
+
+inductive detect_switches1 where
+ "detect_switches1 [] []"
+| "detect_switches1 (x # xs) (y # ys)"
+
+code_pred [detect_switches, skip_proof] detect_switches1 .
+
+thm detect_switches1.equation
+
+inductive detect_switches2 :: "('a => bool) => bool"
+where
+ "detect_switches2 P"
+
+code_pred [detect_switches, skip_proof] detect_switches2 .
+thm detect_switches2.equation
+
+inductive detect_switches3 :: "('a => bool) => 'a list => bool"
+where
+ "detect_switches3 P []"
+| "detect_switches3 P (x # xs)"
+
+code_pred [detect_switches, skip_proof] detect_switches3 .
+
+thm detect_switches3.equation
+
+inductive detect_switches4 :: "('a => bool) => 'a list => 'a list => bool"
+where
+ "detect_switches4 P [] []"
+| "detect_switches4 P (x # xs) (y # ys)"
+
+code_pred [detect_switches, skip_proof] detect_switches4 .
+thm detect_switches4.equation
+
+inductive detect_switches5 :: "('a => 'a => bool) => 'a list => 'a list => bool"
+where
+ "detect_switches5 P [] []"
+| "detect_switches5 P xs ys ==> P x y ==> detect_switches5 P (x # xs) (y # ys)"
+
+code_pred [detect_switches, skip_proof] detect_switches5 .
+
+thm detect_switches5.equation
+
+inductive detect_switches6 :: "(('a => 'b => bool) * 'a list * 'b list) => bool"
+where
+ "detect_switches6 (P, [], [])"
+| "detect_switches6 (P, xs, ys) ==> P x y ==> detect_switches6 (P, x # xs, y # ys)"
+
+code_pred [detect_switches, skip_proof] detect_switches6 .
+
+inductive detect_switches7 :: "('a => bool) => ('b => bool) => ('a * 'b list) => bool"
+where
+ "detect_switches7 P Q (a, [])"
+| "P a ==> Q x ==> detect_switches7 P Q (a, x#xs)"
+
+code_pred [skip_proof] detect_switches7 .
+
+thm detect_switches7.equation
+
+inductive detect_switches8 :: "nat => bool"
+where
+ "detect_switches8 0"
+| "x mod 2 = 0 ==> detect_switches8 (Suc x)"
+
+code_pred [detect_switches, skip_proof] detect_switches8 .
+
+thm detect_switches8.equation
+
+inductive detect_switches9 :: "nat => nat => bool"
+where
+ "detect_switches9 0 0"
+| "detect_switches9 0 (Suc x)"
+| "detect_switches9 (Suc x) 0"
+| "x = y ==> detect_switches9 (Suc x) (Suc y)"
+| "c1 = c2 ==> detect_switches9 c1 c2"
+
+code_pred [detect_switches, skip_proof] detect_switches9 .
+
+thm detect_switches9.equation
--- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy Wed Apr 21 11:23:04 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy Wed Apr 21 12:11:48 2010 +0200
@@ -12,7 +12,7 @@
definition
"greater_than_index xs = (\<forall>i x. nth_el' xs i = Some x --> x > i)"
-code_pred (expected_modes: i => bool) [inductify] greater_than_index .
+code_pred (expected_modes: i => bool) [inductify, skip_proof, specialise] greater_than_index .
ML {* Predicate_Compile_Core.intros_of @{theory} @{const_name specialised_nth_el'P} *}
thm greater_than_index.equation
@@ -38,7 +38,7 @@
text {* In this example, max is specialised, hence the mode o => i => bool is possible *}
-code_pred (modes: o => i => bool) [inductify] max_of_my_Suc .
+code_pred (modes: o => i => bool) [inductify, specialise, skip_proof] max_of_my_Suc .
thm max_of_my_SucP.equation
@@ -218,7 +218,7 @@
\<Gamma> \<turnstile> t\<^isub>1 \<bullet>\<^isub>\<tau> T\<^isub>2 : T\<^isub>1\<^isub>2[0 \<mapsto>\<^isub>\<tau> T\<^isub>2]\<^isub>\<tau>"
| T_Sub: "\<Gamma> \<turnstile> t : S \<Longrightarrow> \<Gamma> \<turnstile> S <: T \<Longrightarrow> \<Gamma> \<turnstile> t : T"
-code_pred [inductify, skip_proof] typing .
+code_pred [inductify, skip_proof, specialise] typing .
thm typing.equation
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Wed Apr 21 11:23:04 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Wed Apr 21 12:11:48 2010 +0200
@@ -18,17 +18,9 @@
val present_graph = Unsynchronized.ref false
val intro_hook = Unsynchronized.ref NONE : (theory -> thm -> unit) option Unsynchronized.ref
-
open Predicate_Compile_Aux;
-(* Some last processing *)
-
-fun remove_pointless_clauses intro =
- if Logic.strip_imp_prems (prop_of intro) = [@{prop "False"}] then
- []
- else [intro]
-
fun print_intross options thy msg intross =
if show_intermediate_results options then
tracing (msg ^
@@ -120,10 +112,15 @@
val intross8 = map_specs (map (eta_contract_ho_arguments thy2)) intross7
val _ = case !intro_hook of NONE => () | SOME f => (map_specs (map (f thy2)) intross8; ())
val _ = print_step options ("Looking for specialisations in " ^ commas (map fst intross8) ^ "...")
- val (intross9, thy3) = Predicate_Compile_Specialisation.find_specialisations [] intross8 thy2
- val _ = print_intross options thy3 "introduction rules before registering: " intross9
+ val (intross9, thy3) =
+ if specialise options then
+ Predicate_Compile_Specialisation.find_specialisations [] intross8 thy2
+ else (intross8, thy2)
+ val _ = print_intross options thy3 "introduction rules after specialisations: " intross9
+ val intross10 = map_specs (map_filter (peephole_optimisation thy3)) intross9
+ val _ = print_intross options thy3 "introduction rules before registering: " intross10
val _ = print_step options "Registering introduction rules..."
- val thy4 = fold Predicate_Compile_Core.register_intros intross9 thy3
+ val thy4 = fold Predicate_Compile_Core.register_intros intross10 thy3
in
thy4
end;
@@ -160,10 +157,12 @@
show_caught_failures = false,
skip_proof = chk "skip_proof",
function_flattening = not (chk "no_function_flattening"),
+ specialise = chk "specialise",
fail_safe_function_flattening = false,
no_topmost_reordering = (chk "no_topmost_reordering"),
no_higher_order_predicate = [],
inductify = chk "inductify",
+ detect_switches = chk "detect_switches",
compilation = compilation
}
end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Apr 21 11:23:04 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Apr 21 12:11:48 2010 +0200
@@ -38,6 +38,8 @@
(* premises *)
datatype indprem = Prem of term | Negprem of term | Sidecond of term
| Generator of (string * typ)
+ val dest_indprem : indprem -> term
+ val map_indprem : (term -> term) -> indprem -> indprem
(* general syntactic functions *)
val conjuncts : term -> term list
val is_equationlike : thm -> bool
@@ -107,8 +109,10 @@
no_topmost_reordering : bool,
function_flattening : bool,
fail_safe_function_flattening : bool,
+ specialise : bool,
no_higher_order_predicate : string list,
inductify : bool,
+ detect_switches : bool,
compilation : compilation
};
val expected_modes : options -> (string * mode list) option
@@ -125,8 +129,10 @@
val no_topmost_reordering : options -> bool
val function_flattening : options -> bool
val fail_safe_function_flattening : options -> bool
+ val specialise : options -> bool
val no_higher_order_predicate : options -> string list
val is_inductify : options -> bool
+ val detect_switches : options -> bool
val compilation : options -> compilation
val default_options : options
val bool_options : string list
@@ -135,6 +141,8 @@
val expand_tuples : theory -> thm -> thm
val eta_contract_ho_arguments : theory -> thm -> thm
val remove_equalities : theory -> thm -> thm
+ val remove_pointless_clauses : thm -> thm list
+ val peephole_optimisation : theory -> thm -> thm option
end;
structure Predicate_Compile_Aux : PREDICATE_COMPILE_AUX =
@@ -384,6 +392,16 @@
datatype indprem = Prem of term | Negprem of term | Sidecond of term
| Generator of (string * typ);
+fun dest_indprem (Prem t) = t
+ | dest_indprem (Negprem t) = t
+ | dest_indprem (Sidecond t) = t
+ | dest_indprem (Generator _) = raise Fail "cannot destruct generator"
+
+fun map_indprem f (Prem t) = Prem (f t)
+ | map_indprem f (Negprem t) = Negprem (f t)
+ | map_indprem f (Sidecond t) = Sidecond (f t)
+ | map_indprem f (Generator (v, T)) = Generator (dest_Free (f (Free (v, T))))
+
(* general syntactic functions *)
(*Like dest_conj, but flattens conjunctions however nested*)
@@ -513,6 +531,20 @@
(Logic.list_implies (map HOLogic.mk_Trueprop literals', head), s')
end;
+fun map_premises f intro =
+ let
+ val (premises, head) = Logic.strip_horn intro
+ in
+ Logic.list_implies (map f premises, head)
+ end
+
+fun map_filter_premises f intro =
+ let
+ val (premises, head) = Logic.strip_horn intro
+ in
+ Logic.list_implies (map_filter f premises, head)
+ end
+
fun maps_premises f intro =
let
val (premises, head) = Logic.strip_horn intro
@@ -649,9 +681,11 @@
skip_proof : bool,
no_topmost_reordering : bool,
function_flattening : bool,
+ specialise : bool,
fail_safe_function_flattening : bool,
no_higher_order_predicate : string list,
inductify : bool,
+ detect_switches : bool,
compilation : compilation
};
@@ -672,6 +706,7 @@
fun function_flattening (Options opt) = #function_flattening opt
fun fail_safe_function_flattening (Options opt) = #fail_safe_function_flattening opt
+fun specialise (Options opt) = #specialise opt
fun no_topmost_reordering (Options opt) = #no_topmost_reordering opt
fun no_higher_order_predicate (Options opt) = #no_higher_order_predicate opt
@@ -679,6 +714,8 @@
fun compilation (Options opt) = #compilation opt
+fun detect_switches (Options opt) = #detect_switches opt
+
val default_options = Options {
expected_modes = NONE,
proposed_modes = NONE,
@@ -693,15 +730,17 @@
skip_proof = true,
no_topmost_reordering = false,
function_flattening = false,
+ specialise = false,
fail_safe_function_flattening = false,
no_higher_order_predicate = [],
inductify = false,
+ detect_switches = true,
compilation = Pred
}
val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", "show_modes",
"show_mode_inference", "show_compilation", "skip_proof", "inductify", "no_function_flattening",
- "no_topmost_reordering"]
+ "detect_switches", "specialise", "no_topmost_reordering"]
fun print_step options s =
if show_steps options then tracing s else ()
@@ -810,4 +849,25 @@
map_term thy remove_eqs intro
end
+(* Some last processing *)
+
+fun remove_pointless_clauses intro =
+ if Logic.strip_imp_prems (prop_of intro) = [@{prop "False"}] then
+ []
+ else [intro]
+
+(* some peephole optimisations *)
+
+fun peephole_optimisation thy intro =
+ let
+ val process = MetaSimplifier.rewrite_rule (Predicate_Compile_Simps.get (ProofContext.init thy))
+ fun process_False intro_t =
+ if member (op =) (Logic.strip_imp_prems intro_t) @{prop "False"} then NONE else SOME intro_t
+ fun process_True intro_t =
+ map_filter_premises (fn p => if p = @{prop True} then NONE else SOME p) intro_t
+ in
+ Option.map (Skip_Proof.make_thm thy)
+ (process_False (process_True (prop_of (process intro))))
+ end
+
end;
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Apr 21 11:23:04 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Apr 21 12:11:48 2010 +0200
@@ -1251,10 +1251,6 @@
| rev_option_ord ord (SOME _, NONE) = LESS
| rev_option_ord ord (SOME x, SOME y) = ord (x, y)
-fun term_of_prem (Prem t) = t
- | term_of_prem (Negprem t) = t
- | term_of_prem (Sidecond t) = t
-
fun random_mode_in_deriv modes t deriv =
case try dest_Const (fst (strip_comb t)) of
SOME (s, _) =>
@@ -1282,8 +1278,28 @@
EQUAL => ord2 (x, x')
| ord => ord
-fun deriv_ord2' thy pred modes t1 t2 ((deriv1, mvars1), (deriv2, mvars2)) =
+fun lexl_ord [] (x, x') = EQUAL
+ | lexl_ord (ord :: ords') (x, x') =
+ case ord (x, x') of
+ EQUAL => lexl_ord ords' (x, x')
+ | ord => ord
+
+fun deriv_ord' thy pol pred modes t1 t2 ((deriv1, mvars1), (deriv2, mvars2)) =
let
+ (* prefer functional modes if it is a function *)
+ fun fun_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
+ let
+ fun is_functional t mode =
+ case try (fst o dest_Const o fst o strip_comb) t of
+ NONE => false
+ | SOME c => is_some (alternative_compilation_of thy c mode)
+ in
+ case (is_functional t1 (head_mode_of deriv1), is_functional t2 (head_mode_of deriv2)) of
+ (true, true) => EQUAL
+ | (true, false) => LESS
+ | (false, true) => GREATER
+ | (false, false) => EQUAL
+ end
(* prefer modes without requirement for generating random values *)
fun mvars_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
int_ord (length mvars1, length mvars2)
@@ -1301,18 +1317,15 @@
fun recursive_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
int_ord (if is_rec_premise t1 then 0 else 1,
if is_rec_premise t2 then 0 else 1)
- val ord = lex_ord mvars_ord (lex_ord random_mode_ord (lex_ord output_mode_ord recursive_ord))
+ val ord = lexl_ord [mvars_ord, fun_ord, random_mode_ord, output_mode_ord, recursive_ord]
in
ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2))
end
-fun deriv_ord2 thy pred modes t = deriv_ord2' thy pred modes t t
+fun deriv_ord thy pol pred modes t = deriv_ord' thy pol pred modes t t
-fun deriv_ord ((deriv1, mvars1), (deriv2, mvars2)) =
- int_ord (length mvars1, length mvars2)
-
-fun premise_ord thy pred modes ((prem1, a1), (prem2, a2)) =
- rev_option_ord (deriv_ord2' thy pred modes (term_of_prem prem1) (term_of_prem prem2)) (a1, a2)
+fun premise_ord thy pol pred modes ((prem1, a1), (prem2, a2)) =
+ rev_option_ord (deriv_ord' thy pol pred modes (dest_indprem prem1) (dest_indprem prem2)) (a1, a2)
fun print_mode_list modes =
tracing ("modes: " ^ (commas (map (fn (s, ms) => s ^ ": " ^
@@ -1322,15 +1335,16 @@
pol (modes, (pos_modes, neg_modes)) vs ps =
let
fun choose_mode_of_prem (Prem t) = partial_hd
- (sort (deriv_ord2 thy pred modes t) (all_derivations_of thy pos_modes vs t))
+ (sort (deriv_ord thy pol pred modes t) (all_derivations_of thy pos_modes vs t))
| choose_mode_of_prem (Sidecond t) = SOME (Context Bool, missing_vars vs t)
| choose_mode_of_prem (Negprem t) = partial_hd
- (sort (deriv_ord2 thy pred modes t) (filter (fn (d, missing_vars) => is_all_input (head_mode_of d))
+ (sort (deriv_ord thy (not pol) pred modes t)
+ (filter (fn (d, missing_vars) => is_all_input (head_mode_of d))
(all_derivations_of thy neg_modes vs t)))
| choose_mode_of_prem p = raise Fail ("choose_mode_of_prem: " ^ string_of_prem thy p)
in
if #reorder_premises mode_analysis_options then
- partial_hd (sort (premise_ord thy pred modes) (ps ~~ map choose_mode_of_prem ps))
+ partial_hd (sort (premise_ord thy pol pred modes) (ps ~~ map choose_mode_of_prem ps))
else
SOME (hd ps, choose_mode_of_prem (hd ps))
end
@@ -1338,7 +1352,7 @@
fun check_mode_clause' (mode_analysis_options : mode_analysis_options) thy pred param_vs (modes :
(string * ((bool * mode) * bool) list) list) ((pol, mode) : bool * mode) (ts, ps) =
let
- val vTs = distinct (op =) (fold Term.add_frees (map term_of_prem ps) (fold Term.add_frees ts []))
+ val vTs = distinct (op =) (fold Term.add_frees (map dest_indprem ps) (fold Term.add_frees ts []))
val modes' = modes @ (param_vs ~~ map (fn x => [((true, x), false), ((false, x), false)]) (ho_arg_modes_of mode))
fun retrieve_modes_of_pol pol = map (fn (s, ms) =>
(s, map_filter (fn ((p, m), r) => if p = pol then SOME m else NONE | _ => NONE) ms))
@@ -1464,13 +1478,26 @@
val prednames = map fst preds
(* extramodes contains all modes of all constants, should we only use the necessary ones
- what is the impact on performance? *)
+ fun predname_of (Prem t) =
+ (case try dest_Const (fst (strip_comb t)) of SOME (c, _) => insert (op =) c | NONE => I)
+ | predname_of (Negprem t) =
+ (case try dest_Const (fst (strip_comb t)) of SOME (c, _) => insert (op =) c | NONE => I)
+ | predname_of _ = I
+ val relevant_prednames = fold (fn (_, clauses') =>
+ fold (fn (_, ps) => fold Term.add_const_names (map dest_indprem ps)) clauses') clauses []
val extra_modes =
if #infer_pos_and_neg_modes mode_analysis_options then
let
val pos_extra_modes =
- all_modes_of compilation thy |> filter_out (fn (name, _) => member (op =) prednames name)
+ map_filter (fn name => Option.map (pair name) (try (modes_of compilation thy) name))
+ relevant_prednames
+ (* all_modes_of compilation thy *)
+ |> filter_out (fn (name, _) => member (op =) prednames name)
val neg_extra_modes =
- all_modes_of (negative_compilation_of compilation) thy
+ map_filter (fn name => Option.map (pair name)
+ (try (modes_of (negative_compilation_of compilation) thy) name))
+ relevant_prednames
+ (*all_modes_of (negative_compilation_of compilation) thy*)
|> filter_out (fn (name, _) => member (op =) prednames name)
in
map (fn (s, ms) => (s, (add_polarity_and_random_bit s true ms)
@@ -1479,7 +1506,10 @@
end
else
map (fn (s, ms) => (s, (add_polarity_and_random_bit s true ms)))
- (all_modes_of compilation thy |> filter_out (fn (name, _) => member (op =) prednames name))
+ (map_filter (fn name => Option.map (pair name) (try (modes_of compilation thy) name))
+ relevant_prednames
+ (*all_modes_of compilation thy*)
+ |> filter_out (fn (name, _) => member (op =) prednames name))
val _ = print_extra_modes options extra_modes
val start_modes =
if #infer_pos_and_neg_modes mode_analysis_options then
@@ -1504,7 +1534,6 @@
val thy' = fold (fn (s, ms) => if member (op =) (map fst preds) s then
set_needs_random s (map_filter (fn ((true, m), true) => SOME m | _ => NONE) ms) else I)
modes thy
-
in
((moded_clauses, errors), thy')
end;
@@ -1608,7 +1637,7 @@
val name' = Name.variant (name :: names) "y";
val T = HOLogic.mk_tupleT (map fastype_of out_ts);
val U = fastype_of success_t;
- val U' = dest_predT compfuns U;
+ val U' = dest_predT compfuns U;
val v = Free (name, T);
val v' = Free (name', T);
in
@@ -1668,13 +1697,12 @@
end
fun compile_clause compilation_modifiers ctxt all_vs param_vs additional_arguments
- mode inp (ts, moded_ps) =
+ mode inp (in_ts, out_ts) moded_ps =
let
val compfuns = Comp_Mod.compfuns compilation_modifiers
- val iss = ho_arg_modes_of mode
+ val iss = ho_arg_modes_of mode (* FIXME! *)
val compile_match = compile_match compilation_modifiers
additional_arguments param_vs iss ctxt
- val (in_ts, out_ts) = split_mode mode ts;
val (in_ts', (all_vs', eqs)) =
fold_map (collect_non_invertible_subterms ctxt) in_ts (all_vs, []);
fun compile_prems out_ts' vs names [] =
@@ -1742,7 +1770,171 @@
mk_bind compfuns (mk_single compfuns inp, prem_t)
end
-fun compile_pred compilation_modifiers thy all_vs param_vs s T (pol, mode) moded_cls =
+(* switch detection *)
+
+(** argument position of an inductive predicates and the executable functions **)
+
+type position = int * int list
+
+fun input_positions_pair Input = [[]]
+ | input_positions_pair Output = []
+ | input_positions_pair (Fun _) = []
+ | input_positions_pair (Pair (m1, m2)) =
+ map (cons 1) (input_positions_pair m1) @ map (cons 2) (input_positions_pair m2)
+
+fun input_positions_of_mode mode = flat (map_index
+ (fn (i, Input) => [(i, [])]
+ | (_, Output) => []
+ | (_, Fun _) => []
+ | (i, m as Pair (m1, m2)) => map (pair i) (input_positions_pair m))
+ (Predicate_Compile_Aux.strip_fun_mode mode))
+
+fun argument_position_pair mode [] = []
+ | argument_position_pair (Pair (Fun _, m2)) (2 :: is) = argument_position_pair m2 is
+ | argument_position_pair (Pair (m1, m2)) (i :: is) =
+ (if eq_mode (m1, Output) andalso i = 2 then
+ argument_position_pair m2 is
+ else if eq_mode (m2, Output) andalso i = 1 then
+ argument_position_pair m1 is
+ else (i :: argument_position_pair (if i = 1 then m1 else m2) is))
+
+fun argument_position_of mode (i, is) =
+ (i - (length (filter (fn Output => true | Fun _ => true | _ => false)
+ (List.take (strip_fun_mode mode, i)))),
+ argument_position_pair (nth (strip_fun_mode mode) i) is)
+
+fun nth_pair [] t = t
+ | nth_pair (1 :: is) (Const (@{const_name Pair}, _) $ t1 $ _) = nth_pair is t1
+ | nth_pair (2 :: is) (Const (@{const_name Pair}, _) $ _ $ t2) = nth_pair is t2
+ | nth_pair _ _ = raise Fail "unexpected input for nth_tuple"
+
+(** switch detection analysis **)
+
+fun find_switch_test thy (i, is) (ts, prems) =
+ let
+ val t = nth_pair is (nth ts i)
+ val T = fastype_of t
+ in
+ case T of
+ TFree _ => NONE
+ | Type (Tcon, _) =>
+ (case Datatype_Data.get_constrs thy Tcon of
+ NONE => NONE
+ | SOME cs =>
+ (case strip_comb t of
+ (Var _, []) => NONE
+ | (Free _, []) => NONE
+ | (Const (c, T), _) => if AList.defined (op =) cs c then SOME (c, T) else NONE))
+ end
+
+fun partition_clause thy pos moded_clauses =
+ let
+ fun insert_list eq (key, value) = AList.map_default eq (key, []) (cons value)
+ fun find_switch_test' moded_clause (cases, left) =
+ case find_switch_test thy pos moded_clause of
+ SOME (c, T) => (insert_list (op =) ((c, T), moded_clause) cases, left)
+ | NONE => (cases, moded_clause :: left)
+ in
+ fold find_switch_test' moded_clauses ([], [])
+ end
+
+datatype switch_tree =
+ Atom of moded_clause list | Node of (position * ((string * typ) * switch_tree) list) * switch_tree
+
+fun mk_switch_tree thy mode moded_clauses =
+ let
+ fun select_best_switch moded_clauses input_position best_switch =
+ let
+ val ord = option_ord (rev_order o int_ord o (pairself (length o snd o snd)))
+ val partition = partition_clause thy input_position moded_clauses
+ val switch = if (length (fst partition) > 1) then SOME (input_position, partition) else NONE
+ in
+ case ord (switch, best_switch) of LESS => best_switch
+ | EQUAL => best_switch | GREATER => switch
+ end
+ fun detect_switches moded_clauses =
+ case fold (select_best_switch moded_clauses) (input_positions_of_mode mode) NONE of
+ SOME (best_pos, (switched_on, left_clauses)) =>
+ Node ((best_pos, map (apsnd detect_switches) switched_on),
+ detect_switches left_clauses)
+ | NONE => Atom moded_clauses
+ in
+ detect_switches moded_clauses
+ end
+
+(** compilation of detected switches **)
+
+fun destruct_constructor_pattern (pat, obj) =
+ (case strip_comb pat of
+ (f as Free _, []) => cons (pat, obj)
+ | (Const (c, T), pat_args) =>
+ (case strip_comb obj of
+ (Const (c', T'), obj_args) =>
+ (if c = c' andalso T = T' then
+ fold destruct_constructor_pattern (pat_args ~~ obj_args)
+ else raise Fail "pattern and object mismatch")
+ | _ => raise Fail "unexpected object")
+ | _ => raise Fail "unexpected pattern")
+
+
+fun compile_switch compilation_modifiers ctxt all_vs param_vs additional_arguments mode
+ in_ts' outTs switch_tree =
+ let
+ val compfuns = Comp_Mod.compfuns compilation_modifiers
+ val thy = ProofContext.theory_of ctxt
+ fun compile_switch_tree _ _ (Atom []) = NONE
+ | compile_switch_tree all_vs ctxt_eqs (Atom moded_clauses) =
+ let
+ val in_ts' = map (Pattern.rewrite_term thy ctxt_eqs []) in_ts'
+ fun compile_clause' (ts, moded_ps) =
+ let
+ val (ts, out_ts) = split_mode mode ts
+ val subst = fold destruct_constructor_pattern (in_ts' ~~ ts) []
+ val (fsubst, pat') = List.partition (fn (_, Free _) => true | _ => false) subst
+ val moded_ps' = (map o apfst o map_indprem)
+ (Pattern.rewrite_term thy (map swap fsubst) []) moded_ps
+ val inp = HOLogic.mk_tuple (map fst pat')
+ val in_ts' = map (Pattern.rewrite_term thy (map swap fsubst) []) (map snd pat')
+ val out_ts' = map (Pattern.rewrite_term thy (map swap fsubst) []) out_ts
+ in
+ compile_clause compilation_modifiers ctxt all_vs param_vs additional_arguments
+ mode inp (in_ts', out_ts') moded_ps'
+ end
+ in SOME (foldr1 (mk_sup compfuns) (map compile_clause' moded_clauses)) end
+ | compile_switch_tree all_vs ctxt_eqs (Node ((position, switched_clauses), left_clauses)) =
+ let
+ val (i, is) = argument_position_of mode position
+ val inp_var = nth_pair is (nth in_ts' i)
+ val x = Name.variant all_vs "x"
+ val xt = Free (x, fastype_of inp_var)
+ fun compile_single_case ((c, T), switched) =
+ let
+ val Ts = binder_types T
+ val argnames = Name.variant_list (x :: all_vs)
+ (map (fn i => "c" ^ string_of_int i) (1 upto length Ts))
+ val args = map2 (curry Free) argnames Ts
+ val pattern = list_comb (Const (c, T), args)
+ val ctxt_eqs' = (inp_var, pattern) :: ctxt_eqs
+ val compilation = the_default (mk_bot compfuns (HOLogic.mk_tupleT outTs))
+ (compile_switch_tree (argnames @ x :: all_vs) ctxt_eqs' switched)
+ in
+ (pattern, compilation)
+ end
+ val switch = fst (Datatype.make_case ctxt Datatype_Case.Quiet [] inp_var
+ ((map compile_single_case switched_clauses) @
+ [(xt, mk_bot compfuns (HOLogic.mk_tupleT outTs))]))
+ in
+ case compile_switch_tree all_vs ctxt_eqs left_clauses of
+ NONE => SOME switch
+ | SOME left_comp => SOME (mk_sup compfuns (switch, left_comp))
+ end
+ in
+ compile_switch_tree all_vs [] switch_tree
+ end
+
+(* compilation of predicates *)
+
+fun compile_pred options compilation_modifiers thy all_vs param_vs s T (pol, mode) moded_cls =
let
val ctxt = ProofContext.init thy
val compilation_modifiers = if pol then compilation_modifiers else
@@ -1757,7 +1949,6 @@
(binder_types T)
val predT = mk_predT compfuns (HOLogic.mk_tupleT outTs)
val funT = Comp_Mod.funT_of compilation_modifiers mode T
-
val (in_ts, _) = fold_map (fold_map_aterms_prodT (curry HOLogic.mk_prod)
(fn T => fn (param_vs, names) =>
if is_param_type T then
@@ -1769,14 +1960,24 @@
(param_vs, (all_vs @ param_vs))
val in_ts' = map_filter (map_filter_prod
(fn t as Free (x, _) => if member (op =) param_vs x then NONE else SOME t | t => SOME t)) in_ts
- val cl_ts =
- map (compile_clause compilation_modifiers
- ctxt all_vs param_vs additional_arguments mode (HOLogic.mk_tuple in_ts')) moded_cls;
- val compilation = Comp_Mod.wrap_compilation compilation_modifiers compfuns
- s T mode additional_arguments
- (if null cl_ts then
- mk_bot compfuns (HOLogic.mk_tupleT outTs)
- else foldr1 (mk_sup compfuns) cl_ts)
+ val compilation =
+ if detect_switches options then
+ the_default (mk_bot compfuns (HOLogic.mk_tupleT outTs))
+ (compile_switch compilation_modifiers ctxt all_vs param_vs additional_arguments
+ mode in_ts' outTs (mk_switch_tree thy mode moded_cls))
+ else
+ let
+ val cl_ts =
+ map (fn (ts, moded_prems) =>
+ compile_clause compilation_modifiers ctxt all_vs param_vs additional_arguments
+ mode (HOLogic.mk_tuple in_ts') (split_mode mode ts) moded_prems) moded_cls;
+ in
+ Comp_Mod.wrap_compilation compilation_modifiers compfuns s T mode additional_arguments
+ (if null cl_ts then
+ mk_bot compfuns (HOLogic.mk_tupleT outTs)
+ else
+ foldr1 (mk_sup compfuns) cl_ts)
+ end
val fun_const =
Const (function_name_of (Comp_Mod.compilation compilation_modifiers)
(ProofContext.theory_of ctxt) s mode, funT)
@@ -1785,7 +1986,7 @@
(HOLogic.mk_eq (list_comb (fun_const, in_ts @ additional_arguments), compilation))
end;
-(* special setup for simpset *)
+(** special setup for simpset **)
val HOL_basic_ss' = HOL_basic_ss addsimps (@{thms HOL.simp_thms} @ [@{thm Pair_eq}])
setSolver (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
setSolver (mk_solver "True_solver" (fn _ => rtac @{thm TrueI}))
@@ -2426,13 +2627,13 @@
fun join_preds_modes table1 table2 =
map_preds_modes (fn pred => fn mode => fn value =>
(value, the (AList.lookup (op =) (the (AList.lookup (op =) table2 pred)) mode))) table1
-
+
fun maps_modes preds_modes_table =
map (fn (pred, modes) =>
(pred, map (fn (mode, value) => value) modes)) preds_modes_table
-
-fun compile_preds comp_modifiers thy all_vs param_vs preds moded_clauses =
- map_preds_modes (fn pred => compile_pred comp_modifiers thy all_vs param_vs pred
+
+fun compile_preds options comp_modifiers thy all_vs param_vs preds moded_clauses =
+ map_preds_modes (fn pred => compile_pred options comp_modifiers thy all_vs param_vs pred
(the (AList.lookup (op =) preds pred))) moded_clauses
fun prove options thy clauses preds moded_clauses compiled_terms =
@@ -2445,7 +2646,6 @@
compiled_terms
(* preparation of introduction rules into special datastructures *)
-
fun dest_prem thy params t =
(case strip_comb t of
(v as Free _, ts) => if member (op =) params v then Prem t else Sidecond t
@@ -2589,9 +2789,6 @@
datatype steps = Steps of
{
define_functions : options -> (string * typ) list -> string * (bool * mode) list -> theory -> theory,
- (*infer_modes : options -> (string * typ) list -> (string * mode list) list
- -> string list -> (string * (term list * indprem list) list) list
- -> theory -> ((moded_clause list pred_mode_table * string list) * theory),*)
prove : options -> theory -> (string * (term list * indprem list) list) list -> (string * typ) list
-> moded_clause list pred_mode_table -> term pred_mode_table -> thm pred_mode_table,
add_code_equations : theory -> (string * typ) list
@@ -2618,32 +2815,39 @@
prepare_intrs options compilation thy prednames (maps (intros_of thy) prednames)
val _ = print_step options "Infering modes..."
val ((moded_clauses, errors), thy') =
- (*Output.cond_timeit true "Infering modes"
- (fn _ =>*) infer_modes mode_analysis_options
- options compilation preds all_modes param_vs clauses thy
+ Output.cond_timeit true "Infering modes"
+ (fn _ => infer_modes mode_analysis_options
+ options compilation preds all_modes param_vs clauses thy)
val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
val _ = check_expected_modes preds options modes
(*val _ = check_proposed_modes preds options modes (fst extra_modes) errors*)
val _ = print_modes options thy' modes
val _ = print_step options "Defining executable functions..."
- val thy'' = fold (#define_functions (dest_steps steps) options preds) modes thy'
- |> Theory.checkpoint
+ val thy'' =
+ Output.cond_timeit (!Quickcheck.timing) "Defining executable functions..."
+ (fn _ => fold (#define_functions (dest_steps steps) options preds) modes thy'
+ |> Theory.checkpoint)
val _ = print_step options "Compiling equations..."
val compiled_terms =
- compile_preds (#comp_modifiers (dest_steps steps)) thy'' all_vs param_vs preds moded_clauses
+ Output.cond_timeit (!Quickcheck.timing) "Compiling equations...." (fn _ =>
+ compile_preds options
+ (#comp_modifiers (dest_steps steps)) thy'' all_vs param_vs preds moded_clauses)
val _ = print_compiled_terms options thy'' compiled_terms
val _ = print_step options "Proving equations..."
val result_thms =
- #prove (dest_steps steps) options thy'' clauses preds moded_clauses compiled_terms
+ Output.cond_timeit (!Quickcheck.timing) "Proving equations...." (fn _ =>
+ #prove (dest_steps steps) options thy'' clauses preds moded_clauses compiled_terms)
val result_thms' = #add_code_equations (dest_steps steps) thy'' preds
(maps_modes result_thms)
val qname = #qname (dest_steps steps)
val attrib = fn thy => Attrib.attribute_i thy (Attrib.internal (K (Thm.declaration_attribute
(fn thm => Context.mapping (Code.add_eqn thm) I))))
- val thy''' = fold (fn (name, result_thms) => fn thy => snd (PureThy.add_thmss
+ val thy''' =
+ Output.cond_timeit (!Quickcheck.timing) "Setting code equations...." (fn _ =>
+ fold (fn (name, result_thms) => fn thy => snd (PureThy.add_thmss
[((Binding.qualify true (Long_Name.base_name name) (Binding.name qname), result_thms),
[attrib thy ])] thy))
- result_thms' thy'' |> Theory.checkpoint
+ result_thms' thy'' |> Theory.checkpoint)
in
thy'''
end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Wed Apr 21 11:23:04 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Wed Apr 21 12:11:48 2010 +0200
@@ -71,17 +71,6 @@
(Ts' @ [T']) ---> HOLogic.boolT
end;
-(* FIXME: create new predicate name -- does not avoid nameclashing *)
-fun pred_of f =
- let
- val (name, T) = dest_Const f
- in
- if (body_type T = @{typ bool}) then
- (Free (Long_Name.base_name name ^ "P", T))
- else
- (Free (Long_Name.base_name name ^ "P", pred_type T))
- end
-
(* creates the list of premises for every intro rule *)
(* theory -> term -> (string list, term list list) *)
@@ -274,6 +263,17 @@
map (apfst Envir.eta_contract) (flatten' (Pattern.eta_long [] t) (names, prems))
end;
+(* FIXME: create new predicate name -- does not avoid nameclashing *)
+fun pred_of thy f =
+ let
+ val (name, T) = dest_Const f
+ val base_name' = (Long_Name.base_name name ^ "P")
+ val name' = Sign.full_bname thy base_name'
+ val T' = if (body_type T = @{typ bool}) then T else pred_type T
+ in
+ (name', Const (name', T'))
+ end
+
(* assumption: mutual recursive predicates all have the same parameters. *)
fun define_predicates specs thy =
if forall (fn (const, _) => defined_const thy const) specs then
@@ -284,14 +284,17 @@
val eqns = maps snd specs
(* create prednames *)
val ((funs, argss), rhss) = map_split dest_code_eqn eqns |>> split_list
+ val dst_funs = distinct (op =) funs
val argss' = map (map transform_ho_arg) argss
fun is_lifted (t1, t2) = (fastype_of t2 = pred_type (fastype_of t1))
- (* FIXME: higher order arguments also occur in tuples! *)
+ (* FIXME: higher order arguments also occur in tuples! *)
val lifted_args = distinct (op =) (filter is_lifted (flat argss ~~ flat argss'))
- val preds = map pred_of funs
+ val (prednames, preds) = split_list (map (pred_of thy) funs)
+ val dst_preds = distinct (op =) preds
+ val dst_prednames = distinct (op =) prednames
(* mapping from term (Free or Const) to term *)
val net = fold Item_Net.update
- ((funs ~~ preds) @ lifted_args)
+ ((dst_funs ~~ dst_preds) @ lifted_args)
(Fun_Pred.get thy)
fun lookup_pred t = lookup thy net t
(* create intro rules *)
@@ -308,51 +311,42 @@
end
fun mk_rewr_thm (func, pred) = @{thm refl}
val intr_ts = maps mk_intros ((funs ~~ preds) ~~ (argss' ~~ rhss))
- val (ind_result, thy') =
- thy
- |> Sign.map_naming Name_Space.conceal
- |> Inductive.add_inductive_global
- {quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false,
- no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
- (map (fn (s, T) =>
- ((Binding.name s, T), NoSyn)) (distinct (op =) (map dest_Free preds)))
- (map (dest_Free o snd) lifted_args)
- (map (fn x => (Attrib.empty_binding, x)) intr_ts)
- []
- ||> Sign.restore_naming thy
- val prednames = map (fst o dest_Const) (#preds ind_result)
- (* add constants to my table *)
- val specs = map (fn predname => (predname, filter (Predicate_Compile_Aux.is_intro predname)
- (#intrs ind_result))) prednames
+ val (intrs, thy') = thy
+ |> Sign.add_consts_i
+ (map (fn Const (name, T) => (Binding.name (Long_Name.base_name name), T, NoSyn))
+ dst_preds)
+ |> fold_map Specification.axiom (map (pair (Binding.empty, [])) intr_ts)
+ val specs = map (fn predname => (predname,
+ map Drule.export_without_context (filter (Predicate_Compile_Aux.is_intro predname) intrs)))
+ dst_prednames
val thy'' = Fun_Pred.map
- (fold Item_Net.update (map (apfst Logic.varify_global)
- (distinct (op =) funs ~~ (#preds ind_result)))) thy'
+ (fold Item_Net.update (map (pairself Logic.varify_global)
+ (dst_funs ~~ dst_preds))) thy'
fun functional_mode_of T =
list_fun_mode (replicate (length (binder_types T)) Input @ [Output])
val thy''' = fold
(fn (predname, Const (name, T)) => Predicate_Compile_Core.register_alternative_function
predname (functional_mode_of T) name)
- (prednames ~~ distinct (op =) funs) thy''
+ (dst_prednames ~~ dst_funs) thy''
in
(specs, thy''')
end
fun rewrite_intro thy intro =
let
- (*val _ = tracing ("Rewriting intro with registered mapping for: " ^
- commas (Symtab.keys (Pred_Compile_Preproc.get thy)))*)
fun lookup_pred t = lookup thy (Fun_Pred.get thy) t
+ (*val _ = tracing ("Rewriting intro " ^ Display.string_of_thm_global thy intro)*)
val intro_t = Logic.unvarify_global (prop_of intro)
val (prems, concl) = Logic.strip_horn intro_t
val frees = map fst (Term.add_frees intro_t [])
fun rewrite prem names =
let
(*val _ = tracing ("Rewriting premise " ^ Syntax.string_of_term_global thy prem ^ "...")*)
- val t = (HOLogic.dest_Trueprop prem)
+ val t = HOLogic.dest_Trueprop prem
val (lit, mk_lit) = case try HOLogic.dest_not t of
SOME t => (t, HOLogic.mk_not)
| NONE => (t, I)
- val (P, args) = (strip_comb lit)
+ val (P, args) = strip_comb lit
in
folds_map (flatten thy lookup_pred) args (names, [])
|> map (fn (resargs, (names', prems')) =>
@@ -365,6 +359,8 @@
rewrite concl frees'
|> map (fn (concl'::conclprems, _) =>
Logic.list_implies ((flat prems') @ conclprems, concl')))
+ (*val _ = tracing ("Rewritten intro to " ^
+ commas (map (Syntax.string_of_term_global thy) intro_ts'))*)
in
map (Drule.export_without_context o Skip_Proof.make_thm thy) intro_ts'
end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Wed Apr 21 11:23:04 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Wed Apr 21 12:11:48 2010 +0200
@@ -68,10 +68,12 @@
skip_proof = false,
compilation = Random,
inductify = true,
+ specialise = true,
+ detect_switches = false,
function_flattening = true,
fail_safe_function_flattening = false,
no_higher_order_predicate = [],
- no_topmost_reordering = true
+ no_topmost_reordering = false
}
val debug_options = Options {
@@ -88,6 +90,8 @@
skip_proof = false,
compilation = Random,
inductify = true,
+ specialise = true,
+ detect_switches = false,
function_flattening = true,
fail_safe_function_flattening = false,
no_higher_order_predicate = [],
@@ -99,13 +103,13 @@
(Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p,
- compilation = c, inductify = i, function_flattening = f_f,
+ compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f,
fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho,
no_topmost_reordering = re}) =
(Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p,
- compilation = c, inductify = i, function_flattening = b,
+ compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = b,
fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho,
no_topmost_reordering = re})
@@ -113,13 +117,13 @@
(Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p,
- compilation = c, inductify = i, function_flattening = f_f,
+ compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f,
fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho,
no_topmost_reordering = re}) =
(Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p,
- compilation = c, inductify = i, function_flattening = f_f,
+ compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f,
fail_safe_function_flattening = b, no_higher_order_predicate = no_ho,
no_topmost_reordering = re})
@@ -127,13 +131,13 @@
(Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p,
- compilation = c, inductify = i, function_flattening = f_f,
+ compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f,
fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho,
no_topmost_reordering = re}) =
(Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p,
- compilation = c, inductify = i, function_flattening = f_f,
+ compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f,
fail_safe_function_flattening = fs_ff, no_higher_order_predicate = ss, no_topmost_reordering = re})
@@ -198,7 +202,7 @@
val tac = fn _ => Skip_Proof.cheat_tac thy1
val intro = Goal.prove (ProofContext.init thy1) (map fst vs') [] t tac
val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1
- val (thy3, preproc_time) = cpu_time "predicate preprocessing"
+ val (thy3, preproc_time) = cpu_time "predicate preprocessing"
(fn () => Predicate_Compile.preprocess options const thy2)
val (thy4, core_comp_time) = cpu_time "random_dseq core compilation"
(fn () =>
@@ -209,7 +213,9 @@
Predicate_Compile_Core.add_new_random_dseq_equations options [full_constname] thy3
(*| Depth_Limited_Random =>
Predicate_Compile_Core.add_depth_limited_random_equations options [full_constname] thy3*))
- val _ = Predicate_Compile_Core.print_all_modes compilation thy4
+ (*val _ = Predicate_Compile_Core.print_all_modes compilation thy4*)
+ val _ = Output.tracing ("Preprocessing time: " ^ string_of_int (snd preproc_time))
+ val _ = Output.tracing ("Core compilation time: " ^ string_of_int (snd core_comp_time))
val modes = Predicate_Compile_Core.modes_of compilation thy4 full_constname
val output_mode = fold_rev (curry Fun) (map (K Output) (binder_types constT)) Bool
val prog =
@@ -228,7 +234,6 @@
Const (name, T)
end
else error ("Predicate Compile Quickcheck failed: " ^ commas (map string_of_mode modes))
-
val qc_term =
case compilation of
Pos_Random_DSeq => mk_bind (prog,
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Wed Apr 21 11:23:04 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Wed Apr 21 12:11:48 2010 +0200
@@ -107,7 +107,9 @@
val [t, specialised_t] = Variable.exportT_terms ctxt' ctxt
[list_comb (pred, pats), list_comb (specialised_const, result_pats)]
val thy'' = Specialisations.map (Item_Net.update (t, specialised_t)) thy'
- val ([spec], thy''') = find_specialisations black_list [(constname, exported_intros)] thy''
+ val optimised_intros =
+ map_filter (Predicate_Compile_Aux.peephole_optimisation thy'') exported_intros
+ val ([spec], thy''') = find_specialisations black_list [(constname, optimised_intros)] thy''
val thy'''' = Predicate_Compile_Core.register_intros spec thy'''
in
thy''''