Fix warnings in demo programs

copilot-verifier-demo/src/Demo2.hs

@@ -24,11 +24,15 @@ temp = extern "temperature"
 ctemp :: Stream Float
 ctemp = (unsafeCast temp * constant (150.0/255.0)) - constant 50.0
 
+-- width of the sliding window
+window :: Int
+window = 5
+
 -- Compute the sliding average of the last 5 temps
 -- (Here, 19.5 is the average of 18.0 and 21.0, the two temperature extremes
 -- that we check for in the spec.)
 avgTemp :: Stream Float
-avgTemp = (sum 5 (replicate 5 19.5 ++ ctemp)) / fromIntegral 5
+avgTemp = (sum 5 (replicate 5 19.5 ++ ctemp)) / fromIntegral window
 
 spec :: Spec
 spec = do

copilot-verifier-demo/src/Demo3.hs

@@ -12,8 +12,6 @@ import Language.Copilot
 import Copilot.Compile.C99
 import Copilot.Verifier
 
-import qualified Prelude as P
-import Data.Foldable (forM_)
 import qualified Control.Monad as Monad
 
 
@@ -36,44 +34,6 @@ tcoathr = extern "tcoathr" Nothing
 type Vect2 = (Stream Double, Stream Double)
 
 
---------------------------------
--- External streams for relative position and velocity.
---------------------------------
-
--- | The relative x velocity between ownship and the intruder.
-vx :: Stream Double
-vx = extern "relative_velocity_x" Nothing
-
--- | The relative y velocity between ownship and the intruder.
-vy :: Stream Double
-vy = extern "relative_velocity_y" Nothing
-
--- | The relative z velocity between ownship and the intruder.
-vz :: Stream Double
-vz = extern "relative_velocity_z" Nothing
-
--- | The relative velocity as a 2D vector.
-v :: (Stream Double, Stream Double)
-v = (vx, vy)
-
-
--- | The relative x position between ownship and the intruder.
-sx :: Stream Double
-sx = extern "relative_position_x" Nothing
-
--- | The relative y position between ownship and the intruder.
-sy :: Stream Double
-sy = extern "relative_position_y" Nothing
-
--- | The relative z position between ownship and the intruder.
-sz :: Stream Double
-sz = extern "relative_position_z" Nothing
-
--- | The relative position as a 2D vector.
-s :: (Stream Double, Stream Double)
-s = (sx, sy)
-
-
 ------------------
 -- The following section contains basic libraries for working with vectors.
 ------------------
@@ -167,11 +127,45 @@ horizontalWCV tvar s v =
   (norm s <= dthr) ||
   (((dcpa s v) <= dthr) && (0 <= (tvar s v)) && ((tvar s v) <= tthr))
 
+spec :: Spec
 spec = do
-  Monad.void $ prop "1a" (forall $ (tau s v) ~= (tau (neg s) (neg v)))
+  -- External streams for relative position and velocity.
+  let -- The relative x velocity between ownship and the intruder.
+      vx :: Stream Double
+      vx = extern "relative_velocity_x" Nothing
+
+      -- The relative y velocity between ownship and the intruder.
+      vy :: Stream Double
+      vy = extern "relative_velocity_y" Nothing
+
+      -- The relative z velocity between ownship and the intruder.
+      vz :: Stream Double
+      vz = extern "relative_velocity_z" Nothing
+
+      -- The relative velocity as a 2D vector.
+      v :: (Stream Double, Stream Double)
+      v = (vx, vy)
+
+
+      -- The relative x position between ownship and the intruder.
+      sx :: Stream Double
+      sx = extern "relative_position_x" Nothing
+
+      -- The relative y position between ownship and the intruder.
+      sy :: Stream Double
+      sy = extern "relative_position_y" Nothing
+
+      -- The relative z position between ownship and the intruder.
+      sz :: Stream Double
+      sz = extern "relative_position_z" Nothing
+
+      -- The relative position as a 2D vector.
+      s :: (Stream Double, Stream Double)
+      s = (sx, sy)
+  Monad.void $ prop "1a" (forAll $ (tau s v) ~= (tau (neg s) (neg v)))
   trigger "well_clear_violation" (wcv tep s sz v vz) []
 
 main :: IO ()
 main = do
   spec' <- reify spec
-  verify mkDefaultCSettings [] "demo3" spec'
+  verify mkDefaultCSettings [] "demo3" spec'