-- 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