{-# LANGUAGE AllowAmbiguousTypes, DataKinds, GADTs, QuantifiedConstraints, CPP #-}
module Instance.Runtime (
Instances,
instanceForTypeRep, instanceForInvisible,
instancesForInvisible,
withInstance, withInstanceProxy, withInstanceTypeRep,
foldInstances,
) where
import qualified Data.Map.Lazy as M
import Data.SOP.NP
import Data.SOP.Constraint ( All )
import Type.Reflection.List
import Type.Reflection.Name
import Data.Proxy
import Data.Kind
import Type.Reflection
import Data.Functor
#if __GLASGOW_HASKELL__ < 904
import Unsafe.Coerce
#endif
type Instances :: forall k. Type -> (k -> Constraint) -> Type
newtype Instances type_namer c = MkInstances (M.Map type_namer (EDict c))
deriving (NonEmpty (Instances type_namer c) -> Instances type_namer c
Instances type_namer c
-> Instances type_namer c -> Instances type_namer c
forall b.
Integral b =>
b -> Instances type_namer c -> Instances type_namer c
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
forall type_namer k (c :: k -> Constraint).
Ord type_namer =>
NonEmpty (Instances type_namer c) -> Instances type_namer c
forall type_namer k (c :: k -> Constraint).
Ord type_namer =>
Instances type_namer c
-> Instances type_namer c -> Instances type_namer c
forall type_namer k (c :: k -> Constraint) b.
(Ord type_namer, Integral b) =>
b -> Instances type_namer c -> Instances type_namer c
stimes :: forall b.
Integral b =>
b -> Instances type_namer c -> Instances type_namer c
$cstimes :: forall type_namer k (c :: k -> Constraint) b.
(Ord type_namer, Integral b) =>
b -> Instances type_namer c -> Instances type_namer c
sconcat :: NonEmpty (Instances type_namer c) -> Instances type_namer c
$csconcat :: forall type_namer k (c :: k -> Constraint).
Ord type_namer =>
NonEmpty (Instances type_namer c) -> Instances type_namer c
<> :: Instances type_namer c
-> Instances type_namer c -> Instances type_namer c
$c<> :: forall type_namer k (c :: k -> Constraint).
Ord type_namer =>
Instances type_namer c
-> Instances type_namer c -> Instances type_namer c
Semigroup, Instances type_namer c
[Instances type_namer c] -> Instances type_namer c
Instances type_namer c
-> Instances type_namer c -> Instances type_namer c
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
forall type_namer k (c :: k -> Constraint).
Ord type_namer =>
Semigroup (Instances type_namer c)
forall type_namer k (c :: k -> Constraint).
Ord type_namer =>
Instances type_namer c
forall type_namer k (c :: k -> Constraint).
Ord type_namer =>
[Instances type_namer c] -> Instances type_namer c
forall type_namer k (c :: k -> Constraint).
Ord type_namer =>
Instances type_namer c
-> Instances type_namer c -> Instances type_namer c
mconcat :: [Instances type_namer c] -> Instances type_namer c
$cmconcat :: forall type_namer k (c :: k -> Constraint).
Ord type_namer =>
[Instances type_namer c] -> Instances type_namer c
mappend :: Instances type_namer c
-> Instances type_namer c -> Instances type_namer c
$cmappend :: forall type_namer k (c :: k -> Constraint).
Ord type_namer =>
Instances type_namer c
-> Instances type_namer c -> Instances type_namer c
mempty :: Instances type_namer c
$cmempty :: forall type_namer k (c :: k -> Constraint).
Ord type_namer =>
Instances type_namer c
Monoid)
instance (Show type_namer, Typeable c) => Show (Instances type_namer c) where
show :: Instances type_namer c -> String
show (MkInstances Map type_namer (EDict c)
m) = String
"(Instances for " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @c) forall a. [a] -> [a] -> [a]
++ String
" for types " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall k a. Map k a -> [k]
M.keys Map type_namer (EDict c)
m) forall a. [a] -> [a] -> [a]
++ String
")"
type EDict :: forall k. (k -> Constraint) -> Type
data EDict c where
PackDict :: forall x c. c x => EDict c
instanceForTypeRep ::
forall {k} (x :: k) (c :: k -> Constraint) tn.
c x =>
TypeText tn =>
TypeRep x ->
Instances tn c
instanceForTypeRep :: forall {k} (x :: k) (c :: k -> Constraint) tn.
(c x, TypeText tn) =>
TypeRep x -> Instances tn c
instanceForTypeRep TypeRep x
tr = forall k type_namer (c :: k -> Constraint).
Map type_namer (EDict c) -> Instances type_namer c
MkInstances (forall k a. k -> a -> Map k a
M.singleton (forall tt {k} (t :: k). TypeText tt => TypeRep t -> tt
renderTypeRep TypeRep x
tr) (forall {k} (x :: k) (c :: k -> Constraint). c x => EDict c
PackDict @x))
instanceForInvisible ::
forall {k} (x :: k) (c :: k -> Constraint) tn.
Typeable x =>
c x =>
TypeText tn =>
Instances tn c
instanceForInvisible :: forall {k} (x :: k) (c :: k -> Constraint) tn.
(Typeable x, c x, TypeText tn) =>
Instances tn c
instanceForInvisible = forall {k} (x :: k) (c :: k -> Constraint) tn.
(c x, TypeText tn) =>
TypeRep x -> Instances tn c
instanceForTypeRep (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @x)
instancesForInvisible ::
forall {k} (xs :: [k]) (c :: k -> Constraint) tn.
Typeable xs =>
All c xs =>
TypeText tn =>
Instances tn c
instancesForInvisible :: forall {k} (xs :: [k]) (c :: k -> Constraint) tn.
(Typeable xs, All c xs, TypeText tn) =>
Instances tn c
instancesForInvisible = forall (inner_xs :: [k]).
All c inner_xs =>
NP TypeRep inner_xs -> Instances tn c
go NP TypeRep xs
all_trs
where
tr_xs :: TypeRep xs
tr_xs = forall {k} (a :: k). Typeable a => TypeRep a
typeRep @xs
all_trs :: NP TypeRep xs
all_trs = forall {k} (xs :: [k]). TypeRep xs -> NP TypeRep xs
typeRepList TypeRep xs
tr_xs
go :: forall (inner_xs :: [k]). All c inner_xs => NP TypeRep inner_xs -> Instances tn c
go :: forall (inner_xs :: [k]).
All c inner_xs =>
NP TypeRep inner_xs -> Instances tn c
go (TypeRep x
tr :* NP TypeRep xs
trs) = forall {k} (x :: k) (c :: k -> Constraint) tn.
(c x, TypeText tn) =>
TypeRep x -> Instances tn c
instanceForTypeRep TypeRep x
tr forall a. Semigroup a => a -> a -> a
<> forall (inner_xs :: [k]).
All c inner_xs =>
NP TypeRep inner_xs -> Instances tn c
go NP TypeRep xs
trs
go NP TypeRep inner_xs
Nil = forall a. Monoid a => a
mempty
withInstance :: Ord tn => Instances tn c -> tn -> (forall x. c x => r) -> Maybe r
withInstance :: forall {k} tn (c :: k -> Constraint) r.
Ord tn =>
Instances tn c -> tn -> (forall (x :: k). c x => r) -> Maybe r
withInstance Instances tn c
inst_db tn
type_name forall (x :: k). c x => r
f = forall {k} tn (c :: k -> Constraint) r.
Ord tn =>
Instances tn c
-> tn -> (forall (x :: k). c x => Proxy x -> r) -> Maybe r
withInstanceProxy Instances tn c
inst_db tn
type_name (\ (Proxy x
_ :: Proxy x) -> forall (x :: k). c x => r
f @x)
withInstanceProxy :: Ord tn => Instances tn c -> tn -> (forall x. c x => Proxy x -> r) -> Maybe r
withInstanceProxy :: forall {k} tn (c :: k -> Constraint) r.
Ord tn =>
Instances tn c
-> tn -> (forall (x :: k). c x => Proxy x -> r) -> Maybe r
withInstanceProxy (MkInstances Map tn (EDict c)
mapping) tn
type_name forall (x :: k). c x => Proxy x -> r
f =
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup tn
type_name Map tn (EDict c)
mapping forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ (PackDict @_ @x) -> forall (x :: k). c x => Proxy x -> r
f (forall {k} (t :: k). Proxy t
Proxy @x)
withInstanceTypeRep ::
forall t c tn r.
TypeText tn =>
#if __GLASGOW_HASKELL__ >= 904
(forall x. c x => Typeable x) =>
#endif
Instances tn c -> TypeRep t -> (c t => r) -> Maybe r
withInstanceTypeRep :: forall {k} (t :: k) (c :: k -> Constraint) tn r.
TypeText tn =>
Instances tn c -> TypeRep t -> (c t => r) -> Maybe r
withInstanceTypeRep Instances tn c
instances TypeRep t
type_rep c t => r
action =
forall {k} tn (c :: k -> Constraint) r.
Ord tn =>
Instances tn c
-> tn -> (forall (x :: k). c x => Proxy x -> r) -> Maybe r
withInstanceProxy Instances tn c
instances (forall tt {k} (t :: k). TypeText tt => TypeRep t -> tt
renderTypeRep TypeRep t
type_rep) forall a b. (a -> b) -> a -> b
$ \ (Proxy x
_ :: Proxy t') ->
let
type_rep' :: TypeRep t'
#if __GLASGOW_HASKELL__ >= 904
type_rep' = typeRep
#else
type_rep' :: TypeRep x
type_rep' = forall a b. a -> b
unsafeCoerce TypeRep t
type_rep
#endif
in
case TypeRep t
type_rep forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
`eqTypeRep` TypeRep x
type_rep' of
Just t :~~: x
HRefl -> c t => r
action
Maybe (t :~~: x)
Nothing -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Retrieved type " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypeRep x
type_rep' forall a. [a] -> [a] -> [a]
++
String
" different from expected type " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypeRep t
type_rep forall a. [a] -> [a] -> [a]
++ String
"."
foldInstances ::
Monoid m =>
Instances tn c ->
(forall x. c x => Proxy x -> m) ->
m
foldInstances :: forall {k} m tn (c :: k -> Constraint).
Monoid m =>
Instances tn c -> (forall (x :: k). c x => Proxy x -> m) -> m
foldInstances (MkInstances Map tn (EDict c)
mapping) forall (x :: k). c x => Proxy x -> m
action =
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (\ (PackDict @_ @x) -> forall (x :: k). c x => Proxy x -> m
action @x forall {k} (t :: k). Proxy t
Proxy) Map tn (EDict c)
mapping