adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
authorbulwahn
Fri Apr 01 13:49:38 2011 +0200 (2011-04-01)
changeset 421951e7b62c93f5d
parent 42194 bd416284a432
child 42196 9893b2913a44
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
src/HOL/Quickcheck_Exhaustive.thy
src/HOL/Tools/Quickcheck/exhaustive_generators.ML
src/HOL/Tools/Quickcheck/quickcheck_common.ML
src/HOL/Tools/Quickcheck/random_generators.ML
     1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Fri Apr 01 13:49:36 2011 +0200
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Fri Apr 01 13:49:38 2011 +0200
     1.3 @@ -355,7 +355,22 @@
     1.4  
     1.5  end
     1.6  
     1.7 +subsection {* Bounded universal quantifiers *}
     1.8  
     1.9 +class bounded_forall =
    1.10 +  fixes bounded_forall :: "('a \<Rightarrow> bool) \<Rightarrow> code_numeral \<Rightarrow> bool"
    1.11 +
    1.12 +
    1.13 +instantiation nat :: bounded_forall
    1.14 +begin
    1.15 +
    1.16 +fun bounded_forall_nat :: "(nat => bool) => code_numeral => bool"
    1.17 +where
    1.18 +  "bounded_forall P d = ((P 0) \<and> (if d > 0 then bounded_forall (%n. P (Suc n)) (d - 1) else True))"
    1.19 +
    1.20 +instance ..
    1.21 +
    1.22 +end
    1.23  
    1.24  subsection {* Defining combinators for any first-order data type *}
    1.25  
     2.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Apr 01 13:49:36 2011 +0200
     2.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Apr 01 13:49:38 2011 +0200
     2.3 @@ -9,12 +9,14 @@
     2.4    val compile_generator_expr:
     2.5      Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option
     2.6    val compile_generator_exprs: Proof.context -> term list -> (int -> term list option) list
     2.7 +  val compile_validator_exprs: Proof.context -> term list -> (int -> bool) list
     2.8    val put_counterexample: (unit -> int -> int -> term list option)
     2.9      -> Proof.context -> Proof.context
    2.10    val put_counterexample_batch: (unit -> (int -> term list option) list)
    2.11      -> Proof.context -> Proof.context
    2.12 -  val smart_quantifier : bool Config.T;
    2.13 -  val quickcheck_pretty : bool Config.T;
    2.14 +  val put_validator_batch: (unit -> (int -> bool) list) -> Proof.context -> Proof.context
    2.15 +  val smart_quantifier : bool Config.T
    2.16 +  val quickcheck_pretty : bool Config.T
    2.17    val setup: theory -> theory
    2.18  end;
    2.19  
    2.20 @@ -238,8 +240,6 @@
    2.21        @{term "Quickcheck_Exhaustive.catch_match :: term list option => term list option => term list option"} $
    2.22          (@{term "If :: bool => term list option => term list option => term list option"}
    2.23          $ cond $ then_t $ else_t) $ none_t;
    2.24 -    fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B)
    2.25 -        | strip_imp A = ([], A)
    2.26      fun lookup v = the (AList.lookup (op =) (names ~~ (frees ~~ term_vars)) v)
    2.27      fun mk_naive_test_term t =
    2.28        fold_rev mk_exhaustive_closure (frees ~~ term_vars) (mk_safe_if (t, none_t, return)) 
    2.29 @@ -255,7 +255,7 @@
    2.30        end
    2.31      fun mk_smart_test_term t =
    2.32        let
    2.33 -        val (assms, concl) = strip_imp t
    2.34 +        val (assms, concl) = Quickcheck_Common.strip_imp t
    2.35        in
    2.36          mk_smart_test_term' concl [] assms
    2.37        end
    2.38 @@ -267,7 +267,41 @@
    2.39    Quickcheck_Common.gen_mk_parametric_generator_expr 
    2.40      ((mk_generator_expr, absdummy (@{typ "code_numeral"}, @{term "None :: term list option"})),
    2.41        @{typ "code_numeral => term list option"})
    2.42 -  
    2.43 +
    2.44 +fun mk_validator_expr ctxt t =
    2.45 +  let
    2.46 +    fun bounded_forallT T = (T --> @{typ bool}) --> @{typ code_numeral} --> @{typ bool}
    2.47 +    val thy = ProofContext.theory_of ctxt
    2.48 +    val ctxt' = Variable.auto_fixes t ctxt
    2.49 +    val ([depth_name], ctxt'') = Variable.variant_fixes ["depth"] ctxt'
    2.50 +    val depth = Free (depth_name, @{typ code_numeral})
    2.51 +    fun mk_bounded_forall (s, T) t =
    2.52 +      Const (@{const_name "Quickcheck_Exhaustive.bounded_forall_class.bounded_forall"}, bounded_forallT T)
    2.53 +        $ lambda (Free (s, T)) t $ depth
    2.54 +    fun mk_implies (cond, then_t) =
    2.55 +      @{term "If :: bool => bool => bool => bool"} $ cond $ then_t $ @{term False}
    2.56 +    fun mk_naive_test_term t = fold_rev mk_bounded_forall (Term.add_frees t []) t 
    2.57 +    fun mk_smart_test_term' concl bound_frees assms =
    2.58 +      let
    2.59 +        fun vars_of t = subtract (op =) bound_frees (Term.add_frees t [])
    2.60 +        val (vars, check) =
    2.61 +          case assms of [] => (vars_of concl, concl)
    2.62 +            | assm :: assms => (vars_of assm, mk_implies (assm,
    2.63 +                mk_smart_test_term' concl (union (op =) (vars_of assm) bound_frees) assms))
    2.64 +      in
    2.65 +        fold_rev mk_bounded_forall vars check
    2.66 +      end
    2.67 +    fun mk_smart_test_term t =
    2.68 +      let
    2.69 +        val (assms, concl) = Quickcheck_Common.strip_imp t
    2.70 +      in
    2.71 +        mk_smart_test_term' concl [] assms
    2.72 +      end
    2.73 +    val mk_test_term =
    2.74 +      if Config.get ctxt smart_quantifier then mk_smart_test_term else mk_naive_test_term 
    2.75 +  in lambda depth (mk_test_term t) end
    2.76 +
    2.77 +
    2.78  (** generator compiliation **)
    2.79  
    2.80  structure Counterexample = Proof_Data
    2.81 @@ -286,6 +320,15 @@
    2.82  );
    2.83  val put_counterexample_batch = Counterexample_Batch.put;
    2.84  
    2.85 +structure Validator_Batch = Proof_Data
    2.86 +(
    2.87 +  type T = unit -> (int -> bool) list
    2.88 +  (* FIXME avoid user error with non-user text *)
    2.89 +  fun init _ () = error "Counterexample"
    2.90 +);
    2.91 +val put_validator_batch = Validator_Batch.put;
    2.92 +
    2.93 +
    2.94  val target = "Quickcheck";
    2.95    
    2.96  fun compile_generator_expr ctxt ts =
    2.97 @@ -295,7 +338,7 @@
    2.98      val compile = Code_Runtime.dynamic_value_strict
    2.99        (Counterexample.get, put_counterexample, "Exhaustive_Generators.put_counterexample")
   2.100        thy (SOME target) (fn proc => fn g =>
   2.101 -        fn card => fn size => g card size |> (Option.map o map) proc) t' [];
   2.102 +        fn card => fn size => g card size |> (Option.map o map) proc) t' []
   2.103    in
   2.104      fn [card, size] => rpair NONE (compile card size |> 
   2.105        (if Config.get ctxt quickcheck_pretty then
   2.106 @@ -310,12 +353,22 @@
   2.107        (Counterexample_Batch.get, put_counterexample_batch,
   2.108          "Exhaustive_Generators.put_counterexample_batch")
   2.109        thy (SOME target) (fn proc => map (fn g => g #> (Option.map o map) proc))
   2.110 -      (HOLogic.mk_list @{typ "code_numeral => term list option"} ts') [];
   2.111 +      (HOLogic.mk_list @{typ "code_numeral => term list option"} ts') []
   2.112    in
   2.113      map (fn compile => fn size => compile size
   2.114        |> Option.map (map Quickcheck_Common.post_process_term)) compiles
   2.115    end;
   2.116 -  
   2.117 +
   2.118 +fun compile_validator_exprs ctxt ts =
   2.119 +  let
   2.120 +    val thy = ProofContext.theory_of ctxt
   2.121 +    val ts' = map (mk_validator_expr ctxt) ts;
   2.122 +  in
   2.123 +    Code_Runtime.dynamic_value_strict
   2.124 +      (Validator_Batch.get, put_validator_batch, "Exhaustive_Generators.put_validator_batch")
   2.125 +      thy (SOME target) (K I) (HOLogic.mk_list @{typ "code_numeral => bool"} ts') []
   2.126 +  end;
   2.127 +
   2.128  (** setup **)
   2.129  
   2.130  val setup =
   2.131 @@ -324,6 +377,7 @@
   2.132    #> setup_smart_quantifier
   2.133    #> setup_quickcheck_pretty
   2.134    #> Context.theory_map (Quickcheck.add_generator ("exhaustive", compile_generator_expr))
   2.135 -  #> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs));
   2.136 +  #> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs))
   2.137 +  #> Context.theory_map (Quickcheck.add_batch_validator ("exhaustive", compile_validator_exprs));
   2.138  
   2.139  end;
     3.1 --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Fri Apr 01 13:49:36 2011 +0200
     3.2 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Fri Apr 01 13:49:38 2011 +0200
     3.3 @@ -6,6 +6,7 @@
     3.4  
     3.5  signature QUICKCHECK_COMMON =
     3.6  sig
     3.7 +  val strip_imp : term -> (term list * term)
     3.8    val perhaps_constrain: theory -> (typ * sort) list -> (string * sort) list
     3.9      -> (string * sort -> string * sort) option
    3.10    val ensure_sort_datatype:
    3.11 @@ -20,6 +21,11 @@
    3.12  structure Quickcheck_Common : QUICKCHECK_COMMON =
    3.13  struct
    3.14  
    3.15 +(* HOLogic's term functions *)
    3.16 +
    3.17 +fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B)
    3.18 +  | strip_imp A = ([], A)
    3.19 +
    3.20  (** ensuring sort constraints **)
    3.21  
    3.22  fun perhaps_constrain thy insts raw_vs =
     4.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Apr 01 13:49:36 2011 +0200
     4.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Apr 01 13:49:38 2011 +0200
     4.3 @@ -322,11 +322,9 @@
     4.4      val bound_max = length Ts - 1
     4.5      val bounds = map_index (fn (i, ty) =>
     4.6        (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
     4.7 -    fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B)
     4.8 -      | strip_imp A = ([], A)
     4.9      val prop' = betapplys (prop, map (fn (i, _, _, _) => Bound i) bounds);
    4.10      val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds)
    4.11 -    val (assms, concl) = strip_imp prop'
    4.12 +    val (assms, concl) = Quickcheck_Common.strip_imp prop'
    4.13      val return =
    4.14        @{term "Pair :: term list option * (bool list * bool) => Random.seed => (term list option * (bool list * bool)) * Random.seed"};
    4.15      fun mk_assms_report i =