{-# LANGUAGE DataKinds #-}
module Copilot.Verifier.Examples.ShouldPass.ArrayGen where

import Copilot.Compile.C99
import Copilot.Verifier ( Verbosity, VerifierOptions(..)
                        , defaultVerifierOptions, verifyWithOptions )
import Language.Copilot
import qualified Prelude hiding ((++), (>))

spec :: Spec
spec :: Spec
spec = String -> Stream Bool -> [Arg] -> Spec
trigger String
"f" (Stream (Array 2 Int16)
stream Stream (Array 2 Int16) -> Stream Word32 -> Stream Int16
forall (n :: Nat) t.
(KnownNat n, Typed t) =>
Stream (Array n t) -> Stream Word32 -> Stream t
! Stream Word32
0 Stream Int16 -> Stream Int16 -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
> Stream Int16
0) [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 = [[Int16] -> Array 2 Int16
forall (n :: Nat) t. KnownNat n => [t] -> Array n t
array [Int16
3,Int16
4]] [Array 2 Int16] -> Stream (Array 2 Int16) -> Stream (Array 2 Int16)
forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream (Array 2 Int16)
rest

    rest :: Stream (Array 2 Int16)
    rest :: Stream (Array 2 Int16)
rest = Array 2 Int16 -> Stream (Array 2 Int16)
forall a. Typed a => a -> Stream a
constant (Array 2 Int16 -> Stream (Array 2 Int16))
-> Array 2 Int16 -> Stream (Array 2 Int16)
forall a b. (a -> b) -> a -> b
$ [Int16] -> Array 2 Int16
forall (n :: Nat) t. KnownNat n => [t] -> Array n t
array [Int16
5,Int16
6]

verifySpec :: Verbosity -> IO ()
verifySpec :: Verbosity -> IO ()
verifySpec Verbosity
verb = Spec -> IO Spec
forall a. Spec' a -> IO Spec
reify Spec
spec IO Spec -> (Spec -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= VerifierOptions -> CSettings -> [String] -> String -> Spec -> IO ()
verifyWithOptions VerifierOptions
defaultVerifierOptions{verbosity = verb}
                                                   CSettings
mkDefaultCSettings [] String
"arrayGen"