199 val {descr, sorts, ...} = dt_info; |
199 val {descr, sorts, ...} = dt_info; |
200 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
200 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
201 val alpha_bn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn))); |
201 val alpha_bn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn))); |
202 val alpha_bn_type = @{typ perm} --> nth_dtyp ith_dtyp --> nth_dtyp ith_dtyp --> @{typ bool} |
202 val alpha_bn_type = @{typ perm} --> nth_dtyp ith_dtyp --> nth_dtyp ith_dtyp --> @{typ bool} |
203 val alpha_bn_free = Free(alpha_bn_name, alpha_bn_type); |
203 val alpha_bn_free = Free(alpha_bn_name, alpha_bn_type); |
204 (*... *) |
204 fun alpha_bn_constr (cname, dts) args_in_bn = |
|
205 let |
|
206 val Ts = map (typ_of_dtyp descr sorts) dts; |
|
207 val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); |
|
208 val names2 = Name.variant_list ("pi" :: names) (Datatype_Prop.make_tnames Ts); |
|
209 val args = map Free (names ~~ Ts); |
|
210 val args2 = map Free (names2 ~~ Ts); |
|
211 val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp)); |
|
212 (*...*) |
|
213 in |
|
214 [] |
|
215 end |
205 val (_, (_, _, constrs)) = nth descr ith_dtyp; |
216 val (_, (_, _, constrs)) = nth descr ith_dtyp; |
206 val eqs = [] (*map2i alpha_bn_constr constrs args_in_bns*) |
217 val eqs = map2i alpha_bn_constr constrs args_in_bns |
207 in |
218 in |
208 ((bn, alpha_bn_name), (alpha_bn_free, eqs)) |
219 ((bn, alpha_bn_name), (alpha_bn_free, eqs)) |
209 end |
220 end |
210 *} |
221 *} |
211 |
222 |