@@ -0,0 +1,205 @@
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+{-# LANGUAGE DeriveGeneric #-}
16+-----------------------------------------------------------------------------
17+-- |
18+-- Module : Data.Generics.Sum.HasConstructor
19+-- Copyright : (C) 2017 Csongor Kiss
20+-- License : BSD3
21+-- Maintainer : Csongor Kiss <kiss.csongor.kiss@gmail.com>
22+-- Stability : experimental
23+-- Portability : non-portable
24+--
25+-- Derive prisms generically
26+--
27+-- TODO: add examples
28+-----------------------------------------------------------------------------
29+
30+module Data.Generics.Sum.HasConstructor where
31+
32+import Data.Generics.Internal.Lens
33+
34+import GHC.TypeLits (Symbol, TypeError, ErrorMessage (..))
35+import Data.Kind (Type, Constraint)
36+import GHC.Generics
37+
38+class HasConstructor (con :: Symbol) a s | s con -> a where
39+ is :: Prism' s a
40+
41+instance
42+ ( Generic s
43+ , ErrorUnless (ContainsC con (Rep s)) con s
44+ , GHasConstructor con (Rep s) a
45+ ) => HasConstructor con a s where
46+ is = repIso . gconstruct @con
47+
48+type family ErrorUnless (contains :: Bool) (con :: Symbol) (s :: *) :: Constraint where
49+ ErrorUnless 'False con s
50+ = TypeError ( 'ShowType s
51+ ':<>: 'Text " has no constructor with name "
52+ ':<>: 'ShowType con)
53+ ErrorUnless _ _ _
54+ = ()
55+
56+data HList (xs :: [Type]) where
57+ Nil :: HList '[]
58+ (:>) :: x -> HList xs -> HList (x ': xs)
59+
60+infixr 5 :>
61+
62+append :: HList xs -> HList ys -> HList (xs ++ ys)
63+append Nil ys = ys
64+append (x :> xs) ys = x :> (xs `append` ys)
65+
66+class AsList (tup :: *) (xs :: [*]) | xs -> tup where
67+ asList :: tup -> HList xs
68+ asTuple :: HList xs -> tup
69+
70+instance AsList a '[a] where
71+ asList a
72+ = a :> Nil
73+
74+ asTuple (a :> Nil)
75+ = a
76+
77+instance AsList (a, b) '[a, b] where
78+ asList (a, b)
79+ = a :> b :> Nil
80+
81+ asTuple (a :> b :> Nil)
82+ = (a, b)
83+
84+instance AsList (a, b, c) '[a, b, c] where
85+ asList (a, b, c)
86+ = a :> b :> c :> Nil
87+
88+ asTuple (a :> b :> c :> Nil)
89+ = (a, b, c)
90+
91+instance AsList (a, b, c, d) '[a, b, c, d] where
92+ asList (a, b, c, d)
93+ = a :> b :> c :> d :> Nil
94+
95+ asTuple (a :> b :> c :> d :> Nil)
96+ = (a, b, c, d)
97+
98+instance AsList (a, b, c, d, e) '[a, b, c, d, e] where
99+ asList (a, b, c, d, e)
100+ = a :> b :> c :> d :> e :> Nil
101+
102+ asTuple (a :> b :> c :> d :> e :> Nil)
103+ = (a, b, c, d, e)
104+
105+instance AsList (a, b, c, d, e, f) '[a, b, c, d, e, f] where
106+ asList (a, b, c, d, e, f)
107+ = a :> b :> c :> d :> e :> f :> Nil
108+
109+ asTuple (a :> b :> c :> d :> e :> f :> Nil)
110+ = (a, b, c, d, e, f)
111+
112+instance AsList (a, b, c, d, e, f, g) '[a, b, c, d, e, f, g] where
113+ asList (a, b, c, d, e, f, g)
114+ = a :> b :> c :> d :> e :> f :> g :> Nil
115+
116+ asTuple (a :> b :> c :> d :> e :> f :> g :> Nil)
117+ = (a, b, c, d, e, f, g)
118+
119+instance AsList (a, b, c, d, e, f, g, h) '[a, b, c, d, e, f, g, h] where
120+ asList (a, b, c, d, e, f, g, h)
121+ = a :> b :> c :> d :> e :> f :> g :> h :> Nil
122+
123+ asTuple (a :> b :> c :> d :> e :> f :> g :> h :> Nil)
124+ = (a, b, c, d, e, f, g, h)
125+
126+type family ((xs :: [k]) ++ (ys :: [k])) :: [k] where
127+ '[] ++ ys = ys
128+ (x ': xs) ++ ys = x ': xs ++ ys
129+
130+class GHasConstructor (con :: Symbol) (s :: Type -> Type) a | con s -> a where
131+ gconstruct :: Prism' (s x) a
132+
133+instance GHasConstructor con s a => GHasConstructor con (M1 D c s) a where
134+ gconstruct = mIso . gconstruct @con
135+
136+instance (GCollect s xs, AsList a xs) => GHasConstructor con (M1 C ('MetaCons con f n) s) a where
137+ gconstruct = prism (M1 . gto . asList) (Right . asTuple @_ @xs . gfrom . unM1)
138+
139+instance (GHasConstructor con s a) => GHasConstructor con (M1 S m s) a where
140+ gconstruct = mIso . gconstruct @con
141+
142+class GHasConstructorSum (con :: Symbol) l r a (p :: Bool) | con l r p -> a where
143+ gconstructSum :: Prism' ((l :+: r) x) a
144+
145+instance GHasConstructor con l a => GHasConstructorSum con l r a 'True where
146+ gconstructSum = left . gconstruct @con
147+
148+instance GHasConstructor con r a => GHasConstructorSum con l r a 'False where
149+ gconstructSum = right . gconstruct @con
150+
151+instance GHasConstructorSum con l r a (ContainsC con l) => GHasConstructor con (l :+: r) a where
152+ gconstruct = gconstructSum @con @l @r @a @(ContainsC con l)
153+
154+class Partition xs ys zs | xs ys -> zs, xs zs -> ys where
155+ partition :: HList zs -> (HList xs, HList ys)
156+
157+instance Partition '[] xs xs where
158+ partition xs = (Nil, xs)
159+
160+instance Partition xs ys zs => Partition (x ': xs) ys (x ': zs) where
161+ partition (x :> xs) = (x :> xs', ys')
162+ where (xs', ys') = partition xs
163+
164+class GCollect (s :: Type -> Type) (xs :: [Type]) | s -> xs where
165+ gfrom :: s x -> HList xs
166+ gto :: HList xs -> s x
167+
168+instance (GCollect a as, GCollect b bs, xs ~ (as ++ bs), Partition as bs xs) => GCollect (a :*: b) xs where
169+ gfrom (a :*: b) = gfrom a `append` gfrom b
170+ gto xs = gto l :*: gto r
171+ where (l, r) = partition @as @bs xs
172+
173+instance GCollect (K1 R a) '[a] where
174+ gfrom (K1 x) = x :> Nil
175+ gto (x :> Nil) = K1 x
176+
177+instance GCollect s a => GCollect (M1 S c s) a where
178+ gfrom (M1 x) = gfrom x
179+ gto x = M1 $ gto x
180+
181+instance GCollect s a => GCollect (M1 D c s) a where
182+ gfrom (M1 x) = gfrom x
183+ gto x = M1 $ gto x
184+
185+instance GCollect s a => GCollect (M1 C c s) a where
186+ gfrom (M1 x) = gfrom x
187+ gto x = M1 $ gto x
188+
189+--------------------------------------------------------------------------------
190+
191+type family ContainsC (cname :: Symbol) f :: Bool where
192+ ContainsC cname (C1 ('MetaCons cname _ _) _)
193+ = 'True
194+ ContainsC cname (f :+: g)
195+ = ContainsC cname f || ContainsC cname g
196+ ContainsC cname (D1 m f)
197+ = ContainsC cname f
198+ ContainsC cname _
199+ = 'False
200+
201+-- | Type-level alternative
202+type family (a :: Bool) || (b :: Bool) :: Bool where
203+ 'True || _ = 'True
204+ 'False || b = b
205+