src/HOL/Tools/datatype_prop.ML
changeset 24098 f1eb34ae33af
parent 22994 02440636214f
child 24112 6c4e7d17f9b0
equal deleted inserted replaced
24097:86734ba03ca2 24098:f1eb34ae33af
     5 Characteristic properties of datatypes.
     5 Characteristic properties of datatypes.
     6 *)
     6 *)
     7 
     7 
     8 signature DATATYPE_PROP =
     8 signature DATATYPE_PROP =
     9 sig
     9 sig
    10   val dtK : int ref
    10   val distinctness_limit : int ConfigOption.T
       
    11   val distinctness_limit_setup : theory -> theory
    11   val indexify_names: string list -> string list
    12   val indexify_names: string list -> string list
    12   val make_tnames: typ list -> string list
    13   val make_tnames: typ list -> string list
    13   val make_injs : DatatypeAux.descr list -> (string * sort) list -> term list list
    14   val make_injs : DatatypeAux.descr list -> (string * sort) list -> term list list
    14   val make_ind : DatatypeAux.descr list -> (string * sort) list -> term
    15   val make_ind : DatatypeAux.descr list -> (string * sort) list -> term
    15   val make_casedists : DatatypeAux.descr list -> (string * sort) list -> term list
    16   val make_casedists : DatatypeAux.descr list -> (string * sort) list -> term list
    37 struct
    38 struct
    38 
    39 
    39 open DatatypeAux;
    40 open DatatypeAux;
    40 
    41 
    41 (*the kind of distinctiveness axioms depends on number of constructors*)
    42 (*the kind of distinctiveness axioms depends on number of constructors*)
    42 val dtK = ref 7;
    43 val (distinctness_limit, distinctness_limit_setup) =
       
    44   ConfigOption.int "datatype_distinctness_limit" 7;
    43 
    45 
    44 fun indexify_names names =
    46 fun indexify_names names =
    45   let
    47   let
    46     fun index (x :: xs) tab =
    48     fun index (x :: xs) tab =
    47       (case AList.lookup (op =) tab x of
    49       (case AList.lookup (op =) tab x of
   275   let
   277   let
   276     val descr' = List.concat descr;
   278     val descr' = List.concat descr;
   277     val recTs = get_rec_types descr' sorts;
   279     val recTs = get_rec_types descr' sorts;
   278     val newTs = Library.take (length (hd descr), recTs);
   280     val newTs = Library.take (length (hd descr), recTs);
   279 
   281 
   280     (**** number of constructors < dtK : C_i ... ~= C_j ... ****)
   282     (**** number of constructors < distinctness_limit : C_i ... ~= C_j ... ****)
   281 
   283 
   282     fun make_distincts_1 _ [] = []
   284     fun make_distincts_1 _ [] = []
   283       | make_distincts_1 T ((cname, cargs)::constrs) =
   285       | make_distincts_1 T ((cname, cargs)::constrs) =
   284           let
   286           let
   285             val Ts = map (typ_of_dtyp descr' sorts) cargs;
   287             val Ts = map (typ_of_dtyp descr' sorts) cargs;
   301 
   303 
   302           in (make_distincts' constrs) @ (make_distincts_1 T constrs)
   304           in (make_distincts' constrs) @ (make_distincts_1 T constrs)
   303           end;
   305           end;
   304 
   306 
   305   in map (fn (((_, (_, _, constrs)), T), tname) =>
   307   in map (fn (((_, (_, _, constrs)), T), tname) =>
   306       if length constrs < !dtK then make_distincts_1 T constrs else [])
   308       if length constrs < ConfigOption.get_thy thy distinctness_limit
       
   309       then make_distincts_1 T constrs else [])
   307         ((hd descr) ~~ newTs ~~ new_type_names)
   310         ((hd descr) ~~ newTs ~~ new_type_names)
   308   end;
   311   end;
   309 
   312 
   310 
   313 
   311 (*************************** the "split" - equations **************************)
   314 (*************************** the "split" - equations **************************)