36 val n_fold_cartesian_product : 'a list list -> 'a list list |
36 val n_fold_cartesian_product : 'a list list -> 'a list list |
37 val all_distinct_unordered_pairs_of : ''a list -> (''a * ''a) list |
37 val all_distinct_unordered_pairs_of : ''a list -> (''a * ''a) list |
38 val nth_combination : (int * int) list -> int -> int list |
38 val nth_combination : (int * int) list -> int -> int list |
39 val all_combinations : (int * int) list -> int list list |
39 val all_combinations : (int * int) list -> int list list |
40 val all_permutations : 'a list -> 'a list list |
40 val all_permutations : 'a list -> 'a list list |
41 val batch_list : int -> 'a list -> 'a list list |
41 val chunk_list : int -> 'a list -> 'a list list |
42 val chunk_list_unevenly : int list -> 'a list -> 'a list list |
42 val chunk_list_unevenly : int list -> 'a list -> 'a list list |
43 val map3 : ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list |
43 val map3 : ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list |
44 val double_lookup : |
44 val double_lookup : |
45 ('a * 'a -> bool) -> ('a option * 'b) list -> 'a -> 'b option |
45 ('a * 'a -> bool) -> ('a option * 'b) list -> 'a -> 'b option |
46 val triple_lookup : |
46 val triple_lookup : |
190 fun all_permutations [] = [[]] |
190 fun all_permutations [] = [[]] |
191 | all_permutations xs = |
191 | all_permutations xs = |
192 maps (fn j => map (cons (nth xs j)) (all_permutations (nth_drop j xs))) |
192 maps (fn j => map (cons (nth xs j)) (all_permutations (nth_drop j xs))) |
193 (index_seq 0 (length xs)) |
193 (index_seq 0 (length xs)) |
194 |
194 |
195 fun batch_list _ [] = [] |
195 val chunk_list = ATP_Util.chunk_list |
196 | batch_list k xs = |
|
197 if length xs <= k then [xs] |
|
198 else List.take (xs, k) :: batch_list k (List.drop (xs, k)) |
|
199 |
196 |
200 fun chunk_list_unevenly _ [] = [] |
197 fun chunk_list_unevenly _ [] = [] |
201 | chunk_list_unevenly [] ys = map single ys |
198 | chunk_list_unevenly [] xs = map single xs |
202 | chunk_list_unevenly (k :: ks) ys = |
199 | chunk_list_unevenly (k :: ks) xs = |
203 let val (ys1, ys2) = chop k ys in ys1 :: chunk_list_unevenly ks ys2 end |
200 let val (xs1, xs2) = chop k xs in xs1 :: chunk_list_unevenly ks xs2 end |
204 |
201 |
205 fun map3 _ [] [] [] = [] |
202 fun map3 _ [] [] [] = [] |
206 | map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs |
203 | map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs |
207 | map3 _ _ _ _ = raise ListPair.UnequalLengths |
204 | map3 _ _ _ _ = raise ListPair.UnequalLengths |
208 |
205 |