git.iko.soy/generic-lens
on master help sign in
Remove Peano from Changing (Nat is fine)
e48f8f5Csongor Kiss
src/Data/Generics/Internal/Families/Changing.hs+11−19
compare with master
unifiedsplit
@@ -12,12 +12,10 @@ module Data.Generics.Internal.Families.Changing
12 ( Proxied
12 ( Proxied
13 , Infer
13 , Infer
14 , PTag (..)
14 , PTag (..)
15− , Peano (..)
16− , NatToPeano
17 , P
15 , P
18 ) where
16 ) where
19
17
20−import GHC.TypeLits (Nat, type (-), TypeError, ErrorMessage (..))
18+import GHC.TypeLits (Nat, type (-), type (+), TypeError, ErrorMessage (..))
21
19
22{-
20{-
23 Note [Changing type parameters]
21 Note [Changing type parameters]
@@ -52,16 +50,16 @@ import GHC.TypeLits (Nat, type (-), TypeError, ErrorMessage (..))
52-- application form. In order to distinguish between applications of P and other type constructors, we use a tag, `PTag`
50-- application form. In order to distinguish between applications of P and other type constructors, we use a tag, `PTag`
53-- to fake a type constructor.
51-- to fake a type constructor.
54data PTag = PTag
52data PTag = PTag
55−type family P :: Peano -> k -> PTag -> k
53+type family P :: Nat -> k -> PTag -> k
56
54
57−type Proxied t = Proxied' t 'Z
55+type Proxied t = Proxied' t 0
58
56
59−type family Proxied' (t :: k) (next :: Peano) :: k where
57+type family Proxied' (t :: k) (next :: Nat) :: k where
60− Proxied' (t (a :: j) :: k) next = (Proxied' t ('S next)) (P next a 'PTag)
58+ Proxied' (t (a :: j) :: k) next = (Proxied' t (next + 1)) (P next a 'PTag)
61 Proxied' t _ = t
59 Proxied' t _ = t
62
60
63data Sub where
61data Sub where
64− Sub :: Peano -> k -> Sub
62+ Sub :: Nat -> k -> Sub
65
63
66type family Unify (a :: k) (b :: k) :: [Sub] where
64type family Unify (a :: k) (b :: k) :: [Sub] where
67 Unify (p n _ 'PTag) a' = '[ 'Sub n a']
65 Unify (p n _ 'PTag) a' = '[ 'Sub n a']
@@ -85,26 +83,20 @@ type family Infer (s :: *) (a' :: *) (b :: *) :: * where
85
83
86--------------------------------------------------------------------------------
84--------------------------------------------------------------------------------
87
85
88−data Peano = Z | S Peano
89−
90−type family NatToPeano (n :: Nat) :: Peano where
91− NatToPeano 0 = 'Z
92− NatToPeano n = 'S (NatToPeano (n - 1))
93−
94-- [TODO]: work this out
86-- [TODO]: work this out
95--
87--
96−--type family ArgKind (t :: k) (pos :: Peano) :: * where
88+--type family ArgKind (t :: k) (pos :: Nat) :: * where
97-- ArgKind (t (a :: k)) 'Z = k
89-- ArgKind (t (a :: k)) 'Z = k
98-- ArgKind (t _) ('S pos) = ArgKind t pos
90-- ArgKind (t _) ('S pos) = ArgKind t pos
99--
91--
100−--type family ReplaceArg (t :: k) (pos :: Peano) (to :: ArgKind t pos) :: k where
92+--type family ReplaceArg (t :: k) (pos :: Nat) (to :: ArgKind t pos) :: k where
101-- ReplaceArg (t a) 'Z to = t to
93-- ReplaceArg (t a) 'Z to = t to
102-- ReplaceArg (t a) ('S pos) to = ReplaceArg t pos to a
94-- ReplaceArg (t a) ('S pos) to = ReplaceArg t pos to a
103-- ReplaceArg t _ _ = t
95-- ReplaceArg t _ _ = t
104
96
105−type family ReplaceArg (t :: k) (pos :: Peano) (to :: j) :: k where
97+type family ReplaceArg (t :: k) (pos :: Nat) (to :: j) :: k where
106− ReplaceArg (t a) 'Z to = t to
98+ ReplaceArg (t a) 0 to = t to
107− ReplaceArg (t a) ('S pos) to = ReplaceArg t pos to a
99+ ReplaceArg (t a) pos to = ReplaceArg t (pos - 1) to a
108 ReplaceArg t _ _ = t
100 ReplaceArg t _ _ = t
109
101
110type family ReplaceArgs (t :: k) (subs :: [Sub]) :: k where
102type family ReplaceArgs (t :: k) (subs :: [Sub]) :: k where
src/Data/Generics/Product.hs+2−1
@@ -22,9 +22,10 @@ module Data.Generics.Product
22 , module Data.Generics.Product.Positions
22 , module Data.Generics.Product.Positions
23 , module Data.Generics.Product.Subtype
23 , module Data.Generics.Product.Subtype
24 , module Data.Generics.Product.Typed
24 , module Data.Generics.Product.Typed
25+ , module Data.Generics.Product.List
26+ -- *Traversals
25 , module Data.Generics.Product.Types
27 , module Data.Generics.Product.Types
26 , module Data.Generics.Product.Param
28 , module Data.Generics.Product.Param
27− , module Data.Generics.Product.List
28 ) where
29 ) where
29
30
30import Data.Generics.Product.Any
31import Data.Generics.Product.Any
src/Data/Generics/Product/Param.hs+3−5
@@ -40,13 +40,11 @@ class HasParam (p :: Nat) s t a b | p t a b -> s, p s a b -> t where
40 param :: Applicative g => (a -> g b) -> s -> g t
40 param :: Applicative g => (a -> g b) -> s -> g t
41
41
42instance
42instance
43− ( p ~ NatToPeano n
44− , GenericN s
43+ ( GenericN s
45 , GenericN t
44 , GenericN t
46 -- TODO: merge the old 'Changing' code with 'GenericN'
45 -- TODO: merge the old 'Changing' code with 'GenericN'
47− , '(a', b') ~ '(P p a 'PTag, P p b 'PTag)
46+ , s ~ Infer t (P n b 'PTag) a
48− , s ~ Infer t b' a
49− , t ~ Infer s a' b
47+ , t ~ Infer s (P n a 'PTag) b
50 , GHasParam n (RepN s) (RepN t) a b
48 , GHasParam n (RepN s) (RepN t) a b
51 ) => HasParam n s t a b where
49 ) => HasParam n s t a b where
52
50