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

-- | Specification of Copilot streams as modular transition systems.
module Copilot.Theorem.TransSys.Spec
  ( module Copilot.Theorem.TransSys.Operators
  , module Copilot.Theorem.TransSys.Type
  , module Copilot.Theorem.TransSys.Invariants
  , TransSys (..)
  , Node (..)
  , PropId
  , NodeId
  , Var (..)
  , ExtVar (..)
  , VarDef (..)
  , VarDescr (..)
  , Expr (..)
  , mkExtVar
  , transformExpr
  , isTopologicallySorted
  , nodeVarsSet
  , specDependenciesGraph
  , specTopNode ) where

import Copilot.Theorem.TransSys.Type
import Copilot.Theorem.TransSys.Operators
import Copilot.Theorem.TransSys.Invariants

import Copilot.Theorem.Misc.Utils

import Control.Applicative (liftA2)
import Control.Monad (foldM, guard)

import Data.Maybe
import Data.Monoid ((<>))
import Data.Map (Map)
import Data.Set (Set, isSubsetOf, member)
import Data.Bimap (Bimap)

import qualified Data.List  as List
import qualified Data.Map   as Map
import qualified Data.Set   as Set
import qualified Data.Bimap as Bimap

-- | Unique name that identifies a node.
type NodeId = String

-- | Unique name that identifies a property.
type PropId = String

-- | A modular transition system is defined by a graph of nodes and a series
-- of properties, each mapped to a variable.
data TransSys = TransSys
  { TransSys -> [Node]
specNodes         :: [Node]
  , TransSys -> NodeId
specTopNodeId     :: NodeId
  , TransSys -> Map NodeId ExtVar
specProps         :: Map PropId ExtVar }

-- | A node is a set of variables living in a local namespace and corresponding
-- to the 'Var' type.
data Node = Node
  { Node -> NodeId
nodeId            :: NodeId
  , Node -> [NodeId]
nodeDependencies  :: [NodeId]          -- ^ Nodes from which variables are
                                           --   imported.
  , Node -> Map Var VarDescr
nodeLocalVars     :: Map Var VarDescr  -- ^ Locally defined variables,
                                           --   either as the previous value of
                                           --   another variable (using 'Pre'),
                                           --   an expression involving
                                           --   variables (using 'Expr') or a
                                           --   set of constraints (using
                                           --   'Constrs').
  , Node -> Bimap Var ExtVar
nodeImportedVars  :: Bimap Var ExtVar  -- ^ Binds each imported variable to
                                           --   its local name.
  , Node -> [Expr Bool]
nodeConstrs       :: [Expr Bool] }

-- | Identifer of a variable in the local (within one node) namespace.
data Var      =  Var {Var -> NodeId
varName :: String}
  deriving (Var -> Var -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Var -> Var -> Bool
$c/= :: Var -> Var -> Bool
== :: Var -> Var -> Bool
$c== :: Var -> Var -> Bool
Eq, Int -> Var -> ShowS
[Var] -> ShowS
Var -> NodeId
forall a.
(Int -> a -> ShowS) -> (a -> NodeId) -> ([a] -> ShowS) -> Show a
showList :: [Var] -> ShowS
$cshowList :: [Var] -> ShowS
show :: Var -> NodeId
$cshow :: Var -> NodeId
showsPrec :: Int -> Var -> ShowS
$cshowsPrec :: Int -> Var -> ShowS
Show, Eq Var
Var -> Var -> Bool
Var -> Var -> Ordering
Var -> Var -> Var
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Var -> Var -> Var
$cmin :: Var -> Var -> Var
max :: Var -> Var -> Var
$cmax :: Var -> Var -> Var
>= :: Var -> Var -> Bool
$c>= :: Var -> Var -> Bool
> :: Var -> Var -> Bool
$c> :: Var -> Var -> Bool
<= :: Var -> Var -> Bool
$c<= :: Var -> Var -> Bool
< :: Var -> Var -> Bool
$c< :: Var -> Var -> Bool
compare :: Var -> Var -> Ordering
$ccompare :: Var -> Var -> Ordering
Ord)

-- | Identifer of a variable in the global namespace by specifying both a node
-- name and a variable.
data ExtVar   =  ExtVar {ExtVar -> NodeId
extVarNode :: NodeId, ExtVar -> Var
extVarLocalPart :: Var }
  deriving (ExtVar -> ExtVar -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ExtVar -> ExtVar -> Bool
$c/= :: ExtVar -> ExtVar -> Bool
== :: ExtVar -> ExtVar -> Bool
$c== :: ExtVar -> ExtVar -> Bool
Eq, Eq ExtVar
ExtVar -> ExtVar -> Bool
ExtVar -> ExtVar -> Ordering
ExtVar -> ExtVar -> ExtVar
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ExtVar -> ExtVar -> ExtVar
$cmin :: ExtVar -> ExtVar -> ExtVar
max :: ExtVar -> ExtVar -> ExtVar
$cmax :: ExtVar -> ExtVar -> ExtVar
>= :: ExtVar -> ExtVar -> Bool
$c>= :: ExtVar -> ExtVar -> Bool
> :: ExtVar -> ExtVar -> Bool
$c> :: ExtVar -> ExtVar -> Bool
<= :: ExtVar -> ExtVar -> Bool
$c<= :: ExtVar -> ExtVar -> Bool
< :: ExtVar -> ExtVar -> Bool
$c< :: ExtVar -> ExtVar -> Bool
compare :: ExtVar -> ExtVar -> Ordering
$ccompare :: ExtVar -> ExtVar -> Ordering
Ord)

-- | A description of a variable together with its type.
data VarDescr = forall t . VarDescr
  { ()
varType :: Type t
  , ()
varDef  :: VarDef t }

-- | A variable definition either as a delay, an operation on variables, or
-- a constraint.
data VarDef t = Pre t Var | Expr (Expr t) | Constrs [Expr Bool]

-- | A point-wise (time-wise) expression.
data Expr t where
  Const :: Type t -> t -> Expr t
  Ite   :: Type t -> Expr Bool -> Expr t -> Expr t -> Expr t
  Op1   :: Type t -> Op1 t -> Expr t -> Expr t
  Op2   :: Type t -> Op2 a t -> Expr a -> Expr a -> Expr t
  VarE  :: Type t -> Var -> Expr t

-- | Constructor for variables identifiers in the global namespace.
mkExtVar :: NodeId -> NodeId -> ExtVar
mkExtVar NodeId
node NodeId
name = NodeId -> Var -> ExtVar
ExtVar NodeId
node (NodeId -> Var
Var NodeId
name)

foldExpr :: (Monoid m) => (forall t . Expr t -> m) -> Expr a -> m
foldExpr :: forall m a. Monoid m => (forall t. Expr t -> m) -> Expr a -> m
foldExpr forall t. Expr t -> m
f Expr a
expr = forall t. Expr t -> m
f Expr a
expr forall a. Semigroup a => a -> a -> a
<> m
fargs
  where
    fargs :: m
fargs = case Expr a
expr of
      (Ite Type a
_ Expr Bool
c Expr a
e1 Expr a
e2)  -> forall m a. Monoid m => (forall t. Expr t -> m) -> Expr a -> m
foldExpr forall t. Expr t -> m
f Expr Bool
c forall a. Semigroup a => a -> a -> a
<> forall m a. Monoid m => (forall t. Expr t -> m) -> Expr a -> m
foldExpr forall t. Expr t -> m
f Expr a
e1 forall a. Semigroup a => a -> a -> a
<> forall m a. Monoid m => (forall t. Expr t -> m) -> Expr a -> m
foldExpr forall t. Expr t -> m
f Expr a
e2
      (Op1 Type a
_ Op1 a
_ Expr a
e)      -> forall m a. Monoid m => (forall t. Expr t -> m) -> Expr a -> m
foldExpr forall t. Expr t -> m
f Expr a
e
      (Op2 Type a
_ Op2 a a
_ Expr a
e1 Expr a
e2)  -> forall m a. Monoid m => (forall t. Expr t -> m) -> Expr a -> m
foldExpr forall t. Expr t -> m
f Expr a
e1 forall a. Semigroup a => a -> a -> a
<> forall m a. Monoid m => (forall t. Expr t -> m) -> Expr a -> m
foldExpr forall t. Expr t -> m
f Expr a
e2
      Expr a
_                -> forall a. Monoid a => a
mempty

foldUExpr :: (Monoid m) => (forall t . Expr t -> m) -> U Expr -> m
foldUExpr :: forall m. Monoid m => (forall t. Expr t -> m) -> U Expr -> m
foldUExpr forall t. Expr t -> m
f (U Expr t
e) = forall m a. Monoid m => (forall t. Expr t -> m) -> Expr a -> m
foldExpr forall t. Expr t -> m
f Expr t
e

-- | Apply an arbitrary transformation to the leafs of an expression.
transformExpr :: (forall a . Expr a -> Expr a) -> Expr t -> Expr t
transformExpr :: forall t. (forall a. Expr a -> Expr a) -> Expr t -> Expr t
transformExpr forall a. Expr a -> Expr a
f = forall a. Expr a -> Expr a
tre
  where
    tre :: forall t . Expr t -> Expr t
    tre :: forall a. Expr a -> Expr a
tre (Ite Type t
t Expr Bool
c Expr t
e1 Expr t
e2)   = forall a. Expr a -> Expr a
f (forall t. Type t -> Expr Bool -> Expr t -> Expr t -> Expr t
Ite Type t
t (forall a. Expr a -> Expr a
tre Expr Bool
c) (forall a. Expr a -> Expr a
tre Expr t
e1) (forall a. Expr a -> Expr a
tre Expr t
e2))
    tre (Op1 Type t
t Op1 t
op Expr t
e)      = forall a. Expr a -> Expr a
f (forall t. Type t -> Op1 t -> Expr t -> Expr t
Op1 Type t
t Op1 t
op (forall a. Expr a -> Expr a
tre Expr t
e))
    tre (Op2 Type t
t Op2 a t
op Expr a
e1 Expr a
e2)  = forall a. Expr a -> Expr a
f (forall t a. Type t -> Op2 a t -> Expr a -> Expr a -> Expr t
Op2 Type t
t Op2 a t
op (forall a. Expr a -> Expr a
tre Expr a
e1) (forall a. Expr a -> Expr a
tre Expr a
e2))
    tre Expr t
e                 = forall a. Expr a -> Expr a
f Expr t
e

-- | The set of variables related to a node (union of the local variables and
-- the imported variables after deferencing them).
nodeVarsSet :: Node -> Set Var
nodeVarsSet :: Node -> Set Var
nodeVarsSet = forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 forall a. Ord a => Set a -> Set a -> Set a
Set.union
  Node -> Set Var
nodeLocalVarsSet
  (forall k a. Map k a -> Set k
Map.keysSet forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. Bimap a b -> Map a b
Bimap.toMap  forall b c a. (b -> c) -> (a -> b) -> a -> c
. Node -> Bimap Var ExtVar
nodeImportedVars)

nodeLocalVarsSet :: Node -> Set Var
nodeLocalVarsSet :: Node -> Set Var
nodeLocalVarsSet = forall k a. Map k a -> Set k
Map.keysSet forall b c a. (b -> c) -> (a -> b) -> a -> c
. Node -> Map Var VarDescr
nodeLocalVars

nodeRhsVarsSet :: Node -> Set Var
nodeRhsVarsSet :: Node -> Set Var
nodeRhsVarsSet Node
n =
  let varOcc :: Expr t -> Set Var
varOcc (VarE Type t
_ Var
v) = forall a. a -> Set a
Set.singleton Var
v
      varOcc Expr t
_          = forall a. Set a
Set.empty

      descrRhsVars :: VarDescr -> Set Var
descrRhsVars (VarDescr Type t
_ (Expr Expr t
e))      = forall m a. Monoid m => (forall t. Expr t -> m) -> Expr a -> m
foldExpr forall {t}. Expr t -> Set Var
varOcc Expr t
e
      descrRhsVars (VarDescr Type t
_ (Pre t
_ Var
v))     = forall a. a -> Set a
Set.singleton Var
v
      descrRhsVars (VarDescr Type t
_ (Constrs [Expr Bool]
cs))  =
        forall a. Monoid a => [a] -> a
mconcat (forall a b. (a -> b) -> [a] -> [b]
map (forall m a. Monoid m => (forall t. Expr t -> m) -> Expr a -> m
foldExpr forall {t}. Expr t -> Set Var
varOcc) [Expr Bool]
cs)

  in forall a b k. (a -> b -> b) -> b -> Map k a -> b
Map.foldr (forall a. Ord a => Set a -> Set a -> Set a
Set.union forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarDescr -> Set Var
descrRhsVars) forall a. Set a
Set.empty (Node -> Map Var VarDescr
nodeLocalVars Node
n)

nodeImportedExtVarsSet :: Node -> Set ExtVar
nodeImportedExtVarsSet :: Node -> Set ExtVar
nodeImportedExtVarsSet = forall k a. Map k a -> Set k
Map.keysSet forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. Bimap a b -> Map b a
Bimap.toMapR forall b c a. (b -> c) -> (a -> b) -> a -> c
. Node -> Bimap Var ExtVar
nodeImportedVars

nodeExportedExtVarsSet :: Node -> Set ExtVar
nodeExportedExtVarsSet :: Node -> Set ExtVar
nodeExportedExtVarsSet Node
n = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (NodeId -> Var -> ExtVar
ExtVar forall a b. (a -> b) -> a -> b
$ Node -> NodeId
nodeId Node
n) (Node -> Set Var
nodeLocalVarsSet Node
n)

instance HasInvariants Node where

  invariants :: Node -> [(NodeId, Bool)]
invariants Node
n =
    [ NodeId -> Bool -> (NodeId, Bool)
prop NodeId
"The dependencies declaration doesn't lie" forall a b. (a -> b) -> a -> b
$
      (forall a b. (a -> b) -> [a] -> [b]
map ExtVar -> NodeId
extVarNode forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. Bimap a b -> [b]
Bimap.elems forall a b. (a -> b) -> a -> b
$ Node -> Bimap Var ExtVar
nodeImportedVars Node
n)
      forall a. Ord a => [a] -> [a] -> Bool
`isSublistOf` Node -> [NodeId]
nodeDependencies Node
n

    , NodeId -> Bool -> (NodeId, Bool)
prop NodeId
"All local variables are declared" forall a b. (a -> b) -> a -> b
$
      Node -> Set Var
nodeRhsVarsSet Node
n forall a. Ord a => Set a -> Set a -> Bool
`isSubsetOf` Node -> Set Var
nodeVarsSet Node
n

    , NodeId -> Bool -> (NodeId, Bool)
prop NodeId
"Never apply 'pre' to an imported var" forall a b. (a -> b) -> a -> b
$
      let preVars :: Set Var
preVars = forall a. Ord a => [a] -> Set a
Set.fromList
            [Var
v | (VarDescr Type t
_ (Pre t
_ Var
v)) <- forall k a. Map k a -> [a]
Map.elems forall a b. (a -> b) -> a -> b
$ Node -> Map Var VarDescr
nodeLocalVars Node
n]
      in Set Var
preVars forall a. Ord a => Set a -> Set a -> Bool
`isSubsetOf` Node -> Set Var
nodeLocalVarsSet Node
n
    ]

specNodesIds :: TransSys -> Set NodeId
specNodesIds :: TransSys -> Set NodeId
specNodesIds TransSys
s = forall a. Ord a => [a] -> Set a
Set.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map Node -> NodeId
nodeId forall a b. (a -> b) -> a -> b
$ TransSys -> [Node]
specNodes TransSys
s

-- | Given a modular transition system, produce a map from each node to its
-- dependencies.
specDependenciesGraph :: TransSys -> Map NodeId [NodeId]
specDependenciesGraph :: TransSys -> Map NodeId [NodeId]
specDependenciesGraph TransSys
s =
  forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (Node -> NodeId
nodeId Node
n, Node -> [NodeId]
nodeDependencies Node
n) | Node
n <- TransSys -> [Node]
specNodes TransSys
s ]

-- | Return the top node of a modular transition system.
specTopNode :: TransSys -> Node
specTopNode :: TransSys -> Node
specTopNode TransSys
spec = forall a. HasCallStack => Maybe a -> a
fromJust forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
List.find
  ((forall a. Eq a => a -> a -> Bool
== TransSys -> NodeId
specTopNodeId TransSys
spec) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Node -> NodeId
nodeId)
  (TransSys -> [Node]
specNodes TransSys
spec)

instance HasInvariants TransSys where

  invariants :: TransSys -> [(NodeId, Bool)]
invariants TransSys
s =
    [ NodeId -> Bool -> (NodeId, Bool)
prop NodeId
"All mentioned nodes are declared" forall a b. (a -> b) -> a -> b
$
      TransSys -> NodeId
specTopNodeId TransSys
s forall a. Ord a => a -> Set a -> Bool
`member` TransSys -> Set NodeId
specNodesIds TransSys
s
      Bool -> Bool -> Bool
&& forall a. Ord a => [a] -> Set a
Set.fromList [NodeId
nId | Node
n <- TransSys -> [Node]
specNodes TransSys
s, NodeId
nId <- Node -> [NodeId]
nodeDependencies Node
n]
         forall a. Ord a => Set a -> Set a -> Bool
`isSubsetOf` TransSys -> Set NodeId
specNodesIds TransSys
s

    , NodeId -> Bool -> (NodeId, Bool)
prop NodeId
"The imported vars are not broken" forall a b. (a -> b) -> a -> b
$
      forall a. Monoid a => [a] -> a
mconcat (forall a b. (a -> b) -> [a] -> [b]
map Node -> Set ExtVar
nodeImportedExtVarsSet forall a b. (a -> b) -> a -> b
$ TransSys -> [Node]
specNodes TransSys
s) forall a. Ord a => Set a -> Set a -> Bool
`isSubsetOf`
      forall a. Monoid a => [a] -> a
mconcat (forall a b. (a -> b) -> [a] -> [b]
map Node -> Set ExtVar
nodeExportedExtVarsSet forall a b. (a -> b) -> a -> b
$ TransSys -> [Node]
specNodes TransSys
s)

    , NodeId -> Bool -> (NodeId, Bool)
prop NodeId
"The nodes invariants hold" forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall a. HasInvariants a => a -> Bool
checkInvs (TransSys -> [Node]
specNodes TransSys
s)
    ]

-- | True if the graph is topologically sorted (i.e., if the dependencies of a
-- node appear in the list of 'specNodes' before the node that depends on
-- them).
isTopologicallySorted :: TransSys -> Bool
isTopologicallySorted :: TransSys -> Bool
isTopologicallySorted TransSys
spec =
  forall a. Maybe a -> Bool
isJust forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM forall {m :: * -> *}.
(Monad m, Alternative m) =>
Set NodeId -> Node -> m (Set NodeId)
inspect forall a. Set a
Set.empty (TransSys -> [Node]
specNodes TransSys
spec)
  where
    inspect :: Set NodeId -> Node -> m (Set NodeId)
inspect Set NodeId
acc Node
n = do
      forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> Set a
Set.fromList (Node -> [NodeId]
nodeDependencies Node
n) forall a. Ord a => Set a -> Set a -> Bool
`isSubsetOf` Set NodeId
acc
      forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => a -> Set a -> Set a
Set.insert (Node -> NodeId
nodeId Node
n) forall a b. (a -> b) -> a -> b
$ Set NodeId
acc

-- For debugging purposes
instance Show ExtVar where
  show :: ExtVar -> NodeId
show (ExtVar NodeId
n Var
v) = NodeId
"(" forall a. [a] -> [a] -> [a]
++ NodeId
n forall a. [a] -> [a] -> [a]
++ NodeId
" : " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> NodeId
show Var
v forall a. [a] -> [a] -> [a]
++ NodeId
")"