{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Effect.OpenUnion.Internal.FO where
import Data.Coerce (coerce)
import Data.Effect (EffectF)
import Data.Effect.Key (type (#>))
import Data.Effect.OpenUnion.Internal (
BundleUnder,
Drop,
ElemAt,
ElemIndex,
FindElem,
IfKeyNotFound,
IfNotFound,
IsSuffixOf,
KnownLength,
Length,
P (unP),
PrefixLength,
Reverse,
Split,
Strengthen,
StrengthenN,
StrengthenNUnder,
StrengthenUnder,
Take,
WeakenN,
WeakenNUnder,
WeakenUnder,
elemNo,
prefixLen,
reifyLength,
strengthenMap,
strengthenMapUnder,
wordVal,
type (++),
)
import Data.Kind (Type)
import GHC.TypeNats (KnownNat, type (-))
import Unsafe.Coerce (unsafeCoerce)
data Union (es :: [EffectF]) (a :: Type) where
Union
:: {-# UNPACK #-} !Word
-> e a
-> Union es a
unsafeInj :: Word -> e a -> Union es a
unsafeInj :: forall (e :: * -> *) a (es :: [* -> *]). Word -> e a -> Union es a
unsafeInj = Word -> e a -> Union es a
forall (e :: * -> *) a (es :: [* -> *]). Word -> e a -> Union es a
Union
{-# INLINE unsafeInj #-}
unsafePrj :: Word -> Union es a -> Maybe (e a)
unsafePrj :: forall (es :: [* -> *]) a (e :: * -> *).
Word -> Union es a -> Maybe (e a)
unsafePrj Word
n (Union Word
n' e a
e)
| Word
n Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
n' = e a -> Maybe (e a)
forall a. a -> Maybe a
Just (e a -> e a
forall a b. a -> b
unsafeCoerce e a
e)
| Bool
otherwise = Maybe (e a)
forall a. Maybe a
Nothing
{-# INLINE unsafePrj #-}
class (FindElem e es) => Member (e :: EffectF) es where
inj :: e a -> Union es a
prj :: Union es a -> Maybe (e a)
instance (FindElem e es, IfNotFound e es es) => Member e es where
inj :: forall a. e a -> Union es a
inj = Word -> e a -> Union es a
forall (e :: * -> *) a (es :: [* -> *]). Word -> e a -> Union es a
unsafeInj (Word -> e a -> Union es a) -> Word -> e a -> Union es a
forall a b. (a -> b) -> a -> b
$ P e es -> Word
forall k (e :: k) (es :: [k]). P e es -> Word
unP (P e es
forall {k} (e :: k) (es :: [k]). FindElem e es => P e es
elemNo :: P e es)
{-# INLINE inj #-}
prj :: forall a. Union es a -> Maybe (e a)
prj = Word -> Union es a -> Maybe (e a)
forall (es :: [* -> *]) a (e :: * -> *).
Word -> Union es a -> Maybe (e a)
unsafePrj (Word -> Union es a -> Maybe (e a))
-> Word -> Union es a -> Maybe (e a)
forall a b. (a -> b) -> a -> b
$ P e es -> Word
forall k (e :: k) (es :: [k]). P e es -> Word
unP (P e es
forall {k} (e :: k) (es :: [k]). FindElem e es => P e es
elemNo :: P e es)
{-# INLINE prj #-}
infix 3 <|
type (<|) = Member
type MemberBy key e es = (key #> e <| es, Lookup key es ~ key #> e, IfKeyNotFound key es es)
type family Lookup (key :: k) r :: EffectF where
Lookup key (key #> e ': _) = key #> e
Lookup key (_ ': r) = Lookup key r
decomp :: Union (e ': es) a -> Either (Union es a) (e a)
decomp :: forall (e :: * -> *) (es :: [* -> *]) a.
Union (e : es) a -> Either (Union es a) (e a)
decomp (Union Word
0 e a
a) = e a -> Either (Union es a) (e a)
forall a b. b -> Either a b
Right (e a -> Either (Union es a) (e a))
-> e a -> Either (Union es a) (e a)
forall a b. (a -> b) -> a -> b
$ e a -> e a
forall a b. a -> b
unsafeCoerce e a
a
decomp (Union Word
n e a
a) = Union es a -> Either (Union es a) (e a)
forall a b. a -> Either a b
Left (Union es a -> Either (Union es a) (e a))
-> Union es a -> Either (Union es a) (e a)
forall a b. (a -> b) -> a -> b
$ Word -> e a -> Union es a
forall (e :: * -> *) a (es :: [* -> *]). Word -> e a -> Union es a
Union (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
1) e a
a
{-# INLINE [2] decomp #-}
decomp0 :: Union '[e] a -> Either (Union '[] a) (e a)
decomp0 :: forall (e :: * -> *) a. Union '[e] a -> Either (Union '[] a) (e a)
decomp0 (Union Word
_ e a
a) = e a -> Either (Union '[] a) (e a)
forall a b. b -> Either a b
Right (e a -> Either (Union '[] a) (e a))
-> e a -> Either (Union '[] a) (e a)
forall a b. (a -> b) -> a -> b
$ e a -> e a
forall a b. a -> b
unsafeCoerce e a
a
{-# INLINE decomp0 #-}
{-# RULES "decomp/singleton" decomp = decomp0 #-}
infixr 5 !+
(!+) :: (e a -> r) -> (Union es a -> r) -> Union (e : es) a -> r
(e a -> r
f !+ :: forall (e :: * -> *) a r (es :: [* -> *]).
(e a -> r) -> (Union es a -> r) -> Union (e : es) a -> r
!+ Union es a -> r
g) Union (e : es) a
u = case Union (e : es) a -> Either (Union es a) (e a)
forall (e :: * -> *) (es :: [* -> *]) a.
Union (e : es) a -> Either (Union es a) (e a)
decomp Union (e : es) a
u of
Left Union es a
x -> Union es a -> r
g Union es a
x
Right e a
x -> e a -> r
f e a
x
{-# INLINE (!+) #-}
extract :: Union '[e] a -> e a
(Union Word
_ e a
a) = e a -> e a
forall a b. a -> b
unsafeCoerce e a
a
{-# INLINE extract #-}
inj0 :: forall e es a. e a -> Union (e ': es) a
inj0 :: forall (e :: * -> *) (es :: [* -> *]) a. e a -> Union (e : es) a
inj0 = Word -> e a -> Union (e : es) a
forall (e :: * -> *) a (es :: [* -> *]). Word -> e a -> Union es a
Union Word
0
{-# INLINE inj0 #-}
injN :: forall i es a. (KnownNat i) => ElemAt i es a -> Union es a
injN :: forall (i :: Nat) (es :: [* -> *]) a.
KnownNat i =>
ElemAt i es a -> Union es a
injN = Word -> ElemAt i es a -> Union es a
forall (e :: * -> *) a (es :: [* -> *]). Word -> e a -> Union es a
Union (forall (n :: Nat). KnownNat n => Word
wordVal @i)
{-# INLINE injN #-}
prjN :: forall i es a. (KnownNat i) => Union es a -> Maybe (ElemAt i es a)
prjN :: forall (i :: Nat) (es :: [* -> *]) a.
KnownNat i =>
Union es a -> Maybe (ElemAt i es a)
prjN (Union Word
n e a
a)
| Word
n Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== forall (n :: Nat). KnownNat n => Word
wordVal @i = ElemAt i es a -> Maybe (ElemAt i es a)
forall a. a -> Maybe a
Just (ElemAt i es a -> Maybe (ElemAt i es a))
-> ElemAt i es a -> Maybe (ElemAt i es a)
forall a b. (a -> b) -> a -> b
$ e a -> ElemAt i es a
forall a b. a -> b
unsafeCoerce e a
a
| Bool
otherwise = Maybe (ElemAt i es a)
forall a. Maybe a
Nothing
{-# INLINE prjN #-}
weaken :: forall any es a. Union es a -> Union (any ': es) a
weaken :: forall (any :: * -> *) (es :: [* -> *]) a.
Union es a -> Union (any : es) a
weaken (Union Word
n e a
a) = Word -> e a -> Union (any : es) a
forall (e :: * -> *) a (es :: [* -> *]). Word -> e a -> Union es a
Union (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
+ Word
1) e a
a
{-# INLINE weaken #-}
weakens :: forall es es' a. (es `IsSuffixOf` es') => Union es a -> Union es' a
weakens :: forall (es :: [* -> *]) (es' :: [* -> *]) a.
IsSuffixOf es es' =>
Union es a -> Union es' a
weakens (Union Word
n e a
a) = Word -> e a -> Union es' a
forall (e :: * -> *) a (es :: [* -> *]). Word -> e a -> Union es a
Union (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
+ forall (es :: [* -> *]) (es' :: [* -> *]).
IsSuffixOf es es' =>
Word
forall {k} {k1} (es :: k) (es' :: k1). IsSuffixOf es es' => Word
prefixLen @es @es') e a
a
{-# INLINE weakens #-}
weakenN :: forall len es es' a. (WeakenN len es es') => Union es a -> Union es' a
weakenN :: forall (len :: Nat) (es :: [* -> *]) (es' :: [* -> *]) a.
WeakenN len es es' =>
Union es a -> Union es' a
weakenN (Union Word
n e a
a) = Word -> e a -> Union es' a
forall (e :: * -> *) a (es :: [* -> *]). Word -> e a -> Union es a
Union (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
+ forall (n :: Nat). KnownNat n => Word
wordVal @len) e a
a
{-# INLINE weakenN #-}
weakenUnder :: forall any e es a. Union (e ': es) a -> Union (e ': any ': es) a
weakenUnder :: forall (any :: * -> *) (e :: * -> *) (es :: [* -> *]) a.
Union (e : es) a -> Union (e : any : es) a
weakenUnder u :: Union (e : es) a
u@(Union Word
n e a
a)
| Word
n Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
0 = Union (e : es) a -> Union (e : any : es) a
forall a b. Coercible a b => a -> b
coerce Union (e : es) a
u
| Bool
otherwise = Word -> e a -> Union (e : any : es) a
forall (e :: * -> *) a (es :: [* -> *]). Word -> e a -> Union es a
Union (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
+ Word
1) e a
a
{-# INLINE weakenUnder #-}
weakensUnder :: forall offset es es' a. (WeakenUnder offset es es') => Union es a -> Union es' a
weakensUnder :: forall (offset :: Nat) (es :: [* -> *]) (es' :: [* -> *]) a.
WeakenUnder offset es es' =>
Union es a -> Union es' a
weakensUnder = forall (len :: Nat) (offset :: Nat) (es :: [* -> *])
(es' :: [* -> *]) a.
WeakenNUnder len offset es es' =>
Union es a -> Union es' a
weakenNUnder @(PrefixLength es es') @offset
{-# INLINE weakensUnder #-}
weakenNUnder
:: forall len offset es es' a
. (WeakenNUnder len offset es es')
=> Union es a
-> Union es' a
weakenNUnder :: forall (len :: Nat) (offset :: Nat) (es :: [* -> *])
(es' :: [* -> *]) a.
WeakenNUnder len offset es es' =>
Union es a -> Union es' a
weakenNUnder u :: Union es a
u@(Union Word
n e a
a)
| Word
n Word -> Word -> Bool
forall a. Ord a => a -> a -> Bool
< forall (n :: Nat). KnownNat n => Word
wordVal @offset = Union es a -> Union es' a
forall a b. Coercible a b => a -> b
coerce Union es a
u
| Bool
otherwise = Word -> e a -> Union es' a
forall (e :: * -> *) a (es :: [* -> *]). Word -> e a -> Union es a
Union (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
+ forall (n :: Nat). KnownNat n => Word
wordVal @len) e a
a
{-# INLINE weakenNUnder #-}
strengthen :: forall e es a. (e <| es) => Union (e ': es) a -> Union es a
strengthen :: forall (e :: * -> *) (es :: [* -> *]) a.
(e <| es) =>
Union (e : es) a -> Union es a
strengthen (Union Word
n e a
a)
| Word
n Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
0 = Word -> e a -> Union es a
forall (e :: * -> *) a (es :: [* -> *]). Word -> e a -> Union es a
Union (forall (n :: Nat). KnownNat n => Word
wordVal @(ElemIndex e es)) e a
a
| Bool
otherwise = Word -> e a -> Union es a
forall (e :: * -> *) a (es :: [* -> *]). Word -> e a -> Union es a
Union (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
1) e a
a
{-# INLINE strengthen #-}
strengthens :: forall es es' a. (Strengthen es es') => Union es a -> Union es' a
strengthens :: forall (es :: [* -> *]) (es' :: [* -> *]) a.
Strengthen es es' =>
Union es a -> Union es' a
strengthens = forall (len :: Nat) (es :: [* -> *]) (es' :: [* -> *]) a.
StrengthenN len es es' =>
Union es a -> Union es' a
strengthenN @(PrefixLength es' es)
{-# INLINE strengthens #-}
strengthenN :: forall len es es' a. (StrengthenN len es es') => Union es a -> Union es' a
strengthenN :: forall (len :: Nat) (es :: [* -> *]) (es' :: [* -> *]) a.
StrengthenN len es es' =>
Union es a -> Union es' a
strengthenN (Union Word
n e a
a) = Word -> e a -> Union es' a
forall (e :: * -> *) a (es :: [* -> *]). Word -> e a -> Union es a
Union (forall k (isLenZero :: Bool) (len :: Nat) (es :: [k]) (es' :: [k]).
StrengthenMap_ isLenZero len es es' =>
Word -> Word
strengthenMap @_ @_ @len @es @es' Word
n) e a
a
{-# INLINE strengthenN #-}
strengthenUnder :: forall e2 e1 es a. (e2 <| es) => Union (e1 ': e2 ': es) a -> Union (e1 ': es) a
strengthenUnder :: forall (e2 :: * -> *) (e1 :: * -> *) (es :: [* -> *]) a.
(e2 <| es) =>
Union (e1 : e2 : es) a -> Union (e1 : es) a
strengthenUnder u :: Union (e1 : e2 : es) a
u@(Union Word
n e a
a)
| Word
n Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
0 = Union (e1 : e2 : es) a -> Union (e1 : es) a
forall a b. Coercible a b => a -> b
coerce Union (e1 : e2 : es) a
u
| Word
n Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
1 = Word -> e a -> Union (e1 : es) a
forall (e :: * -> *) a (es :: [* -> *]). Word -> e a -> Union es a
Union (Word
1 Word -> Word -> Word
forall a. Num a => a -> a -> a
+ forall (n :: Nat). KnownNat n => Word
wordVal @(ElemIndex e2 es)) e a
a
| Bool
otherwise = Word -> e a -> Union (e1 : es) a
forall (e :: * -> *) a (es :: [* -> *]). Word -> e a -> Union es a
Union (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
1) e a
a
{-# INLINE strengthenUnder #-}
strengthensUnder :: forall offset es es' a. (StrengthenUnder offset es es') => Union es a -> Union es' a
strengthensUnder :: forall (offset :: Nat) (es :: [* -> *]) (es' :: [* -> *]) a.
StrengthenUnder offset es es' =>
Union es a -> Union es' a
strengthensUnder = forall (len :: Nat) (offset :: Nat) (es :: [* -> *])
(es' :: [* -> *]) a.
StrengthenNUnder len offset es es' =>
Union es a -> Union es' a
strengthenNUnder @(PrefixLength es' es) @offset
{-# INLINE strengthensUnder #-}
strengthenNUnder
:: forall len offset es es' a
. (StrengthenNUnder len offset es es')
=> Union es a
-> Union es' a
strengthenNUnder :: forall (len :: Nat) (offset :: Nat) (es :: [* -> *])
(es' :: [* -> *]) a.
StrengthenNUnder len offset es es' =>
Union es a -> Union es' a
strengthenNUnder u :: Union es a
u@(Union Word
n e a
a)
| Word
n Word -> Word -> Bool
forall a. Ord a => a -> a -> Bool
< Word
off = Union es a -> Union es' a
forall a b. Coercible a b => a -> b
coerce Union es a
u
| Bool
otherwise = Word -> e a -> Union es' a
forall (e :: * -> *) a (es :: [* -> *]). Word -> e a -> Union es a
Union (Word
off Word -> Word -> Word
forall a. Num a => a -> a -> a
+ forall (len :: Nat) (offset :: Nat) (es :: [* -> *])
(es' :: [* -> *]).
StrengthenNUnder len offset es es' =>
Word -> Word
forall {k} (len :: Nat) (offset :: Nat) (es :: [k]) (es' :: [k]).
StrengthenNUnder len offset es es' =>
Word -> Word
strengthenMapUnder @len @offset @es @es' (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
off)) e a
a
where
off :: Word
off = forall (n :: Nat). KnownNat n => Word
wordVal @offset
{-# INLINE strengthenNUnder #-}
bundleUnion
:: forall es bundle rest a
. (Split es bundle rest)
=> Union es a
-> Union (Union bundle ': rest) a
bundleUnion :: forall (es :: [* -> *]) (bundle :: [* -> *]) (rest :: [* -> *]) a.
Split es bundle rest =>
Union es a -> Union (Union bundle : rest) a
bundleUnion = forall (len :: Nat) (es :: [* -> *]) a.
KnownNat len =>
Union es a -> Union (Union (Take len es) : Drop len es) a
bundleUnionN @(Length bundle)
bundleUnionN
:: forall len es a
. (KnownNat len)
=> Union es a
-> Union (Union (Take len es) ': Drop len es) a
bundleUnionN :: forall (len :: Nat) (es :: [* -> *]) a.
KnownNat len =>
Union es a -> Union (Union (Take len es) : Drop len es) a
bundleUnionN (Union Word
n e a
a)
| Word
n Word -> Word -> Bool
forall a. Ord a => a -> a -> Bool
< Word
len = Word -> Union Any a -> Union (Union (Take len es) : Drop len es) a
forall (e :: * -> *) a (es :: [* -> *]). Word -> e a -> Union es a
Union Word
0 (Union Any a -> Union (Union (Take len es) : Drop len es) a)
-> Union Any a -> Union (Union (Take len es) : Drop len es) a
forall a b. (a -> b) -> a -> b
$ Word -> e a -> Union Any a
forall (e :: * -> *) a (es :: [* -> *]). Word -> e a -> Union es a
Union Word
n e a
a
| Bool
otherwise = Word -> e a -> Union (Union (Take len es) : Drop len es) a
forall (e :: * -> *) a (es :: [* -> *]). Word -> e a -> Union es a
Union (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
len Word -> Word -> Word
forall a. Num a => a -> a -> a
+ Word
1) e a
a
where
len :: Word
len = forall (n :: Nat). KnownNat n => Word
wordVal @len
{-# INLINE bundleUnionN #-}
unbundleUnion
:: forall es bundle rest a
. (Split es bundle rest)
=> Union (Union bundle ': rest) a
-> Union es a
unbundleUnion :: forall (es :: [* -> *]) (bundle :: [* -> *]) (rest :: [* -> *]) a.
Split es bundle rest =>
Union (Union bundle : rest) a -> Union es a
unbundleUnion = forall (len :: Nat) (es :: [* -> *]) a.
KnownNat len =>
Union (Union (Take len es) : Drop len es) a -> Union es a
unbundleUnionN @(Length bundle)
{-# INLINE unbundleUnion #-}
unbundleUnionN
:: forall len es a
. (KnownNat len)
=> Union (Union (Take len es) ': Drop len es) a
-> Union es a
unbundleUnionN :: forall (len :: Nat) (es :: [* -> *]) a.
KnownNat len =>
Union (Union (Take len es) : Drop len es) a -> Union es a
unbundleUnionN (Union Word
n e a
a)
| Word
n Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
0 = e a -> Union es a
forall a b. a -> b
unsafeCoerce e a
a
| Bool
otherwise = Word -> e a -> Union es a
forall (e :: * -> *) a (es :: [* -> *]). Word -> e a -> Union es a
Union (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
1 Word -> Word -> Word
forall a. Num a => a -> a -> a
+ forall (n :: Nat). KnownNat n => Word
wordVal @len) e a
a
{-# INLINE unbundleUnionN #-}
bundleUnionUnder
:: forall offset bundle es es' a
. (BundleUnder Union offset es es' bundle)
=> Union es a
-> Union es' a
bundleUnionUnder :: forall (offset :: Nat) (bundle :: [* -> *]) (es :: [* -> *])
(es' :: [* -> *]) a.
BundleUnder Union offset es es' bundle =>
Union es a -> Union es' a
bundleUnionUnder = forall (len :: Nat) (offset :: Nat) (es :: [* -> *]) a.
(KnownNat len, KnownNat offset) =>
Union es a
-> Union
(Take offset es
++ (Union (Take len (Drop offset es)) : Drop len (Drop offset es)))
a
bundleUnionNUnder @(Length bundle) @offset
{-# INLINE bundleUnionUnder #-}
bundleUnionNUnder
:: forall len offset es a
. (KnownNat len, KnownNat offset)
=> Union es a
-> Union (Take offset es ++ (Union (Take len (Drop offset es)) ': Drop len (Drop offset es))) a
bundleUnionNUnder :: forall (len :: Nat) (offset :: Nat) (es :: [* -> *]) a.
(KnownNat len, KnownNat offset) =>
Union es a
-> Union
(Take offset es
++ (Union (Take len (Drop offset es)) : Drop len (Drop offset es)))
a
bundleUnionNUnder u :: Union es a
u@(Union Word
n e a
a)
| Word
n Word -> Word -> Bool
forall a. Ord a => a -> a -> Bool
< Word
off = Union es a
-> Union
(Take offset es
++ (Union (Take len (Drop offset es)) : Drop len (Drop offset es)))
a
forall a b. Coercible a b => a -> b
coerce Union es a
u
| Word
n' Word -> Word -> Bool
forall a. Ord a => a -> a -> Bool
< Word
len = Word
-> Union Any a
-> Union
(Take offset es
++ (Union (Take len (Drop offset es)) : Drop len (Drop offset es)))
a
forall (e :: * -> *) a (es :: [* -> *]). Word -> e a -> Union es a
Union Word
0 (Union Any a
-> Union
(Take offset es
++ (Union (Take len (Drop offset es)) : Drop len (Drop offset es)))
a)
-> Union Any a
-> Union
(Take offset es
++ (Union (Take len (Drop offset es)) : Drop len (Drop offset es)))
a
forall a b. (a -> b) -> a -> b
$ Word -> e a -> Union Any a
forall (e :: * -> *) a (es :: [* -> *]). Word -> e a -> Union es a
Union Word
n' e a
a
| Bool
otherwise = Word
-> e a
-> Union
(Take offset es
++ (Union (Take len (Drop offset es)) : Drop len (Drop offset es)))
a
forall (e :: * -> *) a (es :: [* -> *]). Word -> e a -> Union es a
Union (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
len Word -> Word -> Word
forall a. Num a => a -> a -> a
+ Word
1) e a
a
where
off :: Word
off = forall (n :: Nat). KnownNat n => Word
wordVal @offset
len :: Word
len = forall (n :: Nat). KnownNat n => Word
wordVal @len
n' :: Word
n' = Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
off
{-# INLINE bundleUnionNUnder #-}
unbundleUnionUnder
:: forall offset bundle es es' a
. (BundleUnder Union offset es es' bundle)
=> Union es' a
-> Union es a
unbundleUnionUnder :: forall (offset :: Nat) (bundle :: [* -> *]) (es :: [* -> *])
(es' :: [* -> *]) a.
BundleUnder Union offset es es' bundle =>
Union es' a -> Union es a
unbundleUnionUnder = forall (len :: Nat) (offset :: Nat) (es :: [* -> *]) a.
(KnownNat len, KnownNat offset) =>
Union
(Take offset es
++ (Union (Take len (Drop offset es)) : Drop len (Drop offset es)))
a
-> Union es a
unbundleUnionNUnder @(Length bundle) @offset
{-# INLINE unbundleUnionUnder #-}
unbundleUnionNUnder
:: forall len offset es a
. (KnownNat len, KnownNat offset)
=> Union (Take offset es ++ (Union (Take len (Drop offset es)) ': Drop len (Drop offset es))) a
-> Union es a
unbundleUnionNUnder :: forall (len :: Nat) (offset :: Nat) (es :: [* -> *]) a.
(KnownNat len, KnownNat offset) =>
Union
(Take offset es
++ (Union (Take len (Drop offset es)) : Drop len (Drop offset es)))
a
-> Union es a
unbundleUnionNUnder u :: Union
(Take offset es
++ (Union (Take len (Drop offset es)) : Drop len (Drop offset es)))
a
u@(Union Word
n e a
a)
| Word
n Word -> Word -> Bool
forall a. Ord a => a -> a -> Bool
< Word
off = Union
(Take offset es
++ (Union (Take len (Drop offset es)) : Drop len (Drop offset es)))
a
-> Union es a
forall a b. Coercible a b => a -> b
coerce Union
(Take offset es
++ (Union (Take len (Drop offset es)) : Drop len (Drop offset es)))
a
u
| Word
n Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
off =
case e a -> Union Any a
forall a b. a -> b
unsafeCoerce e a
a of
Union Word
n' e a
a' -> Word -> e a -> Union es a
forall (e :: * -> *) a (es :: [* -> *]). Word -> e a -> Union es a
Union (Word
off Word -> Word -> Word
forall a. Num a => a -> a -> a
+ Word
n') e a
a'
| Bool
otherwise = Word -> e a -> Union es a
forall (e :: * -> *) a (es :: [* -> *]). Word -> e a -> Union es a
Union (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
1 Word -> Word -> Word
forall a. Num a => a -> a -> a
+ Word
len) e a
a
where
off :: Word
off = forall (n :: Nat). KnownNat n => Word
wordVal @offset
len :: Word
len = forall (n :: Nat). KnownNat n => Word
wordVal @len
{-# INLINE unbundleUnionNUnder #-}
bundleAllUnion :: Union es a -> Union '[Union es] a
bundleAllUnion :: forall (es :: [* -> *]) a. Union es a -> Union '[Union es] a
bundleAllUnion = Word -> Union es a -> Union '[Union es] a
forall (e :: * -> *) a (es :: [* -> *]). Word -> e a -> Union es a
Union Word
0
{-# INLINE bundleAllUnion #-}
unbundleAllUnion :: Union '[Union es] a -> Union es a
unbundleAllUnion :: forall (es :: [* -> *]) a. Union '[Union es] a -> Union es a
unbundleAllUnion = Union '[Union es] a -> Union es a
forall (e :: * -> *) a. Union '[e] a -> e a
extract
{-# INLINE unbundleAllUnion #-}
prefixUnion :: forall any es a. (KnownLength any) => Union es a -> Union (any ++ es) a
prefixUnion :: forall (any :: [* -> *]) (es :: [* -> *]) a.
KnownLength any =>
Union es a -> Union (any ++ es) a
prefixUnion (Union Word
n e a
a) = Word -> e a -> Union (any ++ es) a
forall (e :: * -> *) a (es :: [* -> *]). Word -> e a -> Union es a
Union (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
+ forall (es :: [* -> *]). KnownLength es => Word
forall {a} (es :: [a]). KnownLength es => Word
reifyLength @any) e a
a
{-# INLINE prefixUnion #-}
prefixUnionUnder
:: forall any offset es a
. (KnownLength any, KnownNat offset)
=> Union es a
-> Union (Take offset es ++ any ++ Drop offset es) a
prefixUnionUnder :: forall (any :: [* -> *]) (offset :: Nat) (es :: [* -> *]) a.
(KnownLength any, KnownNat offset) =>
Union es a -> Union (Take offset es ++ (any ++ Drop offset es)) a
prefixUnionUnder u :: Union es a
u@(Union Word
n e a
a)
| Word
n Word -> Word -> Bool
forall a. Ord a => a -> a -> Bool
< forall (n :: Nat). KnownNat n => Word
wordVal @offset = Union es a -> Union (Take offset es ++ (any ++ Drop offset es)) a
forall a b. Coercible a b => a -> b
coerce Union es a
u
| Bool
otherwise = Word -> e a -> Union (Take offset es ++ (any ++ Drop offset es)) a
forall (e :: * -> *) a (es :: [* -> *]). Word -> e a -> Union es a
Union (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
+ forall (es :: [* -> *]). KnownLength es => Word
forall {a} (es :: [a]). KnownLength es => Word
reifyLength @any) e a
a
{-# INLINE prefixUnionUnder #-}
suffixUnion :: forall any es a. Union es a -> Union (es ++ any) a
suffixUnion :: forall (any :: [* -> *]) (es :: [* -> *]) a.
Union es a -> Union (es ++ any) a
suffixUnion = Union es a -> Union (es ++ any) a
forall a b. Coercible a b => a -> b
coerce
{-# INLINE suffixUnion #-}
suffixUnionOverN
:: forall any offset es a
. (KnownLength any, KnownNat offset, KnownLength es)
=> Union es a
-> Union (Take (Length es - offset) es ++ any ++ Drop (Length es - offset) es) a
suffixUnionOverN :: forall (any :: [* -> *]) (offset :: Nat) (es :: [* -> *]) a.
(KnownLength any, KnownNat offset, KnownLength es) =>
Union es a
-> Union
(Take (Length es - offset) es
++ (any ++ Drop (Length es - offset) es))
a
suffixUnionOverN u :: Union es a
u@(Union Word
n e a
a)
| Word
n Word -> Word -> Bool
forall a. Ord a => a -> a -> Bool
< forall (es :: [* -> *]). KnownLength es => Word
forall {a} (es :: [a]). KnownLength es => Word
reifyLength @es Word -> Word -> Word
forall a. Num a => a -> a -> a
- forall (n :: Nat). KnownNat n => Word
wordVal @offset = Union es a
-> Union
(Take (Length es - offset) es
++ (any ++ Drop (Length es - offset) es))
a
forall a b. Coercible a b => a -> b
coerce Union es a
u
| Bool
otherwise = Word
-> e a
-> Union
(Take (Length es - offset) es
++ (any ++ Drop (Length es - offset) es))
a
forall (e :: * -> *) a (es :: [* -> *]). Word -> e a -> Union es a
Union (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
+ forall (es :: [* -> *]). KnownLength es => Word
forall {a} (es :: [a]). KnownLength es => Word
reifyLength @any) e a
a
{-# INLINE suffixUnionOverN #-}
flipAllUnion :: forall es a. (KnownLength es) => Union es a -> Union (Reverse es) a
flipAllUnion :: forall (es :: [* -> *]) a.
KnownLength es =>
Union es a -> Union (Reverse es) a
flipAllUnion (Union Word
n e a
a) = Word -> e a -> Union (Reverse_ '[] es) a
forall (e :: * -> *) a (es :: [* -> *]). Word -> e a -> Union es a
Union (forall (es :: [* -> *]). KnownLength es => Word
forall {a} (es :: [a]). KnownLength es => Word
reifyLength @es Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
n) e a
a
{-# INLINE flipAllUnion #-}
flipUnion
:: forall len es a
. (KnownNat len)
=> Union es a
-> Union (Reverse (Take len es) ++ Drop len es) a
flipUnion :: forall (len :: Nat) (es :: [* -> *]) a.
KnownNat len =>
Union es a -> Union (Reverse (Take len es) ++ Drop len es) a
flipUnion u :: Union es a
u@(Union Word
n e a
a)
| Word
n Word -> Word -> Bool
forall a. Ord a => a -> a -> Bool
< Word
len = Word -> e a -> Union (Reverse_ '[] (Take len es) ++ Drop len es) a
forall (e :: * -> *) a (es :: [* -> *]). Word -> e a -> Union es a
Union (Word
len Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
n) e a
a
| Bool
otherwise = Union es a -> Union (Reverse_ '[] (Take len es) ++ Drop len es) a
forall a b. Coercible a b => a -> b
coerce Union es a
u
where
len :: Word
len = forall (n :: Nat). KnownNat n => Word
wordVal @len
{-# INLINE flipUnion #-}
flipUnionUnder
:: forall len offset es a
. (KnownNat len, KnownNat offset)
=> Union es a
-> Union (Take offset es ++ Reverse (Take len (Drop offset es)) ++ Drop len (Drop offset es)) a
flipUnionUnder :: forall (len :: Nat) (offset :: Nat) (es :: [* -> *]) a.
(KnownNat len, KnownNat offset) =>
Union es a
-> Union
(Take offset es
++ (Reverse (Take len (Drop offset es))
++ Drop len (Drop offset es)))
a
flipUnionUnder u :: Union es a
u@(Union Word
n e a
a)
| Word
n Word -> Word -> Bool
forall a. Ord a => a -> a -> Bool
>= Word
off Bool -> Bool -> Bool
&& Word
n' Word -> Word -> Bool
forall a. Ord a => a -> a -> Bool
< Word
len = Word
-> e a
-> Union
(Take offset es
++ (Reverse_ '[] (Take len (Drop offset es))
++ Drop len (Drop offset es)))
a
forall (e :: * -> *) a (es :: [* -> *]). Word -> e a -> Union es a
Union (Word
off Word -> Word -> Word
forall a. Num a => a -> a -> a
+ Word
len Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
n') e a
a
| Bool
otherwise = Union es a
-> Union
(Take offset es
++ (Reverse_ '[] (Take len (Drop offset es))
++ Drop len (Drop offset es)))
a
forall a b. Coercible a b => a -> b
coerce Union es a
u
where
off :: Word
off = forall (n :: Nat). KnownNat n => Word
wordVal @offset
len :: Word
len = forall (n :: Nat). KnownNat n => Word
wordVal @len
n' :: Word
n' = Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
off
{-# INLINE flipUnionUnder #-}
nil :: Union '[] a -> r
nil :: forall a r. Union '[] a -> r
nil Union '[] a
_ = [Char] -> r
forall a. HasCallStack => [Char] -> a
error [Char]
"Effect system internal error: nil - An empty effect union, which should not be possible to create, has been created."