--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Mon Sep 20 09:19:22 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Mon Sep 20 09:26:15 2010 +0200
@@ -970,37 +970,16 @@
(* quickcheck generator *)
-(* FIXME: large copy of Predicate_Compile_Quickcheck - refactor out commons *)
-
-fun strip_imp_prems (Const(@{const_name HOL.implies}, _) $ A $ B) = A :: strip_imp_prems B
- | strip_imp_prems _ = [];
-
-fun strip_imp_concl (Const(@{const_name HOL.implies}, _) $ A $ B) = strip_imp_concl B
- | strip_imp_concl A = A : term;
-
-fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
+(* FIXME: a small clone of Predicate_Compile_Quickcheck - maybe refactor out commons *)
fun quickcheck ctxt t size =
let
val options = code_options_of (ProofContext.theory_of ctxt)
val thy = Theory.copy (ProofContext.theory_of ctxt)
- val (vs, t') = strip_abs t
- val vs' = Variable.variant_frees ctxt [] vs
- val Ts = map snd vs'
- val t'' = subst_bounds (map Free (rev vs'), t')
- val (prems, concl) = strip_horn t''
- val constname = "quickcheck"
- val full_constname = Sign.full_bname thy constname
- val constT = Ts ---> @{typ bool}
- 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]),
- 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_global thy1) (map fst vs') [] t tac
+ val ((((full_constname, constT), vs'), intro), thy1) =
+ Predicate_Compile_Aux.define_quickcheck_predicate t thy
val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1
- val thy3 = Predicate_Compile.preprocess preprocess_options const thy2
+ val thy3 = Predicate_Compile.preprocess preprocess_options (Const (full_constname, constT)) thy2
val ctxt' = ProofContext.init_global thy3
val _ = tracing "Generating prolog program..."
val (p, constant_table) = generate (NONE, true) ctxt' full_constname
@@ -1015,7 +994,7 @@
val _ = tracing "Restoring terms..."
val res =
case tss of
- [ts] => SOME (map (restore_term ctxt' constant_table) (ts ~~ Ts))
+ [ts] => SOME (map (restore_term ctxt' constant_table) (ts ~~ map snd vs'))
| _ => NONE
val empty_report = ([], false)
in
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Mon Sep 20 09:19:22 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Mon Sep 20 09:26:15 2010 +0200
@@ -148,6 +148,8 @@
val remove_equalities : theory -> thm -> thm
val remove_pointless_clauses : thm -> thm list
val peephole_optimisation : theory -> thm -> thm option
+ val define_quickcheck_predicate :
+ term -> theory -> (((string * typ) * (string * typ) list) * thm) * theory
end;
structure Predicate_Compile_Aux : PREDICATE_COMPILE_AUX =
@@ -909,4 +911,34 @@
(process_False (process_True (prop_of (process intro))))
end
+(* defining a quickcheck predicate *)
+
+fun strip_imp_prems (Const(@{const_name HOL.implies}, _) $ A $ B) = A :: strip_imp_prems B
+ | strip_imp_prems _ = [];
+
+fun strip_imp_concl (Const(@{const_name HOL.implies}, _) $ A $ B) = strip_imp_concl B
+ | strip_imp_concl A = A : term;
+
+fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
+
+fun define_quickcheck_predicate t thy =
+ let
+ val (vs, t') = strip_abs t
+ val vs' = Variable.variant_frees (ProofContext.init_global thy) [] vs
+ val t'' = subst_bounds (map Free (rev vs'), t')
+ val (prems, concl) = strip_horn t''
+ val constname = "quickcheck"
+ val full_constname = Sign.full_bname thy constname
+ val constT = map snd vs' ---> @{typ bool}
+ 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]),
+ HOLogic.mk_Trueprop (list_comb (const, map Free vs')))
+ val tac = fn _ => Skip_Proof.cheat_tac thy1
+ val intro = Goal.prove (ProofContext.init_global thy1) (map fst vs') [] t tac
+ in
+ ((((full_constname, constT), vs'), intro), thy1)
+ end
+
end;
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Mon Sep 20 09:19:22 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Mon Sep 20 09:26:15 2010 +0200
@@ -187,14 +187,6 @@
mk_split_lambda' xs t
end;
-fun strip_imp_prems (Const(@{const_name HOL.implies}, _) $ A $ B) = A :: strip_imp_prems B
- | strip_imp_prems _ = [];
-
-fun strip_imp_concl (Const(@{const_name HOL.implies}, _) $ A $ B) = strip_imp_concl B
- | strip_imp_concl A = A : term;
-
-fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
-
fun cpu_time description f =
let
val start = start_timing ()
@@ -205,23 +197,11 @@
fun compile_term compilation options ctxt t =
let
val thy = Theory.copy (ProofContext.theory_of ctxt)
- val (vs, t') = strip_abs t
- val vs' = Variable.variant_frees ctxt [] vs
- val t'' = subst_bounds (map Free (rev vs'), t')
- val (prems, concl) = strip_horn t''
- val constname = "pred_compile_quickcheck"
- val full_constname = Sign.full_bname thy constname
- val constT = map snd vs' ---> @{typ bool}
- 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]),
- 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_global thy1) (map fst vs') [] t tac
+ val ((((full_constname, constT), vs'), intro), thy1) =
+ Predicate_Compile_Aux.define_quickcheck_predicate t thy
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)
+ (fn () => Predicate_Compile.preprocess options (Const (full_constname, constT)) thy2)
val (thy4, core_comp_time) = cpu_time "random_dseq core compilation"
(fn () =>
case compilation of