{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts#-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.HVect
(
HVect (..)
, empty, null, head, tail
, singleton
, length, HVectLen
, findFirst, InList, ListContains, NotInList
, MaybeToList
, (!!), HVectIdx
, HVectElim
, Append, (<++>)
, ReverseLoop, Reverse, reverse
, uncurry
, Rep (..), HasRep (..)
, curryExpl, curry
, packExpl, pack
, AllHave
, Nat (..), SNat (..), sNatToInt
, intToSNat, AnySNat (..)
, (:<)
) where
import GHC.Exts
import Prelude hiding (reverse, uncurry, curry, head, null, (!!), length, tail)
data HVect (ts :: [*]) where
HNil :: HVect '[]
(:&:) :: !t -> !(HVect ts) -> HVect (t ': ts)
infixr 5 :&:
instance Eq (HVect '[]) where
HVect '[]
_ == :: HVect '[] -> HVect '[] -> Bool
== HVect '[]
_ =
Bool
True
instance (Eq (HVect ts), Eq t) => Eq (HVect (t ': ts)) where
t
a :&: HVect ts
as == :: HVect (t : ts) -> HVect (t : ts) -> Bool
== t
b :&: HVect ts
bs =
t
a t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
t
b Bool -> Bool -> Bool
&& HVect ts
as HVect ts -> HVect ts -> Bool
forall a. Eq a => a -> a -> Bool
== HVect ts
HVect ts
bs
instance Show (HVect '[]) where
showsPrec :: Int -> HVect '[] -> ShowS
showsPrec Int
d HVect '[]
HNil =
Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"[]"
instance (Show (HVect ts), Show t) => Show (HVect (t ': ts)) where
showsPrec :: Int -> HVect (t : ts) -> ShowS
showsPrec Int
d (t
a :&: HVect ts
as) =
Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
5) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
Int -> t -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
6 t
a ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
String -> ShowS
showString String
" <:> " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
Int -> HVect ts -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
6 HVect ts
as
instance Ord (HVect '[]) where
HVect '[]
_ compare :: HVect '[] -> HVect '[] -> Ordering
`compare` HVect '[]
_ = Ordering
EQ
HVect '[]
_ <= :: HVect '[] -> HVect '[] -> Bool
<= HVect '[]
_ = Bool
True
instance (Ord (HVect ts), Ord t) => Ord (HVect (t ': ts)) where
(t
a :&: HVect ts
as) compare :: HVect (t : ts) -> HVect (t : ts) -> Ordering
`compare` (t
b :&: HVect ts
bs) =
case t
a t -> t -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` t
t
b of
Ordering
EQ -> HVect ts
as HVect ts -> HVect ts -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` HVect ts
HVect ts
bs
Ordering
o -> Ordering
o
t
a :&: HVect ts
as <= :: HVect (t : ts) -> HVect (t : ts) -> Bool
<= t
b :&: HVect ts
bs =
t
a t -> t -> Bool
forall a. Ord a => a -> a -> Bool
<= t
t
b Bool -> Bool -> Bool
&& HVect ts
as HVect ts -> HVect ts -> Bool
forall a. Ord a => a -> a -> Bool
<= HVect ts
HVect ts
bs
type family HVectElim (ts :: [*]) (a :: *) :: * where
HVectElim '[] a = a
HVectElim (t ': ts) a = t -> HVectElim ts a
type family Append (as :: [*]) (bs :: [*]) :: [*] where
Append '[] bs = bs
Append (a ': as) bs = a ': (Append as bs)
type family InList (x :: *) (xs :: [*]) :: Nat where
InList x (x ': ys) = 'Zero
InList x (y ': ys) = 'Succ (InList x ys)
type family AllHave (c :: * -> Constraint) (xs :: [*]) :: Constraint where
AllHave c '[] = 'True ~ 'True
AllHave c (x ': xs) = (c x, AllHave c xs)
class SNatRep n where
getSNat :: SNat n
instance SNatRep 'Zero where
getSNat :: SNat 'Zero
getSNat = SNat 'Zero
SZero
instance SNatRep n => SNatRep ('Succ n) where
getSNat :: SNat ('Succ n)
getSNat = SNat n -> SNat ('Succ n)
forall (n :: Nat). SNat n -> SNat ('Succ n)
SSucc SNat n
forall (n :: Nat). SNatRep n => SNat n
getSNat
type family NotInList (x :: *) (xs :: [*]) :: Bool where
NotInList x (x ': ys) = 'False
NotInList x (y ': ys) = NotInList x ys
NotInList x '[] = 'True
type ListContains n x ts = (SNatRep n, InList x ts ~ n, HVectIdx n ts ~ x)
type family MaybeToList (a :: Maybe *) :: [*] where
MaybeToList ('Just r) = '[r]
MaybeToList 'Nothing = '[]
findFirst :: forall x ts n. (ListContains n x ts) => HVect ts -> x
findFirst :: HVect ts -> x
findFirst HVect ts
vect = SNat n
idx SNat n -> HVect ts -> HVectIdx n ts
forall (n :: Nat) (as :: [*]). SNat n -> HVect as -> HVectIdx n as
!! HVect ts
vect
where
idx :: SNat n
idx :: SNat n
idx = SNat n
forall (n :: Nat). SNatRep n => SNat n
getSNat
singleton :: a -> HVect '[a]
singleton :: a -> HVect '[a]
singleton a
el = a
el a -> HVect '[] -> HVect '[a]
forall t (ts :: [*]). t -> HVect ts -> HVect (t : ts)
:&: HVect '[]
HNil
empty :: HVect '[]
empty :: HVect '[]
empty = HVect '[]
HNil
null :: HVect as -> Bool
null :: HVect as -> Bool
null HVect as
HNil = Bool
True
null HVect as
_ = Bool
False
head :: HVect (t ': ts) -> t
head :: HVect (t : ts) -> t
head (t
a :&: HVect ts
_) = t
t
a
tail :: HVect (t ': ts) -> HVect ts
tail :: HVect (t : ts) -> HVect ts
tail (t
_ :&: HVect ts
as) = HVect ts
HVect ts
as
length :: HVect as -> SNat (HVectLen as)
length :: HVect as -> SNat (HVectLen as)
length HVect as
HNil = SNat (HVectLen as)
SNat 'Zero
SZero
length (t
_ :&: HVect ts
as) = SNat (HVectLen ts) -> SNat ('Succ (HVectLen ts))
forall (n :: Nat). SNat n -> SNat ('Succ n)
SSucc (HVect ts -> SNat (HVectLen ts)
forall (as :: [*]). HVect as -> SNat (HVectLen as)
length HVect ts
as)
sNatToInt :: SNat n -> Int
sNatToInt :: SNat n -> Int
sNatToInt SNat n
SZero = Int
0
sNatToInt (SSucc SNat n
n) = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (SNat n -> Int
forall (n :: Nat). SNat n -> Int
sNatToInt SNat n
n)
intToSNat :: Int -> AnySNat
intToSNat :: Int -> AnySNat
intToSNat Int
0 = SNat 'Zero -> AnySNat
forall (n :: Nat). SNat n -> AnySNat
AnySNat SNat 'Zero
SZero
intToSNat Int
n =
case Int -> AnySNat
intToSNat (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) of
AnySNat SNat n
m -> SNat ('Succ n) -> AnySNat
forall (n :: Nat). SNat n -> AnySNat
AnySNat (SNat n -> SNat ('Succ n)
forall (n :: Nat). SNat n -> SNat ('Succ n)
SSucc SNat n
m)
data Nat where
Zero :: Nat
Succ :: Nat -> Nat
data SNat (n :: Nat) where
SZero :: SNat 'Zero
SSucc :: SNat n -> SNat ('Succ n)
data AnySNat where
AnySNat :: forall n. SNat n -> AnySNat
type family HVectLen (ts :: [*]) :: Nat where
HVectLen '[] = 'Zero
HVectLen (t ': ts) = 'Succ (HVectLen ts)
type family HVectIdx (n :: Nat) (ts :: [*]) :: * where
HVectIdx 'Zero (a ': as) = a
HVectIdx ('Succ n) (a ': as) = HVectIdx n as
type family (m :: Nat) :< (n :: Nat) :: Bool where
m :< 'Zero = 'False
'Zero :< ('Succ n) = 'True
('Succ m) :< ('Succ n) = m :< n
type family (m :: Nat) :- (n :: Nat) :: Nat where
n :- 'Zero = n
('Succ m) :- ('Succ n) = m :- n
(!!) :: SNat n -> HVect as -> HVectIdx n as
SNat n
SZero !! :: SNat n -> HVect as -> HVectIdx n as
!! (t
a :&: HVect ts
_) = t
HVectIdx n as
a
(SSucc SNat n
s) !! (t
_ :&: HVect ts
as) = SNat n
s SNat n -> HVect ts -> HVectIdx n ts
forall (n :: Nat) (as :: [*]). SNat n -> HVect as -> HVectIdx n as
!! HVect ts
as
SNat n
_ !! HVect as
_ = String -> HVectIdx n as
forall a. HasCallStack => String -> a
error String
"HVect !!: This should never happen"
infixr 5 <++>
infixl 9 !!
(<++>) :: HVect as -> HVect bs -> HVect (Append as bs)
<++> :: HVect as -> HVect bs -> HVect (Append as bs)
(<++>) HVect as
HNil HVect bs
bs = HVect bs
HVect (Append as bs)
bs
(<++>) (t
a :&: HVect ts
as) HVect bs
bs = t
a t -> HVect (Append ts bs) -> HVect (t : Append ts bs)
forall t (ts :: [*]). t -> HVect ts -> HVect (t : ts)
:&: (HVect ts
as HVect ts -> HVect bs -> HVect (Append ts bs)
forall (as :: [*]) (bs :: [*]).
HVect as -> HVect bs -> HVect (Append as bs)
<++> HVect bs
bs)
type family ReverseLoop (as :: [*]) (bs :: [*]) :: [*] where
ReverseLoop '[] bs = bs
ReverseLoop (a ': as) bs = ReverseLoop as (a ': bs)
type Reverse as = ReverseLoop as '[]
reverse :: HVect as -> HVect (Reverse as)
reverse :: HVect as -> HVect (Reverse as)
reverse HVect as
vs = HVect as -> HVect '[] -> HVect (Reverse as)
forall (as :: [*]) (bs :: [*]).
HVect as -> HVect bs -> HVect (ReverseLoop as bs)
go HVect as
vs HVect '[]
HNil
where
go :: HVect as -> HVect bs -> HVect (ReverseLoop as bs)
go :: HVect as -> HVect bs -> HVect (ReverseLoop as bs)
go HVect as
HNil HVect bs
bs = HVect bs
HVect (ReverseLoop as bs)
bs
go (t
a :&: HVect ts
as) HVect bs
bs = HVect ts -> HVect (t : bs) -> HVect (ReverseLoop ts (t : bs))
forall (as :: [*]) (bs :: [*]).
HVect as -> HVect bs -> HVect (ReverseLoop as bs)
go HVect ts
as (t
a t -> HVect bs -> HVect (t : bs)
forall t (ts :: [*]). t -> HVect ts -> HVect (t : ts)
:&: HVect bs
bs)
uncurry :: HVectElim ts a -> HVect ts -> a
uncurry :: HVectElim ts a -> HVect ts -> a
uncurry HVectElim ts a
f HVect ts
HNil = a
HVectElim ts a
f
uncurry HVectElim ts a
f (t
x :&: HVect ts
xs) = HVectElim ts a -> HVect ts -> a
forall (ts :: [*]) a. HVectElim ts a -> HVect ts -> a
uncurry (HVectElim ts a
t -> HVectElim ts a
f t
x) HVect ts
xs
data Rep (ts :: [*]) where
RNil :: Rep '[]
RCons :: Rep ts -> Rep (t ': ts)
class HasRep (ts :: [*]) where
hasRep :: Rep ts
instance HasRep '[] where
hasRep :: Rep '[]
hasRep = Rep '[]
RNil
instance HasRep ts => HasRep (t ': ts) where
hasRep :: Rep (t : ts)
hasRep = Rep ts -> Rep (t : ts)
forall (ts :: [*]) t. Rep ts -> Rep (t : ts)
RCons Rep ts
forall (ts :: [*]). HasRep ts => Rep ts
hasRep
curryExpl :: Rep ts -> (HVect ts -> a) -> HVectElim ts a
curryExpl :: Rep ts -> (HVect ts -> a) -> HVectElim ts a
curryExpl Rep ts
RNil HVect ts -> a
f = HVect ts -> a
f HVect ts
HVect '[]
HNil
curryExpl (RCons Rep ts
r) HVect ts -> a
f = \t
x -> Rep ts -> (HVect ts -> a) -> HVectElim ts a
forall (ts :: [*]) a. Rep ts -> (HVect ts -> a) -> HVectElim ts a
curryExpl Rep ts
r (HVect ts -> a
f (HVect ts -> a) -> (HVect ts -> HVect ts) -> HVect ts -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> HVect ts -> HVect (t : ts)
forall t (ts :: [*]). t -> HVect ts -> HVect (t : ts)
(:&:) t
x)
curry :: HasRep ts => (HVect ts -> a) -> HVectElim ts a
curry :: (HVect ts -> a) -> HVectElim ts a
curry = Rep ts -> (HVect ts -> a) -> HVectElim ts a
forall (ts :: [*]) a. Rep ts -> (HVect ts -> a) -> HVectElim ts a
curryExpl Rep ts
forall (ts :: [*]). HasRep ts => Rep ts
hasRep
buildElim :: Rep ts -> (HVect ts -> HVect ss) -> HVectElim ts (HVect ss)
buildElim :: Rep ts -> (HVect ts -> HVect ss) -> HVectElim ts (HVect ss)
buildElim Rep ts
RNil HVect ts -> HVect ss
f = HVect ts -> HVect ss
f HVect ts
HVect '[]
HNil
buildElim (RCons Rep ts
r) HVect ts -> HVect ss
f = \t
x -> Rep ts -> (HVect ts -> HVect ss) -> HVectElim ts (HVect ss)
forall (ts :: [*]) (ss :: [*]).
Rep ts -> (HVect ts -> HVect ss) -> HVectElim ts (HVect ss)
buildElim Rep ts
r (HVect ts -> HVect ss
f (HVect ts -> HVect ss)
-> (HVect ts -> HVect ts) -> HVect ts -> HVect ss
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> HVect ts -> HVect (t : ts)
forall t (ts :: [*]). t -> HVect ts -> HVect (t : ts)
(:&:) t
x)
packExpl :: Rep ts -> (forall a. HVectElim ts a -> a) -> HVect ts
packExpl :: Rep ts -> (forall a. HVectElim ts a -> a) -> HVect ts
packExpl Rep ts
rep forall a. HVectElim ts a -> a
f = HVectElim ts (HVect ts) -> HVect ts
forall a. HVectElim ts a -> a
f (Rep ts -> (HVect ts -> HVect ts) -> HVectElim ts (HVect ts)
forall (ts :: [*]) (ss :: [*]).
Rep ts -> (HVect ts -> HVect ss) -> HVectElim ts (HVect ss)
buildElim Rep ts
rep HVect ts -> HVect ts
forall a. a -> a
id)
pack :: HasRep ts => (forall a. HVectElim ts a -> a) -> HVect ts
pack :: (forall a. HVectElim ts a -> a) -> HVect ts
pack = Rep ts -> (forall a. HVectElim ts a -> a) -> HVect ts
forall (ts :: [*]).
Rep ts -> (forall a. HVectElim ts a -> a) -> HVect ts
packExpl Rep ts
forall (ts :: [*]). HasRep ts => Rep ts
hasRep