{-# LANGUAGE AllowAmbiguousTypes   #-}
{-# LANGUAGE BangPatterns          #-}
{-# LANGUAGE CPP                   #-}
{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}

{-| This module uses 'RecAll' to extend common typeclass methods to records.
    Generally, it is preferable to use the original typeclass methods to these
    variants. For example, in most places where 'recCompare' could be used,
    you could use 'compare' instead. They are useful in scenarios
    that involve working on unknown subsets of a record's fields
    because 'RecAll' constraints can easily be weakened. An example of this
    is given at the bottom of this page.
-}

module Data.Vinyl.Class.Method
  ( -- * Mapping methods over records
    RecMapMethod(..)
  , rmapMethodF
  , mapFields
  , RecMapMethod1(..)
  , RecPointed(..)
  , rtraverseInMethod
  , rsequenceInFields
    -- * Support for 'RecMapMethod'
  , FieldTyper, ApplyFieldTyper, PayloadType
    -- * Eq Functions
  ,  recEq
     -- * Ord Functions
  , recCompare
    -- * Monoid Functions
  , recMempty
  , recMappend
  , recMconcat
    -- * Num Functions
  , recAdd
  , recSubtract
  , recMultiply
  , recAbs
  , recSignum
  , recNegate
    -- * Bounded Functions
  , recMinBound
  , recMaxBound
    -- * Example
    -- $example
  ) where
import Data.Functor.Product (Product(Pair))
import Data.Vinyl.Core
import Data.Vinyl.Derived (KnownField, AllFields, FieldRec, traverseField)
import Data.Vinyl.Functor ((:.), getCompose, ElField(..))
import Data.Vinyl.TypeLevel
#if __GLASGOW_HASKELL__ < 804
import Data.Monoid
#endif

recEq :: RecAll f rs Eq => Rec f rs -> Rec f rs -> Bool
recEq RNil RNil = True
recEq (a :& as) (b :& bs) = a == b && recEq as bs

recCompare :: RecAll f rs Ord => Rec f rs -> Rec f rs -> Ordering
recCompare RNil RNil = EQ
recCompare (a :& as) (b :& bs) = compare a b <> recCompare as bs

-- | This function differs from the original 'mempty' in that
--   it takes an argument. In some cases, you will already
--   have a record of the type you are interested in, and
--   that can be passed an the argument. In other situations
--   where this is not the case, you may need the
--   interpretation function of the argument record to be
--   @Const ()@ or @Proxy@ so the you can generate the
--   argument with 'rpure'.
recMempty :: RecAll f rs Monoid => Rec proxy rs -> Rec f rs
recMempty RNil = RNil
recMempty (_ :& rs) = mempty :& recMempty rs

recMappend :: RecAll f rs Monoid => Rec f rs -> Rec f rs -> Rec f rs
recMappend RNil RNil = RNil
recMappend (a :& as) (b :& bs) = mappend a b :& recMappend as bs

-- | This function differs from the original 'mconcat'.
--   See 'recMempty'.
recMconcat :: RecAll f rs Monoid => Rec proxy rs -> [Rec f rs] -> Rec f rs
recMconcat p [] = recMempty p
recMconcat p (rec : recs) = recMappend rec (recMconcat p recs)

recAdd :: RecAll f rs Num => Rec f rs -> Rec f rs -> Rec f rs
recAdd RNil RNil = RNil
recAdd (a :& as) (b :& bs) = (a + b) :& recAdd as bs

recSubtract :: RecAll f rs Num => Rec f rs -> Rec f rs -> Rec f rs
recSubtract RNil RNil = RNil
recSubtract (a :& as) (b :& bs) = (a - b) :& recSubtract as bs

recMultiply :: RecAll f rs Num => Rec f rs -> Rec f rs -> Rec f rs
recMultiply RNil RNil = RNil
recMultiply (a :& as) (b :& bs) = (a * b) :& recSubtract as bs

recAbs :: RecAll f rs Num => Rec f rs -> Rec f rs
recAbs RNil = RNil
recAbs (a :& as) = abs a :& recAbs as

recSignum :: RecAll f rs Num => Rec f rs -> Rec f rs
recSignum RNil = RNil
recSignum (a :& as) = signum a :& recAbs as

recNegate :: RecAll f rs Num => Rec f rs -> Rec f rs
recNegate RNil = RNil
recNegate (a :& as) = negate a :& recAbs as

-- | This function differs from the original 'minBound'.
--   See 'recMempty'.
recMinBound :: RecAll f rs Bounded => Rec proxy rs -> Rec f rs
recMinBound RNil = RNil
recMinBound (_ :& rs) = minBound :& recMinBound rs

-- | This function differs from the original 'maxBound'.
--   See 'recMempty'.
recMaxBound :: RecAll f rs Bounded => Rec proxy rs -> Rec f rs
recMaxBound RNil = RNil
recMaxBound (_ :& rs) = maxBound :& recMaxBound rs

-- | When we wish to apply a typeclass method to each field of a
-- 'Rec', we typically care about typeclass instances of the record
-- field types irrespective of the record's functor context. To expose
-- the field types themselves, we utilize a constraint built from a
-- defunctionalized type family in the 'rmapMethod' method. The
-- symbols of the function space are defined by this data type.
data FieldTyper = FieldId | FieldSnd

-- | The interpretation function of the 'FieldTyper' symbols.
type family ApplyFieldTyper (f :: FieldTyper) (a :: k) :: * where
  ApplyFieldTyper 'FieldId a = a
  ApplyFieldTyper 'FieldSnd '(s, b) = b

-- | A mapping of record contexts into the 'FieldTyper' function
-- space. We explicitly match on 'ElField' to pick out the payload
-- type, and 'Compose' to pick out the inner-most context. All other
-- type constructor contexts are understood to not perform any
-- computation on their arguments.
type family FieldPayload (f :: u -> *) :: FieldTyper where
  FieldPayload ElField = 'FieldSnd
  FieldPayload (f :. g) = FieldPayload g
  FieldPayload f = 'FieldId

-- | Shorthand for combining 'ApplyFieldTyper' and 'FieldPayload'.
type family PayloadType f (a :: u) :: * where
  PayloadType f a = ApplyFieldTyper (FieldPayload f) a

-- | Generate a record from fields derived from type class
-- instances.
class RecPointed c f ts where
  rpointMethod :: (forall a. c (f a) => f a) -> Rec f ts

instance RecPointed c f '[] where
  rpointMethod _ = RNil
  {-# INLINE rpointMethod #-}

instance (c (f t), RecPointed c f ts)
  => RecPointed c f (t ': ts) where
  rpointMethod f = f :& rpointMethod @c f
  {-# INLINE rpointMethod #-}

-- | Apply a typeclass method to each field of a 'Rec' where the class
-- constrains the index of the field, but not its interpretation
-- functor.
class RecMapMethod c f ts where
  rmapMethod :: (forall a. c (PayloadType f a) => f a -> g a)
             -> Rec f ts -> Rec g ts

-- | Apply a typeclass method to each field of a 'Rec' where the class
-- constrains the field when considered as a value interpreted by the
-- record's interpretation functor.
class RecMapMethod1 c f ts where
  rmapMethod1 :: (forall a. c (f a) => f a -> g a)
              -> Rec f ts -> Rec g ts

instance RecMapMethod c f '[] where
  rmapMethod _ RNil = RNil
  {-# INLINE rmapMethod #-}

instance RecMapMethod1 c f '[] where
  rmapMethod1 _ RNil = RNil
  {-# INLINE rmapMethod1 #-}

instance (c (PayloadType f t), RecMapMethod c f ts)
  => RecMapMethod c f (t ': ts) where
  rmapMethod f (x :& xs) = f x :& rmapMethod @c f xs
  {-# INLINE rmapMethod #-}

instance (c (f t), RecMapMethod1 c f ts) => RecMapMethod1 c f (t ': ts) where
  rmapMethod1 f (x :& xs) = f x :& rmapMethod1 @c f xs
  {-# INLINE rmapMethod1 #-}

-- | Apply a typeclass method to each field of a @Rec f ts@ using the
-- 'Functor' instance for @f@ to lift the function into the
-- functor. This is a commonly-used specialization of 'rmapMethod'
-- composed with 'fmap'.
rmapMethodF :: forall c f ts. (Functor f, FieldPayload f ~ 'FieldId, RecMapMethod c f ts)
            => (forall a. c a => a -> a) -> Rec f ts -> Rec f ts
rmapMethodF f = rmapMethod @c (fmap f)
{-# INLINE rmapMethodF #-}

-- | Apply a typeclass method to each field of a 'FieldRec'. This is a
-- specialization of 'rmapMethod'.
mapFields :: forall c ts. RecMapMethod c ElField ts
           => (forall a. c a => a -> a) -> FieldRec ts -> FieldRec ts
mapFields f = rmapMethod @c g
  where g :: c (PayloadType ElField t) => ElField t -> ElField t
        g (Field x) = Field (f x)
{-# INLINE mapFields #-}

-- | Like 'rtraverseIn', but the function between functors may be
-- constrained.
rtraverseInMethod :: forall c h f g rs.
                     (RMap rs, RPureConstrained c rs, RApply rs)
                  => (forall a. c a => f a -> g (ApplyToField h a))
                  -> Rec f rs
                  -> Rec g (MapTyCon h rs)
rtraverseInMethod f = rtraverseIn @h (withPairedDict @c f)
                    . rzipWith Pair (rpureConstrained @c aux)
  where aux :: c b => DictOnly c b
        aux = DictOnly

-- Note: rtraverseInMethod is written with that `aux` helper in order
-- to work around compatibility with GHC < 8.4. Write it more
-- naturally as `DictOnly @c` does not work with older compilers.

-- | Push an outer layer of interpretation functor into each named field.
rsequenceInFields :: forall f rs. (Functor f, AllFields rs, RMap rs)
                  => Rec (f :. ElField) rs -> Rec ElField (MapTyCon f rs)
rsequenceInFields = rtraverseInMethod @KnownField (traverseField id . getCompose)


{- $example
    This module provides variants of typeclass methods that have
    a 'RecAll' constraint instead of the normal typeclass
    constraint. For example, a type-specialized 'compare' would
    look like this:

> compare :: Ord (Rec f rs) => Rec f rs -> Rec f rs -> Ordering

    The 'recCompare' function looks like this:

> recCompare :: RecAll f rs Ord => Rec f rs -> Rec f rs -> Ordering

    The only difference is the constraint. Let's look at a potential
    use case for these functions.

    Let's write a function that projects out a subrecord from two records and
    then compares those for equality. We can write this with
    the '<:' operator from @Data.Vinyl.Lens@ and the normal 'compare'
    function. We don't need 'recCompare':

> -- This needs ScopedTypeVariables
> projectAndCompare :: forall super sub f. (super <: sub, Ord (Rec f sub))
>                   => Proxy sub -> Rec f super -> Rec f super -> Ordering
> projectAndCompare _ a b = compare (rcast a :: Rec f sub) (rcast b :: Rec f sub)

    That works fine for the majority of use cases, and it is probably how you should
    write the function if it does everything you need. However, let's consider
    a somewhat more complicated case.

    What if the exact subrecord we were projecting couldn't be
    known at compile time? Assume that the end user was allowd to
    choose the fields on which he or she wanted to compare records.
    The @projectAndCompare@ function cannot handle this because of the
    @Ord (Rec f sub)@ constraint. Even if we amend the constraint to
    read @Ord (Rec f super)@ instead, we cannot use this information
    to recover the @Ord (Rec f sub)@ constraint that we need. Let's
    try another approach.

    We can use the following GADT to prove subsethood:

> data Sublist (super :: [k]) (sub :: [k]) where
>   SublistNil   :: Sublist '[]
>   SublistSuper :: Proxy r -> Sublist super sub -> Sublist (r ': super) sub
>   SublistBoth  :: Proxy r -> Sublist super sub -> Sublist (r ': super) (r ': sub)
>
> projectRec :: Sublist super sub -> Rec f super -> Rec f sub
> projectRec s r = case s of
>   SublistNil -> RNil
>   SublistBoth n snext -> case r of
>     rhead :& rtail -> rhead :& projectRec snext rtail
>   SublistSuper n snext -> case r of
>     rhead :& rtail -> projectRec snext rtail

    It is also possible to write a typeclass to generate @Sublist@s
    implicitly, but that is beyond the scope of this example. Let's
    now write a function to use @Sublist@ to weaken a 'RecAll'
    constraint:

> import Data.Vinyl.Core hiding (Dict)
> import Data.Constraint
>
> weakenRecAll :: Proxy f -> Proxy c -> Sublist super sub -> RecAll f super c :- RecAll f sub c
> weakenRecAll f c s = case s of
>   SublistNil -> Sub Dict
>   SublistSuper _ snext -> Sub $ case weakenRecAll f c snext of
>     Sub Dict -> Dict
>   SublistBoth _ snext -> Sub $ case weakenRecAll f c snext of
>     Sub Dict -> Dict

    Now we can write a different version of our original function:

> -- This needs ScopedTypeVariables
> projectAndCompare2 :: forall super sub f. (RecAll f super Ord)
>                    => Sublist super sub -> Rec f super -> Rec f super -> Ordering
> projectAndCompare2 s a b = case weakenRecAll (Proxy :: Proxy f) (Proxy :: Proxy Ord) s of
>   Sub Dict -> recCompare (projectRec s a) (projectRec s b)

    Notice that in this case, the 'Ord' constraint applies to the full set of fields
    and is then weakened to target a subset of them instead.
-}