mirror of
https://github.com/i-am-tom/higgledy.git
synced 2024-09-11 16:16:43 +03:00
Use generic-lens for position and field lenses
Why get a dog and bark yourself? This commit uses the generic-lens internal functions to create the lenses, which means the error messages will be substantially better.
This commit is contained in:
parent
b1313d91d2
commit
99a9585284
@ -30,6 +30,7 @@ import Data.Void (Void)
|
||||
import Data.Partial.Types (Partial (..), Partial_)
|
||||
import GHC.Generics
|
||||
import GHC.TypeLits (ErrorMessage (..), Symbol, TypeError)
|
||||
import qualified Data.Generics.Internal.VL.Lens as G
|
||||
import qualified Data.GenericLens.Internal as G
|
||||
|
||||
-- | A la @generic-lens@, we are able to focus on a particular field within our
|
||||
@ -56,18 +57,13 @@ import qualified Data.GenericLens.Internal as G
|
||||
-- ...
|
||||
class HasField' (field :: Symbol) (structure :: Type) (focus :: Type)
|
||||
| field structure -> focus where
|
||||
field :: Lens' (Partial structure) (Maybe focus)
|
||||
field :: Lens' (Partial structure) (Last focus)
|
||||
|
||||
data FieldPredicate :: Symbol -> G.TyFun (Type -> Type) (Maybe Type)
|
||||
type instance G.Eval (FieldPredicate sym) tt = G.HasTotalFieldP sym tt
|
||||
|
||||
instance G.GLens' (FieldPredicate field) (Partial_ structure) (Maybe focus)
|
||||
instance G.GLens' (FieldPredicate field) (Partial_ structure) (Last focus)
|
||||
=> HasField' field structure focus where
|
||||
field = go . into
|
||||
where
|
||||
go :: Lens' (Partial structure) (Partial_ structure Void)
|
||||
go f = fmap Partial . f . runPartial
|
||||
|
||||
into :: Lens' (Partial_ structure Void) (Maybe focus)
|
||||
into = G.glens @(FieldPredicate field)
|
||||
field = go . G.ravel (G.glens @(FieldPredicate field))
|
||||
where go f = fmap Partial . f . runPartial
|
||||
|
||||
|
@ -29,6 +29,8 @@ import Data.Monoid (Last (..))
|
||||
import Data.Partial.Types (Partial (..), Partial_)
|
||||
import GHC.Generics
|
||||
import GHC.TypeLits (ErrorMessage (..), Nat, TypeError, type (<=?), type (+), type (-))
|
||||
import qualified Data.GenericLens.Internal as G
|
||||
import qualified Data.Generics.Internal.VL.Lens as G
|
||||
|
||||
-- | Taking another cue from @generic-lens@, we can lens into partial product
|
||||
-- types whose fields /aren't/ named using a positional index.
|
||||
@ -50,89 +52,13 @@ import GHC.TypeLits (ErrorMessage (..), Nat, TypeError, type (<=?), type (+), ty
|
||||
-- ...
|
||||
class HasPosition' (index :: Nat) (structure :: Type) (focus :: Type)
|
||||
| index structure -> focus where
|
||||
position :: Lens' (Partial structure) (Maybe focus)
|
||||
position :: Lens' (Partial structure) (Last focus)
|
||||
|
||||
-------------------------------------------------------------------------------
|
||||
data PositionPredicate :: Nat -> G.TyFun (Type -> Type) (Maybe Type)
|
||||
type instance G.Eval (PositionPredicate sym) tt = G.HasTotalPositionP sym tt
|
||||
|
||||
type family Position (index :: Nat) (rep :: Type -> Type) :: Maybe Type where
|
||||
Position 1 (K1 _ (Last x)) = 'Just x
|
||||
Position _ (K1 _ _ ) = 'Nothing
|
||||
|
||||
Position n (M1 _ _ x)
|
||||
= Position n x
|
||||
|
||||
Position n (l :*: r)
|
||||
= Position_ (n <=? Count l) n l r
|
||||
|
||||
type family Count (rep :: Type -> Type) :: Nat where
|
||||
Count (left :*: right) = Count left + Count right
|
||||
Count _ = 1
|
||||
|
||||
type family Position_
|
||||
(isLeft :: Bool)
|
||||
(count :: Nat)
|
||||
(left :: Type -> Type)
|
||||
(right :: Type -> Type) :: Maybe Type
|
||||
where
|
||||
Position_ 'True count left _
|
||||
= Position count left
|
||||
|
||||
Position_ 'False count left right
|
||||
= Position (count - Count left) right
|
||||
|
||||
class GHasPosition' (index :: Nat) (rep :: Type -> Type) (focus :: Type)
|
||||
| index rep -> focus where
|
||||
gposition :: Lens' (rep p) (Maybe focus)
|
||||
|
||||
instance GHasPosition' count inner focus
|
||||
=> GHasPosition' count (M1 index meta inner) focus where
|
||||
gposition = dimap unM1 (fmap M1) . gposition @count
|
||||
|
||||
class GHasPositionProduct
|
||||
(goal :: Maybe Type)
|
||||
(count :: Nat)
|
||||
(rep :: Type -> Type)
|
||||
(focus :: Type)
|
||||
| count rep -> focus where
|
||||
gpositionProduct :: Lens' (rep p) (Maybe focus)
|
||||
|
||||
instance GHasPositionProduct (Position count left) count (left :*: right) focus
|
||||
=> GHasPosition' count (left :*: right) focus where
|
||||
gposition = gpositionProduct @(Position count left) @count
|
||||
|
||||
instance (GHasPosition' count left focus, any ~ focus)
|
||||
=> GHasPositionProduct ('Just any) count (left :*: right) focus where
|
||||
gpositionProduct = go . gposition @count
|
||||
where go f (left :*: right) = fmap (:*: right) (f left)
|
||||
|
||||
instance (GHasPosition' (count - Count left) right focus)
|
||||
=> GHasPositionProduct 'Nothing count (left :*: right) focus where
|
||||
gpositionProduct = go . gposition @(count - Count left)
|
||||
where go f (left :*: right) = fmap (left :*:) (f right)
|
||||
|
||||
instance any ~ focus => GHasPosition' 1 (K1 index (Last any)) focus where
|
||||
gposition = dimap (getLast . unK1) (fmap (K1 . Last))
|
||||
|
||||
type HasPosition_ (position :: Nat) (structure :: Type)
|
||||
= AssertHasPosition position structure (Position position (Partial_ structure))
|
||||
|
||||
type family AssertHasPosition
|
||||
(position :: Nat)
|
||||
(structure :: Type)
|
||||
(goal :: Maybe Type) where
|
||||
AssertHasPosition _ _ ('Just xs) = xs
|
||||
AssertHasPosition position structure 'Nothing = TypeError
|
||||
( 'ShowType structure
|
||||
':<>: 'Text " has no position #"
|
||||
':<>: 'ShowType position
|
||||
':<>: 'Text "!"
|
||||
)
|
||||
|
||||
instance
|
||||
( Generic structure
|
||||
, GHasPosition' index (Partial_ structure) focus
|
||||
, HasPosition_ index structure ~ focus
|
||||
)
|
||||
instance G.GLens' (PositionPredicate index) (Partial_ structure) (Last focus)
|
||||
=> HasPosition' index structure focus where
|
||||
position = dimap runPartial (fmap Partial) . gposition @index
|
||||
position = go . G.ravel (G.glens @(PositionPredicate index))
|
||||
where go f = fmap Partial . f . runPartial
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user