adding function generation to SmallCheck; activating exhaustive search space testing
authorbulwahn
Mon Nov 22 10:41:58 2010 +0100 (2010-11-22)
changeset 40639f1f0e6adca0a
parent 40638 6b137c96df07
child 40640 3fa1c2472568
adding function generation to SmallCheck; activating exhaustive search space testing
src/HOL/Smallcheck.thy
src/HOL/Tools/smallvalue_generators.ML
     1.1 --- a/src/HOL/Smallcheck.thy	Mon Nov 22 10:41:57 2010 +0100
     1.2 +++ b/src/HOL/Smallcheck.thy	Mon Nov 22 10:41:58 2010 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4  instantiation unit :: small
     1.5  begin
     1.6  
     1.7 -definition "find_first f d = f ()"
     1.8 +definition "small f d = f ()"
     1.9  
    1.10  instance ..
    1.11  
    1.12 @@ -48,6 +48,73 @@
    1.13  
    1.14  end
    1.15  
    1.16 +section {* full small value generator type classes *}
    1.17 +
    1.18 +class full_small = term_of +
    1.19 +fixes full_small :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
    1.20 +
    1.21 +instantiation unit :: full_small
    1.22 +begin
    1.23 +
    1.24 +definition "full_small f d = f (Code_Evaluation.valtermify ())"
    1.25 +
    1.26 +instance ..
    1.27 +
    1.28 +end
    1.29 +
    1.30 +instantiation int :: full_small
    1.31 +begin
    1.32 +
    1.33 +function full_small' :: "(int * (unit => term) => term list option) => int => int => term list option"
    1.34 +  where "full_small' f d i = (if d < i then None else (case f (i, %_. Code_Evaluation.term_of i) of Some t => Some t | None => full_small' f d (i + 1)))"
    1.35 +by pat_completeness auto
    1.36 +
    1.37 +termination 
    1.38 +  by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
    1.39 +
    1.40 +definition "full_small f d = full_small' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
    1.41 +
    1.42 +instance ..
    1.43 +
    1.44 +end
    1.45 +
    1.46 +instantiation prod :: (full_small, full_small) full_small
    1.47 +begin
    1.48 +ML {* @{const_name "Pair"} *}
    1.49 +definition
    1.50 +  "full_small f d = full_small (%(x, t1). full_small (%(y, t2). f ((x, y),
    1.51 +    %u. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of (Pair :: 'a => 'b => ('a * 'b))) (t1 ())) (t2 ()))) d) d"
    1.52 +
    1.53 +instance ..
    1.54 +
    1.55 +end
    1.56 +
    1.57 +instantiation "fun" :: ("{equal, full_small}", full_small) full_small
    1.58 +begin
    1.59 +
    1.60 +fun full_small_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
    1.61 +where
    1.62 +  "full_small_fun' f i d = (if i > 1 then
    1.63 +    full_small (%(a, at). full_small (%(b, bt).
    1.64 +      full_small_fun' (%(g, gt). f (g(a := b),
    1.65 +        (%_. let T1 = (Typerep.typerep (TYPE('a))); T2 = (Typerep.typerep (TYPE('b))) in Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
    1.66 +         
    1.67 +(Code_Evaluation.Const (STR ''Fun.fun_upd'')
    1.68 +
    1.69 +(Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2], Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]]))
    1.70 +
    1.71 + (gt ())) (at ())) (bt ())))) (i - 1) d) d) d else (if i > 0 then
    1.72 +  full_small (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d else None))"
    1.73 +
    1.74 +definition full_small_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option"
    1.75 +where
    1.76 +  "full_small_fun f d = full_small_fun' f d d" 
    1.77 +
    1.78 +
    1.79 +instance ..
    1.80 +
    1.81 +end
    1.82 +
    1.83  subsection {* Defining combinators for any first-order data type *}
    1.84  
    1.85  definition catch_match :: "term list option => term list option => term list option"
    1.86 @@ -59,7 +126,7 @@
    1.87  
    1.88  use "Tools/smallvalue_generators.ML"
    1.89  
    1.90 -(* We do not activate smallcheck yet. 
    1.91 +(* We do not activate smallcheck yet.
    1.92  setup {* Smallvalue_Generators.setup *}
    1.93  *)
    1.94  
     2.1 --- a/src/HOL/Tools/smallvalue_generators.ML	Mon Nov 22 10:41:57 2010 +0100
     2.2 +++ b/src/HOL/Tools/smallvalue_generators.ML	Mon Nov 22 10:41:58 2010 +0100
     2.3 @@ -6,7 +6,6 @@
     2.4  
     2.5  signature SMALLVALUE_GENERATORS =
     2.6  sig
     2.7 -  val ensure_smallvalue_datatype: Datatype.config -> string list -> theory -> theory
     2.8    val compile_generator_expr:
     2.9      Proof.context -> term -> int -> term list option * (bool list * bool)
    2.10    val put_counterexample: (unit -> int -> term list option)
    2.11 @@ -51,10 +50,12 @@
    2.12  
    2.13  (** abstract syntax **)
    2.14  
    2.15 +fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => Code_Evaluation.term"});
    2.16 +
    2.17  val size = @{term "i :: code_numeral"}
    2.18  val size_pred = @{term "(i :: code_numeral) - 1"}
    2.19  val size_ge_zero = @{term "(i :: code_numeral) > 0"}
    2.20 -fun test_function T = Free ("f", T --> @{typ "term list option"})
    2.21 +fun test_function T = Free ("f", termifyT T --> @{typ "term list option"})
    2.22  
    2.23  fun mk_none_continuation (x, y) =
    2.24    let
    2.25 @@ -75,16 +76,23 @@
    2.26  fun smallT T = (T --> @{typ "Code_Evaluation.term list option"}) --> @{typ code_numeral}
    2.27    --> @{typ "Code_Evaluation.term list option"}
    2.28  
    2.29 +val full_smallN = "full_small";
    2.30 +
    2.31 +fun full_smallT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
    2.32 +  --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
    2.33 + 
    2.34  fun mk_equations thy descr vs tycos (names, auxnames) (Ts, Us) =
    2.35    let
    2.36 -    val smallsN = map (prefix (smallN ^ "_")) (names @ auxnames);
    2.37 -    val smalls = map2 (fn name => fn T => Free (name, smallT T))
    2.38 +    val smallsN = map (prefix (full_smallN ^ "_")) (names @ auxnames);
    2.39 +    val smalls = map2 (fn name => fn T => Free (name, full_smallT T))
    2.40        smallsN (Ts @ Us)
    2.41      fun mk_small_call T =
    2.42        let
    2.43 -        val small = Const (@{const_name "Smallcheck.small_class.small"}, smallT T)        
    2.44 +        val small = Const (@{const_name "Smallcheck.full_small_class.full_small"}, full_smallT T)        
    2.45        in
    2.46 -        (T, (fn t => small $ absdummy (T, t) $ size_pred))
    2.47 +        (T, (fn t => small $
    2.48 +          (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
    2.49 +          $ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred))
    2.50        end
    2.51      fun mk_small_aux_call fTs (k, _) (tyco, Ts) =
    2.52        let
    2.53 @@ -92,14 +100,23 @@
    2.54          val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
    2.55          val small = nth smalls k
    2.56        in
    2.57 -        (T, (fn t => small $ absdummy (T, t) $ size_pred))
    2.58 +       (T, (fn t => small $
    2.59 +          (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
    2.60 +            $ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred))  
    2.61        end
    2.62      fun mk_consexpr simpleT (c, xs) =
    2.63        let
    2.64          val (Ts, fns) = split_list xs
    2.65          val constr = Const (c, Ts ---> simpleT)
    2.66 -        val bounds = map Bound (((length xs) - 1) downto 0)
    2.67 -        val start_term = test_function simpleT $ (list_comb (constr, bounds))
    2.68 +        val bounds = map (fn x => Bound (2 * x + 1)) (((length xs) - 1) downto 0)
    2.69 +        val term_bounds = map (fn x => Bound (2 * x)) (((length xs) - 1) downto 0)
    2.70 +        val Eval_App = Const ("Code_Evaluation.App", HOLogic.termT --> HOLogic.termT --> HOLogic.termT)
    2.71 +        val Eval_Const = Const ("Code_Evaluation.Const", HOLogic.literalT --> @{typ typerep} --> HOLogic.termT)
    2.72 +        val term = fold (fn u => fn t => Eval_App $ t $ (u $ @{term "()"}))
    2.73 +          bounds (Eval_Const $ HOLogic.mk_literal c $ HOLogic.mk_typerep (Ts ---> simpleT))
    2.74 +        val start_term = test_function simpleT $ 
    2.75 +        (HOLogic.pair_const simpleT @{typ "unit => Code_Evaluation.term"}
    2.76 +          $ (list_comb (constr, bounds)) $ absdummy (@{typ unit}, term))
    2.77        in fold_rev (fn f => fn t => f t) fns start_term end
    2.78      fun mk_rhs exprs =
    2.79          @{term "If :: bool => term list option => term list option => term list option"}
    2.80 @@ -129,7 +146,7 @@
    2.81          PRIMITIVE (Drule.cterm_instantiate [(cert (Var v), rel')]) st'
    2.82        end
    2.83    | _ => Seq.empty;
    2.84 -
    2.85 +  
    2.86  fun instantiate_smallvalue_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
    2.87    let
    2.88      val _ = Datatype_Aux.message config "Creating smallvalue generators ...";
    2.89 @@ -155,45 +172,22 @@
    2.90        Pat_Completeness.pat_completeness_tac ctxt 1
    2.91        THEN auto_tac (clasimpset_of ctxt)
    2.92    in
    2.93 -    thy
    2.94 -    |> Class.instantiation (tycos, vs, @{sort small})
    2.95 +    (thy
    2.96 +    |> Class.instantiation (tycos, vs, @{sort full_small})
    2.97      |> Function.add_function
    2.98        (map (fn (T, (name, _)) =>
    2.99 -          Syntax.no_syn (Binding.conceal (Binding.name name), SOME (smallT T))) eqs)
   2.100 +          Syntax.no_syn (Binding.conceal (Binding.name name), SOME (full_smallT T))) eqs)
   2.101          (map (pair (apfst Binding.conceal Attrib.empty_binding) o snd o snd) eqs)
   2.102          Function_Common.default_config pat_completeness_auto
   2.103      |> snd
   2.104      |> Local_Theory.restore
   2.105      |> (fn lthy => Function.prove_termination NONE (termination_tac lthy) lthy)
   2.106      |> snd
   2.107 -    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
   2.108 -  end;
   2.109 -
   2.110 -fun ensure_smallvalue_datatype config raw_tycos thy =
   2.111 -  let
   2.112 -    val algebra = Sign.classes_of thy;
   2.113 -    val (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) =
   2.114 -      Datatype.the_descr thy raw_tycos;
   2.115 -    val typerep_vs = (map o apsnd)
   2.116 -      (curry (Sorts.inter_sort algebra) @{sort typerep}) raw_vs;
   2.117 -    val smallvalue_insts = (map (rpair @{sort small}) o flat o maps snd o maps snd)
   2.118 -      (Datatype_Aux.interpret_construction descr typerep_vs
   2.119 -        { atyp = single, dtyp = (K o K o K) [] });
   2.120 -    (*val term_of_insts = (map (rpair @{sort term_of}) o flat o maps snd o maps snd)
   2.121 -      (Datatype_Aux.interpret_construction descr typerep_vs
   2.122 -        { atyp = K [], dtyp = K o K });*)
   2.123 -    val has_inst = exists (fn tyco =>
   2.124 -      can (Sorts.mg_domain algebra tyco) @{sort small}) tycos;
   2.125 -  in if has_inst then thy
   2.126 -    else case Quickcheck_Generators.perhaps_constrain thy smallvalue_insts typerep_vs
   2.127 -     of SOME constrain => (instantiate_smallvalue_datatype config descr
   2.128 -          (map constrain typerep_vs) tycos prfx (names, auxnames)
   2.129 -            ((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
   2.130 -            handle FUNCTION_TYPE =>
   2.131 -              (Datatype_Aux.message config
   2.132 -                "Creation of smallvalue generators failed because the datatype contains a function type";
   2.133 -              thy))
   2.134 -      | NONE => thy
   2.135 +    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac [])))
   2.136 +    handle FUNCTION_TYPE =>
   2.137 +    (Datatype_Aux.message config
   2.138 +      "Creation of smallvalue generators failed because the datatype contains a function type";
   2.139 +    thy)
   2.140    end;
   2.141  
   2.142  (** building and compiling generator expressions **)
   2.143 @@ -209,19 +203,20 @@
   2.144  fun mk_generator_expr thy prop Ts =
   2.145    let
   2.146      val bound_max = length Ts - 1;
   2.147 -    val bounds = map Bound (bound_max downto 0)
   2.148 -    val result = list_comb (prop, bounds);
   2.149 -    val terms = HOLogic.mk_list @{typ term} (map2 HOLogic.mk_term_of Ts bounds);
   2.150 +    val bounds = map_index (fn (i, ty) =>
   2.151 +      (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
   2.152 +    val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds);
   2.153 +    val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
   2.154      val check =
   2.155        @{term "Smallcheck.catch_match :: term list option => term list option => term list option"} $
   2.156          (@{term "If :: bool => term list option => term list option => term list option"}
   2.157 -        $ result $ @{term "None :: term list option"}
   2.158 -        $ (@{term "Some :: term list => term list option"} $ terms))
   2.159 +        $ result $ @{term "None :: term list option"} $ (@{term "Some :: term list => term list option"} $ terms))
   2.160        $ @{term "None :: term list option"};
   2.161 -    fun mk_small_closure (depth, T) t =
   2.162 -      Const (@{const_name "Smallcheck.small_class.small"}, smallT T)
   2.163 -        $ absdummy (T, t) $ depth
   2.164 -  in Abs ("d", @{typ code_numeral}, fold_rev mk_small_closure (rev bounds ~~ Ts) check) end
   2.165 +    fun mk_small_closure (_, _, i, T) t =
   2.166 +      Const (@{const_name "Smallcheck.full_small_class.full_small"}, full_smallT T)
   2.167 +        $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) 
   2.168 +        $ absdummy (T, absdummy (@{typ "unit => term"}, t))) $ Bound i
   2.169 +  in Abs ("d", @{typ code_numeral}, fold_rev mk_small_closure bounds check) end
   2.170  
   2.171  fun compile_generator_expr ctxt t =
   2.172    let
   2.173 @@ -242,7 +237,8 @@
   2.174  (** setup **)
   2.175  
   2.176  val setup =
   2.177 -  Datatype.interpretation ensure_smallvalue_datatype
   2.178 +  Datatype.interpretation
   2.179 +    (Quickcheck_Generators.ensure_sort_datatype (@{sort full_small}, instantiate_smallvalue_datatype))
   2.180    #> Context.theory_map
   2.181      (Quickcheck.add_generator ("small", compile_generator_expr));
   2.182