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

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

module Copilot.Core.Spec
  ( Stream (..)
  , Observer (..)
  , Trigger (..)
  , Spec (..)
  , Property (..)
  ) where

import Copilot.Core.Expr (Name, Id, Expr, UExpr)
import Copilot.Core.Type (Type, Typed)
import Data.Typeable (Typeable)

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

-- | A stream.
data Stream = forall a. (Typeable a, Typed a) => Stream
  { Stream -> Id
streamId         :: Id
  , ()
streamBuffer     :: [a]
  , ()
streamExpr       :: Expr a
  , ()
streamExprType   :: Type a }

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

-- | An observer.
data Observer = forall a. Typeable a => Observer
  { Observer -> Name
observerName     :: Name
  , ()
observerExpr     :: Expr a
  , ()
observerExprType :: Type a }

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

-- | A trigger.
data Trigger = Trigger
  { Trigger -> Name
triggerName      :: Name
  , Trigger -> Expr Bool
triggerGuard     :: Expr Bool
  , Trigger -> [UExpr]
triggerArgs      :: [UExpr] }

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

-- | A property.
data Property = Property
  { Property -> Name
propertyName     :: Name
  , Property -> Expr Bool
propertyExpr     :: Expr Bool }

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

-- | A Copilot specification consists of a list of variables bound to anonymous
-- streams, a list of anomymous streams, a list of observers, a list of
-- triggers, and a list of structs.
data Spec = Spec
  { Spec -> [Stream]
specStreams      :: [Stream]
  , Spec -> [Observer]
specObservers    :: [Observer]
  , Spec -> [Trigger]
specTriggers     :: [Trigger]
  , Spec -> [Property]
specProperties   :: [Property] }

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