replaced dtK ref by datatype_distinctness_limit configuration option;
authorwenzelm
Tue Jul 31 21:19:20 2007 +0200 (2007-07-31)
changeset 24098f1eb34ae33af
parent 24097 86734ba03ca2
child 24099 6534fd4c5d46
replaced dtK ref by datatype_distinctness_limit configuration option;
src/HOL/Nominal/nominal_package.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/datatype_prop.ML
src/HOL/Tools/datatype_rep_proofs.ML
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Tue Jul 31 21:19:18 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Tue Jul 31 21:19:20 2007 +0200
     1.3 @@ -880,8 +880,10 @@
     1.4  
     1.5      (* prove distinctness theorems *)
     1.6  
     1.7 -    val distinct_props = setmp DatatypeProp.dtK 1000
     1.8 -      (DatatypeProp.make_distincts new_type_names descr' sorts') thy8;
     1.9 +    val distinctness_limit = ConfigOption.get_thy thy8 DatatypeProp.distinctness_limit;
    1.10 +    val thy8' = ConfigOption.put_thy DatatypeProp.distinctness_limit 1000 thy8;
    1.11 +    val distinct_props = DatatypeProp.make_distincts new_type_names descr' sorts' thy8';
    1.12 +    val thy8 = ConfigOption.put_thy DatatypeProp.distinctness_limit distinctness_limit thy8';
    1.13  
    1.14      val dist_rewrites = map (fn (rep_thms, dist_lemma) =>
    1.15        dist_lemma::(rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0]))
     2.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Jul 31 21:19:18 2007 +0200
     2.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Jul 31 21:19:20 2007 +0200
     2.3 @@ -930,7 +930,10 @@
     2.4  (* setup theory *)
     2.5  
     2.6  val setup =
     2.7 -  Method.add_methods tactic_emulations #> simproc_setup #> trfun_setup;
     2.8 +  DatatypeProp.distinctness_limit_setup #>
     2.9 +  Method.add_methods tactic_emulations #>
    2.10 +  simproc_setup #>
    2.11 +  trfun_setup;
    2.12  
    2.13  
    2.14  (* outer syntax *)
     3.1 --- a/src/HOL/Tools/datatype_prop.ML	Tue Jul 31 21:19:18 2007 +0200
     3.2 +++ b/src/HOL/Tools/datatype_prop.ML	Tue Jul 31 21:19:20 2007 +0200
     3.3 @@ -7,7 +7,8 @@
     3.4  
     3.5  signature DATATYPE_PROP =
     3.6  sig
     3.7 -  val dtK : int ref
     3.8 +  val distinctness_limit : int ConfigOption.T
     3.9 +  val distinctness_limit_setup : theory -> theory
    3.10    val indexify_names: string list -> string list
    3.11    val make_tnames: typ list -> string list
    3.12    val make_injs : DatatypeAux.descr list -> (string * sort) list -> term list list
    3.13 @@ -39,7 +40,8 @@
    3.14  open DatatypeAux;
    3.15  
    3.16  (*the kind of distinctiveness axioms depends on number of constructors*)
    3.17 -val dtK = ref 7;
    3.18 +val (distinctness_limit, distinctness_limit_setup) =
    3.19 +  ConfigOption.int "datatype_distinctness_limit" 7;
    3.20  
    3.21  fun indexify_names names =
    3.22    let
    3.23 @@ -277,7 +279,7 @@
    3.24      val recTs = get_rec_types descr' sorts;
    3.25      val newTs = Library.take (length (hd descr), recTs);
    3.26  
    3.27 -    (**** number of constructors < dtK : C_i ... ~= C_j ... ****)
    3.28 +    (**** number of constructors < distinctness_limit : C_i ... ~= C_j ... ****)
    3.29  
    3.30      fun make_distincts_1 _ [] = []
    3.31        | make_distincts_1 T ((cname, cargs)::constrs) =
    3.32 @@ -303,7 +305,8 @@
    3.33            end;
    3.34  
    3.35    in map (fn (((_, (_, _, constrs)), T), tname) =>
    3.36 -      if length constrs < !dtK then make_distincts_1 T constrs else [])
    3.37 +      if length constrs < ConfigOption.get_thy thy distinctness_limit
    3.38 +      then make_distincts_1 T constrs else [])
    3.39          ((hd descr) ~~ newTs ~~ new_type_names)
    3.40    end;
    3.41  
     4.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Tue Jul 31 21:19:18 2007 +0200
     4.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Tue Jul 31 21:19:20 2007 +0200
     4.3 @@ -526,7 +526,8 @@
     4.4        DatatypeProp.make_distincts new_type_names descr sorts thy5);
     4.5  
     4.6      val simproc_dists = map (fn ((((_, (_, _, constrs)), rep_thms), congr), dists) =>
     4.7 -      if length constrs < !DatatypeProp.dtK then FewConstrs dists
     4.8 +      if length constrs < ConfigOption.get_thy thy5 DatatypeProp.distinctness_limit
     4.9 +      then FewConstrs dists
    4.10        else ManyConstrs (congr, HOL_basic_ss addsimps rep_thms)) (hd descr ~~
    4.11          constr_rep_thms ~~ rep_congs ~~ distinct_thms);
    4.12