{-# LANGUAGE AllowAmbiguousTypes, BangPatterns, CPP, ConstraintKinds,
             DataKinds, EmptyCase, FlexibleContexts,
             FlexibleInstances, GADTs, KindSignatures,
             MultiParamTypeClasses, PolyKinds, RankNTypes,
             ScopedTypeVariables, TypeApplications, TypeOperators,
             UndecidableInstances #-}
-- | Co-records: open sum types.
--
-- Consider a record with three fields @A@, @B@, and @C@. A record is
-- a product of its fields; that is, it contains all of them: @A@,
-- @B@, /and/ @C@. If we want to talk about a value whose type is one
-- of those three types, it is /any one/ of type @A@, @B@, /or/
-- @C@. The type @CoRec '[A,B,C]@ corresponds to this sum type.
module Data.Vinyl.CoRec where
import Data.Maybe(fromJust)
import Data.Vinyl.Core
import Data.Vinyl.Lens (RElem, rget, rput, type (∈))
import Data.Vinyl.Functor (Compose(..), (:.), Identity(..), Const(..))
import Data.Vinyl.TypeLevel
import Data.Vinyl.Derived (FieldType, (:::))
import GHC.TypeLits (Symbol, KnownSymbol)
import GHC.Types (type Type)

import Unsafe.Coerce (unsafeCoerce)

-- | Generalize algebraic sum types.
data CoRec :: (k -> *) -> [k] -> * where
  CoRec :: RElem a ts (RIndex a ts) => !(f a) -> CoRec f ts

-- | A 'CoRec' constructor with better inference. If you have a label
-- that should pick out a type from the list of types that index a
-- 'CoRec', this function will help you more so than the raw 'CoRec'
-- data constructor.
corec :: forall (l :: Symbol)
                (ts :: [(Symbol,Type)])
                (f :: (Symbol,Type) -> Type).
         (KnownSymbol l, (l ::: FieldType l ts)  ts)
      => f (l ::: FieldType l ts) -> CoRec f ts
corec :: forall (l :: Symbol) (ts :: [(Symbol, *)]) (f :: (Symbol, *) -> *).
(KnownSymbol l, (l ::: FieldType l ts) ∈ ts) =>
f (l ::: FieldType l ts) -> CoRec f ts
corec f (l ::: FieldType l ts)
x = forall {k} (r :: k) (ts :: [k]) (f :: k -> *).
RElem r ts (RIndex r ts) =>
f r -> CoRec f ts
CoRec f (l ::: FieldType l ts)
x

-- | Apply a function to a 'CoRec' value. The function must accept
-- /any/ variant.
foldCoRec :: (forall a. RElem a ts (RIndex a ts) => f a -> b) -> CoRec f ts -> b
foldCoRec :: forall {k} (ts :: [k]) (f :: k -> *) b.
(forall (a :: k). RElem a ts (RIndex a ts) => f a -> b)
-> CoRec f ts -> b
foldCoRec forall (a :: k). RElem a ts (RIndex a ts) => f a -> b
f (CoRec f a
x) = forall (a :: k). RElem a ts (RIndex a ts) => f a -> b
f f a
x

-- | A Field of a 'Rec' 'Identity' is a 'CoRec' 'Identity'.
type Field = CoRec Identity

-- | A function type constructor that takes its arguments in the
-- reverse order.
newtype Op b a = Op { forall b a. Op b a -> a -> b
runOp :: a -> b }

-- | Helper for writing a 'Show' instance for 'CoRec'. This lets us
-- ask for a 'Show' constraint on the type formed by applying a type
-- constructor to a type index.
class ShowF f a where
  showf :: f a -> String

instance Show (f a) => ShowF f a where
  showf :: f a -> String
showf = forall a. Show a => a -> String
show

instance forall f ts. RPureConstrained (ShowF f) ts => Show (CoRec f ts) where
  show :: CoRec f ts -> String
show CoRec f ts
x = String
"{|" forall a. [a] -> [a] -> [a]
++ forall {k} {k} (c :: k -> Constraint) (f :: k -> *) (ts :: [k])
       (b :: k) (g :: k -> *).
RPureConstrained c ts =>
(forall (a :: k). (a ∈ ts, c a) => f a -> g b) -> CoRec f ts -> g b
onCoRec @(ShowF f) forall {k} (f :: k -> *) (a :: k). ShowF f a => f a -> String
showf CoRec f ts
x forall a. [a] -> [a] -> [a]
++ String
"|}"

instance forall ts. (RecApplicative ts, RecordToList ts,
                     RApply ts, ReifyConstraint Eq Maybe ts, RMap ts)
  => Eq (CoRec Identity ts) where
  CoRec Identity ts
crA == :: CoRec Identity ts -> CoRec Identity ts -> Bool
== CoRec Identity ts
crB = forall (t :: * -> *). Foldable t => t Bool -> Bool
and forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {u} (rs :: [u]) a.
RecordToList rs =>
Rec (Const a) rs -> [a]
recordToList
             forall a b. (a -> b) -> a -> b
$ forall {u} (xs :: [u]) (f :: u -> *) (g :: u -> *) (h :: u -> *).
(RMap xs, RApply xs) =>
(forall (x :: u). f x -> g x -> h x)
-> Rec f xs -> Rec g xs -> Rec h xs
rzipWith forall a. (:.) (Dict Eq) Maybe a -> Maybe a -> Const Bool a
f (CoRec Identity ts -> Rec (Dict Eq :. Maybe) ts
toRec CoRec Identity ts
crA) (forall (ts :: [*]).
(RecApplicative ts, RMap ts) =>
CoRec Identity ts -> Rec Maybe ts
coRecToRec' CoRec Identity ts
crB)
    where
      f :: forall a. (Dict Eq :. Maybe) a -> Maybe a -> Const Bool a
      f :: forall a. (:.) (Dict Eq) Maybe a -> Maybe a -> Const Bool a
f (Compose (Dict Maybe a
a)) Maybe a
b = forall k a (b :: k). a -> Const a b
Const forall a b. (a -> b) -> a -> b
$ Maybe a
a forall a. Eq a => a -> a -> Bool
== Maybe a
b
      toRec :: CoRec Identity ts -> Rec (Dict Eq :. Maybe) ts
toRec = forall {u} (c :: * -> Constraint) (f :: u -> *) (rs :: [u]).
ReifyConstraint c f rs =>
Rec f rs -> Rec (Dict c :. f) rs
reifyConstraint @Eq forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (ts :: [*]).
(RecApplicative ts, RMap ts) =>
CoRec Identity ts -> Rec Maybe ts
coRecToRec'

-- | We can inject a a 'CoRec' into a 'Rec' where every field of the
-- 'Rec' is 'Nothing' except for the one whose type corresponds to the
-- type of the given 'CoRec' variant.
coRecToRec :: forall f ts. RecApplicative ts
           => CoRec f ts -> Rec (Maybe :. f) ts
coRecToRec :: forall {u} (f :: u -> *) (ts :: [u]).
RecApplicative ts =>
CoRec f ts -> Rec (Maybe :. f) ts
coRecToRec (CoRec f a
x) = 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 (forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
Compose (forall a. a -> Maybe a
Just f a
x)) (forall {u} (rs :: [u]) (f :: u -> *).
RecApplicative rs =>
(forall (x :: u). f x) -> Rec f rs
rpure (forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
Compose forall a. Maybe a
Nothing))

-- | Shorthand for applying 'coRecToRec' with common functors.
coRecToRec' :: (RecApplicative ts, RMap ts)
            => CoRec Identity ts -> Rec Maybe ts
coRecToRec' :: forall (ts :: [*]).
(RecApplicative ts, RMap ts) =>
CoRec Identity ts -> Rec Maybe ts
coRecToRec' = forall {u} (rs :: [u]) (f :: u -> *) (g :: u -> *).
RMap rs =>
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
rmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Identity a -> a
getIdentity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l k (f :: l -> *) (g :: k -> l) (x :: k).
Compose f g x -> f (g x)
getCompose) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {u} (f :: u -> *) (ts :: [u]).
RecApplicative ts =>
CoRec f ts -> Rec (Maybe :. f) ts
coRecToRec

-- | Fold a field selection function over a 'Rec'.
class FoldRec ss ts where
  foldRec :: (CoRec f ss -> CoRec f ss -> CoRec f ss)
          -> CoRec f ss
          -> Rec f ts
          -> CoRec f ss

instance FoldRec ss '[] where foldRec :: forall (f :: k -> *).
(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

instance (t  ss, FoldRec ss ts) => FoldRec ss (t ': ts) where
  foldRec :: forall (f :: a -> *).
(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) = forall {k} (ss :: [k]) (ts :: [k]) (f :: k -> *).
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 -> CoRec f ss -> CoRec f ss
f CoRec f ss
z (forall {k} (r :: k) (ts :: [k]) (f :: k -> *).
RElem r ts (RIndex r ts) =>
f r -> CoRec f ts
CoRec f r
x)) Rec f rs
xs

-- | Apply a natural transformation to a variant.
coRecMap :: (forall x. f x -> g x) -> CoRec f ts -> CoRec g ts
coRecMap :: forall {k} (f :: k -> *) (g :: k -> *) (ts :: [k]).
(forall (x :: k). f x -> g x) -> CoRec f ts -> CoRec g ts
coRecMap forall (x :: k). f x -> g x
nt (CoRec f a
x) = forall {k} (r :: k) (ts :: [k]) (f :: k -> *).
RElem r ts (RIndex r ts) =>
f r -> CoRec f ts
CoRec (forall (x :: k). f x -> g x
nt f a
x)

-- | Get a 'DictOnly' from an 'RPureConstrained' instance.
getDict :: forall c ts a proxy. (a  ts, RPureConstrained c ts)
        => proxy a -> DictOnly c a
getDict :: forall {k} (c :: k -> Constraint) (ts :: [k]) (a :: k)
       (proxy :: k -> *).
(a ∈ ts, RPureConstrained c ts) =>
proxy a -> DictOnly c a
getDict proxy a
_ = 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 @a (forall {k} (c :: k -> Constraint) (ts :: [k]) (f :: k -> *).
RPureConstrained c ts =>
(forall (a :: k). c a => f a) -> Rec f ts
rpureConstrained @c @ts forall {k} (c :: k -> Constraint) (a :: k). c a => DictOnly c a
DictOnly)

-- | Like 'coRecMap', but the function mapped over the 'CoRec' can
-- have a constraint.
coRecMapC :: forall c ts f g.
             (RPureConstrained c ts)
          => (forall x. (x  ts, c x) => f x -> g x)
          -> CoRec f ts
          -> CoRec g ts
coRecMapC :: forall {k} (c :: k -> Constraint) (ts :: [k]) (f :: k -> *)
       (g :: k -> *).
RPureConstrained c ts =>
(forall (x :: k). (x ∈ ts, c x) => f x -> g x)
-> CoRec f ts -> CoRec g ts
coRecMapC forall (x :: k). (x ∈ ts, c x) => f x -> g x
nt (CoRec f a
x) = case forall {k} (c :: k -> Constraint) (ts :: [k]) (a :: k)
       (proxy :: k -> *).
(a ∈ ts, RPureConstrained c ts) =>
proxy a -> DictOnly c a
getDict @c @ts f a
x of
                           DictOnly c a
DictOnly -> forall {k} (r :: k) (ts :: [k]) (f :: k -> *).
RElem r ts (RIndex r ts) =>
f r -> CoRec f ts
CoRec (forall (x :: k). (x ∈ ts, c x) => f x -> g x
nt f a
x)

-- | This can be used to pull effects out of a 'CoRec'.
coRecTraverse :: Functor h
              => (forall x. f x -> h (g x)) -> CoRec f ts -> h (CoRec g ts)
coRecTraverse :: forall {k} (h :: * -> *) (f :: k -> *) (g :: k -> *) (ts :: [k]).
Functor h =>
(forall (x :: k). f x -> h (g x)) -> CoRec f ts -> h (CoRec g ts)
coRecTraverse forall (x :: k). f x -> h (g x)
f (CoRec f a
x) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {k} (r :: k) (ts :: [k]) (f :: k -> *).
RElem r ts (RIndex r ts) =>
f r -> CoRec f ts
CoRec (forall (x :: k). f x -> h (g x)
f f a
x)

-- | Fold a field selection function over a non-empty 'Rec'.
foldRec1 :: FoldRec (t ': ts) ts
         => (CoRec f (t ': ts) -> CoRec f (t ': ts) -> CoRec f (t ': ts))
         -> Rec f (t ': ts)
         -> CoRec f (t ': ts)
foldRec1 :: forall {a} (t :: a) (ts :: [a]) (f :: a -> *).
FoldRec (t : ts) ts =>
(CoRec f (t : ts) -> CoRec f (t : ts) -> CoRec f (t : ts))
-> Rec f (t : ts) -> CoRec f (t : ts)
foldRec1 CoRec f (t : ts) -> CoRec f (t : ts) -> CoRec f (t : ts)
f (f r
x :& Rec f rs
xs) = forall {k} (ss :: [k]) (ts :: [k]) (f :: k -> *).
FoldRec ss ts =>
(CoRec f ss -> CoRec f ss -> CoRec f ss)
-> CoRec f ss -> Rec f ts -> CoRec f ss
foldRec CoRec f (t : ts) -> CoRec f (t : ts) -> CoRec f (t : ts)
f (forall {k} (r :: k) (ts :: [k]) (f :: k -> *).
RElem r ts (RIndex r ts) =>
f r -> CoRec f ts
CoRec f r
x) Rec f rs
xs

-- | Similar to 'Data.Monoid.First': find the first field that is not
-- 'Nothing'.
firstField :: FoldRec ts ts
           => Rec (Maybe :. f) ts -> Maybe (CoRec f ts)
firstField :: forall {k} (ts :: [k]) (f :: k -> *).
FoldRec ts ts =>
Rec (Maybe :. f) ts -> Maybe (CoRec f ts)
firstField Rec (Maybe :. f) ts
RNil = forall a. Maybe a
Nothing
firstField v :: Rec (Maybe :. f) ts
v@((:.) Maybe f r
x :& Rec (Maybe :. f) rs
_) = forall {k} (h :: * -> *) (f :: k -> *) (g :: k -> *) (ts :: [k]).
Functor h =>
(forall (x :: k). f x -> h (g x)) -> CoRec f ts -> h (CoRec g ts)
coRecTraverse forall l k (f :: l -> *) (g :: k -> l) (x :: k).
Compose f g x -> f (g x)
getCompose forall a b. (a -> b) -> a -> b
$ forall {k} (ss :: [k]) (ts :: [k]) (f :: k -> *).
FoldRec ss ts =>
(CoRec f ss -> CoRec f ss -> CoRec f ss)
-> CoRec f ss -> Rec f ts -> CoRec f ss
foldRec forall {a} (f :: a -> *) (t :: a) (ts :: [a]).
CoRec (Maybe :. f) (t : ts)
-> CoRec (Maybe :. f) (t : ts) -> CoRec (Maybe :. f) (t : ts)
aux (forall {k} (r :: k) (ts :: [k]) (f :: k -> *).
RElem r ts (RIndex r ts) =>
f r -> CoRec f ts
CoRec (:.) Maybe f r
x) Rec (Maybe :. f) ts
v
  where aux :: CoRec (Maybe :. f) (t ': ts)
            -> CoRec (Maybe :. f) (t ': ts)
            -> CoRec (Maybe :. f) (t ': ts)
        aux :: forall {a} (f :: a -> *) (t :: a) (ts :: [a]).
CoRec (Maybe :. f) (t : ts)
-> CoRec (Maybe :. f) (t : ts) -> CoRec (Maybe :. f) (t : ts)
aux c :: CoRec (Maybe :. f) (t : ts)
c@(CoRec (Compose (Just f a
_))) CoRec (Maybe :. f) (t : ts)
_ =  CoRec (Maybe :. f) (t : ts)
c
        aux CoRec (Maybe :. f) (t : ts)
_ CoRec (Maybe :. f) (t : ts)
c = CoRec (Maybe :. f) (t : ts)
c

-- | Similar to 'Data.Monoid.Last': find the last field that is not
-- 'Nothing'.
lastField :: FoldRec ts ts
          => Rec (Maybe :. f) ts -> Maybe (CoRec f ts)
lastField :: forall {k} (ts :: [k]) (f :: k -> *).
FoldRec ts ts =>
Rec (Maybe :. f) ts -> Maybe (CoRec f ts)
lastField Rec (Maybe :. f) ts
RNil = forall a. Maybe a
Nothing
lastField v :: Rec (Maybe :. f) ts
v@((:.) Maybe f r
x :& Rec (Maybe :. f) rs
_) = forall {k} (h :: * -> *) (f :: k -> *) (g :: k -> *) (ts :: [k]).
Functor h =>
(forall (x :: k). f x -> h (g x)) -> CoRec f ts -> h (CoRec g ts)
coRecTraverse forall l k (f :: l -> *) (g :: k -> l) (x :: k).
Compose f g x -> f (g x)
getCompose forall a b. (a -> b) -> a -> b
$ forall {k} (ss :: [k]) (ts :: [k]) (f :: k -> *).
FoldRec ss ts =>
(CoRec f ss -> CoRec f ss -> CoRec f ss)
-> CoRec f ss -> Rec f ts -> CoRec f ss
foldRec forall {a} (f :: a -> *) (t :: a) (ts :: [a]).
CoRec (Maybe :. f) (t : ts)
-> CoRec (Maybe :. f) (t : ts) -> CoRec (Maybe :. f) (t : ts)
aux (forall {k} (r :: k) (ts :: [k]) (f :: k -> *).
RElem r ts (RIndex r ts) =>
f r -> CoRec f ts
CoRec (:.) Maybe f r
x) Rec (Maybe :. f) ts
v
  where aux :: CoRec (Maybe :. f) (t ': ts)
            -> CoRec (Maybe :. f) (t ': ts)
            -> CoRec (Maybe :. f) (t ': ts)
        aux :: forall {a} (f :: a -> *) (t :: a) (ts :: [a]).
CoRec (Maybe :. f) (t : ts)
-> CoRec (Maybe :. f) (t : ts) -> CoRec (Maybe :. f) (t : ts)
aux CoRec (Maybe :. f) (t : ts)
_ c :: CoRec (Maybe :. f) (t : ts)
c@(CoRec (Compose (Just f a
_))) = CoRec (Maybe :. f) (t : ts)
c
        aux CoRec (Maybe :. f) (t : ts)
c CoRec (Maybe :. f) (t : ts)
_ = CoRec (Maybe :. f) (t : ts)
c

-- | Apply methods from a type class to a 'CoRec'. Intended for use
-- with @TypeApplications@, e.g. @onCoRec \@Show show r@
onCoRec :: forall c f ts b g. (RPureConstrained c ts)
        => (forall a. (a  ts, c a) => f a -> g b)
        -> CoRec f ts -> g b
onCoRec :: forall {k} {k} (c :: k -> Constraint) (f :: k -> *) (ts :: [k])
       (b :: k) (g :: k -> *).
RPureConstrained c ts =>
(forall (a :: k). (a ∈ ts, c a) => f a -> g b) -> CoRec f ts -> g b
onCoRec forall (a :: k). (a ∈ ts, c a) => f a -> g b
f (CoRec f a
x) = case forall {k} (c :: k -> Constraint) (ts :: [k]) (a :: k)
       (proxy :: k -> *).
(a ∈ ts, RPureConstrained c ts) =>
proxy a -> DictOnly c a
getDict @c @ts f a
x of
                        DictOnly c a
DictOnly -> forall (a :: k). (a ∈ ts, c a) => f a -> g b
f f a
x
{-# INLINE onCoRec #-}

-- | Apply a type class method to a 'Field'. Intended for use with
-- @TypeApplications@, e.g. @onField \@Show show r@.
onField :: forall c ts b. (RPureConstrained c ts)
        => (forall a. (a  ts, c a) => a -> b)
        -> Field ts -> b
onField :: forall (c :: * -> Constraint) (ts :: [*]) b.
RPureConstrained c ts =>
(forall a. (a ∈ ts, c a) => a -> b) -> Field ts -> b
onField forall a. (a ∈ ts, c a) => a -> b
f Field ts
x = forall a. Identity a -> a
getIdentity (forall {k} {k} (c :: k -> Constraint) (f :: k -> *) (ts :: [k])
       (b :: k) (g :: k -> *).
RPureConstrained c ts =>
(forall (a :: k). (a ∈ ts, c a) => f a -> g b) -> CoRec f ts -> g b
onCoRec @c (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. (a ∈ ts, c a) => a -> b
f) Field ts
x)
{-# INLINE onField #-}

-- * Extracting values from a CoRec/Pattern matching on a CoRec

-- | Compute a runtime 'Int' index identifying the position of the
-- variant held by a @CoRec f ts@ in the type-level list @ts@.
variantIndexOf :: forall f ts. CoRec f ts -> Int
variantIndexOf :: forall {k} (f :: k -> *) (ts :: [k]). CoRec f ts -> Int
variantIndexOf (CoRec f a
x) = forall (a :: k). NatToInt (RIndex a ts) => f a -> Int
aux f a
x
  where aux :: forall a. NatToInt (RIndex a ts) => f a -> Int
        aux :: forall (a :: k). NatToInt (RIndex a ts) => f a -> Int
aux f a
_ = forall (n :: Nat). NatToInt n => Int
natToInt @(RIndex a ts)
{-# INLINE variantIndexOf #-}

-- [NOTE: asA] We want to say that if @NatToInt (RIndex a ts) ~
-- NatToInt (RIndex b ts)@ then @a ~ b@ by relying on an injectivity
-- property of 'RIndex'. However, we are checking the variant index of
-- the argument at runtime, so we do not statically know that
-- extracting the variant at a particular type is safe at compile
-- time.

-- | If a 'CoRec' is a variant of the requested type, return 'Just'
-- that value; otherwise return 'Nothing'.
asA :: NatToInt (RIndex t ts) => CoRec Identity ts -> Maybe t
asA :: forall t (ts :: [*]).
NatToInt (RIndex t ts) =>
CoRec Identity ts -> Maybe t
asA = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Identity a -> a
getIdentity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (t :: k) (ts :: [k]) (f :: k -> *).
NatToInt (RIndex t ts) =>
CoRec f ts -> Maybe (f t)
asA'
{-# INLINE asA #-}

-- | Like 'asA', but for any interpretation functor.
asA' :: forall t ts f. (NatToInt (RIndex t ts))
     => CoRec f ts -> Maybe (f t)
asA' :: forall {k} (t :: k) (ts :: [k]) (f :: k -> *).
NatToInt (RIndex t ts) =>
CoRec f ts -> Maybe (f t)
asA' f :: CoRec f ts
f@(CoRec f a
x)
  | forall {k} (f :: k -> *) (ts :: [k]). CoRec f ts -> Int
variantIndexOf CoRec f ts
f forall a. Eq a => a -> a -> Bool
== forall (n :: Nat). NatToInt n => Int
natToInt @(RIndex t ts) = forall a. a -> Maybe a
Just (forall a b. a -> b
unsafeCoerce f a
x)
  | Bool
otherwise = forall a. Maybe a
Nothing
{-# INLINE asA' #-}

-- | Pattern match on a CoRec by specifying handlers for each case. Note that
-- the order of the Handlers has to match the type level list (t:ts).
--
-- >>> :{
-- let testCoRec = Col (Identity False) :: CoRec Identity [Int, String, Bool] in
-- match testCoRec $
--       (H $ \i -> "my Int is the successor of " ++ show (i - 1))
--    :& (H $ \s -> "my String is: " ++ s)
--    :& (H $ \b -> "my Bool is not: " ++ show (not b) ++ " thus it is " ++ show b)
--    :& RNil
-- :}
-- "my Bool is not: True thus it is False"
match :: forall ts b. CoRec Identity ts -> Handlers ts b -> b
match :: forall (ts :: [*]) b. CoRec Identity ts -> Handlers ts b -> b
match (CoRec (Identity a
t)) Handlers ts b
hs = forall a. RElem a ts (RIndex a ts) => a -> b
aux a
t
  where aux :: forall a. RElem a ts (RIndex a ts) => a -> b
        aux :: forall a. RElem a ts (RIndex a ts) => a -> b
aux a
x = case 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 @a Handlers ts b
hs of
                  H a -> b
f -> a -> b
f a
x

-- | Helper for handling a variant of a 'CoRec': either the function
-- is applied to the variant or the type of the 'CoRec' is refined to
-- reflect the fact that the variant is /not/ compatible with the type
-- of the would-be handler.
class RIndex t ts ~ i => Match1 t ts i where
  match1' :: Handler r t -> Rec Maybe ts -> Either r (Rec Maybe (RDelete t ts))

instance Match1 t (t ': ts) 'Z where
  match1' :: forall r.
Handler r t
-> Rec Maybe (t : ts) -> Either r (Rec Maybe (RDelete t (t : ts)))
match1' Handler r t
_ (Maybe r
Nothing :& Rec Maybe rs
xs) = forall a b. b -> Either a b
Right Rec Maybe rs
xs
  match1' (H t -> r
h) (Just r
x :& Rec Maybe rs
_) = forall a b. a -> Either a b
Left (t -> r
h r
x)

instance (Match1 t ts i, RIndex t (s ': ts) ~ 'S i,
          RDelete t (s ': ts) ~ (s ': RDelete t ts))
         => Match1 t (s ': ts) ('S i) where
  match1' :: forall r.
Handler r t
-> Rec Maybe (s : ts) -> Either r (Rec Maybe (RDelete t (s : ts)))
match1' Handler r t
h (Maybe r
x :& Rec Maybe rs
xs) = (Maybe r
x 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 t (ts :: [*]) (i :: Nat) r.
Match1 t ts i =>
Handler r t -> Rec Maybe ts -> Either r (Rec Maybe (RDelete t ts))
match1' Handler r t
h Rec Maybe rs
xs

-- | Handle a single variant of a 'CoRec': either the function is
-- applied to the variant or the type of the 'CoRec' is refined to
-- reflect the fact that the variant is /not/ compatible with the type
-- of the would-be handler
match1 :: (Match1 t ts (RIndex t ts),
           RecApplicative ts,
           RMap ts, RMap (RDelete t ts),
           FoldRec (RDelete t ts) (RDelete t ts))
       => Handler r t
       -> CoRec Identity ts
       -> Either r (CoRec Identity (RDelete t ts))
match1 :: forall t (ts :: [*]) r.
(Match1 t ts (RIndex t ts), RecApplicative ts, RMap ts,
 RMap (RDelete t ts), FoldRec (RDelete t ts) (RDelete t ts)) =>
Handler r t
-> CoRec Identity ts -> Either r (CoRec Identity (RDelete t ts))
match1 Handler r t
h = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. HasCallStack => Maybe a -> a
fromJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (ts :: [k]) (f :: k -> *).
FoldRec ts ts =>
Rec (Maybe :. f) ts -> Maybe (CoRec f ts)
firstField forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {u} (rs :: [u]) (f :: u -> *) (g :: u -> *).
RMap rs =>
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
rmap (forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
Compose forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> Identity a
Identity))
         forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t (ts :: [*]) (i :: Nat) r.
Match1 t ts i =>
Handler r t -> Rec Maybe ts -> Either r (Rec Maybe (RDelete t ts))
match1' Handler r t
h
         forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (ts :: [*]).
(RecApplicative ts, RMap ts) =>
CoRec Identity ts -> Rec Maybe ts
coRecToRec'

matchNil :: CoRec f '[] -> r
matchNil :: forall {k} (f :: k -> *) r. CoRec f '[] -> r
matchNil (CoRec f a
x) = case f a
x of f a
_ -> forall a. HasCallStack => String -> a
error String
"matchNil: impossible"

-- | Newtype around functions for a to b
newtype Handler b a = H (a -> b)

-- | 'Handlers ts b', is essentially a list of functions, one for each type in
-- ts. All functions produce a value of type 'b'. Hence, 'Handlers ts b' would
-- represent something like the type-level list: [t -> b | t \in ts ]
type Handlers ts b = Rec (Handler b) ts

-- | A 'CoRec' is either the first possible variant indicated by its
-- type, or a 'CoRec' that must be one of the remaining types.
restrictCoRec :: forall t ts f. (RecApplicative ts, FoldRec ts ts)
              => CoRec f (t ': ts) -> Either (f t) (CoRec f ts)
restrictCoRec :: forall {k} (t :: k) (ts :: [k]) (f :: k -> *).
(RecApplicative ts, FoldRec ts ts) =>
CoRec f (t : ts) -> Either (f t) (CoRec f ts)
restrictCoRec CoRec f (t : ts)
r = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a b. b -> Either a b
Right (forall a b. a -> b
unsafeCoerce CoRec f (t : ts)
r)) forall a b. a -> Either a b
Left (forall {k} (t :: k) (ts :: [k]) (f :: k -> *).
NatToInt (RIndex t ts) =>
CoRec f ts -> Maybe (f t)
asA' @t CoRec f (t : ts)
r)
{-# INLINE restrictCoRec #-}

-- | A 'CoRec' whose possible types are @ts@ may be used at a type of
-- 'CoRec' whose possible types are @t:ts@.
weakenCoRec :: (RecApplicative ts, FoldRec (t ': ts) (t ': ts))
            => CoRec f ts -> CoRec f (t ': ts)
weakenCoRec :: forall {a} (ts :: [a]) (t :: a) (f :: a -> *).
(RecApplicative ts, FoldRec (t : ts) (t : ts)) =>
CoRec f ts -> CoRec f (t : ts)
weakenCoRec = forall a. HasCallStack => Maybe a -> a
fromJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (ts :: [k]) (f :: k -> *).
FoldRec ts ts =>
Rec (Maybe :. f) ts -> Maybe (CoRec f ts)
firstField forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
Compose forall a. Maybe a
Nothing forall {u} (f :: u -> *) (r :: u) (rs :: [u]).
f r -> Rec f rs -> Rec f (r : rs)
:&) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {u} (f :: u -> *) (ts :: [u]).
RecApplicative ts =>
CoRec f ts -> Rec (Maybe :. f) ts
coRecToRec

-- * Safe Variants

-- | A 'CoRec' is either the first possible variant indicated by its
-- type, or a 'CoRec' that must be one of the remaining types. The
-- safety is related to that of 'asASafe'.
restrictCoRecSafe :: forall t ts f. (RecApplicative ts, FoldRec ts ts)
                  => CoRec f (t ': ts) -> Either (f t) (CoRec f ts)
restrictCoRecSafe :: forall {k} (t :: k) (ts :: [k]) (f :: k -> *).
(RecApplicative ts, FoldRec ts ts) =>
CoRec f (t : ts) -> Either (f t) (CoRec f ts)
restrictCoRecSafe = Rec (Maybe :. f) (t : ts) -> Either (f t) (CoRec f ts)
go forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {u} (f :: u -> *) (ts :: [u]).
RecApplicative ts =>
CoRec f ts -> Rec (Maybe :. f) ts
coRecToRec
  where go :: Rec (Maybe :. f) (t ': ts) -> Either (f t) (CoRec f ts)
        go :: Rec (Maybe :. f) (t : ts) -> Either (f t) (CoRec f ts)
go (Compose Maybe (f r)
Nothing :& Rec (Maybe :. f) rs
xs) = forall a b. b -> Either a b
Right (forall a. HasCallStack => Maybe a -> a
fromJust (forall {k} (ts :: [k]) (f :: k -> *).
FoldRec ts ts =>
Rec (Maybe :. f) ts -> Maybe (CoRec f ts)
firstField Rec (Maybe :. f) rs
xs))
        go (Compose (Just f r
x) :& Rec (Maybe :. f) rs
_) = forall a b. a -> Either a b
Left f r
x

-- | Like 'asA', but implemented more safely and typically slower.
asASafe :: (t  ts, RecApplicative ts, RMap ts)
        => CoRec Identity ts -> Maybe t
asASafe :: forall t (ts :: [*]).
(t ∈ ts, RecApplicative ts, RMap ts) =>
CoRec Identity ts -> Maybe t
asASafe c :: CoRec Identity ts
c@(CoRec Identity a
_) = 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 forall a b. (a -> b) -> a -> b
$ forall (ts :: [*]).
(RecApplicative ts, RMap ts) =>
CoRec Identity ts -> Rec Maybe ts
coRecToRec' CoRec Identity ts
c

-- | Like 'asASafe', but for any interpretation functor.
asA'Safe :: (t  ts, RecApplicative ts, RMap ts)
         => CoRec f ts -> (Maybe :. f) t
asA'Safe :: forall {k} (t :: k) (ts :: [k]) (f :: k -> *).
(t ∈ ts, RecApplicative ts, RMap ts) =>
CoRec f ts -> (:.) Maybe f t
asA'Safe c :: CoRec f ts
c@(CoRec f a
_) = 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 forall a b. (a -> b) -> a -> b
$ forall {u} (f :: u -> *) (ts :: [u]).
RecApplicative ts =>
CoRec f ts -> Rec (Maybe :. f) ts
coRecToRec CoRec f ts
c