src/Pure/library.ML
changeset 37851 1ce77362598f
parent 36692 54b64d4ad524
child 39616 8052101883c3
equal deleted inserted replaced
37850:afb5653a3a47 37851:1ce77362598f
   998 
   998 
   999 
   999 
  1000 (*Partition a list into buckets  [ bi, b(i+1), ..., bj ]
  1000 (*Partition a list into buckets  [ bi, b(i+1), ..., bj ]
  1001    putting x in bk if p(k)(x) holds.  Preserve order of elements if possible.*)
  1001    putting x in bk if p(k)(x) holds.  Preserve order of elements if possible.*)
  1002 fun partition_list p i j =
  1002 fun partition_list p i j =
  1003   let fun part k xs =
  1003   let
  1004             if k>j then
  1004     fun part (k: int) xs =
  1005               (case xs of [] => []
  1005       if k > j then
  1006                          | _ => raise Fail "partition_list")
  1006         (case xs of
  1007             else
  1007           [] => []
  1008             let val (ns, rest) = List.partition (p k) xs;
  1008         | _ => raise Fail "partition_list")
  1009             in  ns :: part(k+1)rest  end
  1009       else
  1010   in  part (i: int) end;
  1010         let val (ns, rest) = List.partition (p k) xs
  1011 
  1011         in ns :: part (k + 1) rest end;
  1012 fun partition_eq (eq:'a * 'a -> bool) =
  1012   in part (i: int) end;
       
  1013 
       
  1014 fun partition_eq (eq: 'a * 'a -> bool) =
  1013   let
  1015   let
  1014     fun part [] = []
  1016     fun part [] = []
  1015       | part (x :: ys) =
  1017       | part (x :: ys) =
  1016           let val (xs, xs') = List.partition (fn y => eq (x, y)) ys
  1018           let val (xs, xs') = List.partition (fn y => eq (x, y)) ys
  1017           in (x::xs)::(part xs') end
  1019           in (x :: xs) :: part xs' end;
  1018   in part end;
  1020   in part end;
  1019 
  1021 
  1020 
  1022 
  1021 
  1023 
  1022 (* generating identifiers *)
  1024 (* generating identifiers *)