module Collections ( module Collections, module Prelude
		   ) where

import Prelude hiding (
  -- basic functions
  last, (++), (!!), filter, minimum, maximum,
  elem, reverse, zip, seq, map, length, subtract, 
  -- continued operators
  sum, product, and, or, all, any, concat,
  -- on Streams
  iterate, repeat, cycle, take, drop, span, break,
  -- on Strings
  lines, words, unlines, unwords,
  -- Tools
  foldr, foldr1, scanr, scanr1,
  foldl, foldl1, scanl, scanl1,
  replicate
		      )
import qualified Prelude ( (++) )
import QuickCheck hiding ( Config(size) )
-- import Streams
-- import String  -- if Hugs would permit it

assert _ True exp = exp
assert s False _  = error ("assert: " ++ s)
-- A better version of this should be in Prelude.
-- Apparently the Haskell Committee was not interested in serious
-- program development.

-- Precedence 5 is the level of Prelude.++ and ancient (:).
infixl 5 <+>, ++, \/, /\, \+/
--   ^ 'l' is choosen to make them compatible with the next two.
infixl 5 \\, \-/
--   ^ Those two are not associative and (a \\ b \\ c) is interpreted
--   just like (a - b - c): from left to right.

-- Perhaps those should be on 9, just like (.).
infixr 5 /./, /., ./, °., .°, ° 

-- The next fixities are choosen such that the following parses well:
-- (Note that only one possible parse is well-typed.)
test_seq_fixity xs x = x <: x <: xs ++ xs >: x >: x

infixl 6 >: --, :>
infixr 6 <: --, :<
-- We just need to put them it on a different level than ++, and since
-- 4 is already so populated, I chose 6.  By the way, this makes the
-- following parse well.

prop_has_cons_snoc xs x = x # x<:xs
		       && x # xs>:x

infixr 5 -->    -- i.e. (a --> b --> c) = (a --> (b, c))
(-->) = (,) -- the Maplet constructor
-- or should this be "k --> x = single (k, x)" ?

infix 5 `has`, {-`elem`, `not_elem`,-} `subset`, `strict_subset`
infix 5        #     ,   /#      , <=#     , <#
-- Bind stronger than logical operators (== has 4; && and || are
-- below).  Note that `elem` in Prelude has 4, that's not good when
-- used with == and /= as logical equivalence and exclusive or.

infix 9 `at`, `image`, !!
-- Same as Prelude.!!.

( # ), ( /# ) :: ( Collection coll a ) => 
		 a -> coll a -> Bool
x # coll  = coll `has` x
x /# coll = not $ coll `has` x
-- elem = ( # )
-- not_elem = ( /# )
(<=#), (<#) :: ( OrderedSet set a ) =>
	       set a -> set a -> Bool
(<=#) = subset
(<#) = strict_subset

infix 4 <., .<, .<=, <=., <>., .<>.  

data Splitted coll a = Empty
		     | Single a
		     | (coll a) :+: (coll a)  deriving Eq

-- The :+: invariant.
prop_inner_nonempty coll = case split coll of
--	     	           (s :+: l) -> not (is_empty s)
--			             && not (is_empty l)
                           (Empty :+: _) -> False
			   (_ :+: Empty) -> False
			   (_)           -> True


-- ** Classes without testable specifications ** --

-- We cannot use a single-parameter type-class, since no Ordered
-- Collection could otherwise be an instance of this.  That's bad
-- news, indeed, but not my fault!

-- instance ( ... Ord a ... ) => OperationalCollection coll where
-- ERROR: undefined type-variable 'a' 

class OperationalCollection coll a
    where
    -- Primitive Constructors.
    empty :: coll a     
    single :: a -> coll a
    (<+>) :: coll a -> coll a -> coll a  -- read <+> as "join"

    -- The one and only basic query.
    split :: coll a -> Splitted coll a

    -- All other queries and modificators are defined via split.
    -- Functions that traverse the complete collection can often be
    -- defined indirectly be `fold`.
    size :: coll a -> Int
    is_empty :: coll a -> Bool

    size = fold 0 (const 1) (+)

    -- is_empty_spec coll = size coll == 0
    -- is_empty_spec' = reduce True (const (const False))
    is_empty coll = case split coll of
		    Empty -> True
		    _     -> False


    -- Queries on the ordering.
    -- (Skip implementations on first reading ;-).
    first,     last     :: coll a -> a      
    but_first, but_last :: coll a -> coll a 

    has_index   :: coll a -> Int -> Bool
    (!!)        :: coll a -> Int -> a       
    front, back :: coll a -> Int -> coll a  

    front_view :: coll a -> Maybe (a, coll a)
    back_view  :: coll a -> Maybe (coll a, a)

    first = reduce1 const
    last  = reduce1 (flip const)
{-- first coll = case split coll of
		 (Empty)    -> error "first.Precondition"
		 (Single x) -> x
		 (s :+: _)  -> first s

    last coll  = case split coll of
		 (Empty)    -> error "last.Precondition"
		 (Single x) -> x
		 (_ :+: l)  -> last l
--}
    but_first coll = case split coll of
		     (Empty)    -> error "but_first.Precondition"
		     (Single x) -> empty
		     (s :+: l)  -> but_first s <+> l

    but_last coll  = case split coll of
		     (Empty)    -> error "but_last.Precondition"
		     (Single x) -> empty
		     (s :+: l)  -> s <+> but_last l

    has_index c i  =  1 <= i && i <= size c

    coll !! i | not (has_index coll i) = error "(!!).Precondition"
	      | otherwise              = last $ front coll i

    -- Specification below
    front coll i | i <  0         = error "front.Precondition"
		 | i == 0         = empty
		 | size coll <= i = coll
                 -- assert: 1 <= i < size coll, meaning `coll` is a :+:
		 | size s <= i    = s <+> front l (i - size s)
		 | otherwise      = front s i
		 where
		 (s :+: l) = split coll

    back coll i  | i <  0         = error "back.Precondition"
		 | i == 0         = empty
		 | size coll <= i = coll
                 -- assert: 1 <= i < size coll, meaning `coll` is a :+:
		 | size l <= i    = back s (i - size l) <+> l
		 | otherwise      = back l i
		 where
		 (s :+: l) = split coll

    front_view coll | is_empty coll = Nothing
		    | otherwise     = Just (first coll, but_first coll)
    back_view coll  | is_empty coll = Nothing
		    | otherwise     = Just (but_last coll, last coll)
    -- To be replaced by pattern views with (:<), (:>).

    -- Higher-Order Kingdom
    fold   :: b -> (a -> b) -> (b -> b -> b) -> coll a -> b
    fold1  ::      (a -> b) -> (b -> b -> b) -> coll a -> b

    fold e f g coll | is_empty coll = e
		    | otherwise     = fold1 f g coll
    -- This makes use of the :+: invariant.				      

    fold1 f (*) coll = case split coll of
		       (Single x) -> f x
		       (s :+: l)  -> fold1 f (*) s  *  fold1 f (*) l

    apply   :: Collection coll b =>
	       (a -> b) -> coll a -> coll b
    filter  :: (a -> Bool) -> coll a -> coll a

    apply  f = apply' f
    filter p = fold empty (\x -> if p x then single x else empty) (<+>)

    -- Just for completeness.  In case anyone wants to instantiate
    -- this one feature instead of the basic three.
    unsplit :: Splitted coll a -> coll a
    unsplit (Empty)    = empty
    unsplit (Single x) = single x
    unsplit (s :+: l)  = s <+> l

    empty    = unsplit (Empty)
    single x = unsplit (Single x)
    s <+> l  = unsplit (s :+: l)

    zip_with :: (Collection coll b, Sequence seq' c) =>
		(a     -> b      -> c    ) ->
		coll a -> coll b -> seq' c
    zip :: (Collection coll b, Sequence seq' (a, b)) =>
	   coll a -> coll b -> seq' (a, b)
{-- With Views:
    zip_with (*) (x:<xs) (y:<ys) = x*y <: zip_with (*) xs ys
    zip_with (*) ( _ )   ( _ )   = empty

    -- Withough Views:
    zip_with (*) a b | is_empty a || is_empty b = empty
		     | otherwise = single (first a * first b) 
                                ++ zip_with (*) (but_first a)
				                (but_first b)
    -- With speed:
--}
    zip_with (*) a b | 0 < diff  = front a diff ** b
		     | otherwise = a ** front b diff
	where
	diff = size a - size b
	a ** b = case split a of
		 (Empty)    -> assert "Collections.zip.1" (is_empty b) $
			       empty
	         (Single x) -> assert "Collections.zip.2" (size b == 1)$
	                       single (x * first b)
		 (s :+: l)  -> (s ** front b (size s))
			   <+> (l ** back b  (size l))

    zip a b = zip_with (,) a b
--  zip_with f a b = apply (uncurry f) (zip a b)


{-- With Views...
front_spec (_)       0 = empty
front_spec (Empty)   _ = empty
front_spec (f :< bf) i = f <: front_spec bf (i-1)
--}
front_spec _     0  = empty
front_spec coll  _
    | is_empty coll = empty
front_spec coll  i  = first coll <: front_spec (but_first coll) (i-1)

back_spec _     0   = empty
back_spec coll  _
    | is_empty coll = empty
back_spec coll  i   = back_spec (but_last coll) (i-1) >: last coll

-- 'fold2' can easily be implemented like 'zip_with', but since I
-- don't want to repeat myself, I'll give a an implementation via
-- 'fold' on the first argument list.  This can be used later on for
-- the Collection fusion framework.  (Unfortunately it also has
-- running time O(N*log N) on balanced structures, since it uses the
-- 'front_view' of the second argument.)

fold2 :: ( Collection coll a, Collection coll' b ) =>
	 c -> (a -> b -> c) -> (c -> c -> c) ->
	 coll a -> coll' b -> c
{--
fold2 e f g a b = fst $ fold e' f' g' a $ b
    where
    e' xs = (e, xs)
    f' x xs | is_empty xs = (e, xs)
	    | otherwise   = (f x $ first xs, but_first xs)
    g' a b xs | is_empty xs = (e, xs)
	      | otherwise   = g'' (a xs) b
    g'' (c, xs) b | is_empty xs = (c, xs)
		  | otherwise   = g''' c (b xs)
    g''' c1 (c2, xs) = (g c1 c2, xs)

We can use the law
    fold e f (*) = foldr (\x y -> x * f y) e
to simplify a lot:
--}

fold2 e f g a b = foldr fg (const e) a $ b
    where
    fg x r ys = case front_view ys of
		(Nothing)      -> e
	        (Just (y, ys)) -> f x y `g` r ys

-- We have the obvious law:
--  zip_with f = fold2 empty (single.f) (<+>)
-- which suggests, that 'zip_with' should rather be called 'apply2'.


class ( OperationalCollection seq a
       ) => OperationalSequence seq a
    where
    -- Only adds modification of the explicit ordering.
    -- And a famous synonym for <+>.
    (++) :: seq a -> seq a -> seq a
    (++) = (<+>)

    (<:) :: a -> seq a -> seq a
    (>:) :: seq a -> a -> seq a
    -- For pattern matching: (:<) and (:>)
    -- Mnemonic: the tip points to the single element.

    x <: s = single x ++ s
    s >: x = s ++ single x
--  (++) = foldr (<:)
--  (++) = foldl (:>)

    length :: seq a -> Int
    length = size

    has_gap :: seq a -> Int -> Bool
    has_gap s i  =  1 <= i && i <= size s + 1

    insert_element :: seq a -> Int -> a -> seq a
    insert_segment :: seq a -> Int -> seq a -> seq a

    insert_element s i x
	| not (has_gap s i) = error "insert_element.Precondition"
        | otherwise = front s (i - 1) ++ single x ++ back s n
	where n = size s - i + 1

    insert_segment s i s'
	| not (has_gap s i) = error "insert_element.Precondition"
        | otherwise = front s (i - 1) ++ s' ++ back s n
	where n = size s - i + 1

    reverse :: seq a -> seq a
    reverse = fold empty single (flip (++))
    

-- ** Axioms for class Collection ** --

prop_empty_is_Empty = is_empty (empty :: [Int])

prop_single_is_Single x = split (single x :: [Int]) == (Single x)

-- Due to the definitions of `is_empty` and `size` above (which are
-- part of the specification), these equations fix the result of
-- `split` for the first two constructors.  These two axioms are also
-- implied by "split . unsplit == id", but this is surely too strong:
-- it would make all Collections isomorphic to leave trees and not
-- even allow associativity:

prop_join_associative a b c = (a <+> b) <+> c == a <+> (b <+> c) 

prop_empty_join_unit a = a <+> empty == a
		      && empty <+> a == a

-- Here the == must be understood in a strong logical sense: There is
-- no means to distinguish between two equal abstract values.  (See
-- "principles.html".) 

-- prop_dont_loose a b x = (a `has` x || b `has` x)
--		      ==> (a <+> b) `has` x
-- This property is untrue for Maps.


-- ** Collections ** --

class ( Eq (coll a), Eq a
      , OperationalCollection coll a
      ) => Collection coll a 
    where
    count :: coll a -> a -> Int
    has   :: coll a -> a -> Bool

{--  count coll x = fold 0 eq (+) coll
	where eq y | x == y    = 1
	           | otherwise = 0 
--}
    count coll x = size $ filter (==x) coll

    -- has coll x = count coll x > 0
    has coll x = not.is_empty $ filter (==x) coll
    -- Advantage of the second definition:
    -- It works also on Infinite Streams.

    {-- GHC 5.00 doesn't like the "Ord a" here.
    maximum, minimum :: Ord a => coll a -> a
    maximum = reduce1 max
    minimum = reduce1 min
    --}

    -- ** Point-wise Modification ** --
    remove :: coll a -> a -> coll a
    remove coll x = filter (/=x) coll
    -- (The implementation is more efficient on Ordered Collections.)
    -- On Bags this is not the inverse of `add`, see `subtract`.

    -- Sequences: (<:), (>:), insert_*, delete
    -- OrderedCollection: add, OrderedBag: subtract

-- Equality of Collections 
c_eq a b = size a == size b
        && fold2 True (==) (&&) a b
        -- and (zip_with (==) a b :: [Bool])

-- I opted against the version with the intermediate list, since that
-- would do some unsuitable calls to [].++ and then it would be slower
-- (O(N^2)) than a simple version via 'front_view' (O(N*log N)).



-- ** Derived Higher Order Functions ** --

reduce  :: (OperationalCollection coll a) =>
	   a -> (a -> a -> a) -> coll a -> a
reduce e = fold e id

reduce1 :: (OperationalCollection coll a) =>
	        (a -> a -> a) -> coll a -> a
reduce1  = fold1 id

apply'  :: ( OperationalCollection coll a
	   , OperationalCollection coll' b
	   ) => (a -> b) -> coll a -> coll' b
apply' f = fold empty (single . f) (<+>)


-- As a consequence of the axioms and the above definitions we get a
-- lot of the known laws of functional programming.  For example:
prop_fold_apply_fusion e f f' g xs = (fold e f g . apply f') xs
				     == (fold e (f . f') g :: [Int] -> Int) xs

-- And its consequence:
prop_reduce_apply_fusion e f g xs = (reduce e f . apply g) xs
				    == (fold e g f :: [Int] -> Int) xs

-- Special cases:
-- fold1 f g . apply f' == fold1 (f.f') g
-- reduce1 g . apply f  == fold1  f     g

-- We do use these laws to eliminate intermediate data structures not
-- only for efficiency (that could be done by the compiler), but also
-- to unambiguate types.


class ( Collection coll (a, b)
      , Eq a, Eq b
--    , Ord a, Ord b
      ) => AssociativeCollection coll a b
    where 
    domain :: Collection coll' a => coll (a, b) -> coll' a
    range  :: Collection coll' b => coll (a, b) -> coll' b

    domain = apply' fst
    range  = apply' snd

    image :: (OrderedSet set a, OrderedSet set b) =>
	     coll (a, b) -> set a -> set b
--  image rel set = [ y | (x, y) <- rel, x' <- set, x==x' ]
    image rel set = apply' snd $ filter ((set `has`).fst) $ rel
    -- A deforested version could be implemented like 'merge_with'...

    {-- Deforested:
    image rel set = fold empty f (<+>) rel
	where
	f (x, y) = if set `has` x then single y else empty
    --}

    inverse :: (AssociativeCollection coll' b a) =>
	       coll (a, b) -> coll' (b, a)
    inverse = apply' (\ (x, y) -> (y, x) )

    -- Composition operators are defined separately for Maps and
    -- Relations.  This avoids some type and semantic problems and
    -- gives clear definitions.  Otherwise it would be rather
    -- chaotic. 

    {-- Domain- and range- -restriction and -subtraction from B/Z
      language.  Perhaps not very useful, since B and Z use sets,
      where programmers use predicates anyway ... --}

    (<|), (<-|) :: OrderedSet set a =>
		   set a -> coll (a, b) -> coll (a, b)
    (|>), (|->) :: OrderedSet set b =>
		   coll (a, b) -> set b -> coll (a, b)

    set <|  rel = filter ((set`has`).fst) rel
    set <-| rel = filter (not.(set`has`).fst) rel

    rel |>  set = filter ((set`has`).snd) rel
    rel |-> set = filter (not.(set`has`).snd) rel


-- A consequence of the above definitions.  (Ambigous type.)
-- prop_range_is_image_of_domain a  =  range a == image a (domain a)


class ( Collection seq a
      , OperationalSequence seq a
      ) => Sequence seq a 

-- Sequences are ordered lexicographically (needed for Strings).
-- (Incidentally this corresponds to the derived EQ instance of [].)
seq_compare a b | is_empty a && is_empty b = EQ
		| is_empty a               = LT
		| is_empty b               = GT
seq_compare a b = case first a `compare` last a of
		  LT -> LT
		  GT -> GT
		  EQ -> but_first a `seq_compare` but_first b

-- In fact, we'ld better use "to_list a `compare' to_list b" since
-- 'to_list' is implemented via 'fold': it adapts to the form of the
-- concrete structure giving O(N) runtime, while this one will need
-- O(NlogN) on balanced structures.


-- These instances needed for compatibility and to use QuickCheck.
instance OperationalCollection [] a
    where 
    split ([])   = Empty
    split (x:[]) = Single x
    split (x:xs) = [x] :+: xs

    unsplit (Empty)     = []
    unsplit (Single x)  = [x]
    unsplit (xs :+: ys) = xs Prelude.++ ys

instance OperationalSequence [] a
instance Eq a => Collection [] a
instance Eq a => Sequence [] a

class (Collection coll a, Ord a
      ) => OrderedCollection coll a
    where
    ascending, descending :: (Sequence seq a) =>
			     coll a -> seq a
    ascending = seq
    descending = reverse . seq

    minimum, maximum :: coll a -> a
    but_min, but_max :: coll a -> coll a
    smallest, largest :: coll a -> Int -> coll a

    minimum = first
    maximum = last

    but_min = but_first
    but_max = but_last

    smallest = front
    largest = back

    -- still lacking: 'rank' (aka 'index_of') and 'predecessor',
    -- 'successor': how to specify them for Set/Map/Bag?

    smaller, larger, smaller_equal, larger_equal, equal
	:: coll a -> a -> coll a
    {-- spec:
    smaller       coll a = filter (<a) coll
    larger        coll a = filter (>a) coll
    smaller_equal coll a = filter (<=a) coll
    larger_equal  coll a = filter (>=a) coll
    equal         coll a = filter (==a) coll
    --}

    -- The following code works on all kind of ordered trees
    -- (NodeTree, DoubleNodeTree, Trie).  Explicit version...

    smaller coll a = case split coll of
		     (Empty)             -> coll
		     (Single x) | x < a  -> coll
				| True   -> empty
		     (s :+: l)  | a <. l -> smaller s a
			        | True   -> s <+> smaller l a 

    larger coll a  = case split coll of
		     (Empty)             -> coll
		     (Single x) | a < x  -> coll
			        | True   -> empty
		     (s :+: l)  | a <. l -> larger s a <+> l
			        | True   -> larger l a

    smaller_equal coll a = case split coll of
		     (Empty)             -> coll
		     (Single x) | x <= a -> coll
				| True   -> empty
		     (s :+: l)  | a <. l -> smaller_equal s a
			        | True   -> s <+> smaller_equal l a 

    larger_equal coll a = case split coll of
		     (Empty)             -> coll
		     (Single x) | a <= x -> coll
			        | True   -> empty
		     (s :+: l)  | a <. l -> larger_equal s a <+> l
			        | True   -> larger_equal l a

    equal coll a = case split coll of
		     (Empty)             -> coll
		     (Single x) | a == x -> coll
			        | True   -> empty
		     (s :+: l)  | a <. l -> equal s a <+> l
			        | True   -> equal l a

{-- Compressed version:

    order_filter small select coll a = o_f coll
	where o_f coll = case split coll of
	      (Empty)                        -> coll
	      (Single x) | select x          -> coll
			 | otherwise         -> empty
	      (s :+: l)  | small && (a <. l) -> o_f s
			 | small             -> s <+> o_f l
			 | a .< l            -> o_f l
			 | otherwise         -> o_f s <+> l

    smaller = order_filter True (<a)
    larger = order_filter False (>a)

    smaller_equal = order_filter True (<=a)
    larger_equal = order_filter False (>=a)

    equal = order_filter False (==a)
--}

{-- The following is code for DoubleNodeTrees.  Its advantage is that
    it doesn't descend to the leaves if the element is outside the
    Collection's range.  No idea whether it is really faster.
    Explicit version first ...

    smaller coll a | is_empty coll = coll
		   | coll .< a     = coll
		   | a <=. coll    = empty
	   -- "coll /= Single x" since otherwise "x < a && a <= x"
		   | otherwise     = smaller s a <+> smaller l a
		   where (s :+: l) = split coll

    larger coll a  | is_empty coll = coll
		   | a <. coll     = coll
		   | coll .<= a    = empty
		   | otherwise     = larger s a <+> larger l a
		   where (s :+: l) = split coll

    smaller_equal coll a | is_empty coll = coll
			 | coll .<= a    = coll
			 | a <. coll     = empty
			 | otherwise     = smaller_equal s a
					<+>smaller_equal l a
			 where (s :+: l) = split coll

    larger_equal coll a  | is_empty coll = coll
			 | a <=. coll    = coll
			 | coll .<= a    = empty
			 | otherwise     = larger_equal s a
				        <+>larger_equal l a
			 where (s :+: l) = split coll


    equal coll a | a <>. coll               = empty
		 | a <=. coll && coll .<= a = coll
	         | otherwise                = equal s a <+> equal l a
			 where (s :+: l) = split coll

    -- Compressed version:

    order_filter :: coll a -> (coll a -> Bool) -> (coll a -> Bool) -> coll a
    order_filter coll take leave = o_f coll
	where o_f c | is_empty c = c
		    | take c     = c
		    | leave c    = empty
		    | otherwise  = o_f s <+> o_f l
		    where (s :+: l) = split coll

    smaller coll a = order_filter coll (.<a) (a<=.)
    smaller_equal coll a = order_filter coll (.<=a) (a<.)

    larger  coll a = order_filter coll (a<.) (.<=a)
    larger_equal  coll a = order_filter coll (a<=.) (.<a)
    --}

    (.<), (.<=) :: coll a -> a -> Bool
    (<.), (<=.) :: a -> coll a -> Bool
    (<>.)  :: a      -> coll a -> Bool
    (.<>.) :: coll a -> coll a -> Bool

    x <. c  = is_empty c || x < minimum c
    c .< x  = is_empty c || maximum c < x
    x <=. c = is_empty c || x <= minimum c
    c .<= x = is_empty c || maximum c <= x

    x <>. c = x <. c || c .< x
    a .<>. b = is_empty a || is_empty b
	     || maximum a < minimum b || maximum b < minimum a

-- The default implementation of (<.) .. (.<>.) are constant-time on
-- Balanced Trees, while Tries will provide their own constant-time
-- implementations (albeit with the weaker specification given below).
-- The bottom line is that any tree can provide this in constant time
-- (even if it can't do constant-time 'minimum', 'maximum'), so that
-- we can rely on these functions when implementing other functions --
-- even as elementary ones as <+>!

prop_tree_less_spec    coll x = x <. coll ==> x < minimum coll
prop_tree_greater_spec coll x = coll .< x ==> maximum coll < x

-- And the important consequence:
prop_ordered_has coll x = (x <>. coll) ==> not (coll `has` x)


{-- Ordered Collections' notion of ordering is expressed by the
    following axiom:

    split_ordered :: (OrderedCollection coll a) => coll a -> Bool
    split_ordered a = case split a of
                      (s :+: l) -> and [ x <= y | x <- s, y <- l ]
                      _         -> True
--}

-- Ordered Collections allow the efficient implementation of some of
-- Collection's operations.  Until Haskell supports overwriting
-- default definitions (see my proposal), we'll use the following
-- hack:

{-- The following code works efficiently on all kinds of search trees
  (NodeTree, DoubleNodeTree, Trie), it is also the most efficient on
  simple NodeTrees, since it does very little comparisons.
--}

o_has coll x = case split coll of
	       (Empty)    -> False
	       (Single y) -> x==y
	       (s :+: l) | x <. l    -> o_has s x
			 | otherwise -> o_has l x

o_count coll x = case split coll of
		 (Empty)    -> 0
		 (Single y) -> if x==y then 1 else 0
		 (s :+: l) | x <. l    -> o_count s x
			   | x <=. l   -> o_count s x + o_count l x 
			   -- ^ needed for bags.
			   | otherwise -> o_count l x

o_remove coll x = case split coll of
		  (Empty)    -> coll
		  (Single y) -> if x==y then empty else coll
		  (s :+: l) | x <. l    -> o_remove s x
			    | x <=. l   -> o_remove s x <+> o_remove l x
			    -- ^ needed for bags.
			    | otherwise -> o_remove l x

-- Instances are invited to use those functions (as in "has = o_has"
-- etc.). 

{-- Here is the version of the code for DoubleNodeTrees.  No idea
  whether it is really more efficient than the general version...

o_has coll x | is_empty coll  = False
	     | x <. coll      = False
	     | coll .< x      = False
	     | size coll == 1 = True
	     | otherwise      = o_has s x || o_has l x
	     where (s :+: l) = split coll

o_count coll x | is_empty coll = 0
	       | x <. coll     = 0
	       | coll .< x     = 0
	       | otherwise     = case split coll of
			     (Single y) -> 1 -- since this is the min/max
			     (s :+: l)  -> o_count s x + o_count l x

o_remove coll x | is_empty coll = coll
	        | x <. coll     = coll
	        | coll .< x     = coll
	        | otherwise     = case split coll of
		 	      (Single y) -> empty
			      (s :+: l)  -> o_remove s x <+> o_remove l x

And here for Tries: we can do the .< <. test in one go, but we have to
check the leaves explicitly:

o_has coll x | x <>. coll = False
             | otherwise  = case split coll of
 	       (Single y) -> x==y
	       (s :+: l)  -> o_has s x || o_has l x

o_count coll x | x <>. coll = 0
               | otherwise  = case split coll of
	         (Single y) -> if x==y then 1 else 0
	         (s :+: l)  -> o_count s x + o_count l x

o_remove coll x | x <>. coll = coll
                | otherwise  = case split coll of
		  (Single y) -> if x==y then empty else coll
		  (s :+: l)  -> o_remove s x <+> o_remove l x
--}

class ( OrderedCollection coll a
      ) => CommutativeCollection coll a
    where
    add :: coll a -> a -> coll a
    add coll a = coll <+> single a
--  (<+>) = foldr add

    merge_with :: (coll a -> coll a -> b) ->
		  (a -> b) ->
		  (b -> b -> b) ->
		  coll a -> coll a -> b
    merge_with = merge_with'

prop_union_commutative a b  =  a <+> b == b <+> a

merge_with' :: ( CommutativeCollection coll a
	       , CommutativeCollection coll' a
	       ) => (coll a -> coll' a -> b) ->  -- dis
	            (a -> b) ->                  -- eq
		    (b -> b -> b) ->             -- (*)
		    coll a -> coll' a -> b
merge_with' dis eq (*) a b
    | a .<>. b         = a `dis` b
    | size a <= size b = case split b of
		         (Single x)  -> eq x
			 (bs :+: bl) -> mw as bs * mw al bl
			    where as = smaller a (first bl)
			          al = larger_equal a (first bl)
    | otherwise        = case split a of
			 (Single x)  -> eq x
		         (as :+: al) -> mw as bs * mw al bl
			    where bs = smaller b (first al)
			          bl = larger_equal b (first al)
    where
    mw = merge_with' dis eq (*)
    a .<>. b = is_empty a || is_empty b
	     || maximum a < minimum b
	     || maximum b < minimum a
{--
  - Can't rely on the class .<>., since we need a more polymorphic
    one. 

  - Code duplication needed to avoid polymorphic recursion.
--}

cc_eq a b = size a == size b
	  && merge_with both_empty (const True) (&&) a b
    where 
    both_empty a b = is_empty a && is_empty b


class (CommutativeCollection bag a) => OrderedBag bag a where
    (\+/), (\-/) :: bag a -> bag a -> bag a
    (\+/) = (<+>)
    (\-/) = merge_with (const) (const empty) (<+>)
	             -- ^ take first ^ take none

    -- 'subbag', 'strict_subbag' (if anyone wants them) would have the
    -- same implementations as for Sets. 

    subtract :: bag a -> a -> bag a
    subtract bag a = bag \-/ single a

    bag_map :: OrderedMap map a Int =>
	       bag a -> map (a, Int)
    map_bag :: OrderedMap map a Int =>
	       map (a, Int) -> bag a

--  bag_map b = fun_map (set b) (count b)
    -- Deforested:
    bag_map b = apply' ( \ x -> (x, count b x) ) b
 
--  map_bag = join . apply' (uncurry $ flip replicate)
    -- Deforested:
    map_bag = fold empty ( \ (x, n) -> replicate n x ) (\+/)


prop_bag_union_commutative a b  =  a \+/ b == b \+/ a

-- The difference to Sets is simply that we don't have idempotence of
-- union, which thus gives us a slightly stronger notion of
-- equivalence.  It's lower bound is:

prop_bag_add a b x  =  (a \+/ b) `count` x 
                    == a `count` x  +  b `count` x

-- Definition of subtraction:

prop_sub a b x  =  (a \-/ b) `count` x 
                == (a `count` x) -. (b `count` x)
    where i -. j = 0 `max` (i - j)

class (CommutativeCollection set a) => OrderedSet set a where
    (\/), (/\), (\\) :: set a -> set a -> set a
    (\/) = (<+>)

    (/\) = merge_with (const (const empty)) (single)      (<+>)
                    -- ^ take none           ^ take it  
    (\\) = merge_with (const)               (const empty) (<+>)
                    -- ^ take left           ^ drop it

    subset, strict_subset, disjoint :: set a -> set a -> Bool

--  a `subset` b        = all (b `has`) a
    a `strict_subset` b = size a <  size b && a `subset` b
--  a `disjoint` b      = a /\ b == empty

    -- With "M = size a" and "N = size b" this is O(M*log N) and the
    -- following is O(M `min` N):
    a `subset` b = size a <= size b -- Heuristic optimisation.
                && merge_with (\a b -> is_empty a) (const True) (&&) a b

    disjoint = merge_with (\a b -> True) (\eq -> False) (&&)    

    rank :: set a -> a -> Int
--  pre_rank set a = set `has` a
--  prop_rank set a = set `has` a ==>
--                    set !! set `rank` a == a
    rank set a = size $ smaller_equal set a

prop_union_idempotent set  =  set \/ set == set

-- This upper bound on equality matches the lower bound given by
-- `dont_loose`.  By consequence, OrderedSets are the "weakest" of our
-- data structures.

-- Here is a trivial consequence from the axiom:
prop_at_most_one a x  =  a `count` x <= 1

-- Overwriting default methods:
set_count set x = if set `has` x then 1 else 0

class ( OrderedCollection map (a, b)
      , AssociativeCollection map a b
      , Ord a
      ) => OrderedMap map a b
    where
    (<+) :: map (a, b) -> map (a, b) -> map (a, b)
    (<+) = (<+>)
	 
    fun_map :: (OrderedSet set a) =>
               (set a) -> (a -> b) -> map (a, b)
    fun_map dom f = apply' ( \ x -> (x, f x) ) dom 	   

    has_key :: map (a, b) -> a -> Bool  -- maybe call it `domain_has`
--  has_key = has . domain
    has_key coll k = case split coll of
		     (Empty)          -> False
		     (Single (k', _)) -> k==k'
		     (s :+: l) | k < k'    -> has_key s k
			       | otherwise -> has_key l k
			       where (k', _) = first l

    -- Perhaps use (!) for `at`.
    at         :: map (a, b) -> a -> b
    put        :: map (a, b) -> a -> b -> map (a, b)
    delete_key :: map (a, b) -> a      -> map (a, b)
    update     :: map (a, b) -> a -> (b -> b) -> map (a, b)

    at map k = snd $ first $ key_equal map k
    put map k x = map <+ single (k, x)
--  (<+) = foldr (curry . put)
    delete_key map k = key_smaller map k <+ key_larger map k
    update map k f = put map k $ f $ map `at` k

{-- Same asymptotical performance:   
    at map k = case split map of
	       (Single (k', x)) -> assert "Collections.at" (k'==k)
				   x
	       (s :+: l) | k < k'    -> at s k
			 | otherwise -> at l k
			 where (k', _) = minimum l

    put map k x = let tip = single (k, x) in
		  case split map of
		  (Empty)                        -> tip
		  (Single s@(k', _)) | k' == k   -> tip
				     | otherwise -> single s <+> tip
		  (s :+: l)          | k < k'    -> put s k x <+> l
				     | otherwise -> s <+> put l k x
				     where (k', _) = minimum l

    delete_key map k = case split map of
		(Empty) -> empty
		(Single s@(k', _)) | k' == k   -> empty
		 		   | otherwise -> single s
		(s :+: l)          | k < k'    -> delete_key s k <+> l
				   | otherwise -> s <+> delete_key l k
				   where (k', _) = minimum l
--}

    key_rank :: map (a, b) -> a -> Int
--  pre_key_rank map a = map `has` a
--  prop_key_rank map a = map `has` a
--                     ==> map !! map `rank` a == a
    key_rank map a = size $ key_smaller_equal map a

    -- Map composition operators.

    (/./) :: (OrderedMap map c a, OrderedMap map c b) =>
	     map (a, b) -> map (c, a) -> map (c, b)
    (./)  :: (OrderedMap map a c) =>
	     (b -> c)   -> map (a, b) -> map (a, c)

    (/.)  :: map (a, b) -> (c -> a)   -> (c -> b)
    map /. f = (at map) . f

--  (.)   :: (a -> b)   -> (c -> a)   -> (c -> b)

--  apply :: ((a, b) -> (c, d)) 
--           -> map (a, b) -> map (c, d)

    map_apply :: (OrderedMap map a c) =>
		 ((a, b) -> c) -> map (a, b) -> map (a, c)
    map_apply f = apply ( \ (a, b) -> (a, f (a, b)) )
    -- Instances will overwrite this one to make all the others
    -- efficient. 

    f    ./ map = map_apply (f . snd) map

    map /./ map' = (at map) ./ map'

    map_merge_with :: (map (a, b) -> map (a, b) -> c) -> -- dis
	  	      ((a, b) -> (a, b) -> c) ->         -- eq
		      (c -> c -> c) ->                   -- (*)
		      map (a, b) -> map (a, b) -> c
    map_merge_with = map_merge_with'

    key_smaller, key_smaller_equal, key_larger, key_larger_equal, key_equal 
	:: map (a, b) -> a -> map (a, b)
    {-- spec:
    key_smaller coll a = filter ((<a).fst) coll
    key_larger  coll a = filter ((>a).fst) coll
    key_equal   coll a = filter ((==a).fst) coll
    key_smaller_equal coll a = filter ((<=a).fst) coll
    key_larger_equal  coll a = filter ((>=a).fst) coll
    --}

    key_smaller coll a = case split coll of
		(Empty)                 -> coll
		(Single x) | fst x < a  -> coll
			   | otherwise  -> empty
		(s :+: l)  | a <.. l    -> key_smaller s a
			   | otherwise  -> s <+> key_smaller l a 

    key_larger  coll a  = case split coll of
		(Empty)                 -> coll
		(Single x) | a < fst x  -> coll
			   | otherwise  -> empty
		(s :+: l)  | a <.. l    -> key_larger s a <+> l
			   | otherwise  -> key_larger l a

    key_smaller_equal coll a = case split coll of
		(Empty)                 -> coll
		(Single x) | fst x <= a -> coll
			   | otherwise  -> empty
		(s :+: l)  | a <.. l    -> key_smaller_equal s a
			   | otherwise  -> s <+> key_smaller_equal l a

    key_larger_equal coll a = case split coll of
		(Empty)                 -> coll
		(Single x) | a <= fst x -> coll
			   | otherwise  -> empty
		(s :+: l)  | a <.. l    -> key_larger_equal s a <+> l
			   | otherwise  -> key_larger_equal l a

    key_equal coll a = case split coll of
		(Empty)                 -> coll
		(Single x) | a == fst x -> coll
			   | otherwise  -> empty
		(s :+: l)  | a <.. l    -> key_equal s a <+> l
			   | otherwise  -> key_equal l a

a <.. l = a < first_key l

last_key  coll = fst $ last coll 
first_key coll = fst $ first coll 

map_merge_with' :: (OrderedMap map a b, OrderedMap map' a d) =>
		   (map (a, b) -> map' (a, d) -> c) ->
                   ((a, b) -> (a, d) -> c) ->
		   (c -> c -> c) ->
		   map (a, b) -> map' (a, d) -> c
map_merge_with' dis eq (*) a b
    | a .<>. b         = a `dis` b
    | size b <= size a = case split a of
	 (Single x)  -> x `eq` y
	                where (Single y) = split b
 	 (as :+: al) -> mmw as bs * mmw al bl 
  		where
                bs = key_smaller b (first_key al)
		bl = key_larger_equal b (first_key al)

    | otherwise        = case split b of
	 (Single y)  -> x `eq` y
	                where (Single x) = split a
 	 (bs :+: bl) -> mmw as bs * mmw al bl 
  		where
                as = key_smaller a (first_key bl)
		al = key_larger_equal a (first_key bl)
    where
    mmw = map_merge_with' dis eq (*)
    a .<>. b = is_empty a || is_empty b
	    || last_key a < first_key b
	    || last_key b < first_key a


map_join_with :: ( OrderedMap map a b ) =>
		 (a -> b -> b -> b ) ->
		 map (a, b) -> map (a, b) -> map (a, b)
-- | Like <+, only that 'f' handles the elements of equal keys.
--   If your 'f' doesn't need the key, prefix it with 'cons'.
--   E.g. (<<+) = map_join_with (const min)
map_join_with f = map_merge_with (<+) f' (<+)
    where
    f' (a, b) (_, b') = single (a, f a b b')

-- A helper function I once needed.
map_by :: (Collection coll b, OrderedMap map a b) =>
	  (b -> a) -> coll b -> map (a, b)
map_by f = apply' (\x -> (f x, x))

-- Overwriting defaults...
map_eq a b = size a == size b
	   && map_merge_with both_empty values_eq (&&) a b
    where
    both_empty a b = is_empty a && is_empty b
    values_eq x y = snd x == snd y


class ( OrderedSet rel (a, b)
      , AssociativeCollection rel a b
      ) => OrderedRelation rel a b
    where
    -- Like 'at' on a relation. 
    -- (Perhaps call it 'sat' or give it a symbol.)
    single_image :: (OrderedSet set b) =>
		    rel (a, b) -> a -> set b
--  single_image rel x = rel `image` single x

    -- Since 'set' need not be an instance of "OrderedSet set a" we
    -- deforest once:
--  single_image rel x = [ y | (x', y) <- rel, x'==x ]
    single_image rel x = apply' snd $ filter ((==x).fst) rel

    (°)  :: (OrderedRelation rel c a, OrderedRelation rel c b) =>
	    rel (a, b) -> rel (c, a) -> rel (c, b)

    (.°) :: (OrderedRelation rel a c) =>
	    (b -> c) -> rel (a, b) -> rel (a, c)

    (°.) :: (OrderedSet set b) =>
	    rel (a, b) -> (c -> a) -> (c -> set b)

    -- Semantics:

--  a ° b = [(x, z) | (x, y) <- b, (y', z) <- a, y==y' ]
    a ° b = join_apply ( \ (x, y) ->
                         join_apply ( \ (y', z) ->
                                      if y==y' then single (x, z)
                                               else empty
                                    ) a
                       ) b
    -- This has time O(N*M), but with an optimised
    -- 'single_image' at hand, we can do in O(N * log M):

{-- a ° b = [ (x, z) | (x, y) <- b, z <- a `single_image` y ]
    a ° b = join_apply ( \ (x, y) -> apply' (\z -> (x, z))
			                    (a `single_image` y)
		       ) b
    -- Since Relations are ordered by the domain first, we cannot
    -- "split the larger" to yield a time like that of 'merge_with'. 
    -- (At least this allows us a simple default implementation,
    -- instead ofgoing into the guts every time...)

Unfortunately the result of 'single_image' is an ambigous Set, that we
can't deforest easily... have to wait for a better day...
--}


    f .° rel  =  apply' (\ (x, y) -> (x, f y) ) rel
    -- Composition of a relation with a function is the same as
    -- applying the function on the range.  (Like for Maps, incidentally.) 

    rel °. f  =  \x -> rel `single_image` f x
    -- Composition of a function with a relation yields a function.
    -- We could also write:
--  rel °. f = single_image rel . f

{-- To compose a Map 'm' with a Relation 'rel' simply write:

>   set m ° rel
>   rel ° set m

    This has a well-defined type and also makes clear that the
    semantics used is that of Relations and the result is of course a
    relation. 
--}


-- ** Conversion Functions ** --

convert :: (Collection coll a, Collection coll' a) =>
	   coll a -> coll' a
convert = fold empty single (<+>)
{-# RULES "convert/id" convert = id #-}

set :: (Collection coll a, OrderedSet set a) =>
       coll a -> set a
set = convert

bag :: (Collection coll a, OrderedBag bag a) =>
       coll a -> bag a
bag = convert

seq :: (Collection coll a, Sequence seq a) =>
       coll a -> seq a
seq = convert

map :: (Collection coll (a, b), OrderedMap map a b) =>
       coll (a, b) -> map (a, b)
map = convert

seq_map :: ( Sequence seq a, Sequence seq Int, Sequence seq (Int, a)
	   , OrderedMap map Int a) =>
       seq a -> map (Int, a)
seq_map = map . zip' (seq [1..])
    where
    zip' :: (Sequence seq a, Sequence seq b, Sequence seq (a, b)) =>
            seq a -> seq b -> seq (a, b) 
    zip' = zip
{-- Deforested
seq_map = sm 1
    where
    sm _ (Empty) = empty
    sm i (x:<xs) = single (i, x) <+ sm (i+1) xs

TODO: Is there a version that is both efficient and has no constraints
on intermediate types? 
 --}

------------------------------------------------------------------

-- Some operators can be "continued" (or "lifted", or "generalised" to
-- Sequences or Collections.  In the proposed standard those functions
-- will be defined together with the operator, but since I can't fuzz
-- around in Prelude I put them all here.

-- ** on Bool ** --

and, or :: Collection coll Bool => coll Bool -> Bool
and = reduce True  (&&)
or  = reduce False (||)

any, all :: Collection coll a
	    => (a -> Bool) -> coll a -> Bool

any_spec p = or . apply p
any p = fold False p (||)

all_spec p = and . apply p
all p = fold True p (&&)


-- ** on Numeric ** --

sum, product :: (Num a, Collection coll a) =>
		coll a -> a
sum     = reduce 0 (+)
product = reduce 1 (*)


-- ** on Collection ** --

join :: (Collection coll a, Collection coll' (coll a)) =>
	coll' (coll a) -> coll a
join = reduce empty (<+>)
-- Having different type variables here is very important: E.g., we
-- can join a Sequence of Sets.  It also makes Collection
-- Comprehension with different Collection Types possible.

join_apply :: (Collection coll b, Collection coll' a) =>
	      (a -> coll b) -> coll' a -> coll b
join_apply_spec f = join . apply f
join_apply f = fold empty f (<+>)
-- Here we have used the example law 'prop_reduce_apply_fusion'.

-- apply f = join_apply ( single . f )
-- filter p = join_apply ( \x -> if x then single x else empty )

concat :: (Sequence seq a, Sequence seq' (seq a)) =>
          seq' (seq a) -> seq a
concat = reduce empty (<+>)
-- It makes no sense to concat a Collection of Sequences, since the
-- explicit order of the result would be influenced by the possibly
-- implicit order of the Collection.

concat_apply :: (Sequence seq b, Sequence seq' a) =>
	      (a -> seq b) -> seq' a -> seq b
concat_apply_spec f = concat . apply f
concat_apply f = fold empty f (<+>)

union, intersect :: (OrderedSet set a, Collection coll (set a)) =>
		    coll (set a) -> set a
union = reduce empty (\/)
intersect = reduce empty (/\)


-- ** on Monad ** --

-- Those functions have to change their names, since Sequence and Map
-- now mean different things.  The following names are just a
-- proposal... 

sequence_actions :: (Monad m, Collection coll (m a), Collection coll a) =>
		    coll (m a) -> m (coll a)
{-- old style (front-biased)
sequence_actions cs = case front_view cs of
	              (Nothing)      -> return empty
	              (Just (c, cs)) -> do x  <- c
	                                   xs <- sequence_actions cs
	                                   return (x <: xs) 

sequence_actions' = foldr f (return empty)
    where
    f c cs = c >>= \x-> cs >>= \xs-> return (x <: xs)
--}

-- new style (associative)
sequence_actions = fold (return empty)
	                (>>= (return . single))
		        (\a b -> a >>= \x ->
			         b >>= \y ->
			         return (x <+> y)
			)

sequence_actions_ :: (Monad m, Collection coll (m a)) =>
		     coll (m a) -> m ()
sequence_actions_ = foldr (>>) (return ())


-- The functions formerly known as 'mapM' and 'mapM_' have taken names
-- consistent with other reduce-apply-fusioned functions.

sequence_apply :: (Monad m, Collection coll a, Collection coll b) =>
		  (a -> m b) -> coll a -> m (coll b)

sequence_apply_spec f = sequence . apply f

sequence_apply f = fold (return empty)
		        (\x -> f x >>= (return . single))
			--     ^ here's the little change ;-)
			(\a b -> a >>= \x ->
	                         b >>= \y ->
		                 return (x <+> y)
			)

sequence_apply_ :: (Monad m, Collection coll a) =>
		   (a -> m b) -> coll a -> m ()

sequence_apply__spec f = sequence_actions_ . apply f

sequence_apply_ f = foldr ((>>).f) (return ())



-- 'foldr', `replicate`: Logically they belong to CollectionTools,
-- but they are already used here.

foldr f e coll = fold id f (.) coll e


replicate_pre n _ = n >= 0
replicate_spec 0 _ = empty
replicate_spec n x = single x <+> replicate_spec (n-1) x

-- An implementation with more sharing
-- (assumed <+> doesn't copy its arguments). 
replicate 0 _ = empty
replicate n x = rep (single x) n
    where
    rep coll 1 = coll
    rep coll n = rep coll n2 <+> rep coll (n - n2)
	where n2 = n `div` 2