removing clone in code_prolog and predicate_compile_quickcheck
authorbulwahn
Mon Sep 20 09:26:15 2010 +0200 (2010-09-20)
changeset 395416605c1e87c7f
parent 39540 49c319fff40c
child 39542 a50c0ae2312c
removing clone in code_prolog and predicate_compile_quickcheck
src/HOL/Tools/Predicate_Compile/code_prolog.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Mon Sep 20 09:19:22 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Mon Sep 20 09:26:15 2010 +0200
     1.3 @@ -970,37 +970,16 @@
     1.4  
     1.5  (* quickcheck generator *)
     1.6  
     1.7 -(* FIXME: large copy of Predicate_Compile_Quickcheck - refactor out commons *)
     1.8 -
     1.9 -fun strip_imp_prems (Const(@{const_name HOL.implies}, _) $ A $ B) = A :: strip_imp_prems B
    1.10 -  | strip_imp_prems _ = [];
    1.11 -
    1.12 -fun strip_imp_concl (Const(@{const_name HOL.implies}, _) $ A $ B) = strip_imp_concl B
    1.13 -  | strip_imp_concl A = A : term;
    1.14 -
    1.15 -fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
    1.16 +(* FIXME: a small clone of Predicate_Compile_Quickcheck - maybe refactor out commons *)
    1.17  
    1.18  fun quickcheck ctxt t size =
    1.19    let
    1.20      val options = code_options_of (ProofContext.theory_of ctxt)
    1.21      val thy = Theory.copy (ProofContext.theory_of ctxt)
    1.22 -    val (vs, t') = strip_abs t
    1.23 -    val vs' = Variable.variant_frees ctxt [] vs
    1.24 -    val Ts = map snd vs'
    1.25 -    val t'' = subst_bounds (map Free (rev vs'), t')
    1.26 -    val (prems, concl) = strip_horn t''
    1.27 -    val constname = "quickcheck"
    1.28 -    val full_constname = Sign.full_bname thy constname
    1.29 -    val constT = Ts ---> @{typ bool}
    1.30 -    val thy1 = Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] thy
    1.31 -    val const = Const (full_constname, constT)
    1.32 -    val t = Logic.list_implies
    1.33 -      (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]),
    1.34 -       HOLogic.mk_Trueprop (list_comb (Const (full_constname, constT), map Free vs')))
    1.35 -    val tac = fn _ => Skip_Proof.cheat_tac thy1
    1.36 -    val intro = Goal.prove (ProofContext.init_global thy1) (map fst vs') [] t tac
    1.37 +    val ((((full_constname, constT), vs'), intro), thy1) =
    1.38 +      Predicate_Compile_Aux.define_quickcheck_predicate t thy
    1.39      val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1
    1.40 -    val thy3 = Predicate_Compile.preprocess preprocess_options const thy2
    1.41 +    val thy3 = Predicate_Compile.preprocess preprocess_options (Const (full_constname, constT)) thy2
    1.42      val ctxt' = ProofContext.init_global thy3
    1.43      val _ = tracing "Generating prolog program..."
    1.44      val (p, constant_table) = generate (NONE, true) ctxt' full_constname
    1.45 @@ -1015,7 +994,7 @@
    1.46      val _ = tracing "Restoring terms..."
    1.47      val res =
    1.48        case tss of
    1.49 -        [ts] => SOME (map (restore_term ctxt' constant_table) (ts ~~ Ts))
    1.50 +        [ts] => SOME (map (restore_term ctxt' constant_table) (ts ~~ map snd vs'))
    1.51        | _ => NONE
    1.52      val empty_report = ([], false)
    1.53    in
     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Sep 20 09:19:22 2010 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Sep 20 09:26:15 2010 +0200
     2.3 @@ -148,6 +148,8 @@
     2.4    val remove_equalities : theory -> thm -> thm
     2.5    val remove_pointless_clauses : thm -> thm list
     2.6    val peephole_optimisation : theory -> thm -> thm option
     2.7 +  val define_quickcheck_predicate :
     2.8 +    term -> theory -> (((string * typ) * (string * typ) list) * thm) * theory 
     2.9  end;
    2.10  
    2.11  structure Predicate_Compile_Aux : PREDICATE_COMPILE_AUX =
    2.12 @@ -909,4 +911,34 @@
    2.13        (process_False (process_True (prop_of (process intro))))
    2.14    end
    2.15  
    2.16 +(* defining a quickcheck predicate *)
    2.17 +
    2.18 +fun strip_imp_prems (Const(@{const_name HOL.implies}, _) $ A $ B) = A :: strip_imp_prems B
    2.19 +  | strip_imp_prems _ = [];
    2.20 +
    2.21 +fun strip_imp_concl (Const(@{const_name HOL.implies}, _) $ A $ B) = strip_imp_concl B
    2.22 +  | strip_imp_concl A = A : term;
    2.23 +
    2.24 +fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
    2.25 +
    2.26 +fun define_quickcheck_predicate t thy =
    2.27 +  let
    2.28 +    val (vs, t') = strip_abs t
    2.29 +    val vs' = Variable.variant_frees (ProofContext.init_global thy) [] vs
    2.30 +    val t'' = subst_bounds (map Free (rev vs'), t')
    2.31 +    val (prems, concl) = strip_horn t''
    2.32 +    val constname = "quickcheck"
    2.33 +    val full_constname = Sign.full_bname thy constname
    2.34 +    val constT = map snd vs' ---> @{typ bool}
    2.35 +    val thy1 = Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] thy
    2.36 +    val const = Const (full_constname, constT)
    2.37 +    val t = Logic.list_implies
    2.38 +      (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]),
    2.39 +       HOLogic.mk_Trueprop (list_comb (const, map Free vs')))
    2.40 +    val tac = fn _ => Skip_Proof.cheat_tac thy1
    2.41 +    val intro = Goal.prove (ProofContext.init_global thy1) (map fst vs') [] t tac
    2.42 +  in
    2.43 +    ((((full_constname, constT), vs'), intro), thy1)
    2.44 +  end
    2.45 +
    2.46  end;
     3.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Mon Sep 20 09:19:22 2010 +0200
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Mon Sep 20 09:26:15 2010 +0200
     3.3 @@ -187,14 +187,6 @@
     3.4      mk_split_lambda' xs t
     3.5    end;
     3.6  
     3.7 -fun strip_imp_prems (Const(@{const_name HOL.implies}, _) $ A $ B) = A :: strip_imp_prems B
     3.8 -  | strip_imp_prems _ = [];
     3.9 -
    3.10 -fun strip_imp_concl (Const(@{const_name HOL.implies}, _) $ A $ B) = strip_imp_concl B
    3.11 -  | strip_imp_concl A = A : term;
    3.12 -
    3.13 -fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
    3.14 -
    3.15  fun cpu_time description f =
    3.16    let
    3.17      val start = start_timing ()
    3.18 @@ -205,23 +197,11 @@
    3.19  fun compile_term compilation options ctxt t =
    3.20    let
    3.21      val thy = Theory.copy (ProofContext.theory_of ctxt)
    3.22 -    val (vs, t') = strip_abs t
    3.23 -    val vs' = Variable.variant_frees ctxt [] vs
    3.24 -    val t'' = subst_bounds (map Free (rev vs'), t')
    3.25 -    val (prems, concl) = strip_horn t''
    3.26 -    val constname = "pred_compile_quickcheck"
    3.27 -    val full_constname = Sign.full_bname thy constname
    3.28 -    val constT = map snd vs' ---> @{typ bool}
    3.29 -    val thy1 = Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] thy
    3.30 -    val const = Const (full_constname, constT)
    3.31 -    val t = Logic.list_implies
    3.32 -      (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]),
    3.33 -       HOLogic.mk_Trueprop (list_comb (Const (full_constname, constT), map Free vs')))
    3.34 -    val tac = fn _ => Skip_Proof.cheat_tac thy1
    3.35 -    val intro = Goal.prove (ProofContext.init_global thy1) (map fst vs') [] t tac
    3.36 +    val ((((full_constname, constT), vs'), intro), thy1) =
    3.37 +      Predicate_Compile_Aux.define_quickcheck_predicate t thy
    3.38      val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1
    3.39      val (thy3, preproc_time) = cpu_time "predicate preprocessing"
    3.40 -        (fn () => Predicate_Compile.preprocess options const thy2)
    3.41 +        (fn () => Predicate_Compile.preprocess options (Const (full_constname, constT)) thy2)
    3.42      val (thy4, core_comp_time) = cpu_time "random_dseq core compilation"
    3.43          (fn () =>
    3.44            case compilation of