... | @@ -5,7 +5,7 @@ import GHC.TypeNats |
... | @@ -5,7 +5,7 @@ import GHC.TypeNats |
|
import Unsafe.Coerce
|
|
import Unsafe.Coerce
|
|
|
|
|
|
--------------------------------------------------------------------------------
|
|
--------------------------------------------------------------------------------
|
|
-- Extending GHC.TypeNats with these two declarations allows us to
|
|
-- Extending GHC.TypeNats with these two function allows us to
|
|
-- write inductive definitions.
|
|
-- write inductive definitions.
|
|
|
|
|
|
data UNat :: Nat -> * where
|
|
data UNat :: Nat -> * where
|
... | @@ -16,7 +16,7 @@ toUNat :: Nat n -> UNat n |
... | @@ -16,7 +16,7 @@ toUNat :: Nat n -> UNat n |
|
toUNat n = unsafe (natToInteger n)
|
|
toUNat n = unsafe (natToInteger n)
|
|
where unsafe :: Integer -> UNat n
|
|
where unsafe :: Integer -> UNat n
|
|
unsafe 0 = unsafeCoerce Zero
|
|
unsafe 0 = unsafeCoerce Zero
|
|
unsafe n = unsafeCoerce (Succ (unsafe (n-1)))
|
|
unsafe n = unsafeCoerce (Succ (unsafe $! (n-1)))
|
|
|
|
|
|
--------------------------------------------------------------------------------
|
|
--------------------------------------------------------------------------------
|
|
|
|
|
... | @@ -28,20 +28,26 @@ instance Show a => Show (Vec n a) where |
... | @@ -28,20 +28,26 @@ instance Show a => Show (Vec n a) where |
|
show Nil = "[]"
|
|
show Nil = "[]"
|
|
show (Cons x xs) = show x ++ " : " ++ show xs
|
|
show (Cons x xs) = show x ++ " : " ++ show xs
|
|
|
|
|
|
cat :: Vec m a -> Vec n a -> Vec (m + n) a
|
|
instance Functor (Vec n) where
|
|
|
|
fmap f Nil = Nil
|
|
|
|
fmap f (Cons x xs) = Cons (f x) (fmap f xs)
|
|
|
|
|
|
|
|
cat :: Vec m a -> Vec n a -> Vec (m + n) a
|
|
cat Nil ys = ys
|
|
cat Nil ys = ys
|
|
cat (Cons x xs) ys = Cons x (cat xs ys)
|
|
cat (Cons x xs) ys = Cons x (cat xs ys)
|
|
|
|
|
|
split :: UNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
|
|
|
|
split Zero xs = (Nil, xs)
|
|
|
|
split (Succ n) (Cons x xs) = case split n xs of
|
|
|
|
(as,bs) -> (Cons x as, bs)
|
|
|
|
|
|
|
|
vecLen :: NatI n => Vec n a -> Nat n
|
|
vecLen :: NatI n => Vec n a -> Nat n
|
|
vecLen _ = nat
|
|
vecLen _ = nat
|
|
|
|
|
|
autoSplit :: NatI m => Vec (m + n) a -> (Vec m a, Vec n a)
|
|
|
|
autoSplit xs = res
|
|
splitU :: UNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
|
|
where res@(as,_) = split len xs
|
|
splitU Zero xs = (Nil, xs)
|
|
len = toUNat (vecLen as)
|
|
splitU (Succ n) (Cons x xs) = let (as,bs) = splitU n xs
|
|
|
|
in (Cons x as, bs)
|
|
|
|
|
|
|
|
vecSplitAt :: Nat m -> Vec (m + n) a -> (Vec m a, Vec n a)
|
|
|
|
vecSplitAt n = splitU (toUNat n)
|
|
|
|
|
|
|
|
vecSplit :: NatI m => Vec (m + n) a -> (Vec m a, Vec n a)
|
|
|
|
vecSplit = vecSplitAt nat
|
|
``` |
|
``` |
|
|
|
\ No newline at end of file |