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