canonical prefix for datatype derivates
authorhaftmann
Mon Jun 29 16:17:56 2009 +0200 (2009-06-29)
changeset 31868edd1f30c0477
parent 31867 4d278bbb5cc8
child 31869 01fed718958c
canonical prefix for datatype derivates
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/quickcheck_generators.ML
     1.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Mon Jun 29 16:17:55 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Mon Jun 29 16:17:56 2009 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4    val the_info : theory -> string -> info
     1.5    val the_descr : theory -> string list
     1.6      -> descr * (string * sort) list * string list
     1.7 -      * (string list * string list) * (typ list * typ list)
     1.8 +      * string * (string list * string list) * (typ list * typ list)
     1.9    val the_spec : theory -> string -> (string * sort) list * (string * typ list) list
    1.10    val get_constrs : theory -> string -> (string * typ) list option
    1.11    val get_all : theory -> info Symtab.table
    1.12 @@ -125,9 +125,10 @@
    1.13  
    1.14      val names = map Long_Name.base_name (the_default tycos (#alt_names info));
    1.15      val (auxnames, _) = Name.make_context names
    1.16 -      |> fold_map (yield_singleton Name.variants o name_of_typ) Us
    1.17 +      |> fold_map (yield_singleton Name.variants o name_of_typ) Us;
    1.18 +    val prefix = space_implode "_" names;
    1.19  
    1.20 -  in (descr, vs, tycos, (names, auxnames), (Ts, Us)) end;
    1.21 +  in (descr, vs, tycos, prefix, (names, auxnames), (Ts, Us)) end;
    1.22  
    1.23  fun get_constrs thy dtco =
    1.24    case try (the_spec thy) dtco
     2.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Mon Jun 29 16:17:55 2009 +0200
     2.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Mon Jun 29 16:17:56 2009 +0200
     2.3 @@ -11,10 +11,10 @@
     2.4      -> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed)
     2.5      -> seed -> (('a -> 'b) * (unit -> Term.term)) * seed
     2.6    val ensure_random_typecopy: string -> theory -> theory
     2.7 -  val random_aux_specification: string -> term list -> local_theory -> local_theory
     2.8 +  val random_aux_specification: string -> string -> term list -> local_theory -> local_theory
     2.9    val mk_random_aux_eqs: theory -> Datatype.descr -> (string * sort) list
    2.10      -> string list -> string list * string list -> typ list * typ list
    2.11 -    -> string * (term list * (term * term) list)
    2.12 +    -> term list * (term * term) list
    2.13    val ensure_random_datatype: Datatype.config -> string list -> theory -> theory
    2.14    val eval_ref: (unit -> int -> seed -> term list option * seed) option ref
    2.15    val setup: theory -> theory
    2.16 @@ -184,18 +184,18 @@
    2.17  
    2.18  end;
    2.19  
    2.20 -fun random_aux_primrec_multi prefix [eq] lthy =
    2.21 +fun random_aux_primrec_multi auxname [eq] lthy =
    2.22        lthy
    2.23        |> random_aux_primrec eq
    2.24        |>> (fn simp => [simp])
    2.25 -  | random_aux_primrec_multi prefix (eqs as _ :: _ :: _) lthy =
    2.26 +  | random_aux_primrec_multi auxname (eqs as _ :: _ :: _) lthy =
    2.27        let
    2.28          val thy = ProofContext.theory_of lthy;
    2.29          val (lhss, rhss) = map_split (HOLogic.dest_eq o HOLogic.dest_Trueprop) eqs;
    2.30          val (vs, (arg as Free (v, _)) :: _) = map_split (fn (t1 $ t2) => (t1, t2)) lhss;
    2.31          val Ts = map fastype_of lhss;
    2.32          val tupleT = foldr1 HOLogic.mk_prodT Ts;
    2.33 -        val aux_lhs = Free ("mutual_" ^ prefix, fastype_of arg --> tupleT) $ arg;
    2.34 +        val aux_lhs = Free ("mutual_" ^ auxname, fastype_of arg --> tupleT) $ arg;
    2.35          val aux_eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
    2.36            (aux_lhs, foldr1 HOLogic.mk_prod rhss);
    2.37          fun mk_proj t [T] = [t]
    2.38 @@ -223,7 +223,7 @@
    2.39          |-> (fn (aux_simp, proj_defs) => prove_eqs aux_simp proj_defs)
    2.40        end;
    2.41  
    2.42 -fun random_aux_specification prefix eqs lthy =
    2.43 +fun random_aux_specification prfx name eqs lthy =
    2.44    let
    2.45      val vs = fold Term.add_free_names ((snd o strip_comb o fst o HOLogic.dest_eq
    2.46        o HOLogic.dest_Trueprop o hd) eqs) [];
    2.47 @@ -237,10 +237,10 @@
    2.48          val ext_simps = map (fn thm => fun_cong OF [fun_cong OF [thm]]) proto_simps;
    2.49          val tac = ALLGOALS (ProofContext.fact_tac ext_simps);
    2.50        in (map (fn prop => SkipProof.prove lthy vs [] prop (K tac)) eqs, lthy) end;
    2.51 -    val b = Binding.qualify true prefix (Binding.name "simps");
    2.52 +    val b = Binding.qualify true prfx (Binding.qualify true name (Binding.name "simps"));
    2.53    in
    2.54      lthy
    2.55 -    |> random_aux_primrec_multi prefix proto_eqs
    2.56 +    |> random_aux_primrec_multi (name ^ prfx) proto_eqs
    2.57      |-> (fn proto_simps => prove_simps proto_simps)
    2.58      |-> (fn simps => LocalTheory.note Thm.generatedK ((b,
    2.59             Code.add_default_eqn_attrib :: map (Attrib.internal o K)
    2.60 @@ -252,6 +252,8 @@
    2.61  
    2.62  (* constructing random instances on datatypes *)
    2.63  
    2.64 +val random_auxN = "random_aux";
    2.65 +
    2.66  fun mk_random_aux_eqs thy descr vs tycos (names, auxnames) (Ts, Us) =
    2.67    let
    2.68      val mk_const = curry (Sign.mk_const thy);
    2.69 @@ -259,7 +261,6 @@
    2.70      val i1 = @{term "(i\<Colon>code_numeral) - 1"};
    2.71      val j = @{term "j\<Colon>code_numeral"};
    2.72      val seed = @{term "s\<Colon>Random.seed"};
    2.73 -    val random_auxN = "random_aux";
    2.74      val random_auxsN = map (prefix (random_auxN ^ "_")) (names @ auxnames);
    2.75      fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit \<Rightarrow> term"});
    2.76      val rTs = Ts @ Us;
    2.77 @@ -316,10 +317,9 @@
    2.78            $ seed;
    2.79      val auxs_lhss = map (fn t => t $ i $ j $ seed) random_auxs;
    2.80      val auxs_rhss = map mk_select gen_exprss;
    2.81 -    val prefix = space_implode "_" (random_auxN :: names);
    2.82 -  in (prefix, (random_auxs, auxs_lhss ~~ auxs_rhss)) end;
    2.83 +  in (random_auxs, auxs_lhss ~~ auxs_rhss) end;
    2.84  
    2.85 -fun mk_random_datatype config descr vs tycos (names, auxnames) (Ts, Us) thy =
    2.86 +fun mk_random_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
    2.87    let
    2.88      val _ = DatatypeAux.message config "Creating quickcheck generators ...";
    2.89      val i = @{term "i\<Colon>code_numeral"};
    2.90 @@ -329,14 +329,14 @@
    2.91            else @{term "max :: code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"}
    2.92              $ HOLogic.mk_number @{typ code_numeral} l $ i
    2.93        | NONE => i;
    2.94 -    val (prefix, (random_auxs, auxs_eqs)) = (apsnd o apsnd o map) mk_prop_eq
    2.95 +    val (random_auxs, auxs_eqs) = (apsnd o map) mk_prop_eq
    2.96        (mk_random_aux_eqs thy descr vs tycos (names, auxnames) (Ts, Us));
    2.97      val random_defs = map_index (fn (k, T) => mk_prop_eq
    2.98        (HOLogic.mk_random T i, nth random_auxs k $ mk_size_arg k $ i)) Ts;
    2.99    in
   2.100      thy
   2.101      |> TheoryTarget.instantiation (tycos, vs, @{sort random})
   2.102 -    |> random_aux_specification prefix auxs_eqs
   2.103 +    |> random_aux_specification prfx random_auxN auxs_eqs
   2.104      |> `(fn lthy => map (Syntax.check_term lthy) random_defs)
   2.105      |-> (fn random_defs' => fold_map (fn random_def =>
   2.106            Specification.definition (NONE, (Attrib.empty_binding,
   2.107 @@ -359,7 +359,7 @@
   2.108    let
   2.109      val pp = Syntax.pp_global thy;
   2.110      val algebra = Sign.classes_of thy;
   2.111 -    val (descr, raw_vs, tycos, (names, auxnames), raw_TUs) =
   2.112 +    val (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) =
   2.113        Datatype.the_descr thy raw_tycos;
   2.114      val typrep_vs = (map o apsnd)
   2.115        (curry (Sorts.inter_sort algebra) @{sort typerep}) raw_vs;
   2.116 @@ -374,7 +374,7 @@
   2.117    in if has_inst then thy
   2.118      else case perhaps_constrain thy (random_insts @ term_of_insts) typrep_vs
   2.119       of SOME constrain => mk_random_datatype config descr
   2.120 -          (map constrain typrep_vs) tycos (names, auxnames)
   2.121 +          (map constrain typrep_vs) tycos prfx (names, auxnames)
   2.122              ((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
   2.123        | NONE => thy
   2.124    end;