@@ -0,0 +1,142 @@
1+{-# LANGUAGE AllowAmbiguousTypes #-}
2+{-# LANGUAGE DataKinds #-}
3+{-# LANGUAGE FlexibleInstances #-}
4+{-# LANGUAGE FunctionalDependencies #-}
5+{-# LANGUAGE KindSignatures #-}
6+{-# LANGUAGE MultiParamTypeClasses #-}
7+{-# LANGUAGE ScopedTypeVariables #-}
8+{-# LANGUAGE TypeApplications #-}
9+{-# LANGUAGE TypeFamilies #-}
10+{-# LANGUAGE TypeOperators #-}
11+{-# LANGUAGE UndecidableInstances #-}
12+
13+module Data.Generics.Product.Numbered
14+ ( HasPosition (..)
15+
16+ , GHasPosition (..)
17+ ) where
18+
19+import Data.Generics.Internal.Lens
20+
21+import Data.Kind (Constraint, Type)
22+import GHC.Generics
23+import GHC.TypeLits
24+
25+class HasPosition (i :: Nat) a s | s i -> a where
26+ numbered :: Lens' s a
27+
28+type BaseIndex
29+ = 1
30+
31+instance (Generic s,
32+ hasP ~ HasPositionP BaseIndex i (Rep s),
33+ ErrorUnlessTrue i s hasP,
34+ hasP ~ 'True,
35+ GHasPosition BaseIndex i (Rep s) a)
36+
37+ => HasPosition i a s where
38+
39+ numbered = repIso . gnumbered @BaseIndex @i
40+
41+type family ErrorUnlessTrue (i :: Nat) (s :: Type) (hasP :: Bool) :: Constraint where
42+ ErrorUnlessTrue i s 'False
43+ = TypeError
44+ ( 'Text "The type "
45+ ':<>: 'ShowType s
46+ ':<>: 'Text " does not contain a field at position "
47+ ':<>: 'ShowType i
48+ )
49+
50+ ErrorUnlessTrue _ _ 'True
51+ = ()
52+
53+class GHasPosition (offset :: Nat) (i :: Nat) (f :: Type -> Type) a | offset i f -> a where
54+ gnumbered :: Lens' (f x) a
55+
56+instance GHasPosition i i (S1 meta (Rec0 a)) a where
57+ gnumbered = mIso . gnumbered @i @i
58+
59+instance GHasPosition offset i (K1 R a) a where
60+ gnumbered f (K1 x) = fmap K1 (f x)
61+
62+instance GHasPosition offset i f a => GHasPosition offset i (M1 D meta f) a where
63+ gnumbered = mIso . gnumbered @offset @i
64+
65+instance GHasPosition offset i f a => GHasPosition offset i (M1 C meta f) a where
66+ gnumbered = mIso . gnumbered @offset @i
67+
68+instance (dir ~ ChooseDirection offset i l r,
69+ offset' ~ Offset dir offset (SizeOf l),
70+ GProductHasPosition offset' i l r a dir)
71+
72+ => GHasPosition offset i (l :*: r) a where
73+
74+ gnumbered = gproductNumbered @offset' @i @_ @_ @_ @dir
75+
76+class GProductHasPosition (offset :: Nat) (i :: Nat) l r a (dir :: Direction) | offset i l r dir -> a where
77+ gproductNumbered :: Lens' ((l :*: r) x) a
78+
79+instance GHasPosition offset i l a => GProductHasPosition offset i l r a 'GoLeft where
80+ gproductNumbered = first . gnumbered @offset @i
81+
82+instance GHasPosition offset i r a => GProductHasPosition offset i l r a 'GoRight where
83+ gproductNumbered = second . gnumbered @offset @i
84+
85+data Direction
86+ = GoLeft
87+ | GoRight
88+
89+type family ChooseDirection offset i l r :: Direction where
90+ ChooseDirection offset i l r
91+ = ChooseDirection' (HasPositionP offset i l) (HasPositionP (offset + SizeOf l) i r)
92+
93+type family ChooseDirection' (lHas :: Bool) (rHas :: Bool) :: Direction where
94+ ChooseDirection' 'True _
95+ = 'GoLeft
96+ ChooseDirection' _ 'True
97+ = 'GoRight
98+
99+type family HasPositionP (offset :: Nat) (i :: Nat) f :: Bool where
100+ HasPositionP offset i (D1 meta f)
101+ = HasPositionP offset i f
102+ HasPositionP n n (S1 _ _)
103+ = 'True
104+ HasPositionP _ _ (S1 _ _)
105+ = 'False
106+ HasPositionP offset i (l :*: r)
107+ = HasPositionP offset i l || HasPositionP (offset + SizeOf l) i r
108+ HasPositionP offset i (C1 meta f)
109+ = HasPositionP offset i f
110+ HasPositionP offset i (Rec0 _)
111+ = 'False
112+ HasPositionP offset i U1
113+ = 'False
114+ HasPositionP offset i V1
115+ = 'False
116+ HasPositionP offset i f
117+ = TypeError
118+ ( 'Text "Cannot determine if the type "
119+ ':<>: 'ShowType f
120+ ':<>: 'Text " has position "
121+ ':<>: 'ShowType i
122+ ':<>: 'Text " starting from offset "
123+ ':<>: 'ShowType offset
124+ )
125+
126+type family (x :: Bool) || (y :: Bool) :: Bool where
127+ 'True || _ = 'True
128+ _ || y = y
129+
130+type family SizeOf f :: Nat where
131+ SizeOf (l :*: r)
132+ = SizeOf l + SizeOf r
133+ SizeOf (D1 meta f)
134+ = SizeOf f
135+ SizeOf (C1 meta f)
136+ = SizeOf f
137+ SizeOf f
138+ = 1
139+
140+type family Offset (dir :: Direction) (offset :: Nat) (sizeOfLeft :: Nat) :: Nat where
141+ Offset 'GoLeft offset _ = offset
142+ Offset 'GoRight offset sl = offset + sl