{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Copilot.Verifier.Examples.ShouldPass.FPOps where

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

mkSpecFor :: forall a proxy. (RealFloat a, Typed a) => proxy a -> String -> Spec
mkSpecFor :: forall a (proxy :: * -> *).
(RealFloat a, Typed a) =>
proxy a -> String -> Spec
mkSpecFor proxy a
_ String
nameSuffix = do
  let mkName :: String -> String
      mkName :: String -> String
mkName String
namePrefix = String
namePrefix String -> String -> String
forall a. [a] -> [a] -> [a]
P.++ String
nameSuffix

      stream :: Stream a
      stream :: Stream a
stream = String -> Maybe [a] -> Stream a
forall a. Typed a => String -> Maybe [a] -> Stream a
extern (String -> String
mkName String
"stream") Maybe [a]
forall a. Maybe a
Nothing

  String -> (Stream a -> Stream a) -> Stream a -> Spec
forall a.
(RealFloat a, Typed a) =>
String -> (Stream a -> Stream a) -> Stream a -> Spec
triggerOp1 (String -> String
mkName String
"abs") Stream a -> Stream a
forall a. Num a => a -> a
abs Stream a
stream
  String -> (Stream a -> Stream a) -> Stream a -> Spec
forall a.
(RealFloat a, Typed a) =>
String -> (Stream a -> Stream a) -> Stream a -> Spec
triggerOp1 (String -> String
mkName String
"signum") Stream a -> Stream a
forall a. Num a => a -> a
signum Stream a
stream
  String -> (Stream a -> Stream a) -> Stream a -> Spec
forall a.
(RealFloat a, Typed a) =>
String -> (Stream a -> Stream a) -> Stream a -> Spec
triggerOp1 (String -> String
mkName String
"recip") Stream a -> Stream a
forall a. Fractional a => a -> a
recip Stream a
stream
  String -> (Stream a -> Stream a) -> Stream a -> Spec
forall a.
(RealFloat a, Typed a) =>
String -> (Stream a -> Stream a) -> Stream a -> Spec
triggerOp1 (String -> String
mkName String
"exp") Stream a -> Stream a
forall a. Floating a => a -> a
exp Stream a
stream
  String -> (Stream a -> Stream a) -> Stream a -> Spec
forall a.
(RealFloat a, Typed a) =>
String -> (Stream a -> Stream a) -> Stream a -> Spec
triggerOp1 (String -> String
mkName String
"sqrt") Stream a -> Stream a
forall a. Floating a => a -> a
sqrt Stream a
stream
  String -> (Stream a -> Stream a) -> Stream a -> Spec
forall a.
(RealFloat a, Typed a) =>
String -> (Stream a -> Stream a) -> Stream a -> Spec
triggerOp1 (String -> String
mkName String
"log") Stream a -> Stream a
forall a. Floating a => a -> a
log Stream a
stream
  String -> (Stream a -> Stream a) -> Stream a -> Spec
forall a.
(RealFloat a, Typed a) =>
String -> (Stream a -> Stream a) -> Stream a -> Spec
triggerOp1 (String -> String
mkName String
"sin") Stream a -> Stream a
forall a. Floating a => a -> a
sin Stream a
stream
  String -> (Stream a -> Stream a) -> Stream a -> Spec
forall a.
(RealFloat a, Typed a) =>
String -> (Stream a -> Stream a) -> Stream a -> Spec
triggerOp1 (String -> String
mkName String
"tan") Stream a -> Stream a
forall a. Floating a => a -> a
tan Stream a
stream
  String -> (Stream a -> Stream a) -> Stream a -> Spec
forall a.
(RealFloat a, Typed a) =>
String -> (Stream a -> Stream a) -> Stream a -> Spec
triggerOp1 (String -> String
mkName String
"cos") Stream a -> Stream a
forall a. Floating a => a -> a
cos Stream a
stream
  String -> (Stream a -> Stream a) -> Stream a -> Spec
forall a.
(RealFloat a, Typed a) =>
String -> (Stream a -> Stream a) -> Stream a -> Spec
triggerOp1 (String -> String
mkName String
"asin") Stream a -> Stream a
forall a. Floating a => a -> a
asin Stream a
stream
  String -> (Stream a -> Stream a) -> Stream a -> Spec
forall a.
(RealFloat a, Typed a) =>
String -> (Stream a -> Stream a) -> Stream a -> Spec
triggerOp1 (String -> String
mkName String
"atan") Stream a -> Stream a
forall a. Floating a => a -> a
atan Stream a
stream
  String -> (Stream a -> Stream a) -> Stream a -> Spec
forall a.
(RealFloat a, Typed a) =>
String -> (Stream a -> Stream a) -> Stream a -> Spec
triggerOp1 (String -> String
mkName String
"acos") Stream a -> Stream a
forall a. Floating a => a -> a
acos Stream a
stream
  String -> (Stream a -> Stream a) -> Stream a -> Spec
forall a.
(RealFloat a, Typed a) =>
String -> (Stream a -> Stream a) -> Stream a -> Spec
triggerOp1 (String -> String
mkName String
"sinh") Stream a -> Stream a
forall a. Floating a => a -> a
sinh Stream a
stream
  String -> (Stream a -> Stream a) -> Stream a -> Spec
forall a.
(RealFloat a, Typed a) =>
String -> (Stream a -> Stream a) -> Stream a -> Spec
triggerOp1 (String -> String
mkName String
"tanh") Stream a -> Stream a
forall a. Floating a => a -> a
tanh Stream a
stream
  String -> (Stream a -> Stream a) -> Stream a -> Spec
forall a.
(RealFloat a, Typed a) =>
String -> (Stream a -> Stream a) -> Stream a -> Spec
triggerOp1 (String -> String
mkName String
"cosh") Stream a -> Stream a
forall a. Floating a => a -> a
cosh Stream a
stream
  String -> (Stream a -> Stream a) -> Stream a -> Spec
forall a.
(RealFloat a, Typed a) =>
String -> (Stream a -> Stream a) -> Stream a -> Spec
triggerOp1 (String -> String
mkName String
"asinh") Stream a -> Stream a
forall a. Floating a => a -> a
asinh Stream a
stream
  String -> (Stream a -> Stream a) -> Stream a -> Spec
forall a.
(RealFloat a, Typed a) =>
String -> (Stream a -> Stream a) -> Stream a -> Spec
triggerOp1 (String -> String
mkName String
"atanh") Stream a -> Stream a
forall a. Floating a => a -> a
atanh Stream a
stream
  String -> (Stream a -> Stream a) -> Stream a -> Spec
forall a.
(RealFloat a, Typed a) =>
String -> (Stream a -> Stream a) -> Stream a -> Spec
triggerOp1 (String -> String
mkName String
"acosh") Stream a -> Stream a
forall a. Floating a => a -> a
acosh Stream a
stream
  String -> (Stream a -> Stream a) -> Stream a -> Spec
forall a.
(RealFloat a, Typed a) =>
String -> (Stream a -> Stream a) -> Stream a -> Spec
triggerOp1 (String -> String
mkName String
"ceiling") Stream a -> Stream a
forall a. (Typed a, RealFrac a) => Stream a -> Stream a
Copilot.ceiling Stream a
stream
  String -> (Stream a -> Stream a) -> Stream a -> Spec
forall a.
(RealFloat a, Typed a) =>
String -> (Stream a -> Stream a) -> Stream a -> Spec
triggerOp1 (String -> String
mkName String
"floor") Stream a -> Stream a
forall a. (Typed a, RealFrac a) => Stream a -> Stream a
Copilot.floor Stream a
stream

  String -> (Stream a -> Stream a -> Stream a) -> Stream a -> Spec
forall a.
(RealFloat a, Typed a) =>
String -> (Stream a -> Stream a -> Stream a) -> Stream a -> Spec
triggerOp2 (String -> String
mkName String
"add") Stream a -> Stream a -> Stream a
forall a. Num a => a -> a -> a
(+) Stream a
stream
  String -> (Stream a -> Stream a -> Stream a) -> Stream a -> Spec
forall a.
(RealFloat a, Typed a) =>
String -> (Stream a -> Stream a -> Stream a) -> Stream a -> Spec
triggerOp2 (String -> String
mkName String
"sub") (-) Stream a
stream
  String -> (Stream a -> Stream a -> Stream a) -> Stream a -> Spec
forall a.
(RealFloat a, Typed a) =>
String -> (Stream a -> Stream a -> Stream a) -> Stream a -> Spec
triggerOp2 (String -> String
mkName String
"mul") Stream a -> Stream a -> Stream a
forall a. Num a => a -> a -> a
(*) Stream a
stream
  String -> (Stream a -> Stream a -> Stream a) -> Stream a -> Spec
forall a.
(RealFloat a, Typed a) =>
String -> (Stream a -> Stream a -> Stream a) -> Stream a -> Spec
triggerOp2 (String -> String
mkName String
"div") Stream a -> Stream a -> Stream a
forall a. Fractional a => a -> a -> a
(/) Stream a
stream
  String -> (Stream a -> Stream a -> Stream a) -> Stream a -> Spec
forall a.
(RealFloat a, Typed a) =>
String -> (Stream a -> Stream a -> Stream a) -> Stream a -> Spec
triggerOp2 (String -> String
mkName String
"pow") Stream a -> Stream a -> Stream a
forall a. Floating a => a -> a -> a
(**) Stream a
stream
  String -> (Stream a -> Stream a -> Stream a) -> Stream a -> Spec
forall a.
(RealFloat a, Typed a) =>
String -> (Stream a -> Stream a -> Stream a) -> Stream a -> Spec
triggerOp2 (String -> String
mkName String
"logBase") Stream a -> Stream a -> Stream a
forall a. Floating a => a -> a -> a
logBase Stream a
stream
  String -> (Stream a -> Stream a -> Stream a) -> Stream a -> Spec
forall a.
(RealFloat a, Typed a) =>
String -> (Stream a -> Stream a -> Stream a) -> Stream a -> Spec
triggerOp2 (String -> String
mkName String
"atan2") Stream a -> Stream a -> Stream a
forall a.
(Typed a, RealFloat a) =>
Stream a -> Stream a -> Stream a
Copilot.atan2 Stream a
stream

spec :: Spec
spec :: Spec
spec = do
  Proxy Float -> String -> Spec
forall a (proxy :: * -> *).
(RealFloat a, Typed a) =>
proxy a -> String -> Spec
mkSpecFor (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @Float) String
"F"
  Proxy Double -> String -> Spec
forall a (proxy :: * -> *).
(RealFloat a, Typed a) =>
proxy a -> String -> Spec
mkSpecFor (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @Double) String
"D"

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

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

testOp1 :: (RealFloat a, Typed a) =>
           (Stream a -> Stream a) -> Stream a -> Stream Bool
testOp1 :: forall a.
(RealFloat a, Typed a) =>
(Stream a -> Stream a) -> Stream a -> Stream Bool
testOp1 Stream a -> Stream a
op Stream a
stream =
  -- NB: Use (>=) rather than (==) here, as floating-point equality gets weird
  -- due to NaNs.
  Stream a -> Stream a
op Stream a
stream Stream a -> Stream a -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
>= Stream a -> Stream a
op Stream a
stream

testOp2 :: (RealFloat a, Typed a) =>
           (Stream a -> Stream a -> Stream a) -> Stream a -> Stream Bool
testOp2 :: forall a.
(RealFloat a, Typed a) =>
(Stream a -> Stream a -> Stream a) -> Stream a -> Stream Bool
testOp2 Stream a -> Stream a -> Stream a
op Stream a
stream =
  Stream a -> Stream a -> Stream a
op Stream a
stream Stream a
stream Stream a -> Stream a -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
>= Stream a -> Stream a -> Stream a
op Stream a
stream Stream a
stream

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
"fpOps" Spec
spec'