-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.

-- | Abstract syntax for streams and operators.

{-# LANGUAGE GADTs          #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE Rank2Types     #-}
{-# LANGUAGE Safe           #-}

module Copilot.Language.Stream
  ( Stream (..)
  , Arg (..)
  , Copilot.Language.Stream.ceiling
  , Copilot.Language.Stream.floor
  , Copilot.Language.Stream.atan2
  ) where

import Copilot.Core (Typed, typeOf)
import qualified Copilot.Core as Core
import Copilot.Language.Error
import Copilot.Language.Prelude
import qualified Prelude as P

-- | A stream in Copilot is an infinite succession of values of the same type.
--
-- Streams can be built using simple primities (e.g., 'Const'), by applying
-- step-wise (e.g., 'Op1') or temporal transformations (e.g., 'Append', 'Drop')
-- to streams, or by combining existing streams to form new streams (e.g.,
-- 'Op2', 'Op3').

data Stream :: * -> * where
  Append      :: Typed a
              => [a] -> Maybe (Stream Bool) -> Stream a -> Stream a
  Const       :: Typed a => a -> Stream a
  Drop        :: Typed a
              => Int -> Stream a -> Stream a
  Extern      :: Typed a
              => String -> Maybe [a] -> Stream a
  Local       :: (Typed a, Typed b)
              => Stream a -> (Stream a -> Stream b) -> Stream b
  Var         :: Typed a
              => String -> Stream a
  Op1         :: (Typed a, Typed b)
              => Core.Op1 a b -> Stream a -> Stream b
  Op2         :: (Typed a, Typed b, Typed c)
              => Core.Op2 a b c -> Stream a -> Stream b -> Stream c
  Op3         :: (Typed a, Typed b, Typed c, Typed d)
              => Core.Op3 a b c d -> Stream a -> Stream b -> Stream c -> Stream d
  Label       :: Typed a => String -> Stream a -> Stream a

-- | Wrapper to use 'Stream's as arguments to triggers.
data Arg where
  Arg :: Typed a => Stream a -> Arg

-- | Dummy instance in order to make 'Stream' an instance of 'Num'.
instance Show (Stream a) where
  show :: Stream a -> String
show Stream a
_      = String
"Stream"

-- | Dummy instance in order to make 'Stream' an instance of 'Num'.
instance P.Eq (Stream a) where
  == :: Stream a -> Stream a -> Bool
(==)        = forall a. String -> a
badUsage String
"'Prelude.(==)' isn't implemented for streams!"
  /= :: Stream a -> Stream a -> Bool
(/=)        = forall a. String -> a
badUsage String
"'Prelude.(/=)' isn't implemented for streams!"

-- | Streams carrying numbers are instances of 'Num', and you can apply to them
-- the 'Num' functions, point-wise.
instance (Typed a, P.Eq a, Num a) => Num (Stream a) where
  (Const a
x) + :: Stream a -> Stream a -> Stream a
+ (Const a
y)   = forall a. Typed a => a -> Stream a
Const (a
x forall a. Num a => a -> a -> a
+ a
y)
  (Const a
0) + Stream a
y           = Stream a
y
  Stream a
x + (Const a
0)           = Stream a
x
  Stream a
x + Stream a
y                   = forall a b c.
(Typed a, Typed b, Typed c) =>
Op2 a b c -> Stream a -> Stream b -> Stream c
Op2 (forall a. Num a => Type a -> Op2 a a a
Core.Add forall a. Typed a => Type a
typeOf) Stream a
x Stream a
y

  (Const a
x) - :: Stream a -> Stream a -> Stream a
- (Const a
y)   = forall a. Typed a => a -> Stream a
Const (a
x forall a. Num a => a -> a -> a
- a
y)
  Stream a
x - (Const a
0)           = Stream a
x
  Stream a
x - Stream a
y                   = forall a b c.
(Typed a, Typed b, Typed c) =>
Op2 a b c -> Stream a -> Stream b -> Stream c
Op2 (forall a. Num a => Type a -> Op2 a a a
Core.Sub forall a. Typed a => Type a
typeOf) Stream a
x Stream a
y

  (Const a
x) * :: Stream a -> Stream a -> Stream a
* (Const a
y)   = forall a. Typed a => a -> Stream a
Const (a
x forall a. Num a => a -> a -> a
* a
y)
  (Const a
0) * Stream a
_           = forall a. Typed a => a -> Stream a
Const a
0
  Stream a
_ * (Const a
0)           = forall a. Typed a => a -> Stream a
Const a
0
  (Const a
1) * Stream a
y           = Stream a
y
  Stream a
x * (Const a
1)           = Stream a
x
  Stream a
x * Stream a
y                   = forall a b c.
(Typed a, Typed b, Typed c) =>
Op2 a b c -> Stream a -> Stream b -> Stream c
Op2 (forall a. Num a => Type a -> Op2 a a a
Core.Mul forall a. Typed a => Type a
typeOf) Stream a
x Stream a
y

  abs :: Stream a -> Stream a
abs (Const a
x)           = forall a. Typed a => a -> Stream a
Const (forall a. Num a => a -> a
abs a
x)
  abs Stream a
x                   = forall a b. (Typed a, Typed b) => Op1 a b -> Stream a -> Stream b
Op1 (forall a. Num a => Type a -> Op1 a a
Core.Abs forall a. Typed a => Type a
typeOf) Stream a
x

  signum :: Stream a -> Stream a
signum (Const a
x)        = forall a. Typed a => a -> Stream a
Const (forall a. Num a => a -> a
signum a
x)
  signum Stream a
x                = forall a b. (Typed a, Typed b) => Op1 a b -> Stream a -> Stream b
Op1 (forall a. Num a => Type a -> Op1 a a
Core.Sign forall a. Typed a => Type a
typeOf) Stream a
x

  fromInteger :: Integer -> Stream a
fromInteger             = forall a. Typed a => a -> Stream a
Const forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => Integer -> a
fromInteger

-- | Streams carrying fractional numbers are instances of 'Fractional', and you can
-- apply to them the 'Fractional' functions, point-wise.

-- XXX we may not want to precompute these if they're constants if someone is
-- relying on certain floating-point behavior.
instance (Typed a, P.Eq a, Fractional a) => Fractional (Stream a) where
  / :: Stream a -> Stream a -> Stream a
(/)                     = forall a b c.
(Typed a, Typed b, Typed c) =>
Op2 a b c -> Stream a -> Stream b -> Stream c
Op2 (forall a. Fractional a => Type a -> Op2 a a a
Core.Fdiv forall a. Typed a => Type a
typeOf)

  recip :: Stream a -> Stream a
recip (Const a
x)         = forall a. Typed a => a -> Stream a
Const (forall a. Fractional a => a -> a
recip a
x)
  recip Stream a
x                 = forall a b. (Typed a, Typed b) => Op1 a b -> Stream a -> Stream b
Op1 (forall a. Fractional a => Type a -> Op1 a a
Core.Recip forall a. Typed a => Type a
typeOf) Stream a
x

  fromRational :: Rational -> Stream a
fromRational            = forall a. Typed a => a -> Stream a
Const forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Fractional a => Rational -> a
fromRational

-- | Streams carrying floating point numbers are instances of 'Floating', and
-- you can apply to them the 'Floating' functions, point-wise.

-- XXX we may not want to precompute these if they're constants if someone is
-- relying on certain floating-point behavior.
instance (Typed a, Eq a, Floating a) => Floating (Stream a) where
  pi :: Stream a
pi           = forall a. Typed a => a -> Stream a
Const forall a. Floating a => a
pi
  exp :: Stream a -> Stream a
exp          = forall a b. (Typed a, Typed b) => Op1 a b -> Stream a -> Stream b
Op1 (forall a. Floating a => Type a -> Op1 a a
Core.Exp forall a. Typed a => Type a
typeOf)
  sqrt :: Stream a -> Stream a
sqrt         = forall a b. (Typed a, Typed b) => Op1 a b -> Stream a -> Stream b
Op1 (forall a. Floating a => Type a -> Op1 a a
Core.Sqrt forall a. Typed a => Type a
typeOf)
  log :: Stream a -> Stream a
log          = forall a b. (Typed a, Typed b) => Op1 a b -> Stream a -> Stream b
Op1 (forall a. Floating a => Type a -> Op1 a a
Core.Log forall a. Typed a => Type a
typeOf)
  ** :: Stream a -> Stream a -> Stream a
(**)         = forall a b c.
(Typed a, Typed b, Typed c) =>
Op2 a b c -> Stream a -> Stream b -> Stream c
Op2 (forall a. Floating a => Type a -> Op2 a a a
Core.Pow forall a. Typed a => Type a
typeOf)
  logBase :: Stream a -> Stream a -> Stream a
logBase      = forall a b c.
(Typed a, Typed b, Typed c) =>
Op2 a b c -> Stream a -> Stream b -> Stream c
Op2 (forall a. Floating a => Type a -> Op2 a a a
Core.Logb forall a. Typed a => Type a
typeOf)
  sin :: Stream a -> Stream a
sin          = forall a b. (Typed a, Typed b) => Op1 a b -> Stream a -> Stream b
Op1 (forall a. Floating a => Type a -> Op1 a a
Core.Sin forall a. Typed a => Type a
typeOf)
  tan :: Stream a -> Stream a
tan          = forall a b. (Typed a, Typed b) => Op1 a b -> Stream a -> Stream b
Op1 (forall a. Floating a => Type a -> Op1 a a
Core.Tan forall a. Typed a => Type a
typeOf)
  cos :: Stream a -> Stream a
cos          = forall a b. (Typed a, Typed b) => Op1 a b -> Stream a -> Stream b
Op1 (forall a. Floating a => Type a -> Op1 a a
Core.Cos forall a. Typed a => Type a
typeOf)
  asin :: Stream a -> Stream a
asin         = forall a b. (Typed a, Typed b) => Op1 a b -> Stream a -> Stream b
Op1 (forall a. Floating a => Type a -> Op1 a a
Core.Asin forall a. Typed a => Type a
typeOf)
  atan :: Stream a -> Stream a
atan         = forall a b. (Typed a, Typed b) => Op1 a b -> Stream a -> Stream b
Op1 (forall a. Floating a => Type a -> Op1 a a
Core.Atan forall a. Typed a => Type a
typeOf)
  acos :: Stream a -> Stream a
acos         = forall a b. (Typed a, Typed b) => Op1 a b -> Stream a -> Stream b
Op1 (forall a. Floating a => Type a -> Op1 a a
Core.Acos forall a. Typed a => Type a
typeOf)
  sinh :: Stream a -> Stream a
sinh         = forall a b. (Typed a, Typed b) => Op1 a b -> Stream a -> Stream b
Op1 (forall a. Floating a => Type a -> Op1 a a
Core.Sinh forall a. Typed a => Type a
typeOf)
  tanh :: Stream a -> Stream a
tanh         = forall a b. (Typed a, Typed b) => Op1 a b -> Stream a -> Stream b
Op1 (forall a. Floating a => Type a -> Op1 a a
Core.Tanh forall a. Typed a => Type a
typeOf)
  cosh :: Stream a -> Stream a
cosh         = forall a b. (Typed a, Typed b) => Op1 a b -> Stream a -> Stream b
Op1 (forall a. Floating a => Type a -> Op1 a a
Core.Cosh forall a. Typed a => Type a
typeOf)
  asinh :: Stream a -> Stream a
asinh        = forall a b. (Typed a, Typed b) => Op1 a b -> Stream a -> Stream b
Op1 (forall a. Floating a => Type a -> Op1 a a
Core.Asinh forall a. Typed a => Type a
typeOf)
  atanh :: Stream a -> Stream a
atanh        = forall a b. (Typed a, Typed b) => Op1 a b -> Stream a -> Stream b
Op1 (forall a. Floating a => Type a -> Op1 a a
Core.Atanh forall a. Typed a => Type a
typeOf)
  acosh :: Stream a -> Stream a
acosh        = forall a b. (Typed a, Typed b) => Op1 a b -> Stream a -> Stream b
Op1 (forall a. Floating a => Type a -> Op1 a a
Core.Acosh forall a. Typed a => Type a
typeOf)

-- | Point-wise application of @ceiling@ to a stream.
--
-- Unlike the Haskell variant of this function, this variant takes and returns
-- two streams of the same type. Use a casting function to convert the result
-- to an intergral type of your choice.
--
-- Note that the result can be too big (or, if negative, too small) for that
-- type (see the man page of @ceil@ for details), so you must check that the
-- value fits in the desired integral type before casting it.
--
-- This definition clashes with one in 'RealFrac' in Haskell's Prelude,
-- re-exported from @Language.Copilot@, so you need to import this module
-- qualified to use this function.
ceiling :: (Typed a, RealFrac a) => Stream a -> Stream a
ceiling :: forall a. (Typed a, RealFrac a) => Stream a -> Stream a
ceiling = forall a b. (Typed a, Typed b) => Op1 a b -> Stream a -> Stream b
Op1 (forall a. RealFrac a => Type a -> Op1 a a
Core.Ceiling forall a. Typed a => Type a
typeOf)

-- | Point-wise application of @floor@ to a stream.
--
-- Unlike the Haskell variant of this function, this variant takes and returns
-- two streams of the same type. Use a casting function to convert the result
-- to an intergral type of your choice.
--
-- Note that the result can be too big (or, if negative, too small) for that
-- type (see the man page of @floor@ for details), so you must check that the
-- value fits in the desired integral type before casting it.
--
-- This definition clashes with one in 'RealFrac' in Haskell's Prelude,
-- re-exported from @Language.Copilot@, so you need to import this module
-- qualified to use this function.
floor :: (Typed a, RealFrac a) => Stream a -> Stream a
floor :: forall a. (Typed a, RealFrac a) => Stream a -> Stream a
floor = forall a b. (Typed a, Typed b) => Op1 a b -> Stream a -> Stream b
Op1 (forall a. RealFrac a => Type a -> Op1 a a
Core.Floor forall a. Typed a => Type a
typeOf)

-- | Point-wise application of @atan2@ to the values of two streams.
--
-- For each pair of real floating-point samples @x@ and @y@, one from each
-- stream, @atan2@ computes the angle of the vector from @(0, 0)@ to the point
-- @(x, y)@.
--
-- This definition clashes with one in 'RealFloat' in Haskell's Prelude,
-- re-exported from @Language.Copilot@, so you need to import this module
-- qualified to use this function.
atan2 :: (Typed a, RealFloat a) => Stream a -> Stream a -> Stream a
atan2 :: forall a.
(Typed a, RealFloat a) =>
Stream a -> Stream a -> Stream a
atan2 = forall a b c.
(Typed a, Typed b, Typed c) =>
Op2 a b c -> Stream a -> Stream b -> Stream c
Op2 (forall a. RealFloat a => Type a -> Op2 a a a
Core.Atan2 forall a. Typed a => Type a
typeOf)