pringletons (empty) → 0.1.0.0

raw patch · 6 files changed

+1797/−0 lines, 6 filesdep +aesondep +basedep +hashablesetup-changed

Dependencies added: aeson, base, hashable, singletons, template-haskell, text, unordered-containers, vector

Files

• LICENSE +30/−0
• Setup.hs +2/−0
• pringletons.cabal +50/−0
• src/Data/Case/Enumerate.hs +32/−0
• src/Data/Singletons/Class.hs +272/−0
• src/Data/Singletons/Map.hs +1411/−0

@@ -0,0 +1,30 @@+Copyright Andrew Martin (c) 2016++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Andrew Martin nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

@@ -0,0 +1,50 @@+name:                pringletons+version:             0.1.0.0+synopsis:            Classes and data structures complementing the singletons library+description:         Please see README.md+homepage:            https://github.com/andrewthad/pringletons+license:             BSD3+license-file:        LICENSE+author:              Andrew Martin+maintainer:          andrew.thaddeus@gmail.com+copyright:           2016 Andrew Martin+category:            web+build-type:          Simple+cabal-version:       >=1.10++library+  hs-source-dirs:      src+  exposed-modules:+    Data.Singletons.Map+    Data.Singletons.Class+    Data.Case.Enumerate+  build-depends:       +      base >= 4.7 && < 5+    , hashable+    , singletons+    , aeson+    , text+    , vector+    , unordered-containers+    , template-haskell+  default-language:    Haskell2010+  default-extensions:+    TypeOperators+    InstanceSigs+    KindSignatures+    DataKinds+    TypeFamilies+    GADTs+    ExistentialQuantification+    PolyKinds+    ScopedTypeVariables+    DeriveGeneric+    RankNTypes+    GeneralizedNewtypeDeriving+    StandaloneDeriving+    DefaultSignatures+    BangPatterns++source-repository head+  type:     git+  location: https://github.com/andrewthad/pringletons

@@ -0,0 +1,32 @@+module Data.Case.Enumerate +  ( enumerateConstructors+  ) where++import Language.Haskell.TH+import Control.Monad++{-| This will create a pattern match on the first argument+    that splices in the third argument for each pattern.+    Example:++ > data Color = Red | Blue | Green deriving Show+ > myFunc :: Color -> String+ > myFunc c = $(enumerateConstructors 'c ''Color =<< [|show c|])++   I should fix this function to actually make it work that+   way. It actually uses the singletonized data type instead.+-}++enumerateConstructors :: Name -> Name -> Exp -> Q Exp+enumerateConstructors vname name expr = do+  TyConI (DataD _ _ _ ctors _) <- reify name+  matches <- forM ctors $ \(NormalC cname args) -> case args of+    [] -> return $ Match (ConP (sketchyNameSingletonize cname) []) (NormalB expr) []+    _ -> fail "constConstructors2: empty data constructor required"+  return $ CaseE (VarE vname) matches++sketchyNameSingletonize :: Name -> Name+sketchyNameSingletonize = id+  . mkName . ('S':) . reverse +  . takeWhile (/= '.') . reverse . show+

@@ -0,0 +1,272 @@+{-# LANGUAGE FlexibleContexts #-}++module Data.Singletons.Class +  ( +  -- * Singleton Classes+  -- $singletonClasses+    EqSing1(..)+  , EqSing2(..)+  , OrdSing1(..)+  , OrdSing2(..)+  , HashableSing1(..)+  , HashableSing2(..)+  , ToJSONSing1(..)+  , ToJSONSing2(..)+  , FromJSONSing1(..)+  , FromJSONSing2(..)+  -- * Kind classes+  -- $kindClasses+  , ShowKind(..)+  , ReadKind(..)+  , HashableKind(..)+  , ToJSONKind(..)+  , FromJSONKind(..)+  , ToJSONKeyKind(..)+  , FromJSONKeyKind(..)+  -- * Data types+  , Applied1(..)+  , Applied2(..)+  , Applied3(..)+  , SomeSingWith1(..)+  , SomeSingWith1'+  , SomeSingWith2(..)+  , SomeSingWith2'+  -- * Classes for Applied+  -- $appliedClasses+  , EqApplied1(..)+  , HashableApplied1(..)+  , ToJSONApplied1(..)+  , FromJSONApplied1(..)+  -- * Functions+  , showKind+  , readMaybeKind+  ) where++import Data.Hashable+import Data.Maybe+import Data.Singletons+import Data.Singletons.Prelude+import Data.Singletons.Decide+import Data.Text (Text)+import Data.Functor.Identity+import Text.Read (readMaybe)+import qualified Data.Text as Text+import qualified Data.Aeson as Aeson+import qualified Data.Aeson.Types as Aeson+import Data.Type.Equality+import Data.Aeson (FromJSON(..),ToJSON(..))+import Data.Proxy+import Control.Arrow (first)+import qualified Data.Vector as Vector+import Data.Function ((&))++{- $singletonClasses+ + These are singleton variants of the commonly used classes from @base@, + @hashable@, and @aeson@. These variants work on higher-kinded types instead+ of on ground types. For example, if you wrote the following:++ > data MyType = MyInt | MyBool | MyChar+ > $(genSingletons [''MyType])+ > type family Interpret m where+ >   Interpret 'MyInt  = Int+ >   Interpret 'MyChar = Char+ >   Interpret 'MyBool = Bool+ > newtype MyValue x = MyValue { getMyValue :: Interpret x }++ You could then write @MyValue@ instances for all of the classes that in this+ module that end in @Sing1@. For example:++ > instance EqSing1 MyValue where+ >   eqSing1 x a b = case x of+ >     SMyInt  -> a == b+ >     SMyChar -> a == b+ >     SMyBool -> a == b++ For our example @MyValue@ type, the @EqSing1@ instance is trivial. We simply + pattern match on the singleton and then do the same thing in each case. This+ kind of pattern matching ends up happening any time our universe + interpreter maps to types that all have @Eq@ instances. Since writing this+ out is tedious, we can instead use a template haskell function provided in+ the @Data.Case.Enumerate@ module:++ > instance EqSing1 MyValue where+ >   eqSing1 x a b $(enumerateConstructors 'x ''MyValue =<< [|a == b|])++ Instances for the other classes here can be written similarly.++-}++class EqSing1 f where+  eqSing1 :: Sing a -> f a -> f a -> Bool++class EqSing2 f where+  eqSing2 :: Sing a -> Sing b -> f a b -> f a b -> Bool++class EqSing1 f => OrdSing1 f where+  compareSing1 :: Sing a -> f a -> f a -> Ordering++class EqSing2 f => OrdSing2 f where+  compareSing2 :: Sing a -> Sing b -> f a b -> f a b -> Ordering++class HashableSing1 f where+  hashWithSaltSing1 :: Sing a -> Int -> f a -> Int++class HashableSing2 f where+  hashWithSaltSing2 :: Sing a -> Sing b -> Int -> f a b -> Int++class ToJSONSing1 f where+  toJSONSing1 :: Sing a -> f a -> Aeson.Value++class ToJSONSing2 f where+  toJSONSing2 :: Sing a -> Sing b -> f a b -> Aeson.Value++class FromJSONSing1 f where+  parseJSONSing1 :: Sing a -> Aeson.Value -> Aeson.Parser (f a)++class FromJSONSing2 f where+  parseJSONSing2 :: Sing a -> Sing b -> Aeson.Value -> Aeson.Parser (f a b)++{- $kindClasses+ + These are kind classes. They express that something is true for all + singletons of a particular kind. Note that these are different from the+ kind classes provided in the @singletons@ library itself. The methods+ in those classes ('SOrd','SEnum',etc.) work entirely on singletons. Here,+ the methods also work with normal data types.++ Notice that classes like @EqKind@ and @OrdKind@ have been omitted from + this library. The reason is that that functions that would be provided by+ these can be trivially recovered by demoting the results of methods in 'SEq'+ and 'SOrd'.++ These methods in these classes all have defaults that involve demoting the+ singleton and using the corresponding method from the normal typeclass.+-}++class (kproxy ~ 'KProxy) => ShowKind (kproxy :: KProxy a) where+  showsPrecKind :: Int -> Sing (x :: a) -> ShowS+  default showsPrecKind :: (SingKind kproxy, Show (DemoteRep kproxy)) => Int -> Sing (x :: a) -> ShowS+  showsPrecKind i s xs = showsPrec i (fromSing s) xs++class (kproxy ~ 'KProxy) => ReadKind (kproxy :: KProxy a) where+  readsPrecKind :: Int -> ReadS (SomeSing kproxy)+  default readsPrecKind :: (SingKind kproxy, Read (DemoteRep kproxy)) => Int -> ReadS (SomeSing kproxy)+  readsPrecKind i s = map (first toSing) (readsPrec i s)++class (kproxy ~ 'KProxy) => HashableKind (kproxy :: KProxy a) where+  hashWithSaltKind :: Int -> Sing (x :: a) -> Int+  default hashWithSaltKind :: (SingKind kproxy, Hashable (DemoteRep kproxy)) => Int -> Sing (x :: a) -> Int+  hashWithSaltKind i s = hashWithSalt i (fromSing s)++class (kproxy ~ 'KProxy) => ToJSONKind (kproxy :: KProxy a) where+  toJSONKind :: Sing (x :: a) -> Aeson.Value+  default toJSONKind :: ShowKind kproxy => Sing (x :: a) -> Aeson.Value+  toJSONKind s = Aeson.String (Text.pack (showKind s))++class (kproxy ~ 'KProxy) => FromJSONKind (kproxy :: KProxy a) where+  parseJSONKind :: Aeson.Value -> Aeson.Parser (SomeSing kproxy)++class (kproxy ~ 'KProxy) => ToJSONKeyKind (kproxy :: KProxy a) where+  toJSONKeyKind :: Sing (x :: a) -> Text+  default toJSONKeyKind :: ShowKind kproxy => Sing (x :: a) -> Text+  toJSONKeyKind s = Text.pack (showKind s)++class (kproxy ~ 'KProxy) => FromJSONKeyKind (kproxy :: KProxy a) where+  parseJSONKeyKind :: Text -> Aeson.Parser (SomeSing kproxy)+  default parseJSONKeyKind :: ReadKind kproxy => Text -> Aeson.Parser (SomeSing kproxy)+  parseJSONKeyKind t = let s = Text.unpack t in +    case readMaybeKind s of+      Nothing -> fail ("Could not parse key " ++ s)+      Just a -> return a++------------------------+-- Data Types+------------------------+newtype Applied1 (f :: TyFun k * -> *) (a :: k) =+  Applied1 { getApplied1 :: Apply f a }++newtype Applied2 (f :: TyFun k (TyFun j * -> *) -> *) (a :: k) (b :: j) =+  Applied2 { getApplied2 :: Apply (Apply f a) b }++newtype Applied3 (f :: TyFun k (TyFun j (TyFun l * -> *) -> *) -> *) (a :: k) (b :: j) (c :: l) =+  Applied3 { getApplied3 :: Apply (Apply (Apply f a) b) c }++data SomeSingWith1 (kproxy :: KProxy k) (f :: k -> *) where+  SomeSingWith1 :: Sing a -> f a -> SomeSingWith1 'KProxy f++type SomeSingWith1' = SomeSingWith1 'KProxy++data SomeSingWith2 (kproxy1 :: KProxy k) (kproxy2 :: KProxy j) (f :: k -> j -> *) where+  SomeSingWith2 :: Sing a -> Sing b -> f a b -> SomeSingWith2 'KProxy 'KProxy f++type SomeSingWith2' = SomeSingWith2 'KProxy 'KProxy++{- $appliedClasses+ + These are additional classes used to provide instances for 'Applied1'.+ If you have a defunctionalized typeclass that provides produces types+ in the category hask, you can use this. Instances will often look like+ this:++ > data Thing = ...+ > type family ToType (x :: Thing) :: * where ...+ > instance EqApplied1 ToTypeSym0 where+ >   eqApplied1 _ x (Applied a) (Applied b) = $(enumerateConstructors 'x ''Thing =<< [|a == b|])++-}+class EqApplied1 (f :: TyFun k * -> *) where+  eqApplied1 :: proxy f -> Sing a -> Apply f a -> Apply f a -> Bool++class HashableApplied1 (f :: TyFun k * -> *) where+  hashWithSaltApplied1 :: proxy f -> Sing a -> Int -> Apply f a -> Int++class ToJSONApplied1 (f :: TyFun k * -> *) where+  toJSONApplied1 :: proxy f -> Sing a -> Apply f a -> Aeson.Value++class FromJSONApplied1 (f :: TyFun k * -> *) where+  parseJSONApplied1 :: proxy f -> Sing a -> Aeson.Value -> Aeson.Parser (Apply f a)+++------------------------+-- A bunch of instances+------------------------++instance EqApplied1 f => EqSing1 (Applied1 f) where+  eqSing1 s (Applied1 a) (Applied1 b) = eqApplied1 (Proxy :: Proxy f) s a b++instance ToJSONApplied1 f => ToJSONSing1 (Applied1 f) where+  toJSONSing1 s (Applied1 a) = toJSONApplied1 (Proxy :: Proxy f) s a++instance FromJSONApplied1 f => FromJSONSing1 (Applied1 f) where+  parseJSONSing1 s v = fmap Applied1 (parseJSONApplied1 (Proxy :: Proxy f) s v)++instance HashableApplied1 f => HashableSing1 (Applied1 f) where+  hashWithSaltSing1 s i (Applied1 a) = hashWithSaltApplied1 (Proxy :: Proxy f) s i a++instance (EqSing1 f, SDecide kproxy) => Eq (SomeSingWith1 kproxy f) where+  SomeSingWith1 s1 v1 == SomeSingWith1 s2 v2 = +    case testEquality s1 s2 of+      Nothing -> False+      Just Refl -> eqSing1 s1 v1 v2++instance (ToJSONKind kproxy1, ToJSONKind kproxy2, ToJSONSing2 f) => ToJSON (SomeSingWith2 kproxy1 kproxy2 f) where+  toJSON (SomeSingWith2 s1 s2 v) = +    toJSON [toJSONKind s1, toJSONKind s2, toJSONSing2 s1 s2 v]++instance FromJSON (SomeSingWith2 kproxy1 kproxy2 f) where+  parseJSON = error "from json somesingwith2: write this"++instance (HashableKind kproxy1, HashableSing1 f) => Hashable (SomeSingWith1 kproxy1 f) where+  hashWithSalt i (SomeSingWith1 s v) = i+    & flip hashWithSaltKind s +    & flip (hashWithSaltSing1 s) v++showKind :: forall (kproxy :: KProxy k) (a :: k). ShowKind kproxy => Sing a -> String+showKind x = showsPrecKind 0 x ""++readMaybeKind :: ReadKind kproxy => String -> Maybe (SomeSing kproxy)+readMaybeKind s = listToMaybe +  $ mapMaybe (\(a,x) -> if null x then Just a else Nothing) +  $ readsPrecKind 0 s+

@@ -0,0 +1,1411 @@+{-| This is a dependent version of the @Data.Map@ module from @containers@.+ +    This module was largely copied from the @dependent-map@ package.+-}+module Data.Singletons.Map where++import Data.Singletons+import Data.Singletons.Decide+import Data.Singletons.Prelude+import Data.Type.Equality+import Data.Typeable+import Data.Singletons.Class+import Data.Maybe+import Prelude hiding (null, lookup)+import qualified Data.HashMap.Strict as HashMap+import Data.Aeson+import Data.Aeson.Types (Parser)+import Data.Text (Text)+import Data.Hashable++data SingMap (kproxy :: KProxy j) (f :: j -> *) where+    Tip :: SingMap kproxy f+    Bin :: {- sz    -} !Int+        -> {- key   -} !(Sing v)+        -> {- value -} !(f v)+        -> {- left  -} !(SingMap kproxy f)+        -> {- right -} !(SingMap kproxy f)+        -> SingMap kproxy f++type SingMap' = SingMap 'KProxy++instance (SEq kproxy, SDecide kproxy, EqSing1 f) => Eq (SingMap kproxy f) where+  t1 == t2 = (size t1 == size t2) && (toAscList t1 == toAscList t2)++instance (HashableKind kproxy, HashableSing1 f) => Hashable (SingMap kproxy f) where+  hashWithSalt i m = hashWithSalt i (toAscList m)++instance (ToJSONKeyKind kproxy, ToJSONSing1 f) => ToJSON (SingMap kproxy f) where+  toJSON = Object . foldrWithKey (\s f -> HashMap.insert (toJSONKeyKind s) (toJSONSing1 s f)) HashMap.empty++instance (SOrd kproxy, SDecide kproxy, FromJSONKeyKind kproxy, FromJSONSing1 f) => FromJSON (SingMap kproxy f) where+  parseJSON = withObject "SingMap kproxy a" $ fmap fromList . mapM parseSingWith . HashMap.toList+    where +    parseSingWith :: (Text,Value) -> Parser (SomeSingWith1 kproxy f)+    parseSingWith (t,v) = do+      SomeSing s :: SomeSing kproxy  <- parseJSONKeyKind t+      pv <- parseJSONSing1 s v+      return (SomeSingWith1 s pv)+      +++{--------------------------------------------------------------------+  Construction+--------------------------------------------------------------------}++-- | /O(1)/. The empty map.+--+-- > empty      == fromList []+-- > size empty == 0+empty :: SingMap kproxy f+empty = Tip++-- | /O(1)/. A map with a single element.+--+-- > singleton 1 'a'        == fromList [(1, 'a')]+-- > size (singleton 1 'a') == 1+singleton :: Sing v -> f v -> SingMap kproxy f+singleton k x = Bin 1 k x Tip Tip++{--------------------------------------------------------------------+  Query+--------------------------------------------------------------------}++-- | /O(1)/. Is the map empty?+null :: SingMap kproxy f -> Bool+null Tip    = True+null Bin{}  = False++-- | /O(1)/. The number of elements in the map.+size :: SingMap kproxy f -> Int+size Tip                = 0+size (Bin n _ _ _ _)    = n++-- | /O(log n)/. Lookup the value at a key in the map.+--+-- The function will return the corresponding value as @('Just' value)@,+-- or 'Nothing' if the key isn't in the map.+lookup :: forall kproxy f v. (SOrd kproxy, SDecide kproxy) => Sing v -> SingMap kproxy f -> Maybe (f v)+lookup k = k `seq` go+  where+  go :: SingMap kproxy f -> Maybe (f v)+  go Tip = Nothing+  go (Bin _ kx x l r) = +    case sCompare k kx of+      SLT -> go l+      SGT -> go r+      SEQ -> case testEquality k kx of+        Nothing -> error "lookup: inconsistent SOrd and SDecide instances"+        Just Refl -> Just x++lookupAssoc :: forall kproxy f v. (SOrd kproxy, SDecide kproxy) => SomeSing kproxy -> SingMap kproxy f -> Maybe (SomeSingWith1 kproxy f)+lookupAssoc (SomeSing k) = k `seq` go+  where+  go :: SingMap kproxy f -> Maybe (SomeSingWith1 kproxy f)+  go Tip = Nothing+  go (Bin _ kx x l r) =+    case sCompare k kx of+      SLT -> go l+      SGT -> go r+      SEQ -> case testEquality k kx of+        Nothing -> error "lookupAssoc: inconsistent SOrd and SDecide instances"+        Just Refl -> Just (SomeSingWith1 kx x)+{--------------------------------------------------------------------+  Utility functions that maintain the balance properties of the tree.+  All constructors assume that all values in [l] < [k] and all values+  in [r] > [k], and that [l] and [r] are valid trees.+  +  In order of sophistication:+    [Bin sz k x l r]  The type constructor.+    [bin k x l r]     Maintains the correct size, assumes that both [l]+                      and [r] are balanced with respect to each other.+    [balance k x l r] Restores the balance and size.+                      Assumes that the original tree was balanced and+                      that [l] or [r] has changed by at most one element.+    [combine k x l r] Restores balance and size. ++  Furthermore, we can construct a new tree from two trees. Both operations+  assume that all values in [l] < all values in [r] and that [l] and [r]+  are valid:+    [glue l r]        Glues [l] and [r] together. Assumes that [l] and+                      [r] are already balanced with respect to each other.+    [merge l r]       Merges two trees and restores balance.++  Note: in contrast to Adam's paper, we use (<=) comparisons instead+  of (<) comparisons in [combine], [merge] and [balance]. +  Quickcheck (on [difference]) showed that this was necessary in order +  to maintain the invariants. It is quite unsatisfactory that I haven't +  been able to find out why this is actually the case! Fortunately, it +  doesn't hurt to be a bit more conservative.+--------------------------------------------------------------------}++{--------------------------------------------------------------------+  Combine+--------------------------------------------------------------------}+combine :: (SOrd kproxy, SDecide kproxy) => Sing v -> f v -> SingMap kproxy f -> SingMap kproxy f -> SingMap kproxy f+combine kx x Tip r  = insertMin kx x r+combine kx x l Tip  = insertMax kx x l+combine kx x l@(Bin sizeL ky y ly ry) r@(Bin sizeR kz z lz rz)+  | delta*sizeL <= sizeR  = balance kz z (combine kx x l lz) rz+  | delta*sizeR <= sizeL  = balance ky y ly (combine kx x ry r)+  | otherwise             = bin kx x l r+++-- insertMin and insertMax don't perform potentially expensive comparisons.+insertMax,insertMin :: Sing v -> f v -> SingMap kproxy f -> SingMap kproxy f+insertMax kx x t+  = case t of+      Tip -> singleton kx x+      Bin _ ky y l r+          -> balance ky y l (insertMax kx x r)+             +insertMin kx x t+  = case t of+      Tip -> singleton kx x+      Bin _ ky y l r+          -> balance ky y (insertMin kx x l) r+             +{--------------------------------------------------------------------+  [merge l r]: merges two trees.+--------------------------------------------------------------------}+merge :: SOrd kproxy => SingMap kproxy f -> SingMap kproxy f -> SingMap kproxy f+merge Tip r   = r+merge l Tip   = l+merge l@(Bin sizeL kx x lx rx) r@(Bin sizeR ky y ly ry)+  | delta*sizeL <= sizeR = balance ky y (merge l ly) ry+  | delta*sizeR <= sizeL = balance kx x lx (merge rx r)+  | otherwise            = glue l r++{--------------------------------------------------------------------+  [glue l r]: glues two trees together.+  Assumes that [l] and [r] are already balanced with respect to each other.+--------------------------------------------------------------------}+glue :: (kproxy ~ 'KProxy) => SingMap kproxy f -> SingMap kproxy f -> SingMap kproxy f+glue Tip r = r+glue l Tip = l+glue l r   +  | size l > size r = case deleteFindMax l of (SomeSingWith1 km m,l') -> balance km m l' r+  | otherwise       = case deleteFindMin r of (SomeSingWith1 km m,r') -> balance km m l r'++-- | /O(log n)/. Delete and find the minimal element.+--+-- > deleteFindMin (fromList [(5,"a"), (3,"b"), (10,"c")]) == ((3,"b"), fromList[(5,"a"), (10,"c")]) +-- > deleteFindMin                                            Error: can not return the minimal element of an empty map++deleteFindMin :: (kproxy ~ 'KProxy) => SingMap kproxy f -> (SomeSingWith1 kproxy f, SingMap kproxy f)+deleteFindMin t +  = case t of+      Bin _ k x Tip r -> (SomeSingWith1 k x ,r)+      Bin _ k x l r   -> let (km,l') = deleteFindMin l in (km,balance k x l' r)+      Tip             -> (error "Map.deleteFindMin: can not return the minimal element of an empty map", Tip)++-- | /O(log n)/. Delete and find the maximal element.+--+-- > deleteFindMax (fromList [(5,"a"), (3,"b"), (10,"c")]) == ((10,"c"), fromList [(3,"b"), (5,"a")])+-- > deleteFindMax empty                                      Error: can not return the maximal element of an empty map++deleteFindMax :: (kproxy ~ 'KProxy) => SingMap kproxy f -> (SomeSingWith1 kproxy f, SingMap kproxy f)+deleteFindMax t+  = case t of+      Bin _ k x l Tip -> (SomeSingWith1 k x,l)+      Bin _ k x l r   -> let (km,r') = deleteFindMax r in (km,balance k x l r')+      Tip             -> (error "Map.deleteFindMax: can not return the maximal element of an empty map", Tip)+++{--------------------------------------------------------------------+  [balance l x r] balances two trees with value x.+  The sizes of the trees should balance after decreasing the+  size of one of them. (a rotation).++  [delta] is the maximal relative difference between the sizes of+          two trees, it corresponds with the [w] in Adams' paper.+  [ratio] is the ratio between an outer and inner sibling of the+          heavier subtree in an unbalanced setting. It determines+          whether a double or single rotation should be performed+          to restore balance. It is correspondes with the inverse+          of $\alpha$ in Adam's article.++  Note that:+  - [delta] should be larger than 4.646 with a [ratio] of 2.+  - [delta] should be larger than 3.745 with a [ratio] of 1.534.+  +  - A lower [delta] leads to a more 'perfectly' balanced tree.+  - A higher [delta] performs less rebalancing.++  - Balancing is automatic for random data and a balancing+    scheme is only necessary to avoid pathological worst cases.+    Almost any choice will do, and in practice, a rather large+    [delta] may perform better than smaller one.++  Note: in contrast to Adam's paper, we use a ratio of (at least) [2]+  to decide whether a single or double rotation is needed. Allthough+  he actually proves that this ratio is needed to maintain the+  invariants, his implementation uses an invalid ratio of [1].+--------------------------------------------------------------------}+delta,ratio :: Int+delta = 4+ratio = 2++balance :: Sing v -> f v -> SingMap kproxy f -> SingMap kproxy f -> SingMap kproxy f+balance k x l r+  | sizeL + sizeR <= 1    = Bin sizeX k x l r+  | sizeR >= delta*sizeL  = rotateL k x l r+  | sizeL >= delta*sizeR  = rotateR k x l r+  | otherwise             = Bin sizeX k x l r+  where+    sizeL = size l+    sizeR = size r+    sizeX = sizeL + sizeR + 1++-- rotate+rotateL :: Sing v -> f v -> SingMap kproxy f -> SingMap kproxy f -> SingMap kproxy f+rotateL k x l r@(Bin _ _ _ ly ry)+  | size ly < ratio*size ry = singleL k x l r+  | otherwise               = doubleL k x l r+rotateL _ _ _ Tip = error "rotateL Tip"++rotateR :: Sing v -> f v -> SingMap kproxy f -> SingMap kproxy f -> SingMap kproxy f+rotateR k x l@(Bin _ _ _ ly ry) r+  | size ry < ratio*size ly = singleR k x l r+  | otherwise               = doubleR k x l r+rotateR _ _ Tip _ = error "rotateR Tip"++-- basic rotations+singleL, singleR :: Sing v -> f v -> SingMap kproxy f -> SingMap kproxy f -> SingMap kproxy f+singleL k1 x1 t1 (Bin _ k2 x2 t2 t3)  = bin k2 x2 (bin k1 x1 t1 t2) t3+singleL _ _ _ Tip = error "singleL Tip"+singleR k1 x1 (Bin _ k2 x2 t1 t2) t3  = bin k2 x2 t1 (bin k1 x1 t2 t3)+singleR _ _ Tip _ = error "singleR Tip"++doubleL, doubleR :: Sing v -> f v -> SingMap kproxy f -> SingMap kproxy f -> SingMap kproxy f+doubleL k1 x1 t1 (Bin _ k2 x2 (Bin _ k3 x3 t2 t3) t4) = bin k3 x3 (bin k1 x1 t1 t2) (bin k2 x2 t3 t4)+doubleL _ _ _ _ = error "doubleL"+doubleR k1 x1 (Bin _ k2 x2 t1 (Bin _ k3 x3 t2 t3)) t4 = bin k3 x3 (bin k2 x2 t1 t2) (bin k1 x1 t3 t4)+doubleR _ _ _ _ = error "doubleR"++{--------------------------------------------------------------------+  The bin constructor maintains the size of the tree+--------------------------------------------------------------------}+bin :: Sing v -> f v -> SingMap kproxy f -> SingMap kproxy f -> SingMap kproxy f+bin k x l r+  = Bin (size l + size r + 1) k x l r++{--------------------------------------------------------------------+  Utility functions that return sub-ranges of the original+  tree. Some functions take a comparison function as argument to+  allow comparisons against infinite values. A function [cmplo k]+  should be read as [compare lo k].++  [trim cmplo cmphi t]  A tree that is either empty or where [cmplo k == LT]+                        and [cmphi k == GT] for the key [k] of the root.+  [filterGt cmp t]      A tree where for all keys [k]. [cmp k == LT]+  [filterLt cmp t]      A tree where for all keys [k]. [cmp k == GT]++  [split k t]           Returns two trees [l] and [r] where all keys+                        in [l] are <[k] and all keys in [r] are >[k].+  [splitLookup k t]     Just like [split] but also returns whether [k]+                        was found in the tree.+--------------------------------------------------------------------}++{--------------------------------------------------------------------+  [trim lo hi t] trims away all subtrees that surely contain no+  values between the range [lo] to [hi]. The returned tree is either+  empty or the key of the root is between @lo@ and @hi@.+--------------------------------------------------------------------}+trim :: SOrd kproxy => (SomeSing kproxy -> Ordering) -> (SomeSing kproxy -> Ordering) -> SingMap kproxy f -> SingMap kproxy f+trim _     _     Tip = Tip+trim cmplo cmphi t@(Bin _ kx _ l r)+  = case cmplo (SomeSing kx) of+      LT -> case cmphi (SomeSing kx) of+              GT -> t+              _  -> trim cmplo cmphi l+      _  -> trim cmplo cmphi r+              +trimLookupLo :: (SOrd kproxy, SDecide kproxy) => SomeSing kproxy -> (SomeSing kproxy -> Ordering) -> SingMap kproxy f -> (Maybe (SomeSingWith1 kproxy f), SingMap kproxy f)+trimLookupLo _  _     Tip = (Nothing,Tip)+trimLookupLo lo cmphi t@(Bin _ kx x l r)+  = case compareSome lo (SomeSing kx) of+      LT -> case cmphi (SomeSing kx) of+              GT -> (lookupAssoc lo t, t)+              _  -> trimLookupLo lo cmphi l+      GT -> trimLookupLo lo cmphi r+      EQ -> (Just (SomeSingWith1 kx x),trim (compareSome lo) cmphi r)+++{--------------------------------------------------------------------+  [filterGt k t] filter all keys >[k] from tree [t]+  [filterLt k t] filter all keys <[k] from tree [t]+--------------------------------------------------------------------}+filterGt :: (SOrd kproxy, SDecide kproxy) => (SomeSing kproxy -> Ordering) -> SingMap kproxy f -> SingMap kproxy f+filterGt cmp = go+  where+    go Tip              = Tip+    go (Bin _ kx x l r) = case cmp (SomeSing kx) of+              LT -> combine kx x (go l) r+              GT -> go r+              EQ -> r++filterLt :: (SOrd kproxy, SDecide kproxy) => (SomeSing kproxy -> Ordering) -> SingMap kproxy f -> SingMap kproxy f+filterLt cmp = go+  where+    go Tip              = Tip+    go (Bin _ kx x l r) = case cmp (SomeSing kx) of+          LT -> go l+          GT -> combine kx x l (go r)+          EQ -> l++----------------------------------------------------------------+----------------------------------------------------------------+-- Stuff that is, for some reason, in the non-internal module.+----------------------------------------------------------------+----------------------------------------------------------------++{--------------------------------------------------------------------+  Operators+--------------------------------------------------------------------}+infixl 9 !,\\ --++-- | /O(log n)/. Find the value at a key.+-- Calls 'error' when the element can not be found.+--+-- > fromList [(5,'a'), (3,'b')] ! 1    Error: element not in the map+-- > fromList [(5,'a'), (3,'b')] ! 5 == 'a'++(!) :: (SOrd kproxy, SDecide kproxy) => SingMap kproxy f -> Sing v -> f v+(!) m k    = find k m++-- | Same as 'difference'.+(\\) :: (SOrd kproxy, SDecide kproxy) => SingMap kproxy f -> SingMap kproxy f -> SingMap kproxy f+m1 \\ m2 = difference m1 m2++{--------------------------------------------------------------------+  Query+--------------------------------------------------------------------}++-- | /O(log n)/. Is the key a member of the map? See also 'notMember'.+member :: forall (kproxy :: KProxy k) f (v :: k). (SOrd kproxy, SDecide kproxy) => Sing v -> SingMap kproxy f -> Bool+member k = isJust . lookup k++-- | /O(log n)/. Is the key not a member of the map? See also 'member'.+notMember :: forall (kproxy :: KProxy k) f (v :: k). (SOrd kproxy, SDecide kproxy) => Sing v -> SingMap kproxy f -> Bool+notMember k m = not (member k m)++-- | /O(log n)/. Find the value at a key.+-- Calls 'error' when the element can not be found.+-- Consider using 'lookup' when elements may not be present.+find :: (SOrd kproxy, SDecide kproxy) => Sing v -> SingMap kproxy f -> f v+find k m = case lookup k m of+    Nothing -> error "SingMap.find: element not in the map"+    Just v  -> v++-- | /O(log n)/. The expression @('findWithDefault' def k map)@ returns+-- the value at key @k@ or returns default value @def@+-- when the key is not in the map.+findWithDefault :: (SOrd kproxy, SDecide kproxy) => f v -> Sing v -> SingMap kproxy f -> f v+findWithDefault def k m = case lookup k m of+    Nothing -> def+    Just v  -> v++{--------------------------------------------------------------------+  Insertion+--------------------------------------------------------------------}++-- | /O(log n)/. Insert a new key and value in the map.+-- If the key is already present in the map, the associated value is+-- replaced with the supplied value. 'insert' is equivalent to+-- @'insertWith' 'const'@.+insert :: forall kproxy f v. (SOrd kproxy, SDecide kproxy) => Sing v -> f v -> SingMap kproxy f -> SingMap kproxy f+insert kx x = kx `seq` go+    where+        go :: SingMap kproxy f -> SingMap kproxy f+        go Tip = singleton kx x+        go (Bin sz ky y l r) = case sCompare kx ky of+            SLT -> balance ky y (go l) r+            SGT -> balance ky y l (go r)+            SEQ -> Bin sz kx x l r++-- | /O(log n)/. Insert with a function, combining new value and old value.+-- @'insertWith' f key value mp@ +-- will insert the entry @key :=> value@ into @mp@ if key does+-- not exist in the map. If the key does exist, the function will+-- insert the entry @key :=> f new_value old_value@.+insertWith :: (SOrd kproxy, SDecide kproxy) => (f v -> f v -> f v) -> Sing v -> f v -> SingMap kproxy f -> SingMap kproxy f+insertWith f = insertWithKey (\_ x' y' -> f x' y')++-- | Same as 'insertWith', but the combining function is applied strictly.+-- This is often the most desirable behavior.+insertWith' :: (SOrd kproxy, SDecide kproxy) => (f v -> f v -> f v) -> Sing v -> f v -> SingMap kproxy f -> SingMap kproxy f+insertWith' f = insertWithKey' (\_ x' y' -> f x' y')++-- | /O(log n)/. Insert with a function, combining key, new value and old value.+-- @'insertWithKey' f key value mp@ +-- will insert the entry @key :=> value@ into @mp@ if key does+-- not exist in the map. If the key does exist, the function will+-- insert the entry @key :=> f key new_value old_value@.+-- Note that the key passed to f is the same key passed to 'insertWithKey'.+insertWithKey :: forall kproxy f v. (SOrd kproxy, SDecide kproxy) => (Sing v -> f v -> f v -> f v) -> Sing v -> f v -> SingMap kproxy f -> SingMap kproxy f+insertWithKey f kx x = kx `seq` go+  where+    go :: SingMap kproxy f -> SingMap kproxy f+    go Tip = singleton kx x+    go (Bin sy ky y l r) =+        case sCompare kx ky of+            SLT -> balance ky y (go l) r+            SGT -> balance ky y l (go r)+            SEQ -> unifyOnCompareEQ kx ky (Bin sy kx (f kx x y) l r)++-- | Same as 'insertWithKey', but the combining function is applied strictly.+insertWithKey' :: forall kproxy f v. (SOrd kproxy, SDecide kproxy) => (Sing v -> f v -> f v -> f v) -> Sing v -> f v -> SingMap kproxy f -> SingMap kproxy f+insertWithKey' f kx x = kx `seq` go+  where+    go :: SingMap kproxy f -> SingMap kproxy f+    go Tip = singleton kx $! x+    go (Bin sy ky y l r) =+        case sCompare kx ky of+            SLT -> balance ky y (go l) r+            SGT -> balance ky y l (go r)+            SEQ -> unifyOnCompareEQ kx ky (let x' = f kx x y in seq x' (Bin sy kx x' l r))++-- | /O(log n)/. Combines insert operation with old value retrieval.+-- The expression (@'insertLookupWithKey' f k x map@)+-- is a pair where the first element is equal to (@'lookup' k map@)+-- and the second element equal to (@'insertWithKey' f k x map@).+insertLookupWithKey :: forall kproxy f v. (SOrd kproxy, SDecide kproxy) => (Sing v -> f v -> f v -> f v) -> Sing v -> f v -> SingMap kproxy f+                    -> (Maybe (f v), SingMap kproxy f)+insertLookupWithKey f kx x = kx `seq` go+  where+    go :: SingMap kproxy f -> (Maybe (f v), SingMap kproxy f)+    go Tip = (Nothing, singleton kx x)+    go (Bin sy ky y l r) =+        case sCompare kx ky of+            SLT -> let (found, l') = go l+                  in (found, balance ky y l' r)+            SGT -> let (found, r') = go r+                  in (found, balance ky y l r')+            SEQ -> unifyOnCompareEQ kx ky (Just y, Bin sy kx (f kx x y) l r)++-- | /O(log n)/. A strict version of 'insertLookupWithKey'.+insertLookupWithKey' :: forall kproxy f v. (SOrd kproxy, SDecide kproxy) => (Sing v -> f v -> f v -> f v) -> Sing v -> f v -> SingMap kproxy f+                     -> (Maybe (f v), SingMap kproxy f)+insertLookupWithKey' f kx x = kx `seq` go+  where+    go :: SingMap kproxy f -> (Maybe (f v), SingMap kproxy f)+    go Tip = x `seq` (Nothing, singleton kx x)+    go (Bin sy ky y l r) =+        case sCompare kx ky of+            SLT -> let (found, l') = go l+                  in (found, balance ky y l' r)+            SGT -> let (found, r') = go r+                  in (found, balance ky y l r')+            SEQ -> unifyOnCompareEQ kx ky (let x' = f kx x y in x' `seq` (Just y, Bin sy kx x' l r))++{--------------------------------------------------------------------+  Deletion+  [delete] is the inlined version of [deleteWith (\k x -> Nothing)]+--------------------------------------------------------------------}++-- | /O(log n)/. Delete a key and its value from the map. When the key is not+-- a member of the map, the original map is returned.+delete :: forall (kproxy :: KProxy k) f (v :: k). (SOrd kproxy, SDecide kproxy) => Sing v -> SingMap kproxy f -> SingMap kproxy f+delete k = k `seq` go+  where+    go :: SingMap kproxy f -> SingMap kproxy f+    go Tip = Tip+    go (Bin _ kx x l r) =+        case sCompare k kx of+            SLT -> balance kx x (go l) r+            SGT -> balance kx x l (go r)+            SEQ -> unifyOnCompareEQ k kx (glue l r)++-- | /O(log n)/. Update a value at a specific key with the result of the provided function.+-- When the key is not+-- a member of the map, the original map is returned.+adjust :: (SOrd kproxy, SDecide kproxy) => (f v -> f v) -> Sing v -> SingMap kproxy f -> SingMap kproxy f+adjust f = adjustWithKey (\_ x -> f x)++-- | /O(log n)/. Adjust a value at a specific key. When the key is not+-- a member of the map, the original map is returned.+adjustWithKey :: (SOrd kproxy, SDecide kproxy) => (Sing v -> f v -> f v) -> Sing v -> SingMap kproxy f -> SingMap kproxy f+adjustWithKey f = updateWithKey (\k' x' -> Just (f k' x'))++-- | /O(log n)/. The expression (@'update' f k map@) updates the value @x@+-- at @k@ (if it is in the map). If (@f x@) is 'Nothing', the element is+-- deleted. If it is (@'Just' y@), the key @k@ is bound to the new value @y@.+update :: (SOrd kproxy, SDecide kproxy) => (f v -> Maybe (f v)) -> Sing v -> SingMap kproxy f -> SingMap kproxy f+update f = updateWithKey (\_ x -> f x)++-- | /O(log n)/. The expression (@'updateWithKey' f k map@) updates the+-- value @x@ at @k@ (if it is in the map). If (@f k x@) is 'Nothing',+-- the element is deleted. If it is (@'Just' y@), the key @k@ is bound+-- to the new value @y@.+updateWithKey :: forall kproxy f v. (SOrd kproxy, SDecide kproxy) => (Sing v -> f v -> Maybe (f v)) -> Sing v -> SingMap kproxy f -> SingMap kproxy f+updateWithKey f k = k `seq` go+  where+    go :: SingMap kproxy f -> SingMap kproxy f+    go Tip = Tip+    go (Bin sx kx x l r) =+        case sCompare k kx of+           SLT -> balance kx x (go l) r+           SGT -> balance kx x l (go r)+           SEQ -> unifyOnCompareEQ k kx $ case f kx x of+                   Just x' -> Bin sx kx x' l r+                   Nothing -> glue l r++-- | /O(log n)/. Lookup and update. See also 'updateWithKey'.+-- The function returns changed value, if it is updated.+-- Returns the original key value if the map entry is deleted. +updateLookupWithKey :: forall kproxy f v. (SOrd kproxy, SDecide kproxy) => (Sing v -> f v -> Maybe (f v)) -> Sing v -> SingMap kproxy f -> (Maybe (f v), SingMap kproxy f)+updateLookupWithKey f k = k `seq` go+ where+   go :: SingMap kproxy f -> (Maybe (f v), SingMap kproxy f)+   go Tip = (Nothing,Tip)+   go (Bin sx kx x l r) =+          case sCompare k kx of+               SLT -> let (found,l') = go l in (found,balance kx x l' r)+               SGT -> let (found,r') = go r in (found,balance kx x l r') +               SEQ -> unifyOnCompareEQ k kx $ case f kx x of+                       Just x' -> (Just x',Bin sx kx x' l r)+                       Nothing -> (Just x,glue l r)++-- | /O(log n)/. The expression (@'alter' f k map@) alters the value @x@ at @k@, or absence thereof.+-- 'alter' can be used to insert, delete, or update a value in a 'Map'.+-- In short : @'lookup' k ('alter' f k m) = f ('lookup' k m)@.+alter :: forall kproxy f v. (SOrd kproxy, SDecide kproxy) => (Maybe (f v) -> Maybe (f v)) -> Sing v -> SingMap kproxy f -> SingMap kproxy f+alter f k = k `seq` go+  where+    go :: SingMap kproxy f -> SingMap kproxy f+    go Tip = case f Nothing of+               Nothing -> Tip+               Just x  -> singleton k x++    go (Bin sx kx x l r) = case sCompare k kx of+               SLT -> balance kx x (go l) r+               SGT -> balance kx x l (go r)+               SEQ -> unifyOnCompareEQ k kx $ case f (Just x) of+                       Just x' -> Bin sx kx x' l r+                       Nothing -> glue l r++{--------------------------------------------------------------------+  Indexing+--------------------------------------------------------------------}++-- | /O(log n)/. Return the /index/ of a key. The index is a number from+-- /0/ up to, but not including, the 'size' of the map. Calls 'error' when+-- the key is not a 'member' of the map.+findIndex :: forall (kproxy :: KProxy k) f (v :: k). (SOrd kproxy, SDecide kproxy) => Sing v -> SingMap kproxy f -> Int+findIndex k t+  = case lookupIndex k t of+      Nothing  -> error "Map.findIndex: element is not in the map"+      Just idx -> idx++-- | /O(log n)/. Lookup the /index/ of a key. The index is a number from+-- /0/ up to, but not including, the 'size' of the map.+lookupIndex :: forall (kproxy :: KProxy k) f (v :: k). (SOrd kproxy, SDecide kproxy) => Sing v -> SingMap kproxy f -> Maybe Int+lookupIndex k = k `seq` go 0+  where+    go :: Int -> SingMap kproxy f -> Maybe Int+    go !idx Tip  = idx `seq` Nothing+    go !idx (Bin _ kx _ l r)+      = case sCompare k kx of+          SLT -> go idx l+          SGT -> go (idx + size l + 1) r +          SEQ -> Just (idx + size l)++-- | /O(log n)/. Retrieve an element by /index/. Calls 'error' when an+-- invalid index is used.+elemAt :: (kproxy ~ 'KProxy) => Int -> SingMap kproxy f -> SomeSingWith1 kproxy f+elemAt _ Tip = error "Map.elemAt: index out of range"+elemAt i (Bin _ kx x l r)+  = case compare i sizeL of+      LT -> elemAt i l+      GT -> elemAt (i-sizeL-1) r+      EQ -> SomeSingWith1 kx x+  where+    sizeL = size l++-- | /O(log n)/. Update the element at /index/. Calls 'error' when an+-- invalid index is used.+updateAt :: (kproxy ~ 'KProxy) => (forall v. Sing v -> f v -> Maybe (f v)) -> Int -> SingMap kproxy f -> SingMap kproxy f+updateAt f i0 t = i0 `seq` go i0 t+ where+    go _ Tip  = error "Map.updateAt: index out of range"+    go i (Bin sx kx x l r) = case compare i sizeL of+      LT -> balance kx x (go i l) r+      GT -> balance kx x l (go (i-sizeL-1) r)+      EQ -> case f kx x of+              Just x' -> Bin sx kx x' l r+              Nothing -> glue l r+      where +        sizeL = size l++-- | /O(log n)/. Delete the element at /index/.+-- Defined as (@'deleteAt' i map = 'updateAt' (\k x -> 'Nothing') i map@).+deleteAt :: (kproxy ~ 'KProxy) => Int -> SingMap kproxy f -> SingMap kproxy f+deleteAt i m+  = updateAt (\_ _ -> Nothing) i m+++{--------------------------------------------------------------------+  Minimal, Maximal+--------------------------------------------------------------------}++-- | /O(log n)/. The minimal key of the map. Calls 'error' is the map is empty.+findMin :: (kproxy ~ 'KProxy) => SingMap kproxy f -> SomeSingWith1 kproxy f+findMin (Bin _ kx x Tip _)  = SomeSingWith1 kx x+findMin (Bin _ _  _ l _)    = findMin l+findMin Tip                 = error "Map.findMin: empty map has no minimal element"++-- | /O(log n)/. The maximal key of the map. Calls 'error' is the map is empty.+findMax :: (kproxy ~ 'KProxy) => SingMap kproxy f -> SomeSingWith1 kproxy f+findMax (Bin _ kx x _ Tip)  = SomeSingWith1 kx x+findMax (Bin _ _  _ _ r)    = findMax r+findMax Tip                 = error "Map.findMax: empty map has no maximal element"++-- | /O(log n)/. Delete the minimal key. Returns an empty map if the map is empty.+deleteMin :: (kproxy ~ 'KProxy) => SingMap kproxy f -> SingMap kproxy f+deleteMin (Bin _ _  _ Tip r)  = r+deleteMin (Bin _ kx x l r)    = balance kx x (deleteMin l) r+deleteMin Tip                 = Tip++-- | /O(log n)/. Delete the maximal key. Returns an empty map if the map is empty.+deleteMax :: (kproxy ~ 'KProxy) => SingMap kproxy f -> SingMap kproxy f+deleteMax (Bin _ _  _ l Tip)  = l+deleteMax (Bin _ kx x l r)    = balance kx x l (deleteMax r)+deleteMax Tip                 = Tip++-- | /O(log n)/. Update the value at the minimal key.+updateMinWithKey :: (forall v. Sing v -> f v -> Maybe (f v)) -> SingMap kproxy f -> SingMap kproxy f+updateMinWithKey f = go+ where+    go (Bin sx kx x Tip r) = case f kx x of+                                  Nothing -> r+                                  Just x' -> Bin sx kx x' Tip r+    go (Bin _ kx x l r)    = balance kx x (go l) r+    go Tip                 = Tip++-- | /O(log n)/. Update the value at the maximal key.+updateMaxWithKey :: (forall v. Sing v -> f v -> Maybe (f v)) -> SingMap kproxy f -> SingMap kproxy f+updateMaxWithKey f = go+ where+    go (Bin sx kx x l Tip) = case f kx x of+                              Nothing -> l+                              Just x' -> Bin sx kx x' l Tip+    go (Bin _ kx x l r)    = balance kx x l (go r)+    go Tip                 = Tip++-- | /O(log n)/. Retrieves the minimal (key :=> value) entry of the map, and+-- the map stripped of that element, or 'Nothing' if passed an empty map.+minViewWithKey :: (kproxy ~ 'KProxy) => SingMap kproxy f -> Maybe (SomeSingWith1 kproxy f, SingMap kproxy f)+minViewWithKey Tip = Nothing+minViewWithKey x   = Just (deleteFindMin x)++-- | /O(log n)/. Retrieves the maximal (key :=> value) entry of the map, and+-- the map stripped of that element, or 'Nothing' if passed an empty map.+maxViewWithKey :: (kproxy ~ 'KProxy) => SingMap kproxy f -> Maybe (SomeSingWith1 kproxy f, SingMap kproxy f)+maxViewWithKey Tip = Nothing+maxViewWithKey x   = Just (deleteFindMax x)++{--------------------------------------------------------------------+  Union. +--------------------------------------------------------------------}++-- | The union of a list of maps:+--   (@'unions' == 'Prelude.foldl' 'union' 'empty'@).+unions :: (SOrd kproxy, SDecide kproxy) => [SingMap kproxy f] -> SingMap kproxy f+unions ts+  = foldlStrict union empty ts++-- | The union of a list of maps, with a combining operation:+--   (@'unionsWithKey' f == 'Prelude.foldl' ('unionWithKey' f) 'empty'@).+unionsWithKey :: (SOrd kproxy, SDecide kproxy) => (forall v. Sing v -> f v -> f v -> f v) -> [SingMap kproxy f] -> SingMap kproxy f+unionsWithKey f ts+  = foldlStrict (unionWithKey f) empty ts++-- | /O(n+m)/.+-- The expression (@'union' t1 t2@) takes the left-biased union of @t1@ and @t2@. +-- It prefers @t1@ when duplicate keys are encountered,+-- i.e. (@'union' == 'unionWith' 'const'@).+-- The implementation uses the efficient /hedge-union/ algorithm.+-- Hedge-union is more efficient on (bigset \``union`\` smallset).+union :: (SOrd kproxy, SDecide kproxy) => SingMap kproxy f -> SingMap kproxy f -> SingMap kproxy f+union Tip t2  = t2+union t1 Tip  = t1+union t1 t2 = hedgeUnionL (const LT) (const GT) t1 t2++-- left-biased hedge union+hedgeUnionL :: (SOrd kproxy, SDecide kproxy)+            => (SomeSing kproxy -> Ordering) -> (SomeSing kproxy -> Ordering) -> SingMap kproxy f -> SingMap kproxy f+            -> SingMap kproxy f+hedgeUnionL _     _     t1 Tip+  = t1+hedgeUnionL cmplo cmphi Tip (Bin _ kx x l r)+  = combine kx x (filterGt cmplo l) (filterLt cmphi r)+hedgeUnionL cmplo cmphi (Bin _ kx x l r) t2+  = combine kx x (hedgeUnionL cmplo cmpkx l (trim cmplo cmpkx t2)) +              (hedgeUnionL cmpkx cmphi r (trim cmpkx cmphi t2))+  where+    cmpkx k  = compareSome (SomeSing kx) k++{--------------------------------------------------------------------+  Union with a combining function+--------------------------------------------------------------------}++-- | /O(n+m)/.+-- Union with a combining function. The implementation uses the efficient /hedge-union/ algorithm.+-- Hedge-union is more efficient on (bigset \``union`\` smallset).+unionWithKey :: (SOrd kproxy, SDecide kproxy) => (forall v. Sing v -> f v -> f v -> f v) -> SingMap kproxy f -> SingMap kproxy f -> SingMap kproxy f+unionWithKey _ Tip t2  = t2+unionWithKey _ t1 Tip  = t1+unionWithKey f t1 t2 = hedgeUnionWithKey f (const LT) (const GT) t1 t2++hedgeUnionWithKey :: forall kproxy f. (SOrd kproxy, SDecide kproxy)+                  => (forall v. Sing v -> f v -> f v -> f v)+                  -> (SomeSing kproxy -> Ordering) -> (SomeSing kproxy -> Ordering)+                  -> SingMap kproxy f -> SingMap kproxy f+                  -> SingMap kproxy f+hedgeUnionWithKey _ _     _     t1 Tip+  = t1+hedgeUnionWithKey _ cmplo cmphi Tip (Bin _ kx x l r)+  = combine kx x (filterGt cmplo l) (filterLt cmphi r)+hedgeUnionWithKey f cmplo cmphi (Bin _ (kx :: Sing tx) x l r) t2+  = combine kx newx (hedgeUnionWithKey f cmplo cmpkx l lt) +                 (hedgeUnionWithKey f cmpkx cmphi r gt)+  where+    cmpkx k     = compareSome (SomeSing kx) k+    lt          = trim cmplo cmpkx t2+    (found,gt)  = trimLookupLo (SomeSing kx) cmphi t2+    newx :: f tx+    newx        = case found of+                    Nothing -> x+                    Just (SomeSingWith1 ky y) -> case kx %:== ky of+                        STrue  -> unifyOnEq kx ky (f kx x y)+                        SFalse -> error "SingMap.union: inconsistent SEq instance"++{--------------------------------------------------------------------+  Difference+--------------------------------------------------------------------}++-- | /O(n+m)/. Difference of two maps. +-- Return elements of the first map not existing in the second map.+-- The implementation uses an efficient /hedge/ algorithm comparable with /hedge-union/.+difference :: (SOrd kproxy, SDecide kproxy) => SingMap kproxy f -> SingMap kproxy g -> SingMap kproxy f+difference Tip _   = Tip+difference t1 Tip  = t1+difference t1 t2   = hedgeDiff (const LT) (const GT) t1 t2++hedgeDiff :: (SOrd kproxy, SDecide kproxy)+          => (SomeSing kproxy -> Ordering) -> (SomeSing kproxy -> Ordering) -> SingMap kproxy f -> SingMap kproxy g+          -> SingMap kproxy f+hedgeDiff _     _     Tip _+  = Tip+hedgeDiff cmplo cmphi (Bin _ kx x l r) Tip +  = combine kx x (filterGt cmplo l) (filterLt cmphi r)+hedgeDiff cmplo cmphi t (Bin _ kx _ l r) +  = merge (hedgeDiff cmplo cmpkx (trim cmplo cmpkx t) l) +          (hedgeDiff cmpkx cmphi (trim cmpkx cmphi t) r)+  where+    cmpkx k = compareSome (SomeSing kx) k   ++-- | /O(n+m)/. Difference with a combining function. When two equal keys are+-- encountered, the combining function is applied to the key and both values.+-- If it returns 'Nothing', the element is discarded (proper set difference). If+-- it returns (@'Just' y@), the element is updated with a new value @y@. +-- The implementation uses an efficient /hedge/ algorithm comparable with /hedge-union/.+differenceWithKey :: (SOrd kproxy, SDecide kproxy) => (forall v. Sing v -> f v -> g v -> Maybe (f v)) -> SingMap kproxy f -> SingMap kproxy g -> SingMap kproxy f+differenceWithKey _ Tip _   = Tip+differenceWithKey _ t1 Tip  = t1+differenceWithKey f t1 t2   = hedgeDiffWithKey f (const LT) (const GT) t1 t2++hedgeDiffWithKey :: (SOrd kproxy, SDecide kproxy)+                 => (forall v. Sing v -> f v -> g v -> Maybe (f v))+                 -> (SomeSing kproxy -> Ordering) -> (SomeSing kproxy -> Ordering)+                 -> SingMap kproxy f -> SingMap kproxy g+                 -> SingMap kproxy f+hedgeDiffWithKey _ _     _     Tip _+  = Tip+hedgeDiffWithKey _ cmplo cmphi (Bin _ kx x l r) Tip+  = combine kx x (filterGt cmplo l) (filterLt cmphi r)+hedgeDiffWithKey f cmplo cmphi t (Bin _ kx x l r) +  = case found of+      Nothing -> merge tl tr+      Just (SomeSingWith1 ky y) -> +        case kx %:== ky of+          SFalse -> error "SingMap.difference: inconsistent SEq instance"+          STrue -> unifyOnEq kx ky $+            case f ky y x of+              Nothing -> merge tl tr+              Just z  -> combine ky z tl tr+  where+    cmpkx k     = compareSome (SomeSing kx) k   +    lt          = trim cmplo cmpkx t+    (found,gt)  = trimLookupLo (SomeSing kx) cmphi t+    tl          = hedgeDiffWithKey f cmplo cmpkx lt l+    tr          = hedgeDiffWithKey f cmpkx cmphi gt r++++{--------------------------------------------------------------------+  Intersection+--------------------------------------------------------------------}++-- | /O(n+m)/. Intersection of two maps.+-- Return data in the first map for the keys existing in both maps.+-- (@'intersection' m1 m2 == 'intersectionWith' 'const' m1 m2@).+intersection :: (SOrd kproxy, SDecide kproxy) => SingMap kproxy f -> SingMap kproxy f -> SingMap kproxy f+intersection m1 m2+  = intersectionWithKey (\_ x _ -> x) m1 m2++-- | /O(n+m)/. Intersection with a combining function.+-- Intersection is more efficient on (bigset \``intersection`\` smallset).+intersectionWithKey :: (SOrd kproxy, SDecide kproxy) => (forall v. Sing v -> f v -> g v -> h v) -> SingMap kproxy f -> SingMap kproxy g -> SingMap kproxy h+intersectionWithKey _ Tip _ = Tip+intersectionWithKey _ _ Tip = Tip+intersectionWithKey f t1@(Bin s1 k1 x1 l1 r1) t2@(Bin s2 k2 x2 l2 r2) =+   if s1 >= s2 then+      let (lt,found,gt) = splitLookupWithKey k2 t1+          tl            = intersectionWithKey f lt l2+          tr            = intersectionWithKey f gt r2+      in case found of+      Just (k,x) -> combine k (f k x x2) tl tr+      Nothing -> merge tl tr+   else let (lt,found,gt) = splitLookup k1 t2+            tl            = intersectionWithKey f l1 lt+            tr            = intersectionWithKey f r1 gt+      in case found of+      Just x -> combine k1 (f k1 x1 x) tl tr+      Nothing -> merge tl tr++++-- TODO: Fix submap functions+-- {--------------------------------------------------------------------+--   Submap+-- --------------------------------------------------------------------}+-- -- | /O(n+m)/.+-- -- This function is defined as (@'isSubmapOf' = 'isSubmapOfBy' 'eqTagged')@).+-- isSubmapOf :: ((SOrd kproxy, SDecide kproxy) EqTag k f) => SingMap kproxy f -> SingMap kproxy f -> Bool+-- isSubmapOf m1 m2 = isSubmapOfBy eqTagged m1 m2+-- +-- {- | /O(n+m)/.+--  The expression (@'isSubmapOfBy' f t1 t2@) returns 'True' if+--  all keys in @t1@ are in tree @t2@, and when @f@ returns 'True' when+--  applied to their respective keys and values.+-- -}+-- isSubmapOfBy :: (SOrd kproxy, SDecide kproxy) => (forall v. Sing v -> Sing v -> f v -> g v -> Bool) -> SingMap kproxy f -> SingMap kproxy g -> Bool+-- isSubmapOfBy f t1 t2+--   = (size t1 <= size t2) && (submap' f t1 t2)+-- +-- submap' :: (SOrd kproxy, SDecide kproxy) => (forall v. Sing v -> Sing v -> f v -> g v -> Bool) -> SingMap kproxy f -> SingMap kproxy g -> Bool+-- submap' _ Tip _ = True+-- submap' _ _ Tip = False+-- submap' f (Bin _ kx x l r) t+--   = case found of+--       Nothing -> False+--       Just (ky, y)  -> f kx ky x y && submap' f l lt && submap' f r gt+--   where+--     (lt,found,gt) = splitLookupWithKey kx t+-- +-- -- | /O(n+m)/. Is this a proper submap? (ie. a submap but not equal). +-- -- Defined as (@'isProperSubmapOf' = 'isProperSubmapOfBy' 'eqTagged'@).+-- isProperSubmapOf :: ((SOrd kproxy, SDecide kproxy) EqTag k f) => SingMap kproxy f -> SingMap kproxy f -> Bool+-- isProperSubmapOf m1 m2+--   = isProperSubmapOfBy eqTagged m1 m2+-- +-- {- | /O(n+m)/. Is this a proper submap? (ie. a submap but not equal).+--  The expression (@'isProperSubmapOfBy' f m1 m2@) returns 'True' when+--  @m1@ and @m2@ are not equal,+--  all keys in @m1@ are in @m2@, and when @f@ returns 'True' when+--  applied to their respective keys and values. +-- -}+-- isProperSubmapOfBy :: (SOrd kproxy, SDecide kproxy) => (forall v. Sing v -> Sing v -> f v -> g v -> Bool) -> SingMap kproxy f -> SingMap kproxy g -> Bool+-- isProperSubmapOfBy f t1 t2+--   = (size t1 < size t2) && (submap' f t1 t2)++{--------------------------------------------------------------------+  Filter and partition+--------------------------------------------------------------------}++-- | /O(n)/. Filter all keys\/values that satisfy the predicate.+filterWithKey :: (SOrd kproxy, SDecide kproxy) => (forall v. Sing v -> f v -> Bool) -> SingMap kproxy f -> SingMap kproxy f+filterWithKey p = go+  where+    go Tip = Tip+    go (Bin _ kx x l r)+          | p kx x    = combine kx x (go l) (go r)+          | otherwise = merge (go l) (go r)++-- | /O(n)/. Partition the map according to a predicate. The first+-- map contains all elements that satisfy the predicate, the second all+-- elements that fail the predicate. See also 'split'.+partitionWithKey :: (SOrd kproxy, SDecide kproxy) => (forall v. Sing v -> f v -> Bool) -> SingMap kproxy f -> (SingMap kproxy f, SingMap kproxy f)+partitionWithKey _ Tip = (Tip,Tip)+partitionWithKey p (Bin _ kx x l r)+  | p kx x    = (combine kx x l1 r1,merge l2 r2)+  | otherwise = (merge l1 r1,combine kx x l2 r2)+  where+    (l1,l2) = partitionWithKey p l+    (r1,r2) = partitionWithKey p r++-- | /O(n)/. Map keys\/values and collect the 'Just' results.+mapMaybeWithKey :: (SOrd kproxy, SDecide kproxy) => (forall v. Sing v -> f v -> Maybe (g v)) -> SingMap kproxy f -> SingMap kproxy g+mapMaybeWithKey f = go+  where+    go Tip = Tip+    go (Bin _ kx x l r) = case f kx x of+        Just y  -> combine kx y (go l) (go r)+        Nothing -> merge (go l) (go r)++-- | /O(n)/. Map keys\/values and separate the 'Left' and 'Right' results.+mapEitherWithKey :: (SOrd kproxy, SDecide kproxy) =>+  (forall v. Sing v -> f v -> Either (g v) (h v)) -> SingMap kproxy f -> (SingMap kproxy g, SingMap kproxy h)+mapEitherWithKey _ Tip = (Tip, Tip)+mapEitherWithKey f (Bin _ kx x l r) = case f kx x of+  Left y  -> (combine kx y l1 r1, merge l2 r2)+  Right z -> (merge l1 r1, combine kx z l2 r2)+ where+    (l1,l2) = mapEitherWithKey f l+    (r1,r2) = mapEitherWithKey f r++{--------------------------------------------------------------------+  Mapping+--------------------------------------------------------------------}++-- | /O(n)/. Map a function over all values in the map.+mapWithKey :: (forall v. Sing v -> f v -> g v) -> SingMap kproxy f -> SingMap kproxy g+mapWithKey f = go+  where+    go Tip = Tip+    go (Bin sx kx x l r) = Bin sx kx (f kx x) (go l) (go r)++-- | /O(n)/. The function 'mapAccumLWithKey' threads an accumulating+-- argument throught the map in ascending order of keys.+mapAccumLWithKey :: (forall v. a -> Sing v -> f v -> (a, g v)) -> a -> SingMap kproxy f -> (a, SingMap kproxy g)+mapAccumLWithKey f = go+  where+    go a Tip               = (a,Tip)+    go a (Bin sx kx x l r) =+                 let (a1,l') = go a l+                     (a2,x') = f a1 kx x+                     (a3,r') = go a2 r+                 in (a3,Bin sx kx x' l' r')++-- | /O(n)/. The function 'mapAccumRWithKey' threads an accumulating+-- argument through the map in descending order of keys.+mapAccumRWithKey :: (forall v. a -> Sing v -> f v -> (a, g v)) -> a -> SingMap kproxy f -> (a, SingMap kproxy g)+mapAccumRWithKey f = go+  where+    go a Tip = (a,Tip)+    go a (Bin sx kx x l r) =+                 let (a1,r') = go a r+                     (a2,x') = f a1 kx x+                     (a3,l') = go a2 l+                 in (a3,Bin sx kx x' l' r')++-- TODO: Maybe fix mapKeysWith. I don't think this function is +-- actually meaningful with singletons though.+-- | /O(n*log n)/.+-- @'mapKeysWith' c f s@ is the map obtained by applying @f@ to each key of @s@.+-- +-- The size of the result may be smaller if @f@ maps two or more distinct+-- keys to the same new key.  In this case the associated values will be+-- combined using @c@.+-- mapKeysWith :: (SOrd kproxy2, SDecide kproxy2) => (forall v. Sing v -> f v -> f v -> f v) -> (forall v. Sing v -> Sing v) -> SingMap kproxy1 f -> SingMap kproxy2 f+-- mapKeysWith c f = fromListWithKey c . map fFirst . toList+--     where fFirst (SomeSingWith1 x y) = (SomeSingWith1 (f x) y)+++-- TODO: Maybe fix mapKeysMonotonic. I don't think this function is +-- actually meaningful with singletons though.+--+-- | /O(n)/.+-- @'mapKeysMonotonic' f s == 'mapKeys' f s@, but works only when @f@+-- is strictly monotonic.+-- That is, for any values @x@ and @y@, if @x@ < @y@ then @f x@ < @f y@.+-- /The precondition is not checked./+-- Semi-formally, we have:+-- +-- > and [x < y ==> f x < f y | x <- ls, y <- ls] +-- >                     ==> mapKeysMonotonic f s == mapKeys f s+-- >     where ls = keys s+--+-- This means that @f@ maps distinct original keys to distinct resulting keys.+-- This function has better performance than 'mapKeys'.+-- mapKeysMonotonic :: forall (kproxy1 :: KProxy k) kproxy2 f. (forall (v :: k). Sing v -> Sing v) -> SingMap kproxy1 f -> SingMap kproxy2 f+-- mapKeysMonotonic _ Tip = Tip+-- mapKeysMonotonic f (Bin sz k x l r) =+--     Bin sz (f k) x (mapKeysMonotonic f l) (mapKeysMonotonic f r)++{--------------------------------------------------------------------+  Folds  +--------------------------------------------------------------------}++-- | /O(n)/. Fold the keys and values in the map, such that+-- @'foldWithKey' f z == 'Prelude.foldr' ('uncurry' f) z . 'toAscList'@.+--+-- This is identical to 'foldrWithKey', and you should use that one instead of+-- this one.  This name is kept for backward compatibility.+foldWithKey :: (forall v. Sing v -> f v -> b -> b) -> b -> SingMap kproxy f -> b+foldWithKey = foldrWithKey+{-# DEPRECATED foldWithKey "Use foldrWithKey instead" #-}++-- | /O(n)/. Post-order fold.  The function will be applied from the lowest+-- value to the highest.+foldrWithKey :: (forall v. Sing v -> f v -> b -> b) -> b -> SingMap kproxy f -> b+foldrWithKey f = go+  where+    go z Tip              = z+    go z (Bin _ kx x l r) = go (f kx x (go z r)) l++-- | /O(n)/. Pre-order fold.  The function will be applied from the highest+-- value to the lowest.+foldlWithKey :: (forall v. b -> Sing v -> f v -> b) -> b -> SingMap kproxy f -> b+foldlWithKey f = go+  where+    go z Tip              = z+    go z (Bin _ kx x l r) = go (f (go z l) kx x) r++{-+-- | /O(n)/. A strict version of 'foldlWithKey'.+foldlWithKey' :: (b -> k -> a -> b) -> b -> SingMap kproxy -> b+foldlWithKey' f = go+  where+    go z Tip              = z+    go z (Bin _ kx x l r) = z `seq` go (f (go z l) kx x) r+-}++{--------------------------------------------------------------------+  List variations +--------------------------------------------------------------------}++-- | /O(n)/. Return all keys of the map in ascending order.+--+-- > keys (fromList [(5,"a"), (3,"b")]) == [3,5]+-- > keys empty == []++keys :: (kproxy ~ 'KProxy) => SingMap kproxy f -> [SomeSing kproxy]+keys m+  = [SomeSing k | (SomeSingWith1 k _) <- assocs m]++-- | /O(n)/. Return all key\/value pairs in the map in ascending key order.+assocs :: (kproxy ~ 'KProxy) => SingMap kproxy f -> [SomeSingWith1 kproxy f]+assocs m+  = toList m++{--------------------------------------------------------------------+  Lists +  use [foldlStrict] to reduce demand on the control-stack+--------------------------------------------------------------------}++-- | /O(n*log n)/. Build a map from a list of key\/value pairs. See also 'fromAscList'.+-- If the list contains more than one value for the same key, the last value+-- for the key is retained.+fromList :: (SOrd kproxy, SDecide kproxy) => [SomeSingWith1 kproxy f] -> SingMap kproxy f+fromList xs       +  = foldlStrict ins empty xs+  where+    ins :: (SOrd kproxy, SDecide kproxy) => SingMap kproxy f -> SomeSingWith1 kproxy f -> SingMap kproxy f+    ins t (SomeSingWith1 k x) = insert k x t++-- | /O(n*log n)/. Build a map from a list of key\/value pairs with a combining function. See also 'fromAscListWithKey'.+fromListWithKey :: (SOrd kproxy, SDecide kproxy) => (forall v. Sing v -> f v -> f v -> f v) -> [SomeSingWith1 kproxy f] -> SingMap kproxy f+fromListWithKey f xs +  = foldlStrict (ins f) empty xs+  where+    ins :: (SOrd kproxy, SDecide kproxy) => (forall v. Sing v -> f v -> f v -> f v) -> SingMap kproxy f -> SomeSingWith1 kproxy f -> SingMap kproxy f+    ins f t (SomeSingWith1 k x) = insertWithKey f k x t++-- | /O(n)/. Convert to a list of key\/value pairs.+toList :: (kproxy ~ 'KProxy) => SingMap kproxy f -> [SomeSingWith1 kproxy f]+toList t      = toAscList t++-- | /O(n)/. Convert to an ascending list.+toAscList :: (kproxy ~ 'KProxy) => SingMap kproxy f -> [SomeSingWith1 kproxy f]+toAscList t   = foldrWithKey (\k x xs -> (SomeSingWith1 k x):xs) [] t++-- | /O(n)/. Convert to a descending list.+toDescList :: (kproxy ~ 'KProxy) => SingMap kproxy f -> [SomeSingWith1 kproxy f]+toDescList t  = foldlWithKey (\xs k x -> (SomeSingWith1 k x):xs) [] t++{--------------------------------------------------------------------+  Building trees from ascending/descending lists can be done in linear time.+  +  Note that if [xs] is ascending that: +    fromAscList xs       == fromList xs+    fromAscListWith f xs == fromListWith f xs+--------------------------------------------------------------------}++-- | /O(n)/. Build a map from an ascending list in linear time.+-- /The precondition (input list is ascending) is not checked./+fromAscList :: (SEq kproxy, SDecide kproxy) => [SomeSingWith1 kproxy f] -> SingMap kproxy f+fromAscList xs+  = fromAscListWithKey (\_ x _ -> x) xs++-- | /O(n)/. Build a map from an ascending list in linear time with a+-- combining function for equal keys.+-- /The precondition (input list is ascending) is not checked./+fromAscListWithKey :: (SEq kproxy, SDecide kproxy) => (forall v. Sing v -> f v -> f v -> f v) -> [SomeSingWith1 kproxy f] -> SingMap kproxy f +fromAscListWithKey f xs+  = fromDistinctAscList (combineEq f xs)+  where+  -- [combineEq f xs] combines equal elements with function [f] in an ordered list [xs]+  combineEq _ xs'+    = case xs' of+        []     -> []+        [x]    -> [x]+        (x:xx) -> combineEq' f x xx++  combineEq' :: (SEq kproxy, SDecide kproxy) => (forall v. Sing v -> f v -> f v -> f v) -> SomeSingWith1 kproxy f -> [SomeSingWith1 kproxy f] -> [SomeSingWith1 kproxy f]+  combineEq' f z [] = [z]+  combineEq' f z@(SomeSingWith1 kz zz) (x@(SomeSingWith1 kx xx):xs') =+    case kx %:== kz of+      STrue  -> unifyOnEq kx kz (let yy = f kx xx zz in combineEq' f (SomeSingWith1 kx yy) xs')+      SFalse -> z : combineEq' f x xs'+++-- | /O(n)/. Build a map from an ascending list of distinct elements in linear time.+-- /The precondition is not checked./+fromDistinctAscList :: [SomeSingWith1 kproxy f] -> SingMap kproxy f+fromDistinctAscList xs+  = build const (length xs) xs+  where+    -- 1) use continutations so that we use heap space instead of stack space.+    -- 2) special case for n==5 to build bushier trees. +    +    build :: (SingMap kproxy f -> [SomeSingWith1 kproxy f] -> b) -> Int -> [SomeSingWith1 kproxy f] -> b+    build c 0 xs'  = c Tip xs'+    build c 5 xs'  = case xs' of+                       ((SomeSingWith1 k1 x1):(SomeSingWith1 k2 x2):(SomeSingWith1 k3 x3):(SomeSingWith1 k4 x4):(SomeSingWith1 k5 x5):xx) +                            -> c (bin k4 x4 (bin k2 x2 (singleton k1 x1) (singleton k3 x3)) (singleton k5 x5)) xx+                       _ -> error "fromDistinctAscList build"+    build c n xs'  = seq nr $ build (buildR nr c) nl xs'+                   where+                     nl = n `div` 2+                     nr = n - nl - 1++    buildR :: Int -> (SingMap kproxy f -> [SomeSingWith1 kproxy f] -> b) -> SingMap kproxy f -> [SomeSingWith1 kproxy f] -> b+    buildR n c l (SomeSingWith1 k x : ys) = build (buildB l k x c) n ys+    buildR _ _ _ []           = error "fromDistinctAscList buildR []"+    +    buildB :: SingMap kproxy f -> Sing v -> f v -> (SingMap kproxy f -> a -> b) -> SingMap kproxy f -> a -> b+    buildB l k x c r zs       = c (bin k x l r) zs+                      ++{--------------------------------------------------------------------+  Split+--------------------------------------------------------------------}++-- | /O(log n)/. The expression (@'split' k map@) is a pair @(map1,map2)@ where+-- the keys in @map1@ are smaller than @k@ and the keys in @map2@ larger than @k@.+-- Any key equal to @k@ is found in neither @map1@ nor @map2@.+split :: forall (kproxy :: KProxy k) f (v :: k). (SOrd kproxy, SDecide kproxy) => Sing v -> SingMap kproxy f -> (SingMap kproxy f, SingMap kproxy f)+split k = go+  where+    go :: SingMap kproxy f -> (SingMap kproxy f, SingMap kproxy f)+    go Tip              = (Tip, Tip)+    go (Bin _ kx x l r) = case sCompare k kx of+      SLT -> let (lt,gt) = go l in (lt,combine kx x gt r)+      SGT -> let (lt,gt) = go r in (combine kx x l lt,gt)+      SEQ -> unifyOnCompareEQ k kx (l,r)++-- | /O(log n)/. The expression (@'splitLookup' k map@) splits a map just+-- like 'split' but also returns @'lookup' k map@.+splitLookup :: forall kproxy f v. (SOrd kproxy, SDecide kproxy) => Sing v -> SingMap kproxy f -> (SingMap kproxy f, Maybe (f v), SingMap kproxy f)+splitLookup k = go+  where+    go :: SingMap kproxy f -> (SingMap kproxy f, Maybe (f v), SingMap kproxy f)+    go Tip              = (Tip,Nothing,Tip)+    go (Bin _ kx x l r) = case sCompare k kx of+      SLT -> let (lt,z,gt) = go l in (lt,z,combine kx x gt r)+      SGT -> let (lt,z,gt) = go r in (combine kx x l lt,z,gt)+      SEQ -> unifyOnCompareEQ k kx (l,Just x,r)++-- | /O(log n)/.+splitLookupWithKey :: forall kproxy f v. (SOrd kproxy, SDecide kproxy) => Sing v -> SingMap kproxy f -> (SingMap kproxy f, Maybe (Sing v, f v), SingMap kproxy f)+splitLookupWithKey k = go+  where+    go :: SingMap kproxy f -> (SingMap kproxy f, Maybe (Sing v, f v), SingMap kproxy f)+    go Tip              = (Tip,Nothing,Tip)+    go (Bin _ kx x l r) = case sCompare k kx of+      SLT -> let (lt,z,gt) = go l in (lt,z,combine kx x gt r)+      SGT -> let (lt,z,gt) = go r in (combine kx x l lt,z,gt)+      SEQ -> unifyOnCompareEQ k kx (l,Just (kx, x),r)++-- TODO: Enable Eq and Ord instances+{--------------------------------------------------------------------+  Eq converts the tree to a list. In a lazy setting, this +  actually seems one of the faster methods to compare two trees +  and it is certainly the simplest :-)+--------------------------------------------------------------------}+-- instance EqSing1 f => Eq (SingMap kproxy f) where+--   t1 == t2  = (size t1 == size t2) && (toAscList t1 == toAscList t2)++{--------------------------------------------------------------------+  Ord +--------------------------------------------------------------------}++-- instance OrdTag k f => Ord (SingMap kproxy f) where+--     compare m1 m2 = compare (toAscList m1) (toAscList m2)++-- TODO: Figure out show to recreate a Read instance+{--------------------------------------------------------------------+  Read+--------------------------------------------------------------------}++-- instance ((SOrd kproxy, SDecide kproxy) ReadTag k f) => Read (SingMap kproxy f) where+--   readPrec = parens $ prec 10 $ do+--     Ident "fromList" <- lexP+--     xs <- readPrec+--     return (fromList xs)+-- +--   readListPrec = readListPrecDefault++-- TODO: Figure out show to recreate a Show instance+{--------------------------------------------------------------------+  Show+--------------------------------------------------------------------}+-- instance ShowTag k f => Show (SingMap kproxy f) where+--     showsPrec p m = showParen (p>10)+--         ( showString "fromList "+--         . showsPrec 11 (toList m)+--         )+-- +-- -- | /O(n)/. Show the tree that implements the map. The tree is shown+-- -- in a compressed, hanging format. See 'showTreeWith'.+-- showTree :: ShowTag k f => SingMap kproxy f -> String+-- showTree m+--   = showTreeWith showElem True False m+--   where+--     showElem :: ShowTag k f => Sing v -> f v -> String+--     showElem k x  = show (k :=> x)+++{- | /O(n)/. The expression (@'showTreeWith' showelem hang wide map@) shows+ the tree that implements the map. Elements are shown using the @showElem@ function. If @hang@ is+ 'True', a /hanging/ tree is shown otherwise a rotated tree is shown. If+ @wide@ is 'True', an extra wide version is shown.+-}+showTreeWith :: (forall v. Sing v -> f v -> String) -> Bool -> Bool -> SingMap kproxy f -> String+showTreeWith showelem hang wide t+  | hang      = (showsTreeHang showelem wide [] t) ""+  | otherwise = (showsTree showelem wide [] [] t) ""++showsTree :: (forall v. Sing v -> f v -> String) -> Bool -> [String] -> [String] -> SingMap kproxy f -> ShowS+showsTree showelem wide lbars rbars t+  = case t of+      Tip -> showsBars lbars . showString "|\n"+      Bin _ kx x Tip Tip+          -> showsBars lbars . showString (showelem kx x) . showString "\n" +      Bin _ kx x l r+          -> showsTree showelem wide (withBar rbars) (withEmpty rbars) r .+             showWide wide rbars .+             showsBars lbars . showString (showelem kx x) . showString "\n" .+             showWide wide lbars .+             showsTree showelem wide (withEmpty lbars) (withBar lbars) l++showsTreeHang :: (forall v. Sing v -> f v -> String) -> Bool -> [String] -> SingMap kproxy f -> ShowS+showsTreeHang showelem wide bars t+  = case t of+      Tip -> showsBars bars . showString "|\n" +      Bin _ kx x Tip Tip+          -> showsBars bars . showString (showelem kx x) . showString "\n" +      Bin _ kx x l r+          -> showsBars bars . showString (showelem kx x) . showString "\n" . +             showWide wide bars .+             showsTreeHang showelem wide (withBar bars) l .+             showWide wide bars .+             showsTreeHang showelem wide (withEmpty bars) r++showWide :: Bool -> [String] -> String -> String+showWide wide bars +  | wide      = showString (concat (reverse bars)) . showString "|\n" +  | otherwise = id++showsBars :: [String] -> ShowS+showsBars bars+  = case bars of+      [] -> id+      _  -> showString (concat (reverse (tail bars))) . showString node++node :: String+node           = "+--"++withBar, withEmpty :: [String] -> [String]+withBar bars   = "|  ":bars+withEmpty bars = "   ":bars++{--------------------------------------------------------------------+  Assertions+--------------------------------------------------------------------}++-- | /O(n)/. Test if the internal map structure is valid.+valid :: (SOrd kproxy, SDecide kproxy) => SingMap kproxy f -> Bool+valid t+  = balanced t && ordered t && validsize t++ordered :: (SOrd kproxy, SDecide kproxy) => SingMap kproxy f -> Bool+ordered t+  = bounded (const True) (const True) t+  where+    bounded :: (SOrd kproxy, SDecide kproxy) => (SomeSing kproxy -> Bool) -> (SomeSing kproxy -> Bool) -> SingMap kproxy f -> Bool+    bounded lo hi t'+      = case t' of+          Tip              -> True+          Bin _ kx _ l r  -> (lo (SomeSing kx)) +                          && (hi (SomeSing kx)) +                          && bounded lo (`ltSome` SomeSing kx) l +                          && bounded (`gtSome` SomeSing kx) hi r++-- | Exported only for "Debug.QuickCheck"+balanced :: SingMap kproxy f -> Bool+balanced t+  = case t of+      Tip            -> True+      Bin _ _ _ l r  -> (size l + size r <= 1 || (size l <= delta*size r && size r <= delta*size l)) &&+                        balanced l && balanced r++validsize :: SingMap kproxy f -> Bool+validsize t+  = (realsize t == Just (size t))+  where+    realsize t'+      = case t' of+          Tip            -> Just 0+          Bin sz _ _ l r -> case (realsize l,realsize r) of+                            (Just n,Just m)  | n+m+1 == sz  -> Just sz+                            _                               -> Nothing+{--------------------------------------------------------------------+  Utilities+--------------------------------------------------------------------}+foldlStrict :: (a -> b -> a) -> a -> [b] -> a+foldlStrict f = go+  where+    go z []     = z+    go z (x:xs) = z `seq` go (f z x) xs+++-- Helper function to demote a comparison+compareSome :: SOrd kproxy => SomeSing kproxy -> SomeSing kproxy -> Ordering+compareSome (SomeSing a) (SomeSing b) = fromSing (sCompare a b)++ltSome :: SOrd kproxy => SomeSing kproxy -> SomeSing kproxy -> Bool+ltSome (SomeSing a) (SomeSing b) = fromSing (a %:< b)++gtSome :: SOrd kproxy => SomeSing kproxy -> SomeSing kproxy -> Bool+gtSome (SomeSing a) (SomeSing b) = fromSing (a %:> b)++unifyOnCompareEQ :: forall (kproxy :: KProxy k) (a :: k) (b :: k) x. +  (SDecide kproxy, Compare a b ~ 'EQ)+  => Sing a -> Sing b -> (a ~ b => x) -> x+unifyOnCompareEQ a b x =+  case testEquality a b of+    Nothing -> error "unifyOnCompareEQ: inconsistent SOrd and SDecide instances"+    Just Refl -> x++unifyOnEq :: forall (kproxy :: KProxy k) (a :: k) (b :: k) x. +  (SDecide kproxy, (a :== b) ~ 'True)+  => Sing a -> Sing b -> (a ~ b => x) -> x+unifyOnEq a b x =+  case testEquality a b of+    Nothing -> error "unifyOnEq: inconsistent SEq and SDecide instances"+    Just Refl -> x+