mirror of
https://github.com/sayo-hs/heftia.git
synced 2024-11-26 23:05:04 +03:00
[add] utility functions to permutate the sequence of effects.
This commit is contained in:
Yamada Ryo
parent
900fecbf30
commit
9dd91b9224
@ -37,13 +37,34 @@ import Data.Free.Sum (SumUnion)
|
||||
import Data.Free.Union (
|
||||
IsMember,
|
||||
Member,
|
||||
Union,
|
||||
absurdUnion,
|
||||
decomp,
|
||||
inject,
|
||||
project,
|
||||
weakenL,
|
||||
weakenR,
|
||||
Union (
|
||||
absurdUnion,
|
||||
bundleUnion2,
|
||||
bundleUnion3,
|
||||
bundleUnion4,
|
||||
decomp,
|
||||
flipUnion,
|
||||
flipUnion3,
|
||||
flipUnionUnder,
|
||||
inject,
|
||||
inject0,
|
||||
project,
|
||||
rot3,
|
||||
rot3',
|
||||
unbundleUnion2,
|
||||
unbundleUnion3,
|
||||
unbundleUnion4,
|
||||
weaken,
|
||||
weaken2,
|
||||
weaken2Under,
|
||||
weaken2Under2,
|
||||
weaken3,
|
||||
weaken3Under,
|
||||
weaken4,
|
||||
weakenUnder,
|
||||
weakenUnder2,
|
||||
weakenUnder3
|
||||
),
|
||||
)
|
||||
import Data.Kind (Type)
|
||||
|
||||
@ -133,7 +154,14 @@ reinterpret i a =
|
||||
freerEffects $ ($ runFreerEffects a) $ reinterpretFT \u ->
|
||||
case decomp u of
|
||||
Left e -> runFreerEffects $ i e
|
||||
Right e -> liftInsT $ weakenR e
|
||||
Right e -> liftInsT $ weaken e
|
||||
|
||||
transformAll ::
|
||||
(TransFreer c fr, Union u, Union u', c f) =>
|
||||
(u es ~> u' es') ->
|
||||
FreerEffects fr u es f ~> FreerEffects fr u' es' f
|
||||
transformAll f = overFreerEffects $ transformT f
|
||||
{-# INLINE transformAll #-}
|
||||
|
||||
transform ::
|
||||
(TransFreer c fr, Union u, c f) =>
|
||||
@ -142,8 +170,8 @@ transform ::
|
||||
transform f a =
|
||||
freerEffects $ ($ runFreerEffects a) $ transformT \u ->
|
||||
case decomp u of
|
||||
Left e -> weakenL $ f e
|
||||
Right e -> weakenR e
|
||||
Left e -> inject0 $ f e
|
||||
Right e -> weaken e
|
||||
|
||||
interpose ::
|
||||
forall e fr u es f c.
|
||||
@ -213,24 +241,160 @@ intercept f a =
|
||||
Just e -> inject $ f e
|
||||
Nothing -> u
|
||||
|
||||
raiseUnder ::
|
||||
forall e' e es fr u f c.
|
||||
(TransFreer c fr, Union u, c f) =>
|
||||
FreerEffects fr u (e ': es) f ~> FreerEffects fr u (e ': e' ': es) f
|
||||
raiseUnder a =
|
||||
freerEffects
|
||||
. ($ runFreerEffects a)
|
||||
$ transformT \u -> case decomp u of
|
||||
Left e -> weakenL e
|
||||
Right e -> weakenR $ weakenR e
|
||||
|
||||
raise ::
|
||||
forall e es fr u f c.
|
||||
(TransFreer c fr, Union u, c f) =>
|
||||
FreerEffects fr u es f ~> FreerEffects fr u (e ': es) f
|
||||
raise a = freerEffects . ($ runFreerEffects a) $ transformT weakenR
|
||||
raise = transformAll weaken
|
||||
{-# INLINE raise #-}
|
||||
|
||||
raise2 ::
|
||||
forall e1 e2 es fr u f c.
|
||||
(TransFreer c fr, Union u, c f) =>
|
||||
FreerEffects fr u es f ~> FreerEffects fr u (e1 ': e2 ': es) f
|
||||
raise2 = transformAll weaken2
|
||||
{-# INLINE raise2 #-}
|
||||
|
||||
raise3 ::
|
||||
forall e1 e2 e3 es fr u f c.
|
||||
(TransFreer c fr, Union u, c f) =>
|
||||
FreerEffects fr u es f ~> FreerEffects fr u (e1 ': e2 ': e3 ': es) f
|
||||
raise3 = transformAll weaken3
|
||||
{-# INLINE raise3 #-}
|
||||
|
||||
raise4 ::
|
||||
forall e1 e2 e3 e4 es fr u f c.
|
||||
(TransFreer c fr, Union u, c f) =>
|
||||
FreerEffects fr u es f ~> FreerEffects fr u (e1 ': e2 ': e3 ': e4 ': es) f
|
||||
raise4 = transformAll weaken4
|
||||
{-# INLINE raise4 #-}
|
||||
|
||||
raiseUnder ::
|
||||
forall e1 e2 es fr u f c.
|
||||
(TransFreer c fr, Union u, c f) =>
|
||||
FreerEffects fr u (e1 ': es) f ~> FreerEffects fr u (e1 ': e2 ': es) f
|
||||
raiseUnder = transformAll weakenUnder
|
||||
{-# INLINE raiseUnder #-}
|
||||
|
||||
raiseUnder2 ::
|
||||
forall e1 e2 e3 es fr u f c.
|
||||
(TransFreer c fr, Union u, c f) =>
|
||||
FreerEffects fr u (e1 ': e2 ': es) f ~> FreerEffects fr u (e1 ': e2 ': e3 ': es) f
|
||||
raiseUnder2 = transformAll weakenUnder2
|
||||
{-# INLINE raiseUnder2 #-}
|
||||
|
||||
raiseUnder3 ::
|
||||
forall e1 e2 e3 e4 es fr u f c.
|
||||
(TransFreer c fr, Union u, c f) =>
|
||||
FreerEffects fr u (e1 ': e2 ': e3 ': es) f ~> FreerEffects fr u (e1 ': e2 ': e3 ': e4 ': es) f
|
||||
raiseUnder3 = transformAll weakenUnder3
|
||||
{-# INLINE raiseUnder3 #-}
|
||||
|
||||
raise2Under ::
|
||||
forall e1 e2 e3 es fr u f c.
|
||||
(TransFreer c fr, Union u, c f) =>
|
||||
FreerEffects fr u (e1 ': es) f ~> FreerEffects fr u (e1 ': e2 ': e3 ': es) f
|
||||
raise2Under = transformAll weaken2Under
|
||||
{-# INLINE raise2Under #-}
|
||||
|
||||
raise2Under2 ::
|
||||
forall e1 e2 e3 e4 es fr u f c.
|
||||
(TransFreer c fr, Union u, c f) =>
|
||||
FreerEffects fr u (e1 ': e2 ': es) f ~> FreerEffects fr u (e1 ': e2 ': e3 ': e4 ': es) f
|
||||
raise2Under2 = transformAll weaken2Under2
|
||||
{-# INLINE raise2Under2 #-}
|
||||
|
||||
raise3Under ::
|
||||
forall e1 e2 e3 e4 es fr u f c.
|
||||
(TransFreer c fr, Union u, c f) =>
|
||||
FreerEffects fr u (e1 ': es) f ~> FreerEffects fr u (e1 ': e2 ': e3 ': e4 ': es) f
|
||||
raise3Under = transformAll weaken3Under
|
||||
{-# INLINE raise3Under #-}
|
||||
|
||||
flipFreer ::
|
||||
forall e1 e2 es fr u f c.
|
||||
(TransFreer c fr, Union u, c f) =>
|
||||
FreerEffects fr u (e1 ': e2 ': es) f ~> FreerEffects fr u (e2 ': e1 ': es) f
|
||||
flipFreer = transformAll flipUnion
|
||||
{-# INLINE flipFreer #-}
|
||||
|
||||
flipFreer3 ::
|
||||
forall e1 e2 e3 es fr u f c.
|
||||
(TransFreer c fr, Union u, c f) =>
|
||||
FreerEffects fr u (e1 ': e2 ': e3 ': es) f ~> FreerEffects fr u (e3 ': e2 ': e1 ': es) f
|
||||
flipFreer3 = transformAll flipUnion3
|
||||
{-# INLINE flipFreer3 #-}
|
||||
|
||||
flipFreerUnder ::
|
||||
forall e1 e2 e3 es fr u f c.
|
||||
(TransFreer c fr, Union u, c f) =>
|
||||
FreerEffects fr u (e1 ': e2 ': e3 ': es) f ~> FreerEffects fr u (e1 ': e3 ': e2 ': es) f
|
||||
flipFreerUnder = transformAll flipUnionUnder
|
||||
{-# INLINE flipFreerUnder #-}
|
||||
|
||||
rotate3 ::
|
||||
forall e1 e2 e3 es fr u f c.
|
||||
(TransFreer c fr, Union u, c f) =>
|
||||
FreerEffects fr u (e1 ': e2 ': e3 ': es) f ~> FreerEffects fr u (e2 ': e3 ': e1 ': es) f
|
||||
rotate3 = transformAll rot3
|
||||
{-# INLINE rotate3 #-}
|
||||
|
||||
rotate3' ::
|
||||
forall e1 e2 e3 es fr u f c.
|
||||
(TransFreer c fr, Union u, c f) =>
|
||||
FreerEffects fr u (e1 ': e2 ': e3 ': es) f ~> FreerEffects fr u (e3 ': e1 ': e2 ': es) f
|
||||
rotate3' = transformAll rot3'
|
||||
{-# INLINE rotate3' #-}
|
||||
|
||||
bundle2 ::
|
||||
forall e1 e2 es fr u f c u'.
|
||||
(TransFreer c fr, Union u, Union u', c f) =>
|
||||
FreerEffects fr u (e1 ': e2 ': es) f ~> FreerEffects fr u (u' '[e1, e2] ': es) f
|
||||
bundle2 = transformAll bundleUnion2
|
||||
{-# INLINE bundle2 #-}
|
||||
|
||||
bundle3 ::
|
||||
forall e1 e2 e3 es fr u f c u'.
|
||||
(TransFreer c fr, Union u, Union u', c f) =>
|
||||
FreerEffects fr u (e1 ': e2 ': e3 ': es) f ~> FreerEffects fr u (u' '[e1, e2, e3] ': es) f
|
||||
bundle3 = transformAll bundleUnion3
|
||||
{-# INLINE bundle3 #-}
|
||||
|
||||
bundle4 ::
|
||||
forall e1 e2 e3 e4 es fr u f c u'.
|
||||
(TransFreer c fr, Union u, Union u', c f) =>
|
||||
FreerEffects fr u (e1 ': e2 ': e3 ': e4 ': es) f ~> FreerEffects fr u (u' '[e1, e2, e3, e4] ': es) f
|
||||
bundle4 = transformAll bundleUnion4
|
||||
{-# INLINE bundle4 #-}
|
||||
|
||||
unbundle2 ::
|
||||
forall e1 e2 es fr u f c u'.
|
||||
(TransFreer c fr, Union u, Union u', c f) =>
|
||||
FreerEffects fr u (u' '[e1, e2] ': es) f ~> FreerEffects fr u (e1 ': e2 ': es) f
|
||||
unbundle2 = transformAll unbundleUnion2
|
||||
{-# INLINE unbundle2 #-}
|
||||
|
||||
unbundle3 ::
|
||||
forall e1 e2 e3 es fr u f c u'.
|
||||
(TransFreer c fr, Union u, Union u', c f) =>
|
||||
FreerEffects fr u (u' '[e1, e2, e3] ': es) f ~> FreerEffects fr u (e1 ': e2 ': e3 ': es) f
|
||||
unbundle3 = transformAll unbundleUnion3
|
||||
{-# INLINE unbundle3 #-}
|
||||
|
||||
unbundle4 ::
|
||||
forall e1 e2 e3 e4 es fr u f c u'.
|
||||
(TransFreer c fr, Union u, Union u', c f) =>
|
||||
FreerEffects fr u (u' '[e1, e2, e3, e4] ': es) f ~> FreerEffects fr u (e1 ': e2 ': e3 ': e4 ': es) f
|
||||
unbundle4 = transformAll unbundleUnion4
|
||||
{-# INLINE unbundle4 #-}
|
||||
|
||||
overFreerEffects ::
|
||||
(fr (u es) f a -> fr' (u' es') g b) ->
|
||||
FreerEffects fr u es f a ->
|
||||
FreerEffects fr' u' es' g b
|
||||
overFreerEffects f = freerEffects . f . runFreerEffects
|
||||
{-# INLINE overFreerEffects #-}
|
||||
|
||||
interpreted :: (TransFreer c fr, c f, Union u) => FreerEffects fr u '[] f ~> f
|
||||
interpreted = runInterpretF absurdUnion . runFreerEffects
|
||||
{-# INLINE interpreted #-}
|
||||
|
||||
@ -33,6 +33,7 @@ import Control.Heftia.Trans (
|
||||
liftSigT,
|
||||
reelaborateHT,
|
||||
runElaborateH,
|
||||
transformHT,
|
||||
translateT,
|
||||
)
|
||||
import Control.Monad (MonadPlus)
|
||||
@ -44,13 +45,34 @@ import Data.Hefty.Sum (SumUnionH)
|
||||
import Data.Hefty.Union (
|
||||
IsMemberH,
|
||||
MemberH,
|
||||
UnionH,
|
||||
absurdUnionH,
|
||||
decompH,
|
||||
injectH,
|
||||
projectH,
|
||||
weakenLH,
|
||||
weakenRH,
|
||||
UnionH (
|
||||
absurdUnionH,
|
||||
bundleUnion2H,
|
||||
bundleUnion3H,
|
||||
bundleUnion4H,
|
||||
decompH,
|
||||
flipUnion3H,
|
||||
flipUnionH,
|
||||
flipUnionUnderH,
|
||||
inject0H,
|
||||
injectH,
|
||||
projectH,
|
||||
rot3H,
|
||||
rot3H',
|
||||
unbundleUnion2H,
|
||||
unbundleUnion3H,
|
||||
unbundleUnion4H,
|
||||
weaken2H,
|
||||
weaken2Under2H,
|
||||
weaken2UnderH,
|
||||
weaken3H,
|
||||
weaken3UnderH,
|
||||
weaken4H,
|
||||
weakenH,
|
||||
weakenUnder2H,
|
||||
weakenUnder3H,
|
||||
weakenUnderH
|
||||
),
|
||||
)
|
||||
import Data.Kind (Type)
|
||||
|
||||
@ -163,7 +185,20 @@ reinterpretH i a =
|
||||
heftiaEffects $ ($ runHeftiaEffects a) $ reelaborateHT \u ->
|
||||
case decompH u of
|
||||
Left e -> runHeftiaEffects $ i $ hfmap heftiaEffects e
|
||||
Right e -> liftSigT $ weakenRH e
|
||||
Right e -> liftSigT $ weakenH e
|
||||
|
||||
transformAllH ::
|
||||
( TransHeftia c h
|
||||
, UnionH u
|
||||
, UnionH u'
|
||||
, HFunctor (u es)
|
||||
, HFunctor (u' es')
|
||||
, c f
|
||||
) =>
|
||||
(forall g. u es g ~> u' es' g) ->
|
||||
HeftiaEffects h u es f ~> HeftiaEffects h u' es' f
|
||||
transformAllH f = overHeftiaEffects $ transformHT f
|
||||
{-# INLINE transformAllH #-}
|
||||
|
||||
translate ::
|
||||
( TransHeftia c h
|
||||
@ -179,8 +214,22 @@ translate ::
|
||||
translate f a =
|
||||
heftiaEffects $ ($ runHeftiaEffects a) $ translateT \u ->
|
||||
case decompH u of
|
||||
Left e -> weakenLH $ hfmap runHeftiaEffects $ f $ hfmap heftiaEffects e
|
||||
Right e -> weakenRH e
|
||||
Left e -> inject0H $ hfmap runHeftiaEffects $ f $ hfmap heftiaEffects e
|
||||
Right e -> weakenH e
|
||||
|
||||
translateAll ::
|
||||
( TransHeftia c h
|
||||
, UnionH u
|
||||
, UnionH u'
|
||||
, HFunctor (u es)
|
||||
, HFunctor (u' es')
|
||||
, c f
|
||||
) =>
|
||||
(u es (HeftiaEffects h u' es' f) ~> u' es' (HeftiaEffects h u' es' f)) ->
|
||||
HeftiaEffects h u es f ~> HeftiaEffects h u' es' f
|
||||
translateAll f =
|
||||
overHeftiaEffects $ translateT (hfmap runHeftiaEffects . f . hfmap heftiaEffects)
|
||||
{-# INLINE translateAll #-}
|
||||
|
||||
interposeH ::
|
||||
forall e h u es f c.
|
||||
@ -206,24 +255,280 @@ interceptH f a =
|
||||
Just e -> injectH $ hfmap runHeftiaEffects $ f e
|
||||
Nothing -> hfmap runHeftiaEffects u'
|
||||
|
||||
raiseH ::
|
||||
forall e hs h u f c.
|
||||
( TransHeftia c h
|
||||
, HFunctor (u hs)
|
||||
, HFunctor (u (e ': hs))
|
||||
, c f
|
||||
, UnionH u
|
||||
) =>
|
||||
HeftiaEffects h u hs f ~> HeftiaEffects h u (e ': hs) f
|
||||
raiseH = transformAllH weakenH
|
||||
{-# INLINE raiseH #-}
|
||||
|
||||
raise2H ::
|
||||
forall e1 e2 hs h u f c.
|
||||
( TransHeftia c h
|
||||
, HFunctor (u hs)
|
||||
, HFunctor (u (e1 ': e2 ': hs))
|
||||
, c f
|
||||
, UnionH u
|
||||
) =>
|
||||
HeftiaEffects h u hs f ~> HeftiaEffects h u (e1 ': e2 ': hs) f
|
||||
raise2H = transformAllH weaken2H
|
||||
{-# INLINE raise2H #-}
|
||||
|
||||
raise3H ::
|
||||
forall e1 e2 e3 hs h u f c.
|
||||
( TransHeftia c h
|
||||
, HFunctor (u hs)
|
||||
, HFunctor (u (e1 ': e2 ': e3 ': hs))
|
||||
, c f
|
||||
, UnionH u
|
||||
) =>
|
||||
HeftiaEffects h u hs f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': hs) f
|
||||
raise3H = transformAllH weaken3H
|
||||
{-# INLINE raise3H #-}
|
||||
|
||||
raise4H ::
|
||||
forall e1 e2 e3 e4 hs h u f c.
|
||||
( TransHeftia c h
|
||||
, HFunctor (u hs)
|
||||
, HFunctor (u (e1 ': e2 ': e3 ': e4 ': hs))
|
||||
, c f
|
||||
, UnionH u
|
||||
) =>
|
||||
HeftiaEffects h u hs f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': e4 ': hs) f
|
||||
raise4H = transformAllH weaken4H
|
||||
{-# INLINE raise4H #-}
|
||||
|
||||
raiseUnderH ::
|
||||
forall e' e es h u f c.
|
||||
(TransHeftia c h, HFunctor (u (e : es)), HFunctor (u (e : e' : es)), UnionH u, c f) =>
|
||||
HeftiaEffects h u (e ': es) f ~> HeftiaEffects h u (e ': e' ': es) f
|
||||
raiseUnderH a =
|
||||
heftiaEffects
|
||||
. ($ runHeftiaEffects a)
|
||||
$ translateT \u -> case decompH u of
|
||||
Left e -> weakenLH e
|
||||
Right e -> weakenRH $ weakenRH e
|
||||
forall e1 e2 hs h u f c.
|
||||
( TransHeftia c h
|
||||
, HFunctor (u (e1 ': hs))
|
||||
, HFunctor (u (e1 ': e2 ': hs))
|
||||
, c f
|
||||
, UnionH u
|
||||
) =>
|
||||
HeftiaEffects h u (e1 ': hs) f ~> HeftiaEffects h u (e1 ': e2 ': hs) f
|
||||
raiseUnderH = transformAllH weakenUnderH
|
||||
{-# INLINE raiseUnderH #-}
|
||||
|
||||
raiseUnder2H ::
|
||||
forall e1 e2 e3 hs h u f c.
|
||||
( TransHeftia c h
|
||||
, HFunctor (u (e1 ': e2 ': hs))
|
||||
, HFunctor (u (e1 ': e2 ': e3 ': hs))
|
||||
, c f
|
||||
, UnionH u
|
||||
) =>
|
||||
HeftiaEffects h u (e1 ': e2 ': hs) f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': hs) f
|
||||
raiseUnder2H = transformAllH weakenUnder2H
|
||||
{-# INLINE raiseUnder2H #-}
|
||||
|
||||
raiseUnder3H ::
|
||||
forall e1 e2 e3 e4 hs h u f c.
|
||||
( TransHeftia c h
|
||||
, HFunctor (u (e1 ': e2 ': e3 ': hs))
|
||||
, HFunctor (u (e1 ': e2 ': e3 ': e4 ': hs))
|
||||
, c f
|
||||
, UnionH u
|
||||
) =>
|
||||
HeftiaEffects h u (e1 ': e2 ': e3 ': hs) f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': e4 ': hs) f
|
||||
raiseUnder3H = transformAllH weakenUnder3H
|
||||
{-# INLINE raiseUnder3H #-}
|
||||
|
||||
raise2UnderH ::
|
||||
forall e1 e2 e3 hs h u f c.
|
||||
( TransHeftia c h
|
||||
, HFunctor (u (e1 ': hs))
|
||||
, HFunctor (u (e1 ': e2 ': e3 ': hs))
|
||||
, c f
|
||||
, UnionH u
|
||||
) =>
|
||||
HeftiaEffects h u (e1 ': hs) f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': hs) f
|
||||
raise2UnderH = transformAllH weaken2UnderH
|
||||
{-# INLINE raise2UnderH #-}
|
||||
|
||||
raise2Under2H ::
|
||||
forall e1 e2 e3 e4 hs h u f c.
|
||||
( TransHeftia c h
|
||||
, HFunctor (u (e1 ': e2 ': hs))
|
||||
, HFunctor (u (e1 ': e2 ': e3 ': e4 ': hs))
|
||||
, c f
|
||||
, UnionH u
|
||||
) =>
|
||||
HeftiaEffects h u (e1 ': e2 ': hs) f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': e4 ': hs) f
|
||||
raise2Under2H = transformAllH weaken2Under2H
|
||||
{-# INLINE raise2Under2H #-}
|
||||
|
||||
raise3UnderH ::
|
||||
forall e1 e2 e3 e4 hs h u f c.
|
||||
( TransHeftia c h
|
||||
, HFunctor (u (e1 ': hs))
|
||||
, HFunctor (u (e1 ': e2 ': e3 ': e4 ': hs))
|
||||
, c f
|
||||
, UnionH u
|
||||
) =>
|
||||
HeftiaEffects h u (e1 ': hs) f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': e4 ': hs) f
|
||||
raise3UnderH = transformAllH weaken3UnderH
|
||||
{-# INLINE raise3UnderH #-}
|
||||
|
||||
flipHeftia ::
|
||||
forall e1 e2 hs h u f c.
|
||||
( TransHeftia c h
|
||||
, HFunctor (u (e1 ': e2 ': hs))
|
||||
, HFunctor (u (e2 ': e1 ': hs))
|
||||
, c f
|
||||
, UnionH u
|
||||
) =>
|
||||
HeftiaEffects h u (e1 ': e2 ': hs) f ~> HeftiaEffects h u (e2 ': e1 ': hs) f
|
||||
flipHeftia = transformAllH flipUnionH
|
||||
{-# INLINE flipHeftia #-}
|
||||
|
||||
flipHeftia3 ::
|
||||
forall e1 e2 e3 es h u f c.
|
||||
( TransHeftia c h
|
||||
, HFunctor (u (e1 ': e2 ': e3 ': es))
|
||||
, HFunctor (u (e3 : e2 : e1 : es))
|
||||
, c f
|
||||
, UnionH u
|
||||
) =>
|
||||
HeftiaEffects h u (e1 ': e2 ': e3 ': es) f ~> HeftiaEffects h u (e3 ': e2 ': e1 ': es) f
|
||||
flipHeftia3 = transformAllH flipUnion3H
|
||||
{-# INLINE flipHeftia3 #-}
|
||||
|
||||
flipHeftiaUnder ::
|
||||
forall e1 e2 e3 es h u f c.
|
||||
( TransHeftia c h
|
||||
, HFunctor (u (e1 ': e2 ': e3 ': es))
|
||||
, HFunctor (u (e1 : e3 : e2 : es))
|
||||
, c f
|
||||
, UnionH u
|
||||
) =>
|
||||
HeftiaEffects h u (e1 ': e2 ': e3 ': es) f ~> HeftiaEffects h u (e1 ': e3 ': e2 ': es) f
|
||||
flipHeftiaUnder = transformAllH flipUnionUnderH
|
||||
{-# INLINE flipHeftiaUnder #-}
|
||||
|
||||
rotate3H ::
|
||||
forall e1 e2 e3 es h u f c.
|
||||
( TransHeftia c h
|
||||
, HFunctor (u (e1 ': e2 ': e3 ': es))
|
||||
, HFunctor (u (e2 : e3 : e1 : es))
|
||||
, c f
|
||||
, UnionH u
|
||||
) =>
|
||||
HeftiaEffects h u (e1 ': e2 ': e3 ': es) f ~> HeftiaEffects h u (e2 ': e3 ': e1 ': es) f
|
||||
rotate3H = transformAllH rot3H
|
||||
{-# INLINE rotate3H #-}
|
||||
|
||||
rotate3H' ::
|
||||
forall e1 e2 e3 es h u f c.
|
||||
( TransHeftia c h
|
||||
, HFunctor (u (e1 ': e2 ': e3 ': es))
|
||||
, HFunctor (u (e3 : e1 : e2 : es))
|
||||
, c f
|
||||
, UnionH u
|
||||
) =>
|
||||
HeftiaEffects h u (e1 ': e2 ': e3 ': es) f ~> HeftiaEffects h u (e3 ': e1 ': e2 ': es) f
|
||||
rotate3H' = transformAllH rot3H'
|
||||
{-# INLINE rotate3H' #-}
|
||||
|
||||
bundle2H ::
|
||||
forall u' e1 e2 es h u f c.
|
||||
( TransHeftia c h
|
||||
, HFunctor (u (e1 ': e2 ': es))
|
||||
, HFunctor (u (u' '[e1, e2] ': es))
|
||||
, c f
|
||||
, UnionH u
|
||||
, UnionH u'
|
||||
) =>
|
||||
HeftiaEffects h u (e1 ': e2 ': es) f ~> HeftiaEffects h u (u' '[e1, e2] ': es) f
|
||||
bundle2H = transformAllH bundleUnion2H
|
||||
{-# INLINE bundle2H #-}
|
||||
|
||||
bundle3H ::
|
||||
forall u' e1 e2 e3 es h u f c.
|
||||
( TransHeftia c h
|
||||
, HFunctor (u (e1 ': e2 ': e3 ': es))
|
||||
, HFunctor (u (u' '[e1, e2, e3] : es))
|
||||
, c f
|
||||
, UnionH u
|
||||
, UnionH u'
|
||||
) =>
|
||||
HeftiaEffects h u (e1 ': e2 ': e3 ': es) f ~> HeftiaEffects h u (u' '[e1, e2, e3] ': es) f
|
||||
bundle3H = transformAllH bundleUnion3H
|
||||
{-# INLINE bundle3H #-}
|
||||
|
||||
bundle4H ::
|
||||
forall u' e1 e2 e3 e4 es h u f c.
|
||||
( TransHeftia c h
|
||||
, HFunctor (u (e1 ': e2 ': e3 ': e4 ': es))
|
||||
, HFunctor (u (u' '[e1, e2, e3, e4] : es))
|
||||
, c f
|
||||
, UnionH u
|
||||
, UnionH u'
|
||||
) =>
|
||||
HeftiaEffects h u (e1 ': e2 ': e3 ': e4 ': es) f
|
||||
~> HeftiaEffects h u (u' '[e1, e2, e3, e4] ': es) f
|
||||
bundle4H = transformAllH bundleUnion4H
|
||||
{-# INLINE bundle4H #-}
|
||||
|
||||
unbundle2H ::
|
||||
forall e1 e2 es h u u' f c.
|
||||
( TransHeftia c h
|
||||
, HFunctor (u (e1 ': e2 ': es))
|
||||
, HFunctor (u (u' '[e1, e2] ': es))
|
||||
, c f
|
||||
, UnionH u
|
||||
, UnionH u'
|
||||
) =>
|
||||
HeftiaEffects h u (u' '[e1, e2] ': es) f ~> HeftiaEffects h u (e1 ': e2 ': es) f
|
||||
unbundle2H = transformAllH unbundleUnion2H
|
||||
{-# INLINE unbundle2H #-}
|
||||
|
||||
unbundle3H ::
|
||||
forall e1 e2 e3 es h u u' f c.
|
||||
( TransHeftia c h
|
||||
, HFunctor (u (e1 ': e2 ': e3 ': es))
|
||||
, HFunctor (u (u' '[e1, e2, e3] ': es))
|
||||
, c f
|
||||
, UnionH u
|
||||
, UnionH u'
|
||||
) =>
|
||||
HeftiaEffects h u (u' '[e1, e2, e3] ': es) f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': es) f
|
||||
unbundle3H = transformAllH unbundleUnion3H
|
||||
{-# INLINE unbundle3H #-}
|
||||
|
||||
unbundle4H ::
|
||||
forall e1 e2 e3 e4 es h u u' f c.
|
||||
( TransHeftia c h
|
||||
, HFunctor (u (e1 ': e2 ': e3 ': e4 ': es))
|
||||
, HFunctor (u (u' '[e1, e2, e3, e4] ': es))
|
||||
, c f
|
||||
, UnionH u
|
||||
, UnionH u'
|
||||
) =>
|
||||
HeftiaEffects h u (u' '[e1, e2, e3, e4] ': es) f
|
||||
~> HeftiaEffects h u (e1 ': e2 ': e3 ': e4 ': es) f
|
||||
unbundle4H = transformAllH unbundleUnion4H
|
||||
{-# INLINE unbundle4H #-}
|
||||
|
||||
hoistHeftiaEffects ::
|
||||
(TransHeftia c h, HFunctor (u es), c f, c g) =>
|
||||
(f ~> g) ->
|
||||
HeftiaEffects h u es f ~> HeftiaEffects h u es g
|
||||
hoistHeftiaEffects f = heftiaEffects . hoistHeftia f . runHeftiaEffects
|
||||
hoistHeftiaEffects f = overHeftiaEffects $ hoistHeftia f
|
||||
{-# INLINE hoistHeftiaEffects #-}
|
||||
|
||||
overHeftiaEffects ::
|
||||
(h (u es) f a -> h' (u' es') g b) ->
|
||||
HeftiaEffects h u es f a ->
|
||||
HeftiaEffects h' u' es' g b
|
||||
overHeftiaEffects f = heftiaEffects . f . runHeftiaEffects
|
||||
{-# INLINE overHeftiaEffects #-}
|
||||
|
||||
hoistInterpose ::
|
||||
forall e h u es fr u' es' f c c'.
|
||||
( TransHeftia c h
|
||||
|
||||
@ -4,13 +4,13 @@
|
||||
|
||||
module Data.Free.Union where
|
||||
|
||||
import Control.Effect.Class (Instruction)
|
||||
import Control.Effect.Class (Instruction, type (~>))
|
||||
import Data.Kind (Constraint)
|
||||
|
||||
class Union (u :: [Instruction] -> Instruction) where
|
||||
type HasMembership u (f :: Instruction) (fs :: [Instruction]) :: Constraint
|
||||
|
||||
inject :: HasMembership u f fs => f a -> u fs a
|
||||
inject :: HasMembership u f fs => f ~> u fs
|
||||
project :: HasMembership u f fs => u fs a -> Maybe (f a)
|
||||
|
||||
comp :: Either (f a) (u fs a) -> u (f ': fs) a
|
||||
@ -23,16 +23,101 @@ class Union (u :: [Instruction] -> Instruction) where
|
||||
(f |+|: g) u = case decomp u of
|
||||
Left x -> f x
|
||||
Right x -> g x
|
||||
|
||||
weakenL :: f a -> u (f ': fs) a
|
||||
weakenL = comp . Left
|
||||
|
||||
weakenR :: u fs a -> u (f ': fs) a
|
||||
weakenR = comp . Right
|
||||
|
||||
{-# INLINE (|+|:) #-}
|
||||
{-# INLINE weakenL #-}
|
||||
{-# INLINE weakenR #-}
|
||||
|
||||
inject0 :: f ~> u (f ': fs)
|
||||
inject0 = comp . Left
|
||||
{-# INLINE inject0 #-}
|
||||
|
||||
injectUnder :: f2 ~> u (f1 ': f2 ': fs)
|
||||
injectUnder = weaken . inject0
|
||||
{-# INLINE injectUnder #-}
|
||||
|
||||
injectUnder2 :: f3 ~> u (f1 ': f2 ': f3 ': fs)
|
||||
injectUnder2 = weaken2 . inject0
|
||||
{-# INLINE injectUnder2 #-}
|
||||
|
||||
injectUnder3 :: f4 ~> u (f1 ': f2 ': f3 ': f4 ': fs)
|
||||
injectUnder3 = weaken3 . inject0
|
||||
{-# INLINE injectUnder3 #-}
|
||||
|
||||
weaken :: u fs a -> u (f ': fs) a
|
||||
weaken = comp . Right
|
||||
{-# INLINE weaken #-}
|
||||
|
||||
weaken2 :: u fs a -> u (f1 ': f2 ': fs) a
|
||||
weaken2 = weaken . weaken
|
||||
{-# INLINE weaken2 #-}
|
||||
|
||||
weaken3 :: u fs a -> u (f1 ': f2 ': f3 ': fs) a
|
||||
weaken3 = weaken2 . weaken
|
||||
{-# INLINE weaken3 #-}
|
||||
|
||||
weaken4 :: u fs a -> u (f1 ': f2 ': f3 ': f4 ': fs) a
|
||||
weaken4 = weaken3 . weaken
|
||||
{-# INLINE weaken4 #-}
|
||||
|
||||
weakenUnder :: u (f1 ': fs) ~> u (f1 ': f2 ': fs)
|
||||
weakenUnder = inject0 |+|: weaken2
|
||||
|
||||
weakenUnder2 :: u (f1 ': f2 ': fs) ~> u (f1 ': f2 ': f3 ': fs)
|
||||
weakenUnder2 = inject0 |+|: injectUnder |+|: weaken3
|
||||
|
||||
weakenUnder3 :: u (f1 ': f2 ': f3 ': fs) ~> u (f1 ': f2 ': f3 ': f4 ': fs)
|
||||
weakenUnder3 = inject0 |+|: injectUnder |+|: injectUnder2 |+|: weaken4
|
||||
|
||||
weaken2Under :: u (f1 ': fs) ~> u (f1 ': f2 ': f3 ': fs)
|
||||
weaken2Under = inject0 |+|: weaken3
|
||||
|
||||
weaken2Under2 :: u (f1 ': f2 ': fs) ~> u (f1 ': f2 ': f3 ': f4 ': fs)
|
||||
weaken2Under2 = inject0 |+|: injectUnder |+|: weaken4
|
||||
|
||||
weaken3Under :: u (f1 ': fs) ~> u (f1 ': f2 ': f3 ': f4 ': fs)
|
||||
weaken3Under = inject0 |+|: weaken4
|
||||
|
||||
flipUnion :: u (f1 ': f2 ': fs) ~> u (f2 ': f1 ': fs)
|
||||
flipUnion = injectUnder |+|: inject0 |+|: weaken2
|
||||
|
||||
flipUnion3 :: u (f1 ': f2 ': f3 ': fs) ~> u (f3 ': f2 ': f1 ': fs)
|
||||
flipUnion3 = injectUnder2 |+|: injectUnder |+|: inject0 |+|: weaken3
|
||||
|
||||
flipUnionUnder :: u (f1 ': f2 ': f3 ': fs) ~> u (f1 ': f3 ': f2 ': fs)
|
||||
flipUnionUnder = inject0 |+|: injectUnder2 |+|: injectUnder |+|: weaken3
|
||||
|
||||
rot3 :: u (f1 ': f2 ': f3 ': fs) ~> u (f2 ': f3 ': f1 ': fs)
|
||||
rot3 = injectUnder2 |+|: inject0 |+|: injectUnder |+|: weaken3
|
||||
|
||||
rot3' :: u (f1 ': f2 ': f3 ': fs) ~> u (f3 ': f1 ': f2 ': fs)
|
||||
rot3' = injectUnder |+|: injectUnder2 |+|: inject0 |+|: weaken3
|
||||
|
||||
bundleUnion2 :: Union u' => u (f1 ': f2 ': fs) ~> u (u' '[f1, f2] ': fs)
|
||||
bundleUnion2 = inject0 . inject0 |+|: inject0 . injectUnder |+|: weaken
|
||||
|
||||
bundleUnion3 :: Union u' => u (f1 ': f2 ': f3 ': fs) ~> u (u' '[f1, f2, f3] ': fs)
|
||||
bundleUnion3 =
|
||||
(inject0 . inject0)
|
||||
|+|: (inject0 . injectUnder)
|
||||
|+|: (inject0 . injectUnder2)
|
||||
|+|: weaken
|
||||
|
||||
bundleUnion4 :: Union u' => u (f1 ': f2 ': f3 ': f4 ': fs) ~> u (u' '[f1, f2, f3, f4] ': fs)
|
||||
bundleUnion4 =
|
||||
(inject0 . inject0)
|
||||
|+|: (inject0 . injectUnder)
|
||||
|+|: (inject0 . injectUnder2)
|
||||
|+|: (inject0 . injectUnder3)
|
||||
|+|: weaken
|
||||
|
||||
unbundleUnion2 :: Union u' => u (u' '[f1, f2] ': fs) ~> u (f1 ': f2 ': fs)
|
||||
unbundleUnion2 = (inject0 |+|: injectUnder |+|: absurdUnion) |+|: weaken2
|
||||
|
||||
unbundleUnion3 :: Union u' => u (u' '[f1, f2, f3] ': fs) ~> u (f1 ': f2 ': f3 ': fs)
|
||||
unbundleUnion3 = (inject0 |+|: injectUnder |+|: injectUnder2 |+|: absurdUnion) |+|: weaken3
|
||||
|
||||
unbundleUnion4 :: Union u' => u (u' '[f1, f2, f3, f4] ': fs) ~> u (f1 ': f2 ': f3 ': f4 ': fs)
|
||||
unbundleUnion4 =
|
||||
(inject0 |+|: injectUnder |+|: injectUnder2 |+|: injectUnder3 |+|: absurdUnion)
|
||||
|+|: weaken4
|
||||
|
||||
type family IsMember (f :: Instruction) fs where
|
||||
IsMember f (f ': fs) = 'True
|
||||
|
||||
@ -6,13 +6,13 @@
|
||||
|
||||
module Data.Hefty.Union where
|
||||
|
||||
import Control.Effect.Class (Signature)
|
||||
import Control.Effect.Class (Signature, type (~>))
|
||||
import Data.Kind (Constraint)
|
||||
|
||||
class UnionH (u :: [Signature] -> Signature) where
|
||||
type HasMembershipH u (h :: Signature) (hs :: [Signature]) :: Constraint
|
||||
|
||||
injectH :: HasMembershipH u h hs => h f a -> u hs f a
|
||||
injectH :: HasMembershipH u h hs => h f ~> u hs f
|
||||
projectH :: HasMembershipH u h hs => u hs f a -> Maybe (h f a)
|
||||
|
||||
compH :: Either (h f a) (u hs f a) -> u (h ': hs) f a
|
||||
@ -25,16 +25,106 @@ class UnionH (u :: [Signature] -> Signature) where
|
||||
(f |+: g) u = case decompH u of
|
||||
Left x -> f x
|
||||
Right x -> g x
|
||||
|
||||
weakenLH :: h f a -> u (h ': hs) f a
|
||||
weakenLH = compH . Left
|
||||
|
||||
weakenRH :: u hs f a -> u (h ': hs) f a
|
||||
weakenRH = compH . Right
|
||||
|
||||
{-# INLINE (|+:) #-}
|
||||
{-# INLINE weakenLH #-}
|
||||
{-# INLINE weakenRH #-}
|
||||
|
||||
inject0H :: h f ~> u (h ': hs) f
|
||||
inject0H = compH . Left
|
||||
{-# INLINE inject0H #-}
|
||||
|
||||
injectUnderH :: h2 f ~> u (h1 ': h2 ': hs) f
|
||||
injectUnderH = weakenH . inject0H
|
||||
{-# INLINE injectUnderH #-}
|
||||
|
||||
injectUnder2H :: h3 f ~> u (h1 ': h2 ': h3 ': hs) f
|
||||
injectUnder2H = weaken2H . inject0H
|
||||
{-# INLINE injectUnder2H #-}
|
||||
|
||||
injectUnder3H :: h4 f ~> u (h1 ': h2 ': h3 ': h4 ': hs) f
|
||||
injectUnder3H = weaken3H . inject0H
|
||||
{-# INLINE injectUnder3H #-}
|
||||
|
||||
weakenH :: u hs f ~> u (h ': hs) f
|
||||
weakenH = compH . Right
|
||||
{-# INLINE weakenH #-}
|
||||
|
||||
weaken2H :: u hs f ~> u (h1 ': h2 ': hs) f
|
||||
weaken2H = weakenH . weakenH
|
||||
{-# INLINE weaken2H #-}
|
||||
|
||||
weaken3H :: u hs f ~> u (h1 ': h2 ': h3 ': hs) f
|
||||
weaken3H = weaken2H . weakenH
|
||||
{-# INLINE weaken3H #-}
|
||||
|
||||
weaken4H :: u hs f ~> u (h1 ': h2 ': h3 ': h4 ': hs) f
|
||||
weaken4H = weaken3H . weakenH
|
||||
{-# INLINE weaken4H #-}
|
||||
|
||||
weakenUnderH :: u (h1 ': hs) f ~> u (h1 ': h2 ': hs) f
|
||||
weakenUnderH = inject0H |+: weaken2H
|
||||
|
||||
weakenUnder2H :: u (h1 ': h2 ': hs) f ~> u (h1 ': h2 ': h3 ': hs) f
|
||||
weakenUnder2H = inject0H |+: injectUnderH |+: weaken3H
|
||||
|
||||
weakenUnder3H :: u (h1 ': h2 ': h3 ': hs) f ~> u (h1 ': h2 ': h3 ': h4 ': hs) f
|
||||
weakenUnder3H = inject0H |+: injectUnderH |+: injectUnder2H |+: weaken4H
|
||||
|
||||
weaken2UnderH :: u (h1 ': hs) f ~> u (h1 ': h2 ': h3 ': hs) f
|
||||
weaken2UnderH = inject0H |+: weaken3H
|
||||
|
||||
weaken2Under2H :: u (h1 ': h2 ': hs) f ~> u (h1 ': h2 ': h3 ': h4 ': hs) f
|
||||
weaken2Under2H = inject0H |+: injectUnderH |+: weaken4H
|
||||
|
||||
weaken3UnderH :: u (h1 ': hs) f ~> u (h1 ': h2 ': h3 ': h4 ': hs) f
|
||||
weaken3UnderH = inject0H |+: weaken4H
|
||||
|
||||
flipUnionH :: u (h1 ': h2 ': hs) f ~> u (h2 ': h1 ': hs) f
|
||||
flipUnionH = injectUnderH |+: inject0H |+: weaken2H
|
||||
|
||||
flipUnion3H :: u (h1 ': h2 ': h3 ': hs) f ~> u (h3 ': h2 ': h1 ': hs) f
|
||||
flipUnion3H = injectUnder2H |+: injectUnderH |+: inject0H |+: weaken3H
|
||||
|
||||
flipUnionUnderH :: u (h1 ': h2 ': h3 ': hs) f ~> u (h1 ': h3 ': h2 ': hs) f
|
||||
flipUnionUnderH = inject0H |+: injectUnder2H |+: injectUnderH |+: weaken3H
|
||||
|
||||
rot3H :: u (h1 ': h2 ': h3 ': hs) f ~> u (h2 ': h3 ': h1 ': hs) f
|
||||
rot3H = injectUnder2H |+: inject0H |+: injectUnderH |+: weaken3H
|
||||
|
||||
rot3H' :: u (h1 ': h2 ': h3 ': hs) f ~> u (h3 ': h1 ': h2 ': hs) f
|
||||
rot3H' = injectUnderH |+: injectUnder2H |+: inject0H |+: weaken3H
|
||||
|
||||
bundleUnion2H :: UnionH u' => u (h1 ': h2 ': hs) f ~> u (u' '[h1, h2] ': hs) f
|
||||
bundleUnion2H = inject0H . inject0H |+: inject0H . injectUnderH |+: weakenH
|
||||
|
||||
bundleUnion3H :: UnionH u' => u (h1 ': h2 ': h3 ': hs) f ~> u (u' '[h1, h2, h3] ': hs) f
|
||||
bundleUnion3H =
|
||||
(inject0H . inject0H)
|
||||
|+: (inject0H . injectUnderH)
|
||||
|+: (inject0H . injectUnder2H)
|
||||
|+: weakenH
|
||||
|
||||
bundleUnion4H ::
|
||||
UnionH u' =>
|
||||
u (h1 ': h2 ': h3 ': h4 ': hs) f ~> u (u' '[h1, h2, h3, h4] ': hs) f
|
||||
bundleUnion4H =
|
||||
(inject0H . inject0H)
|
||||
|+: (inject0H . injectUnderH)
|
||||
|+: (inject0H . injectUnder2H)
|
||||
|+: (inject0H . injectUnder3H)
|
||||
|+: weakenH
|
||||
|
||||
unbundleUnion2H :: UnionH u' => u (u' '[h1, h2] ': hs) f ~> u (h1 ': h2 ': hs) f
|
||||
unbundleUnion2H = (inject0H |+: injectUnderH |+: absurdUnionH) |+: weaken2H
|
||||
|
||||
unbundleUnion3H :: UnionH u' => u (u' '[h1, h2, h3] ': hs) f ~> u (h1 ': h2 ': h3 ': hs) f
|
||||
unbundleUnion3H = (inject0H |+: injectUnderH |+: injectUnder2H |+: absurdUnionH) |+: weaken3H
|
||||
|
||||
unbundleUnion4H ::
|
||||
UnionH u' =>
|
||||
u (u' '[h1, h2, h3, h4] ': hs) f
|
||||
~> u (h1 ': h2 ': h3 ': h4 ': hs) f
|
||||
unbundleUnion4H =
|
||||
(inject0H |+: injectUnderH |+: injectUnder2H |+: injectUnder3H |+: absurdUnionH)
|
||||
|+: weaken4H
|
||||
|
||||
type family IsMemberH (h :: Signature) hs where
|
||||
IsMemberH h (h ': hs) = 'True
|
||||
|
||||
Loading…
Reference in New Issue
Block a user