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

    -- |
    -- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc.
    --
    -- Copilot specifications constitute the main declaration of Copilot modules.
    --
    -- A specification normally contains the association between streams to monitor
    -- and their handling functions, or streams to observe, or a theorem that must
    -- be proved.
    --
    -- In order to be executed, high-level Copilot Language Spec must be turned
    -- into Copilot Core's 'Spec'. This module defines the low-level Copilot Core
    -- representations for Specs and the main types of element in a spec.
    module Copilot.Core.Spec
        ( Stream (..)
        , Observer (..)
        , Trigger (..)
        , Spec (..)
        , Property (..)
        , Prop (..)
        , extractProp
        )
      where

    -- External imports
    import Data.Typeable (Typeable)

    -- Internal imports
    import Copilot.Core.Expr (Expr, Id, Name, UExpr)
    import Copilot.Core.Type (Type, Typed)

    -- | A stream in an infinite succession of values of the same type.
    --
    -- Stream can carry different types of data. Boolean streams play a special
    -- role: they are used by other parts (e.g., 'Trigger') to detect when the
    -- properties being monitored are violated.
    data Stream = forall a . (Typeable a, Typed a) => Stream
      { Stream -> Id
    streamId       :: Id
      , ()
    streamBuffer   :: [a]
      , ()
    streamExpr     :: Expr a
      , ()
    streamExprType :: Type a
      }

    -- | An observer, representing a stream that we observe during interpretation
    -- at every sample.
    data Observer = forall a . Typeable a => Observer
      { Observer -> Name
    observerName     :: Name
      , ()
    observerExpr     :: Expr a
      , ()
    observerExprType :: Type a
      }

    -- | A trigger, representing a function we execute when a boolean stream becomes
    -- true at a sample.
    data Trigger = Trigger
      { Trigger -> Name
    triggerName  :: Name
      , Trigger -> Expr Bool
    triggerGuard :: Expr Bool
      , Trigger -> [UExpr]
    triggerArgs  :: [UExpr]
      }

    -- | A property, representing a boolean stream that is existentially or
    -- universally quantified over time.
    data Property = Property
      { Property -> Name
    propertyName :: Name
      , Property -> Prop
    propertyProp :: Prop
      }

    -- | A proposition, representing a boolean stream that is existentially or
    -- universally quantified over time.
    data Prop
      = Forall (Expr Bool)
      | Exists (Expr Bool)

    -- | Extract the underlying stream from a quantified proposition.
    --
    -- Think carefully before using this function, as this function will remove the
    -- quantifier from a proposition. Universally quantified streams usually require
    -- separate treatment from existentially quantified ones, so carelessly using
    -- this function to remove quantifiers can result in hard-to-spot soundness
    -- bugs.
    extractProp :: Prop -> Expr Bool
    extractProp :: Prop -> Expr Bool
    extractProp (Forall Expr Bool
    e) = Expr Bool
    e
    extractProp (Exists Expr Bool
    e) = Expr Bool
    e

    -- | A Copilot specification is a list of streams, together with monitors on
    -- these streams implemented as observers, triggers or properties.
    data Spec = Spec
      { Spec -> [Stream]
    specStreams    :: [Stream]
      , Spec -> [Observer]
    specObservers  :: [Observer]
      , Spec -> [Trigger]
    specTriggers   :: [Trigger]
      , Spec -> [Property]
    specProperties :: [Property]
      }