equal
deleted
inserted
replaced
68 *} |
68 *} |
69 |
69 |
70 ML {* |
70 ML {* |
71 (* permutation function for one argument |
71 (* permutation function for one argument |
72 |
72 |
73 - in case the argument is non-recursive it returns |
73 - in case the argument is recursive it returns |
|
74 |
|
75 permute_fn p arg |
|
76 |
|
77 - in case the argument is non-recursive it will build |
74 |
78 |
75 p o arg |
79 p o arg |
76 |
80 |
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 *) |
81 *) |
84 fun perm_arg permute_fns pi (arg_dty, arg) = |
82 fun perm_arg permute_fns pi (arg_dty, arg) = |
85 if Datatype_Aux.is_rec_type arg_dty |
83 if Datatype_Aux.is_rec_type arg_dty |
86 then |
84 then Free (nth permute_fns (Datatype_Aux.body_index arg_dty)) $ pi $ arg |
87 let |
|
88 val T = type_of arg |
|
89 val (Us, _) = strip_type T |
|
90 val indxs_tys = (length Us - 1 downto 0) ~~ Us |
|
91 val permute_fn = Free (nth permute_fns (Datatype_Aux.body_index arg_dty)) |
|
92 in |
|
93 list_abs (map (pair "x") Us, permute_fn $ pi $ |
|
94 list_comb (arg, map (fn (i, U) => (mk_perm_ty U (mk_minus pi) (Bound i))) indxs_tys)) |
|
95 end |
|
96 else mk_perm pi arg |
85 else mk_perm pi arg |
97 *} |
86 *} |
98 |
87 |
99 ML {* |
88 ML {* |
100 (* equation for permutation function for one constructor *) |
89 (* equation for permutation function for one constructor *) |