src/Pure/library.ML
changeset 46891 af4c1dd3963f
parent 46838 c54b81bb9588
child 47022 8eac39af4ec0
equal deleted inserted replaced
46890:38171cab67ae 46891:af4c1dd3963f
    64   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
    65   val perhaps_apply: ('a -> 'a option) list -> 'a -> 'a option
    65   val perhaps_apply: ('a -> 'a option) list -> 'a -> 'a option
    66   val perhaps_loop: ('a -> 'a option) -> 'a -> 'a option
    66   val perhaps_loop: ('a -> 'a option) -> 'a -> 'a option
    67   val foldl1: ('a * 'a -> 'a) -> 'a list -> 'a
    67   val foldl1: ('a * 'a -> 'a) -> 'a list -> 'a
    68   val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
    68   val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
    69   val flat: 'a list list -> 'a list
    69   val eq_list: ('a * 'a -> bool) -> 'a list * 'a list -> bool
    70   val unflat: 'a list list -> 'b list -> 'b list list
       
    71   val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list
       
    72   val burrow_options: ('a list -> 'b list) -> 'a option list -> 'b option list
       
    73   val burrow_fst: ('a list -> 'b list) -> ('a * 'c) list -> ('b * 'c) list
       
    74   val fold_burrow: ('a list -> 'c -> 'b list * 'd) -> 'a list list -> 'c -> 'b list list * 'd
       
    75   val maps: ('a -> 'b list) -> 'a list -> 'b list
    70   val maps: ('a -> 'b list) -> 'a list -> 'b list
    76   val filter: ('a -> bool) -> 'a list -> 'a list
    71   val filter: ('a -> bool) -> 'a list -> 'a list
    77   val filter_out: ('a -> bool) -> 'a list -> 'a list
    72   val filter_out: ('a -> bool) -> 'a list -> 'a list
    78   val map_filter: ('a -> 'b option) -> 'a list -> 'b list
    73   val map_filter: ('a -> 'b option) -> 'a list -> 'b list
    79   val take: int -> 'a list -> 'a list
    74   val take: int -> 'a list -> 'a list
    80   val drop: int -> 'a list -> 'a list
    75   val drop: int -> 'a list -> 'a list
    81   val chop: int -> 'a list -> 'a list * 'a list
    76   val chop: int -> 'a list -> 'a list * 'a list
    82   val chop_while: ('a -> bool) -> 'a list -> 'a list * 'a list
    77   val chop_while: ('a -> bool) -> 'a list -> 'a list * 'a list
       
    78   val chop_groups: int -> 'a list -> 'a list list
    83   val nth: 'a list -> int -> 'a
    79   val nth: 'a list -> int -> 'a
       
    80   val nth_list: 'a list list -> int -> 'a list
    84   val nth_map: int -> ('a -> 'a) -> 'a list -> 'a list
    81   val nth_map: int -> ('a -> 'a) -> 'a list -> 'a list
    85   val nth_drop: int -> 'a list -> 'a list
    82   val nth_drop: int -> 'a list -> 'a list
    86   val nth_list: 'a list list -> int -> 'a list
       
    87   val map_index: (int * 'a -> 'b) -> 'a list -> 'b list
    83   val map_index: (int * 'a -> 'b) -> 'a list -> 'b list
    88   val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
    84   val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
    89   val map_range: (int -> 'a) -> int -> 'a list
    85   val map_range: (int -> 'a) -> int -> 'a list
    90   val split_last: 'a list -> 'a list * 'a
    86   val split_last: 'a list -> 'a list * 'a
       
    87   val find_first: ('a -> bool) -> 'a list -> 'a option
    91   val find_index: ('a -> bool) -> 'a list -> int
    88   val find_index: ('a -> bool) -> 'a list -> int
    92   val find_first: ('a -> bool) -> 'a list -> 'a option
    89   val get_first: ('a -> 'b option) -> 'a list -> 'b option
    93   val get_index: ('a -> 'b option) -> 'a list -> (int * 'b) option
    90   val get_index: ('a -> 'b option) -> 'a list -> (int * 'b) option
    94   val get_first: ('a -> 'b option) -> 'a list -> 'b option
    91   val flat: 'a list list -> 'a list
    95   val eq_list: ('a * 'a -> bool) -> 'a list * 'a list -> bool
    92   val unflat: 'a list list -> 'b list -> 'b list list
       
    93   val grouped: int -> (('a list -> 'b list) -> 'c list list -> 'd list list) ->
       
    94     ('a -> 'b) -> 'c list -> 'd list
       
    95   val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list
       
    96   val burrow_options: ('a list -> 'b list) -> 'a option list -> 'b option list
       
    97   val fold_burrow: ('a list -> 'c -> 'b list * 'd) -> 'a list list -> 'c -> 'b list list * 'd
       
    98   val separate: 'a -> 'a list -> 'a list
       
    99   val surround: 'a -> 'a list -> 'a list
       
   100   val replicate: int -> 'a -> 'a list
       
   101   val map_product: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
       
   102   val fold_product: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
    96   val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
   103   val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
    97   val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
   104   val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
    98   val fold_rev2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
   105   val fold_rev2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
    99   val forall2: ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
   106   val forall2: ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
       
   107   val map_split: ('a -> 'b * 'c) -> 'a list -> 'b list * 'c list
   100   val zip_options: 'a list -> 'b option list -> ('a * 'b) list
   108   val zip_options: 'a list -> 'b option list -> ('a * 'b) list
   101   val ~~ : 'a list * 'b list -> ('a * 'b) list
   109   val ~~ : 'a list * 'b list -> ('a * 'b) list
   102   val map_split: ('a -> 'b * 'c) -> 'a list -> 'b list * 'c list
       
   103   val split_list: ('a * 'b) list -> 'a list * 'b list
   110   val split_list: ('a * 'b) list -> 'a list * 'b list
   104   val map_product: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
   111   val burrow_fst: ('a list -> 'b list) -> ('a * 'c) list -> ('b * 'c) list
   105   val fold_product: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
       
   106   val map_transpose: ('a list -> 'b) -> 'a list list -> 'b list
       
   107   val separate: 'a -> 'a list -> 'a list
       
   108   val surround: 'a -> 'a list -> 'a list
       
   109   val replicate: int -> 'a -> 'a list
       
   110   val is_prefix: ('a * 'a -> bool) -> 'a list -> 'a list -> bool
   112   val is_prefix: ('a * 'a -> bool) -> 'a list -> 'a list -> bool
   111   val take_prefix: ('a -> bool) -> 'a list -> 'a list * 'a list
   113   val take_prefix: ('a -> bool) -> 'a list -> 'a list * 'a list
   112   val chop_prefix: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list * ('a list * 'b list)
   114   val chop_prefix: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list * ('a list * 'b list)
   113   val take_suffix: ('a -> bool) -> 'a list -> 'a list * 'a list
   115   val take_suffix: ('a -> bool) -> 'a list -> 'a list * 'a list
   114   val prefixes1: 'a list -> 'a list list
   116   val prefixes1: 'a list -> 'a list list
   169   val subset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   171   val subset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   170   val eq_set: ('a * 'a -> bool) -> 'a list * 'a list -> bool
   172   val eq_set: ('a * 'a -> bool) -> 'a list * 'a list -> bool
   171   val distinct: ('a * 'a -> bool) -> 'a list -> 'a list
   173   val distinct: ('a * 'a -> bool) -> 'a list -> 'a list
   172   val duplicates: ('a * 'a -> bool) -> 'a list -> 'a list
   174   val duplicates: ('a * 'a -> bool) -> 'a list -> 'a list
   173   val has_duplicates: ('a * 'a -> bool) -> 'a list -> bool
   175   val has_duplicates: ('a * 'a -> bool) -> 'a list -> bool
       
   176   val map_transpose: ('a list -> 'b) -> 'a list list -> 'b list
   174 
   177 
   175   (*lists as multisets*)
   178   (*lists as multisets*)
   176   val remove1: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list
   179   val remove1: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list
   177   val combine: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list
   180   val combine: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list
   178   val submultiset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   181   val submultiset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   412 
   415 
   413 fun chop_while P [] = ([], [])
   416 fun chop_while P [] = ([], [])
   414   | chop_while P (ys as x :: xs) =
   417   | chop_while P (ys as x :: xs) =
   415       if P x then chop_while P xs |>> cons x else ([], ys);
   418       if P x then chop_while P xs |>> cons x else ([], ys);
   416 
   419 
       
   420 fun chop_groups n list =
       
   421   (case chop (Int.max (n, 1)) list of
       
   422     ([], _) => []
       
   423   | (g, rest) => g :: chop_groups n rest);
       
   424 
       
   425 
   417 (*return nth element of a list, where 0 designates the first element;
   426 (*return nth element of a list, where 0 designates the first element;
   418   raise Subscript if list too short*)
   427   raise Subscript if list too short*)
   419 fun nth xs i = List.nth (xs, i);
   428 fun nth xs i = List.nth (xs, i);
   420 
   429 
   421 fun nth_list xss i = nth xss i handle General.Subscript => [];
   430 fun nth_list xss i = nth xss i handle General.Subscript => [];
   447 
   456 
   448 (*rear decomposition*)
   457 (*rear decomposition*)
   449 fun split_last [] = raise Empty
   458 fun split_last [] = raise Empty
   450   | split_last [x] = ([], x)
   459   | split_last [x] = ([], x)
   451   | split_last (x :: xs) = apfst (cons x) (split_last xs);
   460   | split_last (x :: xs) = apfst (cons x) (split_last xs);
       
   461 
       
   462 (*find first element satisfying predicate*)
       
   463 val find_first = List.find;
   452 
   464 
   453 (*find position of first element satisfying a predicate*)
   465 (*find position of first element satisfying a predicate*)
   454 fun find_index pred =
   466 fun find_index pred =
   455   let fun find (_: int) [] = ~1
   467   let fun find (_: int) [] = ~1
   456         | find n (x :: xs) = if pred x then n else find (n + 1) xs;
   468         | find n (x :: xs) = if pred x then n else find (n + 1) xs;
   457   in find 0 end;
   469   in find 0 end;
   458 
       
   459 (*find first element satisfying predicate*)
       
   460 val find_first = List.find;
       
   461 
   470 
   462 (*get first element by lookup function*)
   471 (*get first element by lookup function*)
   463 fun get_first _ [] = NONE
   472 fun get_first _ [] = NONE
   464   | get_first f (x :: xs) =
   473   | get_first f (x :: xs) =
   465       (case f x of
   474       (case f x of
   480 fun unflat (xs :: xss) ys =
   489 fun unflat (xs :: xss) ys =
   481       let val (ps, qs) = chop (length xs) ys
   490       let val (ps, qs) = chop (length xs) ys
   482       in ps :: unflat xss qs end
   491       in ps :: unflat xss qs end
   483   | unflat [] [] = []
   492   | unflat [] [] = []
   484   | unflat _ _ = raise ListPair.UnequalLengths;
   493   | unflat _ _ = raise ListPair.UnequalLengths;
       
   494 
       
   495 fun grouped n comb f = chop_groups n #> comb (map f) #> flat;
   485 
   496 
   486 fun burrow f xss = unflat xss (f (flat xss));
   497 fun burrow f xss = unflat xss (f (flat xss));
   487 
   498 
   488 fun burrow_options f os = map (try hd) (burrow f (map the_list os));
   499 fun burrow_options f os = map (try hd) (burrow f (map the_list os));
   489 
   500