--- 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