{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE CPP #-}
#if __GLASGOW_HASKELL__ < 806
{-# LANGUAGE TypeInType #-}
#endif

-- | Recursive definitions of various core vinyl functions. These are
-- simple definitions that put less strain on the compiler. They are
-- expected to have slower run times, but faster compile times than
-- the definitions in "Data.Vinyl.Core".
module Data.Vinyl.Recursive where
#if __GLASGOW_HASKELL__ < 806
import Data.Kind
#endif
import Data.Proxy (Proxy(..))
import Data.Vinyl.Core (rpure, RecApplicative, Rec(..), Dict(..))
import Data.Vinyl.Functor (Compose(..), (:.), Lift(..), Const(..))
import Data.Vinyl.TypeLevel

-- | Two records may be pasted together.
rappend
  :: Rec f as
  -> Rec f bs
  -> Rec f (as ++ bs)
rappend :: forall {k} (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
rappend Rec f as
RNil Rec f bs
ys = Rec f bs
ys
rappend (f r
x :& Rec f rs
xs) Rec f bs
ys = f r
x forall {u} (f :: u -> *) (r :: u) (rs :: [u]).
f r -> Rec f rs -> Rec f (r : rs)
:& (Rec f rs
xs forall {k} (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
`rappend` Rec f bs
ys)

-- | A shorthand for 'rappend'.
(<+>)
  :: Rec f as
  -> Rec f bs
  -> Rec f (as ++ bs)
<+> :: forall {k} (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
(<+>) = forall {k} (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
rappend

-- | 'Rec' @_ rs@ with labels in kind @u@ gives rise to a functor @Hask^u ->
-- Hask@; that is, a natural transformation between two interpretation functors
-- @f,g@ may be used to transport a value from 'Rec' @f rs@ to 'Rec' @g rs@.
rmap
  :: (forall x. f x -> g x)
  -> Rec f rs
  -> Rec g rs
rmap :: forall {u} (f :: u -> *) (g :: u -> *) (rs :: [u]).
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
rmap forall (x :: u). f x -> g x
_ Rec f rs
RNil = forall {u} (f :: u -> *). Rec f '[]
RNil
rmap forall (x :: u). f x -> g x
η (f r
x :& Rec f rs
xs) = forall (x :: u). f x -> g x
η f r
x forall {u} (f :: u -> *) (r :: u) (rs :: [u]).
f r -> Rec f rs -> Rec f (r : rs)
:& (forall (x :: u). f x -> g x
η forall {u} (f :: u -> *) (g :: u -> *) (rs :: [u]).
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
`rmap` Rec f rs
xs)
{-# INLINE rmap #-}

-- | A shorthand for 'rmap'.
(<<$>>)
  :: (forall x. f x -> g x)
  -> Rec f rs
  -> Rec g rs
<<$>> :: forall {u} (f :: u -> *) (g :: u -> *) (rs :: [u]).
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
(<<$>>) = forall {u} (f :: u -> *) (g :: u -> *) (rs :: [u]).
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
rmap
{-# INLINE (<<$>>) #-}

-- | An inverted shorthand for 'rmap'.
(<<&>>)
  :: Rec f rs
  -> (forall x. f x -> g x)
  -> Rec g rs
Rec f rs
xs <<&>> :: forall {u} (f :: u -> *) (rs :: [u]) (g :: u -> *).
Rec f rs -> (forall (x :: u). f x -> g x) -> Rec g rs
<<&>> forall (x :: u). f x -> g x
f = forall {u} (f :: u -> *) (g :: u -> *) (rs :: [u]).
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
rmap forall (x :: u). f x -> g x
f Rec f rs
xs
{-# INLINE (<<&>>) #-}

-- | A record of components @f r -> g r@ may be applied to a record of @f@ to
-- get a record of @g@.
rapply
  :: Rec (Lift (->) f g) rs
  -> Rec f rs
  -> Rec g rs
rapply :: forall {u} (f :: u -> *) (g :: u -> *) (rs :: [u]).
Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs
rapply Rec (Lift (->) f g) rs
RNil Rec f rs
RNil = forall {u} (f :: u -> *). Rec f '[]
RNil
rapply (Lift (->) f g r
f :& Rec (Lift (->) f g) rs
fs) (f r
x :& Rec f rs
xs) = forall l l' k (op :: l -> l' -> *) (f :: k -> l) (g :: k -> l')
       (x :: k).
Lift op f g x -> op (f x) (g x)
getLift Lift (->) f g r
f f r
x forall {u} (f :: u -> *) (r :: u) (rs :: [u]).
f r -> Rec f rs -> Rec f (r : rs)
:& (Rec (Lift (->) f g) rs
fs forall {u} (f :: u -> *) (g :: u -> *) (rs :: [u]).
Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs
`rapply` Rec f rs
xs)
{-# INLINE rapply #-}

-- | A shorthand for 'rapply'.
(<<*>>)
  :: Rec (Lift (->) f g) rs
  -> Rec f rs
  -> Rec g rs
<<*>> :: forall {u} (f :: u -> *) (g :: u -> *) (rs :: [u]).
Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs
(<<*>>) = forall {u} (f :: u -> *) (g :: u -> *) (rs :: [u]).
Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs
rapply
{-# INLINE (<<*>>) #-}

-- | A record may be traversed with respect to its interpretation functor. This
-- can be used to yank (some or all) effects from the fields of the record to
-- the outside of the record.
rtraverse
  :: Applicative h
  => (forall x. f x -> h (g x))
  -> Rec f rs
  -> h (Rec g rs)
rtraverse :: forall {u} (h :: * -> *) (f :: u -> *) (g :: u -> *) (rs :: [u]).
Applicative h =>
(forall (x :: u). f x -> h (g x)) -> Rec f rs -> h (Rec g rs)
rtraverse forall (x :: u). f x -> h (g x)
_ Rec f rs
RNil      = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall {u} (f :: u -> *). Rec f '[]
RNil
rtraverse forall (x :: u). f x -> h (g x)
f (f r
x :& Rec f rs
xs) = forall {u} (f :: u -> *) (r :: u) (rs :: [u]).
f r -> Rec f rs -> Rec f (r : rs)
(:&) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (x :: u). f x -> h (g x)
f f r
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall {u} (h :: * -> *) (f :: u -> *) (g :: u -> *) (rs :: [u]).
Applicative h =>
(forall (x :: u). f x -> h (g x)) -> Rec f rs -> h (Rec g rs)
rtraverse forall (x :: u). f x -> h (g x)
f Rec f rs
xs
{-# INLINABLE rtraverse #-}

-- | Given a natural transformation from the product of @f@ and @g@ to @h@, we
-- have a natural transformation from the product of @'Rec' f@ and @'Rec' g@ to
-- @'Rec' h@. You can also think about this operation as zipping two records
-- with the same element types but different interpretations.
rzipWith
  :: (forall x  .     f x  ->     g x  ->     h x)
  -> (forall xs . Rec f xs -> Rec g xs -> Rec h xs)
rzipWith :: forall {k} (f :: k -> *) (g :: k -> *) (h :: k -> *).
(forall (x :: k). f x -> g x -> h x)
-> forall (xs :: [k]). Rec f xs -> Rec g xs -> Rec h xs
rzipWith forall (x :: k). f x -> g x -> h x
m = \Rec f xs
r -> case Rec f xs
r of
  Rec f xs
RNil        -> \Rec g xs
RNil        -> forall {u} (f :: u -> *). Rec f '[]
RNil
  (f r
fa :& Rec f rs
fas) -> \(g r
ga :& Rec g rs
gas) -> forall (x :: k). f x -> g x -> h x
m f r
fa g r
ga forall {u} (f :: u -> *) (r :: u) (rs :: [u]).
f r -> Rec f rs -> Rec f (r : rs)
:& forall {k} (f :: k -> *) (g :: k -> *) (h :: k -> *).
(forall (x :: k). f x -> g x -> h x)
-> forall (xs :: [k]). Rec f xs -> Rec g xs -> Rec h xs
rzipWith forall (x :: k). f x -> g x -> h x
m Rec f rs
fas Rec g rs
gas

-- | Map each element of a record to a monoid and combine the results.
rfoldMap :: forall f m rs.
     Monoid m
  => (forall x. f x -> m)
  -> Rec f rs
  -> m
rfoldMap :: forall {u} (f :: u -> *) m (rs :: [u]).
Monoid m =>
(forall (x :: u). f x -> m) -> Rec f rs -> m
rfoldMap forall (x :: u). f x -> m
f = forall (ss :: [u]). m -> Rec f ss -> m
go forall a. Monoid a => a
mempty
  where
  go :: forall ss. m -> Rec f ss -> m
  go :: forall (ss :: [u]). m -> Rec f ss -> m
go !m
m Rec f ss
record = case Rec f ss
record of
    Rec f ss
RNil -> m
m
    f r
r :& Rec f rs
rs -> forall (ss :: [u]). m -> Rec f ss -> m
go (forall a. Monoid a => a -> a -> a
mappend m
m (forall (x :: u). f x -> m
f f r
r)) Rec f rs
rs
  {-# INLINABLE go #-}
{-# INLINE rfoldMap #-}

-- | A record with uniform fields may be turned into a list.
recordToList
  :: Rec (Const a) rs
  -> [a]
recordToList :: forall {u} a (rs :: [u]). Rec (Const a) rs -> [a]
recordToList Rec (Const a) rs
RNil = []
recordToList (Const a r
x :& Rec (Const a) rs
xs) = forall k a (b :: k). Const a b -> a
getConst Const a r
x forall a. a -> [a] -> [a]
: forall {u} a (rs :: [u]). Rec (Const a) rs -> [a]
recordToList Rec (Const a) rs
xs


-- | Sometimes we may know something for /all/ fields of a record, but when
-- you expect to be able to /each/ of the fields, you are then out of luck.
-- Surely given @∀x:u.φ(x)@ we should be able to recover @x:u ⊢ φ(x)@! Sadly,
-- the constraint solver is not quite smart enough to realize this and we must
-- make it patently obvious by reifying the constraint pointwise with proof.
reifyConstraint
  :: RecAll f rs c
  => proxy c
  -> Rec f rs
  -> Rec (Dict c :. f) rs
reifyConstraint :: forall {u} (f :: u -> *) (rs :: [u]) (c :: * -> Constraint)
       (proxy :: (* -> Constraint) -> *).
RecAll f rs c =>
proxy c -> Rec f rs -> Rec (Dict c :. f) rs
reifyConstraint proxy c
prx Rec f rs
rec =
  case Rec f rs
rec of
    Rec f rs
RNil -> forall {u} (f :: u -> *). Rec f '[]
RNil
    (f r
x :& Rec f rs
xs) -> forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
Compose (forall (c :: * -> Constraint) a. c a => a -> Dict c a
Dict f r
x) forall {u} (f :: u -> *) (r :: u) (rs :: [u]).
f r -> Rec f rs -> Rec f (r : rs)
:& forall {u} (f :: u -> *) (rs :: [u]) (c :: * -> Constraint)
       (proxy :: (* -> Constraint) -> *).
RecAll f rs c =>
proxy c -> Rec f rs -> Rec (Dict c :. f) rs
reifyConstraint proxy c
prx Rec f rs
xs

-- | Build a record whose elements are derived solely from a
-- constraint satisfied by each.
rpureConstrained :: forall u c (f :: u -> *) proxy ts.
                    (AllConstrained c ts, RecApplicative ts)
                 => proxy c -> (forall a. c a => f a) -> Rec f ts
rpureConstrained :: forall u (c :: u -> Constraint) (f :: u -> *)
       (proxy :: (u -> Constraint) -> *) (ts :: [u]).
(AllConstrained c ts, RecApplicative ts) =>
proxy c -> (forall (a :: u). c a => f a) -> Rec f ts
rpureConstrained proxy c
_ forall (a :: u). c a => f a
f = forall (ts' :: [u]).
AllConstrained c ts' =>
Rec Proxy ts' -> Rec f ts'
go (forall {u} (rs :: [u]) (f :: u -> *).
RecApplicative rs =>
(forall (x :: u). f x) -> Rec f rs
rpure forall {k} (t :: k). Proxy t
Proxy)
  where go :: AllConstrained c ts' => Rec Proxy ts' -> Rec f ts'
        go :: forall (ts' :: [u]).
AllConstrained c ts' =>
Rec Proxy ts' -> Rec f ts'
go Rec Proxy ts'
RNil = forall {u} (f :: u -> *). Rec f '[]
RNil
        go (Proxy r
_ :& Rec Proxy rs
xs) = forall (a :: u). c a => f a
f forall {u} (f :: u -> *) (r :: u) (rs :: [u]).
f r -> Rec f rs -> Rec f (r : rs)
:& forall (ts' :: [u]).
AllConstrained c ts' =>
Rec Proxy ts' -> Rec f ts'
go Rec Proxy rs
xs

-- | Build a record whose elements are derived solely from a
-- list of constraint constructors satisfied by each.
rpureConstraints :: forall cs (f :: * -> *) proxy ts. (AllAllSat cs ts, RecApplicative ts)
                 => proxy cs -> (forall a. AllSatisfied cs a => f a) -> Rec f ts
rpureConstraints :: forall {k} (cs :: k) (f :: * -> *) (proxy :: k -> *) (ts :: [*]).
(AllAllSat cs ts, RecApplicative ts) =>
proxy cs -> (forall a. AllSatisfied cs a => f a) -> Rec f ts
rpureConstraints proxy cs
_ forall a. AllSatisfied cs a => f a
f = forall (ts' :: [*]). AllAllSat cs ts' => Rec Maybe ts' -> Rec f ts'
go (forall {u} (rs :: [u]) (f :: u -> *).
RecApplicative rs =>
(forall (x :: u). f x) -> Rec f rs
rpure forall a. Maybe a
Nothing)
  where go :: AllAllSat cs ts' => Rec Maybe ts' -> Rec f ts'
        go :: forall (ts' :: [*]). AllAllSat cs ts' => Rec Maybe ts' -> Rec f ts'
go Rec Maybe ts'
RNil = forall {u} (f :: u -> *). Rec f '[]
RNil
        go (Maybe r
_ :& Rec Maybe rs
xs) = forall a. AllSatisfied cs a => f a
f forall {u} (f :: u -> *) (r :: u) (rs :: [u]).
f r -> Rec f rs -> Rec f (r : rs)
:& forall (ts' :: [*]). AllAllSat cs ts' => Rec Maybe ts' -> Rec f ts'
go Rec Maybe rs
xs