adding smart quantifiers to exhaustive testing
authorbulwahn
Fri Dec 03 08:40:47 2010 +0100 (2010-12-03)
changeset 4090745ba9f05583a
parent 40906 b5a319668955
child 40908 e8806880819e
adding smart quantifiers to exhaustive testing
src/HOL/Tools/smallvalue_generators.ML
     1.1 --- a/src/HOL/Tools/smallvalue_generators.ML	Fri Dec 03 08:40:47 2010 +0100
     1.2 +++ b/src/HOL/Tools/smallvalue_generators.ML	Fri Dec 03 08:40:47 2010 +0100
     1.3 @@ -10,6 +10,7 @@
     1.4      Proof.context -> term -> int -> term list option * (bool list * bool)
     1.5    val put_counterexample: (unit -> int -> term list option)
     1.6      -> Proof.context -> Proof.context
     1.7 +  val smart_quantifier : bool Config.T;
     1.8    val setup: theory -> theory
     1.9  end;
    1.10  
    1.11 @@ -20,6 +21,11 @@
    1.12  
    1.13  val define_foundationally = false
    1.14  
    1.15 +(* dynamic options *)
    1.16 +
    1.17 +val (smart_quantifier, setup_smart_quantifier) =
    1.18 +  Attrib.config_bool "quickcheck_smart_quantifier" (K true)
    1.19 +
    1.20  (** general term functions **)
    1.21  
    1.22  fun mk_measure f =
    1.23 @@ -209,12 +215,50 @@
    1.24  
    1.25  val target = "Quickcheck";
    1.26  
    1.27 -fun mk_generator_expr thy prop Ts =
    1.28 +fun mk_smart_generator_expr ctxt t =
    1.29    let
    1.30 +    val ((vnames, Ts), t') = apfst split_list (strip_abs t)
    1.31 +    val ([depth_name], ctxt') = Variable.variant_fixes ["depth"] ctxt
    1.32 +    val (names, ctxt'') = Variable.variant_fixes vnames ctxt'
    1.33 +    val (term_names, ctxt''') = Variable.variant_fixes (map (prefix "t_") vnames) ctxt''
    1.34 +    val depth = Free (depth_name, @{typ code_numeral})
    1.35 +    val frees = map2 (curry Free) names Ts
    1.36 +    val term_vars = map (fn n => Free (n, @{typ "unit => term"})) term_names 
    1.37 +    fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B)
    1.38 +      | strip_imp A = ([], A)
    1.39 +    val (assms, concl) = strip_imp (subst_bounds (rev frees, t'))
    1.40 +    val terms = HOLogic.mk_list @{typ term} (map (fn v => v $ @{term "()"}) term_vars)
    1.41 +    fun mk_small_closure (free as Free (_, T), term_var) t =
    1.42 +      Const (@{const_name "Smallcheck.full_small_class.full_small"}, full_smallT T)
    1.43 +        $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) 
    1.44 +          $ lambda free (lambda term_var t)) $ depth
    1.45 +    fun lookup v = the (AList.lookup (op =) (names ~~ (frees ~~ term_vars)) v)
    1.46 +    val none_t = @{term "None :: term list option"}
    1.47 +    fun mk_safe_if (cond, then_t, else_t) =
    1.48 +      @{term "Smallcheck.catch_match :: term list option => term list option => term list option"} $
    1.49 +        (@{term "If :: bool => term list option => term list option => term list option"}
    1.50 +        $ cond $ then_t $ else_t) $ none_t;
    1.51 +    fun mk_test_term bound_vars assms =
    1.52 +      let
    1.53 +        fun vars_of t = subtract (op =) bound_vars (Term.add_free_names t [])
    1.54 +        val (vars, check) =
    1.55 +          case assms of [] =>
    1.56 +            (vars_of concl, (concl, none_t, @{term "Some :: term list => term list option"} $ terms))
    1.57 +          | assm :: assms =>
    1.58 +            (vars_of assm, (assm, mk_test_term (union (op =) (vars_of assm) bound_vars) assms, none_t))
    1.59 +      in
    1.60 +        fold_rev mk_small_closure (map lookup vars) (mk_safe_if check)
    1.61 +      end
    1.62 +  in lambda depth (mk_test_term [] assms) end
    1.63 +
    1.64 +fun mk_generator_expr ctxt t =
    1.65 +  let
    1.66 +    val Ts = (map snd o fst o strip_abs) t;
    1.67 +    val thy = ProofContext.theory_of ctxt
    1.68      val bound_max = length Ts - 1;
    1.69      val bounds = map_index (fn (i, ty) =>
    1.70        (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
    1.71 -    val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds);
    1.72 +    val result = list_comb (t, map (fn (i, _, _, _) => Bound i) bounds);
    1.73      val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
    1.74      val check =
    1.75        @{term "Smallcheck.catch_match :: term list option => term list option => term list option"} $
    1.76 @@ -228,26 +272,26 @@
    1.77    in Abs ("d", @{typ code_numeral}, fold_rev mk_small_closure bounds check) end
    1.78  
    1.79  fun compile_generator_expr ctxt t =
    1.80 -  let
    1.81 -    val Ts = (map snd o fst o strip_abs) t;
    1.82 -    val thy = ProofContext.theory_of ctxt
    1.83 -  in if Config.get ctxt Quickcheck.report then
    1.84 +  if Config.get ctxt Quickcheck.report then
    1.85      error "Compilation with reporting facility is not supported"
    1.86    else
    1.87      let
    1.88 -      val t' = mk_generator_expr thy t Ts;
    1.89 +      val thy = ProofContext.theory_of ctxt
    1.90 +      val t' =
    1.91 +        (if Config.get ctxt smart_quantifier then mk_smart_generator_expr else mk_generator_expr)
    1.92 +          ctxt t;
    1.93        val compile = Code_Runtime.dynamic_value_strict
    1.94          (Counterexample.get, put_counterexample, "Smallvalue_Generators.put_counterexample")
    1.95          thy (SOME target) (fn proc => fn g => g #> (Option.map o map) proc) t' [];
    1.96        val dummy_report = ([], false)
    1.97 -    in compile #> rpair dummy_report end
    1.98 -  end;
    1.99 +    in compile #> rpair dummy_report end;
   1.100  
   1.101  (** setup **)
   1.102  
   1.103  val setup =
   1.104    Datatype.interpretation
   1.105      (Quickcheck_Generators.ensure_sort_datatype (@{sort full_small}, instantiate_smallvalue_datatype))
   1.106 +  #> setup_smart_quantifier
   1.107    #> Context.theory_map
   1.108      (Quickcheck.add_generator ("small", compile_generator_expr));
   1.109