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


import Language.Haskell.TH
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] ])
                   |]
                ]

          quantify :: TypeQ -> TypeQ
          quantify ty = forallT [ PlainTV (mkName ("x" ++ show i)) | i <- [1 .. n]] (return []) ty


          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

#if __GLASGOW_HASKELL__ < 710
  -- 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
#endif

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


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