@@ -0,0 +1,177 @@
1+{-# LANGUAGE AllowAmbiguousTypes #-}
2+{-# LANGUAGE DataKinds #-}
3+{-# LANGUAGE FlexibleInstances #-}
4+{-# LANGUAGE FunctionalDependencies #-}
5+{-# LANGUAGE KindSignatures #-}
6+{-# LANGUAGE MultiParamTypeClasses #-}
7+{-# LANGUAGE PolyKinds #-}
8+{-# LANGUAGE ScopedTypeVariables #-}
9+{-# LANGUAGE TypeApplications #-}
10+{-# LANGUAGE TypeFamilies #-}
11+{-# LANGUAGE TypeOperators #-}
12+{-# LANGUAGE UndecidableInstances #-}
13+
14+-----------------------------------------------------------------------------
15+-- |
16+-- Module : Data.Generics.Record.HasField
17+-- Copyright : (C) 2017 Csongor Kiss
18+-- License : BSD3
19+-- Maintainer : Csongor Kiss <kiss.csongor.kiss@gmail.com>
20+-- Stability : experimental
21+-- Portability : non-portable
22+--
23+-- Derive positional product type getters and setters generically.
24+--
25+-----------------------------------------------------------------------------
26+
27+module Data.Generics.Product.Positions
28+ ( -- *Lenses
29+
30+ -- $example
31+ HasPosition (..)
32+ , setPosition
33+ , getPosition
34+
35+ -- *Internals
36+ , GHasPosition (..)
37+ ) where
38+
39+import Data.Generics.Internal.Lens
40+
41+import Data.Kind (Constraint, Type)
42+import GHC.Generics
43+import GHC.TypeLits
44+
45+-- $example
46+-- @
47+-- module Example where
48+--
49+-- import Data.Generics.Product
50+-- import GHC.Generics
51+--
52+-- data Human = Human
53+-- { name :: String
54+-- , age :: Int
55+-- , address :: String
56+-- }
57+-- deriving (Generic, Show)
58+--
59+-- human :: Human
60+-- human = Human \"Tunyasz\" 50 \"London\"
61+-- @
62+
63+-- | Get positional field
64+--
65+-- >>> getPosition @1 human
66+-- "Tunyasz"
67+getPosition :: forall i a s. HasPosition i a s => s -> a
68+getPosition s = s ^. position @i
69+
70+-- | Set positional field
71+--
72+-- >>> setPosition @2 (setField @1 "Tamas" human) 30
73+-- Human "Tamas" 30 "London"
74+setPosition :: forall i a s. HasPosition i a s => a -> s -> s
75+setPosition = set (position @i)
76+
77+-- |Records that have a field at a given position.
78+class HasPosition (i :: Nat) a s | s i -> a where
79+ -- |A lens that focuses on a field at a given position. Compatible with the
80+ -- lens package's 'Control.Lens.Lens' type.
81+ --
82+ -- >>> human ^. position @1
83+ -- "Tunyasz"
84+ -- >>> human & position @2 .~ "Berlin"
85+ -- Human {name = "Tunyasz", age = 50, address = "Berlin"}
86+ position :: Lens' s a
87+
88+instance
89+ ( Generic s
90+ , ErrorUnlessTrue i s (0 <? i && i <=? Size (Rep s))
91+ , GHasPosition 1 i (Rep s) a
92+ ) => HasPosition i a s where
93+
94+ position = repIso . gposition @1 @i
95+
96+type family ErrorUnlessTrue (i :: Nat) (s :: Type) (hasP :: Bool) :: Constraint where
97+ ErrorUnlessTrue i s 'False
98+ = TypeError
99+ ( 'Text "The type "
100+ ':<>: 'ShowType s
101+ ':<>: 'Text " does not contain a field at position "
102+ ':<>: 'ShowType i
103+ )
104+
105+ ErrorUnlessTrue _ _ 'True
106+ = ()
107+
108+-- |As 'HasPosition' but over generic representations as defined by
109+-- "GHC.Generics".
110+class GHasPosition (offset :: Nat) (i :: Nat) (f :: Type -> Type) a | offset i f -> a where
111+ gposition :: Lens' (f x) a
112+
113+instance GHasPosition i i (S1 meta (Rec0 a)) a where
114+ gposition = mIso . gposition @i @i
115+
116+instance GHasPosition offset i (K1 R a) a where
117+ gposition f (K1 x) = fmap K1 (f x)
118+
119+instance GHasPosition offset i f a => GHasPosition offset i (M1 D meta f) a where
120+ gposition = mIso . gposition @offset @i
121+
122+instance GHasPosition offset i f a => GHasPosition offset i (M1 C meta f) a where
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
136+
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
153+ = 1
154+
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 &&