{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
module Control.Monad.Dep.Env (
Has
, TheDefaultFieldName (..)
, TheFieldName (..)
, FieldsFindableByType (..)
, Autowired (..)
, Autowireable
, Phased (..)
, pullPhase
, mapPhase
, liftA2Phase
, DemotableFieldNames (..)
, demoteFieldNames
, mapPhaseWithFieldNames
, bindPhase
, skipPhase
, fixEnv
, Constructor
, constructor
, InductiveEnv (..)
, addDep
, emptyEnv
, Identity (..)
, Constant (..)
, Compose (..)
) where
import Data.Kind
import GHC.Records
import GHC.TypeLits
import Data.Coerce
import GHC.Generics qualified as G
import Control.Applicative
import Control.Monad.Dep.Has
import Data.Proxy
import Data.Functor ((<&>), ($>))
import Data.Functor.Compose
import Data.Functor.Constant
import Data.Functor.Identity
import Data.Function (fix)
import Data.String
import Data.Type.Equality (type (==))
newtype TheDefaultFieldName (env :: Type) = TheDefaultFieldName env
instance (Dep r_, HasField (DefaultFieldName r_) (env_ m) u, Coercible u (r_ m))
=> Has r_ m (TheDefaultFieldName (env_ m)) where
dep :: TheDefaultFieldName (env_ m) -> r_ m
dep (TheDefaultFieldName env_ m
env) = u -> r_ m
coerce (u -> r_ m) -> (env_ m -> u) -> env_ m -> r_ m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (x :: k) r a. HasField x r a => r -> a
forall r a. HasField (DefaultFieldName r_) r a => r -> a
getField @(DefaultFieldName r_) (env_ m -> r_ m) -> env_ m -> r_ m
forall a b. (a -> b) -> a -> b
$ env_ m
env
type TheFieldName :: Symbol -> Type -> Type
newtype TheFieldName (name :: Symbol) (env :: Type) = TheFieldName env
instance (HasField name (env_ m) u, Coercible u (r_ m))
=> Has r_ m (TheFieldName name (env_ m)) where
dep :: TheFieldName name (env_ m) -> r_ m
dep (TheFieldName env_ m
env) = u -> r_ m
coerce (u -> r_ m) -> (env_ m -> u) -> env_ m -> r_ m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (x :: k) r a. HasField x r a => r -> a
forall r a. HasField name r a => r -> a
getField @name (env_ m -> r_ m) -> env_ m -> r_ m
forall a b. (a -> b) -> a -> b
$ env_ m
env
type FieldsFindableByType :: Type -> Constraint
class FieldsFindableByType (env :: Type) where
type FindFieldByType env (r :: Type) :: Symbol
type FindFieldByType env r = FindFieldByType_ env r
type Autowired :: Type -> Type
newtype Autowired (env :: Type) = Autowired env
type Autowireable r_ (m :: Type -> Type) (env :: Type) = HasField (FindFieldByType env (r_ m)) env (Identity (r_ m))
instance (
FieldsFindableByType (env_ m),
HasField (FindFieldByType (env_ m) (r_ m)) (env_ m) u,
Coercible u (r_ m)
)
=> Has r_ m (Autowired (env_ m)) where
dep :: Autowired (env_ m) -> r_ m
dep (Autowired env_ m
env) = forall b. Coercible u b => u -> b
coerce @u (u -> r_ m) -> u -> r_ m
forall a b. (a -> b) -> a -> b
$ env_ m -> u
forall k (x :: k) r a. HasField x r a => r -> a
getField @(FindFieldByType (env_ m) (r_ m)) env_ m
env
type FindFieldByType_ :: Type -> Type -> Symbol
type family FindFieldByType_ env r where
FindFieldByType_ env r = IfMissing r (GFindFieldByType (ExtractProduct (G.Rep env)) r)
type ExtractProduct :: (k -> Type) -> k -> Type
type family envRep where
(G.D1 _ (G.C1 _ z)) = z
type IfMissing :: Type -> Maybe Symbol -> Symbol
type family IfMissing r ms where
IfMissing r Nothing =
TypeError (
Text "The component "
:<>: ShowType r
:<>: Text " could not be found in environment.")
IfMissing _ (Just name) = name
type GFindFieldByType :: (k -> Type) -> Type -> Maybe Symbol
type family GFindFieldByType r x where
GFindFieldByType (left G.:*: right) r =
WithLeftResult_ (GFindFieldByType left r) right r
GFindFieldByType (G.S1 (G.MetaSel ('Just name) _ _ _) (G.Rec0 r)) r = Just name
GFindFieldByType (G.S1 (G.MetaSel ('Just name) _ _ _) (G.Rec0 (_ r))) r = Just name
GFindFieldByType _ _ = Nothing
type WithLeftResult_ :: Maybe Symbol -> (k -> Type) -> Type -> Maybe Symbol
type family WithLeftResult_ leftResult right r where
WithLeftResult_ ('Just ls) right r = 'Just ls
WithLeftResult_ Nothing right r = GFindFieldByType right r
type Phased :: ((Type -> Type) -> (Type -> Type) -> Type) -> Constraint
class Phased (env_ :: (Type -> Type) -> (Type -> Type) -> Type) where
traverseH ::
Applicative f
=> (forall x . h x -> f (g x)) -> env_ h m -> f (env_ g m)
default traverseH
:: ( G.Generic (env_ h m)
, G.Generic (env_ g m)
, GTraverseH h g (G.Rep (env_ h m)) (G.Rep (env_ g m))
, Applicative f )
=> (forall x . h x -> f (g x)) -> env_ h m -> f (env_ g m)
traverseH forall x. h x -> f (g x)
t env_ h m
env = Rep (env_ g m) Any -> env_ g m
forall a x. Generic a => Rep a x -> a
G.to (Rep (env_ g m) Any -> env_ g m)
-> f (Rep (env_ g m) Any) -> f (env_ g m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall x. h x -> f (g x))
-> Rep (env_ h m) Any -> f (Rep (env_ g m) Any)
forall k k (h :: k -> *) (g :: k -> *) (env :: k -> *)
(env' :: k -> *) (f :: * -> *) (x :: k).
(GTraverseH h g env env', Applicative f) =>
(forall (x :: k). h x -> f (g x)) -> env x -> f (env' x)
gTraverseH forall x. h x -> f (g x)
t (env_ h m -> Rep (env_ h m) Any
forall a x. Generic a => a -> Rep a x
G.from env_ h m
env)
liftA2H :: (forall x. a x -> f x -> f' x) -> env_ a m -> env_ f m -> env_ f' m
default liftA2H
:: ( G.Generic (env_ a m)
, G.Generic (env_ f m)
, G.Generic (env_ f' m)
, GLiftA2Phase a f f' (G.Rep (env_ a m)) (G.Rep (env_ f m)) (G.Rep (env_ f' m))
)
=> (forall x. a x -> f x -> f' x) -> env_ a m -> env_ f m -> env_ f' m
liftA2H forall x. a x -> f x -> f' x
f env_ a m
enva env_ f m
env = Rep (env_ f' m) Any -> env_ f' m
forall a x. Generic a => Rep a x -> a
G.to ((forall x. a x -> f x -> f' x)
-> Rep (env_ a m) Any -> Rep (env_ f m) Any -> Rep (env_ f' m) Any
forall k k (a :: k -> *) (f :: k -> *) (f' :: k -> *)
(enva :: k -> *) (env :: k -> *) (env' :: k -> *) (x :: k).
GLiftA2Phase a f f' enva env env' =>
(forall (r :: k). a r -> f r -> f' r) -> enva x -> env x -> env' x
gLiftA2Phase forall x. a x -> f x -> f' x
f (env_ a m -> Rep (env_ a m) Any
forall a x. Generic a => a -> Rep a x
G.from env_ a m
enva) (env_ f m -> Rep (env_ f m) Any
forall a x. Generic a => a -> Rep a x
G.from env_ f m
env))
pullPhase :: forall f g env_ m . (Applicative f, Phased env_) => env_ (Compose f g) m -> f (env_ g m)
pullPhase :: env_ (Compose f g) m -> f (env_ g m)
pullPhase = (forall x. Compose f g x -> f (g x))
-> env_ (Compose f g) m -> f (env_ g m)
forall (env_ :: (* -> *) -> (* -> *) -> *) (f :: * -> *)
(h :: * -> *) (g :: * -> *) (m :: * -> *).
(Phased env_, Applicative f) =>
(forall x. h x -> f (g x)) -> env_ h m -> f (env_ g m)
traverseH forall x. Compose f g x -> f (g x)
forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose
mapPhase :: forall f' f g env_ m . Phased env_ => (forall x. f x -> f' x) -> env_ (Compose f g) m -> env_ (Compose f' g) m
mapPhase :: (forall (x :: k). f x -> f' x)
-> env_ (Compose f g) m -> env_ (Compose f' g) m
mapPhase forall (x :: k). f x -> f' x
f env_ (Compose f g) m
env = Identity (env_ (Compose f' g) m) -> env_ (Compose f' g) m
forall a. Identity a -> a
runIdentity (Identity (env_ (Compose f' g) m) -> env_ (Compose f' g) m)
-> Identity (env_ (Compose f' g) m) -> env_ (Compose f' g) m
forall a b. (a -> b) -> a -> b
$ (forall x. Compose f g x -> Identity (Compose f' g x))
-> env_ (Compose f g) m -> Identity (env_ (Compose f' g) m)
forall (env_ :: (* -> *) -> (* -> *) -> *) (f :: * -> *)
(h :: * -> *) (g :: * -> *) (m :: * -> *).
(Phased env_, Applicative f) =>
(forall x. h x -> f (g x)) -> env_ h m -> f (env_ g m)
traverseH (\(Compose fg) -> Compose f' g x -> Identity (Compose f' g x)
forall a. a -> Identity a
Identity (f' (g x) -> Compose f' g x
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f (g x) -> f' (g x)
forall (x :: k). f x -> f' x
f f (g x)
fg))) env_ (Compose f g) m
env
liftA2Phase :: forall f' a f g env_ m . Phased env_ => (forall x. a x -> f x -> f' x) -> env_ (Compose a g) m -> env_ (Compose f g) m -> env_ (Compose f' g) m
liftA2Phase :: (forall (x :: k). a x -> f x -> f' x)
-> env_ (Compose a g) m
-> env_ (Compose f g) m
-> env_ (Compose f' g) m
liftA2Phase forall (x :: k). a x -> f x -> f' x
f = (forall x. Compose a g x -> Compose f g x -> Compose f' g x)
-> env_ (Compose a g) m
-> env_ (Compose f g) m
-> env_ (Compose f' g) m
forall (env_ :: (* -> *) -> (* -> *) -> *) (a :: * -> *)
(f :: * -> *) (f' :: * -> *) (m :: * -> *).
Phased env_ =>
(forall x. a x -> f x -> f' x) -> env_ a m -> env_ f m -> env_ f' m
liftA2H (\(Compose fa) (Compose fg) -> f' (g x) -> Compose f' g x
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (a (g x) -> f (g x) -> f' (g x)
forall (x :: k). a x -> f x -> f' x
f a (g x)
fa f (g x)
fg))
class GTraverseH h g env env' | env -> h, env' -> g where
gTraverseH :: Applicative f => (forall x . h x -> f (g x)) -> env x -> f (env' x)
instance (GTraverseH h g fields fields')
=> GTraverseH h
g
(G.D1 metaData (G.C1 metaCons fields))
(G.D1 metaData (G.C1 metaCons fields')) where
gTraverseH :: (forall (x :: k). h x -> f (g x))
-> D1 metaData (C1 metaCons fields) x
-> f (D1 metaData (C1 metaCons fields') x)
gTraverseH forall (x :: k). h x -> f (g x)
t (G.M1 (G.M1 fields x
fields)) =
M1 C metaCons fields' x -> D1 metaData (C1 metaCons fields') x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (M1 C metaCons fields' x -> D1 metaData (C1 metaCons fields') x)
-> (fields' x -> M1 C metaCons fields' x)
-> fields' x
-> D1 metaData (C1 metaCons fields') x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. fields' x -> M1 C metaCons fields' x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (fields' x -> D1 metaData (C1 metaCons fields') x)
-> f (fields' x) -> f (D1 metaData (C1 metaCons fields') x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: k). h x -> f (g x)) -> fields x -> f (fields' x)
forall k k (h :: k -> *) (g :: k -> *) (env :: k -> *)
(env' :: k -> *) (f :: * -> *) (x :: k).
(GTraverseH h g env env', Applicative f) =>
(forall (x :: k). h x -> f (g x)) -> env x -> f (env' x)
gTraverseH @h @g forall (x :: k). h x -> f (g x)
t fields x
fields
instance (GTraverseH h g left left',
GTraverseH h g right right')
=> GTraverseH h g (left G.:*: right) (left' G.:*: right') where
gTraverseH :: (forall (x :: k). h x -> f (g x))
-> (:*:) left right x -> f ((:*:) left' right' x)
gTraverseH forall (x :: k). h x -> f (g x)
t (left x
left G.:*: right x
right) =
let left' :: f (left' x)
left' = (forall (x :: k). h x -> f (g x)) -> left x -> f (left' x)
forall k k (h :: k -> *) (g :: k -> *) (env :: k -> *)
(env' :: k -> *) (f :: * -> *) (x :: k).
(GTraverseH h g env env', Applicative f) =>
(forall (x :: k). h x -> f (g x)) -> env x -> f (env' x)
gTraverseH @h @g forall (x :: k). h x -> f (g x)
t left x
left
right' :: f (right' x)
right' = (forall (x :: k). h x -> f (g x)) -> right x -> f (right' x)
forall k k (h :: k -> *) (g :: k -> *) (env :: k -> *)
(env' :: k -> *) (f :: * -> *) (x :: k).
(GTraverseH h g env env', Applicative f) =>
(forall (x :: k). h x -> f (g x)) -> env x -> f (env' x)
gTraverseH @h @g forall (x :: k). h x -> f (g x)
t right x
right
in (left' x -> right' x -> (:*:) left' right' x)
-> f (left' x) -> f (right' x) -> f ((:*:) left' right' x)
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 left' x -> right' x -> (:*:) left' right' x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
(G.:*:) f (left' x)
left' f (right' x)
right'
instance GTraverseH h g (G.S1 metaSel (G.Rec0 (h bean)))
(G.S1 metaSel (G.Rec0 (g bean))) where
gTraverseH :: (forall (x :: k). h x -> f (g x))
-> S1 metaSel (Rec0 (h bean)) x -> f (S1 metaSel (Rec0 (g bean)) x)
gTraverseH forall (x :: k). h x -> f (g x)
t (G.M1 (G.K1 (h bean
hbean))) =
K1 R (g bean) x -> S1 metaSel (Rec0 (g bean)) x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (K1 R (g bean) x -> S1 metaSel (Rec0 (g bean)) x)
-> (g bean -> K1 R (g bean) x)
-> g bean
-> S1 metaSel (Rec0 (g bean)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g bean -> K1 R (g bean) x
forall k i c (p :: k). c -> K1 i c p
G.K1 (g bean -> S1 metaSel (Rec0 (g bean)) x)
-> f (g bean) -> f (S1 metaSel (Rec0 (g bean)) x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> h bean -> f (g bean)
forall (x :: k). h x -> f (g x)
t h bean
hbean
class GLiftA2Phase a f f' enva env env' | enva -> a, env -> f, env' -> f' where
gLiftA2Phase :: (forall r. a r -> f r -> f' r) -> enva x -> env x -> env' x
instance GLiftA2Phase a f f' fieldsa fields fields'
=> GLiftA2Phase
a
f
f'
(G.D1 metaData (G.C1 metaCons fieldsa))
(G.D1 metaData (G.C1 metaCons fields))
(G.D1 metaData (G.C1 metaCons fields')) where
gLiftA2Phase :: (forall (r :: k). a r -> f r -> f' r)
-> D1 metaData (C1 metaCons fieldsa) x
-> D1 metaData (C1 metaCons fields) x
-> D1 metaData (C1 metaCons fields') x
gLiftA2Phase forall (r :: k). a r -> f r -> f' r
f (G.M1 (G.M1 fieldsa x
fieldsa)) (G.M1 (G.M1 fields x
fields)) =
M1 C metaCons fields' x -> D1 metaData (C1 metaCons fields') x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (fields' x -> M1 C metaCons fields' x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 ((forall (r :: k). a r -> f r -> f' r)
-> fieldsa x -> fields x -> fields' x
forall k k (a :: k -> *) (f :: k -> *) (f' :: k -> *)
(enva :: k -> *) (env :: k -> *) (env' :: k -> *) (x :: k).
GLiftA2Phase a f f' enva env env' =>
(forall (r :: k). a r -> f r -> f' r) -> enva x -> env x -> env' x
gLiftA2Phase @a @f @f' forall (r :: k). a r -> f r -> f' r
f fieldsa x
fieldsa fields x
fields))
instance ( GLiftA2Phase a f f' lefta left left',
GLiftA2Phase a f f' righta right right'
)
=> GLiftA2Phase a f f' (lefta G.:*: righta) (left G.:*: right) (left' G.:*: right') where
gLiftA2Phase :: (forall (r :: k). a r -> f r -> f' r)
-> (:*:) lefta righta x
-> (:*:) left right x
-> (:*:) left' right' x
gLiftA2Phase forall (r :: k). a r -> f r -> f' r
f (lefta x
lefta G.:*: righta x
righta) (left x
left G.:*: right x
right) =
let left' :: left' x
left' = (forall (r :: k). a r -> f r -> f' r)
-> lefta x -> left x -> left' x
forall k k (a :: k -> *) (f :: k -> *) (f' :: k -> *)
(enva :: k -> *) (env :: k -> *) (env' :: k -> *) (x :: k).
GLiftA2Phase a f f' enva env env' =>
(forall (r :: k). a r -> f r -> f' r) -> enva x -> env x -> env' x
gLiftA2Phase @a @f @f' forall (r :: k). a r -> f r -> f' r
f lefta x
lefta left x
left
right' :: right' x
right' = (forall (r :: k). a r -> f r -> f' r)
-> righta x -> right x -> right' x
forall k k (a :: k -> *) (f :: k -> *) (f' :: k -> *)
(enva :: k -> *) (env :: k -> *) (env' :: k -> *) (x :: k).
GLiftA2Phase a f f' enva env env' =>
(forall (r :: k). a r -> f r -> f' r) -> enva x -> env x -> env' x
gLiftA2Phase @a @f @f' forall (r :: k). a r -> f r -> f' r
f righta x
righta right x
right
in left' x -> right' x -> (:*:) left' right' x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
(G.:*:) left' x
left' right' x
right'
instance GLiftA2Phase a f f' (G.S1 metaSel (G.Rec0 (a bean)))
(G.S1 metaSel (G.Rec0 (f bean)))
(G.S1 metaSel (G.Rec0 (f' bean))) where
gLiftA2Phase :: (forall (r :: k). a r -> f r -> f' r)
-> S1 metaSel (Rec0 (a bean)) x
-> S1 metaSel (Rec0 (f bean)) x
-> S1 metaSel (Rec0 (f' bean)) x
gLiftA2Phase forall (r :: k). a r -> f r -> f' r
f (G.M1 (G.K1 a bean
abean)) (G.M1 (G.K1 f bean
fgbean)) =
K1 R (f' bean) x -> S1 metaSel (Rec0 (f' bean)) x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (f' bean -> K1 R (f' bean) x
forall k i c (p :: k). c -> K1 i c p
G.K1 (a bean -> f bean -> f' bean
forall (r :: k). a r -> f r -> f' r
f a bean
abean f bean
fgbean))
type DemotableFieldNames :: ((Type -> Type) -> (Type -> Type) -> Type) -> Constraint
class DemotableFieldNames env_ where
demoteFieldNamesH :: (forall x. String -> h String x) -> env_ (h String) m
default demoteFieldNamesH
:: ( G.Generic (env_ (h String) m)
, GDemotableFieldNamesH h (G.Rep (env_ (h String) m)))
=> (forall x. String -> h String x)
-> env_ (h String) m
demoteFieldNamesH forall x. String -> h String x
f = Rep (env_ (h String) m) Any -> env_ (h String) m
forall a x. Generic a => Rep a x -> a
G.to ((forall x. String -> h String x) -> Rep (env_ (h String) m) Any
forall k k (h :: * -> k -> *) (env :: k -> *) (x :: k).
GDemotableFieldNamesH h env =>
(forall (x :: k). String -> h String x) -> env x
gDemoteFieldNamesH forall x. String -> h String x
f)
demoteFieldNames :: forall env_ m . DemotableFieldNames env_ => env_ (Constant String) m
demoteFieldNames :: env_ (Constant String) m
demoteFieldNames = (forall x. String -> Constant String x) -> env_ (Constant String) m
forall (env_ :: (* -> *) -> (* -> *) -> *) (h :: * -> * -> *)
(m :: * -> *).
DemotableFieldNames env_ =>
(forall x. String -> h String x) -> env_ (h String) m
demoteFieldNamesH forall x. String -> Constant String x
forall k a (b :: k). a -> Constant a b
Constant
class GDemotableFieldNamesH h env | env -> h where
gDemoteFieldNamesH :: (forall x. String -> h String x) -> env x
instance GDemotableFieldNamesH h fields
=> GDemotableFieldNamesH h (G.D1 metaData (G.C1 metaCons fields)) where
gDemoteFieldNamesH :: (forall (x :: k). String -> h String x)
-> D1 metaData (C1 metaCons fields) x
gDemoteFieldNamesH forall (x :: k). String -> h String x
f = M1 C metaCons fields x -> D1 metaData (C1 metaCons fields) x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (fields x -> M1 C metaCons fields x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 ((forall (x :: k). String -> h String x) -> fields x
forall k k (h :: * -> k -> *) (env :: k -> *) (x :: k).
GDemotableFieldNamesH h env =>
(forall (x :: k). String -> h String x) -> env x
gDemoteFieldNamesH forall (x :: k). String -> h String x
f))
instance ( GDemotableFieldNamesH h left,
GDemotableFieldNamesH h right)
=> GDemotableFieldNamesH h (left G.:*: right) where
gDemoteFieldNamesH :: (forall (x :: k). String -> h String x) -> (:*:) left right x
gDemoteFieldNamesH forall (x :: k). String -> h String x
f =
(forall (x :: k). String -> h String x) -> left x
forall k k (h :: * -> k -> *) (env :: k -> *) (x :: k).
GDemotableFieldNamesH h env =>
(forall (x :: k). String -> h String x) -> env x
gDemoteFieldNamesH forall (x :: k). String -> h String x
f left x -> right x -> (:*:) left right x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
G.:*: (forall (x :: k). String -> h String x) -> right x
forall k k (h :: * -> k -> *) (env :: k -> *) (x :: k).
GDemotableFieldNamesH h env =>
(forall (x :: k). String -> h String x) -> env x
gDemoteFieldNamesH forall (x :: k). String -> h String x
f
instance KnownSymbol name => GDemotableFieldNamesH h (G.S1 (G.MetaSel ('Just name) u v w) (G.Rec0 (h String bean))) where
gDemoteFieldNamesH :: (forall (x :: k). String -> h String x)
-> S1 ('MetaSel ('Just name) u v w) (Rec0 (h String bean)) x
gDemoteFieldNamesH forall (x :: k). String -> h String x
f =
K1 R (h String bean) x
-> S1 ('MetaSel ('Just name) u v w) (Rec0 (h String bean)) x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (h String bean -> K1 R (h String bean) x
forall k i c (p :: k). c -> K1 i c p
G.K1 (String -> h String bean
forall (x :: k). String -> h String x
f (Proxy name -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (Proxy name
forall k (t :: k). Proxy t
Proxy @name))))
mapPhaseWithFieldNames :: forall f' f g env_ m. (Phased env_, DemotableFieldNames env_)
=> (forall x. String -> f x -> f' x) -> env_ (Compose f g) m -> env_ (Compose f' g) m
mapPhaseWithFieldNames :: (forall (x :: k). String -> f x -> f' x)
-> env_ (Compose f g) m -> env_ (Compose f' g) m
mapPhaseWithFieldNames forall (x :: k). String -> f x -> f' x
f env_ (Compose f g) m
env =
(forall (x :: k). Constant String x -> f x -> f' x)
-> env_ (Compose (Constant String) g) m
-> env_ (Compose f g) m
-> env_ (Compose f' g) m
forall k (f' :: k -> *) (a :: k -> *) (f :: k -> *) (g :: * -> k)
(env_ :: (* -> *) -> (* -> *) -> *) (m :: * -> *).
Phased env_ =>
(forall (x :: k). a x -> f x -> f' x)
-> env_ (Compose a g) m
-> env_ (Compose f g) m
-> env_ (Compose f' g) m
liftA2Phase (\(Constant name) f x
z -> String -> f x -> f' x
forall (x :: k). String -> f x -> f' x
f String
name f x
z) (Identity (env_ (Compose (Constant String) g) m)
-> env_ (Compose (Constant String) g) m
forall a. Identity a -> a
runIdentity (Identity (env_ (Compose (Constant String) g) m)
-> env_ (Compose (Constant String) g) m)
-> Identity (env_ (Compose (Constant String) g) m)
-> env_ (Compose (Constant String) g) m
forall a b. (a -> b) -> a -> b
$ (forall x.
Constant String x -> Identity (Compose (Constant String) g x))
-> env_ (Constant String) m
-> Identity (env_ (Compose (Constant String) g) m)
forall (env_ :: (* -> *) -> (* -> *) -> *) (f :: * -> *)
(h :: * -> *) (g :: * -> *) (m :: * -> *).
(Phased env_, Applicative f) =>
(forall x. h x -> f (g x)) -> env_ h m -> f (env_ g m)
traverseH (\(Constant z) -> Compose (Constant String) g x
-> Identity (Compose (Constant String) g x)
forall a. a -> Identity a
Identity (Constant String (g x) -> Compose (Constant String) g x
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (String -> Constant String (g x)
forall k a (b :: k). a -> Constant a b
Constant String
z))) env_ (Constant String) m
forall (env_ :: (* -> *) -> (* -> *) -> *) (m :: * -> *).
DemotableFieldNames env_ =>
env_ (Constant String) m
demoteFieldNames) env_ (Compose f g) m
env
bindPhase :: forall f g a b . Functor f => f a -> (a -> g b) -> Compose f g b
bindPhase :: f a -> (a -> g b) -> Compose f g b
bindPhase f a
f a -> g b
k = f (g b) -> Compose f g b
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f a
f f a -> (a -> g b) -> f (g b)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> a -> g b
k)
skipPhase :: forall f g a . Applicative f => g a -> Compose f g a
skipPhase :: g a -> Compose f g a
skipPhase g a
g = f (g a) -> Compose f g a
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (g a -> f (g a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure g a
g)
type Constructor (env_ :: (Type -> Type) -> (Type -> Type) -> Type) (m :: Type -> Type) = ((->) (env_ Identity m)) `Compose` Identity
constructor :: forall r_ env_ m . (env_ Identity m -> r_ m) -> Constructor env_ m (r_ m)
constructor :: (env_ Identity m -> r_ m) -> Constructor env_ m (r_ m)
constructor = (env_ Identity m -> r_ m) -> Constructor env_ m (r_ m)
coerce
fixEnv :: Phased env_ => env_ (Constructor env_ m) m -> env_ Identity m
fixEnv :: env_ (Constructor env_ m) m -> env_ Identity m
fixEnv env_ (Constructor env_ m) m
env = (env_ Identity m -> env_ Identity m) -> env_ Identity m
forall a. (a -> a) -> a
fix (env_ (Constructor env_ m) m -> env_ Identity m -> env_ Identity m
forall (f :: * -> *) (g :: * -> *)
(env_ :: (* -> *) -> (* -> *) -> *) (m :: * -> *).
(Applicative f, Phased env_) =>
env_ (Compose f g) m -> f (env_ g m)
pullPhase env_ (Constructor env_ m) m
env)
data InductiveEnv (rs :: [(Type -> Type) -> Type]) (h :: Type -> Type) (m :: Type -> Type) where
AddDep :: forall r_ m rs h . h (r_ m) -> InductiveEnv rs h m -> InductiveEnv (r_ : rs) h m
EmptyEnv :: forall m h . InductiveEnv '[] h m
addDep :: forall r_ m rs . r_ m -> InductiveEnv rs Identity m -> InductiveEnv (r_ : rs) Identity m
addDep :: r_ m
-> InductiveEnv rs Identity m -> InductiveEnv (r_ : rs) Identity m
addDep = forall (h :: * -> *).
h (r_ m) -> InductiveEnv rs h m -> InductiveEnv (r_ : rs) h m
forall (r_ :: (* -> *) -> *) (m :: * -> *) (rs :: [(* -> *) -> *])
(h :: * -> *).
h (r_ m) -> InductiveEnv rs h m -> InductiveEnv (r_ : rs) h m
AddDep @r_ @m @rs (Identity (r_ m)
-> InductiveEnv rs Identity m -> InductiveEnv (r_ : rs) Identity m)
-> (r_ m -> Identity (r_ m))
-> r_ m
-> InductiveEnv rs Identity m
-> InductiveEnv (r_ : rs) Identity m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. r_ m -> Identity (r_ m)
forall a. a -> Identity a
Identity
emptyEnv :: forall m . InductiveEnv '[] Identity m
emptyEnv :: InductiveEnv '[] Identity m
emptyEnv = InductiveEnv '[] Identity m
forall (m :: * -> *) (h :: * -> *). InductiveEnv '[] h m
EmptyEnv @m @Identity
instance Phased (InductiveEnv rs) where
traverseH :: (forall x. h x -> f (g x))
-> InductiveEnv rs h m -> f (InductiveEnv rs g m)
traverseH forall x. h x -> f (g x)
t InductiveEnv rs h m
EmptyEnv = InductiveEnv '[] g m -> f (InductiveEnv '[] g m)
forall (f :: * -> *) a. Applicative f => a -> f a
pure InductiveEnv '[] g m
forall (m :: * -> *) (h :: * -> *). InductiveEnv '[] h m
EmptyEnv
traverseH forall x. h x -> f (g x)
t (AddDep h (r_ m)
hx InductiveEnv rs h m
rest) =
let headF :: f (g (r_ m))
headF = h (r_ m) -> f (g (r_ m))
forall x. h x -> f (g x)
t h (r_ m)
hx
restF :: f (InductiveEnv rs g m)
restF = (forall x. h x -> f (g x))
-> InductiveEnv rs h m -> f (InductiveEnv rs g m)
forall (env_ :: (* -> *) -> (* -> *) -> *) (f :: * -> *)
(h :: * -> *) (g :: * -> *) (m :: * -> *).
(Phased env_, Applicative f) =>
(forall x. h x -> f (g x)) -> env_ h m -> f (env_ g m)
traverseH forall x. h x -> f (g x)
t InductiveEnv rs h m
rest
in g (r_ m) -> InductiveEnv rs g m -> InductiveEnv (r_ : rs) g m
forall (r_ :: (* -> *) -> *) (m :: * -> *) (rs :: [(* -> *) -> *])
(h :: * -> *).
h (r_ m) -> InductiveEnv rs h m -> InductiveEnv (r_ : rs) h m
AddDep (g (r_ m) -> InductiveEnv rs g m -> InductiveEnv (r_ : rs) g m)
-> f (g (r_ m))
-> f (InductiveEnv rs g m -> InductiveEnv (r_ : rs) g m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (g (r_ m))
headF f (InductiveEnv rs g m -> InductiveEnv (r_ : rs) g m)
-> f (InductiveEnv rs g m) -> f (InductiveEnv (r_ : rs) g m)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f (InductiveEnv rs g m)
restF
liftA2H :: (forall x. a x -> f x -> f' x)
-> InductiveEnv rs a m
-> InductiveEnv rs f m
-> InductiveEnv rs f' m
liftA2H forall x. a x -> f x -> f' x
t InductiveEnv rs a m
EmptyEnv InductiveEnv rs f m
EmptyEnv = InductiveEnv rs f' m
forall (m :: * -> *) (h :: * -> *). InductiveEnv '[] h m
EmptyEnv
liftA2H forall x. a x -> f x -> f' x
t (AddDep a (r_ m)
ax InductiveEnv rs a m
arest) (AddDep f (r_ m)
hx InductiveEnv rs f m
hrest) =
f' (r_ m) -> InductiveEnv rs f' m -> InductiveEnv (r_ : rs) f' m
forall (r_ :: (* -> *) -> *) (m :: * -> *) (rs :: [(* -> *) -> *])
(h :: * -> *).
h (r_ m) -> InductiveEnv rs h m -> InductiveEnv (r_ : rs) h m
AddDep (a (r_ m) -> f (r_ m) -> f' (r_ m)
forall x. a x -> f x -> f' x
t a (r_ m)
ax f (r_ m)
f (r_ m)
hx) ((forall x. a x -> f x -> f' x)
-> InductiveEnv rs a m
-> InductiveEnv rs f m
-> InductiveEnv rs f' m
forall (env_ :: (* -> *) -> (* -> *) -> *) (a :: * -> *)
(f :: * -> *) (f' :: * -> *) (m :: * -> *).
Phased env_ =>
(forall x. a x -> f x -> f' x) -> env_ a m -> env_ f m -> env_ f' m
liftA2H forall x. a x -> f x -> f' x
t InductiveEnv rs a m
arest InductiveEnv rs f m
InductiveEnv rs f m
hrest)
instance InductiveEnvFind r_ m rs => Has r_ m (InductiveEnv rs Identity m) where
dep :: InductiveEnv rs Identity m -> r_ m
dep = InductiveEnv rs Identity m -> r_ m
forall (r_ :: (* -> *) -> *) (m :: * -> *) (rs :: [(* -> *) -> *]).
InductiveEnvFind r_ m rs =>
InductiveEnv rs Identity m -> r_ m
inductiveEnvDep
class InductiveEnvFind r_ m rs where
inductiveEnvDep :: InductiveEnv rs Identity m -> r_ m
instance TypeError (
Text "The component "
:<>: ShowType r_
:<>: Text " could not be found in environment.") => InductiveEnvFind r_ m '[] where
inductiveEnvDep :: InductiveEnv '[] Identity m -> r_ m
inductiveEnvDep = String -> InductiveEnv '[] Identity m -> r_ m
forall a. HasCallStack => String -> a
error String
"never happens"
instance InductiveEnvFind' (r_ == r_') r_ m (r_' : rs) => InductiveEnvFind r_ m (r_' : rs) where
inductiveEnvDep :: InductiveEnv (r_' : rs) Identity m -> r_ m
inductiveEnvDep = forall (matches :: Bool) (r_ :: (* -> *) -> *) (m :: * -> *)
(rs :: [(* -> *) -> *]).
InductiveEnvFind' matches r_ m rs =>
InductiveEnv rs Identity m -> r_ m
forall (r_ :: (* -> *) -> *) (m :: * -> *) (rs :: [(* -> *) -> *]).
InductiveEnvFind' (r_ == r_') r_ m rs =>
InductiveEnv rs Identity m -> r_ m
inductiveEnvDep' @(r_ == r_')
class InductiveEnvFind' (matches :: Bool) r_ m rs where
inductiveEnvDep' :: InductiveEnv rs Identity m -> r_ m
instance InductiveEnvFind' True r_ m (r_ : rs) where
inductiveEnvDep' :: InductiveEnv (r_ : rs) Identity m -> r_ m
inductiveEnvDep' (AddDep (Identity r_ m
r) InductiveEnv rs Identity m
_) = r_ m
r_ m
r
instance InductiveEnvFind r_ m rs => InductiveEnvFind' False r_ m (x : rs) where
inductiveEnvDep' :: InductiveEnv (x : rs) Identity m -> r_ m
inductiveEnvDep' (AddDep Identity (r_ m)
_ InductiveEnv rs Identity m
rest) = InductiveEnv rs Identity m -> r_ m
forall (r_ :: (* -> *) -> *) (m :: * -> *) (rs :: [(* -> *) -> *]).
InductiveEnvFind r_ m rs =>
InductiveEnv rs Identity m -> r_ m
inductiveEnvDep InductiveEnv rs Identity m
rest