Permalink
Browse files

Major update of examples, fixing them up. Not done!

  • Loading branch information...
1 parent 9836093 commit 77885d85c9dd19017a16fc524edc3b6da0046822 @leepike committed Dec 31, 2011
View
@@ -2,44 +2,35 @@
-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
--------------------------------------------------------------------------------
--- |
+-- | Another small example.
-module Main where
+module AddMult ( addMult ) where
-import qualified Prelude as P
+import Prelude ()
import Copilot.Language
import Copilot.Language.Prelude
--------------------------------------------------------------------------------
-addMult :: Spec
-addMult =
- do
- let_ "v" summation
- trigger "f" true [ arg $ mult 5 ]
+spec :: Spec
+spec =
+ trigger "f" true [ arg $ mult 5 ]
where
+ mult :: Word64 -> Stream Word64
+ mult 0 = 1
+ mult i = constant i * mult (i-1)
+
+addMult :: IO ()
+addMult = do
+ putStrLn "PrettyPrinter:"
+ putStrLn ""
+ prettyPrint spec
+ putStrLn ""
+ putStrLn ""
+ putStrLn "Interpreter:"
+ putStrLn ""
+ interpret 100 spec
- summation = nats + nats + nats
- mult :: Int -> Stream Word64
- mult 0 = var "v"
- mult i = var "v" * mult (i-1)
-
- nats :: Stream Word64
- nats = [0] ++ nats + 1
-
-main :: IO ()
-main =
- do
- putStrLn "PrettyPrinter:"
- putStrLn ""
- prettyPrint addMult
- putStrLn ""
- putStrLn ""
- putStrLn "Interpreter:"
- putStrLn ""
- interpret 100 [] addMult
-
-
---------------------------------------------------------------------------------
+--------------------------------------------------------------------------------
View
@@ -6,7 +6,7 @@
-- Examples of casting types.
-module Main where
+module Cast ( castEx ) where
import Language.Copilot hiding (even, odd)
import Copilot.Compile.C99
@@ -26,7 +26,7 @@ y = 1 + cast x
spec :: Spec
spec = trigger "trigger" true [arg y, arg i]
-main :: IO ()
-main = do
- interpret 10 [] spec
+castEx :: IO ()
+castEx = do
+ interpret 10 spec
reify spec >>= compile defaultParams
View
@@ -1,19 +1,15 @@
-- | Clocks library tests.
-module Copilot.Examples.ClockExamples where
+module ClockExamples ( clockExamples ) where
-
-import Prelude ( ($), putStrLn )
-import qualified Prelude as P
+import Prelude ( putStrLn, IO, Bool )
import Copilot.Language
import Copilot.Library.Clocks
-import Data.Bool
-import Data.List ( replicate )
-
-
-p = 5 :: Word8
+p :: Word8
+p = 5
+clkStream, clk1Stream :: Stream Bool
clkStream = clk ( period p ) ( phase 0 )
clk1Stream = clk1 ( period p ) ( phase 0 )
@@ -24,8 +20,9 @@ clockTest = do
observer "clk1" clk1Stream
-test = do
+clockExamples :: IO ()
+clockExamples = do
prettyPrint clockTest
putStrLn ""
putStrLn ""
- interpret 10 [] clockTest
+ interpret 10 clockTest
View
@@ -4,11 +4,11 @@
{-# LANGUAGE RebindableSyntax #-}
-module Main where
+module EngineExample ( engineExample ) where
import Language.Copilot
-import qualified Copilot.Compile.SBV as S
import qualified Prelude as P
+--import qualified Copilot.Compile.SBV as S
{-
"If the majority of the engine temperature probes exeeds 250 degrees, then the
@@ -19,24 +19,22 @@ import qualified Prelude as P
engineMonitor :: Spec
engineMonitor = do
trigger "shutoff" (not ok) [arg maj]
+
where
- vals = map externW8 ["tmp_probe_0", "tmp_probe_1", "tmp_probe_2"]
+ vals = [ externW8 "tmp_probe_0" two51
+ , externW8 "tmp_probe_1" two51
+ , externW8 "tmp_probe_2" zero]
exceed = map (> 250) vals
maj = majority exceed
checkMaj = aMajority exceed maj
- ok = alwaysBeen ((maj && checkMaj) ==> extern "cooler")
-
-main :: IO ()
-main =
- interpret
- 10
- [ var "cooler" cooler, var "tmp_probe_0" two51
- , var "tmp_probe_1" two51, var "tmp_probe_2" zero]
- engineMonitor
- where
- two51 = [251, 251] P.++ repeat (250 :: Word8)
- zero = repeat (0 :: Word8)
- cooler = [True, True] P.++ repeat False
+ ok = alwaysBeen ((maj && checkMaj) ==> extern "cooler" cooler)
+
+ two51 = Just $ [251, 251] P.++ repeat (250 :: Word8)
+ zero = Just $ repeat (0 :: Word8)
+ cooler = Just $ [True, True] P.++ repeat False
+
+engineExample :: IO ()
+engineExample = interpret 10 engineMonitor
-- reify engineMonitor >>= S.compile (S.Params { S.prefix = Just "engine" })
View
@@ -6,7 +6,7 @@
{-# LANGUAGE RebindableSyntax #-}
-module Main where
+module Examples ( examples ) where
import qualified Prelude as P
import Language.Copilot hiding (even, odd)
@@ -18,10 +18,36 @@ import qualified Copilot.Tools.CBMC as C
-- Some utility functions:
--
+{-
implyStream :: Stream Bool -> Stream Bool -> Stream Bool
implyStream p q = not p || q
+
+extEven :: Stream Bool
+extEven = externX `mod` 2 == 0
+
+oddSpec :: Spec
+oddSpec = trigger "f" true [arg (odd nats)]
+
+prop :: Stream Bool
+prop = (x - x') <= 5 && (x - x') <= (-5)
+ where
+ x :: Stream Int32
+ x = [0] ++ cast externX
+ x' = drop 1 x
+
+externX :: Stream Int8
+externX = extern "x" (Just [0..])
+
+foo :: Spec
+foo = do
+ let x = cast externX :: Stream Int16
+ trigger "trigger" true [arg $ x < 3]
+ observer "debug_x" x
+
+-}
+
flipflop :: Stream Bool -> Stream Bool
flipflop x = y
where
@@ -36,9 +62,6 @@ even x = x `mod` 2 == 0
odd :: (P.Integral a, Typed a) => Stream a -> Stream Bool
odd = not . even
-extEven :: Stream Bool
-extEven = externI64 "x" `mod` 2 == 0
-
counter :: (Num a, Typed a) => Stream Bool -> Stream a
counter reset = y
where
@@ -58,23 +81,14 @@ bitWise = ( let a = [ 1, 1, 0 ] ++ a in a )
sumExterns :: Stream Word64
sumExterns =
- let ex1 = extern "e1"
- ex2 = extern "e2"
+ let ex1 = extern "e1" (Just e1)
+ ex2 = extern "e2" (Just e2)
in ex1 + ex2
-oddSpec :: Spec
-oddSpec = trigger "f" true [arg (odd nats)]
-
-prop :: Stream Bool
-prop = (x - x') <= 5 && (x - x') <= (-5)
- where
- x = [0] ++ externI32 "x"
- x' = drop 1 x
-
-foo = do
- let x = externW8 "x"
- trigger "trigger" true [arg $ x < 3]
- observer "debug_x" x
+--- Some infinite lists for simulating external variables:
+e1, e2 :: [Word64]
+e1 = [0..]
+e2 = 5 : 4 : e2
--------------------------------------------------------------------------------
@@ -84,8 +98,7 @@ foo = do
-- A specification:
spec :: Spec
-spec =
- do
+spec = do
-- A trigger with four arguments:
trigger "e" true -- booleans
@@ -102,36 +115,30 @@ spec =
-- [ arg (counter false + 25 :: Stream Int32) ]
-- A trigger with a single argument (should never fire):
- trigger "h" (extern "e3" /= fib)
+ let e3 = [1, 1] P.++ zipWith (+) e3 (P.drop 1 e3)
+ trigger "h" (extern "e3" (Just 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 [var "e1" e1, var "e2" e2, var "e3" e3] spec
- putStrLn ""
- putStrLn ""
- putStrLn "Atom:"
- reify spec >>= compile defaultParams
- putStrLn "Check equivalence:"
- putStrLn ""
- putStrLn ""
- reify spec >>=
- C.genCBMC C.defaultParams {C.numIterations = 20}
+examples :: IO ()
+examples = do
+ putStrLn "PrettyPrinter:"
+ putStrLn ""
+ prettyPrint spec
+ putStrLn ""
+ putStrLn ""
+ putStrLn "Interpreter:"
+ putStrLn ""
+ interpret 10 spec
+ putStrLn ""
+ putStrLn ""
+ putStrLn "Atom:"
+ reify spec >>= compile defaultParams
+ putStrLn "Check equivalence:"
+ putStrLn ""
+ putStrLn ""
+ reify spec >>=
+ C.genCBMC C.defaultParams {C.numIterations = 20}
--------------------------------------------------------------------------------
View
@@ -0,0 +1,60 @@
+module Examples2 ( examples2 ) where
+
+import Prelude ()
+
+import Copilot.Language.Prelude
+import Copilot.Language
+import Copilot.Language.Reify (reify)
+
+import qualified Copilot.Compile.SBV as S
+
+import Data.List (cycle)
+
+--------------------------------------------------------------------------------
+
+nats :: Stream Word64
+nats = [0] ++ nats + 1
+
+alt :: Stream Bool
+alt = [True] ++ not alt
+
+{-
+alt2 :: Stream Word64
+alt2 = [0,1,2] ++ alt2 + 1
+
+alt3 :: Stream Bool
+alt3 = [True,True,False] ++ alt3
+
+fib' :: Stream Word64
+fib' = [0, 1] ++ fib' + drop 1 fib
+-}
+
+fib :: Stream Word64
+fib = [0, 1] ++ fib + drop 1 fib
+
+logic :: Stream Bool
+logic = [True, False] ++ logic || drop 1 logic
+
+sumExterns :: Stream Word64
+sumExterns =
+ let
+ e1 = extern "e1" (Just [0..])
+ e2 = extern "e2" (Just $ cycle [2,3,4])
+ in
+ e1 + e2 + e1
+
+spec :: Spec
+spec = do
+ trigger "trig1" alt [ arg $ nats < 3
+ , arg sumExterns
+ , arg logic
+ ]
+
+fibSpec :: Spec
+fibSpec = do
+ trigger "fib_out" true [arg fib]
+
+examples2 :: IO ()
+examples2 = do
+ reify fibSpec >>= S.compile S.defaultParams
+ reify spec >>= S.compile S.defaultParams
Oops, something went wrong.

0 comments on commit 77885d8

Please sign in to comment.