merged
authorhaftmann
Sat Jun 13 16:32:38 2009 +0200 (2009-06-13)
changeset 31626fe35b72b9ef0
parent 31614 ef6d67b1ad10
parent 31625 9e4d7d60c3e7
child 31627 bc2de3795756
child 31628 28699098b5f3
merged
NEWS
     1.1 --- a/NEWS	Sat Jun 13 16:29:15 2009 +0200
     1.2 +++ b/NEWS	Sat Jun 13 16:32:38 2009 +0200
     1.3 @@ -37,6 +37,9 @@
     1.4  * New method "linarith" invokes existing linear arithmetic decision
     1.5  procedure only.
     1.6  
     1.7 +* Implementation of quickcheck using generic code generator; default generators
     1.8 +are provided for all suitable HOL types, records and datatypes.
     1.9 +
    1.10  
    1.11  *** ML ***
    1.12  
     2.1 --- a/src/HOL/Quickcheck.thy	Sat Jun 13 16:29:15 2009 +0200
     2.2 +++ b/src/HOL/Quickcheck.thy	Sat Jun 13 16:32:38 2009 +0200
     2.3 @@ -93,15 +93,15 @@
     2.4    \<Rightarrow> (Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> (Random.seed \<Rightarrow> Random.seed \<times> Random.seed)
     2.5    \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
     2.6  
     2.7 -definition random_fun_lift :: "(code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
     2.8 -  \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a\<Colon>term_of \<Rightarrow> 'b\<Colon>typerep) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
     2.9 -  "random_fun_lift f i = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of (f i) Random.split_seed"
    2.10 +definition random_fun_lift :: "(Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
    2.11 +  \<Rightarrow> Random.seed \<Rightarrow> (('a\<Colon>term_of \<Rightarrow> 'b\<Colon>typerep) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
    2.12 +  "random_fun_lift f = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of f Random.split_seed"
    2.13  
    2.14  instantiation "fun" :: ("{eq, term_of}", "{type, random}") random
    2.15  begin
    2.16  
    2.17  definition random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
    2.18 -  "random = random_fun_lift random"
    2.19 +  "random i = random_fun_lift (random i)"
    2.20  
    2.21  instance ..
    2.22  
     3.1 --- a/src/HOL/Tools/datatype_package/datatype_codegen.ML	Sat Jun 13 16:29:15 2009 +0200
     3.2 +++ b/src/HOL/Tools/datatype_package/datatype_codegen.ML	Sat Jun 13 16:32:38 2009 +0200
     3.3 @@ -15,13 +15,7 @@
     3.4  structure DatatypeCodegen : DATATYPE_CODEGEN =
     3.5  struct
     3.6  
     3.7 -(** SML code generator **)
     3.8 -
     3.9 -open Codegen;
    3.10 -
    3.11 -(**** datatype definition ****)
    3.12 -
    3.13 -(* find shortest path to constructor with no recursive arguments *)
    3.14 +(** find shortest path to constructor with no recursive arguments **)
    3.15  
    3.16  fun find_nonempty (descr: DatatypeAux.descr) is i =
    3.17    let
    3.18 @@ -41,6 +35,13 @@
    3.19  
    3.20  fun find_shortest_path descr i = find_nonempty descr [i] i;
    3.21  
    3.22 +
    3.23 +(** SML code generator **)
    3.24 +
    3.25 +open Codegen;
    3.26 +
    3.27 +(* datatype definition *)
    3.28 +
    3.29  fun add_dt_defs thy defs dep module (descr: DatatypeAux.descr) sorts gr =
    3.30    let
    3.31      val descr' = List.filter (can (map DatatypeAux.dest_DtTFree o #2 o snd)) descr;
    3.32 @@ -210,7 +211,7 @@
    3.33    end;
    3.34  
    3.35  
    3.36 -(**** case expressions ****)
    3.37 +(* case expressions *)
    3.38  
    3.39  fun pretty_case thy defs dep module brack constrs (c as Const (_, T)) ts gr =
    3.40    let val i = length constrs
    3.41 @@ -252,7 +253,7 @@
    3.42    end;
    3.43  
    3.44  
    3.45 -(**** constructors ****)
    3.46 +(* constructors *)
    3.47  
    3.48  fun pretty_constr thy defs dep module brack args (c as Const (s, T)) ts gr =
    3.49    let val i = length args
    3.50 @@ -271,7 +272,7 @@
    3.51    end;
    3.52  
    3.53  
    3.54 -(**** code generators for terms and types ****)
    3.55 +(* code generators for terms and types *)
    3.56  
    3.57  fun datatype_codegen thy defs dep module brack t gr = (case strip_comb t of
    3.58     (c as Const (s, T), ts) =>
    3.59 @@ -313,6 +314,18 @@
    3.60  
    3.61  (** generic code generator **)
    3.62  
    3.63 +(* liberal addition of code data for datatypes *)
    3.64 +
    3.65 +fun mk_constr_consts thy vs dtco cos =
    3.66 +  let
    3.67 +    val cs = map (fn (c, tys) => (c, tys ---> Type (dtco, map TFree vs))) cos;
    3.68 +    val cs' = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) cs;
    3.69 +  in if is_some (try (Code.constrset_of_consts thy) cs')
    3.70 +    then SOME cs
    3.71 +    else NONE
    3.72 +  end;
    3.73 +
    3.74 +
    3.75  (* case certificates *)
    3.76  
    3.77  fun mk_case_cert thy tyco =
    3.78 @@ -371,7 +384,7 @@
    3.79      val simpset = Simplifier.context (ProofContext.init thy) (HOL_basic_ss
    3.80        addsimps (map Simpdata.mk_eq (@{thm eq} :: @{thm eq_True} :: inject_thms))
    3.81        addsimprocs [DatatypePackage.distinct_simproc]);
    3.82 -    fun prove prop = Goal.prove_global thy [] [] prop (K (ALLGOALS (simp_tac simpset)))
    3.83 +    fun prove prop = SkipProof.prove_global thy [] [] prop (K (ALLGOALS (simp_tac simpset)))
    3.84        |> Simpdata.mk_eq;
    3.85    in map (rpair true o prove) (triv_injects @ injects @ distincts) @ [(prove refl, false)] end;
    3.86  
    3.87 @@ -411,16 +424,7 @@
    3.88    end;
    3.89  
    3.90  
    3.91 -(* liberal addition of code data for datatypes *)
    3.92 -
    3.93 -fun mk_constr_consts thy vs dtco cos =
    3.94 -  let
    3.95 -    val cs = map (fn (c, tys) => (c, tys ---> Type (dtco, map TFree vs))) cos;
    3.96 -    val cs' = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) cs;
    3.97 -  in if is_some (try (Code.constrset_of_consts thy) cs')
    3.98 -    then SOME cs
    3.99 -    else NONE
   3.100 -  end;
   3.101 +(* register a datatype etc. *)
   3.102  
   3.103  fun add_all_code dtcos thy =
   3.104    let
   3.105 @@ -433,6 +437,7 @@
   3.106    in
   3.107      if null css then thy
   3.108      else thy
   3.109 +      |> tap (fn _ => DatatypeAux.message "Registering datatype for code generator ...")
   3.110        |> fold Code.add_datatype css
   3.111        |> fold_rev Code.add_default_eqn case_rewrites
   3.112        |> fold Code.add_case certs
   3.113 @@ -440,7 +445,6 @@
   3.114     end;
   3.115  
   3.116  
   3.117 -
   3.118  (** theory setup **)
   3.119  
   3.120  val setup = 
     4.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Sat Jun 13 16:29:15 2009 +0200
     4.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Sat Jun 13 16:32:38 2009 +0200
     4.3 @@ -170,9 +170,9 @@
     4.4      val eqs1 = map (Pattern.rewrite_term thy rew_ts []) eqs0;
     4.5      val ((_, eqs2), lthy') = PrimrecPackage.add_primrec_simple
     4.6        [((Binding.name random_aux, T), NoSyn)] eqs1 lthy;
     4.7 -    val eq_tac = ALLGOALS Goal.conjunction_tac THEN ALLGOALS (simp_tac rew_ss)
     4.8 +    val eq_tac = ALLGOALS (simp_tac rew_ss)
     4.9        THEN (ALLGOALS (ProofContext.fact_tac (flat eqs2)));
    4.10 -    val eqs3 = Goal.prove_multi lthy' [v] [] eqs0 (K eq_tac);
    4.11 +    val eqs3 = map (fn prop => SkipProof.prove lthy' [v] [] prop (K eq_tac)) eqs0;
    4.12      val cT_random_aux = inst pt_random_aux;
    4.13      val cT_rhs = inst pt_rhs;
    4.14      val rule = @{thm random_aux_rec}
    4.15 @@ -180,7 +180,7 @@
    4.16             [(cT_random_aux, cert t_random_aux), (cT_rhs, cert t_rhs)])
    4.17        |> (fn thm => thm OF eqs3);
    4.18      val tac = ALLGOALS (rtac rule);
    4.19 -    val simp = Goal.prove lthy' [v] [] eq (K tac);
    4.20 +    val simp = SkipProof.prove lthy' [v] [] eq (K tac);
    4.21    in (simp, lthy') end;
    4.22  
    4.23  end;
    4.24 @@ -212,11 +212,11 @@
    4.25          fun prove_eqs aux_simp proj_defs lthy = 
    4.26            let
    4.27              val proj_simps = map (snd o snd) proj_defs;
    4.28 -            fun tac { context = ctxt, ... } = ALLGOALS Goal.conjunction_tac
    4.29 -              THEN ALLGOALS (simp_tac (HOL_ss addsimps proj_simps))
    4.30 +            fun tac { context = ctxt, ... } =
    4.31 +              ALLGOALS (simp_tac (HOL_ss addsimps proj_simps))
    4.32                THEN ALLGOALS (EqSubst.eqsubst_tac ctxt [0] [aux_simp])
    4.33                THEN ALLGOALS (simp_tac (HOL_ss addsimps [fst_conv, snd_conv]));
    4.34 -          in (Goal.prove_multi lthy [v] [] eqs tac, lthy) end;
    4.35 +          in (map (fn prop => SkipProof.prove lthy [v] [] prop tac) eqs, lthy) end;
    4.36        in
    4.37          lthy
    4.38          |> random_aux_primrec aux_eq'
    4.39 @@ -235,10 +235,9 @@
    4.40      val proto_eqs = map mk_proto_eq eqs;
    4.41      fun prove_simps proto_simps lthy =
    4.42        let
    4.43 -        val ext_simps = map (fn thm => fun_cong OF [fun_cong OF  [thm]]) proto_simps;
    4.44 -        val tac = ALLGOALS Goal.conjunction_tac
    4.45 -          THEN ALLGOALS (ProofContext.fact_tac ext_simps);
    4.46 -      in (Goal.prove_multi lthy vs [] eqs (K tac), lthy) end;
    4.47 +        val ext_simps = map (fn thm => fun_cong OF [fun_cong OF [thm]]) proto_simps;
    4.48 +        val tac = ALLGOALS (ProofContext.fact_tac ext_simps);
    4.49 +      in (map (fn prop => SkipProof.prove lthy vs [] prop (K tac)) eqs, lthy) end;
    4.50      val b = Binding.qualify true prefix (Binding.name "simps");
    4.51    in
    4.52      lthy
    4.53 @@ -254,8 +253,6 @@
    4.54  
    4.55  (* constructing random instances on datatypes *)
    4.56  
    4.57 -exception Datatype_Fun; (*FIXME*)
    4.58 -
    4.59  fun mk_random_aux_eqs thy descr vs tycos (names, auxnames) (Ts, Us) =
    4.60    let
    4.61      val mk_const = curry (Sign.mk_const thy);
    4.62 @@ -274,19 +271,20 @@
    4.63      val random_auxT = sizeT o random_resultT;
    4.64      val random_auxs = map2 (fn s => fn rT => Free (s, random_auxT rT))
    4.65        random_auxsN rTs;
    4.66 -
    4.67      fun mk_random_call T = (NONE, (HOLogic.mk_random T j, T));
    4.68      fun mk_random_aux_call fTs (k, _) (tyco, Ts) =
    4.69        let
    4.70 -        val _ = if null fTs then () else raise Datatype_Fun; (*FIXME*)
    4.71 -        val random = nth random_auxs k;
    4.72 +        val T = Type (tyco, Ts);
    4.73 +        fun mk_random_fun_lift [] t = t
    4.74 +          | mk_random_fun_lift (fT :: fTs) t =
    4.75 +              mk_const @{const_name random_fun_lift} [fTs ---> T, fT] $
    4.76 +                mk_random_fun_lift fTs t;
    4.77 +        val t = mk_random_fun_lift fTs (nth random_auxs k $ i1 $ j);
    4.78          val size = Option.map snd (DatatypeCodegen.find_shortest_path descr k)
    4.79            |> the_default 0;
    4.80 -      in (SOME size, (random $ i1 $ j, Type (tyco, Ts))) end;
    4.81 -
    4.82 +      in (SOME size, (t, fTs ---> T)) end;
    4.83      val tss = DatatypeAux.interpret_construction descr vs
    4.84        { atyp = mk_random_call, dtyp = mk_random_aux_call };
    4.85 -
    4.86      fun mk_consexpr simpleT (c, xs) =
    4.87        let
    4.88          val (ks, simple_tTs) = split_list xs;
    4.89 @@ -324,6 +322,7 @@
    4.90  
    4.91  fun mk_random_datatype descr vs tycos (names, auxnames) (Ts, Us) thy =
    4.92    let
    4.93 +    val _ = DatatypeAux.message "Creating quickcheck generators ...";
    4.94      val i = @{term "i\<Colon>code_numeral"};
    4.95      val mk_prop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq;
    4.96      fun mk_size_arg k = case DatatypeCodegen.find_shortest_path descr k
    4.97 @@ -347,35 +346,39 @@
    4.98      |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
    4.99    end;
   4.100  
   4.101 +fun perhaps_constrain thy insts raw_vs =
   4.102 +  let
   4.103 +    fun meet_random (T, sort) = Sorts.meet_sort (Sign.classes_of thy) 
   4.104 +      (Logic.varifyT T, sort);
   4.105 +    val vtab = Vartab.empty
   4.106 +      |> fold (fn (v, sort) => Vartab.update ((v, 0), sort)) raw_vs
   4.107 +      |> fold meet_random insts;
   4.108 +  in SOME (fn (v, _) => (v, (the o Vartab.lookup vtab) (v, 0)))
   4.109 +  end handle CLASS_ERROR => NONE;
   4.110 +
   4.111  fun ensure_random_datatype raw_tycos thy =
   4.112    let
   4.113      val pp = Syntax.pp_global thy;
   4.114      val algebra = Sign.classes_of thy;
   4.115      val (descr, raw_vs, tycos, (names, auxnames), raw_TUs) =
   4.116        DatatypePackage.the_datatype_descr thy raw_tycos;
   4.117 -    val aTs = (flat o maps snd o maps snd) (DatatypeAux.interpret_construction descr raw_vs
   4.118 -      { atyp = single, dtyp = K o K });
   4.119 -    fun meet_random T = Sorts.meet_sort (Sign.classes_of thy) (Logic.varifyT T, @{sort random});
   4.120 -    val vtab = (Vartab.empty
   4.121 -      |> fold (fn (v, sort) => Vartab.update ((v, 0), sort)) raw_vs
   4.122 -      |> fold meet_random aTs
   4.123 -      |> SOME) handle CLASS_ERROR => NONE;
   4.124 -    val vconstrain = case vtab of SOME vtab => (fn (v, _) =>
   4.125 -          (v, (the o Vartab.lookup vtab) (v, 0)))
   4.126 -      | NONE => I;
   4.127 -    val vs = map vconstrain raw_vs;
   4.128 -    val constrain = map_atyps (fn TFree v => TFree (vconstrain v));
   4.129 +    val random_insts = (map (rpair @{sort random}) o flat o maps snd o maps snd)
   4.130 +      (DatatypeAux.interpret_construction descr raw_vs { atyp = single, dtyp = (K o K o K) [] });
   4.131 +    val term_of_insts = (map (rpair @{sort term_of}) o flat o maps snd o maps snd)
   4.132 +      (DatatypeAux.interpret_construction descr raw_vs { atyp = K [], dtyp = K o K });
   4.133      val has_inst = exists (fn tyco =>
   4.134        can (Sorts.mg_domain algebra tyco) @{sort random}) tycos;
   4.135 -  in if is_some vtab andalso not has_inst then
   4.136 -    (mk_random_datatype descr vs tycos (names, auxnames)
   4.137 -      ((pairself o map) constrain raw_TUs) thy
   4.138 -    (*FIXME ephemeral handles*)
   4.139 -    handle Datatype_Fun => thy
   4.140 -         | e as TERM (msg, ts) => (tracing (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts)); raise e)
   4.141 -         | e as TYPE (msg, _, _) =>  (tracing msg; raise e)
   4.142 -         | e as ERROR msg =>  (tracing msg; raise e))
   4.143 -  else thy end;
   4.144 +  in if has_inst then thy
   4.145 +    else case perhaps_constrain thy (random_insts @ term_of_insts) raw_vs
   4.146 +     of SOME constrain => (mk_random_datatype descr
   4.147 +          (map constrain raw_vs) tycos (names, auxnames)
   4.148 +            ((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
   4.149 +            (*FIXME ephemeral handles*)
   4.150 +          handle e as TERM (msg, ts) => (tracing (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts)); raise e)
   4.151 +               | e as TYPE (msg, _, _) => (tracing msg; raise e)
   4.152 +               | e as ERROR msg => (tracing msg; raise e))
   4.153 +      | NONE => thy
   4.154 +  end;
   4.155  
   4.156  
   4.157  (** setup **)