copilot 2.0.5 → 2.0.6
raw patch · 3 files changed
+91/−18 lines, 3 filesdep ~copilot-language
Dependency ranges changed: copilot-language
Files
- Examples/ExtFuns.hs +20/−16
- Examples/Sat.hs +67/−0
- copilot.cabal +4/−2
Examples/ExtFuns.hs view
@@ -9,35 +9,36 @@ module ExtFuns ( extFuns ) where import Language.Copilot ---import qualified Copilot.Compile.C99 as C+import qualified Copilot.Compile.C99 as C+import qualified Copilot.Compile.SBV as S+--import qualified Copilot.Tools.CBMC as B -------------------------------------------------------------------------------- -nats :: Stream Word16-nats = [0] ++ nats + 1+doubles :: Stream Word16+doubles = [0,1] ++ doubles + 1 ------------------------------------------------------------------------------------ Function func0 and it's environment for interpreting +-- Function func0 and it's environment for interpreting func0 :: Stream Word16-func0 = externFun "func0" [ funArg x, funArg nats ]- (Just $ cast x + nats)+func0 = externFun "func0" [ arg x, arg doubles ]+ (Just $ cast x + doubles) where x = externW8 "x" (Just [0..])- ------------------------------------------------------------------------------------- Function func0 with another set of args and it's environment for interpreting --- func2 :: Stream Word16--- func2 = externFun "func0" [ funArg $ constW8 3, funArg $ constW16 4 ]--- (Just $ constW16 4 + 1)- --------------------------------------------------------------------------------- ---------------------------------------------------------------------------------- -- 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@@ -46,11 +47,14 @@ spec :: Spec spec = trigger "trigger" true [ arg func0 , arg func1+ , arg func2 , arg a ] extFuns :: IO () extFuns = do--- reify spec >>= C.compile C.defaultParams - interpret 10 spec+ interpret 10 spec+ reify spec >>= C.compile C.defaultParams + reify spec >>= S.compile S.defaultParams + --------------------------------------------------------------------------------
+ Examples/Sat.hs view
@@ -0,0 +1,67 @@+-- | Example of a simple SAT solver (simply constructs the truth table) in+-- Copilot.++-- {-# LANGUAGE RebindableSyntax #-}++module Sat where++import Language.Copilot+import qualified Prelude as P+import Control.Monad (foldM_)++---------------------------------------------------------------------------------++-- | Number of sat variables and a Boolean function over those variables.+type SatFunc = (Int, [Stream Bool] -> Stream Bool)++-- Takes a Sat function and returns the stream of variables and a SAT function.+sat :: SatFunc -> ([Stream Bool], Stream Bool)+sat (i,f) = (xs, res)+ where+ -- If it becomes true, it stays true.+ res = [False] ++ (f xs || res)++ xs = xs' i++ xs' 0 = []+ xs' n = clk (period $ 2 P.^ n) (phase (0 :: Int)) : xs' (n P.- 1)++satSpec :: SatFunc -> Spec+satSpec f = do+ observer "sat" (snd $ sat f)+ observer "done" done+ foldM_ mkObs (0 :: Int) xs++ where+ xs = fst $ sat f+ cnt :: Stream Word64 -- Would need to be extended depending on number of+ -- variables.+ cnt = [1] ++ cnt + 1+ done = cnt == (2 P.^ length xs)+ mkObs idx strm = do observer ("obs" P.++ show idx) strm+ return (idx P.+ 1)+++f0 :: SatFunc+--f0 = (3, \[a,b,c] -> a && (b || (not c)))+f0 = (3, f) + where + f [a,b,c] = a && (b || (not c))+ f _ = error "Bad SAT function."++f1 :: SatFunc+f1 = (9, f')+ where+ f' [a,b,c,d,e,f,g,h,i] = + a && b && c && d && e && + f && g && h && i && i && not i+ f' _ = error "Bad SAT function."++-- | Run the interpreter long enough to get an answer.+runFunc :: SatFunc -> IO ()+runFunc f = interpret (2 P.^ fst f) (satSpec f)++satExamples :: IO ()+satExamples = runFunc f0 >> runFunc f1++---------------------------------------------------------------------------------
copilot.cabal view
@@ -1,5 +1,5 @@ name: copilot-version: 2.0.5+version: 2.0.6 cabal-version: >= 1.10 license: BSD3 license-file: LICENSE@@ -30,7 +30,7 @@ build-depends: base >= 4.0 && <5 , copilot-core >= 0.2.3- , copilot-language >= 0.3+ , copilot-language >= 0.4 , copilot-libraries , copilot-cbmc exposed-modules: Language.Copilot@@ -63,6 +63,8 @@ , PTLTLExamples , Random , RegExpExamples+ , Sat , StackExamples , StatExamples , VotingExamples+