{-# LANGUAGE ConstraintKinds     #-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE PolyKinds           #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Debug.RecoverRTTI.Util (
    -- * Existentials
    Some(..)
  , mapSome
    -- * Lists
  , dropEnds
    -- * SOP
  , VerifiedSize(..)
  , verifySize
  ) where

import Data.Kind
import Data.SOP

import Debug.RecoverRTTI.Nat

{-------------------------------------------------------------------------------
  Existentials
-------------------------------------------------------------------------------}

data Some (f :: k -> Type) where
  Some :: forall f a. f a -> Some f

mapSome :: (forall x. f x -> g x) -> Some f -> Some g
mapSome :: forall {k} (f :: k -> *) (g :: k -> *).
(forall (x :: k). f x -> g x) -> Some f -> Some g
mapSome forall (x :: k). f x -> g x
f (Some f a
x) = forall {k} (f :: k -> *) (xs :: k). f xs -> Some f
Some (forall (x :: k). f x -> g x
f f a
x)

{-------------------------------------------------------------------------------
  Lists
-------------------------------------------------------------------------------}

-- | Drop the ends of a list
--
-- > dropEnds "abcde" == Just ('a',"bcd",'e')
dropEnds :: forall a. [a] -> Maybe (a, [a], a)
dropEnds :: forall a. [a] -> Maybe (a, [a], a)
dropEnds = \case
    []     -> forall a. Maybe a
Nothing
    (a
a:[a]
xs) -> a -> [a] -> Maybe (a, [a], a)
go a
a [a]
xs
  where
    go :: a -> [a] -> Maybe (a, [a], a)
    go :: a -> [a] -> Maybe (a, [a], a)
go a
a = [a] -> [a] -> Maybe (a, [a], a)
goRest []
      where
        goRest :: [a] -> [a] -> Maybe (a, [a], a)
        goRest :: [a] -> [a] -> Maybe (a, [a], a)
goRest [a]
_   []     = forall a. Maybe a
Nothing
        goRest [a]
acc [a
z]    = forall a. a -> Maybe a
Just (a
a, forall a. [a] -> [a]
reverse [a]
acc, a
z)
        goRest [a]
acc (a
x:[a]
xs) = [a] -> [a] -> Maybe (a, [a], a)
goRest (a
xforall a. a -> [a] -> [a]
:[a]
acc) [a]
xs

{-------------------------------------------------------------------------------
  SOP
-------------------------------------------------------------------------------}

data VerifiedSize (n :: Nat) (a :: Type) where
    -- This is intentionally not kind polymorphic
    VerifiedSize :: forall n a (xs :: [Type]).
         (SListI xs, Length xs ~ n)
      => NP (K a) xs -> VerifiedSize n a

verifySize :: SNat n -> [a] -> Maybe (VerifiedSize n a)
verifySize :: forall (n :: Nat) a. SNat n -> [a] -> Maybe (VerifiedSize n a)
verifySize = forall (n :: Nat) a. SNat n -> [a] -> Maybe (VerifiedSize n a)
go
  where
    go :: SNat n -> [a] -> Maybe (VerifiedSize n a)
    go :: forall (n :: Nat) a. SNat n -> [a] -> Maybe (VerifiedSize n a)
go SNat n
SZ     []     = forall a. a -> Maybe a
Just (forall (n :: Nat) a (xs :: [*]).
(SListI xs, Length xs ~ n) =>
NP (K a) xs -> VerifiedSize n a
VerifiedSize forall {k} (a :: k -> *). NP a '[]
Nil)
    go (SS SNat n
n) (a
x:[a]
xs) = do VerifiedSize NP (K a) xs
np <- forall (n :: Nat) a. SNat n -> [a] -> Maybe (VerifiedSize n a)
go SNat n
n [a]
xs
                          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) a (xs :: [*]).
(SListI xs, Length xs ~ n) =>
NP (K a) xs -> VerifiedSize n a
VerifiedSize (forall k a (b :: k). a -> K a b
K a
x forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP (K a) xs
np)
    go SNat n
SZ     (a
_:[a]
_)  = forall a. Maybe a
Nothing
    go (SS SNat n
_) []     = forall a. Maybe a
Nothing