56 val forall: ('a -> bool) -> 'a list -> bool |
56 val forall: ('a -> bool) -> 'a list -> bool |
57 val setmp_CRITICAL: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c |
57 val setmp_CRITICAL: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c |
58 val setmp_thread_data: 'a Universal.tag -> 'a -> 'a -> ('b -> 'c) -> 'b -> 'c |
58 val setmp_thread_data: 'a Universal.tag -> 'a -> 'a -> ('b -> 'c) -> 'b -> 'c |
59 |
59 |
60 (*lists*) |
60 (*lists*) |
61 exception UnequalLengths |
|
62 val single: 'a -> 'a list |
61 val single: 'a -> 'a list |
63 val the_single: 'a list -> 'a |
62 val the_single: 'a list -> 'a |
64 val singleton: ('a list -> 'b list) -> 'a -> 'b |
63 val singleton: ('a list -> 'b list) -> 'a -> 'b |
65 val yield_singleton: ('a list -> 'c -> 'b list * 'c) -> 'a -> 'c -> 'b * 'c |
64 val yield_singleton: ('a list -> 'c -> 'b list * 'c) -> 'a -> 'c -> 'b * 'c |
66 val apply: ('a -> 'a) list -> 'a -> 'a |
65 val apply: ('a -> 'a) list -> 'a -> 'a |
95 val get_index: ('a -> 'b option) -> 'a list -> (int * 'b) option |
94 val get_index: ('a -> 'b option) -> 'a list -> (int * 'b) option |
96 val get_first: ('a -> 'b option) -> 'a list -> 'b option |
95 val get_first: ('a -> 'b option) -> 'a list -> 'b option |
97 val eq_list: ('a * 'b -> bool) -> 'a list * 'b list -> bool |
96 val eq_list: ('a * 'b -> bool) -> 'a list * 'b list -> bool |
98 val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list |
97 val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list |
99 val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c |
98 val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c |
|
99 val fold_rev2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c |
100 val forall2: ('a -> 'b -> bool) -> 'a list -> 'b list -> bool |
100 val forall2: ('a -> 'b -> bool) -> 'a list -> 'b list -> bool |
101 val zip_options: 'a list -> 'b option list -> ('a * 'b) list |
101 val zip_options: 'a list -> 'b option list -> ('a * 'b) list |
102 val ~~ : 'a list * 'b list -> ('a * 'b) list |
102 val ~~ : 'a list * 'b list -> ('a * 'b) list |
103 val map_split: ('a -> 'b * 'c) -> 'a list -> 'b list * 'c list |
103 val map_split: ('a -> 'b * 'c) -> 'a list -> 'b list * 'c list |
104 val split_list: ('a * 'b) list -> 'a list * 'b list |
104 val split_list: ('a * 'b) list -> 'a list * 'b list |
493 |
491 |
494 fun unflat (xs :: xss) ys = |
492 fun unflat (xs :: xss) ys = |
495 let val (ps, qs) = chop (length xs) ys |
493 let val (ps, qs) = chop (length xs) ys |
496 in ps :: unflat xss qs end |
494 in ps :: unflat xss qs end |
497 | unflat [] [] = [] |
495 | unflat [] [] = [] |
498 | unflat _ _ = raise UnequalLengths; |
496 | unflat _ _ = raise ListPair.UnequalLengths; |
499 |
497 |
500 fun burrow f xss = unflat xss (f (flat xss)); |
498 fun burrow f xss = unflat xss (f (flat xss)); |
501 |
499 |
502 fun burrow_options f os = map (try hd) (burrow f (map the_list os)); |
500 fun burrow_options f os = map (try hd) (burrow f (map the_list os)); |
503 |
501 |
532 | fold_product f (x :: xs) ys z = z |> fold (f x) ys |> fold_product f xs ys; |
530 | fold_product f (x :: xs) ys z = z |> fold (f x) ys |> fold_product f xs ys; |
533 |
531 |
534 |
532 |
535 (* lists of pairs *) |
533 (* lists of pairs *) |
536 |
534 |
537 exception UnequalLengths; |
|
538 |
|
539 fun map2 _ [] [] = [] |
535 fun map2 _ [] [] = [] |
540 | map2 f (x :: xs) (y :: ys) = f x y :: map2 f xs ys |
536 | map2 f (x :: xs) (y :: ys) = f x y :: map2 f xs ys |
541 | map2 _ _ _ = raise UnequalLengths; |
537 | map2 _ _ _ = raise ListPair.UnequalLengths; |
542 |
538 |
543 fun fold2 f [] [] z = z |
539 fun fold2 f [] [] z = z |
544 | fold2 f (x :: xs) (y :: ys) z = fold2 f xs ys (f x y z) |
540 | fold2 f (x :: xs) (y :: ys) z = fold2 f xs ys (f x y z) |
545 | fold2 f _ _ _ = raise UnequalLengths; |
541 | fold2 f _ _ _ = raise ListPair.UnequalLengths; |
|
542 |
|
543 fun fold_rev2 f [] [] z = z |
|
544 | fold_rev2 f (x :: xs) (y :: ys) z = f x y (fold_rev2 f xs ys z) |
|
545 | fold_rev2 f _ _ _ = raise ListPair.UnequalLengths; |
546 |
546 |
547 fun forall2 P [] [] = true |
547 fun forall2 P [] [] = true |
548 | forall2 P (x :: xs) (y :: ys) = P x y andalso forall2 P xs ys |
548 | forall2 P (x :: xs) (y :: ys) = P x y andalso forall2 P xs ys |
549 | forall2 P _ _ = raise UnequalLengths; |
549 | forall2 P _ _ = raise ListPair.UnequalLengths; |
550 |
550 |
551 fun map_split f [] = ([], []) |
551 fun map_split f [] = ([], []) |
552 | map_split f (x :: xs) = |
552 | map_split f (x :: xs) = |
553 let |
553 let |
554 val (y, w) = f x; |
554 val (y, w) = f x; |
556 in (y :: ys, w :: ws) end; |
556 in (y :: ys, w :: ws) end; |
557 |
557 |
558 fun zip_options (x :: xs) (SOME y :: ys) = (x, y) :: zip_options xs ys |
558 fun zip_options (x :: xs) (SOME y :: ys) = (x, y) :: zip_options xs ys |
559 | zip_options (_ :: xs) (NONE :: ys) = zip_options xs ys |
559 | zip_options (_ :: xs) (NONE :: ys) = zip_options xs ys |
560 | zip_options _ [] = [] |
560 | zip_options _ [] = [] |
561 | zip_options [] _ = raise UnequalLengths; |
561 | zip_options [] _ = raise ListPair.UnequalLengths; |
562 |
562 |
563 (*combine two lists forming a list of pairs: |
563 (*combine two lists forming a list of pairs: |
564 [x1, ..., xn] ~~ [y1, ..., yn] ===> [(x1, y1), ..., (xn, yn)]*) |
564 [x1, ..., xn] ~~ [y1, ..., yn] ===> [(x1, y1), ..., (xn, yn)]*) |
565 fun [] ~~ [] = [] |
565 fun [] ~~ [] = [] |
566 | (x :: xs) ~~ (y :: ys) = (x, y) :: (xs ~~ ys) |
566 | (x :: xs) ~~ (y :: ys) = (x, y) :: (xs ~~ ys) |
567 | _ ~~ _ = raise UnequalLengths; |
567 | _ ~~ _ = raise ListPair.UnequalLengths; |
568 |
568 |
569 (*inverse of ~~; the old 'split': |
569 (*inverse of ~~; the old 'split': |
570 [(x1, y1), ..., (xn, yn)] ===> ([x1, ..., xn], [y1, ..., yn])*) |
570 [(x1, y1), ..., (xn, yn)] ===> ([x1, ..., xn], [y1, ..., yn])*) |
571 val split_list = ListPair.unzip; |
571 val split_list = ListPair.unzip; |
572 |
572 |
841 |
841 |
842 (* matrices *) |
842 (* matrices *) |
843 |
843 |
844 fun map_transpose f xss = |
844 fun map_transpose f xss = |
845 let |
845 let |
846 val n = case distinct (op =) (map length xss) |
846 val n = |
847 of [] => 0 |
847 (case distinct (op =) (map length xss) of |
|
848 [] => 0 |
848 | [n] => n |
849 | [n] => n |
849 | _ => raise UnequalLengths; |
850 | _ => raise ListPair.UnequalLengths); |
850 in map_range (fn m => f (map (fn xs => nth xs m) xss)) n end; |
851 in map_range (fn m => f (map (fn xs => nth xs m) xss)) n end; |
851 |
852 |
852 |
853 |
853 |
854 |
854 (** lists as multisets **) |
855 (** lists as multisets **) |