{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

-- | Intended for qualified import
--
-- > import           Data.SOP.InPairs (InPairs(..))
-- > import qualified Data.SOP.InPairs as InPairs
module Data.SOP.InPairs (
    -- * InPairs
    InPairs (..)
    -- * Convenience constructors
  , mk1
  , mk2
  , mk3
    -- * SOP-like operators
  , hcmap
  , hcpure
  , hczipWith
  , hmap
  , hpure
    -- * Requiring
  , Requiring (..)
  , RequiringBoth (..)
  , ignoring
  , ignoringBoth
  , requiring
  , requiringBoth
  ) where

import           Data.Kind (Type)
import           Data.Proxy
import           Data.SOP.Constraint
import           Data.SOP.NonEmpty
import           Data.SOP.Sing
import           Data.SOP.Strict hiding (hcmap, hcpure, hczipWith, hmap, hpure)

{-------------------------------------------------------------------------------
  InPairs
-------------------------------------------------------------------------------}

-- | We have an @f x y@ for each pair @(x, y)@ of successive list elements
type InPairs :: (k -> k -> Type) -> [k] -> Type
data InPairs f xs where
  PNil  :: InPairs f '[x]
  PCons :: f x y -> InPairs f (y ': zs) -> InPairs f (x ': y ': zs)

{-------------------------------------------------------------------------------
  Convenience constructors
-------------------------------------------------------------------------------}

mk1 :: InPairs f '[x]
mk1 :: forall {k} (f :: k -> k -> *) (x :: k). InPairs f '[x]
mk1 = InPairs f '[x]
forall {k} (f :: k -> k -> *) (x :: k). InPairs f '[x]
PNil

mk2 :: f x y -> InPairs f '[x, y]
mk2 :: forall {k} (f :: k -> k -> *) (x :: k) (y :: k).
f x y -> InPairs f '[x, y]
mk2 f x y
xy = f x y -> InPairs f '[y] -> InPairs f '[x, y]
forall {a} (f :: a -> a -> *) (x :: a) (y :: a) (zs :: [a]).
f x y -> InPairs f (y : zs) -> InPairs f (x : y : zs)
PCons f x y
xy InPairs f '[y]
forall {k} (f :: k -> k -> *) (x :: k). InPairs f '[x]
mk1

mk3 :: f x y -> f y z -> InPairs f '[x, y, z]
mk3 :: forall {k} (f :: k -> k -> *) (x :: k) (y :: k) (z :: k).
f x y -> f y z -> InPairs f '[x, y, z]
mk3 f x y
xy f y z
yz = f x y -> InPairs f '[y, z] -> InPairs f '[x, y, z]
forall {a} (f :: a -> a -> *) (x :: a) (y :: a) (zs :: [a]).
f x y -> InPairs f (y : zs) -> InPairs f (x : y : zs)
PCons f x y
xy (f y z -> InPairs f '[y, z]
forall {k} (f :: k -> k -> *) (x :: k) (y :: k).
f x y -> InPairs f '[x, y]
mk2 f y z
yz)

{-------------------------------------------------------------------------------
  SOP-like operators
-------------------------------------------------------------------------------}

hmap :: SListI xs => (forall x y. f x y -> g x y) -> InPairs f xs -> InPairs g xs
hmap :: forall {k} (xs :: [k]) (f :: k -> k -> *) (g :: k -> k -> *).
SListI xs =>
(forall (x :: k) (y :: k). f x y -> g x y)
-> InPairs f xs -> InPairs g xs
hmap = Proxy Top
-> (forall (x :: k) (y :: k). (Top x, Top y) => f x y -> g x y)
-> InPairs f xs
-> InPairs g xs
forall {k} (proxy :: (k -> Constraint) -> *) (c :: k -> Constraint)
       (f :: k -> k -> *) (g :: k -> k -> *) (xs :: [k]).
All c xs =>
proxy c
-> (forall (x :: k) (y :: k). (c x, c y) => f x y -> g x y)
-> InPairs f xs
-> InPairs g xs
hcmap (forall {k} (t :: k). Proxy t
forall (t :: k -> Constraint). Proxy t
Proxy @Top)

hcmap :: forall proxy c f g xs. All c xs
      => proxy c
      -> (forall x y. (c x, c y) => f x y -> g x y)
      -> InPairs f xs -> InPairs g xs
hcmap :: forall {k} (proxy :: (k -> Constraint) -> *) (c :: k -> Constraint)
       (f :: k -> k -> *) (g :: k -> k -> *) (xs :: [k]).
All c xs =>
proxy c
-> (forall (x :: k) (y :: k). (c x, c y) => f x y -> g x y)
-> InPairs f xs
-> InPairs g xs
hcmap proxy c
_ forall (x :: k) (y :: k). (c x, c y) => f x y -> g x y
f = InPairs f xs -> InPairs g xs
forall (xs' :: [k]). All c xs' => InPairs f xs' -> InPairs g xs'
go
  where
    go :: All c xs' => InPairs f xs' -> InPairs g xs'
    go :: forall (xs' :: [k]). All c xs' => InPairs f xs' -> InPairs g xs'
go InPairs f xs'
PNil         = InPairs g xs'
InPairs g '[x]
forall {k} (f :: k -> k -> *) (x :: k). InPairs f '[x]
PNil
    go (PCons f x y
x InPairs f (y : zs)
xs) = g x y -> InPairs g (y : zs) -> InPairs g (x : y : zs)
forall {a} (f :: a -> a -> *) (x :: a) (y :: a) (zs :: [a]).
f x y -> InPairs f (y : zs) -> InPairs f (x : y : zs)
PCons (f x y -> g x y
forall (x :: k) (y :: k). (c x, c y) => f x y -> g x y
f f x y
x) (InPairs f (y : zs) -> InPairs g (y : zs)
forall (xs' :: [k]). All c xs' => InPairs f xs' -> InPairs g xs'
go InPairs f (y : zs)
xs)

hpure :: (SListI xs, IsNonEmpty xs) => (forall x y. f x y) -> InPairs f xs
hpure :: forall {k} (xs :: [k]) (f :: k -> k -> *).
(SListI xs, IsNonEmpty xs) =>
(forall (x :: k) (y :: k). f x y) -> InPairs f xs
hpure = Proxy Top
-> (forall (x :: k) (y :: k). (Top x, Top y) => f x y)
-> InPairs f xs
forall {k} (proxy :: (k -> Constraint) -> *) (c :: k -> Constraint)
       (xs :: [k]) (f :: k -> k -> *).
(All c xs, IsNonEmpty xs) =>
proxy c
-> (forall (x :: k) (y :: k). (c x, c y) => f x y) -> InPairs f xs
hcpure (forall {k} (t :: k). Proxy t
forall (t :: k -> Constraint). Proxy t
Proxy @Top)

hcpure :: forall proxy c xs f. (All c xs, IsNonEmpty xs)
       => proxy c
       -> (forall x y. (c x, c y) => f x y) -> InPairs f xs
hcpure :: forall {k} (proxy :: (k -> Constraint) -> *) (c :: k -> Constraint)
       (xs :: [k]) (f :: k -> k -> *).
(All c xs, IsNonEmpty xs) =>
proxy c
-> (forall (x :: k) (y :: k). (c x, c y) => f x y) -> InPairs f xs
hcpure proxy c
_ forall (x :: k) (y :: k). (c x, c y) => f x y
f =
    case Proxy xs -> ProofNonEmpty xs
forall {a} (xs :: [a]) (proxy :: [a] -> *).
IsNonEmpty xs =>
proxy xs -> ProofNonEmpty xs
forall (proxy :: [k] -> *). proxy xs -> ProofNonEmpty xs
isNonEmpty (forall (t :: [k]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs) of
      ProofNonEmpty {} -> SList xs1 -> InPairs f (x : xs1)
forall (x :: k) (xs' :: [k]).
(c x, All c xs') =>
SList xs' -> InPairs f (x : xs')
go SList xs1
forall {k} (xs :: [k]). SListI xs => SList xs
sList
  where
    go :: (c x, All c xs') => SList xs' -> InPairs f (x ': xs')
    go :: forall (x :: k) (xs' :: [k]).
(c x, All c xs') =>
SList xs' -> InPairs f (x : xs')
go SList xs'
SNil  = InPairs f (x : xs')
InPairs f '[x]
forall {k} (f :: k -> k -> *) (x :: k). InPairs f '[x]
PNil
    go SList xs'
SCons = f x x -> InPairs f (x : xs) -> InPairs f (x : x : xs)
forall {a} (f :: a -> a -> *) (x :: a) (y :: a) (zs :: [a]).
f x y -> InPairs f (y : zs) -> InPairs f (x : y : zs)
PCons f x x
forall (x :: k) (y :: k). (c x, c y) => f x y
f (SList xs -> InPairs f (x : xs)
forall (x :: k) (xs' :: [k]).
(c x, All c xs') =>
SList xs' -> InPairs f (x : xs')
go SList xs
forall {k} (xs :: [k]). SListI xs => SList xs
sList)

hczipWith ::
     forall proxy c f f' f'' xs. All c xs
  => proxy c
  -> (forall x y. (c x, c y) => f x y -> f' x y -> f'' x y)
  -> InPairs f   xs
  -> InPairs f'  xs
  -> InPairs f'' xs
hczipWith :: forall {k} (proxy :: (k -> Constraint) -> *) (c :: k -> Constraint)
       (f :: k -> k -> *) (f' :: k -> k -> *) (f'' :: k -> k -> *)
       (xs :: [k]).
All c xs =>
proxy c
-> (forall (x :: k) (y :: k).
    (c x, c y) =>
    f x y -> f' x y -> f'' x y)
-> InPairs f xs
-> InPairs f' xs
-> InPairs f'' xs
hczipWith proxy c
_ forall (x :: k) (y :: k). (c x, c y) => f x y -> f' x y -> f'' x y
f = InPairs f xs -> InPairs f' xs -> InPairs f'' xs
forall (xs' :: [k]).
All c xs' =>
InPairs f xs' -> InPairs f' xs' -> InPairs f'' xs'
go
  where
    go :: All c xs' => InPairs f xs' -> InPairs f' xs' -> InPairs f'' xs'
    go :: forall (xs' :: [k]).
All c xs' =>
InPairs f xs' -> InPairs f' xs' -> InPairs f'' xs'
go InPairs f xs'
PNil InPairs f' xs'
PNil                 = InPairs f'' xs'
InPairs f'' '[x]
forall {k} (f :: k -> k -> *) (x :: k). InPairs f '[x]
PNil
    go (PCons f x y
x InPairs f (y : zs)
xs) (PCons f' x y
y InPairs f' (y : zs)
ys) = f'' x y -> InPairs f'' (y : zs) -> InPairs f'' (x : y : zs)
forall {a} (f :: a -> a -> *) (x :: a) (y :: a) (zs :: [a]).
f x y -> InPairs f (y : zs) -> InPairs f (x : y : zs)
PCons (f x y -> f' x y -> f'' x y
forall (x :: k) (y :: k). (c x, c y) => f x y -> f' x y -> f'' x y
f f x y
x f' x y
f' x y
y) (InPairs f (y : zs) -> InPairs f' (y : zs) -> InPairs f'' (y : zs)
forall (xs' :: [k]).
All c xs' =>
InPairs f xs' -> InPairs f' xs' -> InPairs f'' xs'
go InPairs f (y : zs)
xs InPairs f' (y : zs)
InPairs f' (y : zs)
ys)

{-------------------------------------------------------------------------------
  RequiringBoth
-------------------------------------------------------------------------------}

newtype Requiring h f x y = Require {
      forall {k} {k} (h :: k -> *) (f :: k -> k -> *) (x :: k) (y :: k).
Requiring h f x y -> h x -> f x y
provide :: h x -> f x y
    }

newtype RequiringBoth h f x y = RequireBoth {
      forall {k} (h :: k -> *) (f :: k -> k -> *) (x :: k) (y :: k).
RequiringBoth h f x y -> h x -> h y -> f x y
provideBoth :: h x -> h y -> f x y
    }

ignoring :: f x y -> Requiring h f x y
ignoring :: forall {k} {k} (f :: k -> k -> *) (x :: k) (y :: k) (h :: k -> *).
f x y -> Requiring h f x y
ignoring f x y
fxy = (h x -> f x y) -> Requiring h f x y
forall {k} {k} (h :: k -> *) (f :: k -> k -> *) (x :: k) (y :: k).
(h x -> f x y) -> Requiring h f x y
Require ((h x -> f x y) -> Requiring h f x y)
-> (h x -> f x y) -> Requiring h f x y
forall a b. (a -> b) -> a -> b
$ f x y -> h x -> f x y
forall a b. a -> b -> a
const f x y
fxy

ignoringBoth :: f x y -> RequiringBoth h f x y
ignoringBoth :: forall {k} (f :: k -> k -> *) (x :: k) (y :: k) (h :: k -> *).
f x y -> RequiringBoth h f x y
ignoringBoth f x y
fxy = (h x -> h y -> f x y) -> RequiringBoth h f x y
forall {k} (h :: k -> *) (f :: k -> k -> *) (x :: k) (y :: k).
(h x -> h y -> f x y) -> RequiringBoth h f x y
RequireBoth ((h x -> h y -> f x y) -> RequiringBoth h f x y)
-> (h x -> h y -> f x y) -> RequiringBoth h f x y
forall a b. (a -> b) -> a -> b
$ \h x
_ h y
_ -> f x y
fxy

requiring :: SListI xs => NP h xs -> InPairs (Requiring h f) xs -> InPairs f xs
requiring :: forall {k} (xs :: [k]) (h :: k -> *) (f :: k -> k -> *).
SListI xs =>
NP h xs -> InPairs (Requiring h f) xs -> InPairs f xs
requiring NP h xs
np =
      NP h xs -> InPairs (RequiringBoth h f) xs -> InPairs f xs
forall {k} (h :: k -> *) (xs :: [k]) (f :: k -> k -> *).
NP h xs -> InPairs (RequiringBoth h f) xs -> InPairs f xs
requiringBoth NP h xs
np
    (InPairs (RequiringBoth h f) xs -> InPairs f xs)
-> (InPairs (Requiring h f) xs -> InPairs (RequiringBoth h f) xs)
-> InPairs (Requiring h f) xs
-> InPairs f xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (x :: k) (y :: k).
 Requiring h f x y -> RequiringBoth h f x y)
-> InPairs (Requiring h f) xs -> InPairs (RequiringBoth h f) xs
forall {k} (xs :: [k]) (f :: k -> k -> *) (g :: k -> k -> *).
SListI xs =>
(forall (x :: k) (y :: k). f x y -> g x y)
-> InPairs f xs -> InPairs g xs
hmap (\Requiring h f x y
f -> (h x -> h y -> f x y) -> RequiringBoth h f x y
forall {k} (h :: k -> *) (f :: k -> k -> *) (x :: k) (y :: k).
(h x -> h y -> f x y) -> RequiringBoth h f x y
RequireBoth ((h x -> h y -> f x y) -> RequiringBoth h f x y)
-> (h x -> h y -> f x y) -> RequiringBoth h f x y
forall a b. (a -> b) -> a -> b
$ \h x
hx h y
_hy -> Requiring h f x y -> h x -> f x y
forall {k} {k} (h :: k -> *) (f :: k -> k -> *) (x :: k) (y :: k).
Requiring h f x y -> h x -> f x y
provide Requiring h f x y
f h x
hx)

requiringBoth :: NP h xs -> InPairs (RequiringBoth h f) xs -> InPairs f xs
requiringBoth :: forall {k} (h :: k -> *) (xs :: [k]) (f :: k -> k -> *).
NP h xs -> InPairs (RequiringBoth h f) xs -> InPairs f xs
requiringBoth = (InPairs (RequiringBoth h f) xs -> NP h xs -> InPairs f xs)
-> NP h xs -> InPairs (RequiringBoth h f) xs -> InPairs f xs
forall a b c. (a -> b -> c) -> b -> a -> c
flip InPairs (RequiringBoth h f) xs -> NP h xs -> InPairs f xs
forall {k} (h :: k -> *) (f :: k -> k -> *) (xs :: [k]).
InPairs (RequiringBoth h f) xs -> NP h xs -> InPairs f xs
go
  where
    go :: InPairs (RequiringBoth h f) xs -> NP h xs -> InPairs f xs
    go :: forall {k} (h :: k -> *) (f :: k -> k -> *) (xs :: [k]).
InPairs (RequiringBoth h f) xs -> NP h xs -> InPairs f xs
go InPairs (RequiringBoth h f) xs
PNil         NP h xs
_              = InPairs f xs
InPairs f '[x]
forall {k} (f :: k -> k -> *) (x :: k). InPairs f '[x]
PNil
    go (PCons RequiringBoth h f x y
f InPairs (RequiringBoth h f) (y : zs)
fs) (h x
x :* h x
y :* NP h xs1
zs) = f x y -> InPairs f (y : zs) -> InPairs f (x : y : zs)
forall {a} (f :: a -> a -> *) (x :: a) (y :: a) (zs :: [a]).
f x y -> InPairs f (y : zs) -> InPairs f (x : y : zs)
PCons (RequiringBoth h f x y -> h x -> h y -> f x y
forall {k} (h :: k -> *) (f :: k -> k -> *) (x :: k) (y :: k).
RequiringBoth h f x y -> h x -> h y -> f x y
provideBoth RequiringBoth h f x y
f h x
h x
x h y
h x
y) (InPairs (RequiringBoth h f) (y : zs)
-> NP h (y : zs) -> InPairs f (y : zs)
forall {k} (h :: k -> *) (f :: k -> k -> *) (xs :: [k]).
InPairs (RequiringBoth h f) xs -> NP h xs -> InPairs f xs
go InPairs (RequiringBoth h f) (y : zs)
fs (h y
h x
y h y -> NP h zs -> NP h (y : zs)
forall {k} (f :: k -> *) (x :: k) (xs1 :: [k]).
f x -> NP f xs1 -> NP f (x : xs1)
:* NP h zs
NP h xs1
zs))