Skip to content
Fetching contributors…
Cannot retrieve contributors at this time
61 lines (42 sloc) 1.94 KB
--------------------------------------------------------------------------------
-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
--------------------------------------------------------------------------------
-- | Example in sampling external functions.
{-# LANGUAGE RebindableSyntax #-}
module ExtFuns ( extFuns ) where
import Language.Copilot
import qualified Copilot.Compile.C99 as C
import qualified Copilot.Compile.SBV as S
--import qualified Copilot.Tools.CBMC as B
--------------------------------------------------------------------------------
doubles :: Stream Word16
doubles = [0,1] ++ doubles + 1
---------------------------------------------------------------------------------
-- Function func0 and it's environment for interpreting
func0 :: Stream Word16
func0 = externFun "func0" [ arg x, arg doubles ]
(Just $ cast x + doubles)
where x = externW8 "x" (Just [0..])
---------------------------------------------------------------------------------
-- Function func1 and it's environment for interpreting
func1 :: Stream Bool
func1 = externFun "func1" [] (Just $ [False] ++ not func1)
---------------------------------------------------------------------------------
-- Function func0 with another set of args and it's environment for interpreting
func2 :: Stream Word16
func2 = externFun "func0" [ arg $ constW8 3, arg $ constW16 4 ]
(Just $ cast (constW8 3) + constW16 4)
---------------------------------------------------------------------------------
a :: Stream Word16
a = func0 + func0
spec :: Spec
spec = trigger "trigger" true [ arg func0
, arg func1
, arg func2
, arg a ]
extFuns :: IO ()
extFuns = do
interpret 10 spec
reify spec >>= C.compile C.defaultParams
reify spec >>= S.compile S.defaultParams
--------------------------------------------------------------------------------
Jump to Line
Something went wrong with that request. Please try again.