-- 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