@@ -1,255 +0,0 @@
1−{-# LANGUAGE AllowAmbiguousTypes #-}
2−{-# LANGUAGE DataKinds #-}
3−{-# LANGUAGE FlexibleInstances #-}
4−{-# LANGUAGE FunctionalDependencies #-}
5−{-# LANGUAGE GADTs #-}
6−{-# LANGUAGE InstanceSigs #-}
7−{-# LANGUAGE PolyKinds #-}
8−{-# LANGUAGE Rank2Types #-}
9−{-# LANGUAGE ScopedTypeVariables #-}
10−{-# LANGUAGE TypeApplications #-}
11−{-# LANGUAGE TypeFamilies #-}
12−{-# LANGUAGE TypeOperators #-}
13−{-# LANGUAGE UndecidableInstances #-}
14−
15−-----------------------------------------------------------------------------
16−-- |
17−-- Module : Data.Generics.Sum.HasConstructor
18−-- Copyright : (C) 2017 Csongor Kiss
19−-- License : BSD3
20−-- Maintainer : Csongor Kiss <kiss.csongor.kiss@gmail.com>
21−-- Stability : experimental
22−-- Portability : non-portable
23−--
24−-- Derive prisms generically
25−--
26−-- @
27−--
28−-- data FooBar
29−-- = Foo Int
30−-- | Bar Int String
31−-- | Baz (Int, String)
32−-- | Qux
33−-- deriving (Show, Generic)
34−--
35−-- @
36−--
37−-- >>> Bar 5 "coconut" ^? as @"Bar"
38−-- Just (5, "coconut")
39−--
40−-- >>> Qux ^? as @"Qux"
41−-- Just ()
42−--
43−-- >>> as @"Bar" # (5, "asd") :: FooBar
44−-- Bar 5 "asd"
45−--
46−
47−-----------------------------------------------------------------------------
48−
49−module Data.Generics.Sum.HasConstructor
50− ( HasConstructor (..)
51− ) where
52−
53−import Data.Generics.Internal.Lens
54−
55−import GHC.TypeLits (Symbol, TypeError, ErrorMessage (..))
56−import Data.Kind (Type, Constraint)
57−import GHC.Generics
58−
59−class HasConstructor (con :: Symbol) a s | s con -> a where
60− as :: Prism' s a
61−
62−instance
63− ( Generic s
64− , ErrorUnless (ContainsC con (Rep s)) con s
65− , GHasConstructor con (Rep s) a
66− ) => HasConstructor con a s where
67− as = repIso . gconstruct @con
68−
69−--------------------------------------------------------------------------------
70−
71−type family ErrorUnless (contains :: Bool) (con :: Symbol) (s :: *) :: Constraint where
72− ErrorUnless 'False con s
73− = TypeError ( 'ShowType s
74− ':<>: 'Text " has no constructor with name "
75− ':<>: 'ShowType con)
76− ErrorUnless _ _ _
77− = ()
78−
79−--------------------------------------------------------------------------------
80−
81−data HList (xs :: [Type]) where
82− Nil :: HList '[]
83− (:>) :: x -> HList xs -> HList (x ': xs)
84−
85−infixr 5 :>
86−
87−append :: HList xs -> HList ys -> HList (xs ++ ys)
88−append Nil ys = ys
89−append (x :> xs) ys = x :> (xs `append` ys)
90−
91−class AsList (tup :: *) (xs :: [*]) | xs -> tup where
92− asList :: tup -> HList xs
93− asTuple :: HList xs -> tup
94−
95−instance AsList () '[] where
96− asList _
97− = Nil
98−
99− asTuple _
100− = ()
101−
102−instance AsList a '[a] where
103− asList a
104− = a :> Nil
105−
106− asTuple (a :> Nil)
107− = a
108−
109−instance AsList (a, b) '[a, b] where
110− asList (a, b)
111− = a :> b :> Nil
112−
113− asTuple (a :> b :> Nil)
114− = (a, b)
115−
116−instance AsList (a, b, c) '[a, b, c] where
117− asList (a, b, c)
118− = a :> b :> c :> Nil
119−
120− asTuple (a :> b :> c :> Nil)
121− = (a, b, c)
122−
123−instance AsList (a, b, c, d) '[a, b, c, d] where
124− asList (a, b, c, d)
125− = a :> b :> c :> d :> Nil
126−
127− asTuple (a :> b :> c :> d :> Nil)
128− = (a, b, c, d)
129−
130−instance AsList (a, b, c, d, e) '[a, b, c, d, e] where
131− asList (a, b, c, d, e)
132− = a :> b :> c :> d :> e :> Nil
133−
134− asTuple (a :> b :> c :> d :> e :> Nil)
135− = (a, b, c, d, e)
136−
137−instance AsList (a, b, c, d, e, f) '[a, b, c, d, e, f] where
138− asList (a, b, c, d, e, f)
139− = a :> b :> c :> d :> e :> f :> Nil
140−
141− asTuple (a :> b :> c :> d :> e :> f :> Nil)
142− = (a, b, c, d, e, f)
143−
144−instance AsList (a, b, c, d, e, f, g) '[a, b, c, d, e, f, g] where
145− asList (a, b, c, d, e, f, g)
146− = a :> b :> c :> d :> e :> f :> g :> Nil
147−
148− asTuple (a :> b :> c :> d :> e :> f :> g :> Nil)
149− = (a, b, c, d, e, f, g)
150−
151−instance AsList (a, b, c, d, e, f, g, h) '[a, b, c, d, e, f, g, h] where
152− asList (a, b, c, d, e, f, g, h)
153− = a :> b :> c :> d :> e :> f :> g :> h :> Nil
154−
155− asTuple (a :> b :> c :> d :> e :> f :> g :> h :> Nil)
156− = (a, b, c, d, e, f, g, h)
157−
158−type family ((xs :: [k]) ++ (ys :: [k])) :: [k] where
159− '[] ++ ys = ys
160− (x ': xs) ++ ys = x ': xs ++ ys
161−
162−--------------------------------------------------------------------------------
163−
164−class GHasConstructor (con :: Symbol) (s :: Type -> Type) a | con s -> a where
165− gconstruct :: Prism' (s x) a
166−
167−instance GHasConstructor con s a => GHasConstructor con (M1 D c s) a where
168− gconstruct = mIso . gconstruct @con
169−
170−instance (GCollect s xs, AsList a xs) => GHasConstructor con (M1 C ('MetaCons con f n) s) a where
171− gconstruct = prism (M1 . gto . asList) (Right . asTuple @_ @xs . gfrom . unM1)
172−
173−instance (GHasConstructor con s a) => GHasConstructor con (M1 S m s) a where
174− gconstruct = mIso . gconstruct @con
175−
176−class GHasConstructorSum (con :: Symbol) l r a (p :: Bool) | con l r p -> a where
177− gconstructSum :: Prism' ((l :+: r) x) a
178−
179−instance GHasConstructor con l a => GHasConstructorSum con l r a 'True where
180− gconstructSum = left . gconstruct @con
181−
182−instance GHasConstructor con r a => GHasConstructorSum con l r a 'False where
183− gconstructSum = right . gconstruct @con
184−
185−instance GHasConstructorSum con l r a (ContainsC con l) => GHasConstructor con (l :+: r) a where
186− gconstruct = gconstructSum @con @l @r @a @(ContainsC con l)
187−
188−--------------------------------------------------------------------------------
189−-- * Split is the inverse of append
190−
191−class Split xs ys zs | xs ys -> zs, xs zs -> ys where
192− split :: HList zs -> (HList xs, HList ys)
193−
194−instance Split '[] xs xs where
195− split xs = (Nil, xs)
196−
197−instance Split xs ys zs => Split (x ': xs) ys (x ': zs) where
198− split (x :> xs) = (x :> xs', ys')
199− where (xs', ys') = split xs
200−
201−--------------------------------------------------------------------------------
202−
203−-- | Collect parameters of a constructor into an HList
204−class GCollect (s :: Type -> Type) (xs :: [Type]) | s -> xs where
205− gfrom :: s x -> HList xs
206− gto :: HList xs -> s x
207−
208−instance
209− ( GCollect a as
210− , GCollect b bs
211− , xs ~ (as ++ bs)
212− , Split as bs xs
213− ) => GCollect (a :*: b) xs where
214−
215− gfrom (a :*: b) = gfrom a `append` gfrom b
216− gto xs = gto l :*: gto r
217− where (l, r) = split @as @bs xs
218−
219−instance GCollect (K1 R a) '[a] where
220− gfrom (K1 x) = x :> Nil
221− gto (x :> Nil) = K1 x
222−
223−instance GCollect U1 '[] where
224− gfrom U1 = Nil
225− gto Nil = U1
226−
227−instance GCollect s a => GCollect (M1 S c s) a where
228− gfrom (M1 x) = gfrom x
229− gto x = M1 $ gto x
230−
231−instance GCollect s a => GCollect (M1 D c s) a where
232− gfrom (M1 x) = gfrom x
233− gto x = M1 $ gto x
234−
235−instance GCollect s a => GCollect (M1 C c s) a where
236− gfrom (M1 x) = gfrom x
237− gto x = M1 $ gto x
238−
239−--------------------------------------------------------------------------------
240−
241−type family ContainsC (cname :: Symbol) f :: Bool where
242− ContainsC cname (C1 ('MetaCons cname _ _) _)
243− = 'True
244− ContainsC cname (f :+: g)
245− = ContainsC cname f || ContainsC cname g
246− ContainsC cname (D1 m f)
247− = ContainsC cname f
248− ContainsC cname _
249− = 'False
250−
251−-- | Type-level alternative
252−type family (a :: Bool) || (b :: Bool) :: Bool where
253− 'True || _ = 'True
254− 'False || b = b
255−