{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE DataKinds        #-}

-- | An example showing of using @copilot-verifier@ to verify a specification
-- involving structs where individual fields are updated.
module Copilot.Verifier.Examples.ShouldPass.UpdateStruct where

import Language.Copilot
import Copilot.Compile.C99
import Copilot.Verifier ( Verbosity, VerifierOptions(..)
                        , defaultVerifierOptions, verifyWithOptions )

-- | Definition for `Volts`.
data Volts = Volts
  { Volts -> Field "numVolts" Word32
numVolts :: Field "numVolts" Word32
  , Volts -> Field "flag" Bool
flag     :: Field "flag"     Bool
  }

-- | `Struct` instance for `Volts`.
instance Struct Volts where
  typeName :: Volts -> String
typeName Volts
_ = String
"volts"
  toValues :: Volts -> [Value Volts]
toValues Volts
vlts = [ Type Word32 -> Field "numVolts" Word32 -> Value Volts
forall a (s :: Symbol) t.
(Typeable t, KnownSymbol s, Show t) =>
Type t -> Field s t -> Value a
Value Type Word32
Word32 (Volts -> Field "numVolts" Word32
numVolts Volts
vlts)
                  , Type Bool -> Field "flag" Bool -> Value Volts
forall a (s :: Symbol) t.
(Typeable t, KnownSymbol s, Show t) =>
Type t -> Field s t -> Value a
Value Type Bool
Bool   (Volts -> Field "flag" Bool
flag Volts
vlts)
                  ]

-- | `Volts` instance for `Typed`.
instance Typed Volts where
  typeOf :: Type Volts
typeOf = Volts -> Type Volts
forall a. (Typed a, Struct a) => a -> Type a
Struct (Field "numVolts" Word32 -> Field "flag" Bool -> Volts
Volts (Word32 -> Field "numVolts" Word32
forall (s :: Symbol) t. t -> Field s t
Field Word32
0) (Bool -> Field "flag" Bool
forall (s :: Symbol) t. t -> Field s t
Field Bool
False))

data Battery = Battery
  { Battery -> Field "temp" Word32
temp  :: Field "temp"  Word32
  , Battery -> Field "volts" (Array 10 Volts)
volts :: Field "volts" (Array 10 Volts)
  , Battery -> Field "other" (Array 10 (Array 5 Word32))
other :: Field "other" (Array 10 (Array 5 Word32))
  }

-- | `Battery` instance for `Struct`.
instance Struct Battery where
  typeName :: Battery -> String
typeName Battery
_ = String
"battery"
  toValues :: Battery -> [Value Battery]
toValues Battery
battery = [ Type Word32 -> Field "temp" Word32 -> Value Battery
forall a (s :: Symbol) t.
(Typeable t, KnownSymbol s, Show t) =>
Type t -> Field s t -> Value a
Value Type Word32
forall a. Typed a => Type a
typeOf (Battery -> Field "temp" Word32
temp Battery
battery)
                     , Type (Array 10 Volts)
-> Field "volts" (Array 10 Volts) -> Value Battery
forall a (s :: Symbol) t.
(Typeable t, KnownSymbol s, Show t) =>
Type t -> Field s t -> Value a
Value Type (Array 10 Volts)
forall a. Typed a => Type a
typeOf (Battery -> Field "volts" (Array 10 Volts)
volts Battery
battery)
                     , Type (Array 10 (Array 5 Word32))
-> Field "other" (Array 10 (Array 5 Word32)) -> Value Battery
forall a (s :: Symbol) t.
(Typeable t, KnownSymbol s, Show t) =>
Type t -> Field s t -> Value a
Value Type (Array 10 (Array 5 Word32))
forall a. Typed a => Type a
typeOf (Battery -> Field "other" (Array 10 (Array 5 Word32))
other Battery
battery)
                     ]

-- | `Battery` instance for `Typed`. Note that `undefined` is used as an
-- argument to `Field`. This argument is never used, so `undefined` will never
-- throw an error.
instance Typed Battery where
  typeOf :: Type Battery
typeOf = Battery -> Type Battery
forall a. (Typed a, Struct a) => a -> Type a
Struct (Field "temp" Word32
-> Field "volts" (Array 10 Volts)
-> Field "other" (Array 10 (Array 5 Word32))
-> Battery
Battery (Word32 -> Field "temp" Word32
forall (s :: Symbol) t. t -> Field s t
Field Word32
0) (Array 10 Volts -> Field "volts" (Array 10 Volts)
forall (s :: Symbol) t. t -> Field s t
Field Array 10 Volts
forall a. HasCallStack => a
undefined) (Array 10 (Array 5 Word32)
-> Field "other" (Array 10 (Array 5 Word32))
forall (s :: Symbol) t. t -> Field s t
Field Array 10 (Array 5 Word32)
forall a. HasCallStack => a
undefined))

spec :: Spec
spec :: Spec
spec = do
  let battery :: Stream Battery
      battery :: Stream Battery
battery = String -> Maybe [Battery] -> Stream Battery
forall a. Typed a => String -> Maybe [a] -> Stream a
extern String
"battery" Maybe [Battery]
forall a. Maybe a
Nothing

  -- Update a struct field, then check it for equality.
  String -> Stream Bool -> [Arg] -> Spec
trigger String
"updateTrig"
    ((Stream Battery
battery Stream Battery
-> (Battery -> Field "temp" Word32)
-> Projection Battery (Battery -> Field "temp" Word32) Word32
forall (f :: Symbol) t s.
(KnownSymbol f, Typed t, Typed s, Struct s) =>
Stream s -> (s -> Field f t) -> Projection s (s -> Field f t) t
## Battery -> Field "temp" Word32
temp Projection Battery (Battery -> Field "temp" Word32) Word32
-> (Stream Word32 -> Stream Word32) -> Stream Battery
forall d s t.
Projectable d s t =>
Projection d s t -> (Stream t -> Stream t) -> Stream d
=$ (Stream Word32 -> Stream Word32 -> Stream Word32
forall a. Num a => a -> a -> a
+Stream Word32
1))Stream Battery -> (Battery -> Field "temp" Word32) -> Stream Word32
forall (f :: Symbol) t s.
(KnownSymbol f, Typed t, Typed s, Struct s) =>
Stream s -> (s -> Field f t) -> Stream t
#Battery -> Field "temp" Word32
temp Stream Word32 -> Stream Word32 -> Stream Bool
forall a. (Eq a, Typed a) => Stream a -> Stream a -> Stream Bool
== (Stream Battery
batteryStream Battery -> (Battery -> Field "temp" Word32) -> Stream Word32
forall (f :: Symbol) t s.
(KnownSymbol f, Typed t, Typed s, Struct s) =>
Stream s -> (s -> Field f t) -> Stream t
#Battery -> Field "temp" Word32
temp Stream Word32 -> Stream Word32 -> Stream Word32
forall a. Num a => a -> a -> a
+ Stream Word32
1))
    [Stream Battery -> Arg
forall a. Typed a => Stream a -> Arg
arg Stream Battery
battery]

verifySpec :: Verbosity -> IO ()
verifySpec :: Verbosity -> IO ()
verifySpec Verbosity
verb = Spec -> IO Spec
forall a. Spec' a -> IO Spec
reify Spec
spec IO Spec -> (Spec -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= VerifierOptions -> CSettings -> [String] -> String -> Spec -> IO ()
verifyWithOptions VerifierOptions
defaultVerifierOptions{verbosity = verb}
                                                   CSettings
mkDefaultCSettings [] String
"updateStruct"