@@ -81,51 +81,24 @@ type BaseIndex = 1
8181-- positional field.
8282instance
8383 ( Generic s
84− , ContainsAt BaseIndex index (Rep s) ~ 'True -- this is needed for the fundep
8584 , GHasFieldAt BaseIndex index (Rep s) a
8685 ) => HasFieldAt index a s where
8786 itemAt = repIso . gItemAt @BaseIndex @index
8887
89−data Choice = GoLeft | GoRight
88+--------------------------------------------------------------------------------
89+type family Not (b :: Bool) where
90+ Not 'True = 'False
91+ Not 'False = 'True
9092
91−class GHasFieldAtProd offset index a b ret (w :: Choice) | offset index a b w -> ret where
92− prodItemAt :: Lens' ((a :*: b) x) ret
93+type family (<) (x :: Nat) (y :: Nat) :: Bool where
94+ x < y = Not (y <=? x)
9395
94−instance (GHasFieldAt offset index f ret) => GHasFieldAtProd offset index f g ret 'GoLeft where
95− prodItemAt = first . gItemAt @offset @index
96+type family If (c :: Bool) (x :: k) (y :: k) :: k where
97+ If 'True x _ = x
98+ If 'False _ y = y
9699
97−instance (GHasFieldAt offset index g ret) => GHasFieldAtProd offset index f g ret 'GoRight where
98− prodItemAt = second . gItemAt @offset @index
99−
100−--------------------------------------------------------------------------------
101−
102−type family Search offset index f g :: Choice where
103− Search offset index f g = Choose (ContainsAt offset index f) (ContainsAt (offset + Size f) index g)
104−
105−type family Choose f g :: Choice where
106− Choose 'True _ = 'GoLeft
107− Choose _ 'True = 'GoRight
108− Choose _ _ = TypeError ('Text "Could not find type")
109−
110−-- | Try find a field by position in the generic representation.
111−type family ContainsAt (offset :: Nat) (index :: Nat) f :: Bool where
112− ContainsAt offset index (D1 m f)
113− = ContainsAt offset index f
114− ContainsAt n n (S1 _ _)
115− = 'True
116− ContainsAt _ _ (S1 _ _)
117− = 'False
118− ContainsAt offset index (f :*: g)
119− = ContainsAt offset index f || ContainsAt (Size f + offset) index g
120− ContainsAt offset index (C1 m f)
121− = ContainsAt offset index f
122− ContainsAt offset index (Rec0 _)
123− = 'False
124− ContainsAt offset index U1
125− = 'False
126− ContainsAt offset index V1
127− = 'False
128− ContainsAt offset index t = TypeError ('ShowType offset ':<>: 'Text " " ':<>: 'ShowType index)
100+type family Min (a :: Nat) (b :: Nat) :: Nat where
101+ Min a b = If (a < b) a b
129102
130103-- | Returns the count of terminal nodes in the generic representation.
131104type family Size f :: Nat where
@@ -133,35 +106,62 @@ type family Size f :: Nat where
133106 = Size f
134107 Size (f :*: g)
135108 = Size f + Size g
109+ Size (f :+: g)
110+ = Min (Size f) (Size g)
136111 Size (C1 m f)
137112 = Size f
138113 Size t = 1
139114
115+
116+data Choice = GoLeft | GoRight
117+
118+type family Search offset index f g :: Choice where
119+ Search offset index f g =
120+ If (index < offset)
121+ (TypeError ('Text "Type does not have specified field."))
122+ (If (index < (Size f + offset))
123+ 'GoLeft
124+ (If (index < (Size f + Size g + offset))
125+ 'GoRight
126+ (TypeError ('Text "Type does not have specified field."))))
127+
140128-- | If traversing to the left, offset does not change.
141129-- If traversing to the right, offset is incremented by size of left subtree.
142−type family Offset (offset :: Nat) (choice :: Choice) (size :: Nat) :: Nat where
143− Offset n 'GoLeft _ = n
144− Offset n 'GoRight s = n + s
145−
146−-- | Type-level or
147−type family (a :: Bool) || (b :: Bool) :: Bool where
148− 'True || _ = 'True
149− _ || b = b
130+type family NewOffset (offset :: Nat) (choice :: Choice) (size :: Nat) :: Nat where
131+ NewOffset n 'GoLeft _ = n
132+ NewOffset n 'GoRight s = n + s
150133
151134--------------------------------------------------------------------------------
152135
136+class GHasFieldAtProd offset index a b ret (w :: Choice) | offset index a b w -> ret where
137+ prodItemAt :: Lens' ((a :*: b) x) ret
138+
139+instance (GHasFieldAt offset index f ret) => GHasFieldAtProd offset index f g ret 'GoLeft where
140+ prodItemAt = first . gItemAt @offset @index
141+
142+instance (GHasFieldAt offset index g ret) => GHasFieldAtProd offset index f g ret 'GoRight where
143+ prodItemAt = second . gItemAt @offset @index
144+
145+
153146-- | Like 'HasFieldAt', but on the generic representation
154147class GHasFieldAt (offset :: Nat) (index :: Nat) (s :: Type -> Type) a | offset index s -> a where
155148 gItemAt :: Lens' (s x) a
156149
157150instance
158151 ( choice ~ (Search offset index s s')
159− , offset' ~ Offset offset choice (Size s)
160− , GHasFieldAtProd offset' index s s' a choice
161− )
152+ , offset' ~ NewOffset offset choice (Size s)
153+ , GHasFieldAtProd offset' index s s' a choice
154+ )
162155 => GHasFieldAt offset index (s :*: s') a where
163156 gItemAt = prodItemAt @offset' @index @_ @_ @_ @choice
164157
158+instance
159+ ( GHasFieldAt offset index s a
160+ , GHasFieldAt offset index s' a
161+ )
162+ => GHasFieldAt offset index (s :+: s') a where
163+ gItemAt = combine (gItemAt @offset @index @s) (gItemAt @offset @index @s')
164+
165165instance GHasFieldAt offset index (K1 R a) a where
166166 gItemAt f (K1 x) = fmap K1 (f x)
167167