-- Copyright (C) 2007 David Roundy
--
-- This program is free software; you can redistribute it and/or modify
-- it under the terms of the GNU General Public License as published by
-- the Free Software Foundation; either version 2, or (at your option)
-- any later version.
--
-- This program is distributed in the hope that it will be useful,
-- but WITHOUT ANY WARRANTY; without even the implied warranty of
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-- GNU General Public License for more details.
--
-- You should have received a copy of the GNU General Public License
-- along with this program; see the file COPYING.  If not, write to
-- the Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor,
-- Boston, MA 02110-1301, USA.

{-# 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 )

-- |A 'Non' stores a context with a 'Prim' patch. It is a patch whose effect
-- isn't visible - a Non-affecting patch.
data Non p wX where
    Non :: FL p wX wY -> PrimOf p wY wZ -> Non p wX

-- |unNon converts a Non into a FL of its context followed by the primitive
-- patch.
unNon :: FromPrim p => Non p wX -> Sealed (FL p wX)
unNon :: Non p wX -> Sealed (FL p wX)
unNon (Non FL p wX wY
c PrimOf p wY wZ
x) = FL p wX wZ -> Sealed (FL p wX)
forall (a :: * -> *) wX. a wX -> Sealed a
Sealed (FL p wX wY
c FL p wX wY -> FL p wY wZ -> FL p wX wZ
forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ PrimOf p wY wZ -> p wY wZ
forall (p :: * -> * -> *) wX wY.
FromPrim p =>
PrimOf p wX wY -> p wX wY
fromAnonymousPrim PrimOf p wY wZ
x p wY wZ -> FL p wZ wZ -> FL p wY wZ
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p wZ 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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
appPrec) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"Non " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                             Int -> FL p wX wY -> ShowS
forall (a :: * -> * -> *) wX wY. Show2 a => Int -> a wX wY -> ShowS
showsPrec2 (Int
appPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) FL p wX wY
cs ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                             Int -> PrimOf p wY wZ -> ShowS
forall (a :: * -> * -> *) wX wY. Show2 a => Int -> a wX wY -> ShowS
showsPrec2 (Int
appPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) PrimOf p wY wZ
p

instance (Show2 p, Show2 (PrimOf p)) => Show1 (Non p)

-- |showNons creates a Doc representing a list of Nons.
showNons :: (ShowPatchBasic p, PatchListFormat p, PrimPatchBase p)
         => ShowPatchFor -> [Non p wX] -> Doc
showNons :: 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 ((Non p wX -> Doc) -> [Non p wX] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (ShowPatchFor -> Non p wX -> Doc
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 creates a Doc representing a Non.
showNon :: (ShowPatchBasic p, PatchListFormat p, PrimPatchBase p)
        => ShowPatchFor
        -> Non p wX
        -> Doc
showNon :: ShowPatchFor -> Non p wX -> Doc
showNon ShowPatchFor
f (Non FL p wX wY
c PrimOf p wY wZ
p) = String -> Doc -> Doc
hiddenPrefix String
"|" (ShowPatchFor -> FL p wX wY -> Doc
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
$$ ShowPatchFor -> PrimOf p wY wZ -> Doc
forall (p :: * -> * -> *) wX wY.
ShowPatchBasic p =>
ShowPatchFor -> p wX wY -> Doc
showPatch ShowPatchFor
f PrimOf p wY wZ
p

-- |readNons is a parser that attempts to read a list of Nons.
readNons :: (ReadPatch p, PatchListFormat p, PrimPatchBase p)
         => Parser [Non p wX]
readNons :: Parser [Non p wX]
readNons = ByteString
-> Parser [Non p wX] -> Parser [Non p wX] -> Parser [Non p wX]
forall a. ByteString -> Parser a -> Parser a -> Parser a
peekfor (String -> ByteString
BC.pack String
"{{") Parser [Non p wX]
forall wX. Parser [Non p wX]
rns ([Non p wX] -> Parser [Non p wX]
forall (m :: * -> *) a. Monad m => a -> m a
return [])
  where rns :: Parser [Non p wX]
rns = ByteString
-> Parser [Non p wX] -> Parser [Non p wX] -> Parser [Non p wX]
forall a. ByteString -> Parser a -> Parser a -> Parser a
peekfor (String -> ByteString
BC.pack String
"}}") ([Non p wX] -> Parser [Non p wX]
forall (m :: * -> *) a. Monad m => a -> m a
return []) (Parser [Non p wX] -> Parser [Non p wX])
-> Parser [Non p wX] -> Parser [Non p wX]
forall a b. (a -> b) -> a -> b
$
              do Sealed FL p wX wX
ps <- Parser (Sealed (FL p wX))
forall (p :: * -> * -> *) wX. ReadPatch p => Parser (Sealed (p wX))
readPatch'
                 Char -> Parser ()
lexChar Char
':'
                 Sealed PrimOf p wX wX
p <- Parser (Sealed (PrimOf p wX))
forall (p :: * -> * -> *) wX. ReadPatch p => Parser (Sealed (p wX))
readPatch'
                 (FL p wX wX -> PrimOf p wX wX -> Non p wX
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 Non p wX -> [Non p wX] -> [Non p wX]
forall a. a -> [a] -> [a]
:) ([Non p wX] -> [Non p wX])
-> Parser [Non p wX] -> Parser [Non p wX]
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
`liftM` Parser [Non p wX]
rns

-- |readNon is a parser that attempts to read a single Non.
readNon :: (ReadPatch p, PatchListFormat p, PrimPatchBase p)
        => Parser (Non p wX)
readNon :: Parser (Non p wX)
readNon = do Sealed FL p wX wX
ps <- Parser (Sealed (FL p wX))
forall (p :: * -> * -> *) wX. ReadPatch p => Parser (Sealed (p wX))
readPatch'
             let doReadPrim :: Parser (Non p wX)
doReadPrim = do Sealed PrimOf p wX wX
p <- Parser (Sealed (PrimOf p wX))
forall (p :: * -> * -> *) wX. ReadPatch p => Parser (Sealed (p wX))
readPatch'
                                 Non p wX -> Parser (Non p wX)
forall (m :: * -> *) a. Monad m => a -> m a
return (Non p wX -> Parser (Non p wX)) -> Non p wX -> Parser (Non p wX)
forall a b. (a -> b) -> a -> b
$ FL p wX wX -> PrimOf p wX wX -> Non p wX
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
             ByteString
-> Parser (Non p wX) -> Parser (Non p wX) -> Parser (Non p wX)
forall a. ByteString -> Parser a -> Parser a -> Parser a
peekfor (Char -> ByteString
BC.singleton Char
':') Parser (Non p wX)
doReadPrim Parser (Non p wX)
forall (m :: * -> *) a. MonadPlus m => m a
mzero

-- |Nons are equal if their context patches are equal, and they have an equal
-- prim patch.
instance (Commute p, Eq2 p, Eq2 (PrimOf p)) => Eq (Non p wX) where
    Non (FL p wX wY
cx :: FL p wX wY1) (x :: PrimOf p wY1 wZ1)
     == :: Non p wX -> Non p wX -> Bool
== Non (FL p wX wY
cy :: FL p wX wY2) (y :: PrimOf p wY2 wZ2) =
      case FL p wX wY
cx FL p wX wY -> FL p wX wY -> EqCheck wY wY
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 PrimOf p wY wZ -> PrimOf p wY wZ -> EqCheck wZ wZ
forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= PrimOf p wY wZ
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

-- |Nonable represents the class of patches that can be turned into a Non.
class Nonable p where
    non :: p wX wY -> Non p wX

-- |'commuteOrAddToCtx' @x cy@ tries to commute @x@ past @cy@ and always
-- returns some variant @cy'@. If commutation suceeds, the variant is just
-- straightforwardly the commuted version. If commutation fails, the variant
-- consists of @x@ prepended to the context of @cy@.
commuteOrAddToCtx :: (Commute p, ToFromPrim p) => p wX wY -> Non p wY
                  -> Non p wX
commuteOrAddToCtx :: 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 p wX wY -> Non p wY -> Maybe (Non p wX)
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) = FL p wX wY -> PrimOf p wY wZ -> Non p wX
forall (p :: * -> * -> *) wX wY wZ.
FL p wX wY -> PrimOf p wY wZ -> Non p wX
Non (p wX wY
pp wX wY -> FL p wY wY -> FL p wX wY
forall (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' @xs cy@ commutes as many patches of @xs@ past @cy@
-- as possible, adding any that don't commute to the context of cy.  Suppose we
-- have
--
-- > x1 x2 x3 [c1 c2 y]
--
-- and that in our example @x1@ fails to commute past @c1@, this function
-- would commute down to
--
-- > x1 [c1'' c2'' y''] x2' x3'
--
-- and return @[x1 c1'' c2'' y'']@
commuteOrAddToCtxRL :: (Apply p, Commute p, Invert p, ToFromPrim p) => RL p wX wY -> Non p wY
                    -> Non p wX
commuteOrAddToCtxRL :: RL p wX wY -> Non p wY -> Non p wX
commuteOrAddToCtxRL RL p wX wY
NilRL Non p wY
n = Non p wX
Non p wY
n
commuteOrAddToCtxRL (RL p wX wY
ps:<:p wY wY
p) Non p wY
n = RL p wX wY -> Non p wY -> Non p wX
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 (Non p wY -> Non p wX) -> Non p wY -> Non p wX
forall a b. (a -> b) -> a -> b
$ p wY wY -> Non p wY -> Non p wY
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

-- |abstract over 'FL'/'RL'
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 :: FL p wX wY -> RL p wX wY
toRL = FL p wX wY -> RL p wX wY
forall (p :: * -> * -> *) wX wY. FL p wX wY -> RL p wX wY
reverseFL
   invertWL :: FL p wX wY -> FL p wY wX
invertWL = RL p wY wX -> FL p wY wX
forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL (RL p wY wX -> FL p wY wX)
-> (FL p wX wY -> RL p wY wX) -> FL p wX wY -> FL p wY wX
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FL p wX wY -> RL p wY wX
forall (p :: * -> * -> *) wX wY.
Invert p =>
FL p wX wY -> RL p wY wX
invertFL

instance WL RL where
   toRL :: RL p wX wY -> RL p wX wY
toRL = RL p wX wY -> RL p wX wY
forall a. a -> a
id
   invertWL :: RL p wX wY -> RL p wY wX
invertWL = FL p wY wX -> RL p wY wX
forall (p :: * -> * -> *) wX wY. FL p wX wY -> RL p wX wY
reverseFL (FL p wY wX -> RL p wY wX)
-> (RL p wX wY -> FL p wY wX) -> RL p wX wY -> RL p wY wX
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RL p wX wY -> FL p wY wX
forall (p :: * -> * -> *) wX wY.
Invert p =>
RL p wX wY -> FL p wY wX
invertRL

-- |commutePrimsOrAddToCtx takes a WL of prims and attempts to commute them
-- past a Non.
commutePrimsOrAddToCtx :: (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 -> Non p wY -> Non p wX
commutePrimsOrAddToCtx l (PrimOf p) wX wY
q = RL p wX wY -> Non p wY -> Non p wX
forall (p :: * -> * -> *) wX wY.
(Apply p, Commute p, Invert p, ToFromPrim p) =>
RL p wX wY -> Non p wY -> Non p wX
commuteOrAddToCtxRL ((forall wW wY. PrimOf p wW wY -> p wW wY)
-> RL (PrimOf p) wX wY -> RL p wX wY
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 wW wY. PrimOf p wW wY -> p wW wY
forall (p :: * -> * -> *) wX wY.
FromPrim p =>
PrimOf p wX wY -> p wX wY
fromAnonymousPrim (RL (PrimOf p) wX wY -> RL p wX wY)
-> RL (PrimOf p) wX wY -> RL p wX wY
forall a b. (a -> b) -> a -> b
$ l (PrimOf p) wX wY -> RL (PrimOf p) wX wY
forall (l :: (* -> * -> *) -> * -> * -> *) (p :: * -> * -> *) wX
       wY.
WL l =>
l p wX wY -> RL p wX wY
toRL l (PrimOf p) wX wY
q)

-- TODO: Figure out what remNons is for; it's is only used in one place - when
-- commuting two Conflictors:
--
-- > commute (Conflictor a1 n1 p1 :> Conflictor a2 n2 p2)
-- > ...
-- >   a1' = map (commutePrimsOrAddToCtx n2) a1
-- >   p2ooo = remNons a1' p2
-- >   n2n1 = n2 +>+ n1
-- > n1' :> n2' <- return $ filterConflictsFL p2ooo n2n1
--
-- which appears to be munging the not-yet-undone FLs in the Conflictors. a1'
-- will be the list of Nons with n2 commuted in/past them. So we then want to
-- modify p2, so that it doesn't have any of a1' in its context.

-- remNons really only works right if the relevant nons are conflicting...
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 :: [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 [Non p wX] -> FL p wX wY -> (:>) (FL (PrimOf p)) (FL p) wX wY
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' -> FL p wZ wY -> PrimOf p wY wZ -> Non p wZ
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 :: [Non p wX] -> FL p wX wY -> (:>) (FL (PrimOf p)) (FL p) wX wY
remNonHelper [] FL p wX wY
x = FL (PrimOf p) wX wX
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL FL (PrimOf p) wX wX
-> FL p wX wY -> (:>) (FL (PrimOf p)) (FL p) wX wY
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 = FL (PrimOf p) wX wX
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL FL (PrimOf p) wX wX
-> FL p wX wX -> (:>) (FL (PrimOf p)) (FL p) wX wX
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wX wX
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL
    remNonHelper [Non p wX]
ns (p wX wY
c:>:FL p wY wY
cs)
        | p wX wY -> Non p wX
forall (p :: * -> * -> *) wX wY. Nonable p => p wX wY -> Non p wX
non p wX wY
c Non p wX -> [Non p wX] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Non p wX]
ns =
          let nsWithoutC :: [Non p wX]
nsWithoutC = Non p wX -> [Non p wX] -> [Non p wX]
forall a. Eq a => a -> [a] -> [a]
delete (p wX wY -> Non p wX
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 = p wY wX -> Non p wX -> Non p wY
forall (p :: * -> * -> *) wX wY.
(Commute p, ToFromPrim p) =>
p wX wY -> Non p wY -> Non p wX
commuteOrAddToCtx (p wY wX -> Non p wX -> Non p wY)
-> p wY wX -> Non p wX -> Non p wY
forall a b. (a -> b) -> a -> b
$ p wX wY -> p wY wX
forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert p wX wY
c in
          case [Non p wY] -> FL p wY wY -> (:>) (FL (PrimOf p)) (FL p) wY wY
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 -> Non p wY) -> [Non p wX] -> [Non p wY]
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 -> FL (PrimOf p) wX wZ -> FL (PrimOf p) wX wZ
forall (prim :: * -> * -> *) wX wY.
PrimCanonize prim =>
FL prim wX wY -> FL prim wX wY
sortCoalesceFL (p wX wY -> FL (PrimOf p) wX wY
forall (p :: * -> * -> *) wX wY.
Effect p =>
p wX wY -> FL (PrimOf p) wX wY
effect p wX wY
c FL (PrimOf p) wX wY -> FL (PrimOf p) wY wZ -> FL (PrimOf p) wX wZ
forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ FL (PrimOf p) wY wZ
a) FL (PrimOf p) wX wZ
-> FL p wZ wY -> (:>) (FL (PrimOf p)) (FL p) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wZ wY
z
        | Bool
otherwise = case (:>) p (FL p) wX wY -> (:>) (FL p) (p :> FL p) wX wY
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p (FL p) wX wY -> (:>) (FL p) (p :> FL p) wX wY
commuteWhatWeCanFL (p wX wY
c p wX wY -> FL p wY wY -> (:>) p (FL p) wX wY
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 [Non p wX] -> FL p wX wZ -> (:>) (FL (PrimOf p)) (FL p) wX wZ
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 FL (PrimOf p) wX wZ
-> FL p wZ wY -> (:>) (FL (PrimOf p)) (FL p) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> (FL p wZ wZ
b' FL p wZ wZ -> FL p wZ wY -> FL p wZ wY
forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ p wZ wZ
c' p wZ wZ -> FL p wZ wY -> FL p wZ wY
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p wZ wY
d)

-- |commuteOrRemFromCtx attempts to remove a given patch from a Non. If the
-- patch was not in the Non, then the commute will succeed and the modified Non
-- will be returned. If the commute fails then the patch is either in the Non
-- context, or the Non patch itself; we attempt to remove the patch from the
-- context and then return the non with the updated context.
--
-- TODO: understand if there is any case where p is equal to the prim patch of
-- the Non, in which case, we return the original Non, is that right?
commuteOrRemFromCtx :: (Commute p, Invert p, Eq2 p, ToFromPrim p) => p wX wY -> Non p wX
     -> Maybe (Non p wY)
commuteOrRemFromCtx :: 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 Non p wX -> p wX wY -> Maybe (Non p wY)
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) = p wX wY -> FL p wX wY -> Maybe (FL p wY wY)
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 Maybe (FL p wY wY)
-> (FL p wY wY -> Maybe (Non p wY)) -> Maybe (Non p wY)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \FL p wY wY
c -> Non p wY -> Maybe (Non p wY)
forall (m :: * -> *) a. Monad m => a -> m a
return (FL p wY wY -> PrimOf p wY wZ -> Non p wY
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 attempts to remove a FL of patches from a Non,
-- returning Nothing if any of the individual removes fail.
commuteOrRemFromCtxFL :: (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 -> Non p wX -> Maybe (Non p wY)
commuteOrRemFromCtxFL FL p wX wY
NilFL Non p wX
n = Non p wX -> Maybe (Non p wX)
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' <- p wX wY -> Non p wX -> Maybe (Non p wY)
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
                                      FL p wY wY -> Non p wY -> Maybe (Non p wY)
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'

-- |(*>) attemts to modify a Non by commuting it past a given patch.
(*>) :: (Commute p, Invert p, ToFromPrim p) => Non p wX -> p wX wY
     -> Maybe (Non p wY)
Non p wX
n *> :: Non p wX -> p wX wY -> Maybe (Non p wY)
*> p wX wY
p = p wX wY -> p wY wX
forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert p wX wY
p p wY wX -> Non p wX -> Maybe (Non p wY)
forall (p :: * -> * -> *) wX wY.
(Commute p, ToFromPrim p) =>
p wX wY -> Non p wY -> Maybe (Non p wX)
>* Non p wX
n

-- |(>*) attempts to modify a Non, by commuting a given patch past it.
(>*) :: (Commute p, ToFromPrim p) => p wX wY -> Non p wY
     -> Maybe (Non p wX)
p wX wY
y >* :: 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' <- (:>) p (FL p) wX wY -> Maybe ((:>) (FL p) p wX wY)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p (FL p) wX wY -> Maybe ((:>) (FL p) p wX wY)
commuteFL (p wX wY
y p wX wY -> FL p wY wY -> (:>) p (FL p) wX wY
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
_ <- (:>) p p wZ wZ -> Maybe ((:>) p p wZ wZ)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p p wX wY -> Maybe ((:>) p p wX wY)
commute (p wZ wY
y' p wZ wY -> p wY wZ -> (:>) p p wZ wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> PrimOf p wY wZ -> p wY wZ
forall (p :: * -> * -> *) wX wY.
FromPrim p =>
PrimOf p wX wY -> p wX wY
fromAnonymousPrim PrimOf p wY wZ
x)
    PrimOf p wZ wZ
x' <- p wZ wZ -> Maybe (PrimOf p wZ wZ)
forall (p :: * -> * -> *) wX wY.
ToPrim p =>
p wX wY -> Maybe (PrimOf p wX wY)
toPrim p wZ wZ
px'
    Non p wX -> Maybe (Non p wX)
forall (m :: * -> *) a. Monad m => a -> m a
return (FL p wX wZ -> PrimOf p wZ wZ -> Non p wX
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')

-- |(*>>) attempts to modify a Non by commuting it past a given WL of patches.
(*>>) :: (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 *>> :: Non p wX -> l (PrimOf p) wX wY -> Maybe (Non p wY)
*>> l (PrimOf p) wX wY
p = l (PrimOf p) wX wY -> l (PrimOf p) wY wX
forall (l :: (* -> * -> *) -> * -> * -> *) (p :: * -> * -> *) wX
       wY.
(WL l, Invert p) =>
l p wX wY -> l p wY wX
invertWL l (PrimOf p) wX wY
p l (PrimOf p) wY wX -> Non p wX -> Maybe (Non p wY)
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

-- |(>>*) attempts to modify a Non by commuting a given WL of patches past it.
(>>*) :: (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 >>* :: l (PrimOf p) wX wY -> Non p wY -> Maybe (Non p wX)
>>* Non p wY
n = RL (PrimOf p) wX wY -> Non p wY -> Maybe (Non p wX)
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 (l (PrimOf p) wX wY -> RL (PrimOf p) wX wY
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 :: RL (PrimOf p) wX wY -> Non p wY -> Maybe (Non p wX)
commuteRLPastNon RL (PrimOf p) wX wY
NilRL Non p wY
n = Non p wY -> Maybe (Non p wY)
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 = PrimOf p wY wY -> p wY wY
forall (p :: * -> * -> *) wX wY.
FromPrim p =>
PrimOf p wX wY -> p wX wY
fromAnonymousPrim PrimOf p wY wY
x p wY wY -> Non p wY -> Maybe (Non p wY)
forall (p :: * -> * -> *) wX wY.
(Commute p, ToFromPrim p) =>
p wX wY -> Non p wY -> Maybe (Non p wX)
>* Non p wY
n Maybe (Non p wY)
-> (Non p wY -> Maybe (Non p wX)) -> Maybe (Non p wX)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= RL (PrimOf p) wX wY -> Non p wY -> Maybe (Non p wX)
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