5 (* definitions of the permute function for raw nominal datatypes *) |
5 (* definitions of the permute function for raw nominal datatypes *) |
6 |
6 |
7 |
7 |
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 descr sorts n = |
11 Datatype_Aux.typ_of_dtyp dt_descr sorts (Datatype_Aux.DtRec i); |
11 Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n); |
|
12 |
|
13 (* returns the constructors of the nth datatype *) |
|
14 fun nth_dtyp_constrs descr n = |
|
15 let |
|
16 val (_, (_, _, constrs)) = nth descr n |
|
17 in |
|
18 constrs |
|
19 end |
|
20 |
|
21 (* returns the types of the constructors of the nth datatype *) |
|
22 fun nth_dtyp_constr_typs descr sorts n = |
|
23 map (map (Datatype_Aux.typ_of_dtyp descr sorts) o snd) (nth_dtyp_constrs descr n) |
12 *} |
24 *} |
13 |
25 |
14 ML {* |
26 ML {* |
15 (* generates for every datatype a name str ^ dt_name |
27 (* generates for every datatype a name str ^ dt_name |
16 plus and index for multiple occurences of a string *) |
28 plus and index for multiple occurences of a string *) |
17 fun prefix_dt_names dt_descr sorts str = |
29 fun prefix_dt_names descr sorts str = |
18 let |
30 let |
19 fun get_nth_name (i, _) = |
31 fun get_nth_name (i, _) = |
20 Datatype_Aux.name_of_typ (nth_dtyp dt_descr sorts i) |
32 Datatype_Aux.name_of_typ (nth_dtyp descr sorts i) |
21 in |
33 in |
22 Datatype_Prop.indexify_names |
34 Datatype_Prop.indexify_names |
23 (map (prefix str o get_nth_name) dt_descr) |
35 (map (prefix str o get_nth_name) descr) |
24 end |
36 end |
25 *} |
37 *} |
26 |
38 |
27 |
39 |
28 ML {* |
40 ML {* |