Changes between Version 2 and Version 3 of TypeNats/SingletonsAndExistentials


Ignore:
Timestamp:
Apr 17, 2012 8:08:23 PM (3 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