{-# 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 :: Spec
spec = do
  let pair :: Stream (Array 2 Word32)
      pair :: Stream (Array 2 Word32)
pair = String -> Maybe [Array 2 Word32] -> Stream (Array 2 Word32)
forall a. Typed a => String -> Maybe [a] -> Stream a
extern String
"pair" Maybe [Array 2 Word32]
forall a. Maybe a
Nothing

  -- Check equality, indexing into array and modifying the value. Note that
  -- this is trivial by equality.
  String -> Stream Bool -> [Arg] -> Spec
trigger String
"trig_1"
    (((Stream (Array 2 Word32)
pair Stream (Array 2 Word32)
-> Stream Word32
-> Projection (Array 2 Word32) (Stream Word32) Word32
forall (n :: Nat) t.
Stream (Array n t)
-> Stream Word32 -> Projection (Array n t) (Stream Word32) t
!! Stream Word32
0 Projection (Array 2 Word32) (Stream Word32) Word32
-> (Stream Word32 -> Stream Word32) -> Stream (Array 2 Word32)
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 (Array 2 Word32) -> Stream Word32 -> Stream Word32
forall (n :: Nat) t.
(KnownNat n, Typed t) =>
Stream (Array n t) -> Stream Word32 -> Stream t
! Stream Word32
0) Stream Word32 -> Stream Word32 -> Stream Bool
forall a. (Eq a, Typed a) => Stream a -> Stream a -> Stream Bool
== ((Stream (Array 2 Word32)
pair Stream (Array 2 Word32) -> Stream Word32 -> Stream Word32
forall (n :: Nat) t.
(KnownNat n, Typed t) =>
Stream (Array n t) -> Stream Word32 -> Stream t
! Stream Word32
0) Stream Word32 -> Stream Word32 -> Stream Word32
forall a. Num a => a -> a -> a
+ Stream Word32
1))
    [Stream (Array 2 Word32) -> Arg
forall a. Typed a => Stream a -> Arg
arg Stream (Array 2 Word32)
pair]

  -- Same as previous example, but get a different array index (so should be
  -- false).
  String -> Stream Bool -> [Arg] -> Spec
trigger String
"trig_2"
    (((Stream (Array 2 Word32)
pair Stream (Array 2 Word32)
-> Stream Word32
-> Projection (Array 2 Word32) (Stream Word32) Word32
forall (n :: Nat) t.
Stream (Array n t)
-> Stream Word32 -> Projection (Array n t) (Stream Word32) t
!! Stream Word32
0 Projection (Array 2 Word32) (Stream Word32) Word32
-> (Stream Word32 -> Stream Word32) -> Stream (Array 2 Word32)
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 (Array 2 Word32) -> Stream Word32 -> Stream Word32
forall (n :: Nat) t.
(KnownNat n, Typed t) =>
Stream (Array n t) -> Stream Word32 -> Stream t
! Stream Word32
1) Stream Word32 -> Stream Word32 -> Stream Bool
forall a. (Eq a, Typed a) => Stream a -> Stream a -> Stream Bool
== ((Stream (Array 2 Word32)
pair Stream (Array 2 Word32) -> Stream Word32 -> Stream Word32
forall (n :: Nat) t.
(KnownNat n, Typed t) =>
Stream (Array n t) -> Stream Word32 -> Stream t
! Stream Word32
0) Stream Word32 -> Stream Word32 -> Stream Word32
forall a. Num a => a -> a -> a
+ Stream Word32
1))
    [Stream (Array 2 Word32) -> Arg
forall a. Typed a => Stream a -> Arg
arg Stream (Array 2 Word32)
pair]

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
"updateArray"