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)

-- TODO this could map over multiple matching mods
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

-- TODO this appends the mod if it is missing, while it should prepend it to preserve the order of effects.
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)