1109 Tuple (T, R, [shape_tuple T1 R1 (List.take (us, arity1)), |
1109 Tuple (T, R, [shape_tuple T1 R1 (List.take (us, arity1)), |
1110 shape_tuple T2 R2 (List.drop (us, arity1))]) |
1110 shape_tuple T2 R2 (List.drop (us, arity1))]) |
1111 end |
1111 end |
1112 | shape_tuple T (R as Vect (k, R')) us = |
1112 | shape_tuple T (R as Vect (k, R')) us = |
1113 Tuple (T, R, map (shape_tuple (pseudo_range_type T) R') |
1113 Tuple (T, R, map (shape_tuple (pseudo_range_type T) R') |
1114 (batch_list (length us div k) us)) |
1114 (chunk_list (length us div k) us)) |
1115 | shape_tuple T _ [u] = |
1115 | shape_tuple T _ [u] = |
1116 if type_of u = T then u else raise NUT ("Nitpick_Nut.shape_tuple", [u]) |
1116 if type_of u = T then u else raise NUT ("Nitpick_Nut.shape_tuple", [u]) |
1117 | shape_tuple _ _ us = raise NUT ("Nitpick_Nut.shape_tuple", us) |
1117 | shape_tuple _ _ us = raise NUT ("Nitpick_Nut.shape_tuple", us) |
1118 |
1118 |
1119 fun rename_n_ary_var rename_free v (ws, pool, table) = |
1119 fun rename_n_ary_var rename_free v (ws, pool, table) = |