generalizing instantiate_datatype in quickcheck_exhaustive to remove clones for different compilations
authorbulwahn
Fri Apr 08 16:31:14 2011 +0200 (2011-04-08)
changeset 4231595dfa082065a
parent 42314 8dfb7878a351
child 42316 12635bb655fd
generalizing instantiate_datatype in quickcheck_exhaustive to remove clones for different compilations
src/HOL/Tools/Quickcheck/exhaustive_generators.ML
     1.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Apr 08 16:31:14 2011 +0200
     1.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Apr 08 16:31:14 2011 +0200
     1.3 @@ -246,78 +246,45 @@
     1.4       @{thm nat_mono_iff}, less_int_pred] @ @{thms sum.cases}) 1))
     1.5  
     1.6  (** instantiating generator classes **)
     1.7 -
     1.8 -fun instantiate_exhaustive_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
     1.9 -  let
    1.10 -    val _ = Datatype_Aux.message config "Creating exhaustive generators...";
    1.11 -    val exhaustivesN = map (prefix (exhaustiveN ^ "_")) (names @ auxnames)
    1.12 -  in
    1.13 -    thy
    1.14 -    |> Class.instantiation (tycos, vs, @{sort exhaustive})
    1.15 -    |> Quickcheck_Common.define_functions
    1.16 -        (fn functerms => mk_equations functerms (descr, vs, Ts @ Us), SOME termination_tac)
    1.17 -        prfx ["f", "i"] exhaustivesN (map exhaustiveT (Ts @ Us))
    1.18 -    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
    1.19 -  end handle FUNCTION_TYPE =>
    1.20 -    (Datatype_Aux.message config
    1.21 -      "Creation of exhaustive generators failed because the datatype contains a function type";
    1.22 -    thy)
    1.23 -
    1.24 -
    1.25 -fun instantiate_full_exhaustive_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
    1.26 -  let
    1.27 -    val _ = Datatype_Aux.message config "Creating exhaustive generators...";
    1.28 -    val full_exhaustivesN = map (prefix (full_exhaustiveN ^ "_")) (names @ auxnames)
    1.29 -  in
    1.30 -    thy
    1.31 -    |> Class.instantiation (tycos, vs, @{sort full_exhaustive})
    1.32 -    |> Quickcheck_Common.define_functions
    1.33 -        (fn functerms => mk_full_equations functerms (descr, vs, Ts @ Us), SOME termination_tac)
    1.34 -        prfx ["f", "i"] full_exhaustivesN (map full_exhaustiveT (Ts @ Us))
    1.35 -    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
    1.36 -  end handle FUNCTION_TYPE =>
    1.37 -    (Datatype_Aux.message config
    1.38 -      "Creation of exhaustive generators failed because the datatype contains a function type";
    1.39 -    thy)
    1.40 -     
    1.41 -fun instantiate_fast_exhaustive_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
    1.42 -  let
    1.43 -    val _ = Datatype_Aux.message config "Creating fast exhaustive generators...";
    1.44 -    val fast_exhaustivesN = map (prefix (fast_exhaustiveN ^ "_")) (names @ auxnames)
    1.45 -  in
    1.46 -    thy
    1.47 -    |> Class.instantiation (tycos, vs, @{sort fast_exhaustive})
    1.48 -    |> Quickcheck_Common.define_functions
    1.49 -        (fn functerms => mk_fast_equations functerms (descr, vs, Ts @ Us), SOME termination_tac)
    1.50 -        prfx ["f", "i"] fast_exhaustivesN (map fast_exhaustiveT (Ts @ Us))
    1.51 -    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
    1.52 -  end handle FUNCTION_TYPE =>
    1.53 -    (Datatype_Aux.message config
    1.54 -      "Creation of exhaustive generators failed because the datatype contains a function type";
    1.55 -    thy)
    1.56 -
    1.57 +  
    1.58  val contains_recursive_type_under_function_types =
    1.59    exists (fn (_, (_, _, cs)) => cs |> exists (snd #> exists (fn dT =>
    1.60      (case Datatype_Aux.strip_dtyp dT of (_ :: _, Datatype.DtRec _) => true | _ => false))))
    1.61      
    1.62 -fun instantiate_bounded_forall_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
    1.63 +fun instantiate_datatype (name, constprfx, sort, mk_equations, mk_T, argnames)
    1.64 +    config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
    1.65    if not (contains_recursive_type_under_function_types descr) then
    1.66      let
    1.67 -      val _ = Datatype_Aux.message config "Creating bounded universal quantifiers..."
    1.68 -      val bounded_forallsN = map (prefix (bounded_forallN ^ "_")) (names @ auxnames)
    1.69 +      val _ = Datatype_Aux.message config ("Creating " ^ name ^ "...")
    1.70 +      val fullnames = map (prefix (constprfx ^ "_")) (names @ auxnames)
    1.71      in
    1.72        thy
    1.73 -      |> Class.instantiation (tycos, vs, @{sort bounded_forall})
    1.74 +      |> Class.instantiation (tycos, vs, sort)
    1.75        |> Quickcheck_Common.define_functions
    1.76 -          (fn functerms => mk_bounded_forall_equations functerms (descr, vs, Ts @ Us), NONE)
    1.77 -          prfx ["P", "i"] bounded_forallsN (map bounded_forallT (Ts @ Us))
    1.78 +          (fn functerms => mk_equations functerms (descr, vs, Ts @ Us), NONE)
    1.79 +          prfx argnames fullnames (map mk_T (Ts @ Us))
    1.80        |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
    1.81      end
    1.82    else
    1.83      (Datatype_Aux.message config
    1.84 -      "Creation of bounded universal quantifiers failed because the datatype is recursive under a function type";
    1.85 +      ("Creation of " ^ name ^ " failed because the datatype is recursive under a function type");
    1.86      thy)
    1.87 -    
    1.88 +
    1.89 +val instantiate_bounded_forall_datatype = instantiate_datatype
    1.90 + ("bounded universal quantifiers", bounded_forallN, @{sort bounded_forall},
    1.91 +   mk_bounded_forall_equations, bounded_forallT, ["P", "i"]);
    1.92 +
    1.93 +val instantiate_fast_exhaustive_datatype = instantiate_datatype 
    1.94 + ("fast exhaustive generators", fast_exhaustiveN, @{sort fast_exhaustive},
    1.95 +   mk_fast_equations, fast_exhaustiveT, ["f", "i"])
    1.96 +
    1.97 +val instantiate_exhaustive_datatype = instantiate_datatype  
    1.98 +  ("exhaustive generators", exhaustiveN, @{sort full_exhaustive}, mk_equations, exhaustiveT, ["f", "i"])
    1.99 +
   1.100 +val instantiate_full_exhaustive_datatype = instantiate_datatype
   1.101 +  ("full exhaustive generators", full_exhaustiveN, @{sort full_exhaustive},
   1.102 +  mk_full_equations, full_exhaustiveT, ["f", "i"])
   1.103 +  
   1.104  (* building and compiling generator expressions *)
   1.105  
   1.106  fun mk_fast_generator_expr ctxt (t, eval_terms) =