THSpec.hs

{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE DeriveGeneric         #-}
{-# LANGUAGE DeriveTraversable     #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TemplateHaskell       #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}

-- | The derived 'ZipMatchK' and 'ZipMatchFoldK' instances must agree with the
-- generic ones.
--
-- Both are available for the same type: 'deriveZipMatchK' provides the
-- instances, and 'genericZipMatchWithK' and 'genericZipMatchFoldK' compute the
-- generic answers without needing them. So the test compares the two, on every
-- pair of a set of sample values, over the field shapes a signature actually
-- uses. The folds collect the components they meet, so the comparison also
-- checks the order in which they are combined.
module Data.ZipMatchK.THSpec (spec) where

import           Data.List.NonEmpty      (NonEmpty (..))
import           Generics.Kind           (LoT (..))
import qualified GHC.Generics            as GHC
import           Generics.Kind.TH        (deriveGenericK)
import           Test.Hspec

import           Data.ZipMatchK
import           Data.Maybe              (isJust)
import           Data.ZipMatchK.Generic  (genericZipMatchFoldK, genericZipMatchWithK)
import           Data.ZipMatchK.TH

-- | An annotation, standing for the extra parameter a generated signature has.
newtype Ann = Ann Int deriving (Eq, Show)
instance ZipMatchK Ann where zipMatchWithK = zipMatchViaEq

-- | A signature exercising every field shape the deriver has to compile: a
-- term, a scoped term, a constant, the extra parameter, a container of terms,
-- a container of scoped terms, and a nest of containers.
data RichSig a scope term
  = AppSig term term
  | LamSig scope
  | LitSig Ann
  | AnnSig a term
  | ManySig [term]
  | SomeSig (Maybe scope)
  | NestSig [Maybe term]
  | NonEmptySig (NonEmpty term)
  | EitherSig (Either Ann term)
  | PairSig (scope, term)
  | NullarySig
  deriving (GHC.Generic, Functor, Foldable, Traversable, Eq, Show)

deriveGenericK ''RichSig
deriveZipMatchK2 ''RichSig

-- | A plain signature bifunctor, with no extra parameters.
data LamSig scope term = App term term | Lam scope
  deriving (GHC.Generic, Functor, Foldable, Traversable, Eq, Show)

deriveGenericK ''LamSig
deriveZipMatchK ''LamSig

-- | A functor, as an annotation would be.
newtype Boxed term = Boxed [term]
  deriving (GHC.Generic, Functor, Foldable, Traversable, Eq, Show)

deriveGenericK ''Boxed
deriveZipMatchK1 ''Boxed

-- | Zip two values by equality, so that a zipped signature has the same type as
-- the signatures it came from, and can be compared with '=='.
zipEq :: Eq a => a -> a -> Maybe a
zipEq x y
  | x == y    = Just x
  | otherwise = Nothing

richSamples :: [RichSig Ann String String]
richSamples =
  [ AppSig "x" "y"
  , AppSig "x" "z"
  , LamSig "s"
  , LamSig "t"
  , LitSig (Ann 1)
  , LitSig (Ann 2)
  , AnnSig (Ann 1) "x"
  , AnnSig (Ann 2) "x"
  , ManySig []
  , ManySig ["x"]
  , ManySig ["x", "y"]
  , SomeSig Nothing
  , SomeSig (Just "s")
  , NestSig [Just "x", Nothing]
  , NestSig [Just "y", Nothing]
  , NonEmptySig ("x" :| [])
  , NonEmptySig ("x" :| ["y"])
  , EitherSig (Left (Ann 1))
  , EitherSig (Right "x")
  , PairSig ("s", "x")
  , NullarySig
  ]

lamSamples :: [LamSig String String]
lamSamples = [App "x" "y", App "x" "x", Lam "s", Lam "t"]

boxedSamples :: [Boxed String]
boxedSamples = [Boxed [], Boxed ["x"], Boxed ["x", "y"]]

spec :: Spec
spec = do
  describe "deriveZipMatchK2" $
    it "agrees with the generic instance on every pair of samples" $
      sequence_
        [ zipMatchWithK @_ @(RichSig Ann) mappings x y
            `shouldBe` genericZipMatchWithK @(RichSig Ann) mappings x y
        | x <- richSamples, y <- richSamples ]

  describe "deriveZipMatchK" $
    it "agrees with the generic instance on every pair of samples" $
      sequence_
        [ zipMatchWithK @_ @LamSig mappings x y
            `shouldBe` genericZipMatchWithK @LamSig mappings x y
        | x <- lamSamples, y <- lamSamples ]

  describe "deriveZipMatchK1" $
    it "agrees with the generic instance on every pair of samples" $
      sequence_
        [ zipMatchWithK @_ @Boxed (zipEq :^: M0) x y
            `shouldBe` genericZipMatchWithK @Boxed (zipEq :^: M0) x y
        | x <- boxedSamples, y <- boxedSamples ]

  describe "deriveZipMatchK2, ZipMatchFoldK" $ do
    it "agrees with the generic instance on every pair of samples" $
      sequence_
        [ zipMatchFoldK @_ @(RichSig Ann) folds x y
            `shouldBe` genericZipMatchFoldK @(RichSig Ann) folds x y
        | x <- richSamples, y <- richSamples ]
    it "fails exactly where zipMatchWithK fails" $
      sequence_
        [ isJust (zipMatchFoldK @_ @(RichSig Ann) folds x y)
            `shouldBe` isJust (zipMatchWithK @_ @(RichSig Ann) keep x y)
        | x <- richSamples, y <- richSamples ]

  describe "deriveZipMatchK, ZipMatchFoldK" $
    it "agrees with the generic instance on every pair of samples" $
      sequence_
        [ zipMatchFoldK @_ @LamSig folds x y
            `shouldBe` genericZipMatchFoldK @LamSig folds x y
        | x <- lamSamples, y <- lamSamples ]

  describe "deriveZipMatchK1, ZipMatchFoldK" $
    it "agrees with the generic instance on every pair of samples" $
      sequence_
        [ zipMatchFoldK @_ @Boxed (collect "t" :%: F0) x y
            `shouldBe` genericZipMatchFoldK @Boxed (collect "t" :%: F0) x y
        | x <- boxedSamples, y <- boxedSamples ]
  where
    mappings :: Mappings (String ':&&: String ':&&: 'LoT0) (String ':&&: String ':&&: 'LoT0) (String ':&&: String ':&&: 'LoT0)
    mappings = zipEq :^: zipEq :^: M0

    -- Functions that always succeed, so that only the shapes can fail.
    keep :: Mappings (String ':&&: String ':&&: 'LoT0) (String ':&&: String ':&&: 'LoT0) (String ':&&: String ':&&: 'LoT0)
    keep = (\x _ -> Just x) :^: (\x _ -> Just x) :^: M0

    folds :: Folds [String] (String ':&&: String ':&&: 'LoT0) (String ':&&: String ':&&: 'LoT0)
    folds = collect "s" :%: collect "t" :%: F0

    -- The two components, tagged with the position they come from.
    collect :: String -> String -> String -> [String]
    collect tag x y = [tag ++ ":" ++ x ++ "/" ++ y]