{-# LANGUAGE CPP #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ConstraintKinds #-}
module Properties.Common where

import Data.HList.CommonMain
import Test.QuickCheck
import Data.Array.Unboxed
import Data.HList.Variant
import Data.Monoid
import Data.Semigroup
import Control.Lens
import Control.Applicative
import GHC.TypeLits (Symbol)
import Language.Haskell.TH

#if MIN_VERSION_hspec_expectations(0,8,0)
import Test.Hspec.Expectations (shouldBe, shouldReturn, Expectation, HasCallStack)
#else
import Test.Hspec.Expectations (shouldBe, shouldReturn, Expectation)
import GHC.Exts (Constraint)
type HasCallStack = (() :: Constraint)
#endif

hListT :: [TypeQ] -> TypeQ
hListT = foldr (\a b -> [t| $a ': $b |]) promotedNilT

hListE :: [ExpQ] -> ExpQ
hListE = foldr (\a b -> [| $a `HCons` $b |]) [| HNil |]

hNatE :: Int -> ExpQ
hNatE n = foldr appE [| hZero |] (replicate n [| hSucc |])

hNatT :: Int -> TypeQ
hNatT n = foldr appT [t| HZero |] (replicate n [t| HSucc |])


lx = Label :: Label "x"
ly = Label :: Label "y"
lz = Label :: Label "z"

data BinF b = BinF (b -> b -> b)

instance (bb ~ (b, b), b ~ b') => ApplyAB (BinF b') bb b where
    applyAB (BinF f) = uncurry f


-- | A more general type than @===@ used to
-- ensure that both sides can infer the same type
eq :: (Show a, Show b, HCast a b, HCast b a, Eq a, Eq b) => a -> b -> Property
eq x y = hCast x === Just y .&&. Just x === hCast y
infix 4 `eq`


shouldShowTo :: (HasCallStack, Show a) => a -> String -> Expectation
shouldShowTo x y = show x `shouldBe` y
infixr 0 `shouldShowTo`

shouldReturnShowTo :: (HasCallStack, Show a) => IO a -> String -> Expectation
shouldReturnShowTo x y = fmap show x `shouldReturn` y
infixr 0 `shouldReturnShowTo`

data HSuccF = HSuccF

instance (psn ~ Proxy (HSucc n),
        pn ~ Proxy n) => ApplyAB HSuccF pn psn where
    applyAB _ = hSucc


data HSplitAtAppend l = HSplitAtAppend (HList l)
instance (pn ~ Proxy n,
          HSplitAt n l a b,
          HAppend (HList a) (HList b),
          y ~ HAppendR (HList a) (HList b)) => ApplyAB (HSplitAtAppend l) pn y where
    applyAB (HSplitAtAppend l) n = case hSplitAt n l of
                                     (a,b) -> hAppend a b



data ConstTrue
instance HEqByFn ConstTrue
instance HEqBy ConstTrue x y True

data ConstFalse
instance HEqByFn ConstFalse
instance HEqBy ConstFalse x y False


instance Arbitrary a => Arbitrary (Tagged t a) where
    arbitrary = fmap Tagged arbitrary

instance Arbitrary (HList '[]) where
    arbitrary = return HNil

instance (Arbitrary x, Arbitrary (HList xs)) => Arbitrary (HList (x ': xs)) where
    arbitrary = do
      x <- arbitrary
      xs <- arbitrary
      return $ x `HCons` xs

instance (Arbitrary x, Arbitrary (Variant (Tagged t y ': ys)),
          HExtend (Tagged s (Maybe x)) (Variant (Tagged t y ': ys)),
          HNat2Integral (HLength ys))
        => Arbitrary (Variant (Tagged s x ': Tagged t y ': ys)) where
    arbitrary = do
      let nys = hNat2Integral (Proxy :: Proxy (HLength ys))
      x :: Maybe x <- frequency [ (1, Just <$> arbitrary), (nys+1, return Nothing) ]
      yys :: Variant (Tagged t y ': ys) <- arbitrary
      return $ Tagged x .*. yys

instance Arbitrary z => Arbitrary (Variant '[Tagged t z]) where
    arbitrary = do
      z <- arbitrary
      return $ mkVariant1 Label z

instance (CoArbitrary x, CoArbitrary (Variant (y ': z)),
         HNat2Integral n, n ~ HLength (y ': z)) => CoArbitrary (Variant (x ': y ': z)) where
    coarbitrary v = case splitVariant1' v of
          Left x -> variant (hNat2Integral (Proxy :: Proxy n) :: Int) . coarbitrary x
          Right v' -> coarbitrary v'

instance (CoArbitrary v, Unvariant '[Tagged t v] v) => CoArbitrary (Variant '[Tagged t v]) where
    coarbitrary v = coarbitrary (unvariant v)

-- | This type is used to make unique types with two members.
--
-- > (BoolN True :: BoolN "x") /= (BoolN True :: BoolN "y")
--
-- is a type error
newtype BoolN (n :: Symbol) = BoolN Bool
  deriving (Eq,CoArbitrary,Arbitrary,Show,Read,Ord)

boolN next = simple $ iso (\(BoolN x) -> x) BoolN next

instance Monoid (BoolN n) where
    mempty = BoolN (getAll mempty)
    mappend (BoolN x) (BoolN y) = BoolN (getAll (mappend (All x) (All y)))

instance Semigroup (BoolN n) where (<>) = mappend

#if !MIN_VERSION_QuickCheck(2,9,0)
instance Arbitrary (Identity (BoolN n)) where
    arbitrary = fmap return arbitrary
#endif


data HSortF = HSortF
instance (x ~ Record xs,
          y ~ Record ys,
          HRLabelSet ys,
          HSort xs ys) => ApplyAB HSortF x y where
  applyAB _ (Record x) = mkRecord (hSort x)