{-# LANGUAGE AllowAmbiguousTypes, BangPatterns, CPP, ConstraintKinds,
DataKinds, EmptyCase, FlexibleContexts,
FlexibleInstances, GADTs, KindSignatures,
MultiParamTypeClasses, PolyKinds, RankNTypes,
ScopedTypeVariables, TypeApplications, TypeOperators,
UndecidableInstances #-}
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)
data CoRec :: (k -> *) -> [k] -> * where
CoRec :: RElem a ts (RIndex a ts) => !(f a) -> CoRec f ts
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
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
type Field = CoRec Identity
newtype Op b a = Op { forall b a. Op b a -> a -> b
runOp :: a -> b }
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'
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))
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
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
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)
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)
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)
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)
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
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
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
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 #-}
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 #-}
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 #-}
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 #-}
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' #-}
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
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
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 Handler b a = H (a -> b)
type Handlers ts b = Rec (Handler b) ts
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 #-}
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
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
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
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