copilot icon indicating copy to clipboard operation
copilot copied to clipboard

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

Open strikef opened this issue 9 months ago • 1 comments

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 avatar Mar 11 '25 06:03 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

https://github.com/Copilot-Language/copilot/blob/e0429336689613f7e7788e3c8589414e2ab43608/copilot-language/src/Copilot/Language/Analyze.hs#L191 It appears that analyzeDrop is throwing DropIndexOverflow even when |drop| == |append|. Could this be the culprit?

strikef avatar Mar 12 '25 01:03 strikef