module Sqel.Class.Mods where
import Generics.SOP (I (I), NP (Nil, (:*)))
import Prelude hiding (Compose)
import Sqel.Data.Dd (Dd (Dd), DdK (DdK), (:>) ((:>)))
import Sqel.Data.Mods (Mods (Mods), unMods)
class SymNP p ps where
symNP :: p -> NP I ps
instance {-# overlappable #-} (
ps ~ '[p]
) => SymNP p ps where
symNP :: p -> NP I ps
symNP p
p =
forall a. a -> I a
I p
p forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* forall {k} (a :: k -> *). NP a '[]
Nil
instance (
SymNP p1 ps
) => SymNP (p0 :> p1) (p0 : ps) where
symNP :: (p0 :> p1) -> NP I (p0 : ps)
symNP (p0
p0 :> p1
p1) =
forall a. a -> I a
I p0
p0 forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* forall p (ps :: [*]). SymNP p ps => p -> NP I ps
symNP p1
p1
instance SymNP (NP I ps) ps where
symNP :: NP I ps -> NP I ps
symNP = forall a. a -> a
id
symMods ::
SymNP p ps =>
p ->
Mods ps
symMods :: forall p (ps :: [*]). SymNP p ps => p -> Mods ps
symMods p
p =
forall (ps :: [*]). NP I ps -> Mods ps
Mods (forall p (ps :: [*]). SymNP p ps => p -> NP I ps
symNP p
p)
class MapMod' p ps0 ps1 | p ps0 -> ps1 where
mapMod' :: p -> (p -> p) -> Mods ps0 -> Mods ps1
instance MapMod' p (p : ps) (p : ps) where
mapMod' :: p -> (p -> p) -> Mods (p : ps) -> Mods (p : ps)
mapMod' p
_ p -> p
f (Mods (I x
p :* NP I xs
ps)) =
forall (ps :: [*]). NP I ps -> Mods ps
Mods (forall a. a -> I a
I (p -> p
f x
p) forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP I xs
ps)
instance {-# overlappable #-} (
MapMod' p ps0 ps1
) => MapMod' p (a' : ps0) (a' : ps1) where
mapMod' :: p -> (p -> p) -> Mods (a' : ps0) -> Mods (a' : ps1)
mapMod' p
p p -> p
f (Mods (I x
a' :* NP I xs
ps)) =
forall (ps :: [*]). NP I ps -> Mods ps
Mods (I x
a' forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* forall (ps :: [*]). Mods ps -> NP I ps
unMods (forall p (ps0 :: [*]) (ps1 :: [*]).
MapMod' p ps0 ps1 =>
p -> (p -> p) -> Mods ps0 -> Mods ps1
mapMod' p
p p -> p
f (forall (ps :: [*]). NP I ps -> Mods ps
Mods NP I xs
ps)))
instance MapMod' p '[] '[p] where
mapMod' :: p -> (p -> p) -> Mods '[] -> Mods '[p]
mapMod' p
p p -> p
f (Mods NP I '[]
Nil) =
forall (ps :: [*]). NP I ps -> Mods ps
Mods (forall a. a -> I a
I (p -> p
f p
p) forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* forall {k} (a :: k -> *). NP a '[]
Nil)
amendMod' ::
MapMod' p ps0 ps1 =>
p ->
Mods ps0 ->
Mods ps1
amendMod' :: forall p (ps0 :: [*]) (ps1 :: [*]).
MapMod' p ps0 ps1 =>
p -> Mods ps0 -> Mods ps1
amendMod' p
p =
forall p (ps0 :: [*]) (ps1 :: [*]).
MapMod' p ps0 ps1 =>
p -> (p -> p) -> Mods ps0 -> Mods ps1
mapMod' p
p forall a. a -> a
id
setMod' ::
MapMod' p ps0 ps1 =>
p ->
Mods ps0 ->
Mods ps1
setMod' :: forall p (ps0 :: [*]) (ps1 :: [*]).
MapMod' p ps0 ps1 =>
p -> Mods ps0 -> Mods ps1
setMod' p
p =
forall p (ps0 :: [*]) (ps1 :: [*]).
MapMod' p ps0 ps1 =>
p -> (p -> p) -> Mods ps0 -> Mods ps1
mapMod' p
p (forall a b. a -> b -> a
const p
p)
class OverMod' p ps where
overMod' :: (p -> p) -> Mods ps -> Mods ps
instance OverMod' p (p : ps) where
overMod' :: (p -> p) -> Mods (p : ps) -> Mods (p : ps)
overMod' p -> p
f (Mods (I x
p :* NP I xs
ps)) =
forall (ps :: [*]). NP I ps -> Mods ps
Mods (forall a. a -> I a
I (p -> p
f x
p) forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP I xs
ps)
instance (
OverMod' p ps
) => OverMod' p (a' : ps) where
overMod' :: (p -> p) -> Mods (a' : ps) -> Mods (a' : ps)
overMod' p -> p
f (Mods (I x
a' :* NP I xs
ps)) =
forall (ps :: [*]). NP I ps -> Mods ps
Mods (I x
a' forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* forall (ps :: [*]). Mods ps -> NP I ps
unMods (forall p (ps :: [*]).
OverMod' p ps =>
(p -> p) -> Mods ps -> Mods ps
overMod' p -> p
f (forall (ps :: [*]). NP I ps -> Mods ps
Mods NP I xs
ps)))
instance OverMod' p '[] where
overMod' :: (p -> p) -> Mods '[] -> Mods '[]
overMod' p -> p
_ (Mods NP I '[]
Nil) =
forall (ps :: [*]). NP I ps -> Mods ps
Mods forall {k} (a :: k -> *). NP a '[]
Nil
class CMapMod' c p0 p p1 ps0 ps1 | ps0 p0 p1 -> p ps1 where
cmapMod' :: p0 -> (c p p1 => p -> p1) -> Mods ps0 -> Mods ps1
instance (
c p p1
) => CMapMod' c p0 p p1 (p : ps) (p1 : ps) where
cmapMod' :: p0 -> (c p p1 => p -> p1) -> Mods (p : ps) -> Mods (p1 : ps)
cmapMod' p0
_ c p p1 => p -> p1
f (Mods (I x
p :* NP I xs
ps)) =
forall (ps :: [*]). NP I ps -> Mods ps
Mods (forall a. a -> I a
I (c p p1 => p -> p1
f x
p) forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP I xs
ps)
instance (
CMapMod' c p0 p p1 ps0 ps1
) => CMapMod' c p0 p p1 (a' : ps0) (a' : ps1) where
cmapMod' :: p0 -> (c p p1 => p -> p1) -> Mods (a' : ps0) -> Mods (a' : ps1)
cmapMod' p0
p c p p1 => p -> p1
f (Mods (I x
a' :* NP I xs
ps)) =
forall (ps :: [*]). NP I ps -> Mods ps
Mods (I x
a' forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* forall (ps :: [*]). Mods ps -> NP I ps
unMods (forall (c :: * -> * -> Constraint) p0 p p1 (ps0 :: [*])
(ps1 :: [*]).
CMapMod' c p0 p p1 ps0 ps1 =>
p0 -> (c p p1 => p -> p1) -> Mods ps0 -> Mods ps1
cmapMod' @c @p0 @p @p1 @ps0 @ps1 p0
p c p p1 => p -> p1
f (forall (ps :: [*]). NP I ps -> Mods ps
Mods NP I xs
ps)))
instance CMapMod' c p0 p1 p1 '[] '[p0] where
cmapMod' :: p0 -> (c p1 p1 => p1 -> p1) -> Mods '[] -> Mods '[p0]
cmapMod' p0
p c p1 p1 => p1 -> p1
_ (Mods NP I '[]
Nil) =
forall (ps :: [*]). NP I ps -> Mods ps
Mods (forall a. a -> I a
I p0
p forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* forall {k} (a :: k -> *). NP a '[]
Nil)
type GetMod :: Constraint -> Type -> [Type] -> Constraint
class GetMod c p ps where
getMod :: (c => p) -> Mods ps -> p
instance c => GetMod c p '[] where
getMod :: (c => p) -> Mods '[] -> p
getMod c => p
f (Mods NP I '[]
Nil) = c => p
f
instance GetMod c p (p : ps) where
getMod :: (c => p) -> Mods (p : ps) -> p
getMod c => p
_ (Mods (I x
p :* NP I xs
_)) = x
p
class AddMod p s0 s1 | p s0 -> s1 where
addMod :: p -> Dd s0 -> Dd s1
instance AddMod p ('DdK sel ps a s) ('DdK sel (p : ps) a s) where
addMod :: p -> Dd ('DdK sel ps a s) -> Dd ('DdK sel (p : ps) a s)
addMod p
p (Dd SelW sel
sel (Mods NP I mods
ps) DdStruct s1
s) =
forall (sel :: Sel) (mods :: [*]) (s1 :: Struct) a.
SelW sel -> Mods mods -> DdStruct s1 -> Dd ('DdK sel mods a s1)
Dd SelW sel
sel (forall (ps :: [*]). NP I ps -> Mods ps
Mods (forall a. a -> I a
I p
p forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP I mods
ps)) DdStruct s1
s
instance {-# overlappable #-} (
GetMod c p ps
) => GetMod c p (a' : ps) where
getMod :: (c => p) -> Mods (a' : ps) -> p
getMod c => p
f (Mods (I x
_ :* NP I xs
ps)) =
forall (c :: Constraint) p (ps :: [*]).
GetMod c p ps =>
(c => p) -> Mods ps -> p
getMod @c c => p
f (forall (ps :: [*]). NP I ps -> Mods ps
Mods NP I xs
ps)
class MapMod p s0 s1 | p s0 -> s1 where
mapMod :: p -> (p -> p) -> Dd s0 -> Dd s1
instance (
MapMod' p ps0 ps1
) => MapMod p ('DdK sel ps0 a s0) ('DdK sel ps1 a s0) where
mapMod :: p -> (p -> p) -> Dd ('DdK sel ps0 a s0) -> Dd ('DdK sel ps1 a s0)
mapMod p
p p -> p
f (Dd SelW sel
sel Mods mods
ps0 DdStruct s1
s) =
forall (sel :: Sel) (mods :: [*]) (s1 :: Struct) a.
SelW sel -> Mods mods -> DdStruct s1 -> Dd ('DdK sel mods a s1)
Dd SelW sel
sel (forall p (ps0 :: [*]) (ps1 :: [*]).
MapMod' p ps0 ps1 =>
p -> (p -> p) -> Mods ps0 -> Mods ps1
mapMod' p
p p -> p
f Mods mods
ps0) DdStruct s1
s
class OverMod p s where
overMod :: (p -> p) -> Dd s -> Dd s
instance (
OverMod' p ps
) => OverMod p ('DdK sel ps a s0) where
overMod :: (p -> p) -> Dd ('DdK sel ps a s0) -> Dd ('DdK sel ps a s0)
overMod p -> p
f (Dd SelW sel
sel Mods mods
ps DdStruct s1
s) =
forall (sel :: Sel) (mods :: [*]) (s1 :: Struct) a.
SelW sel -> Mods mods -> DdStruct s1 -> Dd ('DdK sel mods a s1)
Dd SelW sel
sel (forall p (ps :: [*]).
OverMod' p ps =>
(p -> p) -> Mods ps -> Mods ps
overMod' p -> p
f Mods mods
ps) DdStruct s1
s
class CMapMod c p0 p p1 s0 s1 | s0 p0 p1 -> p s1 where
cmapMod :: p0 -> (c p p1 => p -> p1) -> Dd s0 -> Dd s1
instance (
CMapMod' c p0 p p1 ps0 ps1
) => CMapMod c p0 p p1 ('DdK sel ps0 a s0) ('DdK sel ps1 a s0) where
cmapMod :: p0
-> (c p p1 => p -> p1)
-> Dd ('DdK sel ps0 a s0)
-> Dd ('DdK sel ps1 a s0)
cmapMod p0
p0 c p p1 => p -> p1
f (Dd SelW sel
sel Mods mods
ps0 DdStruct s1
s) =
forall (sel :: Sel) (mods :: [*]) (s1 :: Struct) a.
SelW sel -> Mods mods -> DdStruct s1 -> Dd ('DdK sel mods a s1)
Dd SelW sel
sel (forall (c :: * -> * -> Constraint) p0 p p1 (ps0 :: [*])
(ps1 :: [*]).
CMapMod' c p0 p p1 ps0 ps1 =>
p0 -> (c p p1 => p -> p1) -> Mods ps0 -> Mods ps1
cmapMod' @c @_ @_ @p1 p0
p0 c p p1 => p -> p1
f Mods mods
ps0) DdStruct s1
s
amendMod ::
MapMod p s0 s1 =>
p ->
Dd s0 ->
Dd s1
amendMod :: forall p (s0 :: DdK) (s1 :: DdK).
MapMod p s0 s1 =>
p -> Dd s0 -> Dd s1
amendMod p
p =
forall p (s0 :: DdK) (s1 :: DdK).
MapMod p s0 s1 =>
p -> (p -> p) -> Dd s0 -> Dd s1
mapMod p
p forall a. a -> a
id
setMod ::
MapMod p s0 s1 =>
p ->
Dd s0 ->
Dd s1
setMod :: forall p (s0 :: DdK) (s1 :: DdK).
MapMod p s0 s1 =>
p -> Dd s0 -> Dd s1
setMod p
p =
forall p (s0 :: DdK) (s1 :: DdK).
MapMod p s0 s1 =>
p -> (p -> p) -> Dd s0 -> Dd s1
mapMod p
p (forall a b. a -> b -> a
const p
p)
type OptMod :: Type -> [Type] -> Type -> Constraint
class OptMod p ps res | ps p -> res where
optMod :: Mods ps -> res
instance OptMod p '[] () where
optMod :: Mods '[] -> ()
optMod (Mods NP I '[]
Nil) = ()
instance OptMod p (p : ps) p where
optMod :: Mods (p : ps) -> p
optMod (Mods (I x
p :* NP I xs
_)) = x
p
instance {-# overlappable #-} (
OptMod p ps p1
) => OptMod p (p0 : ps) p1 where
optMod :: Mods (p0 : ps) -> p1
optMod (Mods (I x
_ :* NP I xs
ps)) = forall p (ps :: [*]) res. OptMod p ps res => Mods ps -> res
optMod @p (forall (ps :: [*]). NP I ps -> Mods ps
Mods NP I xs
ps)
type MaybeMod :: Type -> [Type] -> Constraint
class MaybeMod p ps where
maybeMod :: Mods ps -> Maybe p
instance MaybeMod p '[] where
maybeMod :: Mods '[] -> Maybe p
maybeMod (Mods NP I '[]
Nil) = forall a. Maybe a
Nothing
instance MaybeMod p (p : ps) where
maybeMod :: Mods (p : ps) -> Maybe p
maybeMod (Mods (I x
p :* NP I xs
_)) = forall a. a -> Maybe a
Just x
p
instance {-# overlappable #-} (
MaybeMod p ps
) => MaybeMod p (p0 : ps) where
maybeMod :: Mods (p0 : ps) -> Maybe p
maybeMod (Mods (I x
_ :* NP I xs
ps)) = forall p (ps :: [*]). MaybeMod p ps => Mods ps -> Maybe p
maybeMod @p (forall (ps :: [*]). NP I ps -> Mods ps
Mods NP I xs
ps)