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

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

data S = S { S -> Field "field" Int16
field :: Field "field" Int16 }

instance Struct S where
  typeName :: S -> String
typeName S
_ = String
"s"
  toValues :: S -> [Value S]
toValues S
s = [Type Int16 -> Field "field" Int16 -> Value S
forall a (s :: Symbol) t.
(Typeable t, KnownSymbol s, Show t) =>
Type t -> Field s t -> Value a
Value Type Int16
Int16 (S -> Field "field" Int16
field S
s)]

instance Typed S where
  typeOf :: Type S
typeOf = S -> Type S
forall a. (Typed a, Struct a) => a -> Type a
Struct (Field "field" Int16 -> S
S (Int16 -> Field "field" Int16
forall (s :: Symbol) t. t -> Field s t
Field Int16
0))

spec :: Spec
spec :: Spec
spec = String -> Stream Bool -> [Arg] -> Spec
trigger String
"f" ((Stream (Array 2 S)
stream Stream (Array 2 S) -> Stream Word32 -> Stream S
forall (n :: Nat) t.
(KnownNat n, Typed t) =>
Stream (Array n t) -> Stream Word32 -> Stream t
! Stream Word32
0)Stream S -> (S -> Field "field" Int16) -> Stream Int16
forall (f :: Symbol) t s.
(KnownSymbol f, Typed t, Typed s, Struct s) =>
Stream s -> (s -> Field f t) -> Stream t
#S -> Field "field" Int16
field Stream Int16 -> Stream Int16 -> Stream Bool
forall a. (Eq a, Typed a) => Stream a -> Stream a -> Stream Bool
== Stream Int16
27) [Stream (Array 2 S) -> Arg
forall a. Typed a => Stream a -> Arg
arg Stream (Array 2 S)
stream]
  where
    stream :: Stream (Array 2 S)
    stream :: Stream (Array 2 S)
stream = [[S] -> Array 2 S
forall (n :: Nat) t. KnownNat n => [t] -> Array n t
array [Field "field" Int16 -> S
S (Int16 -> Field "field" Int16
forall (s :: Symbol) t. t -> Field s t
Field Int16
27), Field "field" Int16 -> S
S (Int16 -> Field "field" Int16
forall (s :: Symbol) t. t -> Field s t
Field Int16
42)]] [Array 2 S] -> Stream (Array 2 S) -> Stream (Array 2 S)
forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream (Array 2 S)
stream

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
"arrayOfStructs" Spec
spec'