13 end; |
13 end; |
14 |
14 |
15 structure SMT_Datatypes: SMT_DATATYPES = |
15 structure SMT_Datatypes: SMT_DATATYPES = |
16 struct |
16 struct |
17 |
17 |
18 fun mk_selectors T Ts = |
18 fun mk_selectors T Ts sels = |
19 Variable.variant_fixes (replicate (length Ts) "select") |
19 if null sels then |
20 #>> map2 (fn U => fn n => Free (n, T --> U)) Ts |
20 Variable.variant_fixes (replicate (length Ts) "select") |
|
21 #>> map2 (fn U => fn n => Free (n, T --> U)) Ts |
|
22 else |
|
23 pair sels |
21 |
24 |
22 |
25 |
23 (* free constructor type declarations *) |
26 (* free constructor type declarations *) |
24 |
27 |
25 fun get_ctr_sugar_decl ({ctrs, ...} : Ctr_Sugar.ctr_sugar) T Ts ctxt = |
28 fun get_ctr_sugar_decl ({ctrs = ctrs0, selss = selss0, ...} : Ctr_Sugar.ctr_sugar) T Ts ctxt = |
26 let |
29 let |
27 fun mk_constr ctr0 = |
30 fun mk_constr ctr0 sels0 = |
28 let val ctr = Ctr_Sugar.mk_ctr Ts ctr0 in |
31 let |
29 mk_selectors T (binder_types (fastype_of ctr)) #>> pair ctr |
32 val sels = map (Ctr_Sugar.mk_disc_or_sel Ts) sels0 |
|
33 val ctr = Ctr_Sugar.mk_ctr Ts ctr0 |
|
34 val binder_Ts = binder_types (fastype_of ctr) |
|
35 in |
|
36 mk_selectors T binder_Ts sels #>> pair ctr |
30 end |
37 end |
|
38 |
|
39 val selss = if has_duplicates (op aconv) (flat selss0) then [] else selss0 |
31 in |
40 in |
32 fold_map mk_constr ctrs ctxt |
41 Ctr_Sugar_Util.fold_map2 mk_constr ctrs0 (Ctr_Sugar_Util.pad_list [] (length ctrs0) selss) ctxt |
33 |>> (pair T #> single) |
42 |>> (pair T #> single) |
34 end |
43 end |
35 |
44 |
36 |
45 |
37 (* typedef declarations *) |
46 (* typedef declarations *) |