content: {-# 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
    { numVolts :: Field "numVolts" Word32
    , flag     :: Field "flag"     Bool
    }
  
  -- | `Struct` instance for `Volts`.
  instance Struct Volts where
    typeName _ = "volts"
    toValues vlts = [ Value Word32 (numVolts vlts)
                    , Value Bool   (flag vlts)
                    ]
  
  -- | `Volts` instance for `Typed`.
  instance Typed Volts where
    typeOf = Struct (Volts (Field 0) (Field False))
  
  data Battery = Battery
    { temp  :: Field "temp"  Word32
    , volts :: Field "volts" (Array 10 Volts)
    , other :: Field "other" (Array 10 (Array 5 Word32))
    }
  
  -- | `Battery` instance for `Struct`.
  instance Struct Battery where
    typeName _ = "battery"
    toValues battery = [ Value typeOf (temp battery)
                       , Value typeOf (volts battery)
                       , Value typeOf (other 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 = Struct (Battery (Field 0) (Field undefined) (Field undefined))
  
  spec :: Spec
  spec = do
    let battery :: Stream Battery
        battery = extern "battery" Nothing
  
    -- Update a struct field, then check it for equality.
    trigger "updateTrig"
      ((battery ## temp =$ (+1))#temp == (battery#temp + 1))
      [arg battery]
  
  verifySpec :: Verbosity -> IO ()
  verifySpec verb = reify spec >>= verifyWithOptions defaultVerifierOptions{verbosity = verb}
                                                     mkDefaultCSettings [] "updateStruct"
  