equal
deleted
inserted
replaced
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 distinctness_limit : int ConfigOption.T |
10 val distinctness_limit : int Config.T |
11 val distinctness_limit_setup : theory -> theory |
11 val distinctness_limit_setup : theory -> theory |
12 val indexify_names: string list -> string list |
12 val indexify_names: string list -> string list |
13 val make_tnames: typ list -> string list |
13 val make_tnames: typ list -> string list |
14 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 |
15 val make_ind : DatatypeAux.descr list -> (string * sort) list -> term |
15 val make_ind : DatatypeAux.descr list -> (string * sort) list -> term |
39 |
39 |
40 open DatatypeAux; |
40 open DatatypeAux; |
41 |
41 |
42 (*the kind of distinctiveness axioms depends on number of constructors*) |
42 (*the kind of distinctiveness axioms depends on number of constructors*) |
43 val (distinctness_limit, distinctness_limit_setup) = |
43 val (distinctness_limit, distinctness_limit_setup) = |
44 ConfigOption.int "datatype_distinctness_limit" 7; |
44 Attrib.config_int "datatype_distinctness_limit" 7; |
45 |
45 |
46 fun indexify_names names = |
46 fun indexify_names names = |
47 let |
47 let |
48 fun index (x :: xs) tab = |
48 fun index (x :: xs) tab = |
49 (case AList.lookup (op =) tab x of |
49 (case AList.lookup (op =) tab x of |
303 |
303 |
304 in (make_distincts' constrs) @ (make_distincts_1 T constrs) |
304 in (make_distincts' constrs) @ (make_distincts_1 T constrs) |
305 end; |
305 end; |
306 |
306 |
307 in map (fn (((_, (_, _, constrs)), T), tname) => |
307 in map (fn (((_, (_, _, constrs)), T), tname) => |
308 if length constrs < ConfigOption.get_thy thy distinctness_limit |
308 if length constrs < Config.get_thy thy distinctness_limit |
309 then make_distincts_1 T constrs else []) |
309 then make_distincts_1 T constrs else []) |
310 ((hd descr) ~~ newTs ~~ new_type_names) |
310 ((hd descr) ~~ newTs ~~ new_type_names) |
311 end; |
311 end; |
312 |
312 |
313 |
313 |