-- |Module containing the sum formulation companion to 'Composite.Record's product formulation. Values of type @'CoRec' f rs@ represent a single value
-- @f r@ for one of the @r@s in @rs@. Heavily based on the great work by Anthony Cowley in Frames.
{-# LANGUAGE UndecidableInstances #-} -- for FoldRec
module Composite.CoRecord where

import Prelude
import Composite.Record (AllHave, HasInstances, (:->)(getVal, Val), reifyDicts, reifyVal, val, zipRecsWith)
import Control.Lens (Prism', prism')
import Data.Functor.Contravariant (Contravariant(contramap))
import Data.Functor.Identity (Identity(Identity), runIdentity)
import Data.Kind (Constraint)
import Data.Maybe (fromMaybe)
import Data.Profunctor (dimap)
import Data.Proxy (Proxy(Proxy))
import Data.Vinyl.Core (Dict(Dict), Rec((:&), RNil), RMap, RecApplicative, RecordToList, ReifyConstraint, recordToList, reifyConstraint, rmap, rpure)
import Data.Vinyl.Functor (Compose(Compose, getCompose), Const(Const), (:.))
import Data.Vinyl.Lens (RElem, type (∈), type (⊆), rget, rput, rreplace)
import Data.Vinyl.TypeLevel (RecAll, RIndex)

-- FIXME? replace with int-index/union or at least lift ideas from there. This encoding is awkward to work with and not compositional.

-- |@CoRef f rs@ represents a single value of type @f r@ for some @r@ in @rs@.
data CoRec :: (u -> *) -> [u] -> * where
  -- |Witness that @r@ is an element of @rs@ using '∈' ('RElem' with 'RIndex') from Vinyl.
  CoVal :: r ∈ rs => !(f r) -> CoRec f rs

instance forall rs. (AllHave '[Show] rs, RecApplicative rs) => Show (CoRec Identity rs) where
  show :: CoRec Identity rs -> String
show (CoVal (Identity r
x)) = String
"(CoVal " String -> ShowS
forall a. [a] -> [a] -> [a]
++ r -> String
show' r
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
    where
      shower :: Rec (Op String) rs
      shower :: Rec (Op String) rs
shower = Proxy '[Show]
-> (forall (proxy' :: * -> *) a.
    HasInstances a '[Show] =>
    proxy' a -> Op String a)
-> Rec (Op String) rs
forall u (cs :: [u -> Constraint]) (f :: u -> *) (rs :: [u])
       (proxy :: [u -> Constraint] -> *).
(AllHave cs rs, RecApplicative rs) =>
proxy cs
-> (forall (proxy' :: u -> *) (a :: u).
    HasInstances a cs =>
    proxy' a -> f a)
-> Rec f rs
reifyDicts (Proxy '[Show]
forall k (t :: k). Proxy t
Proxy @'[Show]) (\ proxy' a
_ -> (a -> String) -> Op String a
forall b a. (a -> b) -> Op b a
Op a -> String
forall a. Show a => a -> String
show)
      show' :: r -> String
show' = Op String r -> r -> String
forall b a. Op b a -> a -> b
runOp (Rec (Op String) rs -> Op String r
forall k (r :: k) (rs :: [k]) (f :: k -> *)
       (record :: (k -> *) -> [k] -> *).
(RecElem record r r rs rs (RIndex r rs), RecElemFCtx record f) =>
record f rs -> f r
rget Rec (Op String) rs
shower)

instance forall rs. (RMap rs, RecAll Maybe rs Eq, RecApplicative rs, RecordToList rs, ReifyConstraint Eq Maybe rs) => Eq (CoRec Identity rs) where
  CoRec Identity rs
crA == :: CoRec Identity rs -> CoRec Identity rs -> Bool
== CoRec Identity rs
crB = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool)
-> (Rec (Const Bool) rs -> [Bool]) -> Rec (Const Bool) rs -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec (Const Bool) rs -> [Bool]
forall u (rs :: [u]) a. RecordToList rs => Rec (Const a) rs -> [a]
recordToList (Rec (Const Bool) rs -> Bool) -> Rec (Const Bool) rs -> Bool
forall a b. (a -> b) -> a -> b
$ (forall a. (:.) (Dict Eq) Maybe a -> Maybe a -> Const Bool a)
-> Rec (Dict Eq :. Maybe) rs -> Rec Maybe rs -> Rec (Const Bool) 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. (:.) (Dict Eq) Maybe a -> Maybe a -> Const Bool a
f (CoRec Identity rs -> Rec (Dict Eq :. Maybe) rs
toRec CoRec Identity rs
crA) (CoRec Identity rs -> Rec Maybe rs
forall (rs :: [*]).
(RMap rs, RecApplicative rs) =>
Field rs -> Rec Maybe rs
fieldToRec CoRec Identity rs
crB)
    where
      f :: forall a. (Dict Eq :. Maybe) a -> Maybe a -> Const Bool a
      f :: (:.) (Dict Eq) Maybe a -> Maybe a -> Const Bool a
f (Compose (Dict Maybe a
a)) Maybe a
b = Bool -> Const Bool a
forall k a (b :: k). a -> Const a b
Const (Bool -> Const Bool a) -> Bool -> Const Bool a
forall a b. (a -> b) -> a -> b
$ Maybe a
a Maybe a -> Maybe a -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe a
b
      toRec :: CoRec Identity rs -> Rec (Dict Eq :. Maybe) rs
toRec = Rec Maybe rs -> Rec (Dict Eq :. Maybe) rs
forall u (c :: * -> Constraint) (f :: u -> *) (rs :: [u]).
ReifyConstraint c f rs =>
Rec f rs -> Rec (Dict c :. f) rs
reifyConstraint (Rec Maybe rs -> Rec (Dict Eq :. Maybe) rs)
-> (CoRec Identity rs -> Rec Maybe rs)
-> CoRec Identity rs
-> Rec (Dict Eq :. Maybe) rs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoRec Identity rs -> Rec Maybe rs
forall (rs :: [*]).
(RMap rs, RecApplicative rs) =>
Field rs -> Rec Maybe rs
fieldToRec

-- |The common case of a 'CoRec' with @f ~ 'Identity'@, i.e. a regular value.
type Field = CoRec Identity

-- |Inject a value @f r@ into a @'CoRec' f rs@ given that @r@ is one of the valid @rs@.
--
-- Equivalent to 'CoVal' the constructor, but exists to parallel 'field'.
coRec :: r ∈ rs => f r -> CoRec f rs
coRec :: f r -> CoRec f rs
coRec = f r -> CoRec f rs
forall u (r :: u) (rs :: [u]) (f :: u -> *).
(r ∈ rs) =>
f r -> CoRec f rs
CoVal

-- |Produce a prism for the given alternative of a 'CoRec'.
coRecPrism :: (RecApplicative rs, r ∈ rs) => Prism' (CoRec f rs) (f r)
coRecPrism :: Prism' (CoRec f rs) (f r)
coRecPrism = (f r -> CoRec f rs)
-> (CoRec f rs -> Maybe (f r)) -> Prism' (CoRec f rs) (f r)
forall b s a. (b -> s) -> (s -> Maybe a) -> Prism s s a b
prism' f r -> CoRec f rs
forall u (r :: u) (rs :: [u]) (f :: u -> *).
(r ∈ rs) =>
f r -> CoRec f rs
CoVal (Compose Maybe f r -> Maybe (f r)
forall l (f :: l -> *) k (g :: k -> l) (x :: k).
Compose f g x -> f (g x)
getCompose (Compose Maybe f r -> Maybe (f r))
-> (CoRec f rs -> Compose Maybe f r) -> CoRec f rs -> Maybe (f r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec (Maybe :. f) rs -> Compose Maybe f r
forall k (r :: k) (rs :: [k]) (f :: k -> *)
       (record :: (k -> *) -> [k] -> *).
(RecElem record r r rs rs (RIndex r rs), RecElemFCtx record f) =>
record f rs -> f r
rget (Rec (Maybe :. f) rs -> Compose Maybe f r)
-> (CoRec f rs -> Rec (Maybe :. f) rs)
-> CoRec f rs
-> Compose Maybe f r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoRec f rs -> Rec (Maybe :. f) rs
forall u (rs :: [u]) (f :: u -> *).
RecApplicative rs =>
CoRec f rs -> Rec (Maybe :. f) rs
coRecToRec)

-- |Inject a value @r@ into a @'Field' rs@ given that @r@ is one of the valid @rs@.
--
-- Equivalent to @'CoVal' . 'Identity'@.
field :: r ∈ rs => r -> Field rs
field :: r -> Field rs
field = Identity r -> Field rs
forall u (r :: u) (rs :: [u]) (f :: u -> *).
(r ∈ rs) =>
f r -> CoRec f rs
CoVal (Identity r -> Field rs) -> (r -> Identity r) -> r -> Field rs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. r -> Identity r
forall a. a -> Identity a
Identity

-- |Inject a value @a@ into a @'Field' rs@ given that @s :-> a@ is one of the valid @rs@.
--
-- Equivalent to @'CoVal' . 'Identity' . 'Val'@.
fieldVal :: forall s a rs proxy. s :-> a ∈ rs => proxy (s :-> a) -> a -> Field rs
fieldVal :: proxy (s :-> a) -> a -> Field rs
fieldVal proxy (s :-> a)
_ = Identity (s :-> a) -> Field rs
forall u (r :: u) (rs :: [u]) (f :: u -> *).
(r ∈ rs) =>
f r -> CoRec f rs
CoVal (Identity (s :-> a) -> Field rs)
-> (a -> Identity (s :-> a)) -> a -> Field rs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Identity (s :-> a)
forall (s :: Symbol) a. a -> Identity (s :-> a)
val @s

-- |Produce a prism for the given alternative of a 'Field'.
fieldPrism :: (RecApplicative rs, r ∈ rs) => Prism' (Field rs) r
fieldPrism :: Prism' (Field rs) r
fieldPrism = p (Identity r) (f (Identity r)) -> p (Field rs) (f (Field rs))
forall u (rs :: [u]) (r :: u) (f :: u -> *).
(RecApplicative rs, r ∈ rs) =>
Prism' (CoRec f rs) (f r)
coRecPrism (p (Identity r) (f (Identity r)) -> p (Field rs) (f (Field rs)))
-> (p r (f r) -> p (Identity r) (f (Identity r)))
-> p r (f r)
-> p (Field rs) (f (Field rs))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Identity r -> r)
-> (f r -> f (Identity r))
-> p r (f r)
-> p (Identity r) (f (Identity r))
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap Identity r -> r
forall a. Identity a -> a
runIdentity ((r -> Identity r) -> f r -> f (Identity r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap r -> Identity r
forall a. a -> Identity a
Identity)

-- |Produce a prism for the given @:->@ alternative of a 'Field', given a proxy to identify which @s :-> a@ you meant.
fieldValPrism :: (RecApplicative rs, s :-> a ∈ rs) => proxy (s :-> a) -> Prism' (Field rs) a
fieldValPrism :: proxy (s :-> a) -> Prism' (Field rs) a
fieldValPrism proxy (s :-> a)
proxy = p (Identity (s :-> a)) (f (Identity (s :-> a)))
-> p (Field rs) (f (Field rs))
forall u (rs :: [u]) (r :: u) (f :: u -> *).
(RecApplicative rs, r ∈ rs) =>
Prism' (CoRec f rs) (f r)
coRecPrism (p (Identity (s :-> a)) (f (Identity (s :-> a)))
 -> p (Field rs) (f (Field rs)))
-> (p a (f a) -> p (Identity (s :-> a)) (f (Identity (s :-> a))))
-> p a (f a)
-> p (Field rs) (f (Field rs))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Identity (s :-> a) -> a)
-> (f a -> f (Identity (s :-> a)))
-> p a (f a)
-> p (Identity (s :-> a)) (f (Identity (s :-> a)))
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap ((s :-> a) -> a
forall (s :: Symbol) a. (s :-> a) -> a
getVal ((s :-> a) -> a)
-> (Identity (s :-> a) -> s :-> a) -> Identity (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 ((s :-> a) -> s :-> a)
-> (Identity (s :-> a) -> s :-> a) -> Identity (s :-> a) -> s :-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity (s :-> a) -> s :-> a
forall a. Identity a -> a
runIdentity) ((a -> Identity (s :-> a)) -> f a -> f (Identity (s :-> a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((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))

-- |Apply an extraction to whatever @f r@ is contained in the given 'CoRec'.
--
-- For example @foldCoVal getConst :: CoRec (Const a) rs -> a@.
foldCoVal :: (forall (r :: u). RElem r rs (RIndex r rs) => f r -> b) -> CoRec f rs -> b
foldCoVal :: (forall (r :: u). RElem r rs (RIndex r rs) => f r -> b)
-> CoRec f rs -> b
foldCoVal forall (r :: u). RElem r rs (RIndex r rs) => f r -> b
f (CoVal f r
x) = f r -> b
forall (r :: u). RElem r rs (RIndex r rs) => f r -> b
f f r
x
{-# INLINE foldCoVal #-}

-- |Map a @'CoRec' f@ to a @'CoRec' g@ using a natural transform from @f@ to @g@ (@forall x. f x -> g x@).
mapCoRec :: (forall x. f x -> g x) -> CoRec f rs -> CoRec g rs
mapCoRec :: (forall (x :: u). f x -> g x) -> CoRec f rs -> CoRec g rs
mapCoRec forall (x :: u). f x -> g x
f (CoVal f r
x) = g r -> CoRec g rs
forall u (r :: u) (rs :: [u]) (f :: u -> *).
(r ∈ rs) =>
f r -> CoRec f rs
CoVal (f r -> g r
forall (x :: u). f x -> g x
f f r
x)
{-# INLINE mapCoRec #-}

-- |Apply some kleisli on @h@ to the @f x@ contained in a @'CoRec' f@ and yank the @h@ outside. Like 'traverse' but for 'CoRec'.
traverseCoRec :: Functor h => (forall x. f x -> h (g x)) -> CoRec f rs -> h (CoRec g rs)
traverseCoRec :: (forall (x :: u). f x -> h (g x)) -> CoRec f rs -> h (CoRec g rs)
traverseCoRec forall (x :: u). f x -> h (g x)
f (CoVal f r
x) = g r -> CoRec g rs
forall u (r :: u) (rs :: [u]) (f :: u -> *).
(r ∈ rs) =>
f r -> CoRec f rs
CoVal (g r -> CoRec g rs) -> h (g r) -> h (CoRec g 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
{-# INLINE traverseCoRec #-}

-- |Project a @'CoRec' f@ into a @'Rec' ('Maybe' ':.' f)@ where only the single @r@ held by the 'CoRec' is 'Just' in the resulting record, and all other
-- fields are 'Nothing'.
coRecToRec :: RecApplicative rs => CoRec f rs -> Rec (Maybe :. f) rs
coRecToRec :: CoRec f rs -> Rec (Maybe :. f) rs
coRecToRec (CoVal f r
a) = Compose Maybe f r -> Rec (Maybe :. f) rs -> Rec (Maybe :. f) rs
forall k (r :: k) (rs :: [k]) (record :: (k -> *) -> [k] -> *)
       (f :: k -> *).
(RecElem record r r rs rs (RIndex r rs), RecElemFCtx record f) =>
f r -> record f rs -> record f rs
rput (Maybe (f r) -> Compose Maybe f r
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
Compose (f r -> Maybe (f r)
forall a. a -> Maybe a
Just f r
a)) ((forall (x :: u). Compose Maybe f x) -> Rec (Maybe :. f) rs
forall u (rs :: [u]) (f :: u -> *).
RecApplicative rs =>
(forall (x :: u). f x) -> Rec f rs
rpure (Maybe (f x) -> Compose Maybe f x
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
Compose Maybe (f x)
forall a. Maybe a
Nothing))
{-# INLINE coRecToRec #-}

-- |Project a 'Field' into a @'Rec' 'Maybe'@ where only the single @r@ held by the 'Field' is 'Just' in the resulting record, and all other
-- fields are 'Nothing'.
fieldToRec :: (RMap rs, RecApplicative rs) => Field rs -> Rec Maybe rs
fieldToRec :: Field rs -> Rec Maybe rs
fieldToRec = (forall x. (:.) Maybe Identity x -> Maybe x)
-> Rec (Maybe :. Identity) rs -> Rec Maybe rs
forall u (rs :: [u]) (f :: u -> *) (g :: u -> *).
RMap rs =>
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
rmap ((Identity x -> x) -> Maybe (Identity x) -> Maybe x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Identity x -> x
forall a. Identity a -> a
runIdentity (Maybe (Identity x) -> Maybe x)
-> (Compose Maybe Identity x -> Maybe (Identity x))
-> Compose Maybe Identity x
-> Maybe x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose Maybe Identity x -> Maybe (Identity x)
forall l (f :: l -> *) k (g :: k -> l) (x :: k).
Compose f g x -> f (g x)
getCompose) (Rec (Maybe :. Identity) rs -> Rec Maybe rs)
-> (Field rs -> Rec (Maybe :. Identity) rs)
-> Field rs
-> Rec Maybe rs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Field rs -> Rec (Maybe :. Identity) rs
forall u (rs :: [u]) (f :: u -> *).
RecApplicative rs =>
CoRec f rs -> Rec (Maybe :. f) rs
coRecToRec
{-# INLINE fieldToRec #-}

-- |Typeclass which allows folding ala 'foldMap' over a 'Rec', using a 'CoRec' as the accumulator.
class FoldRec ss ts where
  -- |Given some combining function, an initial value, and a record, visit each field of the record using the combining function to accumulate the
  -- initial value or previous accumulation with the field of the record.
  foldRec
    :: (CoRec f ss -> CoRec f ss -> CoRec f ss)
    -> CoRec f ss
    -> Rec f ts
    -> CoRec f ss

instance FoldRec ss '[] where
  foldRec :: (CoRec f ss -> CoRec f ss -> CoRec f ss)
-> CoRec f ss -> Rec f '[] -> CoRec f ss
foldRec CoRec f ss -> CoRec f ss -> CoRec f ss
_ CoRec f ss
z Rec f '[]
_ = CoRec f ss
z
  {-# INLINE foldRec #-}

instance (t ∈ ss, FoldRec ss ts) => FoldRec ss (t ': ts) where
  foldRec :: (CoRec f ss -> CoRec f ss -> CoRec f ss)
-> CoRec f ss -> Rec f (t : ts) -> CoRec f ss
foldRec CoRec f ss -> CoRec f ss -> CoRec f ss
f CoRec f ss
z (f r
x :& Rec f rs
xs) = (CoRec f ss -> CoRec f ss -> CoRec f ss)
-> CoRec f ss -> Rec f rs -> CoRec f ss
forall u (ss :: [u]) (ts :: [u]) (f :: u -> *).
FoldRec ss ts =>
(CoRec f ss -> CoRec f ss -> CoRec f ss)
-> CoRec f ss -> Rec f ts -> CoRec f ss
foldRec CoRec f ss -> CoRec f ss -> CoRec f ss
f (CoRec f ss
z CoRec f ss -> CoRec f ss -> CoRec f ss
`f` f r -> CoRec f ss
forall u (r :: u) (rs :: [u]) (f :: u -> *).
(r ∈ rs) =>
f r -> CoRec f rs
CoVal f r
x) Rec f rs
xs
  {-# INLINE foldRec #-}

-- |'foldRec' for records with at least one field that doesn't require an initial value.
foldRec1
  :: FoldRec (r ': rs) rs
  => (CoRec f (r ': rs) -> CoRec f (r ': rs) -> CoRec f (r ': rs))
  -> Rec f (r ': rs)
  -> CoRec f (r ': rs)
foldRec1 :: (CoRec f (r : rs) -> CoRec f (r : rs) -> CoRec f (r : rs))
-> Rec f (r : rs) -> CoRec f (r : rs)
foldRec1 CoRec f (r : rs) -> CoRec f (r : rs) -> CoRec f (r : rs)
f (f r
x :& Rec f rs
xs) = (CoRec f (r : rs) -> CoRec f (r : rs) -> CoRec f (r : rs))
-> CoRec f (r : rs) -> Rec f rs -> CoRec f (r : rs)
forall u (ss :: [u]) (ts :: [u]) (f :: u -> *).
FoldRec ss ts =>
(CoRec f ss -> CoRec f ss -> CoRec f ss)
-> CoRec f ss -> Rec f ts -> CoRec f ss
foldRec CoRec f (r : rs) -> CoRec f (r : rs) -> CoRec f (r : rs)
f (f r -> CoRec f (r : rs)
forall u (r :: u) (rs :: [u]) (f :: u -> *).
(r ∈ rs) =>
f r -> CoRec f rs
CoVal f r
x) Rec f rs
xs
{-# INLINE foldRec1 #-}

-- |Given a @'Rec' ('Maybe' ':.' f) rs@, yield a @Just coRec@ for the first field which is @Just@, or @Nothing@ if there are no @Just@ fields in the record.
firstCoRec :: FoldRec rs rs => Rec (Maybe :. f) rs -> Maybe (CoRec f rs)
firstCoRec :: Rec (Maybe :. f) rs -> Maybe (CoRec f rs)
firstCoRec Rec (Maybe :. f) rs
RNil       = Maybe (CoRec f rs)
forall a. Maybe a
Nothing
firstCoRec v :: Rec (Maybe :. f) rs
v@((:.) Maybe f r
x :& Rec (Maybe :. f) rs
_) = (forall (x :: u). Compose Maybe f x -> Maybe (f x))
-> CoRec (Maybe :. f) rs -> Maybe (CoRec f rs)
forall u (h :: * -> *) (f :: u -> *) (g :: u -> *) (rs :: [u]).
Functor h =>
(forall (x :: u). f x -> h (g x)) -> CoRec f rs -> h (CoRec g rs)
traverseCoRec forall (x :: u). Compose Maybe f x -> Maybe (f x)
forall l (f :: l -> *) k (g :: k -> l) (x :: k).
Compose f g x -> f (g x)
getCompose (CoRec (Maybe :. f) rs -> Maybe (CoRec f rs))
-> CoRec (Maybe :. f) rs -> Maybe (CoRec f rs)
forall a b. (a -> b) -> a -> b
$ (CoRec (Maybe :. f) rs
 -> CoRec (Maybe :. f) rs -> CoRec (Maybe :. f) rs)
-> CoRec (Maybe :. f) rs
-> Rec (Maybe :. f) rs
-> CoRec (Maybe :. f) rs
forall u (ss :: [u]) (ts :: [u]) (f :: u -> *).
FoldRec ss ts =>
(CoRec f ss -> CoRec f ss -> CoRec f ss)
-> CoRec f ss -> Rec f ts -> CoRec f ss
foldRec CoRec (Maybe :. f) rs
-> CoRec (Maybe :. f) rs -> CoRec (Maybe :. f) rs
forall u (g :: u -> *) (b :: [u]).
CoRec (Compose Maybe g) b
-> CoRec (Compose Maybe g) b -> CoRec (Compose Maybe g) b
f ((:.) Maybe f r -> CoRec (Maybe :. f) rs
forall u (r :: u) (rs :: [u]) (f :: u -> *).
(r ∈ rs) =>
f r -> CoRec f rs
CoVal (:.) Maybe f r
x) Rec (Maybe :. f) rs
v
  where
    f :: CoRec (Compose Maybe g) b
-> CoRec (Compose Maybe g) b -> CoRec (Compose Maybe g) b
f c :: CoRec (Compose Maybe g) b
c@(CoVal (Compose (Just _))) CoRec (Compose Maybe g) b
_ = CoRec (Compose Maybe g) b
c
    f CoRec (Compose Maybe g) b
_                            CoRec (Compose Maybe g) b
c = CoRec (Compose Maybe g) b
c
{-# INLINE firstCoRec #-}

-- |Given a @'Rec' 'Maybe' rs@, yield a @Just field@ for the first field which is @Just@, or @Nothing@ if there are no @Just@ fields in the record.
firstField :: (FoldRec rs rs, RMap rs) => Rec Maybe rs -> Maybe (Field rs)
firstField :: Rec Maybe rs -> Maybe (Field rs)
firstField = Rec (Maybe :. Identity) rs -> Maybe (Field rs)
forall u (rs :: [u]) (f :: u -> *).
FoldRec rs rs =>
Rec (Maybe :. f) rs -> Maybe (CoRec f rs)
firstCoRec (Rec (Maybe :. Identity) rs -> Maybe (Field rs))
-> (Rec Maybe rs -> Rec (Maybe :. Identity) rs)
-> Rec Maybe rs
-> Maybe (Field rs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall x. Maybe x -> (:.) Maybe Identity x)
-> Rec Maybe rs -> Rec (Maybe :. Identity) rs
forall u (rs :: [u]) (f :: u -> *) (g :: u -> *).
RMap rs =>
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
rmap (Maybe (Identity x) -> Compose Maybe Identity x
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
Compose (Maybe (Identity x) -> Compose Maybe Identity x)
-> (Maybe x -> Maybe (Identity x))
-> Maybe x
-> Compose Maybe Identity x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (x -> Identity x) -> Maybe x -> Maybe (Identity x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap x -> Identity x
forall a. a -> Identity a
Identity)
{-# INLINE firstField #-}

-- |Given a @'Rec' ('Maybe' ':.' f) rs@, yield a @Just coRec@ for the last field which is @Just@, or @Nothing@ if there are no @Just@ fields in the record.
lastCoRec :: FoldRec rs rs => Rec (Maybe :. f) rs -> Maybe (CoRec f rs)
lastCoRec :: Rec (Maybe :. f) rs -> Maybe (CoRec f rs)
lastCoRec Rec (Maybe :. f) rs
RNil       = Maybe (CoRec f rs)
forall a. Maybe a
Nothing
lastCoRec v :: Rec (Maybe :. f) rs
v@((:.) Maybe f r
x :& Rec (Maybe :. f) rs
_) = (forall (x :: u). Compose Maybe f x -> Maybe (f x))
-> CoRec (Maybe :. f) rs -> Maybe (CoRec f rs)
forall u (h :: * -> *) (f :: u -> *) (g :: u -> *) (rs :: [u]).
Functor h =>
(forall (x :: u). f x -> h (g x)) -> CoRec f rs -> h (CoRec g rs)
traverseCoRec forall (x :: u). Compose Maybe f x -> Maybe (f x)
forall l (f :: l -> *) k (g :: k -> l) (x :: k).
Compose f g x -> f (g x)
getCompose (CoRec (Maybe :. f) rs -> Maybe (CoRec f rs))
-> CoRec (Maybe :. f) rs -> Maybe (CoRec f rs)
forall a b. (a -> b) -> a -> b
$ (CoRec (Maybe :. f) rs
 -> CoRec (Maybe :. f) rs -> CoRec (Maybe :. f) rs)
-> CoRec (Maybe :. f) rs
-> Rec (Maybe :. f) rs
-> CoRec (Maybe :. f) rs
forall u (ss :: [u]) (ts :: [u]) (f :: u -> *).
FoldRec ss ts =>
(CoRec f ss -> CoRec f ss -> CoRec f ss)
-> CoRec f ss -> Rec f ts -> CoRec f ss
foldRec CoRec (Maybe :. f) rs
-> CoRec (Maybe :. f) rs -> CoRec (Maybe :. f) rs
forall u (g :: u -> *) (b :: [u]).
CoRec (Compose Maybe g) b
-> CoRec (Compose Maybe g) b -> CoRec (Compose Maybe g) b
f ((:.) Maybe f r -> CoRec (Maybe :. f) rs
forall u (r :: u) (rs :: [u]) (f :: u -> *).
(r ∈ rs) =>
f r -> CoRec f rs
CoVal (:.) Maybe f r
x) Rec (Maybe :. f) rs
v
  where
    f :: CoRec (Compose Maybe g) b
-> CoRec (Compose Maybe g) b -> CoRec (Compose Maybe g) b
f CoRec (Compose Maybe g) b
_ c :: CoRec (Compose Maybe g) b
c@(CoVal (Compose (Just _))) = CoRec (Compose Maybe g) b
c
    f CoRec (Compose Maybe g) b
c                            CoRec (Compose Maybe g) b
_ = CoRec (Compose Maybe g) b
c
{-# INLINE lastCoRec #-}

-- |Given a @'Rec' 'Maybe' rs@, yield a @Just field@ for the last field which is @Just@, or @Nothing@ if there are no @Just@ fields in the record.
lastField :: (RMap rs, FoldRec rs rs) => Rec Maybe rs -> Maybe (Field rs)
lastField :: Rec Maybe rs -> Maybe (Field rs)
lastField = Rec (Maybe :. Identity) rs -> Maybe (Field rs)
forall u (rs :: [u]) (f :: u -> *).
FoldRec rs rs =>
Rec (Maybe :. f) rs -> Maybe (CoRec f rs)
lastCoRec (Rec (Maybe :. Identity) rs -> Maybe (Field rs))
-> (Rec Maybe rs -> Rec (Maybe :. Identity) rs)
-> Rec Maybe rs
-> Maybe (Field rs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall x. Maybe x -> (:.) Maybe Identity x)
-> Rec Maybe rs -> Rec (Maybe :. Identity) rs
forall u (rs :: [u]) (f :: u -> *) (g :: u -> *).
RMap rs =>
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
rmap (Maybe (Identity x) -> Compose Maybe Identity x
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
Compose (Maybe (Identity x) -> Compose Maybe Identity x)
-> (Maybe x -> Maybe (Identity x))
-> Maybe x
-> Compose Maybe Identity x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (x -> Identity x) -> Maybe x -> Maybe (Identity x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap x -> Identity x
forall a. a -> Identity a
Identity)
{-# INLINE lastField #-}

-- |Helper newtype containing a function @a -> b@ but with the type parameters flipped so @Op b@ has a consistent codomain for a varying domain.
newtype Op b a = Op { Op b a -> a -> b
runOp :: a -> b }

-- |Given a list of constraints @cs@ required to apply some function, apply the function to whatever value @r@ (not @f r@) which the 'CoRec' contains.
onCoRec
  :: forall (cs :: [* -> Constraint]) (f :: * -> *) (rs :: [*]) (b :: *) (proxy :: [* -> Constraint] -> *).
     (AllHave cs rs, Functor f, RecApplicative rs)
  => proxy cs
  -> (forall (a :: *). HasInstances a cs => a -> b)
  -> CoRec f rs
  -> f b
onCoRec :: proxy cs
-> (forall a. HasInstances a cs => a -> b) -> CoRec f rs -> f b
onCoRec proxy cs
p forall a. HasInstances a cs => a -> b
f (CoVal f r
x) = r -> b
go (r -> b) -> f r -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f r
x
  where
    go :: r -> b
go = Op b r -> r -> b
forall b a. Op b a -> a -> b
runOp (Op b r -> r -> b) -> Op b r -> r -> b
forall a b. (a -> b) -> a -> b
$ Rec (Op b) rs -> Op b r
forall k (r :: k) (rs :: [k]) (f :: k -> *)
       (record :: (k -> *) -> [k] -> *).
(RecElem record r r rs rs (RIndex r rs), RecElemFCtx record f) =>
record f rs -> f r
rget (proxy cs
-> (forall (proxy' :: * -> *) a.
    HasInstances a cs =>
    proxy' a -> Op b a)
-> Rec (Op b) rs
forall u (cs :: [u -> Constraint]) (f :: u -> *) (rs :: [u])
       (proxy :: [u -> Constraint] -> *).
(AllHave cs rs, RecApplicative rs) =>
proxy cs
-> (forall (proxy' :: u -> *) (a :: u).
    HasInstances a cs =>
    proxy' a -> f a)
-> Rec f rs
reifyDicts proxy cs
p (\ proxy' a
_ -> (a -> b) -> Op b a
forall b a. (a -> b) -> Op b a
Op a -> b
forall a. HasInstances a cs => a -> b
f) :: Rec (Op b) rs)
{-# INLINE onCoRec #-}

-- |Given a list of constraints @cs@ required to apply some function, apply the function to whatever value @r@ which the 'Field' contains.
onField
  :: forall (cs :: [* -> Constraint]) (rs :: [*]) (b :: *) (proxy :: [* -> Constraint] -> *).
     (AllHave cs rs, RecApplicative rs)
  => proxy cs
  -> (forall (a :: *). HasInstances a cs => a -> b)
  -> Field rs
  -> b
onField :: proxy cs
-> (forall a. HasInstances a cs => a -> b) -> Field rs -> b
onField proxy cs
p forall a. HasInstances a cs => a -> b
f Field rs
x = Identity b -> b
forall a. Identity a -> a
runIdentity (proxy cs
-> (forall a. HasInstances a cs => a -> b)
-> Field rs
-> Identity b
forall (cs :: [* -> Constraint]) (f :: * -> *) (rs :: [*]) b
       (proxy :: [* -> Constraint] -> *).
(AllHave cs rs, Functor f, RecApplicative rs) =>
proxy cs
-> (forall a. HasInstances a cs => a -> b) -> CoRec f rs -> f b
onCoRec proxy cs
p forall a. HasInstances a cs => a -> b
f Field rs
x)
{-# INLINE onField #-}

-- |Given some target type @r@ that's a possible value of @'Field' rs@, yield @Just@ if that is indeed the value being stored by the 'Field', or @Nothing@ if
-- not.
asA :: (r ∈ rs, RMap rs, RecApplicative rs) => Field rs -> Maybe r
asA :: Field rs -> Maybe r
asA = Rec Maybe rs -> Maybe r
forall k (r :: k) (rs :: [k]) (f :: k -> *)
       (record :: (k -> *) -> [k] -> *).
(RecElem record r r rs rs (RIndex r rs), RecElemFCtx record f) =>
record f rs -> f r
rget (Rec Maybe rs -> Maybe r)
-> (Field rs -> Rec Maybe rs) -> Field rs -> Maybe r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Field rs -> Rec Maybe rs
forall (rs :: [*]).
(RMap rs, RecApplicative rs) =>
Field rs -> Rec Maybe rs
fieldToRec
{-# INLINE asA #-}

-- |An extractor function @f a -> b@ which can be passed to 'foldCoRec' to eliminate one possible alternative of a 'CoRec'.
newtype Case' f b a = Case' { Case' f b a -> f a -> b
unCase' :: f a -> b }

instance Functor f => Contravariant (Case' f b) where
  contramap :: (a -> b) -> Case' f b b -> Case' f b a
contramap a -> b
f (Case' f b -> b
r) = (f a -> b) -> Case' f b a
forall k (f :: k -> *) b (a :: k). (f a -> b) -> Case' f b a
Case' ((f a -> b) -> Case' f b a) -> (f a -> b) -> Case' f b a
forall a b. (a -> b) -> a -> b
$ \f a
x -> f b -> b
r ((a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f f a
x) 

-- |A record of @Case'@ eliminators for each @r@ in @rs@ representing the pieces of a total function from @'CoRec' f@ to @b@.
type Cases' f rs b = Rec (Case' f b) rs

-- |Fold a @'CoRec' f@ using @Cases'@ which eliminate each possible value held by the 'CoRec', yielding the @b@ produced by whichever case matches.
foldCoRec :: RecApplicative (r ': rs) => Cases' f (r ': rs) b -> CoRec f (r ': rs) -> b
foldCoRec :: Cases' f (r : rs) b -> CoRec f (r : rs) -> b
foldCoRec Cases' f (r : rs) b
hs = Cases' f (r : rs) b -> Rec (Maybe :. f) (r : rs) -> b
forall u (f :: u -> *) (rs :: [u]) b.
Cases' f rs b -> Rec (Maybe :. f) rs -> b
go Cases' f (r : rs) b
hs (Rec (Maybe :. f) (r : rs) -> b)
-> (CoRec f (r : rs) -> Rec (Maybe :. f) (r : rs))
-> CoRec f (r : rs)
-> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoRec f (r : rs) -> Rec (Maybe :. f) (r : rs)
forall u (rs :: [u]) (f :: u -> *).
RecApplicative rs =>
CoRec f rs -> Rec (Maybe :. f) rs
coRecToRec
  where
    go :: Cases' f rs b -> Rec (Maybe :. f) rs -> b
    go :: Cases' f rs b -> Rec (Maybe :. f) rs -> b
go (Case' f r -> b
f :&  Rec (Case' f b) rs
_) (Compose (Just f r
x) :& Rec (Maybe :. f) rs
_) = f r -> b
f f r
f r
x
    go (Case' f r -> b
_ :& Rec (Case' f b) rs
fs) (Compose Maybe (f r)
Nothing  :& Rec (Maybe :. f) rs
t) = Rec (Case' f b) rs -> Rec (Maybe :. f) rs -> b
forall u (f :: u -> *) (rs :: [u]) b.
Cases' f rs b -> Rec (Maybe :. f) rs -> b
go Rec (Case' f b) rs
fs Rec (Maybe :. f) rs
Rec (Maybe :. f) rs
t
    go Cases' f rs b
RNil            Rec (Maybe :. f) rs
RNil                    = String -> b
forall a. HasCallStack => String -> a
error String
"foldCoRec should be provably total, isn't"
    {-# INLINE go #-}
{-# INLINE foldCoRec #-}

-- |Fold a @'CoRec' f@ using @Cases'@ which eliminate each possible value held by the 'CoRec', yielding the @b@ produced by whichever case matches.
--
-- Equivalent to 'foldCoRec' but with its arguments flipped so it can be written @matchCoRec coRec $ cases@.
matchCoRec :: RecApplicative (r ': rs) => CoRec f (r ': rs) -> Cases' f (r ': rs) b -> b
matchCoRec :: CoRec f (r : rs) -> Cases' f (r : rs) b -> b
matchCoRec = (Cases' f (r : rs) b -> CoRec f (r : rs) -> b)
-> CoRec f (r : rs) -> Cases' f (r : rs) b -> b
forall a b c. (a -> b -> c) -> b -> a -> c
flip Cases' f (r : rs) b -> CoRec f (r : rs) -> b
forall a (r :: a) (rs :: [a]) (f :: a -> *) b.
RecApplicative (r : rs) =>
Cases' f (r : rs) b -> CoRec f (r : rs) -> b
foldCoRec
{-# INLINE matchCoRec #-}

newtype Case b a = Case { Case b a -> a -> b
unCase :: a -> b }

instance Contravariant (Case b) where
  contramap :: (a -> b) -> Case b b -> Case b a
contramap a -> b
f (Case b -> b
r) = (a -> b) -> Case b a
forall b a. (a -> b) -> Case b a
Case ((a -> b) -> Case b a) -> (a -> b) -> Case b a
forall a b. (a -> b) -> a -> b
$ b -> b
r (b -> b) -> (a -> b) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f

type Cases rs b = Rec (Case b) rs

-- |Fold a 'Field' using 'Cases' which eliminate each possible value held by the 'Field', yielding the @b@ produced by whichever case matches.
foldField :: (RMap rs, RecApplicative (r ': rs)) => Cases (r ': rs) b -> Field (r ': rs) -> b
foldField :: Cases (r : rs) b -> Field (r : rs) -> b
foldField Cases (r : rs) b
hs = Cases' Identity (r : rs) b -> Field (r : rs) -> b
forall a (r :: a) (rs :: [a]) (f :: a -> *) b.
RecApplicative (r : rs) =>
Cases' f (r : rs) b -> CoRec f (r : rs) -> b
foldCoRec ((forall x. Case b x -> Case' Identity b x)
-> Cases (r : rs) b -> Cases' Identity (r : rs) b
forall u (rs :: [u]) (f :: u -> *) (g :: u -> *).
RMap rs =>
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
rmap ((Identity x -> b) -> Case' Identity b x
forall k (f :: k -> *) b (a :: k). (f a -> b) -> Case' f b a
Case' ((Identity x -> b) -> Case' Identity b x)
-> (Case b x -> Identity x -> b) -> Case b x -> Case' Identity b x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((x -> b) -> (Identity x -> x) -> Identity x -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity x -> x
forall a. Identity a -> a
runIdentity) ((x -> b) -> Identity x -> b)
-> (Case b x -> x -> b) -> Case b x -> Identity x -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Case b x -> x -> b
forall b a. Case b a -> a -> b
unCase) Cases (r : rs) b
hs)
{-# INLINE foldField #-}

-- |Fold a 'Field' using 'Cases' which eliminate each possible value held by the 'Field', yielding the @b@ produced by whichever case matches.
--
-- Equivalent to 'foldCoRec' but with its arguments flipped so it can be written @matchCoRec coRec $ cases@.
matchField :: (RMap rs, RecApplicative (r ': rs)) => Field (r ': rs) -> Cases (r ': rs) b -> b
matchField :: Field (r : rs) -> Cases (r : rs) b -> b
matchField = (Cases (r : rs) b -> Field (r : rs) -> b)
-> Field (r : rs) -> Cases (r : rs) b -> b
forall a b c. (a -> b -> c) -> b -> a -> c
flip Cases (r : rs) b -> Field (r : rs) -> b
forall (rs :: [*]) r b.
(RMap rs, RecApplicative (r : rs)) =>
Cases (r : rs) b -> Field (r : rs) -> b
foldField
{-# INLINE matchField #-}

-- |Widen a @'CoRec' f rs@ to a @'CoRec' f ss@ given that @rs ⊆ ss@.
widenCoRec :: (FoldRec ss ss, RecApplicative rs, RecApplicative ss, rs ⊆ ss) => CoRec f rs -> CoRec f ss
widenCoRec :: CoRec f rs -> CoRec f ss
widenCoRec CoRec f rs
r =
  CoRec f ss -> Maybe (CoRec f ss) -> CoRec f ss
forall a. a -> Maybe a -> a
fromMaybe (String -> CoRec f ss
forall a. HasCallStack => String -> a
error String
"widenCoRec should be provably total, isn't") (Maybe (CoRec f ss) -> CoRec f ss)
-> Maybe (CoRec f ss) -> CoRec f ss
forall a b. (a -> b) -> a -> b
$
    Rec (Maybe :. f) ss -> Maybe (CoRec f ss)
forall u (rs :: [u]) (f :: u -> *).
FoldRec rs rs =>
Rec (Maybe :. f) rs -> Maybe (CoRec f rs)
firstCoRec (Rec (Maybe :. f) rs -> Rec (Maybe :. f) ss -> Rec (Maybe :. f) ss
forall k1 k2 (rs :: [k1]) (ss :: [k1]) (f :: k2 -> *)
       (record :: (k2 -> *) -> [k1] -> *) (is :: [Nat]).
(RecSubset record rs ss is, RecSubsetFCtx record f) =>
record f rs -> record f ss -> record f ss
rreplace (CoRec f rs -> Rec (Maybe :. f) rs
forall u (rs :: [u]) (f :: u -> *).
RecApplicative rs =>
CoRec f rs -> Rec (Maybe :. f) rs
coRecToRec CoRec f rs
r) ((forall (x :: u). (:.) Maybe f x) -> Rec (Maybe :. f) ss
forall u (rs :: [u]) (f :: u -> *).
RecApplicative rs =>
(forall (x :: u). f x) -> Rec f rs
rpure ((forall (x :: u). (:.) Maybe f x) -> Rec (Maybe :. f) ss)
-> (forall (x :: u). (:.) Maybe f x) -> Rec (Maybe :. f) ss
forall a b. (a -> b) -> a -> b
$ Maybe (f x) -> Compose Maybe f x
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
Compose Maybe (f x)
forall a. Maybe a
Nothing))

-- |Widen a @'Field' rs@ to a @'Field' ss@ given that @rs ⊆ ss@.
widenField :: (FoldRec ss ss, RMap rs, RMap ss, RecApplicative rs, RecApplicative ss, rs ⊆ ss) => Field rs -> Field ss
widenField :: Field rs -> Field ss
widenField Field rs
r =
  Field ss -> Maybe (Field ss) -> Field ss
forall a. a -> Maybe a -> a
fromMaybe (String -> Field ss
forall a. HasCallStack => String -> a
error String
"widenField should be provably total, isn't") (Maybe (Field ss) -> Field ss) -> Maybe (Field ss) -> Field ss
forall a b. (a -> b) -> a -> b
$
    Rec Maybe ss -> Maybe (Field ss)
forall (rs :: [*]).
(FoldRec rs rs, RMap rs) =>
Rec Maybe rs -> Maybe (Field rs)
firstField (Rec Maybe rs -> Rec Maybe ss -> Rec Maybe ss
forall k1 k2 (rs :: [k1]) (ss :: [k1]) (f :: k2 -> *)
       (record :: (k2 -> *) -> [k1] -> *) (is :: [Nat]).
(RecSubset record rs ss is, RecSubsetFCtx record f) =>
record f rs -> record f ss -> record f ss
rreplace (Field rs -> Rec Maybe rs
forall (rs :: [*]).
(RMap rs, RecApplicative rs) =>
Field rs -> Rec Maybe rs
fieldToRec Field rs
r) ((forall a. Maybe a) -> Rec Maybe ss
forall u (rs :: [u]) (f :: u -> *).
RecApplicative rs =>
(forall (x :: u). f x) -> Rec f rs
rpure forall a. Maybe a
Nothing))