#include "gadts.h"
module Darcs.Patch.Non
( Non(..), Nonable(..), unNon,
showNon, readNon, showNons, readNons,
add, rem, addP, remP, addPs, remPs, remAddP, remAddPs, remNons,
(*>), (>*), (*>>), (>>*),
propAdjustTwice ) where
import Prelude hiding ( rem )
import Data.List ( delete )
import Control.Monad ( liftM )
import Darcs.Patch.Prim ( Prim, FromPrim(..), ToFromPrim(..), Effect(..),
showPrim, FileNameFormat(..), sortCoalesceFL )
import Darcs.Patch.Patchy
import Darcs.Patch.ReadMonads ( ParserM, lexChar )
import Darcs.Witnesses.Ordered
import Darcs.Patch.Read ( readPrim )
import Darcs.Patch.Viewing ()
import Darcs.Patch.Permutations ( removeFL, commuteWhatWeCanFL )
import Darcs.Witnesses.Show
import Darcs.Witnesses.Sealed ( Sealed(Sealed) )
import Printer ( Doc, empty, vcat, hiddenPrefix, blueText, redText, ($$) )
showNons :: ShowPatch (FL p) => [Non p C(x)] -> Doc
showNons [] = empty
showNons xs = blueText "{{" $$ vcat (map showNon xs) $$ blueText "}}"
showNon :: ShowPatch (FL p) => Non p C(x) -> Doc
showNon (Non c p) = hiddenPrefix "|" (showPatch c)
$$ hiddenPrefix "|" (blueText ":")
$$ showPrim NewFormat p
readNons :: (ReadPatch p, ParserM m) => m [Non p C(x)]
readNons = peekfor "{{" rns (return [])
where rns = peekfor "}}" (return []) $
do Just (Sealed ps) <- readPatch' False
lexChar ':'
Just (Sealed p) <- readPrim NewFormat
(Non ps p :) `liftM` rns
readNon :: (ReadPatch p, ParserM m) => m (Maybe (Non p C(x)))
readNon = do Just (Sealed ps) <- readPatch' False
peekfor ":" (do Just (Sealed p) <- readPrim NewFormat
return $ Just $ Non ps p)
(return Nothing)
instance (Commute p, MyEq p) => Eq (Non p C(x)) where
(Non cx x) == (Non cy y) | IsEq <- cx =\/= cy,
IsEq <- x =\/= y = True
| otherwise = False
data Non p C(x) where
Non :: FL p C(a x) -> Prim C(x y) -> Non p C(a)
unNon :: FromPrim p => Non p C(x) -> Sealed (FL p C(x))
unNon (Non c x) = Sealed (c +>+ fromPrim x :>: NilFL)
class Nonable p where
non :: p C(x y) -> Non p C(x)
addP :: (Patchy p, ToFromPrim p) => p C(x y) -> Non p C(y) -> Non p C(x)
addP p n | Just n' <- p >* n = n'
addP p (Non c x) = Non (p:>:c) x
addPs :: (Patchy p, ToFromPrim p) => RL p C(x y) -> Non p C(y) -> Non p C(x)
addPs NilRL n = n
addPs (p:<:ps) n = addPs ps $ addP p n
add :: (Effect q, Patchy p, ToFromPrim p) => q C(x y) -> Non p C(y) -> Non p C(x)
add q = addPs (mapRL_RL fromPrim $ effectRL q)
remNons :: (Nonable p, Effect p, Patchy p, ToFromPrim p, ShowPatch p) => [Non p C(x)] -> Non p C(x) -> Non p C(x)
remNons ns (Non c x) = case remNonHelper ns c of
NilFL :> c' -> Non c' x
_ -> Non c x
remNonHelper :: (Nonable p, Effect p, Patchy p, ToFromPrim p) => [Non p C(x)] -> FL p C(x y)
-> (FL Prim :> FL p) C(x y)
remNonHelper [] x = NilFL :> x
remNonHelper ns (c:>:cs)
| non c `elem` ns = case remNonHelper (map (addP $ invert c) $ delete (non c) ns) 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)
remNonHelper _ NilFL = NilFL :> NilFL
remP :: (Patchy p, ToFromPrim p) => p C(x y) -> Non p C(x) -> Maybe (Non p C(y))
remP p n | Just n' <- n *> p = Just n'
remP p (Non pc x) = do c <- removeFL p pc
return (Non c x)
remPs :: (Patchy p, ToFromPrim p) => FL p C(x y) -> Non p C(x) -> Maybe (Non p C(y))
remPs NilFL n = Just n
remPs (p:>:ps) n = remP p n >>= remPs ps
rem :: (Effect q, Patchy p, ToFromPrim p) => q C(x y) -> Non p C(x) -> Maybe (Non p C(y))
rem q = remPs (mapFL_FL fromPrim $ effect q)
remAddP :: (Patchy p, ToFromPrim p) => p C(x y) -> Non p C(y) -> Non p C(x)
remAddP p n = maybe (addP p n) id $ remP (invert p) n
remAddPs :: (Patchy p, ToFromPrim p) => RL p C(x y) -> Non p C(y) -> Non p C(x)
remAddPs NilRL n = n
remAddPs (x:<:xs) n = remAddPs xs $ remAddP x 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) = case commuteFLorComplain (y :> c) of
Right (c' :> y') -> do
px' :> _ <- commute (y' :> fromPrim x)
x' <- toPrim px'
return (Non c' x')
_ -> Nothing
(*>>) :: (Effect q, Patchy q, Patchy p, ToFromPrim p) => Non p C(x) -> q C(x y) -> Maybe (Non p C(y))
n *>> p = invert p >>* n
(>>*) :: (Effect q, Patchy p, ToFromPrim p) => q C(x y) -> Non p C(y) -> Maybe (Non p C(x))
q >>* nn = adj (effectRL q) nn
where adj :: (Patchy p, ToFromPrim p) => RL Prim C(x y) -> Non p C(y) -> Maybe (Non p C(x))
adj NilRL n = Just n
adj (x:<:xs) n = fromPrim x >* n >>= adj xs
propAdjustTwice :: (Patchy p, ToFromPrim p) => p C(x y) -> Non p C(y) -> Maybe Doc
propAdjustTwice p n =
do n' <- p >* n
case n' *> p of
Nothing -> Just (redText "prop_adjust_inverse 1")
Just n'' | n'' /= n -> Just (redText "prop_adjust_inverse 2")
_ -> case n *> invert p of
Nothing -> Just (redText "prop_adjust_inverse 3")
Just n'' | n'' /= n' -> Just (redText "prop_adjust_inverse 4")
_ -> case invert p >* n' of
Nothing -> Just (redText "prop_adjust_inverse 5")
Just n'' | n'' /= n -> Just (redText "prop_adjust_inverse 6")
_ -> Nothing
instance Nonable Prim where
non = Non NilFL
instance Show2 p => Show (Non p C(x)) where
showsPrec d (Non cs p) = showParen (d > appPrec) $ showString "Non " .
showsPrec2 (appPrec + 1) cs . showString " " .
showsPrec (appPrec + 1) p
instance Show2 p => Show1 (Non p) where
showDict1 = ShowDictClass
instance Patchy Prim