src/Pure/library.ML
changeset 40733 a71f786d20da
parent 40731 4e60c7348096
parent 40722 441260986b63
child 40925 7abeb749ae99
equal deleted inserted replaced
40732:4375cc6f1a7e 40733:a71f786d20da
    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
   319 
   319 
   320 
   320 
   321 
   321 
   322 (** lists **)
   322 (** lists **)
   323 
   323 
   324 exception UnequalLengths;
       
   325 
       
   326 fun single x = [x];
   324 fun single x = [x];
   327 
   325 
   328 fun the_single [x] = x
   326 fun the_single [x] = x
   329   | the_single _ = raise Empty;
   327   | the_single _ = raise Empty;
   330 
   328 
   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 **)
  1064 
  1065 
  1065 end;
  1066 end;
  1066 
  1067 
  1067 structure Basic_Library: BASIC_LIBRARY = Library;
  1068 structure Basic_Library: BASIC_LIBRARY = Library;
  1068 open Basic_Library;
  1069 open Basic_Library;
       
  1070 
       
  1071 datatype legacy = UnequalLengths;