Changes between Version 5 and Version 6 of TypeNats/InductiveDefinitions


Ignore:
Timestamp:
Feb 7, 2011 8:12:28 AM (4 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/InductiveDefinitions

    v5 v6  
    66
    77--------------------------------------------------------------------------------
    8 -- Extending GHC.TypeNats with these two declarations allows us to
     8-- Extending GHC.TypeNats with these two function allows us to
    99-- write inductive definitions.
    1010
     
    1717  where unsafe :: Integer -> UNat n
    1818        unsafe 0 = unsafeCoerce Zero
    19         unsafe n = unsafeCoerce (Succ (unsafe (n-1)))
     19        unsafe n = unsafeCoerce (Succ (unsafe $! (n-1)))
    2020
    2121--------------------------------------------------------------------------------
     
    2929  show (Cons x xs) = show x ++ " : " ++ show xs
    3030
    31 cat :: Vec m a -> Vec n a -> Vec (m + n) a
     31instance Functor (Vec n) where
     32  fmap f Nil          = Nil
     33  fmap f (Cons x xs)  = Cons (f x) (fmap f xs)
     34
     35cat :: Vec m a -> Vec n a -> Vec (m + n) a
    3236cat Nil ys          = ys
    3337cat (Cons x xs) ys  = Cons x (cat xs ys)
    34 
    35 split :: UNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
    36 split Zero xs = (Nil, xs)
    37 split (Succ n) (Cons x xs)  = case split n xs of
    38                                 (as,bs) -> (Cons x as, bs)
    3938
    4039vecLen :: NatI n => Vec n a -> Nat n
    4140vecLen _ = nat
    4241
    43 autoSplit :: NatI m => Vec (m + n) a -> (Vec m a, Vec n a)
    44 autoSplit xs = res
    45   where res@(as,_) = split len xs
    46         len        = toUNat (vecLen as)
    47 }}}               
    4842
     43splitU :: UNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
     44splitU Zero xs               = (Nil, xs)
     45splitU (Succ n) (Cons x xs)  = let (as,bs) = splitU n xs
     46                               in (Cons x as, bs)
    4947
     48vecSplitAt :: Nat m -> Vec (m + n) a -> (Vec m a, Vec n a)
     49vecSplitAt n = splitU (toUNat n)
     50
     51vecSplit :: NatI m => Vec (m + n) a -> (Vec m a, Vec n a)
     52vecSplit = vecSplitAt nat
     53}}}