Skip to content

Instantly share code, notes, and snippets.

Show Gist options
  • Save andrewthad/6c2bf12a3900202f9f5317b8daf4ffb7 to your computer and use it in GitHub Desktop.
Save andrewthad/6c2bf12a3900202f9f5317b8daf4ffb7 to your computer and use it in GitHub Desktop.
module Lib
( someFunc
) where
import Control.Monad.Primitive
import Data.Vector.Mutable (MVector,IOVector,unsafeNew,unsafeWrite)
import qualified Data.Vector.Mutable as MV
{-@ measure mvlen :: Data.Vector.MVector s a -> Int @-}
{-@ invariant { v : Data.Vector.MVector s a | 0 <= mvlen v } @-}
{-@ assume MV.replicate :: PrimMonad m => x : Nat -> a -> ( m { v : ( MVector ( PrimState m ) a ) | mvlen v = x } ) @-}
{-@ assume unsafeWrite :: Control.Monad.Primitive.PrimMonad m
=> x:(Data.Vector.MVector (Control.Monad.Primitive.PrimState m) a)
-> ix:{v:Nat | v < mvlen x }
-> a
-> m ()
@-}
{-@ testWrite :: PrimMonad m => x:(MVector (PrimState m) a) -> ix:{v:Nat | v < mvlen x } -> a -> (a -> a) -> m () @-}
testWrite :: PrimMonad m => MVector (PrimState m) a -> Int -> a -> (a -> a) -> m ()
testWrite mv ix a f = unsafeWrite mv ix (f a)
{-@ otherWrite :: PrimMonad m => x:(MVector (PrimState m) a) -> ix:{v:Nat | v < mvlen x } -> a -> a -> m () @-}
otherWrite :: PrimMonad m => MVector (PrimState m) a -> Int -> a -> a -> m ()
otherWrite mv ix a b = unsafeWrite mv ix b
{-@ testFunc :: PrimMonad m => m ( MVector (PrimState m) ( Int<{\x -> x < 100}> ) ) @-}
testFunc :: PrimMonad m => m (MVector (PrimState m) Int)
testFunc = do
v <- MV.replicate 12 99
unsafeWrite v 2 55
unsafeWrite v 3 99
-- This line fails as expected:
-- testWrite v 4 10 (+6)
-- This line succeeds as expected:
otherWrite v 4 99 98
-- This line fails, and I think it's understandable why:
-- otherWrite v 4 101 98
return v
someFunc :: IO ()
someFunc = putStrLn "someFunc"
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment