1.1 --- a/src/HOL/Main.thy	Thu May 05 10:24:12 2011 +0200
     1.2 +++ b/src/HOL/Main.thy	Thu May 05 10:47:31 2011 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  header {* Main HOL *}
     1.5  
     1.6  theory Main
     1.7 -imports Plain Record Predicate_Compile Quickcheck_Exhaustive Nitpick
     1.8 +imports Plain Predicate_Compile Nitpick
     1.9  begin
    1.10  
    1.11  text {*

     2.1 --- a/src/HOL/Record.thy	Thu May 05 10:24:12 2011 +0200
     2.2 +++ b/src/HOL/Record.thy	Thu May 05 10:47:31 2011 +0200
     2.3 @@ -9,7 +9,7 @@
     2.4  header {* Extensible records with structural subtyping *}
     2.5  
     2.6  theory Record
     2.7 -imports Plain Quickcheck
     2.8 +imports Plain Quickcheck_Exhaustive
     2.9  uses ("Tools/record.ML")
    2.10  begin
    2.11  

     3.1 --- a/src/HOL/Tools/record.ML	Thu May 05 10:24:12 2011 +0200
     3.2 +++ b/src/HOL/Tools/record.ML	Thu May 05 10:47:31 2011 +0200
     3.3 @@ -1795,7 +1795,7 @@
     3.4  
     3.5  (* code generation *)
     3.6  
     3.7 -fun instantiate_random_record tyco vs extN Ts thy =
     3.8 +fun mk_random_eq tyco vs extN Ts =
     3.9    let
    3.10      val size = @{term "i::code_numeral"};
    3.11      fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"});
    3.12 @@ -1810,26 +1810,52 @@
    3.13          (map (fn (v, T') =>
    3.14            ((HOLogic.mk_random T' size, @{typ Random.seed}), SOME (v, termifyT T'))) params)
    3.15          tc @{typ Random.seed} (SOME Tm, @{typ Random.seed});
    3.16 -    val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
    3.17 +  in
    3.18 +    (lhs, rhs)
    3.19 +  end
    3.20 +
    3.21 +fun mk_full_exhaustive_eq tyco vs extN Ts =
    3.22 +  let
    3.23 +    val size = @{term "i::code_numeral"};
    3.24 +    fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"});
    3.25 +    val T = Type (tyco, map TFree vs);
    3.26 +    val test_function = Free ("f", termifyT T --> @{typ "term list option"});
    3.27 +    val params = Name.names Name.context "x" Ts;
    3.28 +    fun full_exhaustiveT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
    3.29 +      --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
    3.30 +    fun mk_full_exhaustive T =
    3.31 +      Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"},
    3.32 +        full_exhaustiveT T)
    3.33 +    val lhs = mk_full_exhaustive T $ test_function $ size;
    3.34 +    val tc = test_function $ (HOLogic.mk_valtermify_app extN params T);
    3.35 +    val rhs = fold_rev (fn (v, T) => fn cont =>
    3.36 +        mk_full_exhaustive T $ (lambda (Free (v, termifyT T)) cont) $ size) params tc
    3.37 +  in
    3.38 +    (lhs, rhs)
    3.39 +  end
    3.40 +
    3.41 +fun instantiate_sort_record (sort, mk_eq) tyco vs extN Ts thy =
    3.42 +  let
    3.43 +    val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_eq tyco vs extN Ts));
    3.44    in
    3.45      thy
    3.46 -    |> Class.instantiation ([tyco], vs, @{sort random})
    3.47 +    |> Class.instantiation ([tyco], vs, sort)
    3.48      |> `(fn lthy => Syntax.check_term lthy eq)
    3.49      |-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq)))
    3.50      |> snd
    3.51      |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
    3.52 -  end;
    3.53 -
    3.54 -fun ensure_random_record ext_tyco vs extN Ts thy =
    3.55 +  end
    3.56 +
    3.57 +fun ensure_sort_record (sort, mk_eq) ext_tyco vs extN Ts thy =
    3.58    let
    3.59      val algebra = Sign.classes_of thy;
    3.60 -    val has_inst = can (Sorts.mg_domain algebra ext_tyco) @{sort random};
    3.61 +    val has_inst = can (Sorts.mg_domain algebra ext_tyco) sort;
    3.62    in
    3.63      if has_inst then thy
    3.64      else
    3.65 -      (case Quickcheck_Common.perhaps_constrain thy (map (rpair @{sort random}) Ts) vs of
    3.66 +      (case Quickcheck_Common.perhaps_constrain thy (map (rpair sort) Ts) vs of
    3.67          SOME constrain =>
    3.68 -          instantiate_random_record ext_tyco (map constrain vs) extN
    3.69 +          instantiate_sort_record (sort, mk_eq) ext_tyco (map constrain vs) extN
    3.70              ((map o map_atyps) (fn TFree v => TFree (constrain v)) Ts) thy
    3.71        | NONE => thy)
    3.72    end;
    3.73 @@ -1851,6 +1877,8 @@
    3.74        |> Thm.instantiate
    3.75          ([pairself (ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], [])
    3.76        |> AxClass.unoverload thy;
    3.77 +    val ensure_random_record = ensure_sort_record (@{sort random}, mk_random_eq)
    3.78 +    val ensure_exhaustive_record = ensure_sort_record (@{sort full_exhaustive}, mk_full_exhaustive_eq)
    3.79    in
    3.80      thy
    3.81      |> Code.add_datatype [ext]
    3.82 @@ -1866,6 +1894,7 @@
    3.83            thy |> Code.del_eqn eq_def |> Code.add_default_eqn (mk_eq thy eq_def))
    3.84      |> (fn thy => Code.add_nbe_default_eqn (mk_eq_refl thy) thy)
    3.85      |> ensure_random_record ext_tyco vs (fst ext) (binder_types (snd ext))
    3.86 +    |> ensure_exhaustive_record ext_tyco vs (fst ext) (binder_types (snd ext))
    3.87    end;
    3.88  
    3.89