From 9024e6805c19a05064b8892088317d3bd29f7de5 Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Mon, 8 Jan 2024 11:23:10 -0500
Subject: [PATCH] Add regression test for Copilot-Language/copilot#431

---
 copilot-verifier/copilot-verifier.cabal       |  1 +
 .../examples/Copilot/Verifier/Examples.hs     |  2 ++
 .../ShouldPass/ArrayTriggerArgument.hs        | 23 +++++++++++++++++++
 3 files changed, 26 insertions(+)
 create mode 100644 copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/ArrayTriggerArgument.hs

diff --git a/copilot-verifier/copilot-verifier.cabal b/copilot-verifier/copilot-verifier.cabal
index 9ff81a0..60c7275 100644
--- a/copilot-verifier/copilot-verifier.cabal
+++ b/copilot-verifier/copilot-verifier.cabal
@@ -82,6 +82,7 @@ library copilot-verifier-examples
     Copilot.Verifier.Examples.ShouldPass.Array
     Copilot.Verifier.Examples.ShouldPass.ArrayGen
     Copilot.Verifier.Examples.ShouldPass.ArrayOfStructs
+    Copilot.Verifier.Examples.ShouldPass.ArrayTriggerArgument
     Copilot.Verifier.Examples.ShouldPass.Arith
     Copilot.Verifier.Examples.ShouldPass.Clock
     Copilot.Verifier.Examples.ShouldPass.Counter
diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples.hs b/copilot-verifier/examples/Copilot/Verifier/Examples.hs
index 2ee5834..919a047 100644
--- a/copilot-verifier/examples/Copilot/Verifier/Examples.hs
+++ b/copilot-verifier/examples/Copilot/Verifier/Examples.hs
@@ -23,6 +23,7 @@ import qualified Copilot.Verifier.Examples.ShouldFail.Partial.SubSignedWrap    a
 import qualified Copilot.Verifier.Examples.ShouldPass.Array                    as Array
 import qualified Copilot.Verifier.Examples.ShouldPass.ArrayGen                 as ArrayGen
 import qualified Copilot.Verifier.Examples.ShouldPass.ArrayOfStructs           as ArrayOfStructs
+import qualified Copilot.Verifier.Examples.ShouldPass.ArrayTriggerArgument     as ArrayTriggerArgument
 import qualified Copilot.Verifier.Examples.ShouldPass.Arith                    as Arith
 import qualified Copilot.Verifier.Examples.ShouldPass.Clock                    as Clock
 import qualified Copilot.Verifier.Examples.ShouldPass.Counter                  as Counter
@@ -62,6 +63,7 @@ shouldPassExamples verb = Map.fromList
     [ example "Array" (Array.verifySpec verb)
     , example "ArrayGen" (ArrayGen.verifySpec verb)
     , example "ArrayOfStructs" (ArrayOfStructs.verifySpec verb)
+    , example "ArrayTriggerArgument" (ArrayTriggerArgument.verifySpec verb)
     , example "Arith" (Arith.verifySpec verb)
     , example "Clock" (Clock.verifySpec verb)
     , example "Counter" (Counter.verifySpec verb)
diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/ArrayTriggerArgument.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/ArrayTriggerArgument.hs
new file mode 100644
index 0000000..5c06b62
--- /dev/null
+++ b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/ArrayTriggerArgument.hs
@@ -0,0 +1,23 @@
+{-# 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 = trigger "f" true [arg stream]
+  where
+    stream :: Stream (Array 2 Int16)
+    stream = constant (array [3,4])
+
+verifySpec :: Verbosity -> IO ()
+verifySpec verb = do
+  spec' <- reify spec
+  verifyWithOptions
+    defaultVerifierOptions{verbosity = verb}
+    mkDefaultCSettings [] "arrayTriggerArgument" spec'