@@ -1,3 +1,4 @@
1+{-# LANGUAGE TypeInType #-}
12{-# LANGUAGE AllowAmbiguousTypes #-}
23{-# LANGUAGE ConstraintKinds #-}
34{-# LANGUAGE DataKinds #-}
@@ -27,41 +28,61 @@
2728-----------------------------------------------------------------------------
2829
2930module Data.Generics.Product.Internal.Positions
30− ( GHasPosition (..)
31− , GHasPosition'
32− , type (<?)
31+ ( type (<?)
3332 , Size
33+ , CRep
3434 ) where
3535
36−import Data.Generics.Product.Internal.List
36+import Data.Generics.Internal.Families.Has (Pos)
3737import Data.Kind (Type)
3838import Data.Type.Bool (If, Not)
3939import GHC.Generics
40−import GHC.TypeLits (type (<=?), type (+), type (-), Nat)
41−import Data.Generics.Internal.Profunctor.Lens
42−import Data.Generics.Internal.Profunctor.Iso
40+import GHC.TypeLits (type (<=?), type (+), Nat)
4341
44−-- |As 'HasPosition' but over generic representations as defined by
45−-- "GHC.Generics".
46−class GHasPosition (i :: Nat) (s :: Type -> Type) (t :: Type -> Type) a b | s i -> a, t i -> b, s t i -> b where
47− gposition :: Lens (s x) (t x) a b
42+-- | Alias for the kind of the generic rep
43+type G k = k -> Type
4844
49−type GHasPosition' i s a = GHasPosition i s s a a
45+--------------------------------------------------------------------------------
5046
51−instance (GHasPosition i l l' a b, GHasPosition i r r' a b) => GHasPosition i (l :+: r) (l' :+: r') a b where
52− gposition = \x -> sumIso (choosing (gposition @i) (gposition @i) x)
53− {-# INLINE gposition #-}
47+-- | In-order labeling of the generic tree with the field positions
48+--
49+-- We replace the (K1 R a) nodes with (K1 (Pos n) a), where 'n' is the position
50+-- of the field in question in the data type. This is convenient, because we
51+-- can reuse all the existing functions as long as they are polymorphic in the
52+-- first parameter of 'K1'.
53+type family CRep (a :: Type) :: G k where
54+ CRep rep = Fst (Traverse (Rep rep) 1)
5455
55−instance GHasPosition i s t a b => GHasPosition i (M1 D meta s) (M1 D meta t) a b where
56− gposition x = mLens (gposition @i x)
57− {-# INLINE gposition #-}
56+-- | The actual traversal.
57+--
58+-- Might be cleaner if the sum and product parts were separated (as there's
59+-- and invariant that 'n' should be zero when we're at a sum node, which holds
60+-- for derived Generic instances (where the sums are strictly above the products))
61+type family Traverse (a :: G k) (n :: Nat) :: (G k, Nat) where
62+ Traverse (M1 mt m s) n
63+ = Traverse1 (M1 mt m) (Traverse s n)
64+ Traverse (l :+: r) n
65+ = '(Fst (Traverse l n) :+: Fst (Traverse r n), n)
66+ Traverse (l :*: r) n
67+ = TraverseProd (:*:) (Traverse l n) r
68+ Traverse (K1 _ p) n
69+ = '(K1 (Pos n) p, n + 1)
70+ Traverse U1 n
71+ = '(U1, n)
5872
59−instance
60− ( IndexList (i - 1) as bs a b
61− , GIsList () f g as bs
62− ) => GHasPosition i (M1 C meta f) (M1 C meta g) a b where
63− gposition x = mIso (glist @() (point @(i - 1) x))
64− {-# INLINE gposition #-}
73+type family Traverse1 (w :: G k -> G k) (z :: (G k, Nat)) :: (G k, Nat) where
74+ Traverse1 w '(i, n) = '(w i, n)
75+
76+-- | For products, we first traverse the left-hand side, followed by the second
77+-- using the counter returned by the left traversal.
78+type family TraverseProd (c :: G k -> G k -> G k) (a :: (G k, Nat)) (r :: G k) :: (G k, Nat) where
79+ TraverseProd w '(i, n) r = Traverse1 (w i) (Traverse r n)
80+
81+--------------------------------------------------------------------------------
82+-- Utilities
83+
84+type family Fst (p :: (a, b)) :: a where
85+ Fst '(a, b) = a
6586
6687type family Size f :: Nat where
6788 Size (l :*: r)
@@ -75,8 +96,6 @@ type family Size f :: Nat where
7596 Size f
7697 = 1
7798
78−--------------------------------------------------------------------------------
79−
8099type x <? y = Not (y <=? x)
81100infixl 4 <?
82101