@@ -4,6 +4,7 @@
44{-# LANGUAGE FunctionalDependencies #-}
55{-# LANGUAGE KindSignatures #-}
66{-# LANGUAGE MultiParamTypeClasses #-}
7+{-# LANGUAGE PolyKinds #-}
78{-# LANGUAGE ScopedTypeVariables #-}
89{-# LANGUAGE TypeApplications #-}
910{-# LANGUAGE TypeFamilies #-}
@@ -12,7 +13,7 @@
1213
1314-----------------------------------------------------------------------------
1415-- |
15−-- Module : Data.Generics.Record.HasField
16+-- Module : Data.Generics.Product.Positions
1617-- Copyright : (C) 2017 Csongor Kiss
1718-- License : BSD3
1819-- Maintainer : Csongor Kiss <kiss.csongor.kiss@gmail.com>
@@ -23,7 +24,7 @@
2324--
2425-----------------------------------------------------------------------------
2526
26−module Data.Generics.Product.Numbered
27+module Data.Generics.Product.Positions
2728 ( -- *Lenses
2829
2930 -- $example
@@ -64,37 +65,33 @@ import GHC.TypeLits
6465-- >>> getPosition @1 human
6566-- "Tunyasz"
6667getPosition :: forall i a s. HasPosition i a s => s -> a
67−getPosition s = s ^. numbered @i
68+getPosition s = s ^. position @i
6869
6970-- | Set positional field
7071--
7172-- >>> setPosition @2 (setField @1 "Tamas" human) 30
7273-- Human "Tamas" 30 "London"
7374setPosition :: forall i a s. HasPosition i a s => a -> s -> s
74−setPosition = set (numbered @i)
75+setPosition = set (position @i)
7576
7677-- |Records that have a field at a given position.
7778class HasPosition (i :: Nat) a s | s i -> a where
7879 -- |A lens that focuses on a field at a given position. Compatible with the
7980 -- lens package's 'Control.Lens.Lens' type.
8081 --
81− -- >>> human ^. numbered @1
82+ -- >>> human ^. position @1
8283 -- "Tunyasz"
83− -- >>> human & numbered @2 .~ "Berlin"
84+ -- >>> human & position @2 .~ "Berlin"
8485 -- Human {name = "Tunyasz", age = 50, address = "Berlin"}
85− numbered :: Lens' s a
86−
87−-- |The base index from which positions are counted.
88−type BaseIndex
89− = 1
86+ position :: Lens' s a
9087
9188instance
9289 ( Generic s
93− , ErrorUnlessTrue i s (HasPositionP BaseIndex i (Rep s))
94− , GHasPosition BaseIndex i (Rep s) a
90+ , ErrorUnlessTrue i s (0 <? i && i <=? Size (Rep s))
91+ , GHasPosition 1 i (Rep s) a
9592 ) => HasPosition i a s where
9693
97− numbered = repIso . gnumbered @BaseIndex @i
94+ position = repIso . gposition @1 @i
9895
9996type family ErrorUnlessTrue (i :: Nat) (s :: Type) (hasP :: Bool) :: Constraint where
10097 ErrorUnlessTrue i s 'False
@@ -111,92 +108,70 @@ type family ErrorUnlessTrue (i :: Nat) (s :: Type) (hasP :: Bool) :: Constraint
111108-- |As 'HasPosition' but over generic representations as defined by
112109-- "GHC.Generics".
113110class GHasPosition (offset :: Nat) (i :: Nat) (f :: Type -> Type) a | offset i f -> a where
114− gnumbered :: Lens' (f x) a
111+ gposition :: Lens' (f x) a
115112
116113instance GHasPosition i i (S1 meta (Rec0 a)) a where
117− gnumbered = mIso . gnumbered @i @i
114+ gposition = mIso . gposition @i @i
118115
119116instance GHasPosition offset i (K1 R a) a where
120− gnumbered f (K1 x) = fmap K1 (f x)
117+ gposition f (K1 x) = fmap K1 (f x)
121118
122119instance GHasPosition offset i f a => GHasPosition offset i (M1 D meta f) a where
123− gnumbered = mIso . gnumbered @offset @i
120+ gposition = mIso . gposition @offset @i
124121
125122instance GHasPosition offset i f a => GHasPosition offset i (M1 C meta f) a where
126− gnumbered = mIso . gnumbered @offset @i
127−
128−instance (dir ~ ChooseDirection offset i l r,
129− offset' ~ Offset dir offset (SizeOf l),
130− GProductHasPosition offset' i l r a dir)
131−
132− => GHasPosition offset i (l :*: r) a where
133−
134− gnumbered = gproductNumbered @offset' @i @_ @_ @_ @dir
135−
136−class GProductHasPosition (offset :: Nat) (i :: Nat) l r a (dir :: Direction) | offset i l r dir -> a where
137− gproductNumbered :: Lens' ((l :*: r) x) a
138−
139−instance GHasPosition offset i l a => GProductHasPosition offset i l r a 'GoLeft where
140− gproductNumbered = first . gnumbered @offset @i
141−
142−instance GHasPosition offset i r a => GProductHasPosition offset i l r a 'GoRight where
143− gproductNumbered = second . gnumbered @offset @i
144−
145−data Direction
146− = GoLeft
147− | GoRight
148−
149−type family ChooseDirection offset i l r :: Direction where
150− ChooseDirection offset i l r
151− = ChooseDirection' (HasPositionP offset i l) (HasPositionP (offset + SizeOf l) i r)
152−
153−type family ChooseDirection' (lHas :: Bool) (rHas :: Bool) :: Direction where
154− ChooseDirection' 'True _
155− = 'GoLeft
156− ChooseDirection' _ 'True
157− = 'GoRight
158−
159−type family HasPositionP (offset :: Nat) (i :: Nat) f :: Bool where
160− HasPositionP offset i (D1 meta f)
161− = HasPositionP offset i f
162− HasPositionP n n (S1 _ _)
163− = 'True
164− HasPositionP _ _ (S1 _ _)
165− = 'False
166− HasPositionP offset i (l :*: r)
167− = HasPositionP offset i l || HasPositionP (offset + SizeOf l) i r
168− HasPositionP offset i (C1 meta f)
169− = HasPositionP offset i f
170− HasPositionP offset i (Rec0 _)
171− = 'False
172− HasPositionP offset i U1
173− = 'False
174− HasPositionP offset i V1
175− = 'False
176− HasPositionP offset i f
177− = TypeError
178− ( 'Text "Cannot determine if the type "
179− ':<>: 'ShowType f
180− ':<>: 'Text " has position "
181− ':<>: 'ShowType i
182− ':<>: 'Text " starting from offset "
183− ':<>: 'ShowType offset
184− )
123+ gposition = mIso . gposition @offset @i
124+
125+instance
126+ ( goLeft ~ (i <? (offset + Size l))
127+ , offset' ~ (If goLeft offset (offset + Size l))
128+ , GProductHasPosition offset' i l r a goLeft
129+ ) => GHasPosition offset i (l :*: r) a where
130+
131+ gposition = gproductPosition @offset' @i @_ @_ @_ @goLeft
132+
133+
134+class GProductHasPosition (offset :: Nat) (i :: Nat) l r a (left :: Bool) | offset i l r left -> a where
135+ gproductPosition :: Lens' ((l :*: r) x) a
185136
186−type family (x :: Bool) || (y :: Bool) :: Bool where
187− 'True || _ = 'True
188− _ || y = y
189−
190−type family SizeOf f :: Nat where
191− SizeOf (l :*: r)
192− = SizeOf l + SizeOf r
193− SizeOf (D1 meta f)
194− = SizeOf f
195− SizeOf (C1 meta f)
196− = SizeOf f
197− SizeOf f
137+instance GHasPosition offset i l a => GProductHasPosition offset i l r a 'True where
138+ gproductPosition = first . gposition @offset @i
139+
140+instance GHasPosition offset i r a => GProductHasPosition offset i l r a 'False where
141+ gproductPosition = second . gposition @offset @i
142+
143+type family Size f :: Nat where
144+ Size (l :*: r)
145+ = Size l + Size r
146+ Size (l :+: r)
147+ = Size l + Size r
148+ Size (D1 meta f)
149+ = Size f
150+ Size (C1 meta f)
151+ = Size f
152+ Size f
198153 = 1
199154
200−type family Offset (dir :: Direction) (offset :: Nat) (sizeOfLeft :: Nat) :: Nat where
201− Offset 'GoLeft offset _ = offset
202− Offset 'GoRight offset sl = offset + sl
155+--------------------------------------------------------------------------------
156+
157+type family Not (b :: Bool) where
158+ Not 'True = 'False
159+ Not 'False = 'True
160+
161+type family (<?) (x :: Nat) (y :: Nat) :: Bool where
162+ x <? y = Not (y <=? x)
163+
164+infixl 4 <?
165+
166+type family If (c :: Bool) (x :: k) (y :: k) :: k where
167+ If 'True x _ = x
168+ If 'False _ y = y
169+
170+type family Min (a :: Nat) (b :: Nat) :: Nat where
171+ Min a b = If (a <? b) a b
172+
173+type family (a :: Bool) && (b :: Bool) :: Bool where
174+ 'True && 'True = 'True
175+ _ && _ = 'False
176+
177+infix 3 &&