quickcheck generators for datatypes with functions
authorhaftmann
Sat Jun 13 09:16:25 2009 +0200 (2009-06-13)
changeset 31623b72c11302b39
parent 31622 b30570327b76
child 31624 4b792a97a1fb
quickcheck generators for datatypes with functions
src/HOL/Tools/quickcheck_generators.ML
     1.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Sat Jun 13 09:16:24 2009 +0200
     1.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Sat Jun 13 09:16:25 2009 +0200
     1.3 @@ -254,8 +254,6 @@
     1.4  
     1.5  (* constructing random instances on datatypes *)
     1.6  
     1.7 -exception Datatype_Fun; (*FIXME*)
     1.8 -
     1.9  fun mk_random_aux_eqs thy descr vs tycos (names, auxnames) (Ts, Us) =
    1.10    let
    1.11      val mk_const = curry (Sign.mk_const thy);
    1.12 @@ -274,19 +272,20 @@
    1.13      val random_auxT = sizeT o random_resultT;
    1.14      val random_auxs = map2 (fn s => fn rT => Free (s, random_auxT rT))
    1.15        random_auxsN rTs;
    1.16 -
    1.17      fun mk_random_call T = (NONE, (HOLogic.mk_random T j, T));
    1.18      fun mk_random_aux_call fTs (k, _) (tyco, Ts) =
    1.19        let
    1.20 -        val _ = if null fTs then () else raise Datatype_Fun; (*FIXME*)
    1.21 -        val random = nth random_auxs k;
    1.22 +        val T = Type (tyco, Ts);
    1.23 +        fun mk_random_fun_lift [] t = t
    1.24 +          | mk_random_fun_lift (fT :: fTs) t =
    1.25 +              mk_const @{const_name random_fun_lift} [fTs ---> T, fT] $
    1.26 +                mk_random_fun_lift fTs t;
    1.27 +        val t = mk_random_fun_lift fTs (nth random_auxs k $ i1 $ j);
    1.28          val size = Option.map snd (DatatypeCodegen.find_shortest_path descr k)
    1.29            |> the_default 0;
    1.30 -      in (SOME size, (random $ i1 $ j, Type (tyco, Ts))) end;
    1.31 -
    1.32 +      in (SOME size, (t, fTs ---> T)) end;
    1.33      val tss = DatatypeAux.interpret_construction descr vs
    1.34        { atyp = mk_random_call, dtyp = mk_random_aux_call };
    1.35 -
    1.36      fun mk_consexpr simpleT (c, xs) =
    1.37        let
    1.38          val (ks, simple_tTs) = split_list xs;
    1.39 @@ -347,35 +346,39 @@
    1.40      |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
    1.41    end;
    1.42  
    1.43 +fun perhaps_constrain thy insts raw_vs =
    1.44 +  let
    1.45 +    fun meet_random (T, sort) = Sorts.meet_sort (Sign.classes_of thy) 
    1.46 +      (Logic.varifyT T, sort);
    1.47 +    val vtab = Vartab.empty
    1.48 +      |> fold (fn (v, sort) => Vartab.update ((v, 0), sort)) raw_vs
    1.49 +      |> fold meet_random insts;
    1.50 +  in SOME (fn (v, _) => (v, (the o Vartab.lookup vtab) (v, 0)))
    1.51 +  end handle CLASS_ERROR => NONE;
    1.52 +
    1.53  fun ensure_random_datatype raw_tycos thy =
    1.54    let
    1.55      val pp = Syntax.pp_global thy;
    1.56      val algebra = Sign.classes_of thy;
    1.57      val (descr, raw_vs, tycos, (names, auxnames), raw_TUs) =
    1.58        DatatypePackage.the_datatype_descr thy raw_tycos;
    1.59 -    val aTs = (flat o maps snd o maps snd) (DatatypeAux.interpret_construction descr raw_vs
    1.60 -      { atyp = single, dtyp = K o K });
    1.61 -    fun meet_random T = Sorts.meet_sort (Sign.classes_of thy) (Logic.varifyT T, @{sort random});
    1.62 -    val vtab = (Vartab.empty
    1.63 -      |> fold (fn (v, sort) => Vartab.update ((v, 0), sort)) raw_vs
    1.64 -      |> fold meet_random aTs
    1.65 -      |> SOME) handle CLASS_ERROR => NONE;
    1.66 -    val vconstrain = case vtab of SOME vtab => (fn (v, _) =>
    1.67 -          (v, (the o Vartab.lookup vtab) (v, 0)))
    1.68 -      | NONE => I;
    1.69 -    val vs = map vconstrain raw_vs;
    1.70 -    val constrain = map_atyps (fn TFree v => TFree (vconstrain v));
    1.71 +    val random_insts = (map (rpair @{sort random}) o flat o maps snd o maps snd)
    1.72 +      (DatatypeAux.interpret_construction descr raw_vs { atyp = single, dtyp = (K o K o K) [] });
    1.73 +    val term_of_insts = (map (rpair @{sort term_of}) o flat o maps snd o maps snd)
    1.74 +      (DatatypeAux.interpret_construction descr raw_vs { atyp = K [], dtyp = K o K });
    1.75      val has_inst = exists (fn tyco =>
    1.76        can (Sorts.mg_domain algebra tyco) @{sort random}) tycos;
    1.77 -  in if is_some vtab andalso not has_inst then
    1.78 -    (mk_random_datatype descr vs tycos (names, auxnames)
    1.79 -      ((pairself o map) constrain raw_TUs) thy
    1.80 -    (*FIXME ephemeral handles*)
    1.81 -    handle Datatype_Fun => thy
    1.82 -         | e as TERM (msg, ts) => (tracing (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts)); raise e)
    1.83 -         | e as TYPE (msg, _, _) =>  (tracing msg; raise e)
    1.84 -         | e as ERROR msg =>  (tracing msg; raise e))
    1.85 -  else thy end;
    1.86 +  in if has_inst then thy
    1.87 +    else case perhaps_constrain thy (random_insts @ term_of_insts) raw_vs
    1.88 +     of SOME constrain => (mk_random_datatype descr
    1.89 +          (map constrain raw_vs) tycos (names, auxnames)
    1.90 +            ((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
    1.91 +            (*FIXME ephemeral handles*)
    1.92 +          handle e as TERM (msg, ts) => (tracing (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts)); raise e)
    1.93 +               | e as TYPE (msg, _, _) => (tracing msg; raise e)
    1.94 +               | e as ERROR msg => (tracing msg; raise e))
    1.95 +      | NONE => thy
    1.96 +  end;
    1.97  
    1.98  
    1.99  (** setup **)