module Language.Haskell.Liquid.Bag where
import qualified Data.Map as M
type Bag a = M.Map a Int
empty :: Bag k
empty :: Bag k
empty = Bag k
forall k a. Map k a
M.empty
bagSize :: Bag k -> Int
bagSize :: Bag k -> Int
bagSize Bag k
b = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (Bag k -> [Int]
forall k a. Map k a -> [a]
M.elems Bag k
b)
fromList :: (Ord k) => [k] -> Bag k
fromList :: [k] -> Bag k
fromList [] = Bag k
forall k. Bag k
empty
fromList (k
x:[k]
xs) = k -> Bag k -> Bag k
forall k. Ord k => k -> Bag k -> Bag k
put k
x ([k] -> Bag k
forall k. Ord k => [k] -> Bag k
fromList [k]
xs)
get :: (Ord k) => k -> Bag k -> Int
get :: k -> Bag k -> Int
get k
k Bag k
m = Int -> k -> Bag k -> Int
forall k a. Ord k => a -> k -> Map k a -> a
M.findWithDefault Int
0 k
k Bag k
m
put :: (Ord k) => k -> Bag k -> Bag k
put :: k -> Bag k -> Bag k
put k
k Bag k
m = k -> Int -> Bag k -> Bag k
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert k
k (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ k -> Bag k -> Int
forall k. Ord k => k -> Bag k -> Int
get k
k Bag k
m) Bag k
m
union :: (Ord k) => Bag k -> Bag k -> Bag k
union :: Bag k -> Bag k -> Bag k
union Bag k
m1 Bag k
m2 = Bag k -> Bag k -> Bag k
forall k a. Ord k => Map k a -> Map k a -> Map k a
M.union Bag k
m1 Bag k
m2
thm_emp :: (Ord k) => k -> Bag k -> ()
thm_emp :: k -> Bag k -> ()
thm_emp k
x Bag k
xs = () -> Int -> ()
forall a b. a -> b -> a
const () (k -> Bag k -> Int
forall k. Ord k => k -> Bag k -> Int
get k
x Bag k
xs)
thm_size :: (Ord k) => [k] -> ()
thm_size :: [k] -> ()
thm_size [k]
_ = ()