diff --git a/LiquidExamples.hs b/LiquidExamples.hs index 41f7623..b91fc20 100644 --- a/LiquidExamples.hs +++ b/LiquidExamples.hs @@ -104,20 +104,18 @@ safeLookup x i -- | A pointer tagged with its size +{-@ data PtrSized a = PtrSized { ptrData :: Ptr a , ptrSz :: {n:Int | n >= 0}} @-} data PtrSized a = PtrSized { ptrData :: Ptr a , ptrSz :: Int } -{-@ measure ptrSize @-} -ptrSize :: PtrSized a -> Int -ptrSize (PtrSized _ n) = n -{-@ type SafeIndex N = {i:Int | 0 <= i && i < N} @-} +{-@ type SafeIndex v = {i:Int | 0 <= i && i < ptrSz v} @-} {-@ peekElemN :: Storable a => v:PtrSized a - -> SafeIndex (ptrSize v) + -> SafeIndex v -> IO a @-} peekElemN :: Storable a => PtrSized a -> Int -> IO a