--------------------------------------------------------------------------------

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

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

--------------------------------------------------------------------------------

type NodeId = String
type PropId = String

data TransSys = TransSys
  { TransSys -> [Node]
specNodes         :: [Node]
  , TransSys -> NodeId
specTopNodeId     :: NodeId
  , TransSys -> Map NodeId ExtVar
specProps         :: Map PropId ExtVar }


data Node = Node
  { Node -> NodeId
nodeId            :: NodeId
  , Node -> [NodeId]
nodeDependencies  :: [NodeId]
  , Node -> Map Var VarDescr
nodeLocalVars     :: Map Var VarDescr
  , Node -> Bimap Var ExtVar
nodeImportedVars  :: Bimap Var ExtVar
  , Node -> [Expr Bool]
nodeConstrs       :: [Expr Bool] }


data Var      =  Var {Var -> NodeId
varName :: String}
  deriving (Var -> Var -> Bool
(Var -> Var -> Bool) -> (Var -> Var -> Bool) -> Eq Var
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
(Int -> Var -> ShowS)
-> (Var -> NodeId) -> ([Var] -> ShowS) -> Show Var
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
Eq Var
-> (Var -> Var -> Ordering)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Var)
-> (Var -> Var -> Var)
-> Ord 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
$cp1Ord :: Eq Var
Ord)

data ExtVar   =  ExtVar {ExtVar -> NodeId
extVarNode :: NodeId, ExtVar -> Var
extVarLocalPart :: Var }
  deriving (ExtVar -> ExtVar -> Bool
(ExtVar -> ExtVar -> Bool)
-> (ExtVar -> ExtVar -> Bool) -> Eq ExtVar
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
Eq ExtVar
-> (ExtVar -> ExtVar -> Ordering)
-> (ExtVar -> ExtVar -> Bool)
-> (ExtVar -> ExtVar -> Bool)
-> (ExtVar -> ExtVar -> Bool)
-> (ExtVar -> ExtVar -> Bool)
-> (ExtVar -> ExtVar -> ExtVar)
-> (ExtVar -> ExtVar -> ExtVar)
-> Ord 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
$cp1Ord :: Eq ExtVar
Ord)

data VarDescr = forall t . VarDescr
  { ()
varType :: Type t
  , ()
varDef  :: VarDef t }

data VarDef t = Pre t Var | Expr (Expr t) | Constrs [Expr Bool]

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

--------------------------------------------------------------------------------

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 t. Expr t -> m) -> Expr a -> m
foldExpr forall t. Expr t -> m
f Expr a
expr = Expr a -> m
forall t. Expr t -> m
f Expr a
expr m -> m -> m
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 t. Expr t -> m) -> Expr Bool -> m
forall m a. Monoid m => (forall t. Expr t -> m) -> Expr a -> m
foldExpr forall t. Expr t -> m
f Expr Bool
c m -> m -> m
forall a. Semigroup a => a -> a -> a
<> (forall t. Expr t -> m) -> Expr a -> m
forall m a. Monoid m => (forall t. Expr t -> m) -> Expr a -> m
foldExpr forall t. Expr t -> m
f Expr a
e1 m -> m -> m
forall a. Semigroup a => a -> a -> a
<> (forall t. Expr t -> m) -> Expr a -> m
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 t. Expr t -> m) -> Expr a -> m
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 t. Expr t -> m) -> Expr a -> m
forall m a. Monoid m => (forall t. Expr t -> m) -> Expr a -> m
foldExpr forall t. Expr t -> m
f Expr a
e1 m -> m -> m
forall a. Semigroup a => a -> a -> a
<> (forall t. Expr t -> m) -> Expr a -> m
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
_                -> m
forall a. Monoid a => a
mempty

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

transformExpr :: (forall a . Expr a -> Expr a) -> Expr t -> Expr t
transformExpr :: (forall a. Expr a -> Expr a) -> Expr t -> Expr t
transformExpr forall a. Expr a -> Expr a
f = Expr t -> Expr t
forall a. Expr a -> Expr a
tre
  where
    tre :: forall t . Expr t -> Expr t
    tre :: Expr t -> Expr t
tre (Ite Type t
t Expr Bool
c Expr t
e1 Expr t
e2)   = Expr t -> Expr t
forall a. Expr a -> Expr a
f (Type t -> Expr Bool -> Expr t -> Expr t -> Expr t
forall t. Type t -> Expr Bool -> Expr t -> Expr t -> Expr t
Ite Type t
t (Expr Bool -> Expr Bool
forall a. Expr a -> Expr a
tre Expr Bool
c) (Expr t -> Expr t
forall a. Expr a -> Expr a
tre Expr t
e1) (Expr t -> Expr t
forall a. Expr a -> Expr a
tre Expr t
e2))
    tre (Op1 Type t
t Op1 t
op Expr t
e)      = Expr t -> Expr t
forall a. Expr a -> Expr a
f (Type t -> Op1 t -> Expr t -> Expr t
forall t. Type t -> Op1 t -> Expr t -> Expr t
Op1 Type t
t Op1 t
op (Expr t -> Expr t
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)  = Expr t -> Expr t
forall a. Expr a -> Expr a
f (Type t -> Op2 a t -> Expr a -> Expr a -> Expr t
forall t a. Type t -> Op2 a t -> Expr a -> Expr a -> Expr t
Op2 Type t
t Op2 a t
op (Expr a -> Expr a
forall a. Expr a -> Expr a
tre Expr a
e1) (Expr a -> Expr a
forall a. Expr a -> Expr a
tre Expr a
e2))
    tre Expr t
e                 = Expr t -> Expr t
forall a. Expr a -> Expr a
f Expr t
e

--------------------------------------------------------------------------------

nodeVarsSet :: Node -> Set Var
nodeVarsSet :: Node -> Set Var
nodeVarsSet = (Set Var -> Set Var -> Set Var)
-> (Node -> Set Var) -> (Node -> Set Var) -> Node -> Set Var
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Set Var -> Set Var -> Set Var
forall a. Ord a => Set a -> Set a -> Set a
Set.union
  Node -> Set Var
nodeLocalVarsSet
  (Map Var ExtVar -> Set Var
forall k a. Map k a -> Set k
Map.keysSet (Map Var ExtVar -> Set Var)
-> (Node -> Map Var ExtVar) -> Node -> Set Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bimap Var ExtVar -> Map Var ExtVar
forall a b. Bimap a b -> Map a b
Bimap.toMap  (Bimap Var ExtVar -> Map Var ExtVar)
-> (Node -> Bimap Var ExtVar) -> Node -> Map Var ExtVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Node -> Bimap Var ExtVar
nodeImportedVars)

nodeLocalVarsSet :: Node -> Set Var
nodeLocalVarsSet :: Node -> Set Var
nodeLocalVarsSet = Map Var VarDescr -> Set Var
forall k a. Map k a -> Set k
Map.keysSet (Map Var VarDescr -> Set Var)
-> (Node -> Map Var VarDescr) -> Node -> Set Var
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) = Var -> Set Var
forall a. a -> Set a
Set.singleton Var
v
      varOcc Expr t
_          = Set Var
forall a. Set a
Set.empty

      descrRhsVars :: VarDescr -> Set Var
descrRhsVars (VarDescr Type t
_ (Expr Expr t
e))      = (forall t. Expr t -> Set Var) -> Expr t -> Set Var
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))     = Var -> Set Var
forall a. a -> Set a
Set.singleton Var
v
      descrRhsVars (VarDescr Type t
_ (Constrs [Expr Bool]
cs))  =
        [Set Var] -> Set Var
forall a. Monoid a => [a] -> a
mconcat ((Expr Bool -> Set Var) -> [Expr Bool] -> [Set Var]
forall a b. (a -> b) -> [a] -> [b]
map ((forall t. Expr t -> Set Var) -> Expr Bool -> Set Var
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 (VarDescr -> Set Var -> Set Var)
-> Set Var -> Map Var VarDescr -> Set Var
forall a b k. (a -> b -> b) -> b -> Map k a -> b
Map.foldr (Set Var -> Set Var -> Set Var
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Set Var -> Set Var -> Set Var)
-> (VarDescr -> Set Var) -> VarDescr -> Set Var -> Set Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarDescr -> Set Var
descrRhsVars) Set Var
forall a. Set a
Set.empty (Node -> Map Var VarDescr
nodeLocalVars Node
n)

nodeImportedExtVarsSet :: Node -> Set ExtVar
nodeImportedExtVarsSet :: Node -> Set ExtVar
nodeImportedExtVarsSet = Map ExtVar Var -> Set ExtVar
forall k a. Map k a -> Set k
Map.keysSet (Map ExtVar Var -> Set ExtVar)
-> (Node -> Map ExtVar Var) -> Node -> Set ExtVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bimap Var ExtVar -> Map ExtVar Var
forall a b. Bimap a b -> Map b a
Bimap.toMapR (Bimap Var ExtVar -> Map ExtVar Var)
-> (Node -> Bimap Var ExtVar) -> Node -> Map ExtVar Var
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 = (Var -> ExtVar) -> Set Var -> Set ExtVar
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (NodeId -> Var -> ExtVar
ExtVar (NodeId -> Var -> ExtVar) -> NodeId -> Var -> 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" (Bool -> (NodeId, Bool)) -> Bool -> (NodeId, Bool)
forall a b. (a -> b) -> a -> b
$
      ((ExtVar -> NodeId) -> [ExtVar] -> [NodeId]
forall a b. (a -> b) -> [a] -> [b]
map ExtVar -> NodeId
extVarNode ([ExtVar] -> [NodeId])
-> (Bimap Var ExtVar -> [ExtVar]) -> Bimap Var ExtVar -> [NodeId]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bimap Var ExtVar -> [ExtVar]
forall a b. Bimap a b -> [b]
Bimap.elems (Bimap Var ExtVar -> [NodeId]) -> Bimap Var ExtVar -> [NodeId]
forall a b. (a -> b) -> a -> b
$ Node -> Bimap Var ExtVar
nodeImportedVars Node
n)
      [NodeId] -> [NodeId] -> Bool
forall a. Ord a => [a] -> [a] -> Bool
`isSublistOf` Node -> [NodeId]
nodeDependencies Node
n

    , NodeId -> Bool -> (NodeId, Bool)
prop NodeId
"All local variables are declared" (Bool -> (NodeId, Bool)) -> Bool -> (NodeId, Bool)
forall a b. (a -> b) -> a -> b
$
      Node -> Set Var
nodeRhsVarsSet Node
n Set Var -> Set Var -> Bool
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" (Bool -> (NodeId, Bool)) -> Bool -> (NodeId, Bool)
forall a b. (a -> b) -> a -> b
$
      let preVars :: Set Var
preVars = [Var] -> Set Var
forall a. Ord a => [a] -> Set a
Set.fromList
            [Var
v | (VarDescr Type t
_ (Pre t
_ Var
v)) <- Map Var VarDescr -> [VarDescr]
forall k a. Map k a -> [a]
Map.elems (Map Var VarDescr -> [VarDescr]) -> Map Var VarDescr -> [VarDescr]
forall a b. (a -> b) -> a -> b
$ Node -> Map Var VarDescr
nodeLocalVars Node
n]
      in Set Var
preVars Set Var -> Set Var -> Bool
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 = [NodeId] -> Set NodeId
forall a. Ord a => [a] -> Set a
Set.fromList ([NodeId] -> Set NodeId)
-> ([Node] -> [NodeId]) -> [Node] -> Set NodeId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Node -> NodeId) -> [Node] -> [NodeId]
forall a b. (a -> b) -> [a] -> [b]
map Node -> NodeId
nodeId ([Node] -> Set NodeId) -> [Node] -> Set NodeId
forall a b. (a -> b) -> a -> b
$ TransSys -> [Node]
specNodes TransSys
s

specDependenciesGraph :: TransSys -> Map NodeId [NodeId]
specDependenciesGraph :: TransSys -> Map NodeId [NodeId]
specDependenciesGraph TransSys
s =
  [(NodeId, [NodeId])] -> Map NodeId [NodeId]
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 ]

specTopNode :: TransSys -> Node
specTopNode :: TransSys -> Node
specTopNode TransSys
spec = Maybe Node -> Node
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Node -> Node) -> Maybe Node -> Node
forall a b. (a -> b) -> a -> b
$ (Node -> Bool) -> [Node] -> Maybe Node
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
List.find
  ((NodeId -> NodeId -> Bool
forall a. Eq a => a -> a -> Bool
== TransSys -> NodeId
specTopNodeId TransSys
spec) (NodeId -> Bool) -> (Node -> NodeId) -> Node -> Bool
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" (Bool -> (NodeId, Bool)) -> Bool -> (NodeId, Bool)
forall a b. (a -> b) -> a -> b
$
      TransSys -> NodeId
specTopNodeId TransSys
s NodeId -> Set NodeId -> Bool
forall a. Ord a => a -> Set a -> Bool
`member` TransSys -> Set NodeId
specNodesIds TransSys
s
      Bool -> Bool -> Bool
&& [NodeId] -> Set NodeId
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]
         Set NodeId -> Set NodeId -> Bool
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" (Bool -> (NodeId, Bool)) -> Bool -> (NodeId, Bool)
forall a b. (a -> b) -> a -> b
$
      [Set ExtVar] -> Set ExtVar
forall a. Monoid a => [a] -> a
mconcat ((Node -> Set ExtVar) -> [Node] -> [Set ExtVar]
forall a b. (a -> b) -> [a] -> [b]
map Node -> Set ExtVar
nodeImportedExtVarsSet ([Node] -> [Set ExtVar]) -> [Node] -> [Set ExtVar]
forall a b. (a -> b) -> a -> b
$ TransSys -> [Node]
specNodes TransSys
s) Set ExtVar -> Set ExtVar -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`isSubsetOf`
      [Set ExtVar] -> Set ExtVar
forall a. Monoid a => [a] -> a
mconcat ((Node -> Set ExtVar) -> [Node] -> [Set ExtVar]
forall a b. (a -> b) -> [a] -> [b]
map Node -> Set ExtVar
nodeExportedExtVarsSet ([Node] -> [Set ExtVar]) -> [Node] -> [Set ExtVar]
forall a b. (a -> b) -> a -> b
$ TransSys -> [Node]
specNodes TransSys
s)

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

isTopologicallySorted :: TransSys -> Bool
isTopologicallySorted :: TransSys -> Bool
isTopologicallySorted TransSys
spec =
  Maybe (Set NodeId) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Set NodeId) -> Bool) -> Maybe (Set NodeId) -> Bool
forall a b. (a -> b) -> a -> b
$ (Set NodeId -> Node -> Maybe (Set NodeId))
-> Set NodeId -> [Node] -> Maybe (Set NodeId)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Set NodeId -> Node -> Maybe (Set NodeId)
forall (m :: * -> *).
(Monad m, Alternative m) =>
Set NodeId -> Node -> m (Set NodeId)
inspect Set NodeId
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
          Bool -> m ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> m ()) -> Bool -> m ()
forall a b. (a -> b) -> a -> b
$ [NodeId] -> Set NodeId
forall a. Ord a => [a] -> Set a
Set.fromList (Node -> [NodeId]
nodeDependencies Node
n) Set NodeId -> Set NodeId -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`isSubsetOf` Set NodeId
acc
          Set NodeId -> m (Set NodeId)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set NodeId -> m (Set NodeId))
-> (Set NodeId -> Set NodeId) -> Set NodeId -> m (Set NodeId)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NodeId -> Set NodeId -> Set NodeId
forall a. Ord a => a -> Set a -> Set a
Set.insert (Node -> NodeId
nodeId Node
n) (Set NodeId -> m (Set NodeId)) -> Set NodeId -> m (Set NodeId)
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
"(" NodeId -> ShowS
forall a. [a] -> [a] -> [a]
++ NodeId
n NodeId -> ShowS
forall a. [a] -> [a] -> [a]
++ NodeId
" : " NodeId -> ShowS
forall a. [a] -> [a] -> [a]
++ Var -> NodeId
forall a. Show a => a -> NodeId
show Var
v NodeId -> ShowS
forall a. [a] -> [a] -> [a]
++ NodeId
")"

--------------------------------------------------------------------------------