{-# 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)
data Stream = forall a. (Typeable a, Typed a) => Stream
{ Stream -> Id
streamId :: Id
, ()
streamBuffer :: [a]
, ()
streamExpr :: Expr a
, ()
streamExprType :: Type a }
data Observer = forall a. Typeable a => Observer
{ Observer -> Name
observerName :: Name
, ()
observerExpr :: Expr a
, ()
observerExprType :: Type a }
data Trigger = Trigger
{ Trigger -> Name
triggerName :: Name
, Trigger -> Expr Bool
triggerGuard :: Expr Bool
, Trigger -> [UExpr]
triggerArgs :: [UExpr] }
data Property = Property
{ Property -> Name
propertyName :: Name
, Property -> Expr Bool
propertyExpr :: Expr Bool }
data Spec = Spec
{ Spec -> [Stream]
specStreams :: [Stream]
, Spec -> [Observer]
specObservers :: [Observer]
, Spec -> [Trigger]
specTriggers :: [Trigger]
, Spec -> [Property]
specProperties :: [Property] }