{-# 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
  , hcmap
  , hcpure
  , hmap
  , hpure
  ) where

import           Data.Kind (Type)
import           Data.Proxy
import           Data.SOP.Constraint
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)