module Darcs.Test.Patch.Properties.GenericUnwitnessed where

import qualified Darcs.Test.Patch.Properties.Generic as W
     ( permutivity, partialPermutivity
     , mergeConsistent, mergeArgumentsConsistent, mergeEitherWay
     , mergeCommute, patchAndInverseCommute, coalesceCommute, commuteInverses
     , recommute
     , show_read )
import Darcs.Test.Patch.Arbitrary.Generic ( Tree, MightBeEmptyHunk, MightHaveDuplicate )
import Darcs.Test.Patch.RepoModel( RepoModel, RepoState )
import Darcs.Test.Patch.WithState( WithStartState )

import qualified Darcs.Test.Patch.Properties.RepoPatchV2 as W ( propConsistentTreeFlattenings )
import Darcs.Test.Patch.WSub
import Darcs.Test.Util.TestResult

import Darcs.Patch.Invert ( Invert )
import Darcs.Patch.Read ( ReadPatch )
import Darcs.Patch.Show ( ShowPatchBasic, displayPatch )
import Darcs.Patch.Witnesses.Show
import Darcs.Patch.Witnesses.Eq
import Darcs.Patch.Witnesses.Sealed( Sealed )
import Darcs.Patch.Merge ( Merge )
import Darcs.Util.Printer ( Doc, redText, ($$) )
import qualified Darcs.Util.Tree as T ( Tree )


permutivity :: (ShowPatchBasic wp, Eq2 wp, WSub wp p)
            => (forall wX wY . (p :> p) wX wY -> Maybe ((p :> p) wX wY))
            -> (p :> p :> p) wA wB -> TestResult
permutivity f = W.permutivity (fmap toW . f . fromW) . toW

partialPermutivity :: (Invert wp, ShowPatchBasic wp, Eq2 wp, WSub wp p)
                    => (forall wX wY . (p :> p) wX wY -> Maybe ((p :> p) wX wY))
                    -> (p :> p :> p) wA wB -> TestResult
partialPermutivity f = W.partialPermutivity (fmap toW . f . fromW) . toW

mergeEitherWay :: (ShowPatchBasic wp, Eq2 wp, Merge wp, WSub wp p) => (p :\/: p) wX wY -> TestResult
mergeEitherWay = W.mergeEitherWay . toW

commuteInverses :: (Invert wp, ShowPatchBasic wp, Eq2 wp, WSub wp p)
                 => (forall wX wY . (p :> p) wX wY -> Maybe ((p :> p) wX wY))
                 -> (p :> p) wA wB -> TestResult
commuteInverses f = W.commuteInverses (fmap toW . f . fromW) . toW

recommute :: (ShowPatchBasic wp, MightHaveDuplicate wp, Eq2 wp, WSub wp p)
          => (forall wX wY . ((p :> p) wX wY -> Maybe ((p :> p) wX wY)))
          -> (p :> p) wA wB -> TestResult
recommute f = W.recommute (fmap toW . f . fromW) . toW

mergeCommute :: (MightHaveDuplicate wp, ShowPatchBasic wp, Eq2 wp, Merge wp, WSub wp p)
             => (p :\/: p) wX wY -> TestResult
mergeCommute = W.mergeCommute . toW

mergeConsistent :: (Merge wp, ShowPatchBasic wp, WSub wp p) =>
                           (forall wX wY . p wX wY -> Maybe Doc)
                        -> (p :\/: p) wA wB -> TestResult
mergeConsistent f = W.mergeConsistent (f . fromW) . toW

mergeArgumentsConsistent :: (ShowPatchBasic wp, WSub wp p) =>
                              (forall wX wY . p wX wY -> Maybe Doc)
                           -> (p :\/: p) wA wB -> TestResult
mergeArgumentsConsistent f = W.mergeArgumentsConsistent (f . fromW) . toW

show_read :: (ShowPatchBasic p, ReadPatch p, Eq2 p, Show2 p) => p wX wY -> TestResult
show_read = W.show_read

patchAndInverseCommute :: (Invert wp, ShowPatchBasic wp, Eq2 wp, WSub wp p) =>
                             (forall wX wY . (p :> p) wX wY -> Maybe ((p :> p) wX wY))
                          -> (p :> p) wA wB -> TestResult
patchAndInverseCommute f = W.patchAndInverseCommute (fmap toW . f . fromW) . toW


coalesceCommute :: MightBeEmptyHunk Prim2
                => (forall wX wY . (Prim2 :> Prim2) wX wY -> Maybe (FL Prim2 wX wY))
                -> (Prim2 :> Prim2 :> Prim2) wA wB -> TestResult
coalesceCommute f = W.coalesceCommute (fmap toW . f . fromW) . toW

consistentTreeFlattenings :: (RepoState model ~ T.Tree, RepoModel model)
                          => Sealed (WithStartState model (Tree Prim2)) -> TestResult
consistentTreeFlattenings = (\x -> if W.propConsistentTreeFlattenings x
                                      then succeeded
                                      else failed $ redText "oops")

commuteFails :: (Eq2 p, ShowPatchBasic p)
             => ((p :> p) wX wY -> Maybe ((p :> p) wX wY))
             -> (p :> p) wX wY
             -> TestResult
commuteFails c (x :> y) = case c (x :> y) of
                            Nothing -> succeeded
                            Just (y' :> x') ->
                              failed $ redText "x" $$ displayPatch x $$
                                       redText ":> y" $$ displayPatch y $$
                                       redText "y'" $$ displayPatch y' $$
                                       redText ":> x'" $$ displayPatch x'