removed separate quickcheck_record module
authorhaftmann
Wed Aug 18 16:59:35 2010 +0200 (2010-08-18)
changeset 385393be65f879bcd
parent 38538 c87b69396a37
child 38540 8c08631cb4b6
removed separate quickcheck_record module
src/HOL/IsaMakefile
src/HOL/Record.thy
src/HOL/Tools/quickcheck_record.ML
     1.1 --- a/src/HOL/IsaMakefile	Wed Aug 18 15:01:57 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Wed Aug 18 16:59:35 2010 +0200
     1.3 @@ -302,7 +302,6 @@
     1.4    Tools/Predicate_Compile/predicate_compile_specialisation.ML \
     1.5    Tools/Predicate_Compile/predicate_compile_pred.ML \
     1.6    Tools/quickcheck_generators.ML \
     1.7 -  Tools/quickcheck_record.ML \
     1.8    Tools/Qelim/cooper.ML \
     1.9    Tools/Qelim/cooper_procedure.ML \
    1.10    Tools/Qelim/qelim.ML \
     2.1 --- a/src/HOL/Record.thy	Wed Aug 18 15:01:57 2010 +0200
     2.2 +++ b/src/HOL/Record.thy	Wed Aug 18 16:59:35 2010 +0200
     2.3 @@ -10,7 +10,7 @@
     2.4  
     2.5  theory Record
     2.6  imports Plain Quickcheck
     2.7 -uses ("Tools/quickcheck_record.ML") ("Tools/record.ML")
     2.8 +uses ("Tools/record.ML")
     2.9  begin
    2.10  
    2.11  subsection {* Introduction *}
    2.12 @@ -452,7 +452,6 @@
    2.13  
    2.14  subsection {* Record package *}
    2.15  
    2.16 -use "Tools/quickcheck_record.ML"
    2.17  use "Tools/record.ML" setup Record.setup
    2.18  
    2.19  hide_const (open) Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd
     3.1 --- a/src/HOL/Tools/quickcheck_record.ML	Wed Aug 18 15:01:57 2010 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,56 +0,0 @@
     3.4 -(*  Title:      HOL/Tools/quickcheck_record.ML
     3.5 -    Author:     Florian Haftmann, TU Muenchen
     3.6 -
     3.7 -Quickcheck generators for records.
     3.8 -*)
     3.9 -
    3.10 -signature QUICKCHECK_RECORD =
    3.11 -sig
    3.12 -  val ensure_random_typecopy: string -> (string * sort) list -> string
    3.13 -    -> typ -> theory -> theory
    3.14 -end;
    3.15 -
    3.16 -structure Quickcheck_Record : QUICKCHECK_RECORD =
    3.17 -struct
    3.18 -
    3.19 -fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"})
    3.20 -val size = @{term "i::code_numeral"};
    3.21 -
    3.22 -fun mk_random_typecopy tyco vs constr T' thy =
    3.23 -  let
    3.24 -    val mk_const = curry (Sign.mk_const thy);
    3.25 -    val Ts = map TFree vs;  
    3.26 -    val T = Type (tyco, Ts);
    3.27 -    val Tm = termifyT T;
    3.28 -    val Tm' = termifyT T';
    3.29 -    val v = "x";
    3.30 -    val t_v = Free (v, Tm');
    3.31 -    val t_constr = Const (constr, T' --> T);
    3.32 -    val lhs = HOLogic.mk_random T size;
    3.33 -    val rhs = HOLogic.mk_ST [((HOLogic.mk_random T' size, @{typ Random.seed}), SOME (v, Tm'))]
    3.34 -      (HOLogic.mk_return Tm @{typ Random.seed}
    3.35 -      (mk_const "Code_Evaluation.valapp" [T', T]
    3.36 -        $ HOLogic.mk_prod (t_constr, Abs ("u", @{typ unit}, HOLogic.reflect_term t_constr)) $ t_v))
    3.37 -      @{typ Random.seed} (SOME Tm, @{typ Random.seed});
    3.38 -    val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
    3.39 -  in   
    3.40 -    thy
    3.41 -    |> Class.instantiation ([tyco], vs, @{sort random})
    3.42 -    |> `(fn lthy => Syntax.check_term lthy eq)
    3.43 -    |-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq)))
    3.44 -    |> snd
    3.45 -    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
    3.46 -  end;
    3.47 -
    3.48 -fun ensure_random_typecopy tyco raw_vs constr raw_T thy =
    3.49 -  let
    3.50 -    val constrain = curry (Sorts.inter_sort (Sign.classes_of thy));
    3.51 -    val T = map_atyps (fn TFree (v, sort) =>
    3.52 -      TFree (v, constrain sort @{sort random})) raw_T;
    3.53 -    val vs' = Term.add_tfreesT T [];
    3.54 -    val vs = map (fn (v, sort) =>
    3.55 -      (v, the_default (constrain sort @{sort typerep}) (AList.lookup (op =) vs' v))) raw_vs;
    3.56 -    val can_inst = Sign.of_sort thy (T, @{sort random});
    3.57 -  in if can_inst then mk_random_typecopy tyco vs constr T thy else thy end;
    3.58 -
    3.59 -end;