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 |
494 |
491 |
495 fun unflat (xs :: xss) ys = |
492 fun unflat (xs :: xss) ys = |
496 let val (ps, qs) = chop (length xs) ys |
493 let val (ps, qs) = chop (length xs) ys |
497 in ps :: unflat xss qs end |
494 in ps :: unflat xss qs end |
498 | unflat [] [] = [] |
495 | unflat [] [] = [] |
499 | unflat _ _ = raise UnequalLengths; |
496 | unflat _ _ = raise ListPair.UnequalLengths; |
500 |
497 |
501 fun burrow f xss = unflat xss (f (flat xss)); |
498 fun burrow f xss = unflat xss (f (flat xss)); |
502 |
499 |
503 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)); |
504 |
501 |
533 | 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; |
534 |
531 |
535 |
532 |
536 (* lists of pairs *) |
533 (* lists of pairs *) |
537 |
534 |
538 exception UnequalLengths; |
|
539 |
|
540 fun map2 _ [] [] = [] |
535 fun map2 _ [] [] = [] |
541 | 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 |
542 | map2 _ _ _ = raise UnequalLengths; |
537 | map2 _ _ _ = raise ListPair.UnequalLengths; |
543 |
538 |
544 fun fold2 f [] [] z = z |
539 fun fold2 f [] [] z = z |
545 | 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) |
546 | fold2 f _ _ _ = raise UnequalLengths; |
541 | fold2 f _ _ _ = raise ListPair.UnequalLengths; |
547 |
542 |
548 fun fold_rev2 f [] [] z = z |
543 fun fold_rev2 f [] [] z = z |
549 | fold_rev2 f (x :: xs) (y :: ys) z = f x y (fold_rev2 f xs ys z) |
544 | fold_rev2 f (x :: xs) (y :: ys) z = f x y (fold_rev2 f xs ys z) |
550 | fold_rev2 f _ _ _ = raise UnequalLengths; |
545 | fold_rev2 f _ _ _ = raise ListPair.UnequalLengths; |
551 |
546 |
552 fun forall2 P [] [] = true |
547 fun forall2 P [] [] = true |
553 | 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 |
554 | forall2 P _ _ = false; |
549 | forall2 P _ _ = false; |
555 |
550 |
561 in (y :: ys, w :: ws) end; |
556 in (y :: ys, w :: ws) end; |
562 |
557 |
563 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 |
564 | zip_options (_ :: xs) (NONE :: ys) = zip_options xs ys |
559 | zip_options (_ :: xs) (NONE :: ys) = zip_options xs ys |
565 | zip_options _ [] = [] |
560 | zip_options _ [] = [] |
566 | zip_options [] _ = raise UnequalLengths; |
561 | zip_options [] _ = raise ListPair.UnequalLengths; |
567 |
562 |
568 (*combine two lists forming a list of pairs: |
563 (*combine two lists forming a list of pairs: |
569 [x1, ..., xn] ~~ [y1, ..., yn] ===> [(x1, y1), ..., (xn, yn)]*) |
564 [x1, ..., xn] ~~ [y1, ..., yn] ===> [(x1, y1), ..., (xn, yn)]*) |
570 fun [] ~~ [] = [] |
565 fun [] ~~ [] = [] |
571 | (x :: xs) ~~ (y :: ys) = (x, y) :: (xs ~~ ys) |
566 | (x :: xs) ~~ (y :: ys) = (x, y) :: (xs ~~ ys) |
572 | _ ~~ _ = raise UnequalLengths; |
567 | _ ~~ _ = raise ListPair.UnequalLengths; |
573 |
568 |
574 (*inverse of ~~; the old 'split': |
569 (*inverse of ~~; the old 'split': |
575 [(x1, y1), ..., (xn, yn)] ===> ([x1, ..., xn], [y1, ..., yn])*) |
570 [(x1, y1), ..., (xn, yn)] ===> ([x1, ..., xn], [y1, ..., yn])*) |
576 val split_list = ListPair.unzip; |
571 val split_list = ListPair.unzip; |
577 |
572 |
846 |
841 |
847 (* matrices *) |
842 (* matrices *) |
848 |
843 |
849 fun map_transpose f xss = |
844 fun map_transpose f xss = |
850 let |
845 let |
851 val n = case distinct (op =) (map length xss) |
846 val n = |
852 of [] => 0 |
847 (case distinct (op =) (map length xss) of |
|
848 [] => 0 |
853 | [n] => n |
849 | [n] => n |
854 | _ => raise UnequalLengths; |
850 | _ => raise ListPair.UnequalLengths); |
855 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; |
856 |
852 |
857 |
853 |
858 |
854 |
859 (** lists as multisets **) |
855 (** lists as multisets **) |