Add example testing Copilot-Language/copilot#386

Copilot-Language · Jan 8, 2023 · c6eef4a · c6eef4a
1 parent ce4aa73
commit c6eef4a
Show file tree

Hide file tree

Showing 3 changed files with 24 additions and 0 deletions.
diff --git a/copilot-verifier/copilot-verifier.cabal b/copilot-verifier/copilot-verifier.cabal
@@ -80,6 +80,7 @@ library copilot-verifier-examples
     Copilot.Verifier.Examples.ShouldFail.Partial.SubSignedWrap
 
     Copilot.Verifier.Examples.ShouldPass.Array
+    Copilot.Verifier.Examples.ShouldPass.ArrayGen
     Copilot.Verifier.Examples.ShouldPass.ArrayOfStructs
     Copilot.Verifier.Examples.ShouldPass.Arith
     Copilot.Verifier.Examples.ShouldPass.Clock

diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples.hs b/copilot-verifier/examples/Copilot/Verifier/Examples.hs
@@ -21,6 +21,7 @@ import qualified Copilot.Verifier.Examples.ShouldFail.Partial.ShiftLTooLarge   a
 import qualified Copilot.Verifier.Examples.ShouldFail.Partial.ShiftRTooLarge   as Fail.ShiftRTooLarge
 import qualified Copilot.Verifier.Examples.ShouldFail.Partial.SubSignedWrap    as Fail.SubSignedWrap
 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.Arith                    as Arith
 import qualified Copilot.Verifier.Examples.ShouldPass.Clock                    as Clock
@@ -59,6 +60,7 @@ shouldFailExamples verb = Map.fromList
 shouldPassExamples :: Verbosity -> Map (CI Text) (IO ())
 shouldPassExamples verb = Map.fromList
     [ example "Array" (Array.verifySpec verb)
+    , example "ArrayGen" (ArrayGen.verifySpec verb)
     , example "ArrayOfStructs" (ArrayOfStructs.verifySpec verb)
     , example "Arith" (Arith.verifySpec verb)
     , example "Clock" (Clock.verifySpec verb)

diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/ArrayGen.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/ArrayGen.hs
@@ -0,0 +1,21 @@
+{-# 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 = trigger "f" (stream .!! 0 > 0) [arg stream]
+  where
+    stream :: Stream (Array 2 Int16)
+    stream = [array [3,4]] ++ rest
+
+    rest :: Stream (Array 2 Int16)
+    rest = constant $ array [5,6]
+
+verifySpec :: Verbosity -> IO ()
+verifySpec verb = reify spec >>= verifyWithOptions defaultVerifierOptions{verbosity = verb}
+                                                   mkDefaultCSettings [] "arrayGen"