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

-- | Abstract syntax for streams and operators.

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

module Copilot.Language.Stream
  ( Stream (..)
  , Arg (..)
  , StructArg (..)
  ) where

import Copilot.Core (Typed, typeOf)
import Copilot.Core.Error
import qualified Copilot.Core as Core
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

data StructArg = StructArg { StructArg -> String
name_ :: String, StructArg -> Arg
arg' :: 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
(==)        = String -> Stream a -> Stream a -> Bool
forall a. String -> a
badUsage String
"'Prelude.(==)' isn't implemented for streams!"
  /= :: Stream a -> Stream a -> Bool
(/=)        = String -> 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)   = a -> Stream a
forall a. Typed a => a -> Stream a
Const (a
x a -> a -> a
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                   = Op2 a a a -> 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 (Type a -> Op2 a a a
forall a. Num a => Type a -> Op2 a a a
Core.Add Type a
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)   = a -> Stream a
forall a. Typed a => a -> Stream a
Const (a
x a -> a -> a
forall a. Num a => a -> a -> a
- a
y)
  Stream a
x - (Const a
0)           = Stream a
x
  Stream a
x - Stream a
y                   = Op2 a a a -> 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 (Type a -> Op2 a a a
forall a. Num a => Type a -> Op2 a a a
Core.Sub Type a
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)   = a -> Stream a
forall a. Typed a => a -> Stream a
Const (a
x a -> a -> a
forall a. Num a => a -> a -> a
* a
y)
  (Const a
0) * Stream a
_           = a -> Stream a
forall a. Typed a => a -> Stream a
Const a
0
  Stream a
_ * (Const a
0)           = a -> Stream a
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                   = Op2 a a a -> 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 (Type a -> Op2 a a a
forall a. Num a => Type a -> Op2 a a a
Core.Mul Type a
forall a. Typed a => Type a
typeOf) Stream a
x Stream a
y

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

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

  fromInteger :: Integer -> Stream a
fromInteger             = a -> Stream a
forall a. Typed a => a -> Stream a
Const (a -> Stream a) -> (Integer -> a) -> Integer -> Stream a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> a
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
(/)                     = Op2 a a a -> 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 (Type a -> Op2 a a a
forall a. Fractional a => Type a -> Op2 a a a
Core.Fdiv Type a
forall a. Typed a => Type a
typeOf)

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

  fromRational :: Rational -> Stream a
fromRational            = a -> Stream a
forall a. Typed a => a -> Stream a
Const (a -> Stream a) -> (Rational -> a) -> Rational -> Stream a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> a
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           = a -> Stream a
forall a. Typed a => a -> Stream a
Const a
forall a. Floating a => a
pi
  exp :: Stream a -> Stream a
exp          = Op1 a a -> Stream a -> Stream a
forall a b. (Typed a, Typed b) => Op1 a b -> Stream a -> Stream b
Op1 (Type a -> Op1 a a
forall a. Floating a => Type a -> Op1 a a
Core.Exp Type a
forall a. Typed a => Type a
typeOf)
  sqrt :: Stream a -> Stream a
sqrt         = Op1 a a -> Stream a -> Stream a
forall a b. (Typed a, Typed b) => Op1 a b -> Stream a -> Stream b
Op1 (Type a -> Op1 a a
forall a. Floating a => Type a -> Op1 a a
Core.Sqrt Type a
forall a. Typed a => Type a
typeOf)
  log :: Stream a -> Stream a
log          = Op1 a a -> Stream a -> Stream a
forall a b. (Typed a, Typed b) => Op1 a b -> Stream a -> Stream b
Op1 (Type a -> Op1 a a
forall a. Floating a => Type a -> Op1 a a
Core.Log Type a
forall a. Typed a => Type a
typeOf)
  ** :: Stream a -> Stream a -> Stream a
(**)         = Op2 a a a -> 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 (Type a -> Op2 a a a
forall a. Floating a => Type a -> Op2 a a a
Core.Pow Type a
forall a. Typed a => Type a
typeOf)
  logBase :: Stream a -> Stream a -> Stream a
logBase      = Op2 a a a -> 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 (Type a -> Op2 a a a
forall a. Floating a => Type a -> Op2 a a a
Core.Logb Type a
forall a. Typed a => Type a
typeOf)
  sin :: Stream a -> Stream a
sin          = Op1 a a -> Stream a -> Stream a
forall a b. (Typed a, Typed b) => Op1 a b -> Stream a -> Stream b
Op1 (Type a -> Op1 a a
forall a. Floating a => Type a -> Op1 a a
Core.Sin Type a
forall a. Typed a => Type a
typeOf)
  tan :: Stream a -> Stream a
tan          = Op1 a a -> Stream a -> Stream a
forall a b. (Typed a, Typed b) => Op1 a b -> Stream a -> Stream b
Op1 (Type a -> Op1 a a
forall a. Floating a => Type a -> Op1 a a
Core.Tan Type a
forall a. Typed a => Type a
typeOf)
  cos :: Stream a -> Stream a
cos          = Op1 a a -> Stream a -> Stream a
forall a b. (Typed a, Typed b) => Op1 a b -> Stream a -> Stream b
Op1 (Type a -> Op1 a a
forall a. Floating a => Type a -> Op1 a a
Core.Cos Type a
forall a. Typed a => Type a
typeOf)
  asin :: Stream a -> Stream a
asin         = Op1 a a -> Stream a -> Stream a
forall a b. (Typed a, Typed b) => Op1 a b -> Stream a -> Stream b
Op1 (Type a -> Op1 a a
forall a. Floating a => Type a -> Op1 a a
Core.Asin Type a
forall a. Typed a => Type a
typeOf)
  atan :: Stream a -> Stream a
atan         = Op1 a a -> Stream a -> Stream a
forall a b. (Typed a, Typed b) => Op1 a b -> Stream a -> Stream b
Op1 (Type a -> Op1 a a
forall a. Floating a => Type a -> Op1 a a
Core.Atan Type a
forall a. Typed a => Type a
typeOf)
  acos :: Stream a -> Stream a
acos         = Op1 a a -> Stream a -> Stream a
forall a b. (Typed a, Typed b) => Op1 a b -> Stream a -> Stream b
Op1 (Type a -> Op1 a a
forall a. Floating a => Type a -> Op1 a a
Core.Acos Type a
forall a. Typed a => Type a
typeOf)
  sinh :: Stream a -> Stream a
sinh         = Op1 a a -> Stream a -> Stream a
forall a b. (Typed a, Typed b) => Op1 a b -> Stream a -> Stream b
Op1 (Type a -> Op1 a a
forall a. Floating a => Type a -> Op1 a a
Core.Sinh Type a
forall a. Typed a => Type a
typeOf)
  tanh :: Stream a -> Stream a
tanh         = Op1 a a -> Stream a -> Stream a
forall a b. (Typed a, Typed b) => Op1 a b -> Stream a -> Stream b
Op1 (Type a -> Op1 a a
forall a. Floating a => Type a -> Op1 a a
Core.Tanh Type a
forall a. Typed a => Type a
typeOf)
  cosh :: Stream a -> Stream a
cosh         = Op1 a a -> Stream a -> Stream a
forall a b. (Typed a, Typed b) => Op1 a b -> Stream a -> Stream b
Op1 (Type a -> Op1 a a
forall a. Floating a => Type a -> Op1 a a
Core.Cosh Type a
forall a. Typed a => Type a
typeOf)
  asinh :: Stream a -> Stream a
asinh        = Op1 a a -> Stream a -> Stream a
forall a b. (Typed a, Typed b) => Op1 a b -> Stream a -> Stream b
Op1 (Type a -> Op1 a a
forall a. Floating a => Type a -> Op1 a a
Core.Asinh Type a
forall a. Typed a => Type a
typeOf)
  atanh :: Stream a -> Stream a
atanh        = Op1 a a -> Stream a -> Stream a
forall a b. (Typed a, Typed b) => Op1 a b -> Stream a -> Stream b
Op1 (Type a -> Op1 a a
forall a. Floating a => Type a -> Op1 a a
Core.Atanh Type a
forall a. Typed a => Type a
typeOf)
  acosh :: Stream a -> Stream a
acosh        = Op1 a a -> Stream a -> Stream a
forall a b. (Typed a, Typed b) => Op1 a b -> Stream a -> Stream b
Op1 (Type a -> Op1 a a
forall a. Floating a => Type a -> Op1 a a
Core.Acosh Type a
forall a. Typed a => Type a
typeOf)

--------------------------------------------------------------------------------