95 val append: 'a list -> 'a list -> 'a list |
95 val append: 'a list -> 'a list -> 'a list |
96 val apply: ('a -> 'a) list -> 'a -> 'a |
96 val apply: ('a -> 'a) list -> 'a -> 'a |
97 val fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b |
97 val fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b |
98 val fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b |
98 val fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b |
99 val fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b |
99 val fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b |
100 val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c |
|
101 val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b |
100 val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b |
102 val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a |
101 val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a |
103 val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list |
102 val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list |
104 val unflat: 'a list list -> 'b list -> 'b list list |
103 val unflat: 'a list list -> 'b list -> 'b list list |
105 val splitAt: int * 'a list -> 'a list * 'a list |
104 val splitAt: int * 'a list -> 'a list * 'a list |
111 val split_last: 'a list -> 'a list * 'a |
110 val split_last: 'a list -> 'a list * 'a |
112 val find_index: ('a -> bool) -> 'a list -> int |
111 val find_index: ('a -> bool) -> 'a list -> int |
113 val find_index_eq: ''a -> ''a list -> int |
112 val find_index_eq: ''a -> ''a list -> int |
114 val find_first: ('a -> bool) -> 'a list -> 'a option |
113 val find_first: ('a -> bool) -> 'a list -> 'a option |
115 val get_first: ('a -> 'b option) -> 'a list -> 'b option |
114 val get_first: ('a -> 'b option) -> 'a list -> 'b option |
|
115 val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list |
|
116 val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c |
|
117 val ~~ : 'a list * 'b list -> ('a * 'b) list |
|
118 val split_list: ('a * 'b) list -> 'a list * 'b list |
116 val separate: 'a -> 'a list -> 'a list |
119 val separate: 'a -> 'a list -> 'a list |
117 val replicate: int -> 'a -> 'a list |
120 val replicate: int -> 'a -> 'a list |
118 val multiply: 'a list -> 'a list list -> 'a list list |
121 val multiply: 'a list -> 'a list list -> 'a list list |
119 val product: 'a list -> 'b list -> ('a * 'b) list |
122 val product: 'a list -> 'b list -> ('a * 'b) list |
120 val filter: ('a -> bool) -> 'a list -> 'a list |
123 val filter: ('a -> bool) -> 'a list -> 'a list |
121 val filter_out: ('a -> bool) -> 'a list -> 'a list |
124 val filter_out: ('a -> bool) -> 'a list -> 'a list |
122 val map2: ('a * 'b -> 'c) -> 'a list * 'b list -> 'c list |
|
123 val exists2: ('a * 'b -> bool) -> 'a list * 'b list -> bool |
|
124 val forall2: ('a * 'b -> bool) -> 'a list * 'b list -> bool |
|
125 val seq2: ('a * 'b -> unit) -> 'a list * 'b list -> unit |
|
126 val ~~ : 'a list * 'b list -> ('a * 'b) list |
|
127 val split_list: ('a * 'b) list -> 'a list * 'b list |
|
128 val equal_lists: ('a * 'b -> bool) -> 'a list * 'b list -> bool |
125 val equal_lists: ('a * 'b -> bool) -> 'a list * 'b list -> bool |
129 val prefix: ''a list * ''a list -> bool |
126 val prefix: ''a list * ''a list -> bool |
130 val take_prefix: ('a -> bool) -> 'a list -> 'a list * 'a list |
127 val take_prefix: ('a -> bool) -> 'a list -> 'a list * 'a list |
131 val take_suffix: ('a -> bool) -> 'a list -> 'a list * 'a list |
128 val take_suffix: ('a -> bool) -> 'a list -> 'a list * 'a list |
132 val prefixes1: 'a list -> 'a list list |
129 val prefixes1: 'a list -> 'a list list |
465 let |
462 let |
466 fun fold_aux [] y = y |
463 fun fold_aux [] y = y |
467 | fold_aux (x :: xs) y = fold_aux xs (f x y); |
464 | fold_aux (x :: xs) y = fold_aux xs (f x y); |
468 in fold_aux end; |
465 in fold_aux end; |
469 |
466 |
470 fun fold2 f = |
|
471 let |
|
472 fun fold_aux [] [] z = z |
|
473 | fold_aux (x :: xs) (y :: ys) z = fold_aux xs ys (f x y z) |
|
474 | fold_aux _ _ _ = raise UnequalLengths; |
|
475 in fold_aux end; |
|
476 |
|
477 fun fold_rev f = |
467 fun fold_rev f = |
478 let |
468 let |
479 fun fold_aux [] y = y |
469 fun fold_aux [] y = y |
480 | fold_aux (x :: xs) y = f x (fold_aux xs y); |
470 | fold_aux (x :: xs) y = f x (fold_aux xs y); |
481 in fold_aux end; |
471 in fold_aux end; |
641 |
631 |
642 (* lists of pairs *) |
632 (* lists of pairs *) |
643 |
633 |
644 exception UnequalLengths; |
634 exception UnequalLengths; |
645 |
635 |
646 fun map2 _ ([], []) = [] |
636 fun map2 _ [] [] = [] |
647 | map2 f (x :: xs, y :: ys) = f (x, y) :: map2 f (xs, ys) |
637 | map2 f (x :: xs) (y :: ys) = f x y :: map2 f xs ys |
648 | map2 _ _ = raise UnequalLengths; |
638 | map2 _ _ _ = raise UnequalLengths; |
649 |
639 |
650 fun exists2 _ ([], []) = false |
640 fun fold2 f = |
651 | exists2 pred (x :: xs, y :: ys) = pred (x, y) orelse exists2 pred (xs, ys) |
641 let |
652 | exists2 _ _ = raise UnequalLengths; |
642 fun fold_aux [] [] z = z |
653 |
643 | fold_aux (x :: xs) (y :: ys) z = fold_aux xs ys (f x y z) |
654 fun forall2 _ ([], []) = true |
644 | fold_aux _ _ _ = raise UnequalLengths; |
655 | forall2 pred (x :: xs, y :: ys) = pred (x, y) andalso forall2 pred (xs, ys) |
645 in fold_aux end; |
656 | forall2 _ _ = raise UnequalLengths; |
646 |
657 |
|
658 fun seq2 _ ([], []) = () |
|
659 | seq2 f (x :: xs, y :: ys) = (f (x, y); seq2 f (xs, ys)) |
|
660 | seq2 _ _ = raise UnequalLengths; |
|
661 |
647 |
662 (*combine two lists forming a list of pairs: |
648 (*combine two lists forming a list of pairs: |
663 [x1, ..., xn] ~~ [y1, ..., yn] ===> [(x1, y1), ..., (xn, yn)]*) |
649 [x1, ..., xn] ~~ [y1, ..., yn] ===> [(x1, y1), ..., (xn, yn)]*) |
664 fun [] ~~ [] = [] |
650 fun [] ~~ [] = [] |
665 | (x :: xs) ~~ (y :: ys) = (x, y) :: (xs ~~ ys) |
651 | (x :: xs) ~~ (y :: ys) = (x, y) :: (xs ~~ ys) |
667 |
653 |
668 (*inverse of ~~; the old 'split': |
654 (*inverse of ~~; the old 'split': |
669 [(x1, y1), ..., (xn, yn)] ===> ([x1, ..., xn], [y1, ..., yn])*) |
655 [(x1, y1), ..., (xn, yn)] ===> ([x1, ..., xn], [y1, ..., yn])*) |
670 val split_list = ListPair.unzip; |
656 val split_list = ListPair.unzip; |
671 |
657 |
672 fun equal_lists eq (xs, ys) = length xs = length ys andalso forall2 eq (xs, ys); |
658 fun equal_lists eq (xs, ys) = |
|
659 let |
|
660 fun eq' [] [] = true |
|
661 | eq' (x :: xs) (y :: ys) = eq (x, y) andalso eq' xs ys |
|
662 in length xs = length ys andalso eq' xs ys end; |
673 |
663 |
674 |
664 |
675 (* prefixes, suffixes *) |
665 (* prefixes, suffixes *) |
676 |
666 |
677 fun [] prefix _ = true |
667 fun [] prefix _ = true |