Permalink
Browse files

Very small regression test.

  • Loading branch information...
1 parent b649f42 commit f71944577e99be7c919a269b958c6ba1968bba3f @leepike committed Nov 3, 2011
Showing with 123 additions and 0 deletions.
  1. +123 −0 Tests/Test.hs
View
@@ -0,0 +1,123 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+-- | A very small test suite to check for basic functionality.
+
+{-# LANGUAGE RebindableSyntax #-}
+
+module Main where
+
+import qualified Prelude as P
+import Language.Copilot hiding (even, odd)
+import Copilot.Compile.C99
+
+--------------------------------------------------------------------------------
+
+--
+-- Some utility functions:
+--
+
+flipflop :: Stream Bool -> Stream Bool
+flipflop x = y
+ where
+ y = [False] ++ if x then not y else y
+
+nats :: Stream Word64
+nats = [0] ++ nats + 1
+
+even :: (P.Integral a, Typed a) => Stream a -> Stream Bool
+even x = x `mod` 2 == 0
+
+odd :: (P.Integral a, Typed a) => Stream a -> Stream Bool
+odd = not . even
+
+counter :: (Num a, Typed a) => Stream Bool -> Stream a
+counter reset = y
+ where
+ zy = [0] ++ y
+ y = if reset then 0 else zy + 1
+
+booleans :: Stream Bool
+booleans = [True, True, False] ++ booleans
+
+fib :: Stream Word64
+fib = [1, 1] ++ fib + drop 1 fib
+
+bitWise :: Stream Word8
+bitWise = ( let a = [ 1, 1, 0 ] ++ a in a )
+ .^.
+ ( let b = [ 0, 1, 1 ] ++ b in b )
+
+sumExterns :: Stream Word64
+sumExterns =
+ let
+ ex1 = extern "e1"
+ ex2 = extern "e2"
+ in
+ ex1 + ex2
+
+--------------------------------------------------------------------------------
+
+--
+-- An example of a complete copilot specification.
+
+
+-- A specification:
+spec :: Spec
+spec =
+ do
+ -- A trigger with four arguments:
+ trigger "e" booleans
+ [ arg fib, arg nats, arg sumExterns, arg bitWise ]
+
+ -- A trigger with two arguments:
+ trigger "f" booleans
+ [ arg fib, arg sumExterns ]
+
+ -- A trigger with a single argument:
+ trigger "g" (flipflop booleans)
+ [ arg (sumExterns + counter false + 25) ]
+
+ -- A trigger with a single argument (should never fire):
+ trigger "h" (extern "e3" /= fib)
+ [ arg (0 :: Stream Int8) ]
+
+ observer "i" (odd nats)
+
+--- Some infinite lists for simulating external variables:
+e1, e2, e3 :: [Word64]
+e1 = [0..]
+e2 = 5 : 4 : e2
+e3 = [1, 1] P.++ zipWith (+) e3 (P.drop 1 e3)
+
+main :: IO ()
+main = do
+ putStrLn "PrettyPrinter:"
+ putStrLn ""
+ prettyPrint spec
+ putStrLn ""
+ putStrLn ""
+ putStrLn "Interpreter:"
+ putStrLn ""
+ interpret 10 [input "e1" e1, input "e2" e2, input "e3" e3] spec
+ putStrLn ""
+ putStrLn ""
+ putStrLn "Atom compilation:"
+ reify spec >>= compile defaultParams
+ cleanup
+
+ -- Don't assume SBV is installed.
+ -- putStrLn "Check equivalence:"
+ -- putStrLn ""
+ -- putStrLn ""
+ -- reify spec >>=
+ -- C.genCBMC C.defaultParams {C.numIterations = 20}
+
+--------------------------------------------------------------------------------
+
+cleanUp :: IO ()
+cleanUp = do
+ removeFile "copilot.c"
+ removeFile "copilot.h"
+ return ()

0 comments on commit f719445

Please sign in to comment.