copilot-2.0.5: Examples/Examples2.hs

--------------------------------------------------------------------------------
-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
--------------------------------------------------------------------------------

-- | Some more Copilot examples.

{-# LANGUAGE RebindableSyntax #-}

module Examples2 ( examples2 ) where

import Prelude ()
import Language.Copilot

import qualified Copilot.Compile.SBV as S

import qualified Data.List as L

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

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

fibSpec :: Spec
fibSpec = do
  trigger "fib_out" true [arg fib]

counter :: Stream Bool -> Stream Bool 
        -> Stream Int32
counter inc reset = cnt
  where 
  cnt = if reset then 0
          else if inc then z + 1
                 else z
  z = [0] ++ cnt
-}

nats :: Stream Word64
nats = [0] ++ nats + 1

alt :: Stream Bool
alt = [True] ++ not alt

logic :: Stream Bool
logic = [True, False] ++ logic || drop 1 logic

sumExterns :: Stream Word64
sumExterns =
  let
    e1 = extern "e1" (Just [0..])
    e2 = extern "e2" (Just $ L.cycle [2,3,4])
  in
    e1 + e2 + e1

spec :: Spec
spec = do
  trigger "trig1" alt [ arg $ nats < 3
                      , arg sumExterns 
                      , arg logic
                      ]

examples2 :: IO ()
examples2 = do
--  reify fibSpec >>= S.compile S.defaultParams
  reify spec >>= S.compile S.defaultParams