{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TemplateHaskell #-}
-- NOTE:
--
-- To be able to compile with ghc-7.6 functions like foo are sometimes
-- called
--
-- $(varE 'foo) because this prevents ghc-7.6 from failing to typecheck
-- the expression (which fails because the number of elements in the
-- supplied HList isn't known until Properties.LengthDependentSplice)
module Properties.LengthDependent where


import Data.HList.HSort (hMSortBy)
import Data.HList.Variant (eqVariant)
import Data.HList.Record (hZipRecord2)
import Data.HList.HList (hAppend')
import Data.HList.CommonMain


#if MIN_VERSION_template_haskell(2,17,0)
import Language.Haskell.TH.Lib.Internal hiding (doE)
import Language.Haskell.TH (Name, mkName, doE)
#else
import Language.Haskell.TH
#endif

import Test.QuickCheck
import Properties.Common
import Test.Hspec
import Control.Lens
import Data.List (sort,permutations)
import Data.Monoid

hlN :: Int -> ExpQ
hlN n = [| \proxy -> hSequence
              $ $(varE 'hReplicate) $(hNatE n)
                    (arbitrary `asTypeOf` return proxy) |]

-- > $(rKN id n) (undefined :: t) :: Arbitrary t => Gen (HList [Record t1, Record t2, ... ])
--
-- where
--    t1 ~ '[Tagged 1 t, Tagged 2 t, Tagged 3 t, ... , Tagged n t]
--    t2 ~ '[Tagged 2 t, Tagged 1 t, Tagged 3 t, ... , Tagged n t]
--    tN ~ nth permutation of t1
rKN :: (forall a. [a] -> [a]) -- ^ take some subset of the permutations of 1 .. n
    -> Int
    -> ExpQ
rKN = rKN' (litT . numTyLit)


rKN' ::
    (Integer -> TypeQ) -- ^ make the label
    -> (forall a. [a] -> [a]) -- ^ take some subset of the permutations of 1 .. n
    -> Int
    -> ExpQ
rKN' mkLab takeK n = [| \proxy -> do
        $(recs [| arbitrary `asTypeOf` return proxy |])
            `asTypeOf` return $sig
         |]
    where sig = [| undefined |] `sigE` quantify [t| HList $(hListT rss) |]


          ti :: Int -> Name
          ti i = mkName ("t" ++ show i)

          recs gen = doE $
               [ bindS (varP (ti i)) gen   | i <- [1 .. n] ] ++
               [ noBindS
                  [| return $ $(hListE
                      [ [| unlabeled # $(hListE (map (varE . ti) is)) |]
                        | is <- takeK $ permutations [1 .. n] ])
                   |]
                ]

          myForallT :: [Name] -> TypeQ -> TypeQ
#if MIN_VERSION_template_haskell(2,17,0)
          myForallT ns = forallT [ plainInvisTV n inferredSpec | n <- ns ] (cxt [])
#else
          myForallT ns = forallT (map plainTV ns) (cxt [])
#endif
          quantify :: TypeQ -> TypeQ
          quantify = myForallT [ mkName ("x" ++ show i) | i <- [1 .. n]]


          rss :: [TypeQ]
          rss = takeK $
                [ [t| (Record :: [*] -> *) $(hListT (map taggedN ns)) |]
                   | ns <- permutations [1 .. fromIntegral n] ]

          -- taggedN 1 == [t| Tagged 1 x1 |]
          taggedN :: Integer -> TypeQ
          taggedN i = [t| Tagged $(mkLab i) $(varT (mkName ("x"++show i))) |]

-- | > $(rN n) :: a -> Record [Tagged 1 a, Tagged 2 a, ... Tagged n a]
rN n = [| \proxy -> $(varE 'hHead) `fmap` $(rKN (take 1) n) proxy |]


-- | > $(rNstr n) :: a -> Record [Tagged "1" a, Tagged "2" a, ... Tagged n a]
rNstr n = [| \proxy -> $(varE 'hHead) `fmap` $(rKN' (litT . strTyLit . show) (take 1) n) proxy |]

vN :: Int -> ExpQ
vN n = [| \proxy -> do
       let toV :: Gen (Record a) -> Variant a
           toV = undefined
       v <- arbitrary
       return (v `asTypeOf` toV ($(rN n) proxy))
  |]

-- specs for 1 HList of length >= 1
hl1 n1 = [| do
  let -- | generate a HList of length nMax containing elements
      -- selected from there
      genHL proxy = $(hlN n1) proxy

  it "hConcat/hAppend" $
      property $ do
        x <- genHL True
        y <- genHL True
        return $ conjoin [$(varE 'hConcat) ($(varE 'hBuild) x y) == hAppend x y,
                          $(varE 'hConcat) ($(varE 'hBuild) x y) == hAppend' x y,
                          $(varE 'hConcat) (hBuild x) == x]

  it "partition" $
      property $ do
        x <- genHL True
        return $ conjoin
          [hPartitionEq (Proxy :: Proxy ConstTrue) (Proxy :: Proxy ()) x `eq` (x, HNil),
           hPartitionEq (Proxy :: Proxy ConstFalse) (Proxy :: Proxy ()) x `eq` (HNil, x)]


  it "listAsHList/hList2List" $ do
      property $ do
        x <- genHL True
        return $ conjoin [
            review listAsHList x `eq` hList2List x,
            review listAsHList' x `eq` hList2List x]

  it "read/show" $
      property $ do
        xs <- genHL True
        return $ read (show xs) == xs

  it "hLength/hReplicate" $
      property $ do
        xs <- genHL True
        return $ hNat2Integral (hLength xs) == hNat2Integral $(hNatE n1)

  it "hInits last id" $
      property $ do
        xs <- genHL True
        return $ $(varE 'hLast) (hInits xs) == xs

  it "hInits head empty" $
      property $ do
        xs <- genHL True
        return $ hHead (hInits xs) == HNil

  it "hTails head id" $
      property $ do
        xs <- genHL True
        return $ hHead (hTails xs) == xs

  it "hTails last empty" $
      property $ do
        xs <- genHL True
        return $ $(varE 'hLast) (hTails xs) == HNil

  it "hScanr equals scanr" $
      property $ do
        f <- arbitrary
        a <- arbitrary
        hl <- genHL True
        return $ hList2List (hScanr (BinF f) a hl)
                == scanr f a (hList2List hl)

  it "hFoldr equals foldr" $
      property $ do
        f <- arbitrary
        a <- arbitrary
        hl <- genHL True
        return $ hFoldr (BinF f) a hl == foldr f a (hList2List hl)

  it "hFoldr1 equals foldr1" $
      property $ do
        f <- arbitrary
        hl <- genHL True
        return $ hFoldr1 (BinF f) hl == foldr1 f (hList2List hl)

  it "hFoldl equals foldl" $
      property $ do
        f <- arbitrary
        a <- arbitrary
        hl <- genHL True
        return $ hFoldl (BinF f) a hl == foldl f a (hList2List hl)

  it "hSplitAt" $
      property $ do
        hl <- genHL True
        let n = hLength hl
            l = hList2List hl
        -- hList2List doesn't like empty lists, and hMapOut id needs
        -- annotations, so the following cases are easier to construct
        -- than a direct comparison with splitAt
        return $ conjoin
          [ case hSplitAt hZero hl of
              (hNil, hl') -> (hNil `eq` HNil) .&&. (hl' `eq` hl),
            case $(varE 'hSplitAt) n hl of
              (hl', hNil) -> (hNil `eq` HNil) .&&. (hl' `eq` hl),

            $(varE 'hMap) (HSplitAtAppend hl) ($(varE 'hIterate) (hSucc n) HSuccF hZero) `eq` $(varE 'hReplicate) (hSucc n) hl ,
            map (\n -> uncurry (++) $ splitAt n l) [0 .. length l]      === replicate (length l+1) l
              -- the equivalent list-version
           ]

  it "hAppend empty is identity" $
      property $ do
        x <- genHL (BoolN True :: BoolN "x")
        return $ all (== x) [$(varE 'hAppend) HNil x, $(varE 'hAppend) x HNil]

  it "hReverse involution" $ do
      property $ do
        x <- genHL True
        return $ x == $(varE 'hReverse) (hReverse x)

  it "hReverse does nothing for ()" $
      let xs = $(varE 'hReplicate) $(hNatE n1) ()
      in xs `shouldBe` $(varE 'hReverse) xs

  it "hInit == tail on reverse" $
      property $ do
        let hInitReference xs = hReverse (hTail (hReverse xs))
        hl <- genHL True
        return $ $(varE 'hInit) hl `eq` $(varE 'hInitReference) hl

  it "hList2List/list2HList" $ property $ do
      x <- genHL True
      return $ list2HList (hList2List x) === Just x

  it "hMap equals map" $ property $ do
      f  <- arbitrary
      hl <- genHL True
      return $ hList2List (hMap f hl) `eq` map (f :: Bool -> BoolN "f") (hList2List hl)

  it "hZip" $ property $ do
      x <- genHL (BoolN True :: BoolN "x")
      y <- genHL (BoolN True :: BoolN "y")
      return $ hList2List (hZip x y) `eq` hList2List x `zip` hList2List y

  it "hZipRecord" $ property $ do
      x <- $(rN n1) (BoolN True :: BoolN "x")
      y <- $(rN n1) (BoolN True :: BoolN "y")
      let r1 = hZip x y ^. unlabeled & hList2List
          r2 = hZipRecord2 x y ^. unlabeled & hList2List
          r_ = hList2List (x ^. unlabeled) `zip` hList2List (y ^. unlabeled)

      return $ conjoin [
          r1 `eq` r_,
          r2 `eq` r_,
          hUnzip (hZip x y) `eq` (x,y) ]

  it "hZip/hUnZip" $ property $ do
      x <- genHL (BoolN True :: BoolN "x")
      y <- genHL (BoolN True :: BoolN "y")
      return $ hUnzip (hZip x y) == (x,y)

  it "hUnzip/hZip" $ property $ do
      xy <- genHL (BoolN True :: BoolN "x", BoolN True :: BoolN "y")
      let (x,y) = hUnzip xy
      return $ xy `eq` hZip x y

  it "hUnzip2/hZip2" $ property $ do
      xy <- genHL (BoolN True :: BoolN "x", BoolN True :: BoolN "y")
      let (x,y) = hUnzip2 xy
      return $ xy `eq` hZip2 x y

  -- XXX doesn't work with ghc-7.10.1
  -- (should be fixed for 7.10.2)
  it "hZip/hZip2" $ property $ do
      x <- genHL (BoolN True :: BoolN "x")
      y <- genHL (BoolN True :: BoolN "y")
      return $ hZip x y `eq` hZip2 x y

  -- lots of duplication, not sure if it's worth factoring out
  it "HList monoid unit" $
    property $ do
      x <- genHL (BoolN True :: BoolN "x")
      return $ conjoin
        [ x === (x `mappend` mempty),
          x === (mempty `mappend` x) ]
  it "Record monoid unit" $
    property $ do
      x <- $(rN n1) (BoolN True :: BoolN "x")
      return $ conjoin
        [ x === (x `mappend` mempty),
          x === (mempty `mappend` x) ]
  it "Variant monoid unit" $
    property $ do
      x <- $(rN n1) (BoolN True :: BoolN "x")
      return $ conjoin
        [ x === (x `mappend` mempty),
          x === (mempty `mappend` x) ]

  -- lots of duplication, not sure if it's worth factoring out
  it "HList monoid assoc" $
    property $ do
      x <- genHL (BoolN True :: BoolN "x")
      y <- genHL (BoolN True :: BoolN "x")
      z <- genHL (BoolN True :: BoolN "x")
      return $ ((x `mappend` y) `mappend` z) `eq` (x `mappend` (y `mappend` z))
  it "Record monoid assoc" $ property $ do
    x <- $(rN n1) (BoolN True :: BoolN "x")
    y <- $(rN n1) (BoolN True :: BoolN "x")
    z <- $(rN n1) (BoolN True :: BoolN "x")
    return $ ((x `mappend` y) `mappend` z) `eq` (x `mappend` (y `mappend` z))
  it "Variant monoid assoc" $ property $ do
    x <- $(vN n1) (BoolN True :: BoolN "x")
    y <- $(vN n1) (BoolN True :: BoolN "x")
    z <- $(vN n1) (BoolN True :: BoolN "x")
    return $ ((x `mappend` y) `mappend` z) `eq` (x `mappend` (y `mappend` z))

  it "Variant == /eqVariant" $ property $ do
    x <- $(vN n1) (BoolN True :: BoolN "x")
    y <- $(vN n1) (BoolN True :: BoolN "x")
    return $ conjoin [ eqVariant x y == (x == y),
                       (x == y) == (y == x) ]

  it "Variant ord" $ property $ do
    x <- $(vN n1) (BoolN True :: BoolN "x")
    y <- $(vN n1) (BoolN True :: BoolN "x")
    z <- $(vN n1) (BoolN True :: BoolN "x")
    let xyz = [x,y,z]
        s:ss = map sort (permutations xyz)
    return $ all (s ==) ss

#if __GLASGOW_HASKELL__ > 707 && __GLASGOW_HASKELL__ < 901
  -- ghc-7.6 has no ordering for Nat (only for HNat)
  it "hSort (the labels)" $ property $ do
    x <- $(rN n1) True
    let rx = x & from hListRecord %~ hReverse
    -- rN generates a record that has labels in ascending order already
    return $ conjoin [
         x `eq` (x  & from hListRecord %~ hSort),
         x `eq` (rx & from hListRecord %~ hSort),
         x `eq` (x  & from hListRecord %~ hMSortBy (Proxy :: Proxy HLeFn)),
         x `eq` (rx & from hListRecord %~ hMSortBy (Proxy :: Proxy HLeFn))
         ]

  -- restrict to lists of length 4 (since then the number of permutations
  -- is a manageable 24 not 120)
  it "hSort permutations" $ property $ do
    xs <- $(rKN id (min 4 n1)) True
    return $ all (== hHead xs) (hMapOut HSortF xs)

#endif

  it "hRenameLabel" $ property $ do
    r <- $(rN n1) True
    return $ conjoin
        $(listE [ [| hRenameLabel $ln lx r .!. lx === r .!. $ln |]
              | i <- [1 .. n1],
                let ln = [| Label :: Label $(litT (numTyLit (fromIntegral i))) |]
            ])
#if __GLASGOW_HASKELL__ < 901
  it "rearranged / hMapR" $ property $ do
    r <- $(rN n1) True
    let revR = r & from hListRecord %~ hReverse
        asT :: x -> As x
        asT _ = id
    -- hMap works on the reversed list
    return $ hMapR not r === (r & rearranged' . asT revR . unlabeled %~ hMap not)
#endif


  it "hOccurs" $ property $ do
    w <- arbitrary :: Gen (BoolN "w")
    x <- genHL (BoolN True :: BoolN "x")
    y <- genHL (BoolN True :: BoolN "y")
    z <- genHL (BoolN True :: BoolN "z")
    let xyz = hConcat (hBuild x y z)
        hxyz = hEnd (hBuild (hHead x) (hHead y) (hHead z))

        -- -XNoMonoLocalBinds on ghc <= 7.10.4 allowed
        -- having one function
        hM1 v = hOccursMany xyz === hList2List v
        hM2 v = hOccursMany xyz === hList2List v
        hM3 v = hOccursMany xyz === hList2List v
    return $ conjoin
      [ hM1 x, hM2 y, hM3 z,
        hOccurs (hConcat (hBuild x (HCons w HNil) z)) === w,
        hOccursOpt xyz === (Nothing `asTypeOf` Just w)
        -- hProject hxyz === hBuild (hHead x) (hHead y)
       ]

 |]

hl2 n1 n2 = [| do
  it "splitVariant" $ property $ do
    x <- $(vN (n1 + n2)) True
    let testV :: forall n x yin yout.
               (Eq (Variant x),
                SplitVariant x yin yout,
                HSplitAt n x yin yout,
                ExtendsVariant yin x,
                ExtendsVariant yout x) =>
                Proxy n -> Variant x -> Bool
        testV n v = case $(varE 'splitVariant) v of
                      Left a -> extendsVariant (a :: Variant yin) == v
                      Right a -> extendsVariant (a :: Variant yout) == v
    return $ $(varE 'testV) $(hNatE n1) x


  it "hAppend equals ++" $
    property $ do
      x <- $(hlN n1) True
      y <- $(hlN n2) True
      return $ hList2List (hAppend x y) === hList2List x ++ hList2List y

  it "hTranspose involution" $ property $ do
    x <- return (error "hTranspose involution") `asTypeOf` $(hlN n1) True
    xx <- $(hlN n2) x
    return $ $(varE 'hTranspose) ($(varE 'hTranspose) xx) === xx

  it "leftUnion / unionSR" $
    property $ do
      x <- $(rN n1) True
      y <- $(rN n2) True
      let asL r = r ^. unlabeled . to hList2List
          asLs (r1,r2) = (asL r1, asL r2)
          merge xs ys = xs ++ drop (length xs) ys
          mergeSym xs ys = (merge xs ys, merge ys xs)
          eqSorted (a,b) (c,d) = sort a === sort c .&&. sort b === sort d
      return $ conjoin [
        asL (x .<++. y) === asL x `merge` asL y,
        ($(varE '(.<++.)) x x) === x,
        ($(varE '(.<++.)) y y) === y,
        asLs (unionSR x y) `eqSorted` mergeSym (asL x) (asL y),
        (x `unionSR` x) === (x,x),
        (y `unionSR` y) === (y,y)]

    |]

hl3 n1 n2 n3 = [| do
  it "hAppend/hAppendList assoc" $
    property $ do
      x <- $(hlN n1) (BoolN True :: BoolN "x")
      y <- $(hlN n2) (BoolN True :: BoolN "y")
      z <- $(hlN n3) (BoolN True :: BoolN "z")
      return $ conjoin
#if __GLASGOW_HASKELL__ < 707
        [ $([| (x `hAppend` y) `hAppend` z |]) === $([| x `hAppend` (y `hAppend` z) |]),
          $([| (x `hAppendList` y) `hAppendList` z|]) === $([| x `hAppendList` (y `hAppendList` z)|])
        ]
#else
        [ ((x `hAppend` y) `hAppend` z) === (x `hAppend` (y `hAppend` z)),
          ((x `hAppendList` y) `hAppendList` z) === (x `hAppendList` (y `hAppendList` z))
        ]
#endif
  |]