    -- 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 -cpp -fglasgow-exts -fno-warn-orphans #-}
    {-# LANGUAGE CPP #-}
    -- , TypeOperators, GADTs, FlexibleContexts #-}

    #include "gadts.h"

    -- |'NonPatch' and 'Non' patches are patches that store a context as a
    -- sequence of patches.  See "Darcs.Patch.Real" for example usage.
    module Darcs.Patch.Non
           ( NonPatch, Non(..), Nonable(..), unNon,
             showNon, readNon, showNons, readNons,
             add, rem, addP, remP, addPs, remPs, remAddP, remAddPs, remNons,
             (*>), (>*), (*>>), (>>*),
             prop_adjust_twice ) 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, lex_char )
    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, ($$) )

    --import Darcs.ColorPrinter ( traceDoc )
    --import Printer ( greenText )

    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
                       lex_char ':'
                       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) <- readPatch' False
                                 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

    -- | 'Non' stores a context with a 'Prim' patch.
    data Non p C(x) where
        Non :: FL p C(a x) -> Prim C(x y) -> Non p C(a)

    -- | Convenience type for non primitive patches
    type NonPatch C(x) = Non Prim C(x)

    -- | Return as a list the context followed by the primitive patch.
    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' @x cy@ tries to commute @x@ past @cy@ and always returns some
    -- variant @cy'@.  -- commutation suceeds, the variant is just
    -- straightforwardly the commuted versian.  If commutation fails, the variant
    -- consists of @x@ prepended to the context of @cy@.
    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' @xs cy@ commutes as many patches of @xs@ past @cy@ as
    --   possible, stopping at the first patch that fails to commute.
    --   Note the fact @xs@ is a 'RL'
    --
    --   Suppose we have
    --
    --   > x1 x2 x3 [c1 c2 y]
    --
    --   and that in our example @c1@ fails to commute past @x1@, this
    --   function would commute down to
    --
    --   > x1 [c1'' c2'' y''] x2' x3'
    --
    --   and return @[x1 c1'' c2'' y'']@
    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 really only works right if the relevant nons are conflicting...
    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 commuteFL (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

    prop_adjust_twice :: (Patchy p, ToFromPrim p) => p C(x y) -> Non p C(y) -> Maybe Doc
    prop_adjust_twice 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 = showsPrec1

    instance Show2 p => Show1 (Non p) where
        showsPrec1 d (Non cs p) = showParen (d > app_prec) $ showString "Non " .
                                  showsPrec2 (app_prec + 1) cs . showString " " .
                                  showsPrec (app_prec + 1) p

    instance Patchy Prim