Changes between Version 5 and Version 6 of TypeNats/InductiveDefinitions


Ignore:
Timestamp:
Feb 7, 2011 8:12:28 AM (3 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}}}