mutable_vector_abstract_refinement.hs

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"