{-# OPTIONS_GHC -fno-warn-orphans -fno-warn-name-shadowing #-}
{-# LANGUAGE UndecidableInstances #-}
module Darcs.Patch.V2.Non
( Non(..)
, Nonable(..)
, unNon
, showNon
, showNons
, readNon
, readNons
, commutePrimsOrAddToCtx
, commuteOrAddToCtx
, commuteOrRemFromCtx
, commuteOrAddToCtxRL
, commuteOrRemFromCtxFL
, remNons
, (*>)
, (>*)
, (*>>)
, (>>*)
) where
import Darcs.Prelude hiding ( (*>) )
import Data.List ( delete )
import Control.Monad ( liftM, mzero )
import Darcs.Patch.Apply ( Apply(..) )
import Darcs.Patch.Commute ( commuteFL )
import Darcs.Patch.Effect ( Effect(..) )
import Darcs.Patch.Format ( PatchListFormat )
import Darcs.Patch.Invert ( Invert, invertFL, invertRL )
import Darcs.Patch.FromPrim
( FromPrim(..), ToFromPrim
, PrimOf, PrimPatchBase, toPrim
)
import Darcs.Patch.Prim ( sortCoalesceFL )
import Darcs.Patch.Commute ( Commute(..) )
import Darcs.Patch.Invert ( Invert(invert) )
import Darcs.Patch.Read ( ReadPatch(..) )
import Darcs.Patch.Show ( showPatch )
import Darcs.Util.Parser ( Parser, lexChar )
import Darcs.Patch.Witnesses.Eq ( Eq2(..), EqCheck(..) )
import Darcs.Patch.Witnesses.Ordered
( FL(..), RL(..), (+>+), mapRL_RL
, (:>)(..), reverseFL, reverseRL )
import Darcs.Patch.Witnesses.Show ( Show1, Show2, appPrec, showsPrec2 )
import Darcs.Patch.Witnesses.Sealed ( Sealed(Sealed) )
import Darcs.Patch.Read ( peekfor )
import Darcs.Patch.Show ( ShowPatchBasic, ShowPatchFor )
import Darcs.Patch.Viewing ()
import Darcs.Patch.Permutations ( removeFL, commuteWhatWeCanFL )
import Darcs.Util.Printer ( Doc, empty, vcat, hiddenPrefix, blueText, ($$) )
import qualified Data.ByteString.Char8 as BC ( pack, singleton )
data Non p wX where
Non :: FL p wX wY -> PrimOf p wY wZ -> Non p wX
unNon :: FromPrim p => Non p wX -> Sealed (FL p wX)
unNon :: forall (p :: * -> * -> *) wX.
FromPrim p =>
Non p wX -> Sealed (FL p wX)
unNon (Non FL p wX wY
c PrimOf p wY wZ
x) = forall (a :: * -> *) wY. a wY -> Sealed a
Sealed (FL p wX wY
c forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ forall (p :: * -> * -> *) wX wY.
FromPrim p =>
PrimOf p wX wY -> p wX wY
fromAnonymousPrim PrimOf p wY wZ
x forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: forall (a :: * -> * -> *) wX. FL a wX wX
NilFL)
instance (Show2 p, Show2 (PrimOf p)) => Show (Non p wX) where
showsPrec :: Int -> Non p wX -> ShowS
showsPrec Int
d (Non FL p wX wY
cs PrimOf p wY wZ
p) = Bool -> ShowS -> ShowS
showParen (Int
d forall a. Ord a => a -> a -> Bool
> Int
appPrec) forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"Non " forall b c a. (b -> c) -> (a -> b) -> a -> c
.
forall (a :: * -> * -> *) wX wY. Show2 a => Int -> a wX wY -> ShowS
showsPrec2 (Int
appPrec forall a. Num a => a -> a -> a
+ Int
1) FL p wX wY
cs forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" " forall b c a. (b -> c) -> (a -> b) -> a -> c
.
forall (a :: * -> * -> *) wX wY. Show2 a => Int -> a wX wY -> ShowS
showsPrec2 (Int
appPrec forall a. Num a => a -> a -> a
+ Int
1) PrimOf p wY wZ
p
instance (Show2 p, Show2 (PrimOf p)) => Show1 (Non p)
showNons :: (ShowPatchBasic p, PatchListFormat p, PrimPatchBase p)
=> ShowPatchFor -> [Non p wX] -> Doc
showNons :: forall (p :: * -> * -> *) wX.
(ShowPatchBasic p, PatchListFormat p, PrimPatchBase p) =>
ShowPatchFor -> [Non p wX] -> Doc
showNons ShowPatchFor
_ [] = Doc
empty
showNons ShowPatchFor
f [Non p wX]
xs = String -> Doc
blueText String
"{{" Doc -> Doc -> Doc
$$ [Doc] -> Doc
vcat (forall a b. (a -> b) -> [a] -> [b]
map (forall (p :: * -> * -> *) wX.
(ShowPatchBasic p, PatchListFormat p, PrimPatchBase p) =>
ShowPatchFor -> Non p wX -> Doc
showNon ShowPatchFor
f) [Non p wX]
xs) Doc -> Doc -> Doc
$$ String -> Doc
blueText String
"}}"
showNon :: (ShowPatchBasic p, PatchListFormat p, PrimPatchBase p)
=> ShowPatchFor
-> Non p wX
-> Doc
showNon :: forall (p :: * -> * -> *) wX.
(ShowPatchBasic p, PatchListFormat p, PrimPatchBase p) =>
ShowPatchFor -> Non p wX -> Doc
showNon ShowPatchFor
f (Non FL p wX wY
c PrimOf p wY wZ
p) = String -> Doc -> Doc
hiddenPrefix String
"|" (forall (p :: * -> * -> *) wX wY.
ShowPatchBasic p =>
ShowPatchFor -> p wX wY -> Doc
showPatch ShowPatchFor
f FL p wX wY
c)
Doc -> Doc -> Doc
$$ String -> Doc -> Doc
hiddenPrefix String
"|" (String -> Doc
blueText String
":")
Doc -> Doc -> Doc
$$ forall (p :: * -> * -> *) wX wY.
ShowPatchBasic p =>
ShowPatchFor -> p wX wY -> Doc
showPatch ShowPatchFor
f PrimOf p wY wZ
p
readNons :: (ReadPatch p, PatchListFormat p, PrimPatchBase p)
=> Parser [Non p wX]
readNons :: forall (p :: * -> * -> *) wX.
(ReadPatch p, PatchListFormat p, PrimPatchBase p) =>
Parser [Non p wX]
readNons = forall a. ByteString -> Parser a -> Parser a -> Parser a
peekfor (String -> ByteString
BC.pack String
"{{") forall {wX}. Parser [Non p wX]
rns (forall (m :: * -> *) a. Monad m => a -> m a
return [])
where rns :: Parser [Non p wX]
rns = forall a. ByteString -> Parser a -> Parser a -> Parser a
peekfor (String -> ByteString
BC.pack String
"}}") (forall (m :: * -> *) a. Monad m => a -> m a
return []) forall a b. (a -> b) -> a -> b
$
do Sealed FL p wX wX
ps <- forall (p :: * -> * -> *) wX. ReadPatch p => Parser (Sealed (p wX))
readPatch'
Char -> Parser ()
lexChar Char
':'
Sealed PrimOf p wX wX
p <- forall (p :: * -> * -> *) wX. ReadPatch p => Parser (Sealed (p wX))
readPatch'
(forall (p :: * -> * -> *) wX wY wZ.
FL p wX wY -> PrimOf p wY wZ -> Non p wX
Non FL p wX wX
ps PrimOf p wX wX
p forall a. a -> [a] -> [a]
:) forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
`liftM` Parser [Non p wX]
rns
readNon :: (ReadPatch p, PatchListFormat p, PrimPatchBase p)
=> Parser (Non p wX)
readNon :: forall (p :: * -> * -> *) wX.
(ReadPatch p, PatchListFormat p, PrimPatchBase p) =>
Parser (Non p wX)
readNon = do Sealed FL p wX wX
ps <- forall (p :: * -> * -> *) wX. ReadPatch p => Parser (Sealed (p wX))
readPatch'
let doReadPrim :: Parser (Non p wX)
doReadPrim = do Sealed PrimOf p wX wX
p <- forall (p :: * -> * -> *) wX. ReadPatch p => Parser (Sealed (p wX))
readPatch'
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) wX wY wZ.
FL p wX wY -> PrimOf p wY wZ -> Non p wX
Non FL p wX wX
ps PrimOf p wX wX
p
forall a. ByteString -> Parser a -> Parser a -> Parser a
peekfor (Char -> ByteString
BC.singleton Char
':') Parser (Non p wX)
doReadPrim forall (m :: * -> *) a. MonadPlus m => m a
mzero
instance (Commute p, Eq2 p, Eq2 (PrimOf p)) => Eq (Non p wX) where
Non (FL p wX wY
cx :: FL p wX wY1) (PrimOf p wY wZ
x :: PrimOf p wY1 wZ1)
== :: Non p wX -> Non p wX -> Bool
== Non (FL p wX wY
cy :: FL p wX wY2) (PrimOf p wY wZ
y :: PrimOf p wY2 wZ2) =
case FL p wX wY
cx forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= FL p wX wY
cy of
EqCheck wY wY
IsEq -> case PrimOf p wY wZ
x forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= PrimOf p wY wZ
y :: EqCheck wZ1 wZ2 of
EqCheck wZ wZ
IsEq -> Bool
True
EqCheck wZ wZ
NotEq -> Bool
False
EqCheck wY wY
NotEq -> Bool
False
class Nonable p where
non :: p wX wY -> Non p wX
commuteOrAddToCtx :: (Commute p, ToFromPrim p) => p wX wY -> Non p wY
-> Non p wX
commuteOrAddToCtx :: forall (p :: * -> * -> *) wX wY.
(Commute p, ToFromPrim p) =>
p wX wY -> Non p wY -> Non p wX
commuteOrAddToCtx p wX wY
p Non p wY
n | Just Non p wX
n' <- p wX wY
p forall (p :: * -> * -> *) wX wY.
(Commute p, ToFromPrim p) =>
p wX wY -> Non p wY -> Maybe (Non p wX)
>* Non p wY
n = Non p wX
n'
commuteOrAddToCtx p wX wY
p (Non FL p wY wY
c PrimOf p wY wZ
x) = forall (p :: * -> * -> *) wX wY wZ.
FL p wX wY -> PrimOf p wY wZ -> Non p wX
Non (p wX wY
pforall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>:FL p wY wY
c) PrimOf p wY wZ
x
commuteOrAddToCtxRL :: (Apply p, Commute p, Invert p, ToFromPrim p) => RL p wX wY -> Non p wY
-> Non p wX
commuteOrAddToCtxRL :: forall (p :: * -> * -> *) wX wY.
(Apply p, Commute p, Invert p, ToFromPrim p) =>
RL p wX wY -> Non p wY -> Non p wX
commuteOrAddToCtxRL RL p wX wY
NilRL Non p wY
n = Non p wY
n
commuteOrAddToCtxRL (RL p wX wY
ps:<:p wY wY
p) Non p wY
n = forall (p :: * -> * -> *) wX wY.
(Apply p, Commute p, Invert p, ToFromPrim p) =>
RL p wX wY -> Non p wY -> Non p wX
commuteOrAddToCtxRL RL p wX wY
ps forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) wX wY.
(Commute p, ToFromPrim p) =>
p wX wY -> Non p wY -> Non p wX
commuteOrAddToCtx p wY wY
p Non p wY
n
class WL l where
toRL :: l p wX wY -> RL p wX wY
invertWL :: Invert p => l p wX wY -> l p wY wX
instance WL FL where
toRL :: forall (p :: * -> * -> *) wX wY. FL p wX wY -> RL p wX wY
toRL = forall (p :: * -> * -> *) wX wY. FL p wX wY -> RL p wX wY
reverseFL
invertWL :: forall (p :: * -> * -> *) wX wY.
Invert p =>
FL p wX wY -> FL p wY wX
invertWL = forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: * -> * -> *) wX wY.
Invert p =>
FL p wX wY -> RL p wY wX
invertFL
instance WL RL where
toRL :: forall (p :: * -> * -> *) wX wY. RL p wX wY -> RL p wX wY
toRL = forall a. a -> a
id
invertWL :: forall (p :: * -> * -> *) wX wY.
Invert p =>
RL p wX wY -> RL p wY wX
invertWL = forall (p :: * -> * -> *) wX wY. FL p wX wY -> RL p wX wY
reverseFL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: * -> * -> *) wX wY.
Invert p =>
RL p wX wY -> FL p wY wX
invertRL
commutePrimsOrAddToCtx :: (WL l, Apply p, Commute p, Invert p, ToFromPrim p) => l (PrimOf p) wX wY
-> Non p wY -> Non p wX
commutePrimsOrAddToCtx :: forall (l :: (* -> * -> *) -> * -> * -> *) (p :: * -> * -> *) wX
wY.
(WL l, Apply p, Commute p, Invert p, ToFromPrim p) =>
l (PrimOf p) wX wY -> Non p wY -> Non p wX
commutePrimsOrAddToCtx l (PrimOf p) wX wY
q = forall (p :: * -> * -> *) wX wY.
(Apply p, Commute p, Invert p, ToFromPrim p) =>
RL p wX wY -> Non p wY -> Non p wX
commuteOrAddToCtxRL (forall (a :: * -> * -> *) (b :: * -> * -> *) wX wZ.
(forall wW wY. a wW wY -> b wW wY) -> RL a wX wZ -> RL b wX wZ
mapRL_RL forall (p :: * -> * -> *) wX wY.
FromPrim p =>
PrimOf p wX wY -> p wX wY
fromAnonymousPrim forall a b. (a -> b) -> a -> b
$ forall (l :: (* -> * -> *) -> * -> * -> *) (p :: * -> * -> *) wX
wY.
WL l =>
l p wX wY -> RL p wX wY
toRL l (PrimOf p) wX wY
q)
remNons :: (Nonable p, Effect p, Apply p, Commute p, Invert p, Eq2 p, ToFromPrim p, PrimPatchBase p)
=> [Non p wX] -> Non p wX -> Non p wX
remNons :: forall (p :: * -> * -> *) wX.
(Nonable p, Effect p, Apply p, Commute p, Invert p, Eq2 p,
ToFromPrim p, PrimPatchBase p) =>
[Non p wX] -> Non p wX -> Non p wX
remNons [Non p wX]
ns n :: Non p wX
n@(Non FL p wX wY
c PrimOf p wY wZ
x) = case forall (p :: * -> * -> *) wX wY.
(Nonable p, Effect p, Apply p, Commute p, Invert p, Eq2 p,
ToFromPrim p, PrimPatchBase p) =>
[Non p wX] -> FL p wX wY -> (:>) (FL (PrimOf p)) (FL p) wX wY
remNonHelper [Non p wX]
ns FL p wX wY
c of
FL (PrimOf p) wX wZ
NilFL :> FL p wZ wY
c' -> forall (p :: * -> * -> *) wX wY wZ.
FL p wX wY -> PrimOf p wY wZ -> Non p wX
Non FL p wZ wY
c' PrimOf p wY wZ
x
(:>) (FL (PrimOf p)) (FL p) wX wY
_ -> Non p wX
n
where
remNonHelper :: (Nonable p, Effect p, Apply p, Commute p, Invert p, Eq2 p, ToFromPrim p,
PrimPatchBase p) => [Non p wX]
-> FL p wX wY -> (FL (PrimOf p) :> FL p) wX wY
remNonHelper :: forall (p :: * -> * -> *) wX wY.
(Nonable p, Effect p, Apply p, Commute p, Invert p, Eq2 p,
ToFromPrim p, PrimPatchBase p) =>
[Non p wX] -> FL p wX wY -> (:>) (FL (PrimOf p)) (FL p) wX wY
remNonHelper [] FL p wX wY
x = forall (a :: * -> * -> *) wX. FL a wX wX
NilFL forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wX wY
x
remNonHelper [Non p wX]
_ FL p wX wY
NilFL = forall (a :: * -> * -> *) wX. FL a wX wX
NilFL forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> forall (a :: * -> * -> *) wX. FL a wX wX
NilFL
remNonHelper [Non p wX]
ns (p wX wY
c:>:FL p wY wY
cs)
| forall (p :: * -> * -> *) wX wY. Nonable p => p wX wY -> Non p wX
non p wX wY
c forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Non p wX]
ns =
let nsWithoutC :: [Non p wX]
nsWithoutC = forall a. Eq a => a -> [a] -> [a]
delete (forall (p :: * -> * -> *) wX wY. Nonable p => p wX wY -> Non p wX
non p wX wY
c) [Non p wX]
ns in
let commuteOrAddInvC :: Non p wX -> Non p wY
commuteOrAddInvC = forall (p :: * -> * -> *) wX wY.
(Commute p, ToFromPrim p) =>
p wX wY -> Non p wY -> Non p wX
commuteOrAddToCtx forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert p wX wY
c in
case forall (p :: * -> * -> *) wX wY.
(Nonable p, Effect p, Apply p, Commute p, Invert p, Eq2 p,
ToFromPrim p, PrimPatchBase p) =>
[Non p wX] -> FL p wX wY -> (:>) (FL (PrimOf p)) (FL p) wX wY
remNonHelper (forall a b. (a -> b) -> [a] -> [b]
map Non p wX -> Non p wY
commuteOrAddInvC [Non p wX]
nsWithoutC) FL p wY wY
cs of
FL (PrimOf p) wY wZ
a :> FL p wZ wY
z -> forall (prim :: * -> * -> *) wX wY.
PrimCanonize prim =>
FL prim wX wY -> FL prim wX wY
sortCoalesceFL (forall (p :: * -> * -> *) wX wY.
Effect p =>
p wX wY -> FL (PrimOf p) wX wY
effect p wX wY
c forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ FL (PrimOf p) wY wZ
a) forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wZ wY
z
| Bool
otherwise = case forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p (FL p) wX wY -> (:>) (FL p) (p :> FL p) wX wY
commuteWhatWeCanFL (p wX wY
c forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wY wY
cs) of
FL p wX wZ
b :> p wZ wZ
c' :> FL p wZ wY
d -> case forall (p :: * -> * -> *) wX wY.
(Nonable p, Effect p, Apply p, Commute p, Invert p, Eq2 p,
ToFromPrim p, PrimPatchBase p) =>
[Non p wX] -> FL p wX wY -> (:>) (FL (PrimOf p)) (FL p) wX wY
remNonHelper [Non p wX]
ns FL p wX wZ
b of
FL (PrimOf p) wX wZ
a :> FL p wZ wZ
b' -> FL (PrimOf p) wX wZ
a forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> (FL p wZ wZ
b' forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ p wZ wZ
c' forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p wZ wY
d)
commuteOrRemFromCtx :: (Commute p, Invert p, Eq2 p, ToFromPrim p) => p wX wY -> Non p wX
-> Maybe (Non p wY)
commuteOrRemFromCtx :: forall (p :: * -> * -> *) wX wY.
(Commute p, Invert p, Eq2 p, ToFromPrim p) =>
p wX wY -> Non p wX -> Maybe (Non p wY)
commuteOrRemFromCtx p wX wY
p Non p wX
n | n' :: Maybe (Non p wY)
n'@(Just Non p wY
_) <- Non p wX
n forall (p :: * -> * -> *) wX wY.
(Commute p, Invert p, ToFromPrim p) =>
Non p wX -> p wX wY -> Maybe (Non p wY)
*> p wX wY
p = Maybe (Non p wY)
n'
commuteOrRemFromCtx p wX wY
p (Non FL p wX wY
pc PrimOf p wY wZ
x) = forall (p :: * -> * -> *) wX wY wZ.
(Eq2 p, Commute p) =>
p wX wY -> FL p wX wZ -> Maybe (FL p wY wZ)
removeFL p wX wY
p FL p wX wY
pc forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \FL p wY wY
c -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall (p :: * -> * -> *) wX wY wZ.
FL p wX wY -> PrimOf p wY wZ -> Non p wX
Non FL p wY wY
c PrimOf p wY wZ
x)
commuteOrRemFromCtxFL :: (Apply p, Commute p, Invert p, Eq2 p, ToFromPrim p) => FL p wX wY -> Non p wX
-> Maybe (Non p wY)
commuteOrRemFromCtxFL :: forall (p :: * -> * -> *) wX wY.
(Apply p, Commute p, Invert p, Eq2 p, ToFromPrim p) =>
FL p wX wY -> Non p wX -> Maybe (Non p wY)
commuteOrRemFromCtxFL FL p wX wY
NilFL Non p wX
n = forall a. a -> Maybe a
Just Non p wX
n
commuteOrRemFromCtxFL (p wX wY
p:>:FL p wY wY
ps) Non p wX
n = do Non p wY
n' <- forall (p :: * -> * -> *) wX wY.
(Commute p, Invert p, Eq2 p, ToFromPrim p) =>
p wX wY -> Non p wX -> Maybe (Non p wY)
commuteOrRemFromCtx p wX wY
p Non p wX
n
forall (p :: * -> * -> *) wX wY.
(Apply p, Commute p, Invert p, Eq2 p, ToFromPrim p) =>
FL p wX wY -> Non p wX -> Maybe (Non p wY)
commuteOrRemFromCtxFL FL p wY wY
ps Non p wY
n'
(*>) :: (Commute p, Invert p, ToFromPrim p) => Non p wX -> p wX wY
-> Maybe (Non p wY)
Non p wX
n *> :: forall (p :: * -> * -> *) wX wY.
(Commute p, Invert p, ToFromPrim p) =>
Non p wX -> p wX wY -> Maybe (Non p wY)
*> p wX wY
p = forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert p wX wY
p forall (p :: * -> * -> *) wX wY.
(Commute p, ToFromPrim p) =>
p wX wY -> Non p wY -> Maybe (Non p wX)
>* Non p wX
n
(>*) :: (Commute p, ToFromPrim p) => p wX wY -> Non p wY
-> Maybe (Non p wX)
p wX wY
y >* :: forall (p :: * -> * -> *) wX wY.
(Commute p, ToFromPrim p) =>
p wX wY -> Non p wY -> Maybe (Non p wX)
>* (Non FL p wY wY
c PrimOf p wY wZ
x) = do
FL p wX wZ
c' :> p wZ wY
y' <- forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p (FL p) wX wY -> Maybe ((:>) (FL p) p wX wY)
commuteFL (p wX wY
y forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wY wY
c)
p wZ wZ
px' :> p wZ wZ
_ <- forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p p wX wY -> Maybe ((:>) p p wX wY)
commute (p wZ wY
y' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> forall (p :: * -> * -> *) wX wY.
FromPrim p =>
PrimOf p wX wY -> p wX wY
fromAnonymousPrim PrimOf p wY wZ
x)
PrimOf p wZ wZ
x' <- forall (p :: * -> * -> *) wX wY.
ToPrim p =>
p wX wY -> Maybe (PrimOf p wX wY)
toPrim p wZ wZ
px'
forall (m :: * -> *) a. Monad m => a -> m a
return (forall (p :: * -> * -> *) wX wY wZ.
FL p wX wY -> PrimOf p wY wZ -> Non p wX
Non FL p wX wZ
c' PrimOf p wZ wZ
x')
(*>>) :: (WL l, Apply p, Commute p, Invert p, ToFromPrim p, PrimPatchBase p) => Non p wX
-> l (PrimOf p) wX wY -> Maybe (Non p wY)
Non p wX
n *>> :: forall (l :: (* -> * -> *) -> * -> * -> *) (p :: * -> * -> *) wX
wY.
(WL l, Apply p, Commute p, Invert p, ToFromPrim p,
PrimPatchBase p) =>
Non p wX -> l (PrimOf p) wX wY -> Maybe (Non p wY)
*>> l (PrimOf p) wX wY
p = forall (l :: (* -> * -> *) -> * -> * -> *) (p :: * -> * -> *) wX
wY.
(WL l, Invert p) =>
l p wX wY -> l p wY wX
invertWL l (PrimOf p) wX wY
p forall (l :: (* -> * -> *) -> * -> * -> *) (p :: * -> * -> *) wX
wY.
(WL l, Apply p, Commute p, Invert p, ToFromPrim p) =>
l (PrimOf p) wX wY -> Non p wY -> Maybe (Non p wX)
>>* Non p wX
n
(>>*) :: (WL l, Apply p, Commute p, Invert p, ToFromPrim p) => l (PrimOf p) wX wY -> Non p wY
-> Maybe (Non p wX)
l (PrimOf p) wX wY
ps >>* :: forall (l :: (* -> * -> *) -> * -> * -> *) (p :: * -> * -> *) wX
wY.
(WL l, Apply p, Commute p, Invert p, ToFromPrim p) =>
l (PrimOf p) wX wY -> Non p wY -> Maybe (Non p wX)
>>* Non p wY
n = forall (p :: * -> * -> *) wX wY.
(Apply p, Commute p, Invert p, ToFromPrim p) =>
RL (PrimOf p) wX wY -> Non p wY -> Maybe (Non p wX)
commuteRLPastNon (forall (l :: (* -> * -> *) -> * -> * -> *) (p :: * -> * -> *) wX
wY.
WL l =>
l p wX wY -> RL p wX wY
toRL l (PrimOf p) wX wY
ps) Non p wY
n
where
commuteRLPastNon :: (Apply p, Commute p, Invert p, ToFromPrim p) => RL (PrimOf p) wX wY
-> Non p wY -> Maybe (Non p wX)
commuteRLPastNon :: forall (p :: * -> * -> *) wX wY.
(Apply p, Commute p, Invert p, ToFromPrim p) =>
RL (PrimOf p) wX wY -> Non p wY -> Maybe (Non p wX)
commuteRLPastNon RL (PrimOf p) wX wY
NilRL Non p wY
n = forall a. a -> Maybe a
Just Non p wY
n
commuteRLPastNon (RL (PrimOf p) wX wY
xs:<:PrimOf p wY wY
x) Non p wY
n = forall (p :: * -> * -> *) wX wY.
FromPrim p =>
PrimOf p wX wY -> p wX wY
fromAnonymousPrim PrimOf p wY wY
x forall (p :: * -> * -> *) wX wY.
(Commute p, ToFromPrim p) =>
p wX wY -> Non p wY -> Maybe (Non p wX)
>* Non p wY
n forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (p :: * -> * -> *) wX wY.
(Apply p, Commute p, Invert p, ToFromPrim p) =>
RL (PrimOf p) wX wY -> Non p wY -> Maybe (Non p wX)
commuteRLPastNon RL (PrimOf p) wX wY
xs