module Copilot.Compile.SBV.Queue
( Queue(..)
, lookahead
, QueueSize
) where
import Prelude hiding (id, rem)
import qualified Data.SBV as S
import Copilot.Core.Expr (DropIdx)
import Copilot.Core.Error (impossible)
type QueueSize = DropIdx
data Queue a = Queue
{ queue :: [a] }
lookahead :: (S.SymWord a) => DropIdx -> [S.SBV a] -> S.SBV QueueSize -> S.SBV a
lookahead i buf ptr =
let sz = fromIntegral $ length buf in
let (_, rem) = (ptr + fromIntegral i) `S.sQuotRem` sz in
let defaultVal = if null buf
then impossible "lookahead" "copilot-sbv"
else head buf in
S.select buf defaultVal rem