{-# 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]
  }