`copilot-language` - Unable to drop as many elements from Stream as prepended

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

Since the document states that prepending 'equal' number of elements suffices, I expected the following code to compile

prependedStream :: Stream Bool
prependedStream = [True, True] ++ false

droppedStream :: Stream Bool
droppedStream = drop 2 prependedStream

However, it fails to compile with the following error:

Copilot error: Drop index overflow!

Why is it that I'm not able to drop the exact same number of elements as I prepended?
Could it be a documentation issue or a bug?

[strikef]

analyzeDrop :: Int -> Stream a -> IO ()
analyzeDrop k (Append xs _ _)
 | k >= length xs = throw DropIndexOverflow
 | k > fromIntegral (maxBound :: DropIdx) = throw DropMaxViolation
 | otherwise = return ()
analyzeDrop _ _ = throw DropAppliedToNonAppend

copilot/copilot-language/src/Copilot/Language/Analyze.hs

Line 191 in e042933

| k >= length xs = throw DropIndexOverflow

It appears that analyzeDrop is throwing DropIndexOverflow even when |drop| == |append|. Could this be the culprit?

[RyanGlScott]

Description

The documentation for copilot-language's drop function claims that one can drop a number of elements from a stream equal to the number of elements prepended to the stream. In practice, this is not the case, and copilot-language's analysis will reject such uses of drop.

Type

• Bug: implementation does not match the documented behavior.

Additional context

None.

Requester

• Ryan Scott (Galois)

Method to check presence of bug

Run the following Copilot specification:

{-# 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

This specification will be rejected with the following error message:

$ 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

Expected result

Running the Copilot specification above should succeed, and the Copilot interpreter should print five true samples.

Desired result

Running the Copilot specification above should succeed, and the Copilot interpreter should print five true samples.

Proposed solution

Modify the implementation of drop to add a special case for when the drop length equals the number of elements prepended to a stream with an Append, which will return the underlying stream.

Further notes

None.