--------------------------------------------------------------------------------
-- Copyright 2019 National Institute of Aerospace / Galois, Inc.
--------------------------------------------------------------------------------

-- This is a simple example with basic usage. It implements a simple home
-- heating system: It heats when temp gets too low, and stops when it is high
-- enough. It read temperature as a byte (range -50C to 100C) and translates
-- this to Celcius.

module Copilot.Verifier.Examples.ShouldPass.Heater where

import Language.Copilot
import Copilot.Compile.C99
import Copilot.PrettyPrint as PP
--import Copilot.Language.Prelude

import Copilot.Verifier ( Verbosity(..), VerifierOptions(..)
                        , defaultVerifierOptions, verifyWithOptions )

import qualified Prelude as P
import Control.Monad (when)

-- External temperature as a byte, range of -50C to 100C
temp :: Stream Word8
temp :: Stream Word8
temp = String -> Maybe [Word8] -> Stream Word8
forall a. Typed a => String -> Maybe [a] -> Stream a
extern String
"temperature" Maybe [Word8]
forall a. Maybe a
Nothing

-- Calculate temperature in Celcius.
-- We need to cast the Word8 to a Float. Note that it is an unsafeCast, as there
-- is no direct relation between Word8 and Float.
ctemp :: Stream Float
ctemp :: Stream Float
ctemp = (Stream Word8 -> Stream Float
forall a b.
(UnsafeCast a b, Typed a, Typed b) =>
Stream a -> Stream b
unsafeCast Stream Word8
temp Stream Float -> Stream Float -> Stream Float
forall a. Num a => a -> a -> a
* Float -> Stream Float
forall a. Typed a => a -> Stream a
constant (Float
150.0Float -> Float -> Float
forall a. Fractional a => a -> a -> a
/Float
255.0)) Stream Float -> Stream Float -> Stream Float
forall a. Num a => a -> a -> a
- Float -> Stream Float
forall a. Typed a => a -> Stream a
constant Float
50.0

-- width of the sliding window
window :: Int
window :: Int
window = Int
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 :: Stream Float
avgTemp = (Int -> Stream Float -> Stream Float
forall a. (Typed a, Num a, Eq a) => Int -> Stream a -> Stream a
sum Int
window (Int -> Float -> [Float]
forall a. Int -> a -> [a]
replicate Int
window Float
19.5 [Float] -> Stream Float -> Stream Float
forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream Float
ctemp)) Stream Float -> Stream Float -> Stream Float
forall a. Fractional a => a -> a -> a
/ Int -> Stream Float
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
window

spec :: Spec
spec :: Spec
spec = do
  String -> Stream Bool -> [Arg] -> Spec
trigger String
"heaton"  (Stream Float
avgTemp Stream Float -> Stream Float -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
< Stream Float
18.0) [Stream Float -> Arg
forall a. Typed a => Stream a -> Arg
arg Stream Float
avgTemp]
  String -> Stream Bool -> [Arg] -> Spec
trigger String
"heatoff" (Stream Float
avgTemp Stream Float -> Stream Float -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
> Stream Float
21.0) [Stream Float -> Arg
forall a. Typed a => Stream a -> Arg
arg Stream Float
avgTemp]

-- Compile the spec
verifySpec :: Verbosity -> IO ()
verifySpec :: Verbosity -> IO ()
verifySpec Verbosity
verb =
  do Spec
rspec <- Spec -> IO Spec
forall a. Spec' a -> IO Spec
reify Spec
spec
     Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Verbosity
verb Verbosity -> Verbosity -> Bool
forall a. Ord a => a -> a -> Bool
P.>= Verbosity
Default) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (Spec -> String
PP.prettyPrint Spec
rspec)
     VerifierOptions -> CSettings -> [String] -> String -> Spec -> IO ()
verifyWithOptions VerifierOptions
defaultVerifierOptions{verbosity = verb}
                       CSettings
mkDefaultCSettings [] String
"heater"
                       Spec
rspec

{-
  do spec' <- reify spec
     putStrLn $ prettyPrintDot spec'
-}