--------------------------------------------------------------------------------
-- Copyright © 2019 National Institute of Aerospace / Galois, Inc.
--------------------------------------------------------------------------------

-- | This is a simple example for arrays. As a program, it does not make much
-- sense, however it shows of the features of arrays nicely.

-- | Enable compiler extension for type-level data, necesary for the array
-- length.

{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE DataKinds        #-}

module Copilot.Verifier.Examples.ShouldPass.Array where

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

-- Lets define an array of length 2.
-- Make the buffer of the streams 3 elements long.
arr :: Stream (Array 2 Bool)
arr :: Stream (Array 2 Bool)
arr = [ [Bool] -> Array 2 Bool
forall (n :: Nat) t. KnownNat n => [t] -> Array n t
array [Bool
True, Bool
False]
      , [Bool] -> Array 2 Bool
forall (n :: Nat) t. KnownNat n => [t] -> Array n t
array [Bool
True, Bool
True]
      , [Bool] -> Array 2 Bool
forall (n :: Nat) t. KnownNat n => [t] -> Array n t
array [Bool
False, Bool
False]] [Array 2 Bool] -> Stream (Array 2 Bool) -> Stream (Array 2 Bool)
forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream (Array 2 Bool)
arr

spec :: Spec
spec :: Spec
spec = do
  -- A trigger that fires 'func' when the first element of 'arr' is True.
  -- It passes the current value of arr as an argument.
  -- The prototype of 'func' would be:
  -- void func (int8_t arg[3]);
  String -> Stream Bool -> [Arg] -> Spec
trigger String
"func" (Stream (Array 2 Bool)
arr Stream (Array 2 Bool) -> Stream Word32 -> Stream Bool
forall (n :: Nat) t.
(KnownNat n, Typed t) =>
Stream (Array n t) -> Stream Word32 -> Stream t
! Stream Word32
0) [Stream (Array 2 Bool) -> Arg
forall a. Typed a => Stream a -> Arg
arg Stream (Array 2 Bool)
arr]

-- Compile the spec
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
"array"
-- verifySpec _ = interpret 30 spec