content: {-# 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.
  