# HG changeset patch
# User bulwahn
# Date 1284967575 -7200
# Node ID 6605c1e87c7fba171ae9b17b4107b051525e36c6
# Parent  49c319fff40cd078833affb745236abfa46ac44e
removing clone in code_prolog and predicate_compile_quickcheck

diff -r 49c319fff40c -r 6605c1e87c7f src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- 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
diff -r 49c319fff40c -r 6605c1e87c7f src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- 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;
diff -r 49c319fff40c -r 6605c1e87c7f src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
--- 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