--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mutabelle/ROOT.ML Tue Feb 23 14:00:36 2010 +0100
@@ -0,0 +1,3 @@
+
+use_thy "MutabelleExtra";
+
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Tue Feb 23 12:14:46 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Tue Feb 23 14:00:36 2010 +0100
@@ -10,9 +10,11 @@
val take_random : int -> 'a list -> 'a list
datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error
-type mtd = string * (theory -> term -> outcome)
+type timing = (string * int) list
-type mutant_subentry = term * (string * outcome) list
+type mtd = string * (theory -> term -> outcome * timing)
+
+type mutant_subentry = term * (string * (outcome * timing)) list
type detailed_entry = string * bool * term * mutant_subentry list
type subentry = string * int * int * int * int * int * int
@@ -52,7 +54,7 @@
(* quickcheck options *)
(*val quickcheck_generator = "SML"*)
-val iterations = 100
+val iterations = 1
val size = 5
exception RANDOM;
@@ -75,12 +77,13 @@
else l + Real.floor (rmod (random ()) (real (h - l + 1)));
datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error
-type mtd = string * (theory -> term -> outcome)
+type timing = (string * int) list
-type mutant_subentry = term * (string * outcome) list
+type mtd = string * (theory -> term -> outcome * timing)
+
+type mutant_subentry = term * (string * (outcome * timing)) list
type detailed_entry = string * bool * term * mutant_subentry list
-
type subentry = string * int * int * int * int * int * int
type entry = string * bool * subentry list
type report = entry list
@@ -94,11 +97,11 @@
fun invoke_quickcheck quickcheck_generator thy t =
TimeLimit.timeLimit (Time.fromSeconds (! Auto_Counterexample.time_limit))
(fn _ =>
- case Quickcheck.test_term (ProofContext.init thy) false (SOME quickcheck_generator)
+ case Quickcheck.timed_test_term (ProofContext.init thy) false (SOME quickcheck_generator)
size iterations (preprocess thy [] t) of
- NONE => NoCex
- | SOME _ => GenuineCex) ()
- handle TimeLimit.TimeOut => Timeout
+ (NONE, time_report) => (NoCex, time_report)
+ | (SOME _, time_report) => (GenuineCex, time_report)) ()
+ handle TimeLimit.TimeOut => (Timeout, [("timelimit", !Auto_Counterexample.time_limit)])
fun quickcheck_mtd quickcheck_generator =
("quickcheck_" ^ quickcheck_generator, invoke_quickcheck quickcheck_generator)
@@ -189,9 +192,9 @@
val forbidden =
[(* (@{const_name "power"}, "'a"), *)
- (@{const_name HOL.induct_equal}, "'a"),
- (@{const_name HOL.induct_implies}, "'a"),
- (@{const_name HOL.induct_conj}, "'a"),
+ (*(@{const_name induct_equal}, "'a"),
+ (@{const_name induct_implies}, "'a"),
+ (@{const_name induct_conj}, "'a"),*)
(@{const_name "undefined"}, "'a"),
(@{const_name "default"}, "'a"),
(@{const_name "dummy_pattern"}, "'a::{}") (*,
@@ -245,17 +248,26 @@
Library.nth xs j :: take_random (n - 1) (nth_drop j xs)
end
+fun cpu_time description f =
+ let
+ val start = start_timing ()
+ val result = Exn.capture f ()
+ val time = Time.toMilliseconds (#cpu (end_timing start))
+ in (Exn.release result, (description, time)) end
+
fun safe_invoke_mtd thy (mtd_name, invoke_mtd) t =
let
val _ = priority ("Invoking " ^ mtd_name)
- val res = case try (invoke_mtd thy) t of
- SOME res => res
- | NONE => (priority ("**** PROBLEMS WITH " ^
- Syntax.string_of_term_global thy t); Error)
+ val ((res, timing), time) = cpu_time "total time"
+ (fn () => case try (invoke_mtd thy) t of
+ SOME (res, timing) => (res, timing)
+ | NONE => (priority ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t);
+ (Error , [])))
val _ = priority (" Done")
- in res end
+ in (res, time :: timing) end
(* theory -> term list -> mtd -> subentry *)
+(*
fun test_mutants_using_one_method thy mutants (mtd_name, invoke_mtd) =
let
val res = map (safe_invoke_mtd thy (mtd_name, invoke_mtd)) mutants
@@ -266,7 +278,7 @@
fun create_entry thy thm exec mutants mtds =
(Thm.get_name thm, exec, map (test_mutants_using_one_method thy mutants) mtds)
-
+*)
fun create_detailed_entry thy thm exec mutants mtds =
let
fun create_mutant_subentry mutant = (mutant,
@@ -322,15 +334,22 @@
| string_of_outcome Timeout = "Timeout"
| string_of_outcome Error = "Error"
-fun string_of_mutant_subentry thy (t, results) =
+fun string_of_mutant_subentry thy thm_name (t, results) =
"mutant: " ^ Syntax.string_of_term_global thy t ^ "\n" ^
- space_implode "; " (map (fn (mtd_name, outcome) => mtd_name ^ ": " ^ string_of_outcome outcome) results) ^
+ space_implode "; "
+ (map (fn (mtd_name, (outcome, timing)) => mtd_name ^ ": " ^ string_of_outcome outcome) results) ^
"\n"
+fun string_of_mutant_subentry' thy thm_name (t, results) =
+ "mutant of " ^ thm_name ^ ":" ^
+ cat_lines (map (fn (mtd_name, (outcome, timing)) =>
+ mtd_name ^ ": " ^ string_of_outcome outcome ^ "; " ^
+ space_implode "; " (map (fn (s, t) => (s ^ ": " ^ string_of_int t)) timing)) results)
+
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" ^
- cat_lines (map (string_of_mutant_subentry thy) mutant_subentries) ^ "\n"
+ cat_lines (map (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,
--- a/src/HOL/Tools/Datatype/datatype_prop.ML Tue Feb 23 12:14:46 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML Tue Feb 23 14:00:36 2010 +0100
@@ -22,6 +22,8 @@
(string * sort) list -> theory -> term list list
val make_splits : string list -> descr list ->
(string * sort) list -> theory -> (term * term) list
+ val make_case_combs : string list -> descr list ->
+ (string * sort) list -> theory -> string -> term list
val make_weak_case_congs : string list -> descr list ->
(string * sort) list -> theory -> term list
val make_case_congs : string list -> descr list ->
--- a/src/HOL/Tools/Function/function.ML Tue Feb 23 12:14:46 2010 +0100
+++ b/src/HOL/Tools/Function/function.ML Tue Feb 23 14:00:36 2010 +0100
@@ -97,6 +97,7 @@
|> addsmps (conceal_partial o Binding.qualify false "partial")
"psimps" conceal_partial psimp_attribs psimps
||> fold_option (snd oo addsmps I "simps" I simp_attribs) trsimps
+ ||> fold_option (Spec_Rules.add Spec_Rules.Equational o (pair fs)) trsimps
||>> Local_Theory.note ((conceal_partial (qualify "pinduct"),
[Attrib.internal (K (Rule_Cases.case_names cnames)),
Attrib.internal (K (Rule_Cases.consumes 1)),
@@ -126,7 +127,7 @@
val add_function =
gen_add_function false Specification.check_spec (TypeInfer.anyT HOLogic.typeS)
val add_function_cmd = gen_add_function true Specification.read_spec "_::type"
-
+
fun gen_termination_proof prep_term raw_term_opt lthy =
let
val term_opt = Option.map (prep_term lthy) raw_term_opt
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Tue Feb 23 12:14:46 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Tue Feb 23 14:00:36 2010 +0100
@@ -8,13 +8,13 @@
sig
val setup : theory -> theory
val preprocess : Predicate_Compile_Aux.options -> string -> theory -> theory
+ val present_graph : bool Unsynchronized.ref
end;
structure Predicate_Compile (*: PREDICATE_COMPILE*) =
struct
-(* options *)
-val fail_safe_mode = true
+val present_graph = Unsynchronized.ref false
open Predicate_Compile_Aux;
@@ -33,10 +33,12 @@
commas (map (Display.string_of_thm_global thy) intros)) intross)))
else ()
-fun print_specs thy specs =
- map (fn (c, thms) => "Constant " ^ c ^ " has specification:\n"
- ^ (space_implode "\n" (map (Display.string_of_thm_global thy) thms)) ^ "\n") specs
-
+fun print_specs options thy specs =
+ if show_intermediate_results options then
+ map (fn (c, thms) => "Constant " ^ c ^ " has specification:\n"
+ ^ (space_implode "\n" (map (Display.string_of_thm_global thy) thms)) ^ "\n") specs
+ |> space_implode "\n" |> tracing
+ else ()
fun overload_const thy s = the_default s (Option.map fst (AxClass.inst_of_param thy s))
fun map_specs f specs =
@@ -47,15 +49,21 @@
val _ = print_step options "Compiling predicates to flat introrules..."
val specs = map (apsnd (map
(fn th => if is_equationlike th then Predicate_Compile_Data.normalize_equation thy' th else th))) specs
- val (intross1, thy'') = apfst flat (fold_map Predicate_Compile_Pred.preprocess specs thy')
+ val (intross1, thy'') =
+ apfst flat (fold_map (Predicate_Compile_Pred.preprocess options) specs thy')
val _ = print_intross options thy'' "Flattened introduction rules: " intross1
val _ = print_step options "Replacing functions in introrules..."
val intross2 =
- if fail_safe_mode then
- case try (map_specs (maps (Predicate_Compile_Fun.rewrite_intro thy''))) intross1 of
- SOME intross => intross
- | NONE => let val _ = warning "Function replacement failed!" in intross1 end
- else map_specs (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross1
+ if function_flattening options then
+ if fail_safe_function_flattening options then
+ case try (map_specs (maps (Predicate_Compile_Fun.rewrite_intro thy''))) intross1 of
+ SOME intross => intross
+ | NONE =>
+ (if show_caught_failures options then tracing "Function replacement failed!" else ();
+ intross1)
+ else map_specs (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross1
+ else
+ intross1
val _ = print_intross options thy'' "Introduction rules with replaced functions: " intross2
val _ = print_step options "Introducing new constants for abstractions at higher-order argument positions..."
val (intross3, (new_defs, thy''')) = Predicate_Compile_Pred.flat_higher_order_arguments (intross2, thy'')
@@ -70,35 +78,45 @@
end
fun preprocess_strong_conn_constnames options gr ts thy =
- let
- fun get_specs ts = map_filter (fn t =>
- TermGraph.get_node gr t |>
- (fn ths => if null ths then NONE else SOME (fst (dest_Const t), ths)))
- ts
- val _ = print_step options ("Preprocessing scc of " ^
- commas (map (Syntax.string_of_term_global thy) ts))
- val (prednames, funnames) = List.partition (fn t => body_type (fastype_of t) = @{typ bool}) ts
- (* untangle recursion by defining predicates for all functions *)
- val _ = print_step options
- ("Compiling functions (" ^ commas (map (Syntax.string_of_term_global thy) funnames) ^
- ") to predicates...")
- val (fun_pred_specs, thy') =
- if not (null funnames) then Predicate_Compile_Fun.define_predicates
- (get_specs funnames) thy else ([], thy)
- val _ = print_specs thy' fun_pred_specs
- val specs = (get_specs prednames) @ fun_pred_specs
- val (intross3, thy''') = process_specification options specs thy'
- val _ = print_intross options thy''' "Introduction rules with new constants: " intross3
- val intross4 = map_specs (maps remove_pointless_clauses) intross3
- val _ = print_intross options thy''' "After removing pointless clauses: " intross4
- val intross5 = map (fn (s, ths) => (overload_const thy''' s, map (AxClass.overload thy''') ths)) intross4
- val intross6 = map_specs (map (expand_tuples thy''')) intross5
- val _ = print_intross options thy''' "introduction rules before registering: " intross6
- val _ = print_step options "Registering introduction rules..."
- val thy'''' = fold Predicate_Compile_Core.register_intros intross6 thy'''
- in
- thy''''
- end;
+ if forall (fn (Const (c, _)) => Predicate_Compile_Core.is_registered thy c) ts then
+ thy
+ else
+ let
+ fun get_specs ts = map_filter (fn t =>
+ TermGraph.get_node gr t |>
+ (fn ths => if null ths then NONE else SOME (fst (dest_Const t), ths)))
+ ts
+ val _ = print_step options ("Preprocessing scc of " ^
+ commas (map (Syntax.string_of_term_global thy) ts))
+ val (prednames, funnames) = List.partition (fn t => body_type (fastype_of t) = @{typ bool}) ts
+ (* untangle recursion by defining predicates for all functions *)
+ val _ = print_step options
+ ("Compiling functions (" ^ commas (map (Syntax.string_of_term_global thy) funnames) ^
+ ") to predicates...")
+ val (fun_pred_specs, thy') =
+ (if function_flattening options andalso (not (null funnames)) then
+ if fail_safe_function_flattening options then
+ case try (Predicate_Compile_Fun.define_predicates (get_specs funnames)) thy of
+ SOME (intross, thy) => (intross, thy)
+ | NONE => ([], thy)
+ else Predicate_Compile_Fun.define_predicates (get_specs funnames) thy
+ else ([], thy))
+ (*||> Theory.checkpoint*)
+ val _ = print_specs options thy' fun_pred_specs
+ val specs = (get_specs prednames) @ fun_pred_specs
+ val (intross3, thy''') = process_specification options specs thy'
+ val _ = print_intross options thy''' "Introduction rules with new constants: " intross3
+ val intross4 = map_specs (maps remove_pointless_clauses) intross3
+ val _ = print_intross options thy''' "After removing pointless clauses: " intross4
+ val intross5 =
+ map (fn (s, ths) => (overload_const thy''' s, map (AxClass.overload thy''') ths)) intross4
+ val intross6 = map_specs (map (expand_tuples thy''')) intross5
+ val _ = print_intross options thy''' "introduction rules before registering: " intross6
+ val _ = print_step options "Registering introduction rules..."
+ val thy'''' = fold Predicate_Compile_Core.register_intros intross6 thy'''
+ in
+ thy''''
+ end;
fun preprocess options t thy =
let
@@ -106,6 +124,7 @@
val gr = Output.cond_timeit (!Quickcheck.timing) "preprocess-obtain graph"
(fn () => Predicate_Compile_Data.obtain_specification_graph options thy t
|> (fn gr => TermGraph.subgraph (member (op =) (TermGraph.all_succs gr [t])) gr))
+ val _ = if !present_graph then Predicate_Compile_Data.present_graph gr else ()
in
Output.cond_timeit (!Quickcheck.timing) "preprocess-process"
(fn () => (fold_rev (preprocess_strong_conn_constnames options gr)
@@ -128,7 +147,12 @@
show_modes = chk "show_modes",
show_mode_inference = chk "show_mode_inference",
show_compilation = chk "show_compilation",
+ show_caught_failures = false,
skip_proof = chk "skip_proof",
+ function_flattening = not (chk "no_function_flattening"),
+ fail_safe_function_flattening = false,
+ no_topmost_reordering = false,
+ no_higher_order_predicate = [],
inductify = chk "inductify",
compilation = compilation
}
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Tue Feb 23 12:14:46 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Tue Feb 23 14:00:36 2010 +0100
@@ -29,6 +29,7 @@
fun find_indices f xs =
map_filter (fn (i, true) => SOME i | (i, false) => NONE) (map_index (apsnd f) xs)
+fun assert check = if check then () else error "Assertion failed!"
(* mode *)
datatype mode = Bool | Input | Output | Pair of mode * mode | Fun of mode * mode
@@ -57,21 +58,47 @@
fun dest_tuple_mode (Pair (mode, mode')) = mode :: dest_tuple_mode mode'
| dest_tuple_mode _ = []
-fun all_modes_of_typ (T as Type ("fun", _)) =
+
+fun all_modes_of_typ' (T as Type ("fun", _)) =
+ let
+ val (S, U) = strip_type T
+ in
+ if U = HOLogic.boolT then
+ fold_rev (fn m1 => fn m2 => map_product (curry Fun) m1 m2)
+ (map all_modes_of_typ' S) [Bool]
+ else
+ [Input, Output]
+ end
+ | all_modes_of_typ' (Type ("*", [T1, T2])) =
+ map_product (curry Pair) (all_modes_of_typ' T1) (all_modes_of_typ' T2)
+ | all_modes_of_typ' _ = [Input, Output]
+
+fun all_modes_of_typ (T as Type ("fun", _)) =
let
val (S, U) = strip_type T
in
if U = HOLogic.boolT then
fold_rev (fn m1 => fn m2 => map_product (curry Fun) m1 m2)
- (map all_modes_of_typ S) [Bool]
+ (map all_modes_of_typ' S) [Bool]
else
[Input, Output]
end
- | all_modes_of_typ (Type ("*", [T1, T2])) =
- map_product (curry Pair) (all_modes_of_typ T1) (all_modes_of_typ T2)
| all_modes_of_typ (Type ("bool", [])) = [Bool]
- | all_modes_of_typ _ = [Input, Output]
+ | all_modes_of_typ T = all_modes_of_typ' T
+fun all_smodes_of_typ (T as Type ("fun", _)) =
+ let
+ val (S, U) = strip_type T
+ fun all_smodes (Type ("*", [T1, T2])) =
+ map_product (curry Pair) (all_smodes T1) (all_smodes T2)
+ | all_smodes _ = [Input, Output]
+ in
+ if U = HOLogic.boolT then
+ fold_rev (fn m1 => fn m2 => map_product (curry Fun) m1 m2) (map all_smodes S) [Bool]
+ else
+ error "all_smodes_of_typ: invalid type for predicate"
+ end
+(*
fun extract_params arg =
case fastype_of arg of
(T as Type ("fun", _)) =>
@@ -86,7 +113,7 @@
extract_params t1 @ extract_params t2
end
| _ => []
-
+*)
fun ho_arg_modes_of mode =
let
fun ho_arg_mode (m as Fun _) = [m]
@@ -144,9 +171,10 @@
in
(comb_option HOLogic.mk_prod (i1, i2), comb_option HOLogic.mk_prod (o1, o2))
end
- | split_arg_mode' Input t = (SOME t, NONE)
- | split_arg_mode' Output t = (NONE, SOME t)
- | split_arg_mode' _ _ = error "split_map_mode: mode and term do not match"
+ | split_arg_mode' m t =
+ if eq_mode (m, Input) then (SOME t, NONE)
+ else if eq_mode (m, Output) then (NONE, SOME t)
+ else error "split_map_mode: mode and term do not match"
in
(pairself (map_filter I) o split_list) (map2 split_arg_mode' (strip_fun_mode mode) ts)
end
@@ -269,7 +297,6 @@
let
val T = (Sign.the_const_type thy constname)
in body_type T = @{typ "bool"} end;
-
fun is_predT (T as Type("fun", [_, _])) = (snd (strip_type T) = HOLogic.boolT)
| is_predT _ = false
@@ -373,7 +400,60 @@
in
Logic.list_implies (maps f premises, head)
end
+
+
+(* split theorems of case expressions *)
+
+(*
+fun has_split_rule_cname @{const_name "nat_case"} = true
+ | has_split_rule_cname @{const_name "list_case"} = true
+ | has_split_rule_cname _ = false
+fun has_split_rule_term thy (Const (@{const_name "nat_case"}, _)) = true
+ | has_split_rule_term thy (Const (@{const_name "list_case"}, _)) = true
+ | has_split_rule_term thy _ = false
+
+fun has_split_rule_term' thy (Const (@{const_name "If"}, _)) = true
+ | has_split_rule_term' thy (Const (@{const_name "Let"}, _)) = true
+ | has_split_rule_term' thy c = has_split_rule_term thy c
+
+*)
+fun prepare_split_thm ctxt split_thm =
+ (split_thm RS @{thm iffD2})
+ |> LocalDefs.unfold ctxt [@{thm atomize_conjL[symmetric]},
+ @{thm atomize_all[symmetric]}, @{thm atomize_imp[symmetric]}]
+
+fun find_split_thm thy (Const (name, typ)) =
+ let
+ fun split_name str =
+ case first_field "." str
+ of (SOME (field, rest)) => field :: split_name rest
+ | NONE => [str]
+ val splitted_name = split_name name
+ in
+ if length splitted_name > 0 andalso
+ String.isSuffix "_case" (List.last splitted_name)
+ then
+ (List.take (splitted_name, length splitted_name - 1)) @ ["split"]
+ |> space_implode "."
+ |> PureThy.get_thm thy
+ |> SOME
+ handle ERROR msg => NONE
+ else NONE
+ end
+ | find_split_thm _ _ = NONE
+
+
+(* TODO: split rules for let and if are different *)
+fun find_split_thm' thy (Const (@{const_name "If"}, _)) = SOME @{thm split_if}
+ | find_split_thm' thy (Const (@{const_name "Let"}, _)) = SOME @{thm refl} (* TODO *)
+ | find_split_thm' thy c = find_split_thm thy c
+
+fun has_split_thm thy t = is_some (find_split_thm thy t)
+
+fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t)
+
+
(* lifting term operations to theorems *)
fun map_term thy f th =
@@ -388,7 +468,16 @@
(* Different options for compiler *)
-datatype compilation = Pred | Random | Depth_Limited | DSeq | Annotated | Random_DSeq
+datatype compilation = Pred | Random | Depth_Limited | DSeq | Annotated
+ | Pos_Random_DSeq | Neg_Random_DSeq
+
+
+fun negative_compilation_of Pos_Random_DSeq = Neg_Random_DSeq
+ | negative_compilation_of Neg_Random_DSeq = Pos_Random_DSeq
+ | negative_compilation_of c = c
+
+fun compilation_for_polarity false Pos_Random_DSeq = Neg_Random_DSeq
+ | compilation_for_polarity _ c = c
fun string_of_compilation c = case c of
Pred => ""
@@ -396,8 +485,9 @@
| Depth_Limited => "depth limited"
| DSeq => "dseq"
| Annotated => "annotated"
- | Random_DSeq => "random dseq"
-
+ | Pos_Random_DSeq => "pos_random dseq"
+ | Neg_Random_DSeq => "neg_random_dseq"
+
(*datatype compilation_options =
Pred | Random of int | Depth_Limited of int | DSeq of int | Annotated*)
@@ -411,8 +501,12 @@
show_mode_inference : bool,
show_modes : bool,
show_compilation : bool,
+ show_caught_failures : bool,
skip_proof : bool,
-
+ no_topmost_reordering : bool,
+ function_flattening : bool,
+ fail_safe_function_flattening : bool,
+ no_higher_order_predicate : string list,
inductify : bool,
compilation : compilation
};
@@ -428,8 +522,15 @@
fun show_modes (Options opt) = #show_modes opt
fun show_mode_inference (Options opt) = #show_mode_inference opt
fun show_compilation (Options opt) = #show_compilation opt
+fun show_caught_failures (Options opt) = #show_caught_failures opt
+
fun skip_proof (Options opt) = #skip_proof opt
+fun function_flattening (Options opt) = #function_flattening opt
+fun fail_safe_function_flattening (Options opt) = #fail_safe_function_flattening opt
+fun no_topmost_reordering (Options opt) = #no_topmost_reordering opt
+fun no_higher_order_predicate (Options opt) = #no_higher_order_predicate opt
+
fun is_inductify (Options opt) = #inductify opt
fun compilation (Options opt) = #compilation opt
@@ -444,18 +545,22 @@
show_modes = false,
show_mode_inference = false,
show_compilation = false,
+ show_caught_failures = false,
skip_proof = true,
-
+ no_topmost_reordering = false,
+ function_flattening = false,
+ fail_safe_function_flattening = false,
+ no_higher_order_predicate = [],
inductify = false,
compilation = Pred
}
val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", "show_modes",
- "show_mode_inference", "show_compilation", "skip_proof", "inductify"]
+ "show_mode_inference", "show_compilation", "skip_proof", "inductify", "no_function_flattening"]
val compilation_names = [("pred", Pred),
(*("random", Random), ("depth_limited", Depth_Limited), ("annotated", Annotated),*)
- ("dseq", DSeq), ("random_dseq", Random_DSeq)]
+ ("dseq", DSeq), ("random_dseq", Pos_Random_DSeq)]
fun print_step options s =
if show_steps options then tracing s else ()
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Feb 23 12:14:46 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Feb 23 14:00:36 2010 +0100
@@ -16,7 +16,7 @@
val register_intros : string * thm list -> theory -> theory
val is_registered : theory -> string -> bool
val function_name_of : Predicate_Compile_Aux.compilation -> theory
- -> string -> Predicate_Compile_Aux.mode -> string
+ -> string -> bool * Predicate_Compile_Aux.mode -> string
val predfun_intro_of: theory -> string -> Predicate_Compile_Aux.mode -> thm
val predfun_elim_of: theory -> string -> Predicate_Compile_Aux.mode -> thm
val all_preds_of : theory -> string list
@@ -153,7 +153,7 @@
| mode_of (Term m) = m
| mode_of (Mode_App (d1, d2)) =
(case mode_of d1 of Fun (m, m') =>
- (if m = mode_of d2 then m' else error "mode_of")
+ (if eq_mode (m, mode_of d2) then m' else error "mode_of")
| _ => error "mode_of2")
| mode_of (Mode_Pair (d1, d2)) =
Pair (mode_of d1, mode_of d2)
@@ -182,7 +182,7 @@
type moded_clause = term list * (indprem * mode_derivation) list
-type 'a pred_mode_table = (string * (mode * 'a) list) list
+type 'a pred_mode_table = (string * ((bool * mode) * 'a) list) list
(* book-keeping *)
@@ -257,8 +257,9 @@
^ "functions defined for predicate " ^ quote name)
| SOME fun_names => fun_names
-fun function_name_of compilation thy name mode =
- case AList.lookup (op =) (function_names_of compilation thy name) mode of
+fun function_name_of compilation thy name (pol, mode) =
+ case AList.lookup eq_mode
+ (function_names_of (compilation_for_polarity pol compilation) thy name) mode of
NONE => error ("No " ^ string_of_compilation compilation
^ "function defined for mode " ^ string_of_mode mode ^ " of predicate " ^ quote name)
| SOME function_name => function_name
@@ -296,12 +297,12 @@
if show_modes options then
tracing ("Inferred modes:\n" ^
cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
- string_of_mode ms)) modes))
+ (fn (p, m) => string_of_mode m ^ (if p then "pos" else "neg")) ms)) modes))
else ()
fun print_pred_mode_table string_of_entry thy pred_mode_table =
let
- fun print_mode pred (mode, entry) = "mode : " ^ string_of_mode mode
+ fun print_mode pred ((pol, mode), entry) = "mode : " ^ string_of_mode mode
^ string_of_entry pred mode entry
fun print_pred (pred, modes) =
"predicate " ^ pred ^ ": " ^ cat_lines (map (print_mode pred) modes)
@@ -364,7 +365,7 @@
SOME (s, ms) => (case AList.lookup (op =) modes s of
SOME modes =>
let
- val modes' = modes
+ val modes' = map snd modes
in
if not (eq_set eq_mode (ms, modes')) then
error ("expected modes were not inferred:\n"
@@ -381,7 +382,7 @@
SOME inferred_ms =>
let
val preds_without_modes = map fst (filter (null o snd) (modes @ extra_modes))
- val modes' = inferred_ms
+ val modes' = map snd inferred_ms
in
if not (eq_set eq_mode (ms, modes')) then
error ("expected modes were not inferred:\n"
@@ -880,8 +881,6 @@
Random_Sequence_CompFuns.mk_random_dseqT T) $ random
end;
-
-
(* for external use with interactive mode *)
val pred_compfuns = PredicateCompFuns.compfuns
val randompred_compfuns = Random_Sequence_CompFuns.compfuns;
@@ -898,6 +897,8 @@
(** mode analysis **)
+(* options for mode analysis are: #use_random, #reorder_premises *)
+
fun is_constrt thy =
let
val cnstrs = flat (maps
@@ -935,7 +936,7 @@
in merge (map (fn ks => i::ks) is) is end
else [[]];
-fun print_failed_mode options thy modes p m rs is =
+fun print_failed_mode options thy modes p (pol, m) rs is =
if show_mode_inference options then
let
val _ = tracing ("Clauses " ^ commas (map (fn i => string_of_int (i + 1)) is) ^ " of " ^
@@ -943,7 +944,7 @@
in () end
else ()
-fun error_of p m is =
+fun error_of p (pol, m) is =
(" Clauses " ^ commas (map (fn i => string_of_int (i + 1)) is) ^ " of " ^
p ^ " violates mode " ^ string_of_mode m)
@@ -992,7 +993,7 @@
fun is_invertible_function thy (Const (f, _)) = is_constr thy f
| is_invertible_function thy _ = false
-fun non_invertible_subterms thy (Free _) = []
+fun non_invertible_subterms thy (t as Free _) = []
| non_invertible_subterms thy t =
case (strip_comb t) of (f, args) =>
if is_invertible_function thy f then
@@ -1029,6 +1030,9 @@
forall
(fn t => is_eqT (fastype_of t) andalso forall (member (op =) vs) (term_vs t))
(non_invertible_subterms thy t)
+ andalso
+ (forall (is_eqT o snd)
+ (inter (fn ((f', _), f) => f = f') vs (Term.add_frees t [])))
fun vars_of_destructable_term thy (Free (x, _)) = [x]
| vars_of_destructable_term thy t =
@@ -1042,18 +1046,52 @@
fun missing_vars vs t = subtract (op =) vs (term_vs t)
-fun derivations_of thy modes vs t Input =
- [(Term Input, missing_vars vs t)]
- | derivations_of thy modes vs t Output =
- if is_possible_output thy vs t then [(Term Output, [])] else []
- | derivations_of thy modes vs (Const ("Pair", _) $ t1 $ t2) (Pair (m1, m2)) =
+fun output_terms (Const ("Pair", _) $ t1 $ t2, Mode_Pair (d1, d2)) =
+ output_terms (t1, d1) @ output_terms (t2, d2)
+ | output_terms (t1 $ t2, Mode_App (d1, d2)) =
+ output_terms (t1, d1) @ output_terms (t2, d2)
+ | output_terms (t, Term Output) = [t]
+ | output_terms _ = []
+
+fun lookup_mode modes (Const (s, T)) =
+ (case (AList.lookup (op =) modes s) of
+ SOME ms => SOME (map (fn m => (Context m, [])) ms)
+ | NONE => NONE)
+ | lookup_mode modes (Free (x, _)) =
+ (case (AList.lookup (op =) modes x) of
+ SOME ms => SOME (map (fn m => (Context m , [])) ms)
+ | NONE => NONE)
+
+fun derivations_of thy modes vs (Const ("Pair", _) $ t1 $ t2) (Pair (m1, m2)) =
map_product
(fn (m1, mvars1) => fn (m2, mvars2) => (Mode_Pair (m1, m2), union (op =) mvars1 mvars2))
(derivations_of thy modes vs t1 m1) (derivations_of thy modes vs t2 m2)
+ | derivations_of thy modes vs t (m as Fun _) =
+ (*let
+ val (p, args) = strip_comb t
+ in
+ (case lookup_mode modes p of
+ SOME ms => map_filter (fn (Context m, []) => let
+ val ms = strip_fun_mode m
+ val (argms, restms) = chop (length args) ms
+ val m' = fold_rev (curry Fun) restms Bool
+ in
+ if forall (fn m => eq_mode (Input, m)) argms andalso eq_mode (m', mode) then
+ SOME (fold (curry Mode_App) (map Term argms) (Context m), missing_vars vs t)
+ else NONE
+ end) ms
+ | NONE => (if is_all_input mode then [(Context mode, [])] else []))
+ end*)
+ (case try (all_derivations_of thy modes vs) t of
+ SOME derivs =>
+ filter (fn (d, mvars) => eq_mode (mode_of d, m) andalso null (output_terms (t, d))) derivs
+ | NONE => (if is_all_input m then [(Context m, [])] else []))
| derivations_of thy modes vs t m =
- (case try (all_derivations_of thy modes vs) t of
- SOME derivs => filter (fn (d, mvars) => mode_of d = m) derivs
- | NONE => (if is_all_input m then [(Context m, [])] else []))
+ if eq_mode (m, Input) then
+ [(Term Input, missing_vars vs t)]
+ else if eq_mode (m, Output) then
+ (if is_possible_output thy vs t then [(Term Output, [])] else [])
+ else []
and all_derivations_of thy modes vs (Const ("Pair", _) $ t1 $ t2) =
let
val derivs1 = all_derivations_of thy modes vs t1
@@ -1073,14 +1111,8 @@
(Mode_App (d1, d2), union (op =) mvars1 mvars2)) (derivations_of thy modes vs t2 m')
| _ => error "Something went wrong") derivs1
end
- | all_derivations_of thy modes vs (Const (s, T)) =
- (case (AList.lookup (op =) modes s) of
- SOME ms => map (fn m => (Context m, [])) ms
- | NONE => error ("No mode for constant " ^ s))
- | all_derivations_of _ modes vs (Free (x, _)) =
- (case (AList.lookup (op =) modes x) of
- SOME ms => map (fn m => (Context m , [])) ms
- | NONE => error ("No mode for parameter variable " ^ x))
+ | all_derivations_of thy modes vs (Const (s, T)) = the (lookup_mode modes (Const (s, T)))
+ | all_derivations_of thy modes vs (Free (x, T)) = the (lookup_mode modes (Free (x, T)))
| all_derivations_of _ modes vs _ = error "all_derivations_of"
fun rev_option_ord ord (NONE, NONE) = EQUAL
@@ -1097,7 +1129,7 @@
SOME (s, _) =>
(case AList.lookup (op =) modes s of
SOME ms =>
- (case AList.lookup (op =) ms (head_mode_of deriv) of
+ (case AList.lookup (op =) (map (fn ((p, m), r) => (m, r)) ms) (head_mode_of deriv) of
SOME r => r
| NONE => false)
| NONE => false)
@@ -1146,51 +1178,56 @@
tracing ("modes: " ^ (commas (map (fn (s, ms) => s ^ ": " ^
commas (map (fn (m, r) => string_of_mode m ^ (if r then " random " else " not ")) ms)) modes)))
-fun select_mode_prem' thy modes vs ps =
+fun select_mode_prem mode_analysis_options thy pol (modes, (pos_modes, neg_modes)) vs ps =
let
- val modes' = map (fn (s, ms) => (s, map fst ms)) modes
+ fun choose_mode_of_prem (Prem t) = partial_hd
+ (sort (deriv_ord2 thy 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 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 = error ("choose_mode_of_prem: " ^ string_of_prem thy p)
in
- partial_hd (sort (premise_ord thy modes) (ps ~~ map
- (fn Prem t =>
- partial_hd
- (sort (deriv_ord2 thy modes t) (all_derivations_of thy modes' vs t))
- | Sidecond t => SOME (Context Bool, missing_vars vs t)
- | Negprem t =>
- partial_hd
- (sort (deriv_ord2 thy modes t) (filter (fn (d, missing_vars) => is_all_input (head_mode_of d))
- (all_derivations_of thy modes' vs t)))
- | p => error (string_of_prem thy p))
- ps))
+ if #reorder_premises mode_analysis_options then
+ partial_hd (sort (premise_ord thy modes) (ps ~~ map choose_mode_of_prem ps))
+ else
+ SOME (hd ps, choose_mode_of_prem (hd ps))
end
-fun check_mode_clause' use_random thy param_vs modes mode (ts, ps) =
+fun check_mode_clause' mode_analysis_options thy 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 modes' = modes @ (param_vs ~~ map (fn x => [(x, false)]) (ho_arg_modes_of mode))
- val (in_ts, out_ts) = split_mode mode 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))
+ val (pos_modes', neg_modes') =
+ if #infer_pos_and_neg_modes mode_analysis_options then
+ (retrieve_modes_of_pol pol modes', retrieve_modes_of_pol (not pol) modes')
+ else
+ let
+ val modes = map (fn (s, ms) => (s, map (fn ((p, m), r) => m) ms)) modes'
+ in (modes, modes) end
+ val (in_ts, out_ts) = split_mode mode ts
val in_vs = maps (vars_of_destructable_term thy) in_ts
val out_vs = terms_vs out_ts
+ fun known_vs_after p vs = (case p of
+ Prem t => union (op =) vs (term_vs t)
+ | Sidecond t => union (op =) vs (term_vs t)
+ | Negprem t => union (op =) vs (term_vs t)
+ | _ => error "I do not know")
fun check_mode_prems acc_ps rnd vs [] = SOME (acc_ps, vs, rnd)
| check_mode_prems acc_ps rnd vs ps =
- (case select_mode_prem' thy modes' vs ps of
- SOME (p, SOME (deriv, [])) => check_mode_prems ((p, deriv) :: acc_ps) rnd (*TODO: uses random? *)
- (case p of
- Prem t => union (op =) vs (term_vs t)
- | Sidecond t => vs
- | Negprem t => union (op =) vs (term_vs t)
- | _ => error "I do not know")
- (filter_out (equal p) ps)
+ (case
+ (select_mode_prem mode_analysis_options thy pol (modes', (pos_modes', neg_modes')) vs ps) of
+ SOME (p, SOME (deriv, [])) => check_mode_prems ((p, deriv) :: acc_ps) rnd
+ (known_vs_after p vs) (filter_out (equal p) ps)
| SOME (p, SOME (deriv, missing_vars)) =>
- if use_random then
+ if #use_random mode_analysis_options andalso pol then
check_mode_prems ((p, deriv) :: (map
- (fn v => (Generator (v, the (AList.lookup (op =) vTs v)), Term Output)) missing_vars)
- @ acc_ps) true
- (case p of
- Prem t => union (op =) vs (term_vs t)
- | Sidecond t => union (op =) vs (term_vs t)
- | Negprem t => union (op =) vs (term_vs t)
- | _ => error "I do not know")
- (filter_out (equal p) ps)
+ (fn v => (Generator (v, the (AList.lookup (op =) vTs v)), Term Output))
+ (distinct (op =) missing_vars))
+ @ acc_ps) true (known_vs_after p vs) (filter_out (equal p) ps)
else NONE
| SOME (p, NONE) => NONE
| NONE => NONE)
@@ -1201,11 +1238,11 @@
if forall (is_constructable thy vs) (in_ts @ out_ts) then
SOME (ts, rev acc_ps, rnd)
else
- if use_random then
+ if #use_random mode_analysis_options andalso pol then
let
- val generators = map
+ val generators = map
(fn v => (Generator (v, the (AList.lookup (op =) vTs v)), Term Output))
- (subtract (op =) vs (terms_vs out_ts))
+ (subtract (op =) vs (terms_vs (in_ts @ out_ts)))
in
SOME (ts, rev (generators @ acc_ps), true)
end
@@ -1215,66 +1252,120 @@
datatype result = Success of bool | Error of string
-fun check_modes_pred' use_random options thy param_vs clauses modes (p, ms) =
+fun check_modes_pred' mode_analysis_options options thy param_vs clauses modes (p, (ms : ((bool * mode) * bool) list)) =
let
fun split xs =
let
fun split' [] (ys, zs) = (rev ys, rev zs)
| split' ((m, Error z) :: xs) (ys, zs) = split' xs (ys, z :: zs)
- | split' ((m, Success rnd) :: xs) (ys, zs) = split' xs ((m, rnd) :: ys, zs)
+ | split' (((m : bool * mode), Success rnd) :: xs) (ys, zs) = split' xs ((m, rnd) :: ys, zs)
in
split' xs ([], [])
end
val rs = these (AList.lookup (op =) clauses p)
fun check_mode m =
let
- val res = map (check_mode_clause' use_random thy param_vs modes m) rs
+ val res = Output.cond_timeit false "work part of check_mode for one mode" (fn _ =>
+ map (check_mode_clause' mode_analysis_options thy param_vs modes m) rs)
in
+ Output.cond_timeit false "aux part of check_mode for one mode" (fn _ =>
case find_indices is_none res of
[] => Success (exists (fn SOME (_, _, true) => true | _ => false) res)
- | is => (print_failed_mode options thy modes p m rs is; Error (error_of p m is))
+ | is => (print_failed_mode options thy modes p m rs is; Error (error_of p m is)))
end
- val res = map (fn (m, _) => (m, check_mode m)) ms
+ val _ = if show_mode_inference options then
+ tracing ("checking " ^ string_of_int (length ms) ^ " modes ...")
+ else ()
+ val res = Output.cond_timeit false "check_mode" (fn _ => map (fn (m, _) => (m, check_mode m)) ms)
val (ms', errors) = split res
in
- ((p, ms'), errors)
+ ((p, (ms' : ((bool * mode) * bool) list)), errors)
end;
-fun get_modes_pred' use_random thy param_vs clauses modes (p, ms) =
+fun get_modes_pred' mode_analysis_options thy param_vs clauses modes (p, ms) =
let
val rs = these (AList.lookup (op =) clauses p)
in
(p, map (fn (m, rnd) =>
- (m, map ((fn (ts, ps, rnd) => (ts, ps)) o the o check_mode_clause' use_random thy param_vs modes m) rs)) ms)
+ (m, map
+ ((fn (ts, ps, rnd) => (ts, ps)) o the o
+ check_mode_clause' mode_analysis_options thy param_vs modes m) rs)) ms)
end;
-fun fixp f x =
+fun fixp f (x : (string * ((bool * mode) * bool) list) list) =
let val y = f x
in if x = y then x else fixp f y end;
-fun fixp_with_state f (x, state) =
+fun fixp_with_state f (x : (string * ((bool * mode) * bool) list) list, state) =
let
val (y, state') = f (x, state)
in
if x = y then (y, state') else fixp_with_state f (y, state')
end
-fun infer_modes use_random options preds extra_modes param_vs clauses thy =
+fun string_of_ext_mode ((pol, mode), rnd) =
+ string_of_mode mode ^ "(" ^ (if pol then "pos" else "neg") ^ ", "
+ ^ (if rnd then "rnd" else "nornd") ^ ")"
+
+fun print_extra_modes options modes =
+ if show_mode_inference options then
+ tracing ("Modes of inferred predicates: " ^
+ cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map string_of_ext_mode ms)) modes))
+ else ()
+
+fun infer_modes mode_analysis_options options compilation preds all_modes param_vs clauses thy =
let
- val all_modes = map (fn (s, T) => (s, map (rpair false) (all_modes_of_typ T))) preds
- fun needs_random s m = (m, member (op =) (#needs_random (the_pred_data thy s)) m)
- val extra_modes = map (fn (s, ms) => (s, map (needs_random s) ms)) extra_modes
- val (modes, errors) =
- fixp_with_state (fn (modes, errors) =>
+ val collect_errors = false
+ fun appair f (x1, x2) (y1, y2) = (f x1 y1, f x2 y2)
+ fun needs_random s (false, m) = ((false, m), false)
+ | needs_random s (true, m) = ((true, m), member (op =) (#needs_random (the_pred_data thy s)) m)
+ fun add_polarity_and_random_bit s b ms = map (fn m => needs_random s (b, m)) ms
+ 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? *)
+ val extra_modes =
+ if #infer_pos_and_neg_modes mode_analysis_options then
let
- val res = map
- (check_modes_pred' use_random options thy param_vs clauses (modes @ extra_modes)) modes
- in (map fst res, errors @ maps snd res) end)
- (all_modes, [])
+ val pos_extra_modes =
+ 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
+ |> filter_out (fn (name, _) => member (op =) prednames name)
+ in
+ map (fn (s, ms) => (s, (add_polarity_and_random_bit s true ms)
+ @ add_polarity_and_random_bit s false (the (AList.lookup (op =) neg_extra_modes s))))
+ pos_extra_modes
+ 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))
+ val _ = print_extra_modes options extra_modes
+ val start_modes =
+ if #infer_pos_and_neg_modes mode_analysis_options then
+ map (fn (s, ms) => (s, map (fn m => ((true, m), false)) ms @
+ (map (fn m => ((false, m), false)) ms))) all_modes
+ else
+ map (fn (s, ms) => (s, map (fn m => ((true, m), false)) ms)) all_modes
+ fun iteration modes = map
+ (check_modes_pred' mode_analysis_options options thy param_vs clauses (modes @ extra_modes))
+ modes
+ val ((modes : (string * ((bool * mode) * bool) list) list), errors) =
+ Output.cond_timeit false "Fixpount computation of mode analysis" (fn () =>
+ if collect_errors then
+ fixp_with_state (fn (modes, errors) =>
+ let
+ val (modes', new_errors) = split_list (iteration modes)
+ in (modes', errors @ flat new_errors) end) (start_modes, [])
+ else
+ (fixp (fn modes => map fst (iteration modes)) start_modes, []))
+ val moded_clauses = map (get_modes_pred' mode_analysis_options thy param_vs clauses
+ (modes @ extra_modes)) modes
val thy' = fold (fn (s, ms) => if member (op =) (map fst preds) s then
- set_needs_random s (map fst (filter (fn (_, rnd) => rnd = true) ms)) else I) modes thy
+ set_needs_random s (map_filter (fn ((true, m), true) => SOME m | _ => NONE) ms) else I)
+ modes thy
+
in
- ((map (get_modes_pred' use_random thy param_vs clauses (modes @ extra_modes)) modes, errors), thy')
+ ((moded_clauses, errors), thy')
end;
(* term construction *)
@@ -1414,14 +1505,25 @@
(v', mk_bot compfuns U')]))
end;
-fun compile_expr compilation_modifiers compfuns thy (t, deriv) additional_arguments =
+fun string_of_tderiv thy (t, deriv) =
+ (case (t, deriv) of
+ (t1 $ t2, Mode_App (deriv1, deriv2)) =>
+ string_of_tderiv thy (t1, deriv1) ^ " $ " ^ string_of_tderiv thy (t2, deriv2)
+ | (Const ("Pair", _) $ t1 $ t2, Mode_Pair (deriv1, deriv2)) =>
+ "(" ^ string_of_tderiv thy (t1, deriv1) ^ ", " ^ string_of_tderiv thy (t2, deriv2) ^ ")"
+ | (t, Term Input) => Syntax.string_of_term_global thy t ^ "[Input]"
+ | (t, Term Output) => Syntax.string_of_term_global thy t ^ "[Output]"
+ | (t, Context m) => Syntax.string_of_term_global thy t ^ "[" ^ string_of_mode m ^ "]")
+
+fun compile_expr compilation_modifiers compfuns thy pol (t, deriv) additional_arguments =
let
fun expr_of (t, deriv) =
(case (t, deriv) of
(t, Term Input) => SOME t
| (t, Term Output) => NONE
| (Const (name, T), Context mode) =>
- SOME (Const (function_name_of (Comp_Mod.compilation compilation_modifiers) thy name mode,
+ SOME (Const (function_name_of (Comp_Mod.compilation compilation_modifiers) thy name
+ (pol, mode),
Comp_Mod.funT_of compilation_modifiers mode T))
| (Free (s, T), Context m) =>
SOME (Free (s, Comp_Mod.funT_of compilation_modifiers m T))
@@ -1446,7 +1548,7 @@
end
fun compile_clause compilation_modifiers compfuns thy all_vs param_vs additional_arguments
- mode inp (ts, moded_ps) =
+ (pol, mode) inp (ts, moded_ps) =
let
val iss = ho_arg_modes_of mode
val compile_match = compile_match compilation_modifiers compfuns
@@ -1479,7 +1581,7 @@
let
val u =
compile_expr compilation_modifiers compfuns thy
- (t, deriv) additional_arguments'
+ pol (t, deriv) additional_arguments'
val (_, out_ts''') = split_mode mode (snd (strip_comb t))
val rest = compile_prems out_ts''' vs' names'' ps
in
@@ -1489,7 +1591,7 @@
let
val u = mk_not compfuns
(compile_expr compilation_modifiers compfuns thy
- (t, deriv) additional_arguments')
+ (not pol) (t, deriv) additional_arguments')
val (_, out_ts''') = split_mode mode (snd (strip_comb t))
val rest = compile_prems out_ts''' vs' names'' ps
in
@@ -1506,6 +1608,7 @@
| Generator (v, T) =>
let
val u = mk_random T
+
val rest = compile_prems [Free (v, T)] vs' names'' ps;
in
(u, rest)
@@ -1519,7 +1622,7 @@
mk_bind compfuns (mk_single compfuns inp, prem_t)
end
-fun compile_pred compilation_modifiers thy all_vs param_vs s T mode moded_cls =
+fun compile_pred compilation_modifiers thy all_vs param_vs s T (pol, mode) moded_cls =
let
(* TODO: val additional_arguments = Comp_Mod.additional_arguments compilation_modifiers
(all_vs @ param_vs)
@@ -1547,14 +1650,14 @@
(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 compfuns
- thy all_vs param_vs additional_arguments mode (HOLogic.mk_tuple in_ts')) moded_cls;
+ thy all_vs param_vs additional_arguments (pol, 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 fun_const =
- Const (function_name_of (Comp_Mod.compilation compilation_modifiers) thy s mode, funT)
+ Const (function_name_of (Comp_Mod.compilation compilation_modifiers) thy s (pol, mode), funT)
in
HOLogic.mk_Trueprop
(HOLogic.mk_eq (list_comb (fun_const, in_ts @ additional_arguments), compilation))
@@ -1583,13 +1686,20 @@
| strip_split_abs (Abs (_, _, t)) = strip_split_abs t
| strip_split_abs t = t
-fun mk_args is_eval (Pair (m1, m2), Type ("*", [T1, T2])) names =
- let
- val (t1, names') = mk_args is_eval (m1, T1) names
- val (t2, names'') = mk_args is_eval (m2, T2) names'
- in
- (HOLogic.mk_prod (t1, t2), names'')
- end
+fun mk_args is_eval (m as Pair (m1, m2), T as Type ("*", [T1, T2])) names =
+ if eq_mode (m, Input) orelse eq_mode (m, Output) then
+ let
+ val x = Name.variant names "x"
+ in
+ (Free (x, T), x :: names)
+ end
+ else
+ let
+ val (t1, names') = mk_args is_eval (m1, T1) names
+ val (t2, names'') = mk_args is_eval (m2, T2) names'
+ in
+ (HOLogic.mk_prod (t1, t2), names'')
+ end
| mk_args is_eval ((m as Fun _), T) names =
let
val funT = funT_of PredicateCompFuns.compfuns m T
@@ -1828,11 +1938,11 @@
(* corresponds to compile_fun -- maybe call that also compile_sidecond? *)
-fun prove_sidecond thy modes t =
+fun prove_sidecond thy t =
let
fun preds_of t nameTs = case strip_comb t of
(f as Const (name, T), args) =>
- if AList.defined (op =) modes name then (name, T) :: nameTs
+ if is_registered thy name then (name, T) :: nameTs
else fold preds_of args nameTs
| _ => nameTs
val preds = preds_of t []
@@ -1847,7 +1957,7 @@
(* need better control here! *)
end
-fun prove_clause options thy nargs modes mode (_, clauses) (ts, moded_ps) =
+fun prove_clause options thy nargs mode (_, clauses) (ts, moded_ps) =
let
val (in_ts, clause_out_ts) = split_mode mode ts;
fun prove_prems out_ts [] =
@@ -1911,7 +2021,7 @@
| Sidecond t =>
rtac @{thm if_predI} 1
THEN print_tac' options "before sidecond:"
- THEN prove_sidecond thy modes t
+ THEN prove_sidecond thy t
THEN print_tac' options "after sidecond:"
THEN prove_prems [] ps)
in (prove_match options thy out_ts)
@@ -1929,7 +2039,7 @@
| select_sup _ 1 = [rtac @{thm supI1}]
| select_sup n i = (rtac @{thm supI2})::(select_sup (n - 1) (i - 1));
-fun prove_one_direction options thy clauses preds modes pred mode moded_clauses =
+fun prove_one_direction options thy clauses preds pred mode moded_clauses =
let
val T = the (AList.lookup (op =) preds pred)
val nargs = length (binder_types T)
@@ -1942,7 +2052,7 @@
THEN (EVERY (map
(fn i => EVERY' (select_sup (length moded_clauses) i) i)
(1 upto (length moded_clauses))))
- THEN (EVERY (map2 (prove_clause options thy nargs modes mode) clauses moded_clauses))
+ THEN (EVERY (map2 (prove_clause options thy nargs mode) clauses moded_clauses))
THEN print_tac' options "proved one direction"
end;
@@ -2026,10 +2136,10 @@
(* FIXME: what is this for? *)
(* replace defined by has_mode thy pred *)
(* TODO: rewrite function *)
-fun prove_sidecond2 thy modes t = let
+fun prove_sidecond2 thy t = let
fun preds_of t nameTs = case strip_comb t of
(f as Const (name, T), args) =>
- if AList.defined (op =) modes name then (name, T) :: nameTs
+ if is_registered thy name then (name, T) :: nameTs
else fold preds_of args nameTs
| _ => nameTs
val preds = preds_of t []
@@ -2044,7 +2154,7 @@
THEN print_tac "after sidecond2 simplification"
end
-fun prove_clause2 thy modes pred mode (ts, ps) i =
+fun prove_clause2 thy pred mode (ts, ps) i =
let
val pred_intro_rule = nth (intros_of thy pred) (i - 1)
val (in_ts, clause_out_ts) = split_mode mode ts;
@@ -2102,7 +2212,7 @@
| Sidecond t =>
etac @{thm bindE} 1
THEN etac @{thm if_predE} 1
- THEN prove_sidecond2 thy modes t
+ THEN prove_sidecond2 thy t
THEN prove_prems2 [] ps)
in print_tac "before prove_match2:"
THEN prove_match2 thy out_ts
@@ -2119,11 +2229,11 @@
THEN prems_tac
end;
-fun prove_other_direction options thy modes pred mode moded_clauses =
+fun prove_other_direction options thy pred mode moded_clauses =
let
fun prove_clause clause i =
(if i < length moded_clauses then etac @{thm supE} 1 else all_tac)
- THEN (prove_clause2 thy modes pred mode clause i)
+ THEN (prove_clause2 thy pred mode clause i)
in
(DETERM (TRY (rtac @{thm unit.induct} 1)))
THEN (REPEAT_DETERM (CHANGED (rewtac @{thm split_paired_all})))
@@ -2136,7 +2246,7 @@
(** proof procedure **)
-fun prove_pred options thy clauses preds modes pred mode (moded_clauses, compiled_term) =
+fun prove_pred options thy clauses preds pred (pol, mode) (moded_clauses, compiled_term) =
let
val ctxt = ProofContext.init thy
val clauses = case AList.lookup (op =) clauses pred of SOME rs => rs | NONE => []
@@ -2146,9 +2256,9 @@
(fn _ =>
rtac @{thm pred_iffI} 1
THEN print_tac' options "after pred_iffI"
- THEN prove_one_direction options thy clauses preds modes pred mode moded_clauses
+ THEN prove_one_direction options thy clauses preds pred mode moded_clauses
THEN print_tac' options "proved one direction"
- THEN prove_other_direction options thy modes pred mode moded_clauses
+ THEN prove_other_direction options thy pred mode moded_clauses
THEN print_tac' options "proved other direction")
else (fn _ => Skip_Proof.cheat_tac thy))
end;
@@ -2173,11 +2283,11 @@
map_preds_modes (fn pred => compile_pred comp_modifiers thy all_vs param_vs pred
(the (AList.lookup (op =) preds pred))) moded_clauses
-fun prove options thy clauses preds modes moded_clauses compiled_terms =
- map_preds_modes (prove_pred options thy clauses preds modes)
+fun prove options thy clauses preds moded_clauses compiled_terms =
+ map_preds_modes (prove_pred options thy clauses preds)
(join_preds_modes moded_clauses compiled_terms)
-fun prove_by_skip options thy _ _ _ _ compiled_terms =
+fun prove_by_skip options thy _ _ _ compiled_terms =
map_preds_modes
(fn pred => fn mode => fn t => Drule.export_without_context (Skip_Proof.make_thm thy t))
compiled_terms
@@ -2204,9 +2314,13 @@
val ([preds, intrs], _) = fold_burrow (Variable.import_terms false) [preds, intrs]
(ProofContext.init thy)
val preds = map dest_Const preds
- val extra_modes =
- all_modes_of compilation thy |> filter_out (fn (name, _) => member (op =) prednames name)
val all_vs = terms_vs intrs
+ val all_modes =
+ map (fn (s, T) =>
+ (s,
+ (if member (op =) (no_higher_order_predicate options) s then
+ (all_smodes_of_typ T)
+ else (all_modes_of_typ T)))) preds
val params =
case intrs of
[] =>
@@ -2219,8 +2333,12 @@
in
map2 (curry Free) param_names paramTs
end
- | (intr :: _) => maps extract_params
- (snd (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl intr))))
+ | (intr :: _) =>
+ let
+ val (p, args) = strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl intr))
+ in
+ ho_args_of (hd (the (AList.lookup (op =) all_modes (fst (dest_Const p))))) args
+ end
val param_vs = map (fst o dest_Free) params
fun add_clause intr clauses =
let
@@ -2232,7 +2350,7 @@
end;
val clauses = fold add_clause intrs []
in
- (preds, all_vs, param_vs, extra_modes, clauses)
+ (preds, all_vs, param_vs, all_modes, clauses)
end;
(* sanity check of introduction rules *)
@@ -2294,7 +2412,7 @@
val arg_names = Name.variant_list []
(map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
val args = map2 (curry Free) arg_names Ts
- val predfun = Const (function_name_of Pred thy predname full_mode,
+ val predfun = Const (function_name_of Pred thy predname (true, full_mode),
Ts ---> PredicateCompFuns.mk_predT @{typ unit})
val rhs = @{term Predicate.holds} $ (list_comb (predfun, args))
val eq_term = HOLogic.mk_Trueprop
@@ -2317,20 +2435,20 @@
datatype steps = Steps of
{
- define_functions : options -> (string * typ) list -> string * mode list -> theory -> theory,
- infer_modes : options -> (string * typ) list -> (string * mode list) list
+ 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 -> (string * mode 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
-> (string * thm list) list -> (string * thm list) list,
comp_modifiers : Comp_Mod.comp_modifiers,
+ use_random : bool,
qname : bstring
}
-fun add_equations_of steps options prednames thy =
+fun add_equations_of steps mode_analysis_options options prednames thy =
let
fun dest_steps (Steps s) = s
val _ = print_step options
@@ -2338,14 +2456,20 @@
(*val _ = check_intros_elim_match thy prednames*)
(*val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames)*)
val compilation = Comp_Mod.compilation (#comp_modifiers (dest_steps steps))
- val (preds, all_vs, param_vs, extra_modes, clauses) =
+ val _ =
+ if show_intermediate_results options then
+ tracing (commas (map (Display.string_of_thm_global thy) (maps (intros_of thy) prednames)))
+ else ()
+ val (preds, all_vs, param_vs, all_modes, clauses) =
prepare_intrs options compilation thy prednames (maps (intros_of thy) prednames)
val _ = print_step options "Infering modes..."
val ((moded_clauses, errors), thy') =
- #infer_modes (dest_steps steps) options preds extra_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 extra_modes errors
+ (*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'
@@ -2355,8 +2479,8 @@
compile_preds (#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 (extra_modes @ modes)
- moded_clauses compiled_terms
+ val result_thms =
+ #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)
@@ -2398,7 +2522,14 @@
val thy'' = fold_rev
(fn preds => fn thy =>
if not (forall (defined thy) preds) then
- add_equations_of steps options preds thy
+ let
+ val mode_analysis_options = {use_random = #use_random (dest_steps steps),
+ reorder_premises =
+ not (no_topmost_reordering options andalso not (null (inter (op =) preds names))),
+ infer_pos_and_neg_modes = #use_random (dest_steps steps)}
+ in
+ add_equations_of steps mode_analysis_options options preds thy
+ end
else thy)
scc thy' |> Theory.checkpoint
in thy'' end
@@ -2468,11 +2599,15 @@
}
val add_equations = gen_add_equations
- (Steps {infer_modes = infer_modes false,
- define_functions = create_definitions,
+ (Steps {
+ define_functions =
+ fn options => fn preds => fn (s, modes) =>
+ create_definitions
+ options preds (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes),
prove = prove,
add_code_equations = add_code_equations,
comp_modifiers = predicate_comp_modifiers,
+ use_random = false,
qname = "equation"})
val annotated_comp_modifiers = Comp_Mod.Comp_Modifiers
@@ -2499,9 +2634,9 @@
transform_additional_arguments = K I : (indprem -> term list -> term list)
}
-val random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
+val pos_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
{
- compilation = Random_DSeq,
+ compilation = Pos_Random_DSeq,
function_name_prefix = "random_dseq_",
compfuns = Random_Sequence_CompFuns.compfuns,
additional_arguments = K [],
@@ -2510,6 +2645,17 @@
transform_additional_arguments = K I : (indprem -> term list -> term list)
}
+val neg_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
+ {
+ compilation = Neg_Random_DSeq,
+ function_name_prefix = "random_dseq_neg_",
+ compfuns = Random_Sequence_CompFuns.compfuns,
+ additional_arguments = K [],
+ wrap_compilation = K (K (K (K (K I))))
+ : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
+ transform_additional_arguments = K I : (indprem -> term list -> term list)
+ }
+
(*
val add_depth_limited_equations = gen_add_equations
(Steps {infer_modes = infer_modes,
@@ -2521,11 +2667,15 @@
qname = "depth_limited_equation"})
*)
val add_annotated_equations = gen_add_equations
- (Steps {infer_modes = infer_modes false,
- define_functions = define_functions annotated_comp_modifiers PredicateCompFuns.compfuns,
+ (Steps {
+ define_functions =
+ fn options => fn preds => fn (s, modes) =>
+ define_functions annotated_comp_modifiers PredicateCompFuns.compfuns options preds
+ (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes),
prove = prove_by_skip,
add_code_equations = K (K I),
comp_modifiers = annotated_comp_modifiers,
+ use_random = false,
qname = "annotated_equation"})
(*
val add_quickcheck_equations = gen_add_equations
@@ -2538,19 +2688,33 @@
qname = "random_equation"})
*)
val add_dseq_equations = gen_add_equations
- (Steps {infer_modes = infer_modes false,
- define_functions = define_functions dseq_comp_modifiers DSequence_CompFuns.compfuns,
+ (Steps {
+ define_functions =
+ fn options => fn preds => fn (s, modes) =>
+ define_functions dseq_comp_modifiers DSequence_CompFuns.compfuns
+ options preds (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes),
prove = prove_by_skip,
add_code_equations = K (K I),
comp_modifiers = dseq_comp_modifiers,
+ use_random = false,
qname = "dseq_equation"})
val add_random_dseq_equations = gen_add_equations
- (Steps {infer_modes = infer_modes true,
- define_functions = define_functions random_dseq_comp_modifiers Random_Sequence_CompFuns.compfuns,
+ (Steps {
+ define_functions =
+ fn options => fn preds => fn (s, modes) =>
+ let
+ val pos_modes = map_filter (fn (true, m) => SOME m | _ => NONE) modes
+ val neg_modes = map_filter (fn (false, m) => SOME m | _ => NONE) modes
+ in define_functions pos_random_dseq_comp_modifiers Random_Sequence_CompFuns.compfuns
+ options preds (s, pos_modes)
+ #> define_functions neg_random_dseq_comp_modifiers Random_Sequence_CompFuns.compfuns
+ options preds (s, neg_modes)
+ end,
prove = prove_by_skip,
add_code_equations = K (K I),
- comp_modifiers = random_dseq_comp_modifiers,
+ comp_modifiers = pos_random_dseq_comp_modifiers,
+ use_random = true,
qname = "random_dseq_equation"})
@@ -2700,8 +2864,8 @@
| Depth_Limited => depth_limited_comp_modifiers
| Annotated => annotated_comp_modifiers*)
| DSeq => dseq_comp_modifiers
- | Random_DSeq => random_dseq_comp_modifiers
- val t_pred = compile_expr comp_modifiers compfuns thy (body, deriv) additional_arguments;
+ | Random_DSeq => pos_random_dseq_comp_modifiers
+ val t_pred = compile_expr comp_modifiers compfuns thy true (body, deriv) additional_arguments;
val T_pred = dest_predT compfuns (fastype_of t_pred)
val arrange = split_lambda (HOLogic.mk_tuple outargs) output_tuple
in
@@ -2717,7 +2881,7 @@
case compilation of
Random => RandomPredCompFuns.compfuns
| DSeq => DSequence_CompFuns.compfuns
- | Random_DSeq => Random_Sequence_CompFuns.compfuns
+ | Pos_Random_DSeq => Random_Sequence_CompFuns.compfuns
| _ => PredicateCompFuns.compfuns
val t = analyze_compr thy compfuns param_user_modes options t_compr;
val T = dest_predT compfuns (fastype_of t);
@@ -2729,7 +2893,7 @@
(Code_Eval.eval NONE ("Predicate_Compile_Core.random_eval_ref", random_eval_ref)
(fn proc => fn g => fn s => g s |>> Predicate.map proc) thy t' []
|> Random_Engine.run))
- | Random_DSeq =>
+ | Pos_Random_DSeq =>
let
val [nrandom, size, depth] = arguments
in
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Tue Feb 23 12:14:46 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Tue Feb 23 14:00:36 2010 +0100
@@ -6,11 +6,17 @@
signature PREDICATE_COMPILE_DATA =
sig
- type specification_table;
- (*val make_const_spec_table : Predicate_Compile_Aux.options -> theory -> specification_table*)
- val get_specification : theory -> term -> thm list
+ val ignore_consts : string list -> theory -> theory
+ val keep_functions : string list -> theory -> theory
+ val keep_function : theory -> string -> bool
+ val processed_specs : theory -> string -> (string * thm list) list option
+ val store_processed_specs : (string * (string * thm list) list) -> theory -> theory
+
+ val get_specification : Predicate_Compile_Aux.options -> theory -> term -> thm list
val obtain_specification_graph :
Predicate_Compile_Aux.options -> theory -> term -> thm list TermGraph.T
+
+ val present_graph : thm list TermGraph.T -> unit
val normalize_equation : theory -> thm -> thm
end;
@@ -22,20 +28,39 @@
structure Data = Theory_Data
(
type T =
- {const_spec_table : thm list Symtab.table};
+ {ignore_consts : unit Symtab.table,
+ keep_functions : unit Symtab.table,
+ processed_specs : ((string * thm list) list) Symtab.table};
val empty =
- {const_spec_table = Symtab.empty};
+ {ignore_consts = Symtab.empty,
+ keep_functions = Symtab.empty,
+ processed_specs = Symtab.empty};
val extend = I;
fun merge
- ({const_spec_table = const_spec_table1},
- {const_spec_table = const_spec_table2}) =
- {const_spec_table = Symtab.merge (K true) (const_spec_table1, const_spec_table2)}
+ ({ignore_consts = c1, keep_functions = k1, processed_specs = s1},
+ {ignore_consts = c2, keep_functions = k2, processed_specs = s2}) =
+ {ignore_consts = Symtab.merge (K true) (c1, c2),
+ keep_functions = Symtab.merge (K true) (k1, k2),
+ processed_specs = Symtab.merge (K true) (s1, s2)}
);
-fun mk_data c = {const_spec_table = c}
-fun map_data f {const_spec_table = c} = mk_data (f c)
+
+
+fun mk_data (c, k, s) = {ignore_consts = c, keep_functions = k, processed_specs = s}
+fun map_data f {ignore_consts = c, keep_functions = k, processed_specs = s} = mk_data (f (c, k, s))
+
+fun ignore_consts cs = Data.map (map_data (apfst3 (fold (fn c => Symtab.insert (op =) (c, ())) cs)))
+
+fun keep_functions cs = Data.map (map_data (apsnd3 (fold (fn c => Symtab.insert (op =) (c, ())) cs)))
-type specification_table = thm list Symtab.table
+fun keep_function thy = Symtab.defined (#keep_functions (Data.get thy))
+
+fun processed_specs thy = Symtab.lookup (#processed_specs (Data.get thy))
+
+fun store_processed_specs (constname, specs) =
+ Data.map (map_data (aptrd3 (Symtab.update_new (constname, specs))))
+(* *)
+
fun defining_term_of_introrule_term t =
let
@@ -120,17 +145,11 @@
val t' = Pattern.rewrite_term thy rewr [] t
val tac = Skip_Proof.cheat_tac thy
val th'' = Goal.prove ctxt (Term.add_free_names t' []) [] t' (fn _ => tac)
- val th''' = LocalDefs.unfold ctxt [@{thm split_conv}] th''
+ val th''' = LocalDefs.unfold ctxt [@{thm split_conv}, @{thm fst_conv}, @{thm snd_conv}] th''
in
th'''
end;
-fun normalize_equation thy th =
- mk_meta_equation th
- |> Predicate_Compile_Set.unfold_set_notation
- |> full_fun_cong_expand
- |> split_all_pairs thy
- |> tap check_equation_format
fun inline_equations thy th =
let
@@ -143,69 +162,58 @@
in
th'
end
-(*
-fun store_thm_in_table options ignore thy th=
- let
- val th = th
- |> inline_equations options thy
- |> Predicate_Compile_Set.unfold_set_notation
- |> AxClass.unoverload thy
- val (const, th) =
- if is_equationlike th then
- let
- val eq = normalize_equation thy th
- in
- (defining_const_of_equation eq, eq)
- end
- else if is_introlike th then (defining_const_of_introrule th, th)
- else error "store_thm: unexpected definition format"
- in
- if ignore const then I else Symtab.cons_list (const, th)
- end
+
+fun normalize_equation thy th =
+ mk_meta_equation th
+ |> full_fun_cong_expand
+ |> split_all_pairs thy
+ |> tap check_equation_format
+ |> inline_equations thy
-fun make_const_spec_table options thy =
+fun normalize_intros thy th =
+ split_all_pairs thy th
+ |> inline_equations thy
+
+fun normalize thy th =
+ if is_equationlike th then
+ normalize_equation thy th
+ else
+ normalize_intros thy th
+
+fun get_specification options thy t =
let
- fun store ignore f =
- fold (store_thm_in_table options ignore thy)
- (map (Thm.transfer thy) (f ))
- val table = Symtab.empty
- |> store (K false) Predicate_Compile_Alternative_Defs.get
- val ignore = Symtab.defined table
- in
- table
- |> store ignore (fn ctxt => maps
- else [])
-
- |> store ignore Nitpick_Simps.get
- |> store ignore Nitpick_Intros.get
- end
-
-fun get_specification table constname =
- case Symtab.lookup table constname of
- SOME thms => thms
- | NONE => error ("get_specification: lookup of constant " ^ quote constname ^ " failed")
-*)
-
-fun get_specification thy t =
- Output.cond_timeit true "get_specification" (fn () =>
- let
+ (*val (c, T) = dest_Const t
+ val t = Const (AxClass.unoverload_const thy (c, T), T)*)
+ val _ = if show_steps options then
+ tracing ("getting specification of " ^ Syntax.string_of_term_global thy t ^
+ " with type " ^ Syntax.string_of_typ_global thy (fastype_of t))
+ else ()
val ctxt = ProofContext.init thy
fun filtering th =
if is_equationlike th andalso
- defining_const_of_equation (normalize_equation thy th) = (fst (dest_Const t)) then
+ defining_const_of_equation (normalize_equation thy th) = fst (dest_Const t) then
SOME (normalize_equation thy th)
else
if is_introlike th andalso defining_term_of_introrule th = t then
SOME th
else
NONE
- in
- case map_filter filtering (map (Thm.transfer thy) (Predicate_Compile_Alternative_Defs.get ctxt))
+ val spec = case map_filter filtering (map (normalize thy o Thm.transfer thy) (Predicate_Compile_Alternative_Defs.get ctxt))
of [] => (case Spec_Rules.retrieve ctxt t
- of [] => rev (map_filter filtering (map (Thm.transfer thy) (Nitpick_Intros.get ctxt)))
+ of [] => (case rev (
+ (map_filter filtering (map (normalize_intros thy o Thm.transfer thy)
+ (Nitpick_Intros.get ctxt))))
+ of [] => error ("No specification for " ^ (Syntax.string_of_term_global thy t))
+ | ths => ths)
| ((_, (_, ths)) :: _) => map (normalize_equation thy o Thm.transfer thy) ths)
| ths => rev ths
- end)
+ val _ =
+ if show_intermediate_results options then
+ Output.tracing (commas (map (Display.string_of_thm_global thy) spec))
+ else ()
+ in
+ spec
+ end
val logic_operator_names =
[@{const_name "=="},
@@ -216,7 +224,8 @@
@{const_name "op -->"},
@{const_name "All"},
@{const_name "Ex"},
- @{const_name "op &"}]
+ @{const_name "op &"},
+ @{const_name "op |"}]
fun special_cases (c, T) = member (op =) [
@{const_name Product_Type.Unity},
@@ -233,7 +242,11 @@
@{const_name Int.Bit1},
@{const_name Int.Pls},
@{const_name Int.zero_int_inst.zero_int},
- @{const_name List.filter}] c
+ @{const_name List.filter},
+ @{const_name HOL.If},
+ @{const_name Groups.minus}
+ ] c
+
fun print_specification options thy constname specs =
if show_intermediate_results options then
@@ -254,19 +267,43 @@
|> filter_out has_code_pred_intros
|> filter_out case_consts
|> filter_out special_cases
+ |> filter_out (fn (c, _) => Symtab.defined (#ignore_consts (Data.get thy)) c)
+ |> map (fn (c, _) => (c, Sign.the_const_constraint thy c))
|> map Const
(*
|> filter is_defining_constname*)
fun extend t =
let
- val specs = get_specification thy t
- |> map (inline_equations thy)
+ val specs = get_specification options thy t
(*|> Predicate_Compile_Set.unfold_set_notation*)
(*val _ = print_specification options thy constname specs*)
in (specs, defiants_of specs) end;
in
TermGraph.extend extend t TermGraph.empty
end;
-
+
+
+fun present_graph gr =
+ let
+ fun eq_cname (Const (c1, _), Const (c2, _)) = (c1 = c2)
+ fun string_of_const (Const (c, _)) = c
+ | string_of_const _ = error "string_of_const: unexpected term"
+ val constss = TermGraph.strong_conn gr;
+ val mapping = Termtab.empty |> fold (fn consts => fold (fn const =>
+ Termtab.update (const, consts)) consts) constss;
+ fun succs consts = consts
+ |> maps (TermGraph.imm_succs gr)
+ |> subtract eq_cname consts
+ |> map (the o Termtab.lookup mapping)
+ |> distinct (eq_list eq_cname);
+ val conn = [] |> fold (fn consts => cons (consts, succs consts)) constss;
+
+ fun namify consts = map string_of_const consts
+ |> commas;
+ val prgr = map (fn (consts, constss) =>
+ { name = namify consts, ID = namify consts, dir = "", unfold = true,
+ path = "", parents = map namify constss }) conn;
+ in Present.display_graph prgr end;
+
end;
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Tue Feb 23 12:14:46 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Tue Feb 23 14:00:36 2010 +0100
@@ -9,6 +9,8 @@
val define_predicates : (string * thm list) list -> theory -> (string * thm list) list * theory
val rewrite_intro : theory -> thm -> thm list
val pred_of_function : theory -> string -> string option
+
+ val add_function_predicate_translation : (term * term) -> theory -> theory
end;
structure Predicate_Compile_Fun : PREDICATE_COMPILE_FUN =
@@ -16,19 +18,36 @@
open Predicate_Compile_Aux;
-(* Table from constant name (string) to term of inductive predicate *)
-structure Pred_Compile_Preproc = Theory_Data
+(* Table from function to inductive predicate *)
+structure Fun_Pred = Theory_Data
(
- type T = string Symtab.table;
- val empty = Symtab.empty;
+ type T = (term * term) Item_Net.T;
+ val empty = Item_Net.init (op aconv o pairself fst) (single o fst);
val extend = I;
- fun merge data : T = Symtab.merge (op =) data; (* FIXME handle Symtab.DUP ?? *)
+ val merge = Item_Net.merge;
)
-fun pred_of_function thy name = Symtab.lookup (Pred_Compile_Preproc.get thy) name
+fun lookup thy net t =
+ case Item_Net.retrieve net t of
+ [] => NONE
+ | [(f, p)] =>
+ let
+ val subst = Pattern.match thy (f, t) (Vartab.empty, Vartab.empty)
+ in
+ SOME (Envir.subst_term subst p)
+ end
+ | _ => error ("Multiple matches possible for lookup of " ^ Syntax.string_of_term_global thy t)
-fun defined thy = Symtab.defined (Pred_Compile_Preproc.get thy)
+fun pred_of_function thy name =
+ case Item_Net.retrieve (Fun_Pred.get thy) (Const (name, Term.dummyT)) of
+ [] => NONE
+ | [(f, p)] => SOME (fst (dest_Const p))
+ | _ => error ("Multiple matches possible for lookup of constant " ^ name)
+fun defined_const thy name = is_some (pred_of_function thy name)
+
+fun add_function_predicate_translation (f, p) =
+ Fun_Pred.map (Item_Net.update (f, p))
fun transform_ho_typ (T as Type ("fun", _)) =
let
@@ -63,27 +82,6 @@
(Free (Long_Name.base_name name ^ "P", pred_type T))
end
-fun mk_param thy lookup_pred (t as Free (v, _)) = lookup_pred t
- | mk_param thy lookup_pred t =
- if Predicate_Compile_Aux.is_predT (fastype_of t) then
- t
- else
- let
- val (vs, body) = strip_abs t
- val names = Term.add_free_names body []
- val vs_names = Name.variant_list names (map fst vs)
- val vs' = map2 (curry Free) vs_names (map snd vs)
- val body' = subst_bounds (rev vs', body)
- val (f, args) = strip_comb body'
- val resname = Name.variant (vs_names @ names) "res"
- val resvar = Free (resname, body_type (fastype_of body'))
- (*val P = case try lookup_pred f of SOME P => P | NONE => error "mk_param"
- val pred_body = list_comb (P, args @ [resvar])
- *)
- val pred_body = HOLogic.mk_eq (body', resvar)
- val param = fold_rev lambda (vs' @ [resvar]) pred_body
- in param end
-
(* creates the list of premises for every intro rule *)
(* theory -> term -> (string list, term list list) *)
@@ -92,22 +90,6 @@
val (func, args) = strip_comb lhs
in ((func, args), rhs) end;
-fun string_of_typ T = Syntax.string_of_typ_global @{theory} T
-
-fun string_of_term t =
- case t of
- Const (c, T) => "Const (" ^ c ^ ", " ^ string_of_typ T ^ ")"
- | Free (c, T) => "Free (" ^ c ^ ", " ^ string_of_typ T ^ ")"
- | Var ((c, i), T) => "Var ((" ^ c ^ ", " ^ string_of_int i ^ "), " ^ string_of_typ T ^ ")"
- | Bound i => "Bound " ^ string_of_int i
- | Abs (x, T, t) => "Abs (" ^ x ^ ", " ^ string_of_typ T ^ ", " ^ string_of_term t ^ ")"
- | t1 $ t2 => "(" ^ string_of_term t1 ^ ") $ (" ^ string_of_term t2 ^ ")"
-
-fun ind_package_get_nparams thy name =
- case try (Inductive.the_inductive (ProofContext.init thy)) name of
- SOME (_, result) => length (Inductive.params_of (#raw_induct result))
- | NONE => error ("No such predicate: " ^ quote name)
-
(* TODO: does not work with higher order functions yet *)
fun mk_rewr_eq (func, pred) =
let
@@ -122,49 +104,6 @@
(HOLogic.mk_eq (res, list_comb (func, args)), list_comb (pred, args @ [res]))
end;
-fun has_split_rule_cname @{const_name "nat_case"} = true
- | has_split_rule_cname @{const_name "list_case"} = true
- | has_split_rule_cname _ = false
-
-fun has_split_rule_term thy (Const (@{const_name "nat_case"}, _)) = true
- | has_split_rule_term thy (Const (@{const_name "list_case"}, _)) = true
- | has_split_rule_term thy _ = false
-
-fun has_split_rule_term' thy (Const (@{const_name "If"}, _)) = true
- | has_split_rule_term' thy (Const (@{const_name "Let"}, _)) = true
- | has_split_rule_term' thy c = has_split_rule_term thy c
-
-fun prepare_split_thm ctxt split_thm =
- (split_thm RS @{thm iffD2})
- |> LocalDefs.unfold ctxt [@{thm atomize_conjL[symmetric]},
- @{thm atomize_all[symmetric]}, @{thm atomize_imp[symmetric]}]
-
-fun find_split_thm thy (Const (name, typ)) =
- let
- fun split_name str =
- case first_field "." str
- of (SOME (field, rest)) => field :: split_name rest
- | NONE => [str]
- val splitted_name = split_name name
- in
- if length splitted_name > 0 andalso
- String.isSuffix "_case" (List.last splitted_name)
- then
- (List.take (splitted_name, length splitted_name - 1)) @ ["split"]
- |> space_implode "."
- |> PureThy.get_thm thy
- |> SOME
- handle ERROR msg => NONE
- else NONE
- end
- | find_split_thm _ _ = NONE
-
-fun find_split_thm' thy (Const (@{const_name "If"}, _)) = SOME @{thm split_if}
- | find_split_thm' thy (Const (@{const_name "Let"}, _)) = SOME @{thm refl} (* TODO *)
- | find_split_thm' thy c = find_split_thm thy c
-
-fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t)
-
fun folds_map f xs y =
let
fun folds_map' acc [] y = [(rev acc, y)]
@@ -174,23 +113,91 @@
folds_map' [] xs y
end;
-fun mk_prems thy (lookup_pred, get_nparams) t (names, prems) =
+fun keep_functions thy t =
+ case try dest_Const (fst (strip_comb t)) of
+ SOME (c, _) => Predicate_Compile_Data.keep_function thy c
+ | _ => false
+
+fun mk_prems thy lookup_pred t (names, prems) =
let
fun mk_prems' (t as Const (name, T)) (names, prems) =
- if is_constr thy name orelse (is_none (try lookup_pred t)) then
+ (if is_constr thy name orelse (is_none (lookup_pred t)) then
[(t, (names, prems))]
- else [(lookup_pred t, (names, prems))]
+ else
+ (*(if is_none (try lookup_pred t) then
+ [(Abs ("uu", fastype_of t, HOLogic.mk_eq (t, Bound 0)), (names, prems))]
+ else*) [(the (lookup_pred t), (names, prems))])
| mk_prems' (t as Free (f, T)) (names, prems) =
- [(lookup_pred t, (names, prems))]
+ (case lookup_pred t of
+ SOME t' => [(t', (names, prems))]
+ | NONE => [(t, (names, prems))])
| mk_prems' (t as Abs _) (names, prems) =
if Predicate_Compile_Aux.is_predT (fastype_of t) then
- [(t, (names, prems))] else error "mk_prems': Abs "
- (* mk_param *)
+ ([(Envir.eta_contract t, (names, prems))])
+ else
+ let
+ val (vars, body) = strip_abs t
+ val _ = assert (fastype_of body = body_type (fastype_of body))
+ val absnames = Name.variant_list names (map fst vars)
+ val frees = map2 (curry Free) absnames (map snd vars)
+ val body' = subst_bounds (rev frees, body)
+ val resname = Name.variant (absnames @ names) "res"
+ val resvar = Free (resname, fastype_of body)
+ val t = mk_prems' body' ([], [])
+ |> map (fn (res, (inner_names, inner_prems)) =>
+ let
+ fun mk_exists (x, T) t = HOLogic.mk_exists (x, T, t)
+ val vTs =
+ fold Term.add_frees inner_prems []
+ |> filter (fn (x, T) => member (op =) inner_names x)
+ val t =
+ fold mk_exists vTs
+ (foldr1 HOLogic.mk_conj (HOLogic.mk_eq (resvar, res) ::
+ map HOLogic.dest_Trueprop inner_prems))
+ in
+ t
+ end)
+ |> foldr1 HOLogic.mk_disj
+ |> fold lambda (resvar :: rev frees)
+ in
+ [(t, (names, prems))]
+ end
| mk_prems' t (names, prems) =
- if Predicate_Compile_Aux.is_constrt thy t then
+ if Predicate_Compile_Aux.is_constrt thy t orelse keep_functions thy t then
[(t, (names, prems))]
else
- if has_split_rule_term' thy (fst (strip_comb t)) then
+ case (fst (strip_comb t)) of
+ Const (@{const_name "If"}, _) =>
+ (let
+ val (_, [B, x, y]) = strip_comb t
+ in
+ (mk_prems' x (names, prems)
+ |> map (fn (res, (names, prems)) => (res, (names, (HOLogic.mk_Trueprop B) :: prems))))
+ @ (mk_prems' y (names, prems)
+ |> map (fn (res, (names, prems)) =>
+ (res, (names, (HOLogic.mk_Trueprop (HOLogic.mk_not B)) :: prems))))
+ end)
+ | Const (@{const_name "Let"}, _) =>
+ (let
+ val (_, [f, g]) = strip_comb t
+ in
+ mk_prems' f (names, prems)
+ |> maps (fn (res, (names, prems)) =>
+ mk_prems' (betapply (g, res)) (names, prems))
+ end)
+ | Const (@{const_name "split"}, _) =>
+ (let
+ val (_, [g, res]) = strip_comb t
+ val [res1, res2] = Name.variant_list names ["res1", "res2"]
+ val (T1, T2) = HOLogic.dest_prodT (fastype_of res)
+ val (resv1, resv2) = (Free (res1, T1), Free (res2, T2))
+ in
+ mk_prems' (betapplys (g, [resv1, resv2]))
+ (res1 :: res2 :: names,
+ HOLogic.mk_Trueprop (HOLogic.mk_eq (res, HOLogic.mk_prod (resv1, resv2))) :: prems)
+ end)
+ | _ =>
+ if has_split_thm thy (fst (strip_comb t)) then
let
val (f, args) = strip_comb t
val split_thm = prepare_split_thm (ProofContext.init thy) (the (find_split_thm' thy f))
@@ -208,8 +215,15 @@
val vars = map Free (var_names ~~ (map snd vTs))
val (prems', pre_res) = Logic.strip_horn (subst_bounds (rev vars, assm'))
val (_, [inner_t]) = strip_comb (HOLogic.dest_Trueprop pre_res)
+ val (lhss : term list, rhss) =
+ split_list (map (HOLogic.dest_eq o HOLogic.dest_Trueprop) prems')
in
- mk_prems' inner_t (var_names @ names, prems' @ prems)
+ folds_map mk_prems' lhss (var_names @ names, prems)
+ |> map (fn (ress, (names, prems)) =>
+ let
+ val prems' = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (ress ~~ rhss)
+ in (names, prems' @ prems) end)
+ |> maps (mk_prems' inner_t)
end
in
maps mk_prems_of_assm assms
@@ -219,53 +233,77 @@
val (f, args) = strip_comb t
(* TODO: special procedure for higher-order functions: split arguments in
simple types and function types *)
+ val args = map (Pattern.eta_long []) args
val resname = Name.variant names "res"
val resvar = Free (resname, body_type (fastype_of t))
+ val _ = assert (fastype_of t = body_type (fastype_of t))
val names' = resname :: names
fun mk_prems'' (t as Const (c, _)) =
- if is_constr thy c orelse (is_none (try lookup_pred t)) then
+ if is_constr thy c orelse (is_none (lookup_pred t)) then
+ let
+ val _ = ()(*tracing ("not translating function " ^ Syntax.string_of_term_global thy t)*)
+ in
folds_map mk_prems' args (names', prems) |>
map
(fn (argvs, (names'', prems')) =>
let
val prem = HOLogic.mk_Trueprop (HOLogic.mk_eq (resvar, list_comb (f, argvs)))
in (names'', prem :: prems') end)
+ end
else
let
- val pred = lookup_pred t
- val nparams = get_nparams pred
- val (params, args) = chop nparams args
- val params' = map (mk_param thy lookup_pred) params
+ (* lookup_pred is falsch für polymorphe Argumente und bool. *)
+ val pred = the (lookup_pred t)
+ val Ts = binder_types (fastype_of pred)
in
folds_map mk_prems' args (names', prems)
|> map (fn (argvs, (names'', prems')) =>
let
- val prem = HOLogic.mk_Trueprop (list_comb (pred, params' @ argvs @ [resvar]))
+ fun lift_arg T t =
+ if (fastype_of t) = T then t
+ else
+ let
+ val _ = assert (T =
+ (binder_types (fastype_of t) @ [@{typ bool}] ---> @{typ bool}))
+ fun mk_if T (b, t, e) =
+ Const (@{const_name If}, @{typ bool} --> T --> T --> T) $ b $ t $ e
+ val Ts = binder_types (fastype_of t)
+ val t =
+ list_abs (map (pair "x") Ts @ [("b", @{typ bool})],
+ mk_if @{typ bool} (list_comb (t, map Bound (length Ts downto 1)),
+ HOLogic.mk_eq (@{term True}, Bound 0),
+ HOLogic.mk_eq (@{term False}, Bound 0)))
+ in
+ t
+ end
+ (*val _ = tracing ("Ts: " ^ commas (map (Syntax.string_of_typ_global thy) Ts))
+ val _ = map2 check_arity Ts (map fastype_of (argvs @ [resvar]))*)
+ val argvs' = map2 lift_arg (fst (split_last Ts)) argvs
+ val prem = HOLogic.mk_Trueprop (list_comb (pred, argvs' @ [resvar]))
in (names'', prem :: prems') end)
end
| mk_prems'' (t as Free (_, _)) =
- let
- (* higher order argument call *)
- val pred = lookup_pred t
- in
- folds_map mk_prems' args (resname :: names, prems)
- |> map (fn (argvs, (names', prems')) =>
- let
- val prem = HOLogic.mk_Trueprop (list_comb (pred, argvs @ [resvar]))
- in (names', prem :: prems') end)
- end
+ folds_map mk_prems' args (names', prems) |>
+ map
+ (fn (argvs, (names'', prems')) =>
+ let
+ val prem =
+ case lookup_pred t of
+ NONE => HOLogic.mk_Trueprop (HOLogic.mk_eq (resvar, list_comb (f, argvs)))
+ | SOME p => HOLogic.mk_Trueprop (list_comb (p, argvs @ [resvar]))
+ in (names'', prem :: prems') end)
| mk_prems'' t =
error ("Invalid term: " ^ Syntax.string_of_term_global thy t)
in
map (pair resvar) (mk_prems'' f)
end
in
- mk_prems' t (names, prems)
+ mk_prems' (Pattern.eta_long [] t) (names, prems)
end;
(* assumption: mutual recursive predicates all have the same parameters. *)
fun define_predicates specs thy =
- if forall (fn (const, _) => member (op =) (Symtab.keys (Pred_Compile_Preproc.get thy)) const) specs then
+ if forall (fn (const, _) => defined_const thy const) specs then
([], thy)
else
let
@@ -275,36 +313,20 @@
(* create prednames *)
val ((funs, argss), rhss) = map_split dest_code_eqn eqns |>> split_list
val argss' = map (map transform_ho_arg) argss
- val pnames = map dest_Free (distinct (op =) (maps (filter (is_funtype o fastype_of)) argss'))
+ (* TODO: higher order arguments also occur in tuples! *)
+ val ho_argss = distinct (op =) (maps (filter (is_funtype o fastype_of)) argss)
+ val params = distinct (op =) (maps (filter (is_funtype o fastype_of)) argss')
+ val pnames = map dest_Free params
val preds = map pred_of funs
val prednames = map (fst o dest_Free) preds
val funnames = map (fst o dest_Const) funs
val fun_pred_names = (funnames ~~ prednames)
(* mapping from term (Free or Const) to term *)
- fun lookup_pred (Const (name, T)) =
- (case (Symtab.lookup (Pred_Compile_Preproc.get thy) name) of
- SOME c => Const (c, pred_type T)
- | NONE =>
- (case AList.lookup op = fun_pred_names name of
- SOME f => Free (f, pred_type T)
- | NONE => Const (name, T)))
- | lookup_pred (Free (name, T)) =
- if member op = (map fst pnames) name then
- Free (name, transform_ho_typ T)
- else
- Free (name, T)
- | lookup_pred t =
- error ("lookup function is not defined for " ^ Syntax.string_of_term_global thy t)
-
- (* mapping from term (predicate term, not function term!) to int *)
- fun get_nparams (Const (name, _)) =
- the_default 0 (try (ind_package_get_nparams thy) name)
- | get_nparams (Free (name, _)) =
- (if member op = prednames name then
- length pnames
- else 0)
- | get_nparams t = error ("No parameters for " ^ (Syntax.string_of_term_global thy t))
-
+ fun map_Free f = Free o f o dest_Free
+ val net = fold Item_Net.update
+ ((funs ~~ preds) @ (ho_argss ~~ params))
+ (Fun_Pred.get thy)
+ fun lookup_pred t = lookup thy net t
(* create intro rules *)
fun mk_intros ((func, pred), (args, rhs)) =
@@ -314,14 +336,15 @@
else
let
val names = Term.add_free_names rhs []
- in mk_prems thy (lookup_pred, get_nparams) rhs (names, [])
+ in mk_prems thy lookup_pred rhs (names, [])
|> map (fn (resultt, (names', prems)) =>
Logic.list_implies (prems, HOLogic.mk_Trueprop (list_comb (pred, args @ [resultt]))))
end
fun mk_rewr_thm (func, pred) = @{thm refl}
in
- case try (maps mk_intros) ((funs ~~ preds) ~~ (argss' ~~ rhss)) of
- NONE => ([], thy)
+ case (*try *)SOME (maps mk_intros ((funs ~~ preds) ~~ (argss' ~~ rhss))) of
+ NONE =>
+ let val _ = tracing "error occured!" in ([], thy) end
| SOME intr_ts =>
if is_some (try (map (cterm_of thy)) intr_ts) then
let
@@ -333,53 +356,59 @@
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)))
- pnames
+ []
(map (fn x => (Attrib.empty_binding, x)) intr_ts)
[]
||> Sign.restore_naming thy
val prednames = map (fst o dest_Const) (#preds ind_result)
(* val rewr_thms = map mk_rewr_eq ((distinct (op =) funs) ~~ (#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 thy'' = Pred_Compile_Preproc.map (fold Symtab.update_new (consts ~~ prednames)) thy'
+ *)
+
+ val thy'' = Fun_Pred.map
+ (fold Item_Net.update (map (apfst Logic.varify)
+ (distinct (op =) funs ~~ (#preds ind_result)))) thy'
+ (*val _ = print_specs thy'' specs*)
in
(specs, thy'')
end
else
let
- val _ = tracing "Introduction rules of function_predicate are not welltyped"
+ val _ = Output.tracing (
+ "Introduction rules of function_predicate are not welltyped: " ^
+ commas (map (Syntax.string_of_term_global thy) intr_ts))
in ([], thy) end
end
fun rewrite_intro thy intro =
let
- fun lookup_pred (Const (name, T)) =
+ (*val _ = tracing ("Rewriting intro with registered mapping for: " ^
+ commas (Symtab.keys (Pred_Compile_Preproc.get thy)))*)
+ (*fun lookup_pred (Const (name, T)) =
(case (Symtab.lookup (Pred_Compile_Preproc.get thy) name) of
- SOME c => Const (c, pred_type T)
- | NONE => error ("Function " ^ name ^ " is not inductified"))
- | lookup_pred (Free (name, T)) = Free (name, T)
- | lookup_pred _ = error "lookup function is not defined!"
-
- fun get_nparams (Const (name, _)) =
- the_default 0 (try (ind_package_get_nparams thy) name)
- | get_nparams (Free _) = 0
- | get_nparams t = error ("No parameters for " ^ (Syntax.string_of_term_global thy t))
-
+ SOME c => SOME (Const (c, pred_type T))
+ | NONE => NONE)
+ | lookup_pred _ = NONE
+ *)
+ fun lookup_pred t = lookup thy (Fun_Pred.get thy) t
val intro_t = (Logic.unvarify o 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 (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 (
- fn t => if (is_funtype (fastype_of t)) then (fn x => [(t, x)])
- else mk_prems thy (lookup_pred, get_nparams) t) args (names, [])
+ folds_map (mk_prems thy lookup_pred) args (names, [])
|> map (fn (resargs, (names', prems')) =>
let
val prem' = HOLogic.mk_Trueprop (mk_lit (list_comb (P, resargs)))
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Tue Feb 23 12:14:46 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Tue Feb 23 14:00:36 2010 +0100
@@ -7,23 +7,85 @@
signature PREDICATE_COMPILE_PRED =
sig
(* preprocesses an equation to a set of intro rules; defines new constants *)
- (*
- val preprocess_pred_equation : thm -> theory -> thm list * theory
- *)
- val preprocess : string -> theory -> (thm list list * theory)
- (* output is the term list of clauses of an unknown predicate *)
- val preprocess_term : term -> theory -> (term list * theory)
-
- (*val rewrite : thm -> thm*)
-
+ val preprocess : Predicate_Compile_Aux.options -> (string * thm list) -> theory
+ -> ((string * thm list) list * theory)
+ val flat_higher_order_arguments : ((string * thm list) list * theory)
+ -> ((string * thm list) list * ((string * thm list) list * theory))
end;
-(* : PREDICATE_COMPILE_PREPROC_PRED *) (* FIXME *)
-structure Predicate_Compile_Pred =
+
+structure Predicate_Compile_Pred : PREDICATE_COMPILE_PRED =
struct
open Predicate_Compile_Aux
+
+fun datatype_names_of_case_name thy case_name =
+ map (#1 o #2) (#descr (the (Datatype_Data.info_of_case thy case_name)))
+
+fun make_case_rewrites new_type_names descr sorts thy =
+ let
+ val case_combs = Datatype_Prop.make_case_combs new_type_names descr sorts thy "f";
+ fun make comb =
+ let
+ val Type ("fun", [T, T']) = fastype_of comb;
+ val (Const (case_name, _), fs) = strip_comb comb
+ val used = Term.add_tfree_names comb []
+ val U = TFree (Name.variant used "'t", HOLogic.typeS)
+ val x = Free ("x", T)
+ val f = Free ("f", T' --> U)
+ fun apply_f f' =
+ let
+ val Ts = binder_types (fastype_of f')
+ val bs = map Bound ((length Ts - 1) downto 0)
+ in
+ fold (curry absdummy) (rev Ts) (f $ (list_comb (f', bs)))
+ end
+ val fs' = map apply_f fs
+ val case_c' = Const (case_name, (map fastype_of fs') @ [T] ---> U)
+ in
+ HOLogic.mk_eq (f $ (comb $ x), list_comb (case_c', fs') $ x)
+ end
+ in
+ map make case_combs
+ end
+
+fun case_rewrites thy Tcon =
+ let
+ val info = Datatype.the_info thy Tcon
+ val descr = #descr info
+ val sorts = #sorts info
+ val typ_names = the_default [Tcon] (#alt_names info)
+ in
+ map (Drule.export_without_context o Skip_Proof.make_thm thy o HOLogic.mk_Trueprop)
+ (make_case_rewrites typ_names [descr] sorts thy)
+ end
+
+fun instantiated_case_rewrites thy Tcon =
+ let
+ val rew_ths = case_rewrites thy Tcon
+ val ctxt = ProofContext.init thy
+ fun instantiate th =
+ let
+ val f = (fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th))))))
+ val Type ("fun", [uninst_T, uninst_T']) = fastype_of f
+ val ([tname, tname', uname, yname], ctxt') = Variable.add_fixes ["'t", "'t'", "'u", "y"] ctxt
+ val T = TFree (tname, HOLogic.typeS)
+ val T' = TFree (tname', HOLogic.typeS)
+ val U = TFree (uname, HOLogic.typeS)
+ val y = Free (yname, U)
+ val f' = absdummy (U --> T', Bound 0 $ y)
+ val th' = Thm.certify_instantiate
+ ([(dest_TVar uninst_T, U --> T'), (dest_TVar uninst_T', T')],
+ [((fst (dest_Var f), (U --> T') --> T'), f')]) th
+ val [th'] = Variable.export ctxt' ctxt [th']
+ in
+ th'
+ end
+ in
+ map instantiate rew_ths
+ end
+
fun is_compound ((Const ("Not", _)) $ t) =
error "is_compound: Negation should not occur; preprocessing is defect"
| is_compound ((Const ("Ex", _)) $ _) = true
@@ -35,6 +97,7 @@
fun flatten constname atom (defs, thy) =
if is_compound atom then
let
+ val atom = Envir.beta_norm (Pattern.eta_long [] atom)
val constname = Name.variant (map (Long_Name.base_name o fst) defs)
((Long_Name.base_name constname) ^ "_aux")
val full_constname = Sign.full_bname thy constname
@@ -50,7 +113,82 @@
(lhs, ((full_constname, [definition]) :: defs, thy'))
end
else
- (atom, (defs, thy))
+ (case (fst (strip_comb atom)) of
+ (Const (@{const_name If}, _)) => let
+ val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp}
+ val atom' = MetaSimplifier.rewrite_term thy
+ (map (fn th => th RS @{thm eq_reflection}) [@{thm if_bool_eq_disj}, if_beta]) [] atom
+ val _ = assert (not (atom = atom'))
+ in
+ flatten constname atom' (defs, thy)
+ end
+ | _ =>
+ if (has_split_thm thy (fst (strip_comb atom))) then
+ let
+ val (f, args) = strip_comb atom
+ val split_thm = prepare_split_thm (ProofContext.init thy) (the (find_split_thm' thy f))
+ (* TODO: contextify things - this line is to unvarify the split_thm *)
+ (*val ((_, [isplit_thm]), _) = Variable.import true [split_thm] (ProofContext.init thy)*)
+ val (assms, concl) = Logic.strip_horn (Thm.prop_of split_thm)
+ val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl)
+ val Tcons = datatype_names_of_case_name thy (fst (dest_Const f))
+ val ths = maps (instantiated_case_rewrites thy) Tcons
+ val atom = MetaSimplifier.rewrite_term thy
+ (map (fn th => th RS @{thm eq_reflection}) ths) [] atom
+ val (f, args) = strip_comb atom
+ val subst = Pattern.match thy (split_t, atom) (Vartab.empty, Vartab.empty)
+ val (_, split_args) = strip_comb split_t
+ val match = split_args ~~ args
+
+ (*
+ fun mk_prems_of_assm assm =
+ let
+ val (vTs, assm') = strip_all (Envir.beta_norm (Envir.subst_term subst assm))
+ val names = [] (* TODO *)
+ val var_names = Name.variant_list names (map fst vTs)
+ val vars = map Free (var_names ~~ (map snd vTs))
+ val (prems', pre_res) = Logic.strip_horn (subst_bounds (rev vars, assm'))
+ val (HOLogic.dest_eq (HOLogic.dest_Trueprop prem))
+ val (_, [inner_t]) = strip_comb (HOLogic.dest_Trueprop pre_res)
+ in
+ (*mk_prems' inner_t (var_names @ names, prems' @ prems)*) error "asda"
+ end
+ *)
+ val names = Term.add_free_names atom []
+ val frees = map Free (Term.add_frees atom [])
+ val constname = Name.variant (map (Long_Name.base_name o fst) defs)
+ ((Long_Name.base_name constname) ^ "_aux")
+ val full_constname = Sign.full_bname thy constname
+ val constT = map fastype_of frees ---> HOLogic.boolT
+ val lhs = list_comb (Const (full_constname, constT), frees)
+ fun new_def assm =
+ let
+ val (vTs, assm') = strip_all (Envir.beta_norm (Envir.subst_term subst assm))
+ val var_names = Name.variant_list names (map fst vTs)
+ val vars = map Free (var_names ~~ (map snd vTs))
+ val (prems', pre_res) = Logic.strip_horn (subst_bounds (rev vars, assm'))
+ fun mk_subst prem =
+ let
+ val (Free (x, T), r) = HOLogic.dest_eq (HOLogic.dest_Trueprop prem)
+ in
+ ((x, T), r)
+ end
+ val subst = map mk_subst prems'
+ val (_, [inner_t]) = strip_comb (HOLogic.dest_Trueprop pre_res)
+ val def = Logic.mk_equals (lhs, inner_t)
+ in
+ Envir.expand_term_frees subst def
+ end
+ val new_defs = map new_def assms
+ val (definition, thy') = thy
+ |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
+ |> PureThy.add_axioms (map_index
+ (fn (i, t) => ((Binding.name (constname ^ "_def" ^ string_of_int i), t), [])) new_defs)
+ in
+ (lhs, ((full_constname, definition) :: defs, thy'))
+ end
+ else
+ (atom, (defs, thy)))
fun flatten_intros constname intros thy =
let
@@ -107,30 +245,60 @@
val rewrite =
Simplifier.simplify (HOL_basic_ss addsimps [@{thm Ball_def}, @{thm Bex_def}])
- #> Simplifier.simplify (HOL_basic_ss addsimps [@{thm all_not_ex}])
+ #> Simplifier.simplify (HOL_basic_ss addsimps [@{thm all_not_ex}])
#> Conv.fconv_rule nnf_conv
#> Simplifier.simplify (HOL_basic_ss addsimps [@{thm ex_disj_distrib}])
-val rewrite_intros =
-(* Simplifier.simplify (HOL_basic_ss addsimps @{thms HOL.simp_thms(9)}) *)
- Simplifier.full_simplify (HOL_basic_ss addsimps [@{thm not_not}])
-
-fun preprocess (constname, specs) thy =
+fun split_conjs thy t =
+ let
+ fun split_conjunctions (Const (@{const_name "op &"}, _) $ t1 $ t2) =
+ (split_conjunctions t1) @ (split_conjunctions t2)
+ | split_conjunctions t = [t]
+ in
+ map HOLogic.mk_Trueprop (split_conjunctions (HOLogic.dest_Trueprop t))
+ end
+
+fun rewrite_intros thy =
+ Simplifier.full_simplify (HOL_basic_ss addsimps [@{thm all_not_ex}])
+ #> Simplifier.full_simplify (HOL_basic_ss addsimps @{thms bool_simps} addsimps @{thms nnf_simps})
+ #> map_term thy (maps_premises (split_conjs thy))
+
+fun print_specs options thy msg ths =
+ if show_intermediate_results options then
+ (tracing (msg); tracing (commas (map (Display.string_of_thm_global thy) ths)))
+ else
+ ()
+(*
+fun split_cases thy th =
let
- val ctxt = ProofContext.init thy
+
+ in
+ map_term thy th
+ end
+*)
+fun preprocess options (constname, specs) thy =
+(* case Predicate_Compile_Data.processed_specs thy constname of
+ SOME specss => (specss, thy)
+ | NONE =>*)
+ let
+ val ctxt = ProofContext.init thy
val intros =
- if forall is_pred_equation specs then
- introrulify thy (map rewrite specs)
- else if forall (is_intro constname) specs then
- map rewrite_intros specs
- else
- error ("unexpected specification for constant " ^ quote constname ^ ":\n"
- ^ commas (map (quote o Display.string_of_thm_global thy) specs))
- val (intros', (local_defs, thy')) = flatten_intros constname intros thy
- val (intross, thy'') = fold_map preprocess local_defs thy'
- in
- ((constname, intros') :: flat intross,thy'')
- end;
+ if forall is_pred_equation specs then
+ map (map_term thy (maps_premises (split_conjs thy))) (introrulify thy (map rewrite specs))
+ else if forall (is_intro constname) specs then
+ map (rewrite_intros thy) specs
+ else
+ error ("unexpected specification for constant " ^ quote constname ^ ":\n"
+ ^ commas (map (quote o Display.string_of_thm_global thy) specs))
+ val _ = print_specs options thy "normalized intros" intros
+ (*val intros = maps (split_cases thy) intros*)
+ val (intros', (local_defs, thy')) = flatten_intros constname intros thy
+ val (intross, thy'') = fold_map (preprocess options) local_defs thy'
+ val full_spec = (constname, intros') :: flat intross
+ (*val thy''' = Predicate_Compile_Data.store_processed_specs (constname, full_spec) thy''*)
+ in
+ (full_spec, thy'')
+ end;
fun preprocess_term t thy = error "preprocess_pred_term: to implement"
@@ -166,7 +334,8 @@
else
(arg, (new_defs, thy))
- val (args', (new_defs', thy')) = fold_map replace_abs_arg args (new_defs, thy)
+ val (args', (new_defs', thy')) = fold_map replace_abs_arg
+ (map Envir.beta_eta_contract args) (new_defs, thy)
in
(list_comb (pred, args'), (new_defs', thy'))
end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Tue Feb 23 12:14:46 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Tue Feb 23 14:00:36 2010 +0100
@@ -6,10 +6,18 @@
signature PREDICATE_COMPILE_QUICKCHECK =
sig
- val quickcheck : Proof.context -> term -> int -> term list option
+ (*val quickcheck : Proof.context -> term -> int -> term list option*)
val test_ref :
((unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)) option) Unsynchronized.ref
val tracing : bool Unsynchronized.ref;
+ val quickcheck_compile_term : bool -> bool -> Proof.context -> term -> int -> term list option
+(* val test_term : Proof.context -> bool -> int -> int -> int -> int -> term -> *)
+ val quiet : bool Unsynchronized.ref;
+ val nrandom : int Unsynchronized.ref;
+ val depth : int Unsynchronized.ref;
+ val debug : bool Unsynchronized.ref;
+ val function_flattening : bool Unsynchronized.ref;
+ val no_higher_order_predicate : string list Unsynchronized.ref;
end;
structure Predicate_Compile_Quickcheck : PREDICATE_COMPILE_QUICKCHECK =
@@ -24,21 +32,106 @@
val target = "Quickcheck"
+val quiet = Unsynchronized.ref false;
+
+val nrandom = Unsynchronized.ref 2;
+
+val depth = Unsynchronized.ref 8;
+
+val debug = Unsynchronized.ref false;
+val function_flattening = Unsynchronized.ref true;
+
+
+val no_higher_order_predicate = Unsynchronized.ref [];
+
val options = Options {
expected_modes = NONE,
proposed_modes = NONE,
proposed_names = [],
+ show_steps = false,
+ show_intermediate_results = false,
+ show_proof_trace = false,
+ show_modes = false,
+ show_mode_inference = false,
+ show_compilation = false,
+ show_caught_failures = false,
+ skip_proof = false,
+ compilation = Random,
+ inductify = true,
+ function_flattening = true,
+ fail_safe_function_flattening = false,
+ no_higher_order_predicate = [],
+ no_topmost_reordering = true
+}
+
+val debug_options = Options {
+ expected_modes = NONE,
+ proposed_modes = NONE,
+ proposed_names = [],
show_steps = true,
show_intermediate_results = true,
show_proof_trace = false,
- show_modes = false,
- show_mode_inference = false,
+ show_modes = true,
+ show_mode_inference = true,
show_compilation = false,
+ show_caught_failures = true,
skip_proof = false,
compilation = Random,
- inductify = false
+ inductify = true,
+ function_flattening = true,
+ fail_safe_function_flattening = false,
+ no_higher_order_predicate = [],
+ no_topmost_reordering = true
}
+
+fun set_function_flattening b
+ (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,
+ 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,
+ fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho,
+ no_topmost_reordering = re})
+
+fun set_fail_safe_function_flattening b
+ (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,
+ 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,
+ fail_safe_function_flattening = b, no_higher_order_predicate = no_ho,
+ no_topmost_reordering = re})
+
+fun set_no_higher_order_predicate ss
+ (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,
+ 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,
+ fail_safe_function_flattening = fs_ff, no_higher_order_predicate = ss, no_topmost_reordering = re})
+
+
+fun get_options () =
+ set_no_higher_order_predicate (!no_higher_order_predicate)
+ (set_function_flattening (!function_flattening)
+ (if !debug then debug_options else options))
+
fun dest_compfuns (Predicate_Compile_Core.CompilationFuns funs) = funs
val mk_predT = #mk_predT (dest_compfuns Predicate_Compile_Core.pred_compfuns)
val mk_randompredT = #mk_predT (dest_compfuns Predicate_Compile_Core.randompred_compfuns)
@@ -63,13 +156,15 @@
fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
-fun quickcheck ctxt t =
+fun cpu_time description f =
let
- (*val () =
- if !tracing then
- tracing ("Starting quickcheck with " ^ (Syntax.string_of_term ctxt t))
- else
- ()*)
+ val start = start_timing ()
+ val result = Exn.capture f ()
+ val time = Time.toMilliseconds (#cpu (end_timing start))
+ in (Exn.release result, (description, time)) end
+
+fun compile_term options ctxt t =
+ let
val ctxt' = ProofContext.theory (Context.copy_thy) ctxt
val thy = (ProofContext.theory_of ctxt')
val (vs, t') = strip_abs t
@@ -82,44 +177,73 @@
val thy1 = Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] thy
val const = Const (full_constname, constT)
val t = Logic.list_implies
- (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]),
+ (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]),
HOLogic.mk_Trueprop (list_comb (Const (full_constname, constT), map Free vs')))
val tac = fn _ => Skip_Proof.cheat_tac thy1
val intro = Goal.prove (ProofContext.init thy1) (map fst vs') [] t tac
- (*val _ = tracing (Display.string_of_thm ctxt' intro)*)
- val thy2 = (*Output.cond_timeit (!Quickcheck.timing) "predicate intros"
- (fn () => *)(Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1)
- val thy3 = (*Output.cond_timeit (!Quickcheck.timing) "predicate preprocessing"
- (fn () =>*) (Predicate_Compile.preprocess options const thy2)
- val thy4 = Output.cond_timeit (!Quickcheck.timing) "random_dseq compilation"
+ val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1
+ 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 () => Predicate_Compile_Core.add_random_dseq_equations options [full_constname] thy3)
- (*val depth_limited_modes = Predicate_Compile_Core.modes_of Depth_Limited thy'' full_constname*)
- val modes = Predicate_Compile_Core.modes_of Random_DSeq thy4 full_constname
+ val _ = Predicate_Compile_Core.print_all_modes Pos_Random_DSeq thy4
+ val modes = Predicate_Compile_Core.modes_of Pos_Random_DSeq thy4 full_constname
val output_mode = fold_rev (curry Fun) (map (K Output) (binder_types constT)) Bool
val prog =
if member eq_mode modes output_mode then
let
- val name = Predicate_Compile_Core.function_name_of Random_DSeq thy4 full_constname output_mode
+ val name = Predicate_Compile_Core.function_name_of Pos_Random_DSeq thy4
+ full_constname (true, output_mode)
val T = (mk_randompredT (HOLogic.mk_tupleT (map snd vs')))
in
Const (name, T)
end
- (*else if member (op =) depth_limited_modes ([], []) then
- let
- val name = Predicate_Compile_Core.depth_limited_function_name_of thy'' full_constname ([], [])
- val T = @{typ code_numeral} --> (mk_predT (HOLogic.mk_tupleT (map snd vs')))
- in lift_pred (Const (name, T) $ Bound 0) end*)
- else error "Predicate Compile Quickcheck failed"
+ else error ("Predicate Compile Quickcheck failed: " ^ commas (map string_of_mode modes))
val qc_term = mk_bind (prog,
mk_split_lambda (map Free vs') (mk_return (HOLogic.mk_list @{typ term}
(map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))
val compilation =
- Code_Eval.eval NONE ("Predicate_Compile_Quickcheck.test_ref", test_ref)
+ Code_Eval.eval (SOME target) ("Predicate_Compile_Quickcheck.test_ref", test_ref)
(fn proc => fn g => fn n => fn size => fn s => g n size s |>> (DSequence.map o map) proc)
thy4 qc_term []
in
- (fn size =>
- Option.map fst (DSequence.yield (compilation size size |> Random_Engine.run) size true))
+ (fn size => fn nrandom => fn depth =>
+ Option.map fst (DSequence.yield (compilation nrandom size |> Random_Engine.run) depth true))
+ end
+
+fun try_upto quiet f i =
+ let
+ fun try' j =
+ if j <= i then
+ let
+ val _ = priority ("Executing depth " ^ string_of_int j)
+ in
+ case f j handle Match => (if quiet then ()
+ else warning "Exception Match raised during quickcheck"; NONE)
+ of NONE => try' (j + 1) | SOME q => SOME q
+ end
+ else
+ NONE
+ in
+ try' 0
+ end
+
+(* quickcheck interface functions *)
+
+fun compile_term' options ctxt t =
+ let
+ val c = compile_term options ctxt t
+ in
+ (fn size => try_upto (!quiet) (c size (!nrandom)) (!depth))
+ end
+
+fun quickcheck_compile_term function_flattening fail_safe_function_flattening ctxt t =
+ let
+ val options =
+ set_fail_safe_function_flattening fail_safe_function_flattening
+ (set_function_flattening function_flattening (get_options ()))
+ in
+ compile_term' options ctxt t
end
end;
--- a/src/HOL/ex/Predicate_Compile_Alternative_Defs.thy Tue Feb 23 12:14:46 2010 +0100
+++ b/src/HOL/ex/Predicate_Compile_Alternative_Defs.thy Tue Feb 23 14:00:36 2010 +0100
@@ -2,6 +2,21 @@
imports "../Predicate_Compile"
begin
+section {* Common constants *}
+
+declare HOL.if_bool_eq_disj[code_pred_inline]
+
+setup {* Predicate_Compile_Data.ignore_consts [@{const_name Let}] *}
+
+section {* Pairs *}
+
+setup {* Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name split}] *}
+
+section {* Bounded quantifiers *}
+
+declare Ball_def[code_pred_inline]
+declare Bex_def[code_pred_inline]
+
section {* Set operations *}
declare Collect_def[code_pred_inline]
@@ -9,13 +24,37 @@
declare eq_reflection[OF empty_def, code_pred_inline]
declare insert_code[code_pred_def]
+
+declare subset_iff[code_pred_inline]
+
+declare Int_def[code_pred_inline]
declare eq_reflection[OF Un_def, code_pred_inline]
declare eq_reflection[OF UNION_def, code_pred_inline]
+lemma Diff[code_pred_inline]:
+ "(A - B) = (%x. A x \<and> \<not> B x)"
+by (auto 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)
+
+section {* Setup for Numerals *}
+
+setup {* Predicate_Compile_Data.ignore_consts [@{const_name number_of}] *}
+setup {* Predicate_Compile_Data.keep_functions [@{const_name number_of}] *}
+
+setup {* Predicate_Compile_Data.ignore_consts [@{const_name div}, @{const_name mod}, @{const_name times}] *}
section {* Alternative list definitions *}
+
+text {* size simps are not yet added to the Spec_Rules interface. So they are just added manually here! *}
+lemma [code_pred_def]:
+ "length [] = 0"
+ "length (x # xs) = Suc (length xs)"
+by auto
+
subsection {* Alternative rules for set *}
lemma set_ConsI1 [code_pred_intro]:
--- a/src/HOL/ex/Predicate_Compile_Quickcheck.thy Tue Feb 23 12:14:46 2010 +0100
+++ b/src/HOL/ex/Predicate_Compile_Quickcheck.thy Tue Feb 23 14:00:36 2010 +0100
@@ -3,11 +3,14 @@
header {* A Prototype of Quickcheck based on the Predicate Compiler *}
theory Predicate_Compile_Quickcheck
-imports "../Predicate_Compile"
+imports "../Predicate_Compile" Quickcheck Predicate_Compile_Alternative_Defs
uses "../Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
begin
-setup {* Quickcheck.add_generator ("predicate_compile", Predicate_Compile_Quickcheck.quickcheck) *}
+setup {* Quickcheck.add_generator ("predicate_compile_wo_ff", Predicate_Compile_Quickcheck.quickcheck_compile_term false true) *}
+setup {* Quickcheck.add_generator ("predicate_compile_ff_fs", Predicate_Compile_Quickcheck.quickcheck_compile_term true true) *}
+setup {* Quickcheck.add_generator ("predicate_compile_ff_nofs", Predicate_Compile_Quickcheck.quickcheck_compile_term true false) *}
+
(*
datatype alphabet = a | b
--- a/src/HOL/ex/Predicate_Compile_Quickcheck_ex.thy Tue Feb 23 12:14:46 2010 +0100
+++ b/src/HOL/ex/Predicate_Compile_Quickcheck_ex.thy Tue Feb 23 14:00:36 2010 +0100
@@ -1,45 +1,39 @@
theory Predicate_Compile_Quickcheck_ex
imports Predicate_Compile_Quickcheck
- Predicate_Compile_Alternative_Defs
begin
-ML {* Predicate_Compile_Alternative_Defs.get *}
-
section {* Sets *}
-(*
+
lemma "x \<in> {(1::nat)} ==> False"
-quickcheck[generator=predicate_compile, iterations=10]
+quickcheck[generator=predicate_compile_wo_ff, iterations=10]
oops
-*)
-(* TODO: some error with doubled negation *)
-(*
+
lemma "x \<in> {Suc 0, Suc (Suc 0)} ==> x \<noteq> Suc 0"
-quickcheck[generator=predicate_compile]
+quickcheck[generator=predicate_compile_wo_ff]
oops
-*)
-(*
+
lemma "x \<in> {Suc 0, Suc (Suc 0)} ==> x = Suc 0"
-quickcheck[generator=predicate_compile]
+quickcheck[generator=predicate_compile_wo_ff]
oops
-*)
+
lemma "x \<in> {Suc 0, Suc (Suc 0)} ==> x <= Suc 0"
-(*quickcheck[generator=predicate_compile]*)
+quickcheck[generator=predicate_compile_wo_ff]
oops
section {* Numerals *}
-(*
+
lemma
"x \<in> {1, 2, (3::nat)} ==> x = 1 \<or> x = 2"
-quickcheck[generator=predicate_compile]
+quickcheck[generator=predicate_compile_wo_ff]
oops
-*)
+
lemma "x \<in> {1, 2, (3::nat)} ==> x < 3"
-(*quickcheck[generator=predicate_compile]*)
+quickcheck[generator=predicate_compile_wo_ff]
oops
lemma
"x \<in> {1, 2} \<union> {3, 4} ==> x = (1::nat) \<or> x = (2::nat)"
-(*quickcheck[generator=predicate_compile]*)
+quickcheck[generator=predicate_compile_wo_ff]
oops
section {* Context Free Grammar *}
@@ -53,33 +47,15 @@
| "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1"
| "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
| "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1"
-(*
-code_pred [random_dseq inductify] "S\<^isub>1p" .
-*)
-(*thm B\<^isub>1p.random_dseq_equation*)
-(*
-values [random_dseq 2, 2, 4] 10 "{x. S\<^isub>1p x}"
-values [random_dseq 1, 1, 5] 20 "{x. S\<^isub>1p x}"
-ML {* set ML_Context.trace *}
-*)
-ML {* set Toplevel.debug *}
-(*
-quickcheck[generator = predicate_compile, size = 10, iterations = 1]
-oops
-*)
-ML {* Spec_Rules.get *}
-ML {* Item_Net.retrieve *}
-local_setup {* Local_Theory.checkpoint *}
-ML {* Predicate_Compile_Data.get_specification @{theory} @{term "append"} *}
lemma
- "w \<in> S\<^isub>1p \<Longrightarrow> w = []"
-quickcheck[generator = predicate_compile, iterations=1]
+ "w \<in> S\<^isub>1 \<Longrightarrow> w = []"
+quickcheck[generator = predicate_compile_ff_nofs, iterations=1]
oops
theorem S\<^isub>1_sound:
-"w \<in> S\<^isub>1p \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-quickcheck[generator=predicate_compile, size=15]
+"w \<in> S\<^isub>1 \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
+quickcheck[generator=predicate_compile_ff_nofs, size=15]
oops
@@ -90,7 +66,7 @@
| "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2"
| "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2"
| "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2"
-
+(*
code_pred [random_dseq inductify] S\<^isub>2 .
thm S\<^isub>2.random_dseq_equation
thm A\<^isub>2.random_dseq_equation
@@ -118,10 +94,10 @@
"w \<in> S\<^isub>2 ==> length [x \<leftarrow> w. x = a] <= Suc (Suc 0)"
quickcheck[generator=predicate_compile, size = 10, iterations = 1]
oops
-
+*)
theorem S\<^isub>2_sound:
"w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-quickcheck[generator=predicate_compile, size=15, iterations=1]
+quickcheck[generator=predicate_compile_ff_nofs, size=5, iterations=10]
oops
inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
@@ -141,17 +117,17 @@
lemma S\<^isub>3_sound:
"w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-quickcheck[generator=predicate_compile, size=10, iterations=10]
+quickcheck[generator=predicate_compile_ff_fs, size=10, iterations=10]
oops
lemma "\<not> (length w > 2) \<or> \<not> (length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b])"
-quickcheck[size=10, generator = predicate_compile]
+quickcheck[size=10, generator = predicate_compile_ff_fs]
oops
theorem S\<^isub>3_complete:
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. b = x] \<longrightarrow> w \<in> S\<^isub>3"
(*quickcheck[generator=SML]*)
-quickcheck[generator=predicate_compile, size=10, iterations=100]
+quickcheck[generator=predicate_compile_ff_fs, size=10, iterations=100]
oops
@@ -166,20 +142,23 @@
theorem S\<^isub>4_sound:
"w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-quickcheck[generator = predicate_compile, size=5, iterations=1]
+quickcheck[generator = predicate_compile_ff_nofs, size=5, iterations=1]
oops
theorem S\<^isub>4_complete:
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
-quickcheck[generator = predicate_compile, size=5, iterations=1]
+quickcheck[generator = predicate_compile_ff_nofs, size=5, iterations=1]
oops
-hide const b
+hide const a b
subsection {* Lexicographic order *}
+(* TODO *)
+(*
lemma
"(u, v) : lexord r ==> (x @ u, y @ v) : lexord r"
-
+oops
+*)
subsection {* IMP *}
types
@@ -208,7 +187,7 @@
lemma
"exec c s s' ==> exec (Seq c c) s s'"
-quickcheck[generator = predicate_compile, size=3, iterations=1]
+(*quickcheck[generator = predicate_compile_wo_ff, size=2, iterations=10]*)
oops
subsection {* Lambda *}
@@ -263,28 +242,9 @@
lemma
"\<Gamma> \<turnstile> t : U \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> \<Gamma> \<turnstile> t' : U"
-quickcheck[generator = predicate_compile, size = 7, iterations = 10]
+quickcheck[generator = predicate_compile_ff_fs, size = 7, iterations = 10]
oops
-(*
-code_pred (expected_modes: i => i => o => bool, i => i => i => bool) typing .
-thm typing.equation
-
-code_pred (modes: i => i => bool, i => o => bool as reduce') beta .
-thm beta.equation
-
-values "{x. App (Abs (Atom 0) (Var 0)) (Var 1) \<rightarrow>\<^sub>\<beta> x}"
-
-definition "reduce t = Predicate.the (reduce' t)"
-
-value "reduce (App (Abs (Atom 0) (Var 0)) (Var 1))"
-
-code_pred [random] typing .
-code_pred [random_dseq] typing .
-
-(*values [random] 1 "{(\<Gamma>, t, T). \<Gamma> \<turnstile> t : T}"
-*)*)
-
subsection {* JAD *}
definition matrix :: "('a :: semiring_0) list list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
@@ -300,9 +260,17 @@
lemma [code_pred_intro]:
"matrix [] 0 m"
"matrix xss n m ==> length xs = m ==> matrix (xs # xss) (Suc n) m"
-sorry
+proof -
+ show "matrix [] 0 m" unfolding matrix_def by auto
+next
+ show "matrix xss n m ==> length xs = m ==> matrix (xs # xss) (Suc n) m"
+ unfolding matrix_def by auto
+qed
-code_pred [random_dseq inductify] matrix sorry
+code_pred [random_dseq inductify] matrix
+ apply (cases x)
+ unfolding matrix_def apply fastsimp
+ apply fastsimp done
values [random_dseq 2, 2, 15] 6 "{(M::int list list, n, m). matrix M n m}"
@@ -344,10 +312,10 @@
definition
"length_permutate M = (unzip o sort (length o snd)) (zip [0 ..< length M] M)"
-
+(*
definition
"transpose M = [map (\<lambda> xs. xs ! i) (takeWhile (\<lambda> xs. i < length xs) M). i \<leftarrow> [0 ..< length (M ! 0)]]"
-
+*)
definition
"inflate upds = foldr (\<lambda> (i, x) upds. upds[i := x]) upds (replicate (length upds) 0)"
@@ -356,15 +324,14 @@
definition
"jad_mv v = inflate o split zip o apsnd (map listsum o transpose o map (map (\<lambda> (i, x). v ! i * x)))"
-ML {* ML_Context.trace := false *}
lemma "matrix (M::int list list) rs cs \<Longrightarrow> False"
-quickcheck[generator = predicate_compile, size = 6]
+quickcheck[generator = predicate_compile_ff_nofs, size = 6]
oops
lemma
"\<lbrakk> matrix M rs cs ; length v = cs \<rbrakk> \<Longrightarrow> jad_mv v (jad M) = mv M v"
-(*quickcheck[generator = predicate_compile]*)
+quickcheck[generator = predicate_compile_wo_ff]
oops
end
\ No newline at end of file
--- a/src/HOL/ex/Predicate_Compile_ex.thy Tue Feb 23 12:14:46 2010 +0100
+++ b/src/HOL/ex/Predicate_Compile_ex.thy Tue Feb 23 14:00:36 2010 +0100
@@ -252,10 +252,12 @@
"one_or_two = {Suc 0, (Suc (Suc 0))}"
code_pred [inductify] one_or_two .
+
code_pred [dseq] one_or_two .
-(*code_pred [random_dseq] one_or_two .*)
+code_pred [random_dseq] one_or_two .
+thm one_or_two.dseq_equation
values [expected "{Suc 0::nat, 2::nat}"] "{x. one_or_two x}"
-(*values [random_dseq 1,1,2] "{x. one_or_two x}"*)
+values [random_dseq 0,0,10] 3 "{x. one_or_two x}"
inductive one_or_two' :: "nat => bool"
where
@@ -269,12 +271,12 @@
definition one_or_two'':
"one_or_two'' == {1, (2::nat)}"
-ML {* prop_of @{thm one_or_two''} *}
-(*code_pred [inductify] one_or_two'' .
+
+code_pred [inductify] one_or_two'' .
thm one_or_two''.equation
values "{x. one_or_two'' x}"
-*)
+
subsection {* even predicate *}
inductive even :: "nat \<Rightarrow> bool" and odd :: "nat \<Rightarrow> bool" where
@@ -779,6 +781,25 @@
thm divmod_rel.equation
value [code] "Predicate.the (divmod_rel_i_i_o_o 1705 42)"
+subsection {* Transforming predicate logic into logic programs *}
+
+subsection {* Transforming functions into logic programs *}
+definition
+ "case_f xs ys = (case (xs @ ys) of [] => [] | (x # xs) => xs)"
+
+code_pred [inductify] case_f .
+thm case_fP.equation
+thm case_fP.intros
+
+fun fold_map_idx where
+ "fold_map_idx f i y [] = (y, [])"
+| "fold_map_idx f i y (x # xs) =
+ (let (y', x') = f i y x; (y'', xs') = fold_map_idx f (Suc i) y' xs
+ in (y'', x' # xs'))"
+
+text {* mode analysis explores thousand modes - this is infeasible at the moment... *}
+(*code_pred [inductify, show_steps] fold_map_idx .*)
+
subsection {* Minimum *}
definition Min
@@ -883,9 +904,16 @@
values [random_dseq 1, 2, 5] 10 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}"
-
-
-code_pred [inductify] lenlex .
+thm lenlex_conv
+thm lex_conv
+declare list.size(3,4)[code_pred_def]
+(*code_pred [inductify, show_steps, show_intermediate_results] length .*)
+setup {* Predicate_Compile_Data.ignore_consts [@{const_name Orderings.top_class.top}] *}
+code_pred [inductify] lex .
+thm lex.equation
+thm lex_def
+declare lenlex_conv[code_pred_def]
+code_pred [inductify, show_steps, show_intermediate_results] lenlex .
thm lenlex.equation
code_pred [random_dseq inductify] lenlex .
@@ -893,10 +921,10 @@
values [random_dseq 4, 2, 4] 100 "{(xs, ys::int list). lenlex (%(x, y). x <= y) (xs, ys)}"
thm lists.intros
-(*
+
code_pred [inductify] lists .
-*)
-(*thm lists.equation*)
+
+thm lists.equation
subsection {* AVL Tree *}
@@ -974,13 +1002,17 @@
(o * o => bool) => i => bool,
(i * o => bool) => i => bool) [inductify] Domain .
thm Domain.equation
+thm Range_def
+
code_pred (modes:
(o * o => bool) => o => bool,
(o * o => bool) => i => bool,
(o * i => bool) => i => bool) [inductify] Range .
thm Range.equation
+
code_pred [inductify] Field .
thm Field.equation
+
(*thm refl_on_def
code_pred [inductify] refl_on .
thm refl_on.equation*)
@@ -992,9 +1024,10 @@
thm trans.equation
code_pred [inductify] single_valued .
thm single_valued.equation
-code_pred [inductify] inv_image .
+thm inv_image_def
+(*code_pred [inductify] inv_image .
thm inv_image.equation
-
+*)
subsection {* Inverting list functions *}
(*code_pred [inductify] length .
--- a/src/Tools/quickcheck.ML Tue Feb 23 12:14:46 2010 +0100
+++ b/src/Tools/quickcheck.ML Tue Feb 23 14:00:36 2010 +0100
@@ -10,6 +10,8 @@
val timing : bool Unsynchronized.ref
val test_term: Proof.context -> bool -> string option -> int -> int -> term ->
(string * term) list option
+ val timed_test_term: Proof.context -> bool -> string option -> int -> int -> term ->
+ ((string * term) list option * (string * int) list)
val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory
val setup: theory -> theory
val quickcheck: (string * string) list -> int -> Proof.state -> (string * term) list option
@@ -97,13 +99,20 @@
val frees = Term.add_frees t [];
in (map fst frees, list_abs_free (frees, t)) end
-fun test_term ctxt quiet generator_name size i t =
+fun cpu_time description f =
+ let
+ val start = start_timing ()
+ val result = Exn.capture f ()
+ val time = Time.toMilliseconds (#cpu (end_timing start))
+ in (Exn.release result, (description, time)) end
+
+fun timed_test_term ctxt quiet generator_name size i t =
let
val (names, t') = prep_test_term t;
- val testers = (*cond_timeit (!timing) "quickcheck compilation"
- (fn () => *)(case generator_name
+ val (testers, comp_time) = cpu_time "quickcheck compilation"
+ (fn () => (case generator_name
of NONE => if quiet then mk_testers ctxt t' else mk_testers_strict ctxt t'
- | SOME name => [mk_tester_select name ctxt t']);
+ | SOME name => [mk_tester_select name ctxt t']));
fun iterate f 0 = NONE
| iterate f j = case f () handle Match => (if quiet then ()
else warning "Exception Match raised during quickcheck"; NONE)
@@ -117,13 +126,17 @@
else (if quiet then () else priority ("Test data size: " ^ string_of_int k);
case with_testers k testers
of NONE => with_size (k + 1) | SOME q => SOME q);
+ val (result, exec_time) = cpu_time "quickcheck execution"
+ (fn () => case with_size 1
+ of NONE => NONE
+ | SOME ts => SOME (names ~~ ts))
in
- cond_timeit (!timing) "quickcheck execution"
- (fn () => case with_size 1
- of NONE => NONE
- | SOME ts => SOME (names ~~ ts))
+ (result, [exec_time, comp_time])
end;
+fun test_term ctxt quiet generator_name size i t =
+ fst (timed_test_term ctxt quiet generator_name size i t)
+
fun monomorphic_term thy insts default_T =
let
fun subst (T as TFree (v, S)) =