Tweaks to examples.

leepike · Nov 10, 2011 · bdb29ac · bdb29ac
1 parent 5783358
commit bdb29ac
Show file tree

Hide file tree

Showing 3 changed files with 17 additions and 15 deletions.
diff --git a/Examples/EngineExample.hs b/Examples/EngineExample.hs
@@ -30,8 +30,8 @@ main :: IO ()
 main = 
   interpret 
     10
-    [ input "cooler" cooler, input "tmp_probe_0" two51
-    , input "tmp_probe_1" two51, input "tmp_probe_2" zero]
+    [ var "cooler" cooler, var "tmp_probe_0" two51
+    , var "tmp_probe_1" two51, var "tmp_probe_2" zero]
     engineMonitor
   where
   two51 = [251, 251] P.++ repeat (250 :: Word8)

diff --git a/Examples/Examples.hs b/Examples/Examples.hs
@@ -18,6 +18,7 @@ import qualified Copilot.Tools.CBMC as C
 -- Some utility functions:
 --
 
+
 implyStream :: Stream Bool -> Stream Bool -> Stream Bool
 implyStream p q = not p || q
 
@@ -35,6 +36,9 @@ even x = x `mod` 2 == 0
 odd :: (P.Integral a, Typed a) => Stream a -> Stream Bool
 odd = not . even
 
+extEven :: Stream Bool
+extEven = externI64 "x" `mod` 2 == 0
+
 counter :: (Num a, Typed a) => Stream Bool -> Stream a
 counter reset = y
   where
@@ -67,6 +71,11 @@ prop = (x - x') <= 5 && (x - x') <= (-5)
   x  = [0] ++ externI32 "x"
   x' = drop 1 x
 
+foo = do
+  let x = externW8 "x"
+  trigger "trigger" true [arg $ x < 3]
+  observer "debug_x" x
+
 --------------------------------------------------------------------------------
 
 --
@@ -114,7 +123,7 @@ main =
     putStrLn ""
     putStrLn "Interpreter:"
     putStrLn ""
-    interpret 10 [input "e1" e1, input "e2" e2, input "e3" e3] spec
+    interpret 10 [var "e1" e1, var "e2" e2, var "e3" e3] spec
     putStrLn ""
     putStrLn ""
     putStrLn "Atom:"

diff --git a/Examples/ExtFuns.hs b/Examples/ExtFuns.hs
@@ -18,26 +18,19 @@ nats = [0] ++ nats + 1
 func0 :: Stream Word16
 func0 = externFun "func0" [funArg $ externW8 "x", funArg nats]
 
--- A reference implementation of "func0" for simulation.
-func0Spec :: Stream Word16
-func0Spec = cast (externW8 "x") + nats
-
 func1 :: Stream Bool
 func1 = externFun "func1" []
 
--- A reference implementation of "func0" for simulation.
-func1Spec :: Stream Bool
-func1Spec = [False] ++ not func1
-
 spec :: Spec
 spec = trigger "trigger" true [ arg func0, arg func1 ]
 
 main :: IO ()
-main = 
---  reify spec >>= C.compile C.defaultParams 
-    interpret 10 [ func "func0" func0Spec
+main = do
+    reify spec >>= C.compile C.defaultParams 
+    -- Reference implementations of our functions
+    interpret 10 [ func "func0" (cast (externW8 "x") + nats)
                  , var "x" ([0..] :: [Word8]) 
-                 , func "func1" func1Spec
+                 , func "func1" ([False] ++ not func1)
                  ] 
               spec