{-# LANGUAGE UndecidableInstances #-} -- argh, for ReifyNames
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Composite.Record
  ( Rec((:&), RNil), Record
  , pattern (:*:), pattern (:^:), pattern (:!:)
  , (:->)(Val, getVal), _Val, val, valName, valWithName
  , RElem, rlens, rlens', rlensCo, rlensContra
  , AllHave, HasInstances, ValuesAllHave
  , zipRecsWith, reifyDicts, reifyVal, recordToNonEmpty
  , ReifyNames(reifyNames)
  , RecWithContext(rmapWithContext)
  , RDelete, RDeletable, rdelete
  ) where

import Control.DeepSeq(NFData(rnf))
import Control.Lens (Iso, iso)
import Control.Lens.TH (makeWrapped)
import Data.Functor.Identity (Identity(Identity))
import Data.Functor.Contravariant (Contravariant(contramap))
import Data.Kind (Constraint, Type)
import Data.List.NonEmpty (NonEmpty((:|)))
import Data.Proxy (Proxy(Proxy))
import Data.String (IsString)
import Data.Text (Text, pack)
import Data.Vinyl (Rec((:&), RNil), RecApplicative, rcast, recordToList, rpure)
import qualified Data.Vinyl as Vinyl
import Data.Vinyl.Functor (Compose(Compose), Const(Const), (:.))
import Data.Vinyl.Lens (type (∈), type (⊆))
import qualified Data.Vinyl.TypeLevel as Vinyl
import Data.Vinyl.XRec(IsoHKD(HKD, toHKD, unHKD))
import Foreign.Storable (Storable)
import GHC.TypeLits (KnownSymbol, Symbol, symbolVal)

-- FIXME this file is a big bin of random stuff, and should be at least organized if not split up.

-- |The type of regular plain records where each field has a value, equal to @'Rec' 'Identity'@.
type Record = Rec Identity

-- |Constraint expressing that @r@ is in @rs@ and providing the index of @r@ in @rs@. Equal to @'Vinyl.RElem' rs ('Vinyl.RIndex' r rs)@.
type RElem r rs = Vinyl.RElem r rs (Vinyl.RIndex r rs)

-- |Some value of type @a@ tagged with a symbol indicating its field name or label. Used as the usual type of elements in a 'Rec' or 'Record'.
--
-- Recommended pronunciation: record val.
newtype (:->) (s :: Symbol) a = Val { (s :-> a) -> a
getVal :: a }

_Val :: Iso (s :-> a) (s :-> b) a b
_Val :: p a (f b) -> p (s :-> a) (f (s :-> b))
_Val = ((s :-> a) -> a) -> (b -> s :-> b) -> Iso (s :-> a) (s :-> b) a b
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso (s :-> a) -> a
forall (s :: Symbol) a. (s :-> a) -> a
getVal b -> s :-> b
forall (s :: Symbol) a. a -> s :-> a
Val

makeWrapped ''(:->)

deriving instance Bounded    a => Bounded    (s :-> a)
deriving instance Enum       a => Enum       (s :-> a)
deriving instance Eq         a => Eq         (s :-> a)
deriving instance Floating   a => Floating   (s :-> a)
deriving instance Fractional a => Fractional (s :-> a)
deriving instance Integral   a => Integral   (s :-> a)
deriving instance IsString   a => IsString   (s :-> a)
deriving instance Monoid     a => Monoid     (s :-> a)
deriving instance Num        a => Num        (s :-> a)
deriving instance Ord        a => Ord        (s :-> a)
deriving instance Real       a => Real       (s :-> a)
deriving instance RealFloat  a => RealFloat  (s :-> a)
deriving instance RealFrac   a => RealFrac   (s :-> a)
deriving instance Semigroup  a => Semigroup  (s :-> a)
deriving instance Storable   a => Storable   (s :-> a)

instance Functor ((:->) s) where
  fmap :: (a -> b) -> (s :-> a) -> s :-> b
fmap a -> b
f = b -> s :-> b
forall (s :: Symbol) a. a -> s :-> a
Val (b -> s :-> b) -> ((s :-> a) -> b) -> (s :-> a) -> s :-> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f (a -> b) -> ((s :-> a) -> a) -> (s :-> a) -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (s :-> a) -> a
forall (s :: Symbol) a. (s :-> a) -> a
getVal
  {-# INLINE fmap #-}
instance Applicative ((:->) s) where
  pure :: a -> s :-> a
pure = a -> s :-> a
forall (s :: Symbol) a. a -> s :-> a
Val
  {-# INLINE pure #-}
  Val a -> b
f <*> :: (s :-> (a -> b)) -> (s :-> a) -> s :-> b
<*> Val a
a = b -> s :-> b
forall (s :: Symbol) a. a -> s :-> a
Val (a -> b
f a
a)
  {-# INLINE (<*>) #-}
instance Foldable ((:->) s) where
  foldr :: (a -> b -> b) -> b -> (s :-> a) -> b
foldr a -> b -> b
f b
z (Val a
a) = a -> b -> b
f a
a b
z
  {-# INLINE foldr #-}
instance Traversable ((:->) s) where
  traverse :: (a -> f b) -> (s :-> a) -> f (s :-> b)
traverse a -> f b
k (Val a
a) = b -> s :-> b
forall (s :: Symbol) a. a -> s :-> a
Val (b -> s :-> b) -> f b -> f (s :-> b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
k a
a
  {-# INLINE traverse #-}
instance Monad ((:->) s) where
  return :: a -> s :-> a
return = a -> s :-> a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  {-# INLINE return #-}
  Val a
a >>= :: (s :-> a) -> (a -> s :-> b) -> s :-> b
>>= a -> s :-> b
k = a -> s :-> b
k a
a
  {-# INLINE (>>=) #-}

instance NFData a => NFData (s :-> a) where
  rnf :: (s :-> a) -> ()
rnf (Val a
x) = a -> ()
forall a. NFData a => a -> ()
rnf a
x

instance NFData (Record '[]) where
  rnf :: Record '[] -> ()
rnf Record '[]
RNil = ()

instance (NFData x, NFData (Record xs)) => NFData (Record (x : xs)) where
  rnf :: Record (x : xs) -> ()
rnf (Identity r
x :& Rec Identity rs
xs) = Identity r -> ()
forall a. NFData a => a -> ()
rnf Identity r
x () -> () -> ()
`seq` Rec Identity rs -> ()
forall a. NFData a => a -> ()
rnf Rec Identity rs
xs

instance forall (s :: Symbol) a. (KnownSymbol s, Show a) => Show (s :-> a) where
  showsPrec :: Int -> (s :-> a) -> ShowS
showsPrec Int
p (Val a
a) = ((Proxy s -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (Proxy s
forall k (t :: k). Proxy t
Proxy :: Proxy s) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" :-> ") String -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p a
a

instance KnownSymbol s => IsoHKD Identity (s :-> a) where
  type HKD Identity (s :-> a) = a
  unHKD :: HKD Identity (s :-> a) -> Identity (s :-> a)
unHKD = (s :-> a) -> Identity (s :-> a)
forall a. a -> Identity a
Identity ((s :-> a) -> Identity (s :-> a))
-> (a -> s :-> a) -> a -> Identity (s :-> a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> s :-> a
forall (s :: Symbol) a. a -> s :-> a
Val
  toHKD :: Identity (s :-> a) -> HKD Identity (s :-> a)
toHKD (Identity (Val a
x)) = a
HKD Identity (s :-> a)
x

-- |Convenience function to make an @'Identity' (s ':->' a)@ with a particular symbol, used for named field construction.
--
-- For example:
--
-- @
--   type FFoo = "foo" :-> Int
--   type FBar = "bar" :-> String
--   type FBaz = "baz" :-> Double
--   type MyRecord = [FFoo, FBar, FBaz]
--
--   myRecord1 :: Record MyRecord
--   myRecord1
--     =  val \@"foo" 123
--     :& val \@"bar" "foobar"
--     :& val \@"baz" 3.21
--     :& RNil
--
--   myRecord2 :: Record MyRecord
--   myRecord2 = rcast
--     $  val \@"baz" 3.21
--     :& val \@"foo" 123
--     :& val \@"bar" "foobar"
--     :& RNil
-- @
--
-- In this example, both @myRecord1@ and @myRecord2@ have the same value, since 'Data.Vinyl.Lens.rcast' can reorder records.
val :: forall (s :: Symbol) a. a -> Identity (s :-> a)
val :: a -> Identity (s :-> a)
val = (s :-> a) -> Identity (s :-> a)
forall a. a -> Identity a
Identity ((s :-> a) -> Identity (s :-> a))
-> (a -> s :-> a) -> a -> Identity (s :-> a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> s :-> a
forall (s :: Symbol) a. a -> s :-> a
Val @s

-- |Reflect the type level name of a named value @s :-> a@ to a @Text@. For example, given @"foo" :-> Int@, yields @"foo" :: Text@
valName :: forall s a. KnownSymbol s => s :-> a -> Text
valName :: (s :-> a) -> Text
valName s :-> a
_ = String -> Text
pack (Proxy s -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (Proxy s
forall k (t :: k). Proxy t
Proxy :: Proxy s))
{-# INLINE valName #-}

-- |Extract the value and reflect the name of a named value.
valWithName :: forall s a. KnownSymbol s => s :-> a -> (Text, a)
valWithName :: (s :-> a) -> (Text, a)
valWithName s :-> a
v = ((s :-> a) -> Text
forall (s :: Symbol) a. KnownSymbol s => (s :-> a) -> Text
valName s :-> a
v, (s :-> a) -> a
forall (s :: Symbol) a. (s :-> a) -> a
getVal s :-> a
v)
{-# INLINE valWithName #-}

-- |Bidirectional pattern matching the first field of a record using ':->' values and the 'Identity' functor.
--
-- This pattern is bidirectional meaning you can use it either as a pattern or a constructor, e.g.
--
-- @
--   let rec = 123 :*: Just "foo" :*: RNil
--       foo :*: bar :*: RNil = rec
-- @
--
-- Mnemonic: @*@ for products.
pattern (:*:) :: () => () => a -> Rec Identity rs -> Rec Identity (s :-> a ': rs)
pattern $b:*: :: a -> Rec Identity rs -> Rec Identity ((s :-> a) : rs)
$m:*: :: forall r a (rs :: [*]) (s :: Symbol).
Rec Identity ((s :-> a) : rs)
-> (a -> Rec Identity rs -> r) -> (Void# -> r) -> r
(:*:) a rs = Identity (Val a) :& rs
infixr 5 :*:

-- |Bidirectional pattern matching the first field of a record using ':->' values and any functor.
--
-- This pattern is bidirectional meaning you can use it either as a pattern or a constructor, e.g.
--
-- @
--   let rec = Just 123 :^: Just "foo" :^: RNil
--       Just foo :^: Just bar :^: RNil = rec
-- @
--
-- Mnemonic: @^@ for products (record) of products (functor).
pattern (:^:) :: Functor f => () => f a -> Rec f rs -> Rec f (s :-> a ': rs)
pattern $b:^: :: f a -> Rec f rs -> Rec f ((s :-> a) : rs)
$m:^: :: forall r (f :: * -> *) a (rs :: [*]) (s :: Symbol).
Functor f =>
Rec f ((s :-> a) : rs)
-> (f a -> Rec f rs -> r) -> (Void# -> r) -> r
(:^:) fa rs <- (fmap getVal -> fa) :& rs where
  (:^:) f a
fa Rec f rs
rs = (a -> s :-> a) -> f a -> f (s :-> a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> s :-> a
forall (s :: Symbol) a. a -> s :-> a
Val f a
fa f (s :-> a) -> Rec f rs -> Rec f ((s :-> a) : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec f rs
rs
infixr 5 :^:

pattern (:!:) :: Contravariant f => () => f a -> Rec f rs -> Rec f (s :-> a ': rs)
pattern $b:!: :: f a -> Rec f rs -> Rec f ((s :-> a) : rs)
$m:!: :: forall r (f :: * -> *) a (rs :: [*]) (s :: Symbol).
Contravariant f =>
Rec f ((s :-> a) : rs)
-> (f a -> Rec f rs -> r) -> (Void# -> r) -> r
(:!:) fa rs <- (contramap Val -> fa) :& rs where
  (:!:) f a
fa Rec f rs
rs = ((s :-> a) -> a) -> f a -> f (s :-> a)
forall (f :: * -> *) a b. Contravariant f => (a -> b) -> f b -> f a
contramap (s :-> a) -> a
forall (s :: Symbol) a. (s :-> a) -> a
getVal f a
fa f (s :-> a) -> Rec f rs -> Rec f ((s :-> a) : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec f rs
rs
infixr 5 :!:

-- |Reify the type of a val.
reifyVal :: proxy (s :-> a) -> (s :-> a) -> (s :-> a)
reifyVal :: proxy (s :-> a) -> (s :-> a) -> s :-> a
reifyVal proxy (s :-> a)
_ = (s :-> a) -> s :-> a
forall a. a -> a
id

-- |Lens to a particular field of a record using the 'Identity' functor.
--
-- For example, given:
--
-- @
--   type FFoo = "foo" :-> Int
--   type FBar = "bar" :-> String
--   fBar_ :: Proxy FBar
--   fBar_ = Proxy
--
--   rec :: 'Rec' 'Identity' '[FFoo, FBar]
--   rec = 123 :*: "hello!" :*: Nil
-- @
--
-- Then:
--
-- @
--   view (rlens fBar_)               rec == "hello!"
--   set  (rlens fBar_) "goodbye!"    rec == 123 :*: "goodbye!" :*: Nil
--   over (rlens fBar_) (map toUpper) rec == 123 :*: "HELLO!"   :*: Nil
-- @
rlens :: (Functor g, RElem (s :-> a) rs, Functor g) => proxy (s :-> a) -> (a -> g a) -> Rec Identity rs -> g (Rec Identity rs)
rlens :: proxy (s :-> a)
-> (a -> g a) -> Rec Identity rs -> g (Rec Identity rs)
rlens proxy (s :-> a)
proxy a -> g a
f =
  (Identity (s :-> a) -> g (Identity (s :-> a)))
-> Rec Identity rs -> g (Rec Identity rs)
forall k (r :: k) (record :: (k -> *) -> [k] -> *) (rs :: [k])
       (f :: k -> *) (g :: * -> *).
(RecElem record r r rs rs (RIndex r rs), RecElemFCtx record f,
 Functor g) =>
(f r -> g (f r)) -> record f rs -> g (record f rs)
Vinyl.rlens ((Identity (s :-> a) -> g (Identity (s :-> a)))
 -> Rec Identity rs -> g (Rec Identity rs))
-> (Identity (s :-> a) -> g (Identity (s :-> a)))
-> Rec Identity rs
-> g (Rec Identity rs)
forall a b. (a -> b) -> a -> b
$ \ (Identity ((s :-> a) -> a
forall (s :: Symbol) a. (s :-> a) -> a
getVal ((s :-> a) -> a) -> ((s :-> a) -> s :-> a) -> (s :-> a) -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. proxy (s :-> a) -> (s :-> a) -> s :-> a
forall (proxy :: * -> *) (s :: Symbol) a.
proxy (s :-> a) -> (s :-> a) -> s :-> a
reifyVal proxy (s :-> a)
proxy -> a
a)) ->
    (s :-> a) -> Identity (s :-> a)
forall a. a -> Identity a
Identity ((s :-> a) -> Identity (s :-> a))
-> (a -> s :-> a) -> a -> Identity (s :-> a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> s :-> a
forall (s :: Symbol) a. a -> s :-> a
Val (a -> Identity (s :-> a)) -> g a -> g (Identity (s :-> a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> g a
f a
a
{-# INLINE rlens #-}

-- |Lens to a particular field of a record using any functor.
--
-- For example, given:
--
-- @
--   type FFoo = "foo" :-> Int
--   type FBar = "bar" :-> String
--   fBar_ :: Proxy FBar
--   fBar_ = Proxy
--
--   rec :: 'Rec' 'Maybe' '[FFoo, FBar]
--   rec = Just 123 :^: Just "hello!" :^: Nil
-- @
--
-- Then:
--
-- @
--   view (rlensCo fBar_)                      rec == Just "hello!"
--   set  (rlensCo fBar_) Nothing              rec == Just 123 :^: Nothing       :^: Nil
--   over (rlensCo fBar_) (fmap (map toUpper)) rec == Just 123 :^: Just "HELLO!" :^: Nil
-- @
rlensCo :: (Functor f, Functor g, RElem (s :-> a) rs) => proxy (s :-> a) -> (f a -> g (f a)) -> Rec f rs -> g (Rec f rs)
rlensCo :: proxy (s :-> a) -> (f a -> g (f a)) -> Rec f rs -> g (Rec f rs)
rlensCo proxy (s :-> a)
proxy f a -> g (f a)
f =
  (f (s :-> a) -> g (f (s :-> a))) -> Rec f rs -> g (Rec f rs)
forall k (r :: k) (record :: (k -> *) -> [k] -> *) (rs :: [k])
       (f :: k -> *) (g :: * -> *).
(RecElem record r r rs rs (RIndex r rs), RecElemFCtx record f,
 Functor g) =>
(f r -> g (f r)) -> record f rs -> g (record f rs)
Vinyl.rlens ((f (s :-> a) -> g (f (s :-> a))) -> Rec f rs -> g (Rec f rs))
-> (f (s :-> a) -> g (f (s :-> a))) -> Rec f rs -> g (Rec f rs)
forall a b. (a -> b) -> a -> b
$ \ (((s :-> a) -> a) -> f (s :-> a) -> f a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((s :-> a) -> a
forall (s :: Symbol) a. (s :-> a) -> a
getVal ((s :-> a) -> a) -> ((s :-> a) -> s :-> a) -> (s :-> a) -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. proxy (s :-> a) -> (s :-> a) -> s :-> a
forall (proxy :: * -> *) (s :: Symbol) a.
proxy (s :-> a) -> (s :-> a) -> s :-> a
reifyVal proxy (s :-> a)
proxy) -> f a
fa) ->
    (a -> s :-> a) -> f a -> f (s :-> a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> s :-> a
forall (s :: Symbol) a. a -> s :-> a
Val (f a -> f (s :-> a)) -> g (f a) -> g (f (s :-> a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a -> g (f a)
f f a
fa
{-# INLINE rlensCo #-}

-- |Synonym for `rlensCo`
rlens' :: (Functor f, Functor g, RElem (s :-> a) rs) => proxy (s :-> a) -> (f a -> g (f a)) -> Rec f rs -> g (Rec f rs)
rlens' :: proxy (s :-> a) -> (f a -> g (f a)) -> Rec f rs -> g (Rec f rs)
rlens' = proxy (s :-> a) -> (f a -> g (f a)) -> Rec f rs -> g (Rec f rs)
forall (f :: * -> *) (g :: * -> *) (s :: Symbol) a (rs :: [*])
       (proxy :: * -> *).
(Functor f, Functor g, RElem (s :-> a) rs) =>
proxy (s :-> a) -> (f a -> g (f a)) -> Rec f rs -> g (Rec f rs)
rlensCo
{-# INLINE rlens' #-}

-- |Lens to a particular field of a record using a contravariant functor.
--
-- For example, given:
--
-- @
--   type FFoo = "foo" :-> Int
--   type FBar = "bar" :-> String
--   fBar_ :: Proxy FBar
--   fBar_ = Proxy
--
--   rec :: 'Rec' 'Predicate' '[FFoo, FBar]
--   rec = Predicate even :!: Predicate (even . length) :!: Nil
-- @
--
-- Then:
--
-- @
--   view (rlensContra fBar_)                           rec == Predicate even
--   set  (rlensContra fBar_) Predicate (odd . length)  rec == Predicate even :!: Predicate (odd . length) :!: Nil
--   over (rlensContra fBar_) (contramap show)          rec == Predicate even :!: Predicate (odd . length . show) :!: Nil
-- @
rlensContra :: (Contravariant f, Functor g, RElem (s :-> a) rs) => proxy (s :-> a) -> (f a -> g (f a)) -> Rec f rs -> g (Rec f rs)
rlensContra :: proxy (s :-> a) -> (f a -> g (f a)) -> Rec f rs -> g (Rec f rs)
rlensContra proxy (s :-> a)
proxy f a -> g (f a)
f =
  (f (s :-> a) -> g (f (s :-> a))) -> Rec f rs -> g (Rec f rs)
forall k (r :: k) (record :: (k -> *) -> [k] -> *) (rs :: [k])
       (f :: k -> *) (g :: * -> *).
(RecElem record r r rs rs (RIndex r rs), RecElemFCtx record f,
 Functor g) =>
(f r -> g (f r)) -> record f rs -> g (record f rs)
Vinyl.rlens ((f (s :-> a) -> g (f (s :-> a))) -> Rec f rs -> g (Rec f rs))
-> (f (s :-> a) -> g (f (s :-> a))) -> Rec f rs -> g (Rec f rs)
forall a b. (a -> b) -> a -> b
$ \((a -> s :-> a) -> f (s :-> a) -> f a
forall (f :: * -> *) a b. Contravariant f => (a -> b) -> f b -> f a
contramap (proxy (s :-> a) -> (s :-> a) -> s :-> a
forall (proxy :: * -> *) (s :: Symbol) a.
proxy (s :-> a) -> (s :-> a) -> s :-> a
reifyVal proxy (s :-> a)
proxy ((s :-> a) -> s :-> a) -> (a -> s :-> a) -> a -> s :-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> s :-> a
forall (s :: Symbol) a. a -> s :-> a
Val) -> f a
fa) ->
    ((s :-> a) -> a) -> f a -> f (s :-> a)
forall (f :: * -> *) a b. Contravariant f => (a -> b) -> f b -> f a
contramap (s :-> a) -> a
forall (s :: Symbol) a. (s :-> a) -> a
getVal (f a -> f (s :-> a)) -> g (f a) -> g (f (s :-> a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a -> g (f a)
f f a
fa
{-# INLINE rlensContra #-}

-- | 'zipWith' for Rec's.
zipRecsWith :: (forall a. f a -> g a -> h a) -> Rec f as -> Rec g as -> Rec h as
zipRecsWith :: (forall (a :: u). f a -> g a -> h a)
-> Rec f as -> Rec g as -> Rec h as
zipRecsWith forall (a :: u). f a -> g a -> h a
_ Rec f as
RNil      Rec g as
_         = Rec h as
forall u (a :: u -> *). Rec a '[]
RNil
zipRecsWith forall (a :: u). f a -> g a -> h a
f (f r
r :& Rec f rs
rs) (g r
s :& Rec g rs
ss) = f r -> g r -> h r
forall (a :: u). f a -> g a -> h a
f f r
r g r
g r
s h r -> Rec h rs -> Rec h (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& (forall (a :: u). f a -> g a -> h a)
-> Rec f rs -> Rec g rs -> Rec h rs
forall u (f :: u -> *) (g :: u -> *) (h :: u -> *) (as :: [u]).
(forall (a :: u). f a -> g a -> h a)
-> Rec f as -> Rec g as -> Rec h as
zipRecsWith forall (a :: u). f a -> g a -> h a
f Rec f rs
rs Rec g rs
Rec g rs
ss

-- | Convert a provably nonempty @'Rec' ('Const' a) rs@ to a @'NonEmpty' a@.
recordToNonEmpty :: Vinyl.RecordToList rs => Rec (Const a) (r ': rs) -> NonEmpty a
recordToNonEmpty :: Rec (Const a) (r : rs) -> NonEmpty a
recordToNonEmpty (Const a
a :& Rec (Const a) rs
rs) = a
a a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| Rec (Const a) rs -> [a]
forall u (rs :: [u]) a. RecordToList rs => Rec (Const a) rs -> [a]
recordToList Rec (Const a) rs
rs

-- |Type function which produces a constraint on @a@ for each constraint in @cs@.
--
-- For example, @HasInstances Int '[Eq, Ord]@ is equivalent to @(Eq Int, Ord Int)@.
type family HasInstances (a :: u) (cs :: [u -> Constraint]) :: Constraint where
  HasInstances a '[] = ()
  HasInstances a (c ': cs) = (c a, HasInstances a cs)

-- |Type function which produces the cross product of constraints @cs@ and types @as@.
--
-- For example, @AllHave '[Eq, Ord] '[Int, Text]@ is equivalent to @(Eq Int, Ord Int, Eq Text, Ord Text)@
type family AllHave (cs :: [u -> Constraint]) (as :: [u]) :: Constraint where
  AllHave cs      '[]  = ()
  AllHave cs (a ': as) = (HasInstances a cs, AllHave cs as)

-- |Type function which produces the cross product of constraints @cs@ and the values carried in a record @rs@.
--
-- For example, @ValuesAllHave '[Eq, Ord] '["foo" :-> Int, "bar" :-> Text]@ is equivalent to @(Eq Int, Ord Int, Eq Text, Ord Text)@
type family ValuesAllHave (cs :: [u -> Constraint]) (as :: [u]) :: Constraint where
  ValuesAllHave cs            '[]  = ()
  ValuesAllHave cs (s :-> a ': as) = (HasInstances a cs, ValuesAllHave cs as)


-- |Given a list of constraints @cs@, apply some function for each @r@ in the target record type @rs@ with proof that those constraints hold for @r@,
-- generating a record with the result of each application.
reifyDicts
  :: forall u. forall (cs :: [u -> Constraint]) (f :: u -> Type) (rs :: [u]) (proxy :: [u -> Constraint] -> Type).
     (AllHave cs rs, RecApplicative rs)
  => proxy cs
  -> (forall proxy' (a :: u). HasInstances a cs => proxy' a -> f a)
  -> Rec f rs
reifyDicts :: proxy cs
-> (forall (proxy' :: u -> *) (a :: u).
    HasInstances a cs =>
    proxy' a -> f a)
-> Rec f rs
reifyDicts proxy cs
x forall (proxy' :: u -> *) (a :: u).
HasInstances a cs =>
proxy' a -> f a
f = proxy cs
-> Rec (Const ()) rs
-> (forall (proxy' :: u -> *) (a :: u).
    HasInstances a cs =>
    proxy' a -> f a)
-> Rec f rs
forall (f :: u -> *) (cs :: [u -> Constraint]) (rs' :: [u])
       (proxy :: [u -> Constraint] -> *).
AllHave cs rs' =>
proxy cs
-> Rec (Const ()) rs'
-> (forall (proxy' :: u -> *) (a :: u).
    HasInstances a cs =>
    proxy' a -> f a)
-> Rec f rs'
go proxy cs
x ((forall (x :: u). Const () x) -> Rec (Const ()) rs
forall u (rs :: [u]) (f :: u -> *).
RecApplicative rs =>
(forall (x :: u). f x) -> Rec f rs
rpure (() -> Const () x
forall k a (b :: k). a -> Const a b
Const ())) forall (proxy' :: u -> *) (a :: u).
HasInstances a cs =>
proxy' a -> f a
f
  where
    go :: forall (f :: u -> Type) (cs :: [u -> Constraint]) (rs' :: [u]) (proxy :: [u -> Constraint] -> Type). AllHave cs rs'
       => proxy cs
       -> Rec (Const ()) rs'
       -> (forall proxy' (a :: u). HasInstances a cs => proxy' a -> f a)
       -> Rec f rs'
    go :: proxy cs
-> Rec (Const ()) rs'
-> (forall (proxy' :: u -> *) (a :: u).
    HasInstances a cs =>
    proxy' a -> f a)
-> Rec f rs'
go proxy cs
_ Rec (Const ()) rs'
RNil forall (proxy' :: u -> *) (a :: u).
HasInstances a cs =>
proxy' a -> f a
_ = Rec f rs'
forall u (a :: u -> *). Rec a '[]
RNil
    go proxy cs
y ((Const () r
_ :: Const () a) :& Rec (Const ()) rs
ys) forall (proxy' :: u -> *) (a :: u).
HasInstances a cs =>
proxy' a -> f a
g = Proxy r -> f r
forall (proxy' :: u -> *) (a :: u).
HasInstances a cs =>
proxy' a -> f a
g (Proxy r
forall k (t :: k). Proxy t
Proxy @a) f r -> Rec f rs -> Rec f (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& proxy cs
-> Rec (Const ()) rs
-> (forall (proxy' :: u -> *) (a :: u).
    HasInstances a cs =>
    proxy' a -> f a)
-> Rec f rs
forall (f :: u -> *) (cs :: [u -> Constraint]) (rs' :: [u])
       (proxy :: [u -> Constraint] -> *).
AllHave cs rs' =>
proxy cs
-> Rec (Const ()) rs'
-> (forall (proxy' :: u -> *) (a :: u).
    HasInstances a cs =>
    proxy' a -> f a)
-> Rec f rs'
go proxy cs
y Rec (Const ()) rs
ys forall (proxy' :: u -> *) (a :: u).
HasInstances a cs =>
proxy' a -> f a
g
{-# INLINE reifyDicts #-}

-- |Class which reifies the symbols of a record composed of ':->' fields as 'Text'.
class ReifyNames (rs :: [Type]) where
  -- |Given a @'Rec' f rs@ where each @r@ in @rs@ is of the form @s ':->' a@, make a record which adds the 'Text' for each @s@.
  reifyNames :: Rec f rs -> Rec ((,) Text :. f) rs

instance ReifyNames '[] where
  reifyNames :: Rec f '[] -> Rec ((,) Text :. f) '[]
reifyNames Rec f '[]
_ = Rec ((,) Text :. f) '[]
forall u (a :: u -> *). Rec a '[]
RNil

instance forall (s :: Symbol) a (rs :: [Type]). (KnownSymbol s, ReifyNames rs) => ReifyNames (s :-> a ': rs) where
  reifyNames :: Rec f ((s :-> a) : rs) -> Rec ((,) Text :. f) ((s :-> a) : rs)
reifyNames (f r
fa :& Rec f rs
rs) = (Text, f r) -> Compose ((,) Text) f r
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
Compose ((,) (String -> Text
pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ Proxy s -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (Proxy s
forall k (t :: k). Proxy t
Proxy @s)) f r
fa) Compose ((,) Text) f r
-> Rec ((,) Text :. f) rs -> Rec ((,) Text :. f) (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec f rs -> Rec ((,) Text :. f) rs
forall (rs :: [*]) (f :: * -> *).
ReifyNames rs =>
Rec f rs -> Rec ((,) Text :. f) rs
reifyNames Rec f rs
rs

-- |Class with 'Data.Vinyl.rmap' but which gives the natural transformation evidence that the value its working over is contained within the overall record @ss@.
class RecWithContext (ss :: [Type]) (ts :: [Type]) where
  -- |Apply a natural transformation from @f@ to @g@ to each field of the given record, except that the natural transformation can be mildly unnatural by having
  -- evidence that @r@ is in @ss@.
  rmapWithContext :: proxy ss -> (forall r. r ∈ ss => f r -> g r) -> Rec f ts -> Rec g ts

instance RecWithContext ss '[] where
  rmapWithContext :: proxy ss
-> (forall r. (r ∈ ss) => f r -> g r) -> Rec f '[] -> Rec g '[]
rmapWithContext proxy ss
_ forall r. (r ∈ ss) => f r -> g r
_ Rec f '[]
_ = Rec g '[]
forall u (a :: u -> *). Rec a '[]
RNil

instance forall r (ss :: [Type]) (ts :: [Type]). (r ∈ ss, RecWithContext ss ts) => RecWithContext ss (r ': ts) where
  rmapWithContext :: proxy ss
-> (forall r. (r ∈ ss) => f r -> g r)
-> Rec f (r : ts)
-> Rec g (r : ts)
rmapWithContext proxy ss
proxy forall r. (r ∈ ss) => f r -> g r
n (f r
r :& Rec f rs
rs) = f r -> g r
forall r. (r ∈ ss) => f r -> g r
n f r
r g r -> Rec g rs -> Rec g (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& proxy ss
-> (forall r. (r ∈ ss) => f r -> g r) -> Rec f rs -> Rec g rs
forall (ss :: [*]) (ts :: [*]) (proxy :: [*] -> *) (f :: * -> *)
       (g :: * -> *).
RecWithContext ss ts =>
proxy ss
-> (forall r. (r ∈ ss) => f r -> g r) -> Rec f ts -> Rec g ts
rmapWithContext proxy ss
proxy forall r. (r ∈ ss) => f r -> g r
n Rec f rs
rs

-- |Type function which removes the first element @r@ from a list @rs@, and doesn't expand if @r@ is not present in @rs@.
type family RDelete (r :: u) (rs :: [u]) where
  RDelete r (r ': rs) = rs
  RDelete r (s ': rs) = s ': RDelete r rs

-- |Constraint which reflects that an element @r@ can be removed from @rs@ using 'rdelete'.
type RDeletable r rs = (r ∈ rs, RDelete r rs ⊆ rs)

-- |Remove an element @r@ from a @'Rec' f rs@. Note this is just a type constrained 'rcast'.
rdelete :: RDeletable r rs => proxy r -> Rec f rs -> Rec f (RDelete r rs)
rdelete :: proxy r -> Rec f rs -> Rec f (RDelete r rs)
rdelete proxy r
_ = Rec f rs -> Rec f (RDelete r rs)
forall k1 k2 (rs :: [k1]) (ss :: [k1]) (f :: k2 -> *)
       (record :: (k2 -> *) -> [k1] -> *) (is :: [Nat]).
(RecSubset record rs ss is, RecSubsetFCtx record f) =>
record f ss -> record f rs
rcast