Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

More examples.

  • Loading branch information...
commit f9f8a28ad329bf39fe5011256b37be0ded6c182d 1 parent e308694
@leepike authored
Showing with 66 additions and 1 deletion.
  1. +17 −0 Examples/Examples2.hs
  2. +1 −1  Examples/Languages.hs
  3. +48 −0 Examples/Sat.hs
View
17 Examples/Examples2.hs
@@ -1,3 +1,11 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+-- | Some more Copilot examples.
+
+{-# LANGUAGE RebindableSyntax #-}
+
module Examples2 ( examples2 ) where
import Prelude ()
@@ -27,6 +35,15 @@ 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
View
2  Examples/Languages.hs
@@ -2,7 +2,7 @@
-- an external variable. Assume the input doesn't given tokens outside the
-- alphabet, and the result is always delayed by one w.r.t. the input stream.
--- I think Copilot can recognize context-sensitive grammars.
+-- Copilot can compute at least NP-Complete problems.
{-# LANGUAGE RebindableSyntax #-}
View
48 Examples/Sat.hs
@@ -0,0 +1,48 @@
+-- | Example of a simple SAT solver (simply constructs the truth table) in
+-- Copilot.
+
+module Languages 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)
+
+
+-- Example SAT function.
+f0 :: SatFunc
+f0 = (3, \[a,b,c] -> a && (b || (not c)))
+
+---------------------------------------------------------------------------------
Please sign in to comment.
Something went wrong with that request. Please try again.