{-# LANGUAGE CPP #-} {-# LANGUAGE BangPatterns #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE TupleSections #-} -- | Strict tries (based on "Data.Map.Strict" and "Agda.Utils.Maybe.Strict"). module Agda.Utils.Trie ( Trie , empty, singleton, insert, insertWith, union, unionWith, adjust, delete , toList, toAscList , lookupPath ) where import Prelude hiding (Maybe(..), maybe) import qualified Prelude as Lazy import Data.Function import Data.Functor import Data.List (nubBy, sortBy, isPrefixOf) #if MIN_VERSION_containers(0,5,0) import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map #else import Data.Map (Map) import qualified Data.Map as Map #endif import Test.QuickCheck import Agda.Utils.List (mcons) import Agda.Utils.Maybe.Strict -- | Finite map from @[k]@ to @v@. -- -- With the strict 'Maybe' type, 'Trie' is also strict in 'v'. data Trie k v = Trie !(Maybe v) !(Map k (Trie k v)) deriving Show -- | Empty trie. empty :: Trie k v empty = Trie Nothing Map.empty -- | Singleton trie. singleton :: [k] -> v -> Trie k v singleton [] !v = Trie (Just v) Map.empty singleton (x:xs) !v = Trie Nothing $ Map.singleton x (singleton xs v) -- | Left biased union. -- -- @union = unionWith (\ new old -> new)@. union :: (Ord k) => Trie k v -> Trie k v -> Trie k v union = unionWith const -- | Pointwise union with merge function for values. unionWith :: (Ord k) => (v -> v -> v) -> Trie k v -> Trie k v -> Trie k v unionWith f (Trie v ss) (Trie w ts) = Trie (unionMaybeWith f v w) (Map.unionWith (unionWith f) ss ts) -- | Insert. Overwrites existing value if present. -- -- @insert = insertWith (\ new old -> new)@ insert :: (Ord k) => [k] -> v -> Trie k v -> Trie k v insert k v t = union (singleton k v) t -- | Insert with function merging new value with old value. insertWith :: (Ord k) => (v -> v -> v) -> [k] -> v -> Trie k v -> Trie k v insertWith f k v t = unionWith f (singleton k v) t -- | Delete value at key, but leave subtree intact. delete :: Ord k => [k] -> Trie k v -> Trie k v delete path = adjust path (const Nothing) -- | Adjust value at key, leave subtree intact. adjust :: Ord k => [k] -> (Maybe v -> Maybe v) -> Trie k v -> Trie k v adjust path f t@(Trie v ts) = case path of -- case: found the value we want to adjust: adjust it! [] -> Trie (f v) ts -- case: found the subtrie matching the first key: adjust recursively k : ks | Lazy.Just s <- Map.lookup k ts -> Trie v $ Map.insert k (adjust ks f s) ts -- case: subtrie not found: leave trie untouched _ -> t -- | Convert to ascending list. toList :: Ord k => Trie k v -> [([k],v)] toList = toAscList -- | Convert to ascending list. toAscList :: Ord k => Trie k v -> [([k],v)] toAscList (Trie mv ts) = maybeToList (([],) <$> mv) ++ [ (k:ks, v) | (k, t) <- Map.toAscList ts , (ks, v) <- toAscList t ] -- | Collect all values along a given path. lookupPath :: Ord k => [k] -> Trie k v -> [v] lookupPath xs (Trie v cs) = case xs of [] -> maybeToList v x : xs -> maybeToList v ++ Lazy.maybe [] (lookupPath xs) (Map.lookup x cs) -- Tests ------------------------------------------------------------------ newtype Key = Key Int deriving (Eq, Ord) newtype Val = Val Int deriving (Eq) newtype Model = Model [([Key], Val)] deriving (Eq, Show) instance Show Key where show (Key x) = show x instance Show Val where show (Val x) = show x instance Arbitrary Key where arbitrary = elements $ map Key [1..2] shrink (Key x) = Key <$> shrink x instance Arbitrary Val where arbitrary = elements $ map Val [1..3] shrink (Val x) = Val <$> shrink x instance Arbitrary Model where arbitrary = Model <$> arbitrary shrink (Model xs) = Model <$> shrink xs modelToTrie :: Model -> Trie Key Val modelToTrie (Model xs) = foldr (uncurry insert) empty xs modelPath :: [Key] -> Model -> [Val] modelPath ks (Model xs) = map snd $ sortBy (compare `on` length . fst) $ nubBy ((==) `on` fst) $ filter (flip isPrefixOf ks . fst) xs prop_path :: [Key] -> Model -> Property prop_path ks m = collect (length $ modelPath ks m) $ lookupPath ks (modelToTrie m) == modelPath ks m