#include "gadts.h"
module Darcs.Patch.V2.Non
( Non(..)
, Nonable(..)
, unNon
, showNon
, showNons
, readNon
, readNons
, commutePrimsOrAddToCtx
, commuteOrAddToCtx
, commuteOrRemFromCtx
, commuteOrAddToCtxRL
, commuteOrRemFromCtxFL
, remNons
, (*>)
, (>*)
, (*>>)
, (>>*)
) where
import Prelude hiding ( rem )
import Data.List ( delete )
import Control.Monad ( liftM, mzero )
import Darcs.Patch.Commute ( commuteFL )
import Darcs.Patch.Effect ( Effect(..) )
import Darcs.Patch.Format ( PatchListFormat, FileNameFormat(..) )
import Darcs.Patch.Invert ( Invert, invertFL, invertRL )
import Darcs.Patch.Prim ( FromPrim(..), ToFromPrim(..),
PrimOf, PrimPatchBase,
showPrim, sortCoalesceFL,
readPrim )
import Darcs.Patch.Patchy ( Patchy, showPatch, ReadPatch(..),
Commute(..), invert )
import Darcs.Patch.ReadMonads ( ParserM, lexChar )
import Darcs.Witnesses.Eq ( MyEq(..), EqCheck(..) )
import Darcs.Witnesses.Ordered ( FL(..), RL(..), (+>+), mapRL_RL
, (:>)(..), reverseFL, reverseRL )
import Darcs.Patch.Read ( peekfor )
import Darcs.Patch.Show ( ShowPatchBasic )
import Darcs.Patch.Viewing ()
import Darcs.Patch.Permutations ( removeFL, commuteWhatWeCanFL )
import Darcs.Witnesses.Show ( ShowDict(..), Show1(..), Show2(..), appPrec
, showsPrec2 )
import Darcs.Witnesses.Sealed ( Sealed(Sealed) )
import Printer ( Doc, empty, vcat, hiddenPrefix, blueText, ($$) )
import qualified Data.ByteString.Char8 as BC ( pack, singleton )
data Non p C(x) where
Non :: FL p C(x y) -> PrimOf p C(y z) -> Non p C(x)
unNon :: FromPrim p => Non p C(x) -> Sealed (FL p C(x))
unNon (Non c x) = Sealed (c +>+ fromPrim x :>: NilFL)
instance (Show2 p, Show2 (PrimOf p)) => Show (Non p C(x)) where
showsPrec d (Non cs p) = showParen (d > appPrec) $ showString "Non " .
showsPrec2 (appPrec + 1) cs . showString " " .
showsPrec2 (appPrec + 1) p
instance (Show2 p, Show2 (PrimOf p)) => Show1 (Non p) where
showDict1 = ShowDictClass
showNons :: (ShowPatchBasic p, PatchListFormat p, PrimPatchBase p)
=> [Non p C(x)] -> Doc
showNons [] = empty
showNons xs = blueText "{{" $$ vcat (map showNon xs) $$ blueText "}}"
showNon :: (ShowPatchBasic p, PatchListFormat p, PrimPatchBase p) => Non p C(x)
-> Doc
showNon (Non c p) = hiddenPrefix "|" (showPatch c)
$$ hiddenPrefix "|" (blueText ":")
$$ showPrim NewFormat p
readNons :: (ReadPatch p, PatchListFormat p, PrimPatchBase p, ParserM m)
=> m [Non p C(x)]
readNons = peekfor (BC.pack "{{") rns (return [])
where rns = peekfor (BC.pack "}}") (return []) $
do Sealed ps <- readPatch'
lexChar ':'
Sealed p <- readPrim NewFormat
(Non ps p :) `liftM` rns
readNon :: (ReadPatch p, PatchListFormat p, PrimPatchBase p, ParserM m)
=> m (Non p C(x))
readNon = do Sealed ps <- readPatch'
let doReadPrim = do Sealed p <- readPrim NewFormat
return $ Non ps p
peekfor (BC.singleton ':') doReadPrim mzero
instance (Commute p, MyEq p, MyEq (PrimOf p)) => Eq (Non p C(x)) where
Non (cx :: FL p C(x y1)) (x :: PrimOf p C(y1 z1))
== Non (cy :: FL p C(x y2)) (y :: PrimOf p C(y2 z2)) =
case cx =\/= cy of
IsEq -> case x =\/= y :: EqCheck C(z1 z2) of
IsEq -> True
NotEq -> False
NotEq -> False
class Nonable p where
non :: p C(x y) -> Non p C(x)
commuteOrAddToCtx :: (Patchy p, ToFromPrim p) => p C(x y) -> Non p C(y)
-> Non p C(x)
commuteOrAddToCtx p n | Just n' <- p >* n = n'
commuteOrAddToCtx p (Non c x) = Non (p:>:c) x
commuteOrAddToCtxRL :: (Patchy p, ToFromPrim p) => RL p C(x y) -> Non p C(y)
-> Non p C(x)
commuteOrAddToCtxRL NilRL n = n
commuteOrAddToCtxRL (p:<:ps) n = commuteOrAddToCtxRL ps $ commuteOrAddToCtx p n
class WL l where
toFL :: l p C(x y) -> FL p C(x y)
toRL :: l p C(x y) -> RL p C(x y)
invertWL :: Invert p => l p C(x y) -> l p C(y x)
instance WL FL where
toFL = id
toRL = reverseFL
invertWL = reverseRL . invertFL
instance WL RL where
toFL = reverseRL
toRL = id
invertWL = reverseFL . invertRL
commutePrimsOrAddToCtx :: (WL l, Patchy p, ToFromPrim p) => l (PrimOf p) C(x y)
-> Non p C(y) -> Non p C(x)
commutePrimsOrAddToCtx q = commuteOrAddToCtxRL (mapRL_RL fromPrim $ toRL q)
remNons :: (Nonable p, Effect p, Patchy p, ToFromPrim p, PrimPatchBase p,
MyEq (PrimOf p)) => [Non p C(x)] -> Non p C(x) -> Non p C(x)
remNons ns n@(Non c x) = case remNonHelper ns c of
NilFL :> c' -> Non c' x
_ -> n
where
remNonHelper :: (Nonable p, Effect p, Patchy p, ToFromPrim p,
PrimPatchBase p, MyEq (PrimOf p)) => [Non p C(x)]
-> FL p C(x y) -> (FL (PrimOf p) :> FL p) C(x y)
remNonHelper [] x = NilFL :> x
remNonHelper _ NilFL = NilFL :> NilFL
remNonHelper ns (c:>:cs)
| non c `elem` ns =
let nsWithoutC = delete (non c) ns in
let commuteOrAddInvC = commuteOrAddToCtx $ invert c in
case remNonHelper (map commuteOrAddInvC $ nsWithoutC) cs of
a :> z -> sortCoalesceFL (effect c +>+ a) :> z
| otherwise = case commuteWhatWeCanFL (c :> cs) of
b :> c' :> d -> case remNonHelper ns b of
a :> b' -> a :> (b' +>+ c' :>: d)
commuteOrRemFromCtx :: (Patchy p, ToFromPrim p) => p C(x y) -> Non p C(x)
-> Maybe (Non p C(y))
commuteOrRemFromCtx p n | n'@(Just _) <- n *> p = n'
commuteOrRemFromCtx p (Non pc x) = removeFL p pc >>= \c -> return (Non c x)
commuteOrRemFromCtxFL :: (Patchy p, ToFromPrim p) => FL p C(x y) -> Non p C(x)
-> Maybe (Non p C(y))
commuteOrRemFromCtxFL NilFL n = Just n
commuteOrRemFromCtxFL (p:>:ps) n = do n' <- commuteOrRemFromCtx p n
commuteOrRemFromCtxFL ps n'
(*>) :: (Patchy p, ToFromPrim p) => Non p C(x) -> p C(x y)
-> Maybe (Non p C(y))
n *> p = invert p >* n
(>*) :: (Patchy p, ToFromPrim p) => p C(x y) -> Non p C(y)
-> Maybe (Non p C(x))
y >* (Non c x) = do
c' :> y' <- commuteFL (y :> c)
px' :> _ <- commute (y' :> fromPrim x)
x' <- toPrim px'
return (Non c' x')
(*>>) :: (WL l, Patchy p, ToFromPrim p, PrimPatchBase p) => Non p C(x)
-> l (PrimOf p) C(x y) -> Maybe (Non p C(y))
n *>> p = invertWL p >>* n
(>>*) :: (WL l, Patchy p, ToFromPrim p) => l (PrimOf p) C(x y) -> Non p C(y)
-> Maybe (Non p C(x))
ps >>* n = commuteRLPastNon (toRL ps) n
where
commuteRLPastNon :: (Patchy p, ToFromPrim p) => RL (PrimOf p) C(x y)
-> Non p C(y) -> Maybe (Non p C(x))
commuteRLPastNon NilRL n = Just n
commuteRLPastNon (x:<:xs) n = fromPrim x >* n >>= commuteRLPastNon xs