{-# LANGUAGE NoImplicitPrelude #-}
module Copilot.Verifier.Examples.ShouldPass.IntOps where

import Copilot.Compile.C99 (mkDefaultCSettings)
import Copilot.Verifier ( Verbosity, VerifierOptions(..)
                        , defaultVerifierOptions, verifyWithOptions )
import Language.Copilot
import qualified Prelude as P

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

      shiftBy :: Stream Int16
      shiftBy :: Stream Int16
shiftBy = String -> Maybe [Int16] -> Stream Int16
forall a. Typed a => String -> Maybe [a] -> Stream a
extern String
"shiftBy" Maybe [Int16]
forall a. Maybe a
Nothing

  PropRef Universal
_ <- String -> Prop Universal -> Writer [SpecItem] (PropRef Universal)
forall a. String -> Prop a -> Writer [SpecItem] (PropRef a)
prop String
"nonzero" (Stream Bool -> Prop Universal
forAll (Stream Int16
stream Stream Int16 -> Stream Int16 -> Stream Bool
forall a. (Eq a, Typed a) => Stream a -> Stream a -> Stream Bool
/= Stream Int16
0))
  PropRef Universal
_ <- String -> Prop Universal -> Writer [SpecItem] (PropRef Universal)
forall a. String -> Prop a -> Writer [SpecItem] (PropRef a)
prop String
"shiftByBits" (Stream Bool -> Prop Universal
forAll (Stream Int16
0 Stream Int16 -> Stream Int16 -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
<= Stream Int16
shiftBy Stream Bool -> Stream Bool -> Stream Bool
&& Stream Int16
shiftBy Stream Int16 -> Stream Int16 -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
< Stream Int16
16))

  String -> (Stream Int16 -> Stream Int16) -> Stream Int16 -> Spec
triggerOp1 String
"abs" Stream Int16 -> Stream Int16
forall a. Num a => a -> a
abs Stream Int16
stream
  String -> (Stream Int16 -> Stream Int16) -> Stream Int16 -> Spec
triggerOp1 String
"signum" Stream Int16 -> Stream Int16
forall a. Num a => a -> a
signum Stream Int16
stream
  String -> (Stream Int16 -> Stream Int16) -> Stream Int16 -> Spec
triggerOp1 String
"bwNot" Stream Int16 -> Stream Int16
forall a. Bits a => a -> a
complement Stream Int16
stream

  String
-> (Stream Int16 -> Stream Int16 -> Stream Int16)
-> Stream Int16
-> Stream Int16
-> Spec
triggerOp2 String
"add" Stream Int16 -> Stream Int16 -> Stream Int16
forall a. Num a => a -> a -> a
(+) Stream Int16
stream Stream Int16
stream
  String
-> (Stream Int16 -> Stream Int16 -> Stream Int16)
-> Stream Int16
-> Stream Int16
-> Spec
triggerOp2 String
"sub" (-) Stream Int16
stream Stream Int16
stream
  String
-> (Stream Int16 -> Stream Int16 -> Stream Int16)
-> Stream Int16
-> Stream Int16
-> Spec
triggerOp2 String
"mul" Stream Int16 -> Stream Int16 -> Stream Int16
forall a. Num a => a -> a -> a
(*) Stream Int16
stream Stream Int16
stream
  String
-> (Stream Int16 -> Stream Int16 -> Stream Int16)
-> Stream Int16
-> Stream Int16
-> Spec
triggerOp2 String
"mod" Stream Int16 -> Stream Int16 -> Stream Int16
forall a. (Typed a, Integral a) => Stream a -> Stream a -> Stream a
mod Stream Int16
stream Stream Int16
stream
  String
-> (Stream Int16 -> Stream Int16 -> Stream Int16)
-> Stream Int16
-> Stream Int16
-> Spec
triggerOp2 String
"div" Stream Int16 -> Stream Int16 -> Stream Int16
forall a. (Typed a, Integral a) => Stream a -> Stream a -> Stream a
div Stream Int16
stream Stream Int16
stream
  String
-> (Stream Int16 -> Stream Int16 -> Stream Int16)
-> Stream Int16
-> Stream Int16
-> Spec
triggerOp2 String
"bwAnd" Stream Int16 -> Stream Int16 -> Stream Int16
forall a. Bits a => a -> a -> a
(.&.) Stream Int16
stream Stream Int16
stream
  String
-> (Stream Int16 -> Stream Int16 -> Stream Int16)
-> Stream Int16
-> Stream Int16
-> Spec
triggerOp2 String
"bwOr" Stream Int16 -> Stream Int16 -> Stream Int16
forall a. Bits a => a -> a -> a
(.|.) Stream Int16
stream Stream Int16
stream
  String
-> (Stream Int16 -> Stream Int16 -> Stream Int16)
-> Stream Int16
-> Stream Int16
-> Spec
triggerOp2 String
"bwXor" Stream Int16 -> Stream Int16 -> Stream Int16
forall a. Bits a => a -> a -> a
(.^.) Stream Int16
stream Stream Int16
stream
  String
-> (Stream Int16 -> Stream Int16 -> Stream Int16)
-> Stream Int16
-> Stream Int16
-> Spec
triggerOp2 String
"bwShiftL" Stream Int16 -> Stream Int16 -> Stream Int16
forall a b.
(Bits a, Typed a, Typed b, Integral b) =>
Stream a -> Stream b -> Stream a
(.<<.) Stream Int16
stream Stream Int16
shiftBy
  String
-> (Stream Int16 -> Stream Int16 -> Stream Int16)
-> Stream Int16
-> Stream Int16
-> Spec
triggerOp2 String
"bwShiftR" Stream Int16 -> Stream Int16 -> Stream Int16
forall a b.
(Bits a, Typed a, Typed b, Integral b) =>
Stream a -> Stream b -> Stream a
(.>>.) Stream Int16
stream Stream Int16
shiftBy

triggerOp1 :: String ->
              (Stream Int16 -> Stream Int16) ->
              Stream Int16 ->
              Spec
triggerOp1 :: String -> (Stream Int16 -> Stream Int16) -> Stream Int16 -> Spec
triggerOp1 String
name Stream Int16 -> Stream Int16
op Stream Int16
stream =
  String -> Stream Bool -> [Arg] -> Spec
trigger (String
name String -> String -> String
forall a. [a] -> [a] -> [a]
P.++ String
"Trigger") ((Stream Int16 -> Stream Int16) -> Stream Int16 -> Stream Bool
testOp1 Stream Int16 -> Stream Int16
op Stream Int16
stream) [Stream Int16 -> Arg
forall a. Typed a => Stream a -> Arg
arg Stream Int16
stream]

triggerOp2 :: String ->
              (Stream Int16 -> Stream Int16 -> Stream Int16) ->
              Stream Int16 -> Stream Int16 ->
              Spec
triggerOp2 :: String
-> (Stream Int16 -> Stream Int16 -> Stream Int16)
-> Stream Int16
-> Stream Int16
-> Spec
triggerOp2 String
name Stream Int16 -> Stream Int16 -> Stream Int16
op Stream Int16
stream1 Stream Int16
stream2 =
  String -> Stream Bool -> [Arg] -> Spec
trigger (String
name String -> String -> String
forall a. [a] -> [a] -> [a]
P.++ String
"Trigger") ((Stream Int16 -> Stream Int16 -> Stream Int16)
-> Stream Int16 -> Stream Int16 -> Stream Bool
testOp2 Stream Int16 -> Stream Int16 -> Stream Int16
op Stream Int16
stream1 Stream Int16
stream2) [Stream Int16 -> Arg
forall a. Typed a => Stream a -> Arg
arg Stream Int16
stream1, Stream Int16 -> Arg
forall a. Typed a => Stream a -> Arg
arg Stream Int16
stream2]

testOp1 :: (Stream Int16 -> Stream Int16) -> Stream Int16 -> Stream Bool
testOp1 :: (Stream Int16 -> Stream Int16) -> Stream Int16 -> Stream Bool
testOp1 Stream Int16 -> Stream Int16
op Stream Int16
stream =
  Stream Int16 -> Stream Int16
op Stream Int16
stream Stream Int16 -> Stream Int16 -> Stream Bool
forall a. (Eq a, Typed a) => Stream a -> Stream a -> Stream Bool
== Stream Int16 -> Stream Int16
op Stream Int16
stream

testOp2 :: (Stream Int16 -> Stream Int16 -> Stream Int16) ->
           Stream Int16 -> Stream Int16 ->
           Stream Bool
testOp2 :: (Stream Int16 -> Stream Int16 -> Stream Int16)
-> Stream Int16 -> Stream Int16 -> Stream Bool
testOp2 Stream Int16 -> Stream Int16 -> Stream Int16
op Stream Int16
stream1 Stream Int16
stream2 =
  Stream Int16 -> Stream Int16 -> Stream Int16
op Stream Int16
stream1 Stream Int16
stream2 Stream Int16 -> Stream Int16 -> Stream Bool
forall a. (Eq a, Typed a) => Stream a -> Stream a -> Stream Bool
== Stream Int16 -> Stream Int16 -> Stream Int16
op Stream Int16
stream1 Stream Int16
stream2

verifySpec :: Verbosity -> IO ()
verifySpec :: Verbosity -> IO ()
verifySpec Verbosity
verb = do
  Spec
spec' <- Spec -> IO Spec
forall a. Spec' a -> IO Spec
reify Spec
spec
  VerifierOptions -> CSettings -> [String] -> String -> Spec -> IO ()
verifyWithOptions VerifierOptions
defaultVerifierOptions{verbosity = verb}
                    CSettings
mkDefaultCSettings [String
"nonzero", String
"shiftByBits"] String
"intOps" Spec
spec'