--- a/src/HOL/Tools/Quickcheck/random_generators.ML Fri Mar 11 15:21:13 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Fri Mar 11 15:21:13 2011 +0100
@@ -10,12 +10,6 @@
val random_fun: typ -> typ -> ('a -> 'a -> bool) -> ('a -> term)
-> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed)
-> seed -> (('a -> 'b) * (unit -> term)) * seed
- val perhaps_constrain: theory -> (typ * sort) list -> (string * sort) list
- -> (string * sort -> string * sort) option
- val ensure_sort_datatype:
- sort * (Datatype.config -> Datatype.descr -> (string * sort) list -> string list -> string ->
- string list * string list -> typ list * typ list -> theory -> theory)
- -> Datatype.config -> string list -> theory -> theory
val compile_generator_expr:
Proof.context -> term -> int -> term list option * Quickcheck.report option
val put_counterexample: (unit -> int -> seed -> term list option * seed)
@@ -272,39 +266,6 @@
|> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
end;
-fun perhaps_constrain thy insts raw_vs =
- let
- fun meet (T, sort) = Sorts.meet_sort (Sign.classes_of thy)
- (Logic.varifyT_global T, sort);
- val vtab = Vartab.empty
- |> fold (fn (v, sort) => Vartab.update ((v, 0), sort)) raw_vs
- |> fold meet insts;
- in SOME (fn (v, _) => (v, (the o Vartab.lookup vtab) (v, 0)))
- end handle Sorts.CLASS_ERROR _ => NONE;
-
-fun ensure_sort_datatype (sort, instantiate_datatype) config raw_tycos thy =
- let
- val algebra = Sign.classes_of thy;
- val (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) =
- Datatype.the_descr thy raw_tycos;
- val typerep_vs = (map o apsnd)
- (curry (Sorts.inter_sort algebra) @{sort typerep}) raw_vs;
- val sort_insts = (map (rpair sort) o flat o maps snd o maps snd)
- (Datatype_Aux.interpret_construction descr typerep_vs
- { atyp = single, dtyp = (K o K o K) [] });
- val term_of_insts = (map (rpair @{sort term_of}) o flat o maps snd o maps snd)
- (Datatype_Aux.interpret_construction descr typerep_vs
- { atyp = K [], dtyp = K o K });
- val has_inst = exists (fn tyco =>
- can (Sorts.mg_domain algebra tyco) sort) tycos;
- in if has_inst then thy
- else case perhaps_constrain thy (sort_insts @ term_of_insts) typerep_vs
- of SOME constrain => instantiate_datatype config descr
- (map constrain typerep_vs) tycos prfx (names, auxnames)
- ((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
- | NONE => thy
- end;
-
(** building and compiling generator expressions **)
(* FIXME just one data slot (record) per program unit *)