equal
deleted
inserted
replaced
8 ML {* |
8 ML {* |
9 (* returns the type of the nth datatype *) |
9 (* returns the type of the nth datatype *) |
10 fun nth_dtyp dt_descr sorts i = |
10 fun nth_dtyp dt_descr sorts i = |
11 Datatype_Aux.typ_of_dtyp dt_descr sorts (Datatype_Aux.DtRec i); |
11 Datatype_Aux.typ_of_dtyp dt_descr sorts (Datatype_Aux.DtRec i); |
12 *} |
12 *} |
|
13 |
|
14 ML {* |
|
15 (* generates for every datatype a name str ^ dt_name *) |
|
16 fun prefix_dt_names dt_descr sorts str = |
|
17 let |
|
18 fun get_nth_name (i, _) = |
|
19 Datatype_Aux.name_of_typ (nth_dtyp dt_descr sorts i) |
|
20 in |
|
21 Datatype_Prop.indexify_names |
|
22 (map (prefix str o get_nth_name) dt_descr) |
|
23 end |
|
24 *} |
|
25 |
13 |
26 |
14 ML {* |
27 ML {* |
15 (* permutation function for one argument |
28 (* permutation function for one argument |
16 |
29 |
17 - in case the argument is recursive it returns |
30 - in case the argument is recursive it returns |
106 let |
119 let |
107 val {descr as dt_descr, induct, sorts, ...} = dt_info; |
120 val {descr as dt_descr, induct, sorts, ...} = dt_info; |
108 val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr; |
121 val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr; |
109 val full_tnames = List.take (all_full_tnames, dt_nos); |
122 val full_tnames = List.take (all_full_tnames, dt_nos); |
110 |
123 |
111 val perm_fn_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
124 val perm_fn_names = prefix_dt_names dt_descr sorts "permute_" |
112 "permute_" ^ Datatype_Aux.name_of_typ (nth_dtyp dt_descr sorts i)) dt_descr); |
|
113 |
125 |
114 val perm_types = map (fn (i, _) => perm_ty (nth_dtyp dt_descr sorts i)) dt_descr |
126 val perm_types = map (fn (i, _) => perm_ty (nth_dtyp dt_descr sorts i)) dt_descr |
115 |
127 |
116 val permute_fns = perm_fn_names ~~ perm_types |
128 val permute_fns = perm_fn_names ~~ perm_types |
117 |
129 |