src/Pure/library.ML
changeset 20108 289050bdfff5
parent 20095 432e914a0e95
child 20133 9ee091573fa0
     1.1 --- a/src/Pure/library.ML	Wed Jul 12 17:00:31 2006 +0200
     1.2 +++ b/src/Pure/library.ML	Wed Jul 12 17:00:32 2006 +0200
     1.3 @@ -145,6 +145,7 @@
     1.4    val equal_lists: ('a * 'b -> bool) -> 'a list * 'b list -> bool
     1.5    val is_prefix: ('a * 'a -> bool) -> 'a list -> 'a list -> bool
     1.6    val take_prefix: ('a -> bool) -> 'a list -> 'a list * 'a list
     1.7 +  val chop_prefix: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list * ('a list * 'b list)
     1.8    val take_suffix: ('a -> bool) -> 'a list -> 'a list * 'a list
     1.9    val prefixes1: 'a list -> 'a list list
    1.10    val prefixes: 'a list -> 'a list list
    1.11 @@ -751,6 +752,14 @@
    1.12              if  pred x  then  take(x :: rxs, xs)  else  (rev rxs, x :: xs)
    1.13    in  take([], xs)  end;
    1.14  
    1.15 +fun chop_prefix eq ([], ys) = ([], ([], ys))
    1.16 +  | chop_prefix eq (xs, []) = ([], (xs, []))
    1.17 +  | chop_prefix eq (xs as x::xs', ys as y::ys') =
    1.18 +      if eq (x, y) then
    1.19 +        let val (ps', xys'') = chop_prefix eq (xs', ys')
    1.20 +        in (x::ps', xys'') end
    1.21 +      else ([], (xs, ys));
    1.22 +
    1.23  (* [x1, ..., xi, ..., xn]  --->  ([x1, ..., xi], [x(i+1), ..., xn])
    1.24     where xi is the last element that does not satisfy the predicate*)
    1.25  fun take_suffix _ [] = ([], [])