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

    {-# LANGUAGE GADTs          #-}
    {-# LANGUAGE KindSignatures #-}
    {-# LANGUAGE RankNTypes     #-}
    {-# LANGUAGE Safe           #-}

    -- | Copilot specifications consistute 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, 'Spec's must be turned into Copilot Core (see
    -- 'Reify') and either simulated or converted into C99 code to be executed.
    module Copilot.Language.Spec
      ( Spec, Spec'
      , runSpec
      , SpecItem
      , Observer (..)
      , observer, observers
      , Trigger (..)
      , trigger, triggers
      , arg
      , Arg(..)
      , Property (..)
      , Prop (..)
      , prop, properties
      , theorem, theorems
      , forAll
      , exists
      , extractProp
      , Universal, Existential
      ) where

    import Prelude hiding (not)

    import Control.Monad.Writer

    import Copilot.Core (Typed)
    import qualified Copilot.Core as Core
    import Copilot.Language.Stream

    import Copilot.Theorem.Prove

    -- | A specification is a list of declarations of triggers, observers,
    -- properties and theorems.
    --
    -- Specifications are normally declared in monadic style, for example:
    --
    -- @
    -- monitor1 :: Stream Bool
    -- monitor1 = [False] ++ not monitor1
    --
    -- counter :: Stream Int32
    -- counter = [0] ++ not counter
    --
    -- spec :: Spec
    -- spec = do
    --   trigger "handler_1" monitor1 []
    --   trigger "handler_2" (counter > 10) [arg counter]
    -- @
    type Spec = Writer [SpecItem] ()

    -- | An action in a specification (e.g., a declaration) that returns a value that
    -- can be used in subsequent actions.
    type Spec' a = Writer [SpecItem] a

    -- | Return the complete list of declarations inside a 'Spec' or 'Spec''.
    --
    -- The word run in this function is unrelated to running the underlying
    -- specifications or monitors, and is merely related to the monad defined by a
    -- 'Spec'
    runSpec :: Spec' a -> [SpecItem]
    runSpec :: forall a. Spec' a -> [SpecItem]
    runSpec = Writer [SpecItem] a -> [SpecItem]
    forall w a. Writer w a -> w
    execWriter

    -- | Filter a list of spec items to keep only the observers.
    observers :: [SpecItem] -> [Observer]
    observers :: [SpecItem] -> [Observer]
    observers =
      (SpecItem -> [Observer] -> [Observer])
    -> [Observer] -> [SpecItem] -> [Observer]
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr SpecItem -> [Observer] -> [Observer]
    lets' []
      where
      lets' :: SpecItem -> [Observer] -> [Observer]
    lets' SpecItem
    e [Observer]
    ls =
        case SpecItem
    e of
          ObserverItem Observer
    l -> Observer
    l Observer -> [Observer] -> [Observer]
    forall a. a -> [a] -> [a]
    : [Observer]
    ls
          SpecItem
    _              -> [Observer]
    ls

    -- | Filter a list of spec items to keep only the triggers.
    triggers :: [SpecItem] -> [Trigger]
    triggers :: [SpecItem] -> [Trigger]
    triggers =
      (SpecItem -> [Trigger] -> [Trigger])
    -> [Trigger] -> [SpecItem] -> [Trigger]
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr SpecItem -> [Trigger] -> [Trigger]
    triggers' []
      where
      triggers' :: SpecItem -> [Trigger] -> [Trigger]
    triggers' SpecItem
    e [Trigger]
    ls =
        case SpecItem
    e of
          TriggerItem Trigger
    t -> Trigger
    t Trigger -> [Trigger] -> [Trigger]
    forall a. a -> [a] -> [a]
    : [Trigger]
    ls
          SpecItem
    _             -> [Trigger]
    ls

    -- | Filter a list of spec items to keep only the properties.
    properties :: [SpecItem] -> [Property]
    properties :: [SpecItem] -> [Property]
    properties =
      (SpecItem -> [Property] -> [Property])
    -> [Property] -> [SpecItem] -> [Property]
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr SpecItem -> [Property] -> [Property]
    properties' []
      where
      properties' :: SpecItem -> [Property] -> [Property]
    properties' SpecItem
    e [Property]
    ls =
        case SpecItem
    e of
          PropertyItem Property
    p -> Property
    p Property -> [Property] -> [Property]
    forall a. a -> [a] -> [a]
    : [Property]
    ls
          SpecItem
    _              -> [Property]
    ls

    -- | Filter a list of spec items to keep only the theorems.
    theorems :: [SpecItem] -> [(Property, UProof)]
    theorems :: [SpecItem] -> [(Property, UProof)]
    theorems =
      (SpecItem -> [(Property, UProof)] -> [(Property, UProof)])
    -> [(Property, UProof)] -> [SpecItem] -> [(Property, UProof)]
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr SpecItem -> [(Property, UProof)] -> [(Property, UProof)]
    theorems' []
      where
      theorems' :: SpecItem -> [(Property, UProof)] -> [(Property, UProof)]
    theorems' SpecItem
    e [(Property, UProof)]
    ls =
        case SpecItem
    e of
          TheoremItem (Property, UProof)
    p -> (Property, UProof)
    p (Property, UProof) -> [(Property, UProof)] -> [(Property, UProof)]
    forall a. a -> [a] -> [a]
    : [(Property, UProof)]
    ls
          SpecItem
    _              -> [(Property, UProof)]
    ls

    -- | An item of a Copilot specification.
    data SpecItem
      = ObserverItem Observer
      | TriggerItem  Trigger
      | PropertyItem Property
      | TheoremItem (Property, UProof)

    -- | An observer, representing a stream that we observe during execution at
    -- every sample.
    data Observer where
      Observer :: Typed a => String -> Stream a -> Observer

    -- | Define a new observer as part of a specification. This allows someone to
    -- print the value at every iteration during interpretation. Observers do not
    -- have any functionality outside the interpreter.
    observer :: Typed a
             => String    -- ^ Name used to identify the stream monitored in the
                          -- output produced during interpretation.
             -> Stream a  -- ^ The stream being monitored.
             -> Spec
    observer :: forall a. Typed a => String -> Stream a -> Spec
    observer String
    name Stream a
    e = [SpecItem] -> Spec
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell [Observer -> SpecItem
    ObserverItem (Observer -> SpecItem) -> Observer -> SpecItem
    forall a b. (a -> b) -> a -> b
    $ String -> Stream a -> Observer
    forall a. Typed a => String -> Stream a -> Observer
    Observer String
    name Stream a
    e]

    -- | A trigger, representing a function we execute when a boolean stream becomes
    -- true at a sample.
    data Trigger where
      Trigger :: Core.Name -> Stream Bool -> [Arg] -> Trigger

    -- | Define a new trigger as part of a specification. A trigger declares which
    -- external function, or handler, will be called when a guard defined by a
    -- boolean stream becomes true.
    trigger :: String       -- ^ Name of the handler to be called.
            -> Stream Bool  -- ^ The stream used as the guard for the trigger.
            -> [Arg]        -- ^ List of arguments to the handler.
            -> Spec
    trigger :: String -> Stream Bool -> [Arg] -> Spec
    trigger String
    name Stream Bool
    e [Arg]
    args = [SpecItem] -> Spec
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell [Trigger -> SpecItem
    TriggerItem (Trigger -> SpecItem) -> Trigger -> SpecItem
    forall a b. (a -> b) -> a -> b
    $ String -> Stream Bool -> [Arg] -> Trigger
    Trigger String
    name Stream Bool
    e [Arg]
    args]

    -- | A property, representing a boolean stream that is existentially or
    -- universally quantified over time.
    data Property where
      Property :: String -> Prop a -> Property

    -- | A proposition, representing the quantification of a boolean streams over
    -- time.
    data Prop a where
      Forall :: Stream Bool -> Prop Universal
      Exists :: Stream Bool -> Prop Existential

    -- | Universal quantification of boolean streams over time.
    forAll :: Stream Bool -> Prop Universal
    forAll :: Stream Bool -> Prop Universal
    forAll = Stream Bool -> Prop Universal
    Forall

    -- | Existential quantification of boolean streams over time.
    exists :: Stream Bool -> Prop Existential
    exists :: Stream Bool -> Prop Existential
    exists = Stream Bool -> Prop Existential
    Exists

    -- | 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 a -> Stream Bool
    extractProp :: forall a. Prop a -> Stream Bool
    extractProp (Forall Stream Bool
    p) = Stream Bool
    p
    extractProp (Exists Stream Bool
    p) = Stream Bool
    p

    -- | A proposition, representing a boolean stream that is existentially or
    -- universally quantified over time, as part of a specification.
    --
    -- This function returns, in the monadic context, a reference to the
    -- proposition.
    prop :: String -> Prop a -> Writer [SpecItem] (PropRef a)
    prop :: forall a. String -> Prop a -> Writer [SpecItem] (PropRef a)
    prop String
    name Prop a
    e = [SpecItem] -> Spec
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell [Property -> SpecItem
    PropertyItem (Property -> SpecItem) -> Property -> SpecItem
    forall a b. (a -> b) -> a -> b
    $ String -> Prop a -> Property
    forall a. String -> Prop a -> Property
    Property String
    name Prop a
    e]
      Spec
    -> WriterT [SpecItem] Identity (PropRef a)
    -> WriterT [SpecItem] Identity (PropRef a)
    forall a b.
    WriterT [SpecItem] Identity a
    -> WriterT [SpecItem] Identity b -> WriterT [SpecItem] Identity b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> PropRef a -> WriterT [SpecItem] Identity (PropRef a)
    forall a. a -> WriterT [SpecItem] Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (String -> PropRef a
    forall a. String -> PropRef a
    PropRef String
    name)

    -- | A theorem, or proposition together with a proof.
    --
    -- This function returns, in the monadic context, a reference to the
    -- proposition.
    theorem :: String -> Prop a -> Proof a -> Writer [SpecItem] (PropRef a)
    theorem :: forall a.
    String -> Prop a -> Proof a -> Writer [SpecItem] (PropRef a)
    theorem String
    name Prop a
    e (Proof UProof
    p) = [SpecItem] -> Spec
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell [(Property, UProof) -> SpecItem
    TheoremItem (String -> Prop a -> Property
    forall a. String -> Prop a -> Property
    Property String
    name Prop a
    e, UProof
    p)]
      Spec
    -> WriterT [SpecItem] Identity (PropRef a)
    -> WriterT [SpecItem] Identity (PropRef a)
    forall a b.
    WriterT [SpecItem] Identity a
    -> WriterT [SpecItem] Identity b -> WriterT [SpecItem] Identity b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> PropRef a -> WriterT [SpecItem] Identity (PropRef a)
    forall a. a -> WriterT [SpecItem] Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (String -> PropRef a
    forall a. String -> PropRef a
    PropRef String
    name)

    -- | Construct a function argument from a stream.
    --
    -- 'Arg's can be used to pass arguments to handlers or trigger functions, to
    -- provide additional information to monitor handlers in order to address
    -- property violations. At any given point (e.g., when the trigger must be
    -- called due to a violation), the arguments passed using 'arg' will contain
    -- the current samples of the given streams.
    arg :: Typed a => Stream a -> Arg
    arg :: forall a. Typed a => Stream a -> Arg
    arg = Stream a -> Arg
    forall a. Typed a => Stream a -> Arg
    Arg

    -- | Wrapper to use 'Stream's as arguments to triggers.
    data Arg where
      Arg :: Typed a => Stream a -> Arg