Skip to content
Fetching contributors…
Cannot retrieve contributors at this time
159 lines (120 sloc) 3.59 KB
--------------------------------------------------------------------------------
-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
--------------------------------------------------------------------------------
-- | Some Copilot examples.
{-# LANGUAGE RebindableSyntax #-}
module Examples ( examples ) where
import qualified Prelude as P
import Language.Copilot hiding (even, odd)
--import Copilot.Compile.C99
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
latch :: Stream Bool -> Stream Bool
latch x = out
where out = if x then not st else st
st = [False] ++ out
latch' :: Stream Bool -> Stream Bool
latch' x = out
where out = x `xor` st
st = [False] ++ out
ext :: Stream Word8
ext = [1] ++ ext + extern "e0" (Just [2,4..])
-}
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 :: (Eq a, 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" (Just e1)
ex2 = extern "e2" (Just e2)
in ex1 + ex2
--- Some infinite lists for simulating external variables:
e1, e2 :: [Word64]
e1 = [0..]
e2 = 5 : 4 : e2
--------------------------------------------------------------------------------
--
-- An example of a complete copilot specification.
--
-- A specification:
spec :: Spec
spec = do
-- A trigger with four arguments:
trigger "e" true -- booleans
[ arg fib, arg nats, arg sumExterns, arg bitWise ]
-- A trigger with two arguments:
trigger "f" booleans
[ arg fib, arg sumExterns ]
-- [ arg fib, arg nats ]
-- A trigger with a single argument:
trigger "g" (flipflop booleans)
[ arg (sumExterns + counter false + 25) ]
-- [ arg (counter false + 25 :: Stream Int32) ]
-- A trigger with a single argument (should never fire):
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)
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}
--------------------------------------------------------------------------------
Something went wrong with that request. Please try again.