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.)

[RyanGlScott]

Can you include a comment here saying why we need a special case for k == length a? It wasn't obvious to me until I read the PR description.

[RyanGlScott]

Relatedly, I wonder if Copilot.Language.Reify if the right place to implement this transformation. Most of the simplifications that are performed over Drop streams are implemented in the drop function itself:

copilot/copilot-language/src/Copilot/Language/Operators/Temporal.hs

Lines 35 to 39 in e042933

	drop :: Typed a => Int -> Stream a -> Stream a
	drop 0 s = s
	drop _ ( Const j ) = Const j
	drop i ( Drop j s ) = Drop (fromIntegral i + j) s
	drop i s = Drop (fromIntegral i) s

Perhaps we should implement this transformation as an additional case of drop?

drop i ( Append a _ s ) | i == length a = s

[ivanperez-keera]

Not part of this issue, but that might be a good place to also do something like:

drop i (Op1 op s)     = Op1 op (drop i s)
drop i (Op2 op s1 s2) = Op2 op (drop i s1) (drop i s2)

[strikef]

I agree that Reify module isn't the best place to implement this fix. The Temporal module you recommended looks better to me as well.

My initial intent of this change was getting correct C code (which is why I placed this fix at Reify module), and at that time simplification was just a 'nice' side-effect. But now that you mentioned, I don't see any reason to not treat it as simplification.
I'll move my fix to Temporal module and add explanatory comment as well.

[strikef]

Fixed as suggested

[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.