--------------------------------------------------------------------------------
-- 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 = extern "temperature" 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 = (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 window (replicate window 19.5 ++ ctemp)) / fromIntegral window

spec :: Spec
spec = do
  trigger "heaton"  (avgTemp < 18.0) [arg avgTemp]
  trigger "heatoff" (avgTemp > 21.0) [arg avgTemp]

-- Compile the spec
verifySpec :: Verbosity -> IO ()
verifySpec verb =
  do rspec <- reify spec
     when (verb P.>= Default) $ putStrLn (PP.prettyPrint rspec)
     verifyWithOptions defaultVerifierOptions{verbosity = verb}
                       mkDefaultCSettings [] "heater"
                       rspec

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