{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
module Data.Parameterized.FinMap.Unsafe
( FinMap
, null
, lookup
, size
, incMax
, embed
, empty
, singleton
, insert
, buildFinMap
, append
, fromVector
, delete
, decMax
, mapWithKey
, unionWithKey
, unionWith
, union
) where
import Prelude hiding (lookup, null)
import Data.Functor.WithIndex (FunctorWithIndex(imap))
import Data.Foldable.WithIndex (FoldableWithIndex(ifoldMap))
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import GHC.TypeLits (KnownNat, Nat)
import Numeric.Natural (Natural)
import Unsafe.Coerce (unsafeCoerce)
import Data.Parameterized.Fin (Fin, mkFin)
import qualified Data.Parameterized.Fin as Fin
import Data.Parameterized.NatRepr (LeqProof, NatRepr, type (+), type (<=))
import qualified Data.Parameterized.NatRepr as NatRepr
import Data.Parameterized.Some (Some(Some))
import Data.Parameterized.Vector (Vector)
import qualified Data.Parameterized.Vector as Vec
intToNat :: Int -> Natural
intToNat :: Int -> Natural
intToNat = Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral
{-# INLINE intToNat #-}
unsafeFinToInt :: Fin n -> Int
unsafeFinToInt :: forall (n :: Natural). Fin n -> Int
unsafeFinToInt = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> (Fin n -> Natural) -> Fin n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin n -> Natural
forall (n :: Natural). Fin n -> Natural
Fin.finToNat
{-# INLINE unsafeFinToInt #-}
unsafeNatReprToInt :: NatRepr n -> Int
unsafeNatReprToInt :: forall (n :: Natural). NatRepr n -> Int
unsafeNatReprToInt = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> (NatRepr n -> Natural) -> NatRepr n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NatRepr n -> Natural
forall (n :: Natural). NatRepr n -> Natural
NatRepr.natValue
{-# INLINE unsafeNatReprToInt #-}
newtype FinMap (n :: Nat) a = FinMap { forall (n :: Natural) a. FinMap n a -> IntMap a
getFinMap :: IntMap a }
instance Eq a => Eq (FinMap n a) where
FinMap n a
fm1 == :: FinMap n a -> FinMap n a -> Bool
== FinMap n a
fm2 = FinMap n a -> IntMap a
forall (n :: Natural) a. FinMap n a -> IntMap a
getFinMap FinMap n a
fm1 IntMap a -> IntMap a -> Bool
forall a. Eq a => a -> a -> Bool
== FinMap n a -> IntMap a
forall (n :: Natural) a. FinMap n a -> IntMap a
getFinMap FinMap n a
fm2
{-# INLINABLE (==) #-}
instance Semigroup (FinMap n a) where
<> :: FinMap n a -> FinMap n a -> FinMap n a
(<>) = FinMap n a -> FinMap n a -> FinMap n a
forall (n :: Natural) a. FinMap n a -> FinMap n a -> FinMap n a
union
{-# INLINE (<>) #-}
instance KnownNat n => Monoid (FinMap n a) where
mempty :: FinMap n a
mempty = FinMap n a
forall (n :: Natural) a. KnownNat n => FinMap n a
empty
{-# INLINE mempty #-}
instance Functor (FinMap n) where
fmap :: forall a b. (a -> b) -> FinMap n a -> FinMap n b
fmap a -> b
f = IntMap b -> FinMap n b
forall (n :: Natural) a. IntMap a -> FinMap n a
FinMap (IntMap b -> FinMap n b)
-> (FinMap n a -> IntMap b) -> FinMap n a -> FinMap n b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b) -> IntMap a -> IntMap b
forall a b. (a -> b) -> IntMap a -> IntMap b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f (IntMap a -> IntMap b)
-> (FinMap n a -> IntMap a) -> FinMap n a -> IntMap b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FinMap n a -> IntMap a
forall (n :: Natural) a. FinMap n a -> IntMap a
getFinMap
{-# INLINABLE fmap #-}
instance Foldable (FinMap n) where
foldMap :: forall m a. Monoid m => (a -> m) -> FinMap n a -> m
foldMap a -> m
f = (a -> m) -> IntMap a -> m
forall m a. Monoid m => (a -> m) -> IntMap a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f (IntMap a -> m) -> (FinMap n a -> IntMap a) -> FinMap n a -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FinMap n a -> IntMap a
forall (n :: Natural) a. FinMap n a -> IntMap a
getFinMap
{-# INLINABLE foldMap #-}
instance Traversable (FinMap n) where
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> FinMap n a -> f (FinMap n b)
traverse a -> f b
f FinMap n a
fm = IntMap b -> FinMap n b
forall (n :: Natural) a. IntMap a -> FinMap n a
FinMap (IntMap b -> FinMap n b) -> f (IntMap b) -> f (FinMap n b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> f b) -> IntMap a -> f (IntMap b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> IntMap a -> f (IntMap b)
traverse a -> f b
f (FinMap n a -> IntMap a
forall (n :: Natural) a. FinMap n a -> IntMap a
getFinMap FinMap n a
fm)
instance FunctorWithIndex (Fin n) (FinMap n) where
imap :: forall a b. (Fin n -> a -> b) -> FinMap n a -> FinMap n b
imap Fin n -> a -> b
f = IntMap b -> FinMap n b
forall (n :: Natural) a. IntMap a -> FinMap n a
FinMap (IntMap b -> FinMap n b)
-> (FinMap n a -> IntMap b) -> FinMap n a -> FinMap n b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> a -> b) -> IntMap a -> IntMap b
forall a b. (Int -> a -> b) -> IntMap a -> IntMap b
IntMap.mapWithKey (Fin n -> a -> b
f (Fin n -> a -> b) -> (Int -> Fin n) -> Int -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Fin n
forall (n :: Natural). Int -> Fin n
unsafeFin) (IntMap a -> IntMap b)
-> (FinMap n a -> IntMap a) -> FinMap n a -> IntMap b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FinMap n a -> IntMap a
forall (n :: Natural) a. FinMap n a -> IntMap a
getFinMap
{-# INLINE imap #-}
instance FoldableWithIndex (Fin n) (FinMap n) where
ifoldMap :: forall m a. Monoid m => (Fin n -> a -> m) -> FinMap n a -> m
ifoldMap Fin n -> a -> m
f = (Int -> a -> m) -> IntMap a -> m
forall m a. Monoid m => (Int -> a -> m) -> IntMap a -> m
IntMap.foldMapWithKey (Fin n -> a -> m
f (Fin n -> a -> m) -> (Int -> Fin n) -> Int -> a -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Fin n
forall (n :: Natural). Int -> Fin n
unsafeFin) (IntMap a -> m) -> (FinMap n a -> IntMap a) -> FinMap n a -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FinMap n a -> IntMap a
forall (n :: Natural) a. FinMap n a -> IntMap a
getFinMap
instance Show a => Show (FinMap n a) where
show :: FinMap n a -> String
show FinMap n a
fm = IntMap a -> String
forall a. Show a => a -> String
show (FinMap n a -> IntMap a
forall (n :: Natural) a. FinMap n a -> IntMap a
getFinMap FinMap n a
fm)
{-# INLINABLE show #-}
null :: FinMap n a -> Bool
null :: forall (n :: Natural) a. FinMap n a -> Bool
null = IntMap a -> Bool
forall a. IntMap a -> Bool
IntMap.null (IntMap a -> Bool)
-> (FinMap n a -> IntMap a) -> FinMap n a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FinMap n a -> IntMap a
forall (n :: Natural) a. FinMap n a -> IntMap a
getFinMap
{-# INLINABLE null #-}
lookup :: Fin n -> FinMap n a -> Maybe a
lookup :: forall (n :: Natural) a. Fin n -> FinMap n a -> Maybe a
lookup Fin n
k = Int -> IntMap a -> Maybe a
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup (Fin n -> Int
forall (n :: Natural). Fin n -> Int
unsafeFinToInt Fin n
k) (IntMap a -> Maybe a)
-> (FinMap n a -> IntMap a) -> FinMap n a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FinMap n a -> IntMap a
forall (n :: Natural) a. FinMap n a -> IntMap a
getFinMap
{-# INLINABLE lookup #-}
unsafeFin :: forall n. Int -> Fin n
unsafeFin :: forall (n :: Natural). Int -> Fin n
unsafeFin Int
i =
case Natural -> Some NatRepr
NatRepr.mkNatRepr (Int -> Natural
intToNat Int
i) of
Some (NatRepr x
repr :: NatRepr m) ->
case LeqProof 0 0 -> LeqProof (x + 1) n
forall a b. a -> b
unsafeCoerce (LeqProof 0 0
forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
NatRepr.LeqProof :: LeqProof 0 0) :: LeqProof (m + 1) n of
LeqProof (x + 1) n
NatRepr.LeqProof -> forall (i :: Natural) (n :: Natural).
((i + 1) <= n) =>
NatRepr i -> Fin n
mkFin @m @n NatRepr x
repr
size :: forall n a. FinMap n a -> Fin (n + 1)
size :: forall (n :: Natural) a. FinMap n a -> Fin (n + 1)
size = Int -> Fin (n + 1)
forall (n :: Natural). Int -> Fin n
unsafeFin (Int -> Fin (n + 1))
-> (FinMap n a -> Int) -> FinMap n a -> Fin (n + 1)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntMap a -> Int
forall a. IntMap a -> Int
IntMap.size (IntMap a -> Int) -> (FinMap n a -> IntMap a) -> FinMap n a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FinMap n a -> IntMap a
forall (n :: Natural) a. FinMap n a -> IntMap a
getFinMap
{-# INLINEABLE size #-}
incMax :: FinMap n a -> FinMap (n + 1) a
incMax :: forall (n :: Natural) a. FinMap n a -> FinMap (n + 1) a
incMax = IntMap a -> FinMap (n + 1) a
forall (n :: Natural) a. IntMap a -> FinMap n a
FinMap (IntMap a -> FinMap (n + 1) a)
-> (FinMap n a -> IntMap a) -> FinMap n a -> FinMap (n + 1) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FinMap n a -> IntMap a
forall (n :: Natural) a. FinMap n a -> IntMap a
getFinMap
{-# INLINE incMax #-}
embed :: (n <= m) => NatRepr m -> FinMap n a -> FinMap m a
embed :: forall (n :: Natural) (m :: Natural) a.
(n <= m) =>
NatRepr m -> FinMap n a -> FinMap m a
embed NatRepr m
_ = IntMap a -> FinMap m a
forall (n :: Natural) a. IntMap a -> FinMap n a
FinMap (IntMap a -> FinMap m a)
-> (FinMap n a -> IntMap a) -> FinMap n a -> FinMap m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FinMap n a -> IntMap a
forall (n :: Natural) a. FinMap n a -> IntMap a
getFinMap
{-# INLINE embed #-}
empty :: KnownNat n => FinMap n a
empty :: forall (n :: Natural) a. KnownNat n => FinMap n a
empty = IntMap a -> FinMap n a
forall (n :: Natural) a. IntMap a -> FinMap n a
FinMap IntMap a
forall a. IntMap a
IntMap.empty
{-# INLINE empty #-}
singleton :: a -> FinMap 1 a
singleton :: forall a. a -> FinMap 1 a
singleton = IntMap a -> FinMap 1 a
forall (n :: Natural) a. IntMap a -> FinMap n a
FinMap (IntMap a -> FinMap 1 a) -> (a -> IntMap a) -> a -> FinMap 1 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a -> IntMap a
forall a. Int -> a -> IntMap a
IntMap.singleton Int
0
{-# INLINABLE singleton #-}
insert :: Fin n -> a -> FinMap n a -> FinMap n a
insert :: forall (n :: Natural) a. Fin n -> a -> FinMap n a -> FinMap n a
insert Fin n
k a
v = IntMap a -> FinMap n a
forall (n :: Natural) a. IntMap a -> FinMap n a
FinMap (IntMap a -> FinMap n a)
-> (FinMap n a -> IntMap a) -> FinMap n a -> FinMap n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a -> IntMap a -> IntMap a
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert (Fin n -> Int
forall (n :: Natural). Fin n -> Int
unsafeFinToInt Fin n
k) a
v (IntMap a -> IntMap a)
-> (FinMap n a -> IntMap a) -> FinMap n a -> IntMap a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FinMap n a -> IntMap a
forall (n :: Natural) a. FinMap n a -> IntMap a
getFinMap
{-# INLINABLE insert #-}
newtype FinMap' a (n :: Nat) = FinMap' { forall a (n :: Natural). FinMap' a n -> FinMap n a
unFinMap' :: FinMap n a }
buildFinMap ::
forall m a.
NatRepr m ->
(forall n. (n + 1 <= m) => NatRepr n -> FinMap n a -> FinMap (n + 1) a) ->
FinMap m a
buildFinMap :: forall (m :: Natural) a.
NatRepr m
-> (forall (n :: Natural).
((n + 1) <= m) =>
NatRepr n -> FinMap n a -> FinMap (n + 1) a)
-> FinMap m a
buildFinMap NatRepr m
m forall (n :: Natural).
((n + 1) <= m) =>
NatRepr n -> FinMap n a -> FinMap (n + 1) a
f =
let f' :: forall k. (k + 1 <= m) => NatRepr k -> FinMap' a k -> FinMap' a (k + 1)
f' :: forall (k :: Natural).
((k + 1) <= m) =>
NatRepr k -> FinMap' a k -> FinMap' a (k + 1)
f' = (\NatRepr k
n (FinMap' FinMap k a
fin) -> FinMap (k + 1) a -> FinMap' a (k + 1)
forall a (n :: Natural). FinMap n a -> FinMap' a n
FinMap' (NatRepr k -> FinMap k a -> FinMap (k + 1) a
forall (n :: Natural).
((n + 1) <= m) =>
NatRepr n -> FinMap n a -> FinMap (n + 1) a
f NatRepr k
n FinMap k a
fin))
in FinMap' a m -> FinMap m a
forall a (n :: Natural). FinMap' a n -> FinMap n a
unFinMap' (NatRepr m
-> FinMap' a 0
-> (forall (k :: Natural).
((k + 1) <= m) =>
NatRepr k -> FinMap' a k -> FinMap' a (k + 1))
-> FinMap' a m
forall (m :: Natural) (f :: Natural -> *).
NatRepr m
-> f 0
-> (forall (n :: Natural).
((n + 1) <= m) =>
NatRepr n -> f n -> f (n + 1))
-> f m
NatRepr.natRecStrictlyBounded NatRepr m
m (FinMap 0 a -> FinMap' a 0
forall a (n :: Natural). FinMap n a -> FinMap' a n
FinMap' FinMap 0 a
forall (n :: Natural) a. KnownNat n => FinMap n a
empty) NatRepr n -> FinMap' a n -> FinMap' a (n + 1)
forall (k :: Natural).
((k + 1) <= m) =>
NatRepr k -> FinMap' a k -> FinMap' a (k + 1)
f')
append :: NatRepr n -> a -> FinMap n a -> FinMap (n + 1) a
append :: forall (n :: Natural) a.
NatRepr n -> a -> FinMap n a -> FinMap (n + 1) a
append NatRepr n
k a
v FinMap n a
fm =
case NatRepr n -> LeqProof n (n + 1)
forall (f :: Natural -> *) (z :: Natural).
f z -> LeqProof z (z + 1)
NatRepr.leqSucc NatRepr n
k of
LeqProof n (n + 1)
NatRepr.LeqProof -> Fin (n + 1) -> a -> FinMap (n + 1) a -> FinMap (n + 1) a
forall (n :: Natural) a. Fin n -> a -> FinMap n a -> FinMap n a
insert (NatRepr n -> Fin (n + 1)
forall (i :: Natural) (n :: Natural).
((i + 1) <= n) =>
NatRepr i -> Fin n
mkFin NatRepr n
k) a
v (FinMap n a -> FinMap (n + 1) a
forall (n :: Natural) a. FinMap n a -> FinMap (n + 1) a
incMax FinMap n a
fm)
fromVector :: forall n a. Vector n (Maybe a) -> FinMap n a
fromVector :: forall (n :: Natural) a. Vector n (Maybe a) -> FinMap n a
fromVector Vector n (Maybe a)
v =
NatRepr n
-> (forall (n :: Natural).
((n + 1) <= n) =>
NatRepr n -> FinMap n a -> FinMap (n + 1) a)
-> FinMap n a
forall (m :: Natural) a.
NatRepr m
-> (forall (n :: Natural).
((n + 1) <= m) =>
NatRepr n -> FinMap n a -> FinMap (n + 1) a)
-> FinMap m a
buildFinMap
(Vector n (Maybe a) -> NatRepr n
forall (n :: Natural) a. Vector n a -> NatRepr n
Vec.length Vector n (Maybe a)
v)
(\NatRepr n
k FinMap n a
m ->
case NatRepr n -> Vector n (Maybe a) -> Maybe a
forall (i :: Natural) (n :: Natural) a.
((i + 1) <= n) =>
NatRepr i -> Vector n a -> a
Vec.elemAt NatRepr n
k Vector n (Maybe a)
v of
Just a
e -> NatRepr n -> a -> FinMap n a -> FinMap (n + 1) a
forall (n :: Natural) a.
NatRepr n -> a -> FinMap n a -> FinMap (n + 1) a
append NatRepr n
k a
e FinMap n a
m
Maybe a
Nothing -> FinMap n a -> FinMap (n + 1) a
forall (n :: Natural) a. FinMap n a -> FinMap (n + 1) a
incMax FinMap n a
m)
delete :: Fin n -> FinMap n a -> FinMap n a
delete :: forall (n :: Natural) a. Fin n -> FinMap n a -> FinMap n a
delete Fin n
k = IntMap a -> FinMap n a
forall (n :: Natural) a. IntMap a -> FinMap n a
FinMap (IntMap a -> FinMap n a)
-> (FinMap n a -> IntMap a) -> FinMap n a -> FinMap n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> IntMap a -> IntMap a
forall a. Int -> IntMap a -> IntMap a
IntMap.delete (Fin n -> Int
forall (n :: Natural). Fin n -> Int
unsafeFinToInt Fin n
k) (IntMap a -> IntMap a)
-> (FinMap n a -> IntMap a) -> FinMap n a -> IntMap a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FinMap n a -> IntMap a
forall (n :: Natural) a. FinMap n a -> IntMap a
getFinMap
{-# INLINABLE delete #-}
decMax :: NatRepr n -> FinMap (n + 1) a -> FinMap n a
decMax :: forall (n :: Natural) a.
NatRepr n -> FinMap (n + 1) a -> FinMap n a
decMax NatRepr n
k = IntMap a -> FinMap n a
forall (n :: Natural) a. IntMap a -> FinMap n a
FinMap (IntMap a -> FinMap n a)
-> (FinMap (n + 1) a -> IntMap a) -> FinMap (n + 1) a -> FinMap n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> IntMap a -> IntMap a
forall a. Int -> IntMap a -> IntMap a
IntMap.delete (NatRepr n -> Int
forall (n :: Natural). NatRepr n -> Int
unsafeNatReprToInt NatRepr n
k) (IntMap a -> IntMap a)
-> (FinMap (n + 1) a -> IntMap a) -> FinMap (n + 1) a -> IntMap a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FinMap (n + 1) a -> IntMap a
forall (n :: Natural) a. FinMap n a -> IntMap a
getFinMap
{-# INLINABLE decMax #-}
mapWithKey :: (Fin n -> a -> b) -> FinMap n a -> FinMap n b
mapWithKey :: forall (n :: Natural) a b.
(Fin n -> a -> b) -> FinMap n a -> FinMap n b
mapWithKey Fin n -> a -> b
f = IntMap b -> FinMap n b
forall (n :: Natural) a. IntMap a -> FinMap n a
FinMap (IntMap b -> FinMap n b)
-> (FinMap n a -> IntMap b) -> FinMap n a -> FinMap n b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> a -> b) -> IntMap a -> IntMap b
forall a b. (Int -> a -> b) -> IntMap a -> IntMap b
IntMap.mapWithKey (Fin n -> a -> b
f (Fin n -> a -> b) -> (Int -> Fin n) -> Int -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Fin n
forall (n :: Natural). Int -> Fin n
unsafeFin) (IntMap a -> IntMap b)
-> (FinMap n a -> IntMap a) -> FinMap n a -> IntMap b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FinMap n a -> IntMap a
forall (n :: Natural) a. FinMap n a -> IntMap a
getFinMap
{-# INLINE mapWithKey #-}
unionWithKey :: (Fin n -> a -> a -> a) -> FinMap n a -> FinMap n a -> FinMap n a
unionWithKey :: forall (n :: Natural) a.
(Fin n -> a -> a -> a) -> FinMap n a -> FinMap n a -> FinMap n a
unionWithKey Fin n -> a -> a -> a
f FinMap n a
fm1 FinMap n a
fm2 =
IntMap a -> FinMap n a
forall (n :: Natural) a. IntMap a -> FinMap n a
FinMap ((Int -> a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
forall a. (Int -> a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
IntMap.unionWithKey (Fin n -> a -> a -> a
f (Fin n -> a -> a -> a) -> (Int -> Fin n) -> Int -> a -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Fin n
forall (n :: Natural). Int -> Fin n
unsafeFin) (FinMap n a -> IntMap a
forall (n :: Natural) a. FinMap n a -> IntMap a
getFinMap FinMap n a
fm1) (FinMap n a -> IntMap a
forall (n :: Natural) a. FinMap n a -> IntMap a
getFinMap FinMap n a
fm2))
unionWith :: (a -> a -> a) -> FinMap n a -> FinMap n a -> FinMap n a
unionWith :: forall a (n :: Natural).
(a -> a -> a) -> FinMap n a -> FinMap n a -> FinMap n a
unionWith a -> a -> a
f = (Fin n -> a -> a -> a) -> FinMap n a -> FinMap n a -> FinMap n a
forall (n :: Natural) a.
(Fin n -> a -> a -> a) -> FinMap n a -> FinMap n a -> FinMap n a
unionWithKey (\Fin n
_ a
v1 a
v2 -> a -> a -> a
f a
v1 a
v2)
union :: FinMap n a -> FinMap n a -> FinMap n a
union :: forall (n :: Natural) a. FinMap n a -> FinMap n a -> FinMap n a
union = (a -> a -> a) -> FinMap n a -> FinMap n a -> FinMap n a
forall a (n :: Natural).
(a -> a -> a) -> FinMap n a -> FinMap n a -> FinMap n a
unionWith a -> a -> a
forall a b. a -> b -> a
const