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

{-# OPTIONS_GHC -Wno-redundant-constraints #-}

module Debug.RecoverRTTI.Util (
    -- * Existentials
    Some(..)
  , elimKnownSymbol
    -- * Constraints
  , keepRedundantConstraint
    -- * Traversable
  , checkEmptyTraversable
    -- * Lists
  , dropEnds
    -- * SOP
  , VerifiedSize(..)
  , verifySize
  ) where

import Data.Kind
import Data.Proxy
import Data.SOP
import Data.Void
import GHC.TypeLits (KnownSymbol, SomeSymbol(..), someSymbolVal)

import Debug.RecoverRTTI.Util.TypeLevel

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

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

elimKnownSymbol :: String -> (forall n. KnownSymbol n => Proxy n -> r) -> r
elimKnownSymbol :: String
-> (forall (n :: Symbol). KnownSymbol n => Proxy n -> r) -> r
elimKnownSymbol String
s forall (n :: Symbol). KnownSymbol n => Proxy n -> r
k =
    case String -> SomeSymbol
someSymbolVal String
s of
      SomeSymbol Proxy n
p -> Proxy n -> r
forall (n :: Symbol). KnownSymbol n => Proxy n -> r
k Proxy n
p

{-------------------------------------------------------------------------------
  Constraints
-------------------------------------------------------------------------------}

-- | Can be used to silence individual "redundant constraint" warnings
--
-- > foo :: ConstraintUsefulForDebugging => ...
-- > foo =
-- >     ..
-- >   where
-- >     _ = keepRedundantConstraint (Proxy @ConstraintUsefulForDebugging))
keepRedundantConstraint :: c => proxy c -> ()
keepRedundantConstraint :: proxy c -> ()
keepRedundantConstraint proxy c
_ = ()

{-------------------------------------------------------------------------------
  Traversable
-------------------------------------------------------------------------------}

-- | Check if a traversable data structure is empty
--
-- Returns evidence: an element of the data-structure if it's non-empty,
-- or evidence that it is empty otherwise.
checkEmptyTraversable :: Traversable t => t a -> Either a (t Void)
checkEmptyTraversable :: t a -> Either a (t Void)
checkEmptyTraversable = (a -> Either a Void) -> t a -> Either a (t Void)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> Either a Void
forall a b. a -> Either a b
Left

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

-- | Drop the ends of a list
--
-- > dropEnds "abcde" == Just ('a',"bcd",'e')
dropEnds :: forall a. [a] -> Maybe (a, [a], a)
dropEnds :: [a] -> Maybe (a, [a], a)
dropEnds = \case
    []     -> Maybe (a, [a], a)
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]
_   []     = Maybe (a, [a], a)
forall a. Maybe a
Nothing
        goRest [a]
acc [a
z]    = (a, [a], a) -> Maybe (a, [a], a)
forall a. a -> Maybe a
Just (a
a, [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
xa -> [a] -> [a]
forall 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 :: Sing n -> [a] -> Maybe (VerifiedSize n a)
verifySize :: Sing n -> [a] -> Maybe (VerifiedSize n a)
verifySize = Sing n -> [a] -> Maybe (VerifiedSize n a)
forall (n :: Nat) a. Sing n -> [a] -> Maybe (VerifiedSize n a)
go
  where
    go :: Sing n -> [a] -> Maybe (VerifiedSize n a)
    go :: Sing n -> [a] -> Maybe (VerifiedSize n a)
go Sing n
SZ     []     = VerifiedSize n a -> Maybe (VerifiedSize n a)
forall a. a -> Maybe a
Just (NP (K a) '[] -> VerifiedSize n a
forall (n :: Nat) a (xs :: [*]).
(SListI xs, Length xs ~ n) =>
NP (K a) xs -> VerifiedSize n a
VerifiedSize NP (K a) '[]
forall k (a :: k -> *). NP a '[]
Nil)
    go (SS n) (a
x:[a]
xs) = do VerifiedSize NP (K a) xs
np <- Sing n -> [a] -> Maybe (VerifiedSize n a)
forall (n :: Nat) a. Sing n -> [a] -> Maybe (VerifiedSize n a)
go Sing n
n [a]
xs
                          VerifiedSize n a -> Maybe (VerifiedSize n a)
forall (m :: * -> *) a. Monad m => a -> m a
return (VerifiedSize n a -> Maybe (VerifiedSize n a))
-> VerifiedSize n a -> Maybe (VerifiedSize n a)
forall a b. (a -> b) -> a -> b
$ NP (K a) (Any : xs) -> VerifiedSize n a
forall (n :: Nat) a (xs :: [*]).
(SListI xs, Length xs ~ n) =>
NP (K a) xs -> VerifiedSize n a
VerifiedSize (a -> K a Any
forall k a (b :: k). a -> K a b
K a
x K a Any -> NP (K a) xs -> NP (K a) (Any : xs)
forall k (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP (K a) xs
np)
    go Sing n
SZ     (a
_:[a]
_)  = Maybe (VerifiedSize n a)
forall a. Maybe a
Nothing
    go (SS _) []     = Maybe (VerifiedSize n a)
forall a. Maybe a
Nothing