content: {-# LANGUAGE ApplicativeDo #-}
  {-# LANGUAGE LinearTypes #-}
  {-# LANGUAGE OverloadedStrings #-}
  {-# OPTIONS_GHC -Wno-name-shadowing #-}
  
  -- |
  -- Tests for mutable arrays.
  --
  -- See the testing framework explained in Test.Data.Mutable.Set.
  --
  -- The combination of axioms and homomorphisms provided functionally specify
  -- the behavior of arrays.
  --
  -- Remarks:
  --  * We don't test for failure on out-of-bound access
  --  * We don't test the empty constructor because
  module Test.Data.Mutable.Array
    ( mutArrTests,
    )
  where
  
  import qualified Data.Array.Mutable.Linear as Array
  import qualified Data.Functor.Linear as Data
  import qualified Data.List as List
  import qualified Data.Ord.Linear as Linear
  import Data.Unrestricted.Linear
  import qualified Data.Vector as Vector
  import Hedgehog
  import qualified Hedgehog.Gen as Gen
  import qualified Hedgehog.Range as Range
  import qualified Prelude.Linear as Linear hiding ((>))
  import Test.Tasty (TestTree, testGroup)
  import Test.Tasty.Hedgehog (testPropertyNamed)
  
  -- # Exported Tests
  --------------------------------------------------------------------------------
  
  mutArrTests :: TestTree
  mutArrTests = testGroup "Mutable array tests" group
  
  group :: [TestTree]
  group =
    -- All tests for exprs of the form (read (const ...) i)
    [ testPropertyNamed "∀ s,i,x. read (alloc s x) i = x" "readAlloc" readAlloc,
      testPropertyNamed "∀ a,s,x,i. read (snd (allocBeside s x a)) i = x" "allocBeside" allocBeside,
      testPropertyNamed "∀ s,a,i. i < length a, read (resize s 42 a) i = read a i" "readResize" readResize,
      testPropertyNamed "∀ a,i,x. read (write a i x) i = x " "readWrite1" readWrite1,
      testPropertyNamed "∀ a,i,j/=i,x. read (write a j x) i = read a i" "readWrite2" readWrite2,
      -- All tests for exprs of the form (length (const ...))
      testPropertyNamed "∀ s,x. len (alloc s x) = s" "lenAlloc" lenAlloc,
      testPropertyNamed "∀ a,i,x. len (write a i x) = len a" "lenWrite" lenWrite,
      testPropertyNamed "∀ a,s,x. len (resize s x a) = s" "lenResizeSeed" lenResizeSeed,
      -- Tests against a reference implementation
      testPropertyNamed
        "∀ a,ix. toList . write a ix = (\\l -> take ix l ++ [a] ++ drop (ix+1) l) . toList"
        "writeRef"
        writeRef,
      testPropertyNamed "∀ ix. read ix a = (toList a) !! i" "readRef" readRef,
      testPropertyNamed "size = length . toList" "sizeRef" sizeRef,
      testPropertyNamed "∀ a,s,x. resize s x a = take s (toList a ++ repeat x)" "resizeRef" resizeRef,
      testPropertyNamed "∀ s,n. slice s n = take s . drop n" "sliceRef" sliceRef,
      testPropertyNamed "f <$> fromList xs == fromList (f <$> xs)" "refFmap" refFmap,
      testPropertyNamed "toList . fromList = id" "refToListFromList" refToListFromList,
      testPropertyNamed "toList . freeze . fromList = id" "refFreeze" refFreeze,
      testPropertyNamed "dup2 produces identical arrays" "refDupable" refDupable,
      -- Regression tests
      testPropertyNamed "do not reorder reads and writes" "readAndWriteTest" readAndWriteTest,
      testPropertyNamed "do not evaluate values unnecesesarily" "strictnessTest" strictnessTest
    ]
  
  -- # Internal Library
  --------------------------------------------------------------------------------
  
  type ArrayTester = Array.Array Int %1 -> Ur (TestT IO ())
  
  nonEmptyList :: Gen [Int]
  nonEmptyList = Gen.list (Range.linear 1 1000) value
  
  list :: Gen [Int]
  list = Gen.list (Range.linear 0 1000) value
  
  -- | A random value
  value :: Gen Int
  value = Gen.int (Range.linear (-1000) 1000)
  
  compInts ::
    Ur Int %1 ->
    Ur Int %1 ->
    Ur (TestT IO ())
  compInts (Ur x) (Ur y) = Ur (x === y)
  
  -- XXX: This is a terrible name
  getFst :: (Consumable b) => (a, b) %1 -> a
  getFst (a, b) = lseq b a
  
  -- # Tests
  --------------------------------------------------------------------------------
  
  readAlloc :: Property
  readAlloc = property $ do
    size <- forAll $ Gen.int $ Range.linear 1 1000
    val <- forAll value
    ix <- forAll $ Gen.element [0 .. size - 1]
    test $ unur Linear.$ Array.alloc size val (readAllocTest ix val)
  
  readAllocTest :: Int -> Int -> ArrayTester
  readAllocTest ix val arr = compInts (getFst (Array.read arr ix)) (move val)
  
  readResize :: Property
  readResize = property $ do
    l <- forAll nonEmptyList
    let size = length l
    newSize <- forAll $ Gen.element [1 .. (size * 4)]
    ix <- forAll $ Gen.element [0 .. (min size newSize) - 1]
    let tester = readResizeTest newSize ix
    test $ unur Linear.$ Array.fromList l tester
  
  readResizeTest :: Int -> Int -> ArrayTester
  readResizeTest size ix arr =
    Array.read arr ix
      Linear.& \(Ur old, arr) ->
        Array.resize size 42 arr
          Linear.& \arr ->
            Array.read arr ix
              Linear.& getFst
              Linear.& \(Ur new) -> Ur (old === new)
  
  readWrite1 :: Property
  readWrite1 = property $ do
    l <- forAll nonEmptyList
    let size = length l
    ix <- forAll $ Gen.element [0 .. size - 1]
    val <- forAll value
    let tester = readWrite1Test ix val
    test $ unur Linear.$ Array.fromList l tester
  
  readWrite1Test :: Int -> Int -> ArrayTester
  readWrite1Test ix val arr =
    compInts (move val) (getFst Linear.$ Array.read (Array.write arr ix val) ix)
  
  readWrite2 :: Property
  readWrite2 = property $ do
    let list = Gen.list (Range.linearFrom 2 2 1000) value
    l <- forAll list
    let size = length l
    ix <- forAll $ Gen.element [0 .. size - 1]
    jx <- forAll $ Gen.element [z | z <- [0 .. size - 1], z /= ix]
    val <- forAll value
    let tester = readWrite2Test ix jx val
    test $ unur Linear.$ Array.fromList l tester
  
  readWrite2Test :: Int -> Int -> Int -> ArrayTester
  readWrite2Test ix jx val arr = fromRead (Array.read arr ix)
    where
      fromRead ::
        (Ur Int, Array.Array Int) %1 -> Ur (TestT IO ())
      fromRead (val1, arr) =
        compInts
          val1
          (getFst Linear.$ Array.read (Array.write arr jx val) ix)
  
  allocBeside :: Property
  allocBeside = property $ do
    l <- forAll nonEmptyList
    let size = length l
    newSize <- forAll $ Gen.element [size .. (size * 4)]
    val <- forAll value
    ix <- forAll $ Gen.element [0 .. newSize - 1]
    let tester = allocBesideTest newSize val ix
    test $ unur Linear.$ Array.fromList l tester
  
  allocBesideTest :: Int -> Int -> Int -> ArrayTester
  allocBesideTest newSize val ix arr =
    Array.allocBeside newSize val arr
      Linear.& getFst
      Linear.& \arr ->
        Array.read arr ix
          Linear.& getFst
          Linear.& compInts (move val)
  
  lenAlloc :: Property
  lenAlloc = property $ do
    size <- forAll $ Gen.int $ Range.linear 0 1000
    val <- forAll value
    test $ unur Linear.$ Array.alloc size val (lenAllocTest size)
  
  lenAllocTest :: Int -> ArrayTester
  lenAllocTest size arr =
    compInts (move size) (getFst Linear.$ Array.size arr)
  
  lenWrite :: Property
  lenWrite = property $ do
    l <- forAll nonEmptyList
    let size = length l
    val <- forAll value
    ix <- forAll $ Gen.element [0 .. size - 1]
    let tester = lenWriteTest size val ix
    test $ unur Linear.$ Array.fromList l tester
  
  lenWriteTest :: Int -> Int -> Int -> ArrayTester
  lenWriteTest size val ix arr =
    compInts
      (move size)
      (getFst Linear.$ Array.size (Array.write arr ix val))
  
  lenResizeSeed :: Property
  lenResizeSeed = property $ do
    l <- forAll list
    let size = length l
    val <- forAll value
    newSize <- forAll $ Gen.element [size .. (size * 4)]
    let tester = lenResizeSeedTest newSize val
    test $ unur Linear.$ Array.fromList l tester
  
  lenResizeSeedTest :: Int -> Int -> ArrayTester
  lenResizeSeedTest newSize val arr =
    compInts
      (move newSize)
      (getFst Linear.$ Array.size (Array.resize newSize val arr))
  
  writeRef :: Property
  writeRef = property $ do
    l <- forAll nonEmptyList
    v <- forAll value
    ix <- forAll $ Gen.int $ Range.linear 0 (List.length l - 1)
    let l' = List.take ix l ++ [v] ++ List.drop (ix + 1) l
    l' === unur (Array.fromList l (Array.toList Linear.. Array.set ix v))
  
  readRef :: Property
  readRef = property $ do
    l <- forAll nonEmptyList
    ix <- forAll $ Gen.int $ Range.linear 0 (length l - 1)
    (l List.!! ix) === (unur (Array.fromList l (getFst Linear.. Array.get ix)))
  
  sizeRef :: Property
  sizeRef = property $ do
    l <- forAll list
    length l === (unur (Array.fromList l (getFst Linear.. Array.size)))
  
  resizeRef :: Property
  resizeRef = property $ do
    l <- forAll list
    n <- forAll $ Gen.int (Range.linear 0 (length l * 2))
    x <- forAll value
    let expected = take n $ l ++ repeat x
        actual =
          unur Linear.. Array.fromList l Linear.$ \arr ->
            Array.resize n x arr
              Linear.& Array.toList
    actual === expected
  
  refToListFromList :: Property
  refToListFromList = property $ do
    xs <- forAll list
    let Ur actual = Array.fromList xs Array.toList
    xs === actual
  
  sliceRef :: Property
  sliceRef = property $ do
    xs <- forAll list
    s <- forAll $ Gen.int (Range.linear 0 (length xs))
    n <- forAll $ Gen.int (Range.linear 0 (length xs - s))
    let expected = take n . drop s $ xs
        Ur actual =
          Array.fromList xs Linear.$ \arr ->
            Array.slice s n arr
              Linear.& \(old, new) ->
                old `lseq` Array.toList new
    expected === actual
  
  refFmap :: Property
  refFmap = property $ do
    xs <- forAll list
    let -- An arbitrary function
        f :: Int %1 -> Bool
        f = (Linear.> 0)
        expected = map (Linear.forget f) xs
        Ur actual =
          Array.fromList xs Linear.$ \arr ->
            Array.toList (f Data.<$> arr)
    expected === actual
  
  refFreeze :: Property
  refFreeze = property $ do
    xs <- forAll list
    let Ur vec = Array.fromList xs Array.freeze
    xs === Vector.toList vec
  
  refDupable :: Property
  refDupable = property $ do
    xs <- forAll list
    let Ur (r1, r2) =
          Array.fromList xs Linear.$ \arr ->
            dup2 arr Linear.& \(arr1, arr2) ->
              Array.toList arr1 Linear.& \(Ur l1) ->
                Array.toList arr2 Linear.& \(Ur l2) ->
                  Ur (l1, l2)
    xs === r1
    xs === r2
  
  -- https://github.com/tweag/linear-base/pull/135
  readAndWriteTest :: Property
  readAndWriteTest =
    withTests 1 . property $
      unur (Array.fromList "a" test) === 'a'
    where
      test :: Array.Array Char %1 -> Ur Char
      test arr =
        Array.read arr 0 Linear.& \(before, arr') ->
          Array.write arr' 0 'b' Linear.& \arr'' ->
            arr'' `Linear.lseq` before
  
  -- https://github.com/tweag/linear-base/issues/142
  strictnessTest :: Property
  strictnessTest =
    withTests 1 . property $
      unur (Array.fromList [()] test) === ()
    where
      test :: Array.Array () %1 -> Ur ()
      test arr =
        Array.write arr 0 (error "this should not be evaluated") Linear.& \arr ->
          Array.read arr 0 Linear.& \(Ur _, arr) ->
            arr `Linear.lseq` Ur ()
  