{-# LANGUAGE TypeInType #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Generics.Product.Internal.Positions
( type (<?)
, Size
, CRep
, Context
, Context_
, Context'
, Context0
, derived0
, derived'
) where
import Data.Kind (Type, Constraint)
import Data.Type.Bool (If, Not, type (&&))
import GHC.Generics
import GHC.TypeLits (type (<=?), type (+), Nat, TypeError, ErrorMessage(..))
import Data.Coerce
import Data.Generics.Internal.Families
import Data.Generics.Product.Internal.GLens
import Data.Generics.Internal.Errors
import Data.Generics.Internal.Profunctor.Lens
import Data.Generics.Internal.Profunctor.Iso
type Context' (i :: Nat) s a
= ( Generic s
, ErrorUnless i s (0 <? i && i <=? Size (Rep s))
, Coercible (Rep s) (CRep s)
, GLens' (HasTotalPositionPSym i) (CRep s) a
, Defined (Rep s)
(NoGeneric s '[ 'Text "arising from a generic lens focusing on the field at"
, 'Text "position " ':<>: QuoteType i ':<>: 'Text " of type " ':<>: QuoteType a
':<>: 'Text " in " ':<>: QuoteType s
])
(() :: Constraint)
)
class Context (i :: Nat) s t a b | s i -> a, t i -> b, s i b -> t, t i a -> s
instance
( ErrorUnless i s (0 <? i && i <=? Size (Rep s))
, HasTotalPositionP i (CRep s) ~ 'Just a
, HasTotalPositionP i (CRep t) ~ 'Just b
, HasTotalPositionP i (CRep (Indexed s)) ~ 'Just a'
, HasTotalPositionP i (CRep (Indexed t)) ~ 'Just b'
, t ~ Infer s a' b
, s ~ Infer t b' a
) => Context i s t a b
type Context_ i s t a b =
( ErrorUnless i s (0 <? i && i <=? Size (Rep s))
, UnifyHead s t
, UnifyHead t s
)
type Context0 i s t a b
= ( Generic s
, Generic t
, GLens (HasTotalPositionPSym i) (CRep s) (CRep t) a b
, Coercible (CRep s) (Rep s)
, Coercible (CRep t) (Rep t)
, Defined (Rep s)
(NoGeneric s '[ 'Text "arising from a generic lens focusing on the field at"
, 'Text "position " ':<>: QuoteType i ':<>: 'Text " of type " ':<>: QuoteType a
':<>: 'Text " in " ':<>: QuoteType s
])
(() :: Constraint)
)
derived0 :: forall i s t a b. Context0 i s t a b => Lens s t a b
derived0 :: Lens s t a b
derived0 = (p i (Rep s Any) (Rep t Any) -> p i s t
forall a b x. (Generic a, Generic b) => Iso a b (Rep a x) (Rep b x)
repIso (p i (Rep s Any) (Rep t Any) -> p i s t)
-> (p i a b -> p i (Rep s Any) (Rep t Any)) -> p i a b -> p i s t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (s :: k -> *) (t :: k -> *) (s' :: k -> *) (t' :: k -> *)
(x :: k).
(Coercible t t', Coercible s s') =>
Iso (s' x) (t' x) (s x) (t x)
forall (s' :: G) (t' :: G) x.
(Coercible (CRep t) t', Coercible (CRep s) s') =>
Iso (s' x) (t' x) (CRep s x) (CRep t x)
coerced @(CRep s) @(CRep t) (p i (Fst (Traverse (Rep s) 1) Any) (Fst (Traverse (Rep t) 1) Any)
-> p i (Rep s Any) (Rep t Any))
-> (p i a b
-> p i
(Fst (Traverse (Rep s) 1) Any)
(Fst (Traverse (Rep t) 1) Any))
-> p i a b
-> p i (Rep s Any) (Rep t Any)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: G) (t :: G) a b x.
GLens (HasTotalPositionPSym i) s t a b =>
Lens (s x) (t x) a b
forall (pred :: Pred) (s :: G) (t :: G) a b x.
GLens pred s t a b =>
Lens (s x) (t x) a b
glens @(HasTotalPositionPSym i))
{-# INLINE derived0 #-}
derived' :: forall i s a. Context' i s a => Lens s s a a
derived' :: Lens s s a a
derived' = (p i (Rep s Any) (Rep s Any) -> p i s s
forall a b x. (Generic a, Generic b) => Iso a b (Rep a x) (Rep b x)
repIso (p i (Rep s Any) (Rep s Any) -> p i s s)
-> (p i a a -> p i (Rep s Any) (Rep s Any)) -> p i a a -> p i s s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (s :: k -> *) (t :: k -> *) (s' :: k -> *) (t' :: k -> *)
(x :: k).
(Coercible t t', Coercible s s') =>
Iso (s' x) (t' x) (s x) (t x)
forall (s' :: G) (t' :: G) x.
(Coercible (CRep s) t', Coercible (CRep s) s') =>
Iso (s' x) (t' x) (CRep s x) (CRep s x)
coerced @(CRep s) @(CRep s) (p i (Fst (Traverse (Rep s) 1) Any) (Fst (Traverse (Rep s) 1) Any)
-> p i (Rep s Any) (Rep s Any))
-> (p i a a
-> p i
(Fst (Traverse (Rep s) 1) Any)
(Fst (Traverse (Rep s) 1) Any))
-> p i a a
-> p i (Rep s Any) (Rep s Any)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: G) (t :: G) a b x.
GLens (HasTotalPositionPSym i) s t a b =>
Lens (s x) (t x) a b
forall (pred :: Pred) (s :: G) (t :: G) a b x.
GLens pred s t a b =>
Lens (s x) (t x) a b
glens @(HasTotalPositionPSym i))
{-# INLINE derived' #-}
type family ErrorUnless (i :: Nat) (s :: Type) (hasP :: Bool) :: Constraint where
ErrorUnless i s 'False
= TypeError
( 'Text "The type "
':<>: 'ShowType s
':<>: 'Text " does not contain a field at position "
':<>: 'ShowType i
)
ErrorUnless _ _ 'True
= ()
data HasTotalPositionPSym :: Nat -> (TyFun (Type -> Type) (Maybe Type))
type instance Eval (HasTotalPositionPSym t) tt = HasTotalPositionP t tt
coerced :: forall s t s' t' x. (Coercible t t', Coercible s s')
=> Iso (s' x) (t' x) (s x) (t x)
coerced :: Iso (s' x) (t' x) (s x) (t x)
coerced = (s' x -> s x) -> (t x -> t' x) -> Iso (s' x) (t' x) (s x) (t x)
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso s' x -> s x
coerce t x -> t' x
coerce
{-# INLINE coerced #-}
type G = Type -> Type
type family CRep (a :: Type) :: G where
CRep rep = Fst (Traverse (Rep rep) 1)
type family Traverse (a :: G) (n :: Nat) :: (G, Nat) where
Traverse (M1 mt m s) n
= Traverse1 (M1 mt m) (Traverse s n)
Traverse (l :+: r) n
= '(Fst (Traverse l n) :+: Fst (Traverse r n), n)
Traverse (l :*: r) n
= TraverseProd (:*:) (Traverse l n) r
Traverse (K1 _ p) n
= '(K1 (Pos n) p, n + 1)
Traverse U1 n
= '(U1, n)
type family Traverse1 (w :: G -> G) (z :: (G, Nat)) :: (G, Nat) where
Traverse1 w '(i, n) = '(w i, n)
type family TraverseProd (c :: G -> G -> G) (a :: (G, Nat)) (r :: G) :: (G, Nat) where
TraverseProd w '(i, n) r = Traverse1 (w i) (Traverse r n)
type family Fst (p :: (a, b)) :: a where
Fst '(a, b) = a
type family Size f :: Nat where
Size (l :*: r)
= Size l + Size r
Size (l :+: r)
= Min (Size l) (Size r)
Size (D1 meta f)
= Size f
Size (C1 meta f)
= Size f
Size f
= 1
type x <? y = Not (y <=? x)
infixl 4 <?
type Min a b = If (a <? b) a b