new compilation for exhaustive quickcheck
authorbulwahn
Fri Apr 08 16:31:14 2011 +0200 (2011-04-08)
changeset 4230434366f39d32d
parent 42291 682b35dc1926
child 42305 494c31fdec95
new compilation for exhaustive quickcheck
src/HOL/Quickcheck_Exhaustive.thy
src/HOL/Tools/Quickcheck/exhaustive_generators.ML
     1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Thu Apr 07 21:49:24 2011 +0200
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Fri Apr 08 16:31:14 2011 +0200
     1.3 @@ -16,22 +16,35 @@
     1.4  subsection {* exhaustive generator type classes *}
     1.5  
     1.6  class exhaustive = term_of +
     1.7 -fixes exhaustive :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
     1.8 +  fixes exhaustive :: "('a \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
     1.9 +  fixes full_exhaustive :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
    1.10  
    1.11  instantiation code_numeral :: exhaustive
    1.12  begin
    1.13  
    1.14 -function exhaustive_code_numeral' :: "(code_numeral * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
    1.15 +function full_exhaustive_code_numeral' :: "(code_numeral * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
    1.16 +  where "full_exhaustive_code_numeral' f d i =
    1.17 +    (if d < i then None
    1.18 +    else (f (i, %_. Code_Evaluation.term_of i)) orelse (full_exhaustive_code_numeral' f d (i + 1)))"
    1.19 +by pat_completeness auto
    1.20 +
    1.21 +termination
    1.22 +  by (relation "measure (%(_, d, i). Code_Numeral.nat_of (d + 1 - i))") auto
    1.23 +
    1.24 +definition "full_exhaustive f d = full_exhaustive_code_numeral' f d 0"
    1.25 +
    1.26 +function exhaustive_code_numeral' :: "(code_numeral => term list option) => code_numeral => code_numeral => term list option"
    1.27    where "exhaustive_code_numeral' f d i =
    1.28      (if d < i then None
    1.29 -    else (f (i, %_. Code_Evaluation.term_of i)) orelse (exhaustive_code_numeral' f d (i + 1)))"
    1.30 +    else (f i orelse exhaustive_code_numeral' f d (i + 1)))"
    1.31  by pat_completeness auto
    1.32  
    1.33 -termination 
    1.34 +termination
    1.35    by (relation "measure (%(_, d, i). Code_Numeral.nat_of (d + 1 - i))") auto
    1.36  
    1.37  definition "exhaustive f d = exhaustive_code_numeral' f d 0"
    1.38  
    1.39 +
    1.40  instance ..
    1.41  
    1.42  end
    1.43 @@ -39,7 +52,9 @@
    1.44  instantiation nat :: exhaustive
    1.45  begin
    1.46  
    1.47 -definition "exhaustive f d = exhaustive (%(x, xt). f (Code_Numeral.nat_of x, %_. Code_Evaluation.term_of (Code_Numeral.nat_of x))) d"
    1.48 +definition "exhaustive f d = exhaustive (%x. f (Code_Numeral.nat_of x)) d"
    1.49 +
    1.50 +definition "full_exhaustive f d = full_exhaustive (%(x, xt). f (Code_Numeral.nat_of x, %_. Code_Evaluation.term_of (Code_Numeral.nat_of x))) d"
    1.51  
    1.52  instance ..
    1.53  
    1.54 @@ -48,8 +63,8 @@
    1.55  instantiation int :: exhaustive
    1.56  begin
    1.57  
    1.58 -function exhaustive' :: "(int * (unit => term) => term list option) => int => int => term list option"
    1.59 -  where "exhaustive' f d i = (if d < i then None else (case f (i, %_. Code_Evaluation.term_of i) of Some t => Some t | None => exhaustive' f d (i + 1)))"
    1.60 +function exhaustive' :: "(int => term list option) => int => int => term list option"
    1.61 +  where "exhaustive' f d i = (if d < i then None else (f i orelse exhaustive' f d (i + 1)))"
    1.62  by pat_completeness auto
    1.63  
    1.64  termination 
    1.65 @@ -57,6 +72,15 @@
    1.66  
    1.67  definition "exhaustive f d = exhaustive' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
    1.68  
    1.69 +function full_exhaustive' :: "(int * (unit => term) => term list option) => int => int => term list option"
    1.70 +  where "full_exhaustive' f d i = (if d < i then None else (case f (i, %_. Code_Evaluation.term_of i) of Some t => Some t | None => full_exhaustive' f d (i + 1)))"
    1.71 +by pat_completeness auto
    1.72 +
    1.73 +termination 
    1.74 +  by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
    1.75 +
    1.76 +definition "full_exhaustive f d = full_exhaustive' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
    1.77 +
    1.78  instance ..
    1.79  
    1.80  end
    1.81 @@ -65,7 +89,10 @@
    1.82  begin
    1.83  
    1.84  definition
    1.85 -  "exhaustive f d = exhaustive (%(x, t1). exhaustive (%(y, t2). f ((x, y),
    1.86 +  "exhaustive f d = exhaustive (%x. exhaustive (%y. f ((x, y))) d) d"
    1.87 +
    1.88 +definition
    1.89 +  "full_exhaustive f d = full_exhaustive (%(x, t1). full_exhaustive (%(y, t2). f ((x, y),
    1.90      %u. let T1 = (Typerep.typerep (TYPE('a)));
    1.91              T2 = (Typerep.typerep (TYPE('b)))
    1.92      in Code_Evaluation.App (Code_Evaluation.App (
    1.93 @@ -80,11 +107,23 @@
    1.94  instantiation "fun" :: ("{equal, exhaustive}", exhaustive) exhaustive
    1.95  begin
    1.96  
    1.97 -fun exhaustive_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
    1.98 +fun exhaustive_fun' :: "(('a => 'b) => term list option) => code_numeral => code_numeral => term list option"
    1.99 +where
   1.100 +  "exhaustive_fun' f i d = (exhaustive (%b. f (%_. b)) d)
   1.101 +   orelse (if i > 1 then
   1.102 +     exhaustive_fun' (%g. exhaustive (%a. exhaustive (%b.
   1.103 +       f (g(a := b))) d) d) (i - 1) d else None)"
   1.104 +
   1.105 +definition exhaustive_fun :: "(('a => 'b) => term list option) => code_numeral => term list option"
   1.106  where
   1.107 -  "exhaustive_fun' f i d = (exhaustive (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d)
   1.108 +  "exhaustive_fun f d = exhaustive_fun' f d d" 
   1.109 +
   1.110 +
   1.111 +fun full_exhaustive_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
   1.112 +where
   1.113 +  "full_exhaustive_fun' f i d = (full_exhaustive (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d)
   1.114     orelse (if i > 1 then
   1.115 -     exhaustive_fun' (%(g, gt). exhaustive (%(a, at). exhaustive (%(b, bt).
   1.116 +     full_exhaustive_fun' (%(g, gt). full_exhaustive (%(a, at). full_exhaustive (%(b, bt).
   1.117         f (g(a := b),
   1.118           (%_. let A = (Typerep.typerep (TYPE('a)));
   1.119                    B = (Typerep.typerep (TYPE('b)));
   1.120 @@ -94,9 +133,9 @@
   1.121                    (Code_Evaluation.Const (STR ''Fun.fun_upd'') (fun (fun A B) (fun A (fun B (fun A B)))))
   1.122                  (gt ())) (at ())) (bt ())))) d) d) (i - 1) d else None)"
   1.123  
   1.124 -definition exhaustive_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option"
   1.125 +definition full_exhaustive_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option"
   1.126  where
   1.127 -  "exhaustive_fun f d = exhaustive_fun' f d d" 
   1.128 +  "full_exhaustive_fun f d = full_exhaustive_fun' f d d" 
   1.129  
   1.130  instance ..
   1.131  
     2.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Thu Apr 07 21:49:24 2011 +0200
     2.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Apr 08 16:31:14 2011 +0200
     2.3 @@ -28,6 +28,9 @@
     2.4  val (smart_quantifier, setup_smart_quantifier) =
     2.5    Attrib.config_bool "quickcheck_smart_quantifier" (K true)
     2.6  
     2.7 +val (full_support, setup_full_support) =
     2.8 +  Attrib.config_bool "quickcheck_full_support" (K true)
     2.9 +
    2.10  val (quickcheck_pretty, setup_quickcheck_pretty) =
    2.11    Attrib.config_bool "quickcheck_pretty" (K true)
    2.12   
    2.13 @@ -61,7 +64,9 @@
    2.14  val size = @{term "i :: code_numeral"}
    2.15  val size_pred = @{term "(i :: code_numeral) - 1"}
    2.16  val size_ge_zero = @{term "(i :: code_numeral) > 0"}
    2.17 -fun test_function T = Free ("f", termifyT T --> @{typ "term list option"})
    2.18 +
    2.19 +fun test_function T = Free ("f", T --> @{typ "term list option"})
    2.20 +fun full_test_function T = Free ("f", termifyT T --> @{typ "term list option"})
    2.21  
    2.22  fun mk_none_continuation (x, y) =
    2.23    let
    2.24 @@ -76,8 +81,12 @@
    2.25  
    2.26  exception FUNCTION_TYPE;
    2.27  val exhaustiveN = "exhaustive";
    2.28 +val full_exhaustiveN = "full_exhaustive";
    2.29  
    2.30 -fun exhaustiveT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
    2.31 +fun exhaustiveT T = (T --> @{typ "Code_Evaluation.term list option"})
    2.32 +  --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
    2.33 +
    2.34 +fun full_exhaustiveT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
    2.35    --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
    2.36  
    2.37  fun check_allT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
    2.38 @@ -89,7 +98,45 @@
    2.39        let
    2.40          val exhaustive = Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)
    2.41        in
    2.42 -        (T, (fn t => exhaustive $
    2.43 +        (T, fn t => exhaustive $ absdummy (T, t) $ size_pred)
    2.44 +      end
    2.45 +    fun mk_aux_call fTs (k, _) (tyco, Ts) =
    2.46 +      let
    2.47 +        val T = Type (tyco, Ts)
    2.48 +        val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
    2.49 +      in
    2.50 +       (T, fn t => nth exhaustives k $ absdummy (T, t) $ size_pred)
    2.51 +      end
    2.52 +    fun mk_consexpr simpleT (c, xs) =
    2.53 +      let
    2.54 +        val (Ts, fns) = split_list xs
    2.55 +        val constr = Const (c, Ts ---> simpleT)
    2.56 +        val bounds = map Bound (((length xs) - 1) downto 0)
    2.57 +        val term_bounds = map (fn x => Bound (2 * x)) (((length xs) - 1) downto 0)
    2.58 +        val start_term = test_function simpleT $ list_comb (constr, bounds)
    2.59 +      in fold_rev (fn f => fn t => f t) fns start_term end
    2.60 +    fun mk_rhs exprs =
    2.61 +        @{term "If :: bool => term list option => term list option => term list option"}
    2.62 +            $ size_ge_zero $ (foldr1 mk_none_continuation exprs) $ @{term "None :: term list option"}
    2.63 +    val rhss =
    2.64 +      Datatype_Aux.interpret_construction descr vs
    2.65 +        { atyp = mk_call, dtyp = mk_aux_call }
    2.66 +      |> (map o apfst) Type
    2.67 +      |> map (fn (T, cs) => map (mk_consexpr T) cs)
    2.68 +      |> map mk_rhs
    2.69 +    val lhss = map2 (fn t => fn T => t $ test_function T $ size) exhaustives (Ts @ Us)
    2.70 +    val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
    2.71 +  in
    2.72 +    eqs
    2.73 +  end
    2.74 +    
    2.75 +fun mk_full_equations descr vs tycos full_exhaustives (Ts, Us) =
    2.76 +  let
    2.77 +    fun mk_call T =
    2.78 +      let
    2.79 +        val full_exhaustive = Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.full_exhaustive"}, full_exhaustiveT T)
    2.80 +      in
    2.81 +        (T, (fn t => full_exhaustive $
    2.82            (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
    2.83            $ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred))
    2.84        end
    2.85 @@ -98,7 +145,7 @@
    2.86          val T = Type (tyco, Ts)
    2.87          val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
    2.88        in
    2.89 -       (T, (fn t => nth exhaustives k $
    2.90 +       (T, (fn t => nth full_exhaustives k $
    2.91            (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
    2.92              $ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred))
    2.93        end
    2.94 @@ -112,7 +159,7 @@
    2.95          val Eval_Const = Const ("Code_Evaluation.Const", HOLogic.literalT --> @{typ typerep} --> HOLogic.termT)
    2.96          val term = fold (fn u => fn t => Eval_App $ t $ (u $ @{term "()"}))
    2.97            bounds (Eval_Const $ HOLogic.mk_literal c $ HOLogic.mk_typerep (Ts ---> simpleT))
    2.98 -        val start_term = test_function simpleT $ 
    2.99 +        val start_term = full_test_function simpleT $ 
   2.100          (HOLogic.pair_const simpleT @{typ "unit => Code_Evaluation.term"}
   2.101            $ (list_comb (constr, bounds)) $ absdummy (@{typ unit}, term))
   2.102        in fold_rev (fn f => fn t => f t) fns start_term end
   2.103 @@ -125,7 +172,7 @@
   2.104        |> (map o apfst) Type
   2.105        |> map (fn (T, cs) => map (mk_consexpr T) cs)
   2.106        |> map mk_rhs
   2.107 -    val lhss = map2 (fn t => fn T => t $ test_function T $ size) exhaustives (Ts @ Us);
   2.108 +    val lhss = map2 (fn t => fn T => t $ full_test_function T $ size) full_exhaustives (Ts @ Us);
   2.109      val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
   2.110    in
   2.111      eqs
   2.112 @@ -157,13 +204,18 @@
   2.113  fun instantiate_exhaustive_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
   2.114    let
   2.115      val _ = Datatype_Aux.message config "Creating exhaustive generators...";
   2.116 -    val exhaustivesN = map (prefix (exhaustiveN ^ "_")) (names @ auxnames);
   2.117 +    val exhaustivesN = map (prefix (exhaustiveN ^ "_")) (names @ auxnames)
   2.118 +    val full_exhaustivesN = map (prefix (full_exhaustiveN ^ "_")) (names @ auxnames)
   2.119    in
   2.120      thy
   2.121      |> Class.instantiation (tycos, vs, @{sort exhaustive})
   2.122      |> Quickcheck_Common.define_functions
   2.123          (fn exhaustives => mk_equations descr vs tycos exhaustives (Ts, Us), SOME termination_tac)
   2.124          prfx ["f", "i"] exhaustivesN (map exhaustiveT (Ts @ Us))
   2.125 +    |> Quickcheck_Common.define_functions
   2.126 +        (fn full_exhaustives => mk_full_equations descr vs tycos full_exhaustives (Ts, Us),
   2.127 +        SOME termination_tac)
   2.128 +        prfx ["f", "i"] full_exhaustivesN (map full_exhaustiveT (Ts @ Us))
   2.129      |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
   2.130    end handle FUNCTION_TYPE =>
   2.131      (Datatype_Aux.message config
   2.132 @@ -244,6 +296,48 @@
   2.133      val names = Term.add_free_names t []
   2.134      val frees = map Free (Term.add_frees t [])
   2.135      val ([depth_name], ctxt'') = Variable.variant_fixes ["depth"] ctxt'
   2.136 +    val depth = Free (depth_name, @{typ code_numeral})
   2.137 +    val return = @{term "Some :: term list => term list option"} $
   2.138 +      (HOLogic.mk_list @{typ "term"}
   2.139 +        (map (fn t => HOLogic.mk_term_of (fastype_of t) t) (frees @ eval_terms)))
   2.140 +    fun mk_exhaustive_closure (free as Free (_, T)) t =
   2.141 +      Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)
   2.142 +        $ lambda free t $ depth
   2.143 +    val none_t = @{term "None :: term list option"}
   2.144 +    fun mk_safe_if (cond, then_t, else_t) =
   2.145 +      @{term "Quickcheck_Exhaustive.catch_match :: term list option => term list option => term list option"} $
   2.146 +        (@{term "If :: bool => term list option => term list option => term list option"}
   2.147 +        $ cond $ then_t $ else_t) $ none_t;
   2.148 +    fun lookup v = the (AList.lookup (op =) (names ~~ frees) v)
   2.149 +    fun mk_naive_test_term t =
   2.150 +      fold_rev mk_exhaustive_closure frees (mk_safe_if (t, none_t, return)) 
   2.151 +    fun mk_smart_test_term' concl bound_vars assms =
   2.152 +      let
   2.153 +        fun vars_of t = subtract (op =) bound_vars (Term.add_free_names t [])
   2.154 +        val (vars, check) =
   2.155 +          case assms of [] => (vars_of concl, (concl, none_t, return))
   2.156 +            | assm :: assms => (vars_of assm, (assm,
   2.157 +                mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms, none_t))
   2.158 +      in
   2.159 +        fold_rev mk_exhaustive_closure (map lookup vars) (mk_safe_if check)
   2.160 +      end
   2.161 +    fun mk_smart_test_term t =
   2.162 +      let
   2.163 +        val (assms, concl) = Quickcheck_Common.strip_imp t
   2.164 +      in
   2.165 +        mk_smart_test_term' concl [] assms
   2.166 +      end
   2.167 +    val mk_test_term =
   2.168 +      if Config.get ctxt smart_quantifier then mk_smart_test_term else mk_naive_test_term 
   2.169 +  in lambda depth (mk_test_term t) end
   2.170 +
   2.171 +fun mk_full_generator_expr ctxt (t, eval_terms) =
   2.172 +  let
   2.173 +    val thy = ProofContext.theory_of ctxt
   2.174 +    val ctxt' = Variable.auto_fixes t ctxt
   2.175 +    val names = Term.add_free_names t []
   2.176 +    val frees = map Free (Term.add_frees t [])
   2.177 +    val ([depth_name], ctxt'') = Variable.variant_fixes ["depth"] ctxt'
   2.178      val (term_names, ctxt''') = Variable.variant_fixes (map (prefix "t_") names) ctxt''
   2.179      val depth = Free (depth_name, @{typ code_numeral})
   2.180      val term_vars = map (fn n => Free (n, @{typ "unit => term"})) term_names
   2.181 @@ -288,7 +382,7 @@
   2.182        if Config.get ctxt smart_quantifier then mk_smart_test_term else mk_naive_test_term 
   2.183    in lambda depth (mk_test_term t) end
   2.184  
   2.185 -val mk_parametric_generator_expr =
   2.186 +fun mk_parametric_generator_expr mk_generator_expr =
   2.187    Quickcheck_Common.gen_mk_parametric_generator_expr 
   2.188      ((mk_generator_expr, absdummy (@{typ "code_numeral"}, @{term "None :: term list option"})),
   2.189        @{typ "code_numeral => term list option"})
   2.190 @@ -359,7 +453,9 @@
   2.191  fun compile_generator_expr ctxt ts =
   2.192    let
   2.193      val thy = ProofContext.theory_of ctxt
   2.194 -    val t' = mk_parametric_generator_expr ctxt ts;
   2.195 +    val mk_generator_expr =
   2.196 +      if Config.get ctxt full_support then mk_full_generator_expr else mk_generator_expr
   2.197 +    val t' = mk_parametric_generator_expr mk_generator_expr ctxt ts;
   2.198      val compile = Code_Runtime.dynamic_value_strict
   2.199        (Counterexample.get, put_counterexample, "Exhaustive_Generators.put_counterexample")
   2.200        thy (SOME target) (fn proc => fn g =>
   2.201 @@ -402,6 +498,7 @@
   2.202    #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
   2.203        (((@{sort type}, @{sort type}), @{sort bounded_forall}), instantiate_bounded_forall_datatype))
   2.204    #> setup_smart_quantifier
   2.205 +  #> setup_full_support
   2.206    #> setup_quickcheck_pretty
   2.207    #> Context.theory_map (Quickcheck.add_generator ("exhaustive", compile_generator_expr))
   2.208    #> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs))