{-# 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 Dep.Env (
Has
, TheDefaultFieldName (..)
, TheFieldName (..)
, FieldsFindableByType (..)
, Autowired (..)
, Autowireable
, Phased (..)
, pullPhase
, mapPhase
, liftA2Phase
, DemotableFieldNames (..)
, demoteFieldNames
, mapPhaseWithFieldNames
, bindPhase
, skipPhase
, Bare
, fromBare
, toBare
, fixEnv
, Constructor
, constructor
, InductiveEnv (..)
, addDep
, emptyEnv
, Identity (..)
, Constant (..)
, Compose (..)
) where
import Dep.Has
import Data.Kind
import GHC.Records
import GHC.TypeLits
import Data.Coerce
import GHC.Generics qualified as G
import Control.Applicative
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 (==))
import Data.Typeable
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) = coerce :: forall a b. Coercible a b => a -> b
coerce forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (x :: k) r a. HasField x r a => r -> a
getField @(DefaultFieldName r_) 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) = coerce :: forall a b. Coercible a b => a -> b
coerce forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (x :: k) r a. HasField x r a => r -> a
getField @name 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) = coerce :: forall a b. Coercible a b => a -> b
coerce @u forall a b. (a -> b) -> a -> b
$ 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
:: forall (h :: Type -> Type)
(f :: Type -> Type)
(g :: Type -> Type)
(m :: Type -> Type).
( Applicative f
, Typeable f
, Typeable g
, Typeable h
, Typeable m
) =>
(forall x . h x -> f (g x)) ->
env_ h m ->
f (env_ g m)
default traverseH
:: forall (h :: Type -> Type)
(f :: Type -> Type)
(g :: Type -> Type)
(m :: Type -> Type).
( Applicative f
, Typeable f
, Typeable g
, Typeable h
, Typeable m
, G.Generic (env_ h m)
, G.Generic (env_ g m)
, GTraverseH h g (G.Rep (env_ h m)) (G.Rep (env_ g m))
)
=> (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 = forall a x. Generic a => Rep a x -> a
G.to forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 (forall a x. Generic a => a -> Rep a x
G.from env_ h m
env)
liftA2H
:: forall (a :: Type -> Type) (f :: Type -> Type) (f' :: Type -> Type) (m :: Type -> Type) .
( Typeable a
, Typeable f
, Typeable f'
, Typeable m
)
=>
(forall x. a x -> f x -> f' x) ->
env_ a m ->
env_ f m ->
env_ f' m
default liftA2H
:: forall (a :: Type -> Type) (f :: Type -> Type) (f' :: Type -> Type) m .
( Typeable a
, Typeable f
, Typeable f'
, Typeable m
, 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 = forall a x. Generic a => Rep a x -> a
G.to (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 (forall a x. Generic a => a -> Rep a x
G.from env_ a m
enva) (forall a x. Generic a => a -> Rep a x
G.from env_ f m
env))
pullPhase :: forall (f :: Type -> Type) (g :: Type -> Type) (m :: Type -> Type) env_ . (Phased env_, Applicative f, Typeable f, Typeable g, Typeable m)
=>
env_ (Compose f g) m
->
f (env_ g m)
pullPhase :: forall (f :: * -> *) (g :: * -> *) (m :: * -> *)
(env_ :: (* -> *) -> (* -> *) -> *).
(Phased env_, Applicative f, Typeable f, Typeable g, Typeable m) =>
env_ (Compose f g) m -> f (env_ g m)
pullPhase = forall (env_ :: (* -> *) -> (* -> *) -> *) (h :: * -> *)
(f :: * -> *) (g :: * -> *) (m :: * -> *).
(Phased env_, Applicative f, Typeable f, Typeable g, Typeable h,
Typeable m) =>
(forall x. h x -> f (g x)) -> env_ h m -> f (env_ g m)
traverseH @env_ forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose
mapPhase :: forall (f :: Type -> Type) (f' :: Type -> Type) (g :: Type -> Type) (m :: Type -> Type) env_ . (Phased env_ , Typeable f, Typeable f', Typeable g, Typeable m)
=>
(forall x. f x -> f' x)
->
env_ (Compose f g) m
->
env_ (Compose f' g) m
mapPhase :: forall (f :: * -> *) (f' :: * -> *) (g :: * -> *) (m :: * -> *)
(env_ :: (* -> *) -> (* -> *) -> *).
(Phased env_, Typeable f, Typeable f', Typeable g, Typeable m) =>
(forall x. f x -> f' x)
-> env_ (Compose f g) m -> env_ (Compose f' g) m
mapPhase forall x. f x -> f' x
f env_ (Compose f g) m
env = forall a. Identity a -> a
runIdentity forall a b. (a -> b) -> a -> b
$ forall (env_ :: (* -> *) -> (* -> *) -> *) (h :: * -> *)
(f :: * -> *) (g :: * -> *) (m :: * -> *).
(Phased env_, Applicative f, Typeable f, Typeable g, Typeable h,
Typeable m) =>
(forall x. h x -> f (g x)) -> env_ h m -> f (env_ g m)
traverseH @env_ (\(Compose f (g x)
fg) -> forall a. a -> Identity a
Identity (forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (forall x. f x -> f' x
f f (g x)
fg))) env_ (Compose f g) m
env
liftA2Phase
:: forall (a :: Type -> Type) (f' :: Type -> Type) (f :: Type -> Type) (g :: Type -> Type) (m :: Type -> Type) env_ . (Phased env_, Typeable a, Typeable f, Typeable f', Typeable g, Typeable m)
=>
(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 (a :: * -> *) (f' :: * -> *) (f :: * -> *) (g :: * -> *)
(m :: * -> *) (env_ :: (* -> *) -> (* -> *) -> *).
(Phased env_, Typeable a, Typeable f, Typeable f', Typeable g,
Typeable m) =>
(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. a x -> f x -> f' x
f = forall (env_ :: (* -> *) -> (* -> *) -> *) (a :: * -> *)
(f :: * -> *) (f' :: * -> *) (m :: * -> *).
(Phased env_, Typeable a, Typeable f, Typeable f', Typeable m) =>
(forall x. a x -> f x -> f' x) -> env_ a m -> env_ f m -> env_ f' m
liftA2H @env_ (\(Compose a (g x)
fa) (Compose f (g x)
fg) -> forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (forall x. 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 (f :: * -> *) (x :: k).
Applicative f =>
(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)) =
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 (f :: * -> *) (x :: k).
Applicative f =>
(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 {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 {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 forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 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 (f :: * -> *) (x :: k).
Applicative f =>
(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))) =
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k i c (p :: k). c -> K1 i c p
G.K1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 (x :: k).
(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)) =
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (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 (x :: k).
(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 {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 {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 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 (x :: k).
(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)) =
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (forall k i c (p :: k). c -> K1 i c p
G.K1 (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 = forall a x. Generic a => Rep a x -> a
G.to (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 :: forall (env_ :: (* -> *) -> (* -> *) -> *) (m :: * -> *).
DemotableFieldNames env_ =>
env_ (Constant String) m
demoteFieldNames = forall (env_ :: (* -> *) -> (* -> *) -> *) (h :: * -> * -> *)
(m :: * -> *).
DemotableFieldNames env_ =>
(forall x. String -> h String x) -> env_ (h String) m
demoteFieldNamesH 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).
(forall (x :: k). String -> h String x)
-> D1 metaData (C1 metaCons fields) x
gDemoteFieldNamesH forall (x :: k). String -> h String x
f = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (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).
(forall (x :: k). String -> h String x) -> (:*:) left right x
gDemoteFieldNamesH forall (x :: k). String -> h String x
f =
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 forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
G.:*: 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).
(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 =
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (forall k i c (p :: k). c -> K1 i c p
G.K1 (forall (x :: k). String -> h String x
f (forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
Proxy @name))))
mapPhaseWithFieldNames ::
forall (f :: Type -> Type) (f' :: Type -> Type) (g :: Type -> Type) (m :: Type -> Type) env_ .
( Phased env_
, DemotableFieldNames env_
, Typeable f
, Typeable f'
, Typeable g
, Typeable m )
=>
(forall x. String -> f x -> f' x)
->
env_ (Compose f g) m
->
env_ (Compose f' g) m
mapPhaseWithFieldNames :: forall (f :: * -> *) (f' :: * -> *) (g :: * -> *) (m :: * -> *)
(env_ :: (* -> *) -> (* -> *) -> *).
(Phased env_, DemotableFieldNames env_, Typeable f, Typeable f',
Typeable g, Typeable m) =>
(forall x. String -> f x -> f' x)
-> env_ (Compose f g) m -> env_ (Compose f' g) m
mapPhaseWithFieldNames forall x. String -> f x -> f' x
f env_ (Compose f g) m
env =
forall (a :: * -> *) (f' :: * -> *) (f :: * -> *) (g :: * -> *)
(m :: * -> *) (env_ :: (* -> *) -> (* -> *) -> *).
(Phased env_, Typeable a, Typeable f, Typeable f', Typeable g,
Typeable m) =>
(forall x. a x -> f x -> f' x)
-> env_ (Compose a g) m
-> env_ (Compose f g) m
-> env_ (Compose f' g) m
liftA2Phase (\(Constant String
name) f x
z -> forall x. String -> f x -> f' x
f String
name f x
z) (forall a. Identity a -> a
runIdentity forall a b. (a -> b) -> a -> b
$ forall (env_ :: (* -> *) -> (* -> *) -> *) (h :: * -> *)
(f :: * -> *) (g :: * -> *) (m :: * -> *).
(Phased env_, Applicative f, Typeable f, Typeable g, Typeable h,
Typeable m) =>
(forall x. h x -> f (g x)) -> env_ h m -> f (env_ g m)
traverseH @env_ (\(Constant String
z) -> forall a. a -> Identity a
Identity (forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (forall {k} a (b :: k). a -> Constant a b
Constant String
z))) 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 :: forall {k1} (f :: * -> *) (g :: k1 -> *) a (b :: k1).
Functor f =>
f a -> (a -> g b) -> Compose f g b
bindPhase f a
f a -> g b
k = forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f a
f 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 :: forall {k1} (f :: * -> *) (g :: k1 -> *) (a :: k1).
Applicative f =>
g a -> Compose f g a
skipPhase g a
g = forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (forall (f :: * -> *) a. Applicative f => a -> f a
pure g a
g)
type Bare :: Type -> Type
type family Bare x where
Bare (Compose outer inner x) = Bare (outer (Bare (inner x)))
Bare (Identity x) = x
Bare (Const x k) = x
Bare (Constant x k) = x
Bare other = other
fromBare :: Coercible phases (Bare phases) => Bare phases -> phases
fromBare :: forall phases.
Coercible phases (Bare phases) =>
Bare phases -> phases
fromBare = coerce :: forall a b. Coercible a b => a -> b
coerce
toBare :: Coercible phases (Bare phases) => phases -> Bare phases
toBare :: forall phases.
Coercible phases (Bare phases) =>
phases -> Bare phases
toBare = coerce :: forall a b. Coercible a b => a -> b
coerce
type Constructor (env :: Type) = ((->) env) `Compose` Identity
constructor :: forall r_ m env . (env -> r_ m) -> Constructor env (r_ m)
constructor :: forall {k} (r_ :: k -> *) (m :: k) env.
(env -> r_ m) -> Constructor env (r_ m)
constructor = coerce :: forall a b. Coercible a b => a -> b
coerce
fixEnv :: (Phased env_, Typeable env_, Typeable m) =>
env_ (Constructor (env_ Identity m)) m ->
env_ Identity m
fixEnv :: forall (env_ :: (* -> *) -> (* -> *) -> *) (m :: * -> *).
(Phased env_, Typeable env_, Typeable m) =>
env_ (Constructor (env_ Identity m)) m -> env_ Identity m
fixEnv env_ (Constructor (env_ Identity m)) m
env = forall a. (a -> a) -> a
fix (forall (f :: * -> *) (g :: * -> *) (m :: * -> *)
(env_ :: (* -> *) -> (* -> *) -> *).
(Phased env_, Applicative f, Typeable f, Typeable g, Typeable m) =>
env_ (Compose f g) m -> f (env_ g m)
pullPhase env_ (Constructor (env_ Identity 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 :: forall (r_ :: (* -> *) -> *) (m :: * -> *) (rs :: [(* -> *) -> *]).
r_ m
-> InductiveEnv rs Identity m -> InductiveEnv (r_ : rs) Identity m
addDep = forall (r_ :: (* -> *) -> *) (m :: * -> *) (rs :: [(* -> *) -> *])
(h :: * -> *).
h (r_ m) -> InductiveEnv rs h m -> InductiveEnv (r_ : rs) h m
AddDep @r_ @m @rs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Identity a
Identity
emptyEnv :: forall m . InductiveEnv '[] Identity m
emptyEnv :: forall (m :: * -> *). InductiveEnv '[] Identity m
emptyEnv = forall (m :: * -> *) (h :: * -> *). InductiveEnv '[] h m
EmptyEnv @m @Identity
instance Phased (InductiveEnv rs) where
traverseH :: forall (h :: * -> *) (f :: * -> *) (g :: * -> *) (m :: * -> *).
(Applicative f, Typeable f, Typeable g, Typeable h, Typeable m) =>
(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 = forall (f :: * -> *) a. Applicative f => a -> f a
pure 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 = forall x. h x -> f (g x)
t h (r_ m)
hx
restF :: f (InductiveEnv rs g m)
restF = forall (env_ :: (* -> *) -> (* -> *) -> *) (h :: * -> *)
(f :: * -> *) (g :: * -> *) (m :: * -> *).
(Phased env_, Applicative f, Typeable f, Typeable g, Typeable h,
Typeable m) =>
(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 forall (r_ :: (* -> *) -> *) (m :: * -> *) (rs :: [(* -> *) -> *])
(h :: * -> *).
h (r_ m) -> InductiveEnv rs h m -> InductiveEnv (r_ : rs) h m
AddDep forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (g (r_ m))
headF forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f (InductiveEnv rs g m)
restF
liftA2H :: forall (a :: * -> *) (f :: * -> *) (f' :: * -> *) (m :: * -> *).
(Typeable a, Typeable f, Typeable f', Typeable m) =>
(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 = 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) =
forall (r_ :: (* -> *) -> *) (m :: * -> *) (rs :: [(* -> *) -> *])
(h :: * -> *).
h (r_ m) -> InductiveEnv rs h m -> InductiveEnv (r_ : rs) h m
AddDep (forall x. a x -> f x -> f' x
t a (r_ m)
ax f (r_ m)
hx) (forall (env_ :: (* -> *) -> (* -> *) -> *) (a :: * -> *)
(f :: * -> *) (f' :: * -> *) (m :: * -> *).
(Phased env_, Typeable a, Typeable f, Typeable f', Typeable 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
t InductiveEnv rs a m
arest 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 = 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 = 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
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
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) = forall (r_ :: (* -> *) -> *) (m :: * -> *) (rs :: [(* -> *) -> *]).
InductiveEnvFind r_ m rs =>
InductiveEnv rs Identity m -> r_ m
inductiveEnvDep InductiveEnv rs Identity m
rest