{-# LANGUAGE DataKinds #-}

-- | A regression test for
-- <https://github.com/Copilot-Language/copilot/issues/431>.
module Copilot.Verifier.Examples.ShouldPass.ArrayTriggerArgument where

import Language.Copilot
import Copilot.Compile.C99
import Copilot.Verifier ( Verbosity, VerifierOptions(..)
                        , defaultVerifierOptions, verifyWithOptions )

spec :: Spec
spec :: Spec
spec = String -> Stream Bool -> [Arg] -> Spec
trigger String
"f" Stream Bool
true [Stream (Array 2 Int16) -> Arg
forall a. Typed a => Stream a -> Arg
arg Stream (Array 2 Int16)
stream]
  where
    stream :: Stream (Array 2 Int16)
    stream :: Stream (Array 2 Int16)
stream = Array 2 Int16 -> Stream (Array 2 Int16)
forall a. Typed a => a -> Stream a
constant ([Int16] -> Array 2 Int16
forall (n :: Nat) t. KnownNat n => [t] -> Array n t
array [Int16
3,Int16
4])

verifySpec :: Verbosity -> IO ()
verifySpec :: Verbosity -> IO ()
verifySpec Verbosity
verb = do
  Spec
spec' <- Spec -> IO Spec
forall a. Spec' a -> IO Spec
reify Spec
spec
  VerifierOptions -> CSettings -> [String] -> String -> Spec -> IO ()
verifyWithOptions
    VerifierOptions
defaultVerifierOptions{verbosity = verb}
    CSettings
mkDefaultCSettings [] String
"arrayTriggerArgument" Spec
spec'