content: {-# LANGUAGE RebindableSyntax #-}
  {-# LANGUAGE DataKinds        #-}
  
  -- | An example showing of using @copilot-verifier@ to verify a specification
  -- involving arrays where individual elements are updated.
  module Copilot.Verifier.Examples.ShouldPass.UpdateArray where
  
  import Language.Copilot
  import Copilot.Compile.C99
  import Copilot.Verifier ( Verbosity, VerifierOptions(..)
                          , defaultVerifierOptions, verifyWithOptions )
  
  spec :: Spec
  spec = do
    let pair :: Stream (Array 2 Word32)
        pair = extern "pair" Nothing
  
    -- Check equality, indexing into array and modifying the value. Note that
    -- this is trivial by equality.
    trigger "trig_1"
      (((pair !! 0 =$ (+1)) ! 0) == ((pair ! 0) + 1))
      [arg pair]
  
    -- Same as previous example, but get a different array index (so should be
    -- false).
    trigger "trig_2"
      (((pair !! 0 =$ (+1)) ! 1) == ((pair ! 0) + 1))
      [arg pair]
  
  verifySpec :: Verbosity -> IO ()
  verifySpec verb = reify spec >>= verifyWithOptions defaultVerifierOptions{verbosity = verb}
                                                     mkDefaultCSettings [] "updateArray"
  