    {-# LANGUAGE ExistentialQuantification #-}
    {-# LANGUAGE GADTs                     #-}
    {-# LANGUAGE Safe                      #-}

    -- |
    -- Description: Internal representation of Copilot stream expressions.
    -- Copyright:   (c) 2011 National Institute of Aerospace / Galois, Inc.
    module Copilot.Core.Expr
        ( Id
        , Name
        , Expr (..)
        , UExpr (..)
        , DropIdx
        )
      where

    -- External imports
    import Data.Typeable (Typeable)
    import Data.Word     (Word32)

    -- Internal imports
    import Copilot.Core.Operators (Op1, Op2, Op3)
    import Copilot.Core.Type      (Type)

    -- | A stream identifier.
    type Id = Int

    -- | A name of a trigger, an external variable, or an external function.
    type Name = String

    -- | An index for the drop operator.
    type DropIdx = Word32

    -- | Internal representation of Copilot stream expressions.
    --
    -- The Core representation mimics the high-level Copilot stream, but the Core
    -- representation contains information about the types of elements in the
    -- stream.
    data Expr a where
      Const     :: Typeable a
                => Type a -> a -> Expr a

      Drop      :: Typeable a
                => Type a -> DropIdx -> Id -> Expr a

      Local     :: Typeable a
                => Type a -> Type b -> Name -> Expr a -> Expr b -> Expr b

      Var       :: Typeable a
                => Type a -> Name -> Expr a

      ExternVar :: Typeable a
                => Type a -> Name -> Maybe [a] -> Expr a

      Op1       :: Typeable a
                => Op1 a b -> Expr a -> Expr b

      Op2       :: (Typeable a, Typeable b)
                => Op2 a b c -> Expr a -> Expr b -> Expr c

      Op3       :: (Typeable a, Typeable b, Typeable c)
                => Op3 a b c d -> Expr a -> Expr b -> Expr c -> Expr d

      Label     :: Typeable a
                => Type a -> String -> Expr a -> Expr a

    -- | A untyped expression that carries the information about the type of the
    -- expression as a value, as opposed to exposing it at type level (using an
    -- existential).
    data UExpr = forall a . Typeable a => UExpr (Type a) (Expr a)