66 fun nth_dtyp dt_descr sorts i = |
66 fun nth_dtyp dt_descr sorts i = |
67 Datatype_Aux.typ_of_dtyp dt_descr sorts (Datatype_Aux.DtRec i); |
67 Datatype_Aux.typ_of_dtyp dt_descr sorts (Datatype_Aux.DtRec i); |
68 *} |
68 *} |
69 |
69 |
70 ML {* |
70 ML {* |
71 (* permutation function for one argument *) |
71 (* permutation function for one argument |
|
72 |
|
73 - in case the argument is non-recursive it returns |
|
74 |
|
75 p o arg |
|
76 |
|
77 - in case the argument is recursive it will build |
|
78 |
|
79 %x1..xn. permute_fn p (arg (-p o x1)..(-p o xn)) |
|
80 |
|
81 the x1..xn depend whether the argument is of function |
|
82 type; normally it just returns permute_fn pi arg |
|
83 *) |
72 fun perm_arg permute_fns pi (arg_dty, arg) = |
84 fun perm_arg permute_fns pi (arg_dty, arg) = |
73 let |
|
74 val T = type_of arg |
|
75 in |
|
76 if Datatype_Aux.is_rec_type arg_dty |
85 if Datatype_Aux.is_rec_type arg_dty |
77 then |
86 then |
78 let |
87 let |
|
88 val T = type_of arg |
79 val (Us, _) = strip_type T |
89 val (Us, _) = strip_type T |
80 val indxs_tys = (length Us - 1 downto 0) ~~ Us |
90 val indxs_tys = (length Us - 1 downto 0) ~~ Us |
|
91 val permute_fn = Free (nth permute_fns (Datatype_Aux.body_index arg_dty)) |
81 in |
92 in |
82 list_abs (map (pair "x") Us, |
93 list_abs (map (pair "x") Us, permute_fn $ pi $ |
83 Free (nth permute_fns (Datatype_Aux.body_index arg_dty)) $ pi $ |
94 list_comb (arg, map (fn (i, U) => (mk_perm_ty U (mk_minus pi) (Bound i))) indxs_tys)) |
84 list_comb (arg, map (fn (i, U) => (mk_perm_ty U (mk_minus pi) (Bound i))) indxs_tys)) |
|
85 end |
95 end |
86 else mk_perm_ty T pi arg |
96 else mk_perm pi arg |
87 end |
|
88 *} |
97 *} |
89 |
98 |
90 ML {* |
99 ML {* |
91 (* equation for permutation function for one constructor *) |
100 (* equation for permutation function for one constructor *) |
92 fun perm_eq_constr thy dt_descr sorts permute_fns i (cnstr_name, dts) = |
101 fun perm_eq_constr thy dt_descr sorts permute_fns i (cnstr_name, dts) = |