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

-- |
-- Description: Internal representation of Copilot operators.
-- Copyright:   (c) 2011 National Institute of Aerospace / Galois, Inc.
module Copilot.Core.Operators
    ( Op1 (..)
    , Op2 (..)
    , Op3 (..)
    )
  where

-- External imports
import Data.Bits     (Bits)
import Data.Typeable (Typeable)
import Data.Word     (Word32)
import GHC.TypeLits  (KnownSymbol)

-- Internal imports
import Copilot.Core.Type       (Field (..), Type (..))
import Copilot.Core.Type.Array (Array)

-- | Unary operators.
data Op1 a b where
  -- Boolean operators.
  Not      :: Op1 Bool Bool
  -- Numeric operators.
  Abs      :: Num a => Type a -> Op1 a a
  Sign     :: Num a => Type a -> Op1 a a
  -- Fractional operators.
  Recip    :: Fractional a => Type a -> Op1 a a
  -- Floating operators.
  Exp      :: Floating a => Type a -> Op1 a a
  Sqrt     :: Floating a => Type a -> Op1 a a
  Log      :: Floating a => Type a -> Op1 a a
  Sin      :: Floating a => Type a -> Op1 a a
  Tan      :: Floating a => Type a -> Op1 a a
  Cos      :: Floating a => Type a -> Op1 a a
  Asin     :: Floating a => Type a -> Op1 a a
  Atan     :: Floating a => Type a -> Op1 a a
  Acos     :: Floating a => Type a -> Op1 a a
  Sinh     :: Floating a => Type a -> Op1 a a
  Tanh     :: Floating a => Type a -> Op1 a a
  Cosh     :: Floating a => Type a -> Op1 a a
  Asinh    :: Floating a => Type a -> Op1 a a
  Atanh    :: Floating a => Type a -> Op1 a a
  Acosh    :: Floating a => Type a -> Op1 a a
  -- RealFrac operators
  Ceiling  :: RealFrac a => Type a -> Op1 a a
  Floor    :: RealFrac a => Type a -> Op1 a a
  -- Bitwise operators.
  BwNot    :: Bits a => Type a -> Op1 a a
  -- Casting operator.
  Cast     :: (Integral a, Num b) => Type a -> Type b -> Op1 a b
              -- ^ Casting operator.

  -- Struct operator.
  GetField :: KnownSymbol s => Type a -> Type b -> (a -> Field s b) -> Op1 a b
              -- ^ Projection of a struct field.

-- | Binary operators.
data Op2 a b c where
  -- Boolean operators.
  And      :: Op2 Bool Bool Bool
  Or       :: Op2 Bool Bool Bool
  -- Numeric operators.
  Add      :: Num a => Type a -> Op2 a a a
  Sub      :: Num a => Type a -> Op2 a a a
  Mul      :: Num a => Type a -> Op2 a a a
  -- Integral operators.
  Mod      :: Integral a => Type a -> Op2 a a a
  Div      :: Integral a => Type a -> Op2 a a a
  -- Fractional operators.
  Fdiv     :: Fractional a => Type a -> Op2 a a a
  -- Floating operators.
  Pow      :: Floating a => Type a -> Op2 a a a
  Logb     :: Floating a => Type a -> Op2 a a a
  -- RealFloat operators.
  Atan2    :: RealFloat a => Type a -> Op2 a a a
  -- Equality operators.
  Eq       :: Eq a => Type a -> Op2 a a Bool
  Ne       :: Eq a => Type a -> Op2 a a Bool
  -- Relational operators.
  Le       :: Ord a => Type a -> Op2 a a Bool
  Ge       :: Ord a => Type a -> Op2 a a Bool
  Lt       :: Ord a => Type a -> Op2 a a Bool
  Gt       :: Ord a => Type a -> Op2 a a Bool
  -- Bitwise operators.
  BwAnd    :: Bits a => Type a -> Op2 a a a
  BwOr     :: Bits a => Type a -> Op2 a a a
  BwXor    :: Bits a => Type a -> Op2 a a a
  BwShiftL :: (Bits a, Integral b) => Type a -> Type b -> Op2 a b a
  BwShiftR :: (Bits a, Integral b) => Type a -> Type b -> Op2 a b a
  -- Array operator.
  Index    :: Type (Array n t) -> Op2 (Array n t) Word32 t
              -- ^ Array access/projection of an array element.

  -- Struct operator.
  UpdateField :: (Typeable b, KnownSymbol s, Show b)
              => Type a -> Type b -> (a -> Field s b) -> Op2 a b a
              -- ^ Update a field of a struct.

-- | Ternary operators.
data Op3 a b c d where
  -- Conditional operator.
  Mux :: Type a -> Op3 Bool a a a
  -- Array operator.
  UpdateArray :: Type (Array n t) -> Op3 (Array n t) Word32 t (Array n t)
           -- ^ Update an element of an array.