{-# 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.Tails (Tails(..))
-- > import qualified Data.SOP.Tails as Tails
module Data.SOP.Tails (
    Tails (..)
    -- * Convenience constructors
  , mk1
  , mk2
  , mk3
    -- * SOP-like operators
  , extendWithTails
  , hcmap
  , hcpure
  , hmap
  , hpure
  , inPairsToTails
  ) where

import           Data.Kind (Type)
import           Data.Proxy
import           Data.SOP.Constraint
import           Data.SOP.Index
import qualified Data.SOP.InPairs as InPairs
import           Data.SOP.Sing
import           Data.SOP.Strict hiding (hcmap, hcpure, hmap, hpure)
import qualified Data.SOP.Strict as SOP

{-------------------------------------------------------------------------------
  Tails
-------------------------------------------------------------------------------}

-- | For every tail @(x ': xs)@ of the list, an @f x y@ for every @y@ in @xs@
type Tails :: (k -> k -> Type) -> [k] -> Type
data Tails f xs where
  TNil  :: Tails f '[]
  TCons :: NP (f x) xs -> Tails f xs -> Tails f (x ': xs)

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

mk1 :: Tails f '[x]
mk1 :: forall {k} (f :: k -> k -> *) (x :: k). Tails f '[x]
mk1 = NP (f x) '[] -> Tails f '[] -> Tails f '[x]
forall {k} (f :: k -> k -> *) (x :: k) (xs :: [k]).
NP (f x) xs -> Tails f xs -> Tails f (x : xs)
TCons NP (f x) '[]
forall {k} (f :: k -> *). NP f '[]
Nil Tails f '[]
forall {k} (f :: k -> k -> *). Tails f '[]
TNil

mk2 :: f x y -> Tails f '[x, y]
mk2 :: forall {k} (f :: k -> k -> *) (x :: k) (y :: k).
f x y -> Tails f '[x, y]
mk2 f x y
xy = NP (f x) '[y] -> Tails f '[y] -> Tails f '[x, y]
forall {k} (f :: k -> k -> *) (x :: k) (xs :: [k]).
NP (f x) xs -> Tails f xs -> Tails f (x : xs)
TCons (f x y
xy f x y -> NP (f x) '[] -> NP (f x) '[y]
forall {k} (f :: k -> *) (x :: k) (xs1 :: [k]).
f x -> NP f xs1 -> NP f (x : xs1)
:* NP (f x) '[]
forall {k} (f :: k -> *). NP f '[]
Nil) Tails f '[y]
forall {k} (f :: k -> k -> *) (x :: k). Tails f '[x]
mk1

mk3 :: f x y -> f x z -> f y z -> Tails f '[x, y, z]
mk3 :: forall {k} (f :: k -> k -> *) (x :: k) (y :: k) (z :: k).
f x y -> f x z -> f y z -> Tails f '[x, y, z]
mk3 f x y
xy f x z
xz f y z
yz = NP (f x) '[y, z] -> Tails f '[y, z] -> Tails f '[x, y, z]
forall {k} (f :: k -> k -> *) (x :: k) (xs :: [k]).
NP (f x) xs -> Tails f xs -> Tails f (x : xs)
TCons (f x y
xy f x y -> NP (f x) '[z] -> NP (f x) '[y, z]
forall {k} (f :: k -> *) (x :: k) (xs1 :: [k]).
f x -> NP f xs1 -> NP f (x : xs1)
:* f x z
xz f x z -> NP (f x) '[] -> NP (f x) '[z]
forall {k} (f :: k -> *) (x :: k) (xs1 :: [k]).
f x -> NP f xs1 -> NP f (x : xs1)
:* NP (f x) '[]
forall {k} (f :: k -> *). NP f '[]
Nil) (f y z -> Tails f '[y, z]
forall {k} (f :: k -> k -> *) (x :: k) (y :: k).
f x y -> Tails f '[x, y]
mk2 f y z
yz)

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

hmap :: SListI xs
     => (forall x y. f x y -> g x y)
     -> Tails f xs -> Tails 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)
-> Tails f xs -> Tails g xs
hmap = Proxy Top
-> (forall (x :: k) (y :: k). (Top x, Top y) => f x y -> g x y)
-> Tails f xs
-> Tails 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)
-> Tails f xs
-> Tails 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)
      -> Tails f xs -> Tails 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)
-> Tails f xs
-> Tails g xs
hcmap proxy c
p forall (x :: k) (y :: k). (c x, c y) => f x y -> g x y
g = Tails f xs -> Tails g xs
forall (xs' :: [k]). All c xs' => Tails f xs' -> Tails g xs'
go
  where
    go :: All c xs' => Tails f xs' -> Tails g xs'
    go :: forall (xs' :: [k]). All c xs' => Tails f xs' -> Tails g xs'
go Tails f xs'
TNil           = Tails g xs'
Tails g '[]
forall {k} (f :: k -> k -> *). Tails f '[]
TNil
    go (TCons NP (f x) xs
fs Tails f xs
fss) = NP (g x) xs -> Tails g xs -> Tails g (x : xs)
forall {k} (f :: k -> k -> *) (x :: k) (xs :: [k]).
NP (f x) xs -> Tails f xs -> Tails f (x : xs)
TCons (proxy c
-> (forall (a :: k). c a => f x a -> g x a)
-> NP (f x) xs
-> NP (g x) xs
forall {k} {l} (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *).
(AllN (Prod h) c xs, HAp h) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
SOP.hcmap proxy c
p f x a -> g x a
forall (a :: k). c a => f x a -> g x a
forall (x :: k) (y :: k). (c x, c y) => f x y -> g x y
g NP (f x) xs
fs) (Tails f xs -> Tails g xs
forall (xs' :: [k]). All c xs' => Tails f xs' -> Tails g xs'
go Tails f xs
fss)

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

hcpure :: forall proxy f c xs. All c xs
       => proxy c
       -> (forall x y. (c x, c y) => f x y) -> Tails f xs
hcpure :: forall {k} (proxy :: (k -> Constraint) -> *) (f :: k -> k -> *)
       (c :: k -> Constraint) (xs :: [k]).
All c xs =>
proxy c
-> (forall (x :: k) (y :: k). (c x, c y) => f x y) -> Tails f xs
hcpure proxy c
p forall (x :: k) (y :: k). (c x, c y) => f x y
f = SList xs -> Tails f xs
forall (xs' :: [k]). All c xs' => SList xs' -> Tails f xs'
go SList xs
forall {k} (xs :: [k]). SListI xs => SList xs
sList
  where
    go :: All c xs' => SList xs' -> Tails f xs'
    go :: forall (xs' :: [k]). All c xs' => SList xs' -> Tails f xs'
go SList xs'
SNil  = Tails f xs'
Tails f '[]
forall {k} (f :: k -> k -> *). Tails f '[]
TNil
    go SList xs'
SCons = NP (f x) xs -> Tails f xs -> Tails f (x : xs)
forall {k} (f :: k -> k -> *) (x :: k) (xs :: [k]).
NP (f x) xs -> Tails f xs -> Tails f (x : xs)
TCons (proxy c -> (forall (a :: k). c a => f x a) -> NP (f x) xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *).
(HPure h, AllN h c xs) =>
proxy c -> (forall (a :: k). c a => f a) -> h f xs
forall (c :: k -> Constraint) (xs :: [k])
       (proxy :: (k -> Constraint) -> *) (f :: k -> *).
AllN NP c xs =>
proxy c -> (forall (a :: k). c a => f a) -> NP f xs
SOP.hcpure proxy c
p f x a
forall (a :: k). c a => f x a
forall (x :: k) (y :: k). (c x, c y) => f x y
f) (SList xs -> Tails f xs
forall (xs' :: [k]). All c xs' => SList xs' -> Tails f xs'
go SList xs
forall {k} (xs :: [k]). SListI xs => SList xs
sList)

inPairsToTails ::
     forall f xs .
     All Top xs
  => InPairs.InPairs (InPairs.Fn2 f) xs
  -> Tails (InPairs.Fn2 f) xs
inPairsToTails :: forall {k} (f :: k -> *) (xs :: [k]).
All Top xs =>
InPairs (Fn2 f) xs -> Tails (Fn2 f) xs
inPairsToTails = InPairs (Fn2 f) xs -> Tails (Fn2 f) xs
forall (xs' :: [k]).
All Top xs' =>
InPairs (Fn2 f) xs' -> Tails (Fn2 f) xs'
go
  where
    go ::
         forall xs'.
         All Top xs'
      => InPairs.InPairs (InPairs.Fn2 f) xs'
      -> Tails (InPairs.Fn2 f) xs'
    go :: forall (xs' :: [k]).
All Top xs' =>
InPairs (Fn2 f) xs' -> Tails (Fn2 f) xs'
go InPairs (Fn2 f) xs'
InPairs.PNil = Tails (Fn2 f) xs'
Tails (Fn2 f) '[x]
forall {k} (f :: k -> k -> *) (x :: k). Tails f '[x]
mk1
    go (InPairs.PCons (InPairs.Fn2 f x -> f y
f) InPairs (Fn2 f) (y : zs)
n) =
      case InPairs (Fn2 f) (y : zs) -> Tails (Fn2 f) (y : zs)
forall (xs' :: [k]).
All Top xs' =>
InPairs (Fn2 f) xs' -> Tails (Fn2 f) xs'
go InPairs (Fn2 f) (y : zs)
n of
        n' :: Tails (Fn2 f) (y : zs)
n'@(TCons NP (Fn2 f x) xs
np Tails (Fn2 f) xs
_) ->
          NP (Fn2 f x) (y : xs)
-> Tails (Fn2 f) (y : xs) -> Tails (Fn2 f) (x : y : xs)
forall {k} (f :: k -> k -> *) (x :: k) (xs :: [k]).
NP (f x) xs -> Tails f xs -> Tails f (x : xs)
TCons
            (   (f x -> f y) -> Fn2 f x y
forall {k} (f :: k -> *) (x :: k) (y :: k).
(f x -> f y) -> Fn2 f x y
InPairs.Fn2 f x -> f y
f
             Fn2 f x y -> NP (Fn2 f x) xs -> NP (Fn2 f x) (y : xs)
forall {k} (f :: k -> *) (x :: k) (xs1 :: [k]).
f x -> NP f xs1 -> NP f (x : xs1)
:* (forall (a :: k). Fn2 f x a -> Fn2 f x a)
-> NP (Fn2 f x) xs -> NP (Fn2 f x) xs
forall {k} {l} (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *).
(SListIN (Prod h) xs, HAp h) =>
(forall (a :: k). f a -> f' a) -> h f xs -> h f' xs
SOP.hmap (\(InPairs.Fn2 f y -> f a
g) ->
                            (f x -> f a) -> Fn2 f x a
forall {k} (f :: k -> *) (x :: k) (y :: k).
(f x -> f y) -> Fn2 f x y
InPairs.Fn2 (f y -> f a
g (f y -> f a) -> (f x -> f y) -> f x -> f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f x -> f y
f)) NP (Fn2 f x) xs
np
            ) Tails (Fn2 f) (y : zs)
Tails (Fn2 f) (y : xs)
n'

extendWithTails ::
     SListI xs
  => Index xs x
  -> Index xs y
  -> Tails (InPairs.Fn2 f) xs
  -> f x
  -> Maybe (f y)
extendWithTails :: forall {k} (xs :: [k]) (x :: k) (y :: k) (f :: k -> *).
SListI xs =>
Index xs x -> Index xs y -> Tails (Fn2 f) xs -> f x -> Maybe (f y)
extendWithTails Index xs x
IZ        Index xs y
IZ        Tails (Fn2 f) xs
_           = f y -> Maybe (f y)
forall a. a -> Maybe a
Just (f y -> Maybe (f y)) -> (f x -> f y) -> f x -> Maybe (f y)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f x -> f x
f x -> f y
forall a. a -> a
id
extendWithTails Index xs x
IZ        (IS Index xs' y
idx)  (TCons NP (Fn2 f x) xs
t Tails (Fn2 f) xs
_) = f y -> Maybe (f y)
forall a. a -> Maybe a
Just (f y -> Maybe (f y)) -> (f x -> f y) -> f x -> Maybe (f y)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fn2 f x y -> f x -> f y
forall {k} (f :: k -> *) (x :: k) (y :: k). Fn2 f x y -> f x -> f y
InPairs.apFn2 (Index xs' y -> NP (Fn2 f x) xs' -> Fn2 f x y
forall {k} (xs :: [k]) (x :: k) (f :: k -> *).
All Top xs =>
Index xs x -> NP f xs -> f x
projectNP Index xs' y
idx NP (Fn2 f x) xs'
NP (Fn2 f x) xs
t)
extendWithTails (IS Index xs' x
idx1) (IS Index xs' y
idx2) (TCons NP (Fn2 f x) xs
_ Tails (Fn2 f) xs
n) = Index xs' x
-> Index xs' y -> Tails (Fn2 f) xs' -> f x -> Maybe (f y)
forall {k} (xs :: [k]) (x :: k) (y :: k) (f :: k -> *).
SListI xs =>
Index xs x -> Index xs y -> Tails (Fn2 f) xs -> f x -> Maybe (f y)
extendWithTails Index xs' x
idx1 Index xs' y
Index xs' y
idx2 Tails (Fn2 f) xs'
Tails (Fn2 f) xs
n
extendWithTails IS{}      Index xs y
IZ        Tails (Fn2 f) xs
_           = Maybe (f y) -> f x -> Maybe (f y)
forall a b. a -> b -> a
const Maybe (f y)
forall a. Maybe a
Nothing