--------------------------------------------------------------------------------
-- 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 


--------------------------------------------------------------------------------