group record-related ML files
authorhaftmann
Thu Aug 12 17:56:41 2010 +0200 (2010-08-12)
changeset 383937c045c03598f
parent 38392 8a3ca8b96b23
child 38394 3142c1e21a0e
group record-related ML files
src/HOL/Main.thy
src/HOL/Nitpick.thy
src/HOL/Plain.thy
src/HOL/Tools/quickcheck_generators.ML
src/HOL/Typedef.thy
     1.1 --- a/src/HOL/Main.thy	Thu Aug 12 13:53:42 2010 +0200
     1.2 +++ b/src/HOL/Main.thy	Thu Aug 12 17:56:41 2010 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  header {* Main HOL *}
     1.5  
     1.6  theory Main
     1.7 -imports Plain Predicate_Compile Nitpick SMT
     1.8 +imports Plain Record Predicate_Compile Nitpick SMT
     1.9  begin
    1.10  
    1.11  text {*
     2.1 --- a/src/HOL/Nitpick.thy	Thu Aug 12 13:53:42 2010 +0200
     2.2 +++ b/src/HOL/Nitpick.thy	Thu Aug 12 17:56:41 2010 +0200
     2.3 @@ -8,7 +8,7 @@
     2.4  header {* Nitpick: Yet Another Counterexample Generator for Isabelle/HOL *}
     2.5  
     2.6  theory Nitpick
     2.7 -imports Map Quotient SAT
     2.8 +imports Map Quotient SAT Record
     2.9  uses ("Tools/Nitpick/kodkod.ML")
    2.10       ("Tools/Nitpick/kodkod_sat.ML")
    2.11       ("Tools/Nitpick/nitpick_util.ML")
     3.1 --- a/src/HOL/Plain.thy	Thu Aug 12 13:53:42 2010 +0200
     3.2 +++ b/src/HOL/Plain.thy	Thu Aug 12 17:56:41 2010 +0200
     3.3 @@ -1,7 +1,7 @@
     3.4  header {* Plain HOL *}
     3.5  
     3.6  theory Plain
     3.7 -imports Datatype Record FunDef Extraction
     3.8 +imports Datatype FunDef Extraction
     3.9  begin
    3.10  
    3.11  text {*
     4.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Thu Aug 12 13:53:42 2010 +0200
     4.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Thu Aug 12 17:56:41 2010 +0200
     4.3 @@ -10,7 +10,6 @@
     4.4    val random_fun: typ -> typ -> ('a -> 'a -> bool) -> ('a -> term)
     4.5      -> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed)
     4.6      -> seed -> (('a -> 'b) * (unit -> term)) * seed
     4.7 -  val ensure_random_typecopy: string -> theory -> theory
     4.8    val random_aux_specification: string -> string -> term list -> local_theory -> local_theory
     4.9    val mk_random_aux_eqs: theory -> Datatype.descr -> (string * sort) list
    4.10      -> string list -> string list * string list -> typ list * typ list
    4.11 @@ -65,53 +64,10 @@
    4.12    in ((random_fun', term_fun'), seed''') end;
    4.13  
    4.14  
    4.15 -(** type copies **)
    4.16 -
    4.17 -fun mk_random_typecopy tyco vs constr T' thy =
    4.18 -  let
    4.19 -    val mk_const = curry (Sign.mk_const thy);
    4.20 -    val Ts = map TFree vs;  
    4.21 -    val T = Type (tyco, Ts);
    4.22 -    val Tm = termifyT T;
    4.23 -    val Tm' = termifyT T';
    4.24 -    val v = "x";
    4.25 -    val t_v = Free (v, Tm');
    4.26 -    val t_constr = Const (constr, T' --> T);
    4.27 -    val lhs = HOLogic.mk_random T size;
    4.28 -    val rhs = HOLogic.mk_ST [((HOLogic.mk_random T' size, @{typ Random.seed}), SOME (v, Tm'))]
    4.29 -      (HOLogic.mk_return Tm @{typ Random.seed}
    4.30 -      (mk_const "Code_Evaluation.valapp" [T', T]
    4.31 -        $ HOLogic.mk_prod (t_constr, Abs ("u", @{typ unit}, HOLogic.reflect_term t_constr)) $ t_v))
    4.32 -      @{typ Random.seed} (SOME Tm, @{typ Random.seed});
    4.33 -    val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
    4.34 -  in   
    4.35 -    thy
    4.36 -    |> Class.instantiation ([tyco], vs, @{sort random})
    4.37 -    |> `(fn lthy => Syntax.check_term lthy eq)
    4.38 -    |-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq)))
    4.39 -    |> snd
    4.40 -    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
    4.41 -  end;
    4.42 -
    4.43 -fun ensure_random_typecopy tyco thy =
    4.44 -  let
    4.45 -    val SOME { vs = raw_vs, constr, typ = raw_T, ... } =
    4.46 -      Typecopy.get_info thy tyco;
    4.47 -    val constrain = curry (Sorts.inter_sort (Sign.classes_of thy));
    4.48 -    val T = map_atyps (fn TFree (v, sort) =>
    4.49 -      TFree (v, constrain sort @{sort random})) raw_T;
    4.50 -    val vs' = Term.add_tfreesT T [];
    4.51 -    val vs = map (fn (v, sort) =>
    4.52 -      (v, the_default (constrain sort @{sort typerep}) (AList.lookup (op =) vs' v))) raw_vs;
    4.53 -    val can_inst = Sign.of_sort thy (T, @{sort random});
    4.54 -  in if can_inst then mk_random_typecopy tyco vs constr T thy else thy end;
    4.55 -
    4.56 -
    4.57  (** datatypes **)
    4.58  
    4.59  (* definitional scheme for random instances on datatypes *)
    4.60  
    4.61 -(*FIXME avoid this low-level proving*)
    4.62  local
    4.63  
    4.64  fun dest_ctyp_nth k cT = nth (Thm.dest_ctyp cT) k;
    4.65 @@ -450,8 +406,8 @@
    4.66  
    4.67  (** setup **)
    4.68  
    4.69 -val setup = Typecopy.interpretation ensure_random_typecopy
    4.70 -  #> Datatype.interpretation ensure_random_datatype
    4.71 +val setup =
    4.72 +  Datatype.interpretation ensure_random_datatype
    4.73    #> Code_Target.extend_target (target, (Code_Eval.target, K I))
    4.74    #> Quickcheck.add_generator ("code", compile_generator_expr o ProofContext.theory_of);
    4.75  
     5.1 --- a/src/HOL/Typedef.thy	Thu Aug 12 13:53:42 2010 +0200
     5.2 +++ b/src/HOL/Typedef.thy	Thu Aug 12 17:56:41 2010 +0200
     5.3 @@ -8,7 +8,6 @@
     5.4  imports Set
     5.5  uses
     5.6    ("Tools/typedef.ML")
     5.7 -  ("Tools/typecopy.ML")
     5.8    ("Tools/typedef_codegen.ML")
     5.9  begin
    5.10  
    5.11 @@ -116,7 +115,6 @@
    5.12  end
    5.13  
    5.14  use "Tools/typedef.ML" setup Typedef.setup
    5.15 -use "Tools/typecopy.ML" setup Typecopy.setup
    5.16  use "Tools/typedef_codegen.ML" setup TypedefCodegen.setup
    5.17  
    5.18  end