{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Debug.RecoverRTTI.Util (
Some(..)
, mapSome
, dropEnds
, VerifiedSize(..)
, verifySize
) where
import Data.Kind
import Data.SOP
import Debug.RecoverRTTI.Nat
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)
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
data VerifiedSize (n :: Nat) (a :: Type) where
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