{-# 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 :: Rec f as -> Rec f bs -> Rec f (as ++ bs)
rappend Rec f as
RNil Rec f bs
ys = Rec f bs
Rec f (as ++ bs)
ys
rappend (f r
x :& Rec f rs
xs) Rec f bs
ys = f r
x f r -> Rec f (rs ++ bs) -> Rec f (r : (rs ++ bs))
forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
:& (Rec f rs
xs Rec f rs -> Rec f bs -> Rec f (rs ++ bs)
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)
<+> :: Rec f as -> Rec f bs -> Rec f (as ++ bs)
(<+>) = 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 (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
rmap forall (x :: u). f x -> g x
_ Rec f rs
RNil = Rec g rs
forall u (f :: u -> *). Rec f '[]
RNil
rmap forall (x :: u). f x -> g x
η (f r
x :& Rec f rs
xs) = f r -> g r
forall (x :: u). f x -> g x
η f r
x g r -> Rec g rs -> Rec g (r : rs)
forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
:& (forall (x :: u). f x -> g x
η (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` Rec f rs
xs)
{-# INLINE rmap #-}

-- | A shorthand for 'rmap'.
(<<$>>)
  :: (forall x. f x -> g x)
  -> Rec f rs
  -> Rec g rs
<<$>> :: (forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
(<<$>>) = (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 <<&>> :: Rec f rs -> (forall (x :: u). f x -> g x) -> Rec g rs
<<&>> forall (x :: u). f x -> g x
f = (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 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 :: Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs
rapply Rec (Lift (->) f g) rs
RNil Rec f rs
RNil = Rec g rs
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) = Lift (->) f g r -> f r -> g r
forall l l' (op :: l -> l' -> *) k (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 g r -> Rec g rs -> Rec g (r : rs)
forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
:& (Rec (Lift (->) f g) rs
fs 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` Rec f rs
Rec f rs
xs)
{-# INLINE rapply #-}

-- | A shorthand for 'rapply'.
(<<*>>)
  :: Rec (Lift (->) f g) rs
  -> Rec f rs
  -> Rec g rs
<<*>> :: Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs
(<<*>>) = 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 (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      = Rec g '[] -> h (Rec g '[])
forall (f :: * -> *) a. Applicative f => a -> f a
pure Rec g '[]
forall u (f :: u -> *). Rec f '[]
RNil
rtraverse forall (x :: u). f x -> h (g x)
f (f r
x :& Rec f rs
xs) = g r -> Rec g rs -> Rec g (r : rs)
forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
(:&) (g r -> Rec g rs -> Rec g (r : rs))
-> h (g r) -> h (Rec g rs -> Rec g (r : rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f r -> h (g r)
forall (x :: u). f x -> h (g x)
f f r
x h (Rec g rs -> Rec g (r : rs))
-> h (Rec g rs) -> h (Rec g (r : rs))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall (x :: u). f x -> h (g x)) -> Rec f rs -> h (Rec g rs)
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 (x :: u). f x -> g x -> h x)
-> forall (xs :: [u]). Rec f xs -> Rec g xs -> Rec h xs
rzipWith forall (x :: u). 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        -> Rec h xs
forall u (f :: u -> *). Rec f '[]
RNil
  (f r
fa :& Rec f rs
fas) -> \(g r
ga :& Rec g rs
gas) -> f r -> g r -> h r
forall (x :: u). f x -> g x -> h x
m f r
fa g r
g r
ga h r -> Rec h rs -> Rec h (r : rs)
forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
:& (forall (x :: u). f x -> g x -> h x)
-> Rec f rs -> Rec g rs -> Rec h rs
forall u (f :: u -> *) (g :: u -> *) (h :: u -> *).
(forall (x :: u). f x -> g x -> h x)
-> forall (xs :: [u]). Rec f xs -> Rec g xs -> Rec h xs
rzipWith forall (x :: u). f x -> g x -> h x
m Rec f rs
fas Rec g rs
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 (x :: u). f x -> m) -> Rec f rs -> m
rfoldMap forall (x :: u). f x -> m
f = m -> Rec f rs -> m
forall (ss :: [u]). m -> Rec f ss -> m
go m
forall a. Monoid a => a
mempty
  where
  go :: forall ss. m -> Rec f ss -> m
  go :: 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 -> m -> Rec f rs -> m
forall (ss :: [u]). m -> Rec f ss -> m
go (m -> m -> m
forall a. Monoid a => a -> a -> a
mappend m
m (f r -> 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 :: Rec (Const a) rs -> [a]
recordToList Rec (Const a) rs
RNil = []
recordToList (Const a r
x :& Rec (Const a) rs
xs) = Const a r -> a
forall a k (b :: k). Const a b -> a
getConst Const a r
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: Rec (Const a) rs -> [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 :: 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 -> Rec (Dict c :. f) rs
forall u (f :: u -> *). Rec f '[]
RNil
    (f r
x :& Rec f rs
xs) -> Dict c (f r) -> Compose (Dict c) f r
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
Compose (f r -> Dict c (f r)
forall (c :: * -> Constraint) a. c a => a -> Dict c a
Dict f r
x) Compose (Dict c) f r
-> Rec (Dict c :. f) rs -> Rec (Dict c :. f) (r : rs)
forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
:& proxy c -> Rec f rs -> Rec (Dict c :. f) 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 :: proxy c -> (forall (a :: u). c a => f a) -> Rec f ts
rpureConstrained proxy c
_ forall (a :: u). c a => f a
f = Rec Proxy ts -> Rec f ts
forall (ts' :: [u]).
AllConstrained c ts' =>
Rec Proxy ts' -> Rec f ts'
go ((forall (x :: u). Proxy x) -> Rec Proxy ts
forall u (rs :: [u]) (f :: u -> *).
RecApplicative rs =>
(forall (x :: u). f x) -> Rec f rs
rpure forall (x :: u). Proxy x
forall k (t :: k). Proxy t
Proxy)
  where go :: AllConstrained c ts' => Rec Proxy ts' -> Rec f ts'
        go :: Rec Proxy ts' -> Rec f ts'
go Rec Proxy ts'
RNil = Rec f ts'
forall u (f :: u -> *). Rec f '[]
RNil
        go (Proxy r
_ :& Rec Proxy rs
xs) = f r
forall (a :: u). c a => f a
f f r -> Rec f rs -> Rec f (r : rs)
forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
:& Rec Proxy rs -> Rec f 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 :: proxy cs -> (forall a. AllSatisfied cs a => f a) -> Rec f ts
rpureConstraints proxy cs
_ forall a. AllSatisfied cs a => f a
f = Rec Maybe ts -> Rec f ts
forall (ts' :: [*]). AllAllSat cs ts' => Rec Maybe ts' -> Rec f ts'
go ((forall x. Maybe x) -> Rec Maybe ts
forall u (rs :: [u]) (f :: u -> *).
RecApplicative rs =>
(forall (x :: u). f x) -> Rec f rs
rpure forall x. Maybe x
Nothing)
  where go :: AllAllSat cs ts' => Rec Maybe ts' -> Rec f ts'
        go :: Rec Maybe ts' -> Rec f ts'
go Rec Maybe ts'
RNil = Rec f ts'
forall u (f :: u -> *). Rec f '[]
RNil
        go (Maybe r
_ :& Rec Maybe rs
xs) = f r
forall a. AllSatisfied cs a => f a
f f r -> Rec f rs -> Rec f (r : rs)
forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
:& Rec Maybe rs -> Rec f rs
forall (ts' :: [*]). AllAllSat cs ts' => Rec Maybe ts' -> Rec f ts'
go Rec Maybe rs
xs