Allow appending and then dropping the same number of elements from Stream

[strikef]

https://hackage.haskell.org/package/copilot-language-4.3/docs/Copilot-Language-Operators-Temporal.html#v:drop

The elements must be realizable at the present time to be able to drop elements. For most kinds of streams, you cannot drop elements without prepending an equal or greater number of elements to them first, as it could result in undefined samples.

Current specification states that one may drop the elements from the stream as long as you have appended at least the same number of elements. But the current implementation throws DropIndexOverflow when you try to drop as many elements as appended.

By modifying analyzeDrop we can avoid exception, but copilot would emit incorrect C code from Drop k (Append k s). This is because Append k s emits an array of length k, but Drop k s gets converted to index k access, which becomes incorrect when drop length and append length are the same. So I also modified the Reify module s.t. Drop k (Append k s) can be simplified to s. This way we can achieve both correct C codegen & reduced constructor chain.

This modification has been verified using copilot-verifier using several homegrown test cases.

[ivanperez-keera]

Tagging @fdedden and @RyanGlScott so that they take a look.

[RyanGlScott]

Good catch! Here is a concrete test case that demonstrates the bug in action:

{-# LANGUAGE NoImplicitPrelude #-}
module Main (main) where

import Language.Copilot

spec :: Spec
spec = do
  let s :: Stream Bool
      s = drop 2 ([False, False] ++ true)
  trigger "example" s [arg s]

main :: IO ()
main = interpret 5 spec

Intuitively, I would expect drop 2 ([False, False] ++ true) to be equivalent to true, but in practice, Copilot rejects this with an error:

$ runghc Bug.hs
Bug.hs: Copilot error: Drop index overflow!
CallStack (from HasCallStack):
  error, called at src/Copilot/Language/Error.hs:24:16 in copilot-language-4.3-inplace:Copilot.Language.Error

On the other hand, drop 1 ([False, False] ++ true) does not throw an error. As such, I think your suggested fix of using k > length xs is apt.

(It would be helpful to include something like the program above as a test case.)

[strikef]

Good catch! Here is a concrete test case that demonstrates the bug in action:

{-# LANGUAGE NoImplicitPrelude #-}
module Main (main) where

import Language.Copilot

spec :: Spec
spec = do
  let s :: Stream Bool
      s = drop 2 ([False, False] ++ true)
  trigger "example" s [arg s]

main :: IO ()
main = interpret 5 spec

Intuitively, I would expect drop 2 ([False, False] ++ true) to be equivalent to true, but in practice, Copilot rejects this with an error:

$ runghc Bug.hs
Bug.hs: Copilot error: Drop index overflow!
CallStack (from HasCallStack):
  error, called at src/Copilot/Language/Error.hs:24:16 in copilot-language-4.3-inplace:Copilot.Language.Error

On the other hand, drop 1 ([False, False] ++ true) does not throw an error. As such, I think your suggested fix of using k > length xs is apt.

(It would be helpful to include something like the program above as a test case.)

Thanks for the review! Could you recommend a module to add such tests? I'm not very familiar with the Copilot source tree yet.

[RyanGlScott]

Could you recommend a module to add such tests?

Since the property of interest is checked in copilot-language, I think it makes sense to add a regression test in the copilot-language test suite. Currently, the copilot-language test suite only contains property-based tests (via QuickCheck), however. We could imagine adding some additional machinery to support a unit test that checks to see if reifying drop 2 [False, False] ++ true throws an exception or not, similar to this unit test in copilot-theorem.

This would take a fair bit of extra work, however, so I'll defer to @ivanperez-keera on whether we want to do all of this as part of this PR.