Changes between Version 2 and Version 3 of TypeNats/SingletonsAndExistentials


Ignore:
Timestamp:
Apr 17, 2012 8:08:23 PM (2 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/SingletonsAndExistentials

    v2 v3  
    11Consider a type for arrays with a statically known size. 
    22{{{ 
    3 newtype ArrPtr (n :: Nat) a = SA (Ptr a) 
     3newtype ArrPtr (n :: Nat) a = ArrPtr (Ptr a) 
     4 
     5memset_c :: ArrPtr n a -> a -> Sing n -> IO () 
     6memset_c (ArrPtr p) a n = forM_ [ 1 .. fromSing n - 1 ] $ \i -> 
     7   pokeElemOff p (fromIntegral i) a 
     8 
     9memset :: SingI n => ArrPtr n a -> a -> IO () 
     10memset p a = withSing (memset_c p a) 
    411}}} 
    512