{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE Safe #-}
module Copilot.Theorem.TransSys.Transform
( mergeNodes
, inline
, removeCycles
, complete
) where
import Copilot.Theorem.TransSys.Spec
import Copilot.Theorem.TransSys.Renaming
import Copilot.Theorem.Misc.Utils
import Control.Monad (foldM, forM_, forM, guard)
import Data.List (sort, (\\), intercalate, partition)
import Control.Exception.Base (assert)
import Data.Map (Map, (!))
import Data.Set (member)
import Data.Bimap (Bimap)
import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Data.Graph as Graph
import qualified Data.Bimap as Bimap
prefix :: String -> Var -> Var
prefix :: String -> Var -> Var
prefix String
s1 (Var String
s2) = String -> Var
Var forall a b. (a -> b) -> a -> b
$ String
s1 forall a. [a] -> [a] -> [a]
++ String
"." forall a. [a] -> [a] -> [a]
++ String
s2
ncNodeIdSep :: String
ncNodeIdSep = String
"-"
mergeNodes :: [NodeId] -> TransSys -> TransSys
mergeNodes :: [String] -> TransSys -> TransSys
mergeNodes [String]
toMergeIds TransSys
spec =
TransSys
spec
{ specNodes :: [Node]
specNodes = Node
newNode forall a. a -> [a] -> [a]
:
forall a b. (a -> b) -> [a] -> [b]
map (String -> [String] -> (ExtVar -> ExtVar) -> Node -> Node
updateOtherNode String
newNodeId [String]
toMergeIds ExtVar -> ExtVar
renamingExtF) [Node]
otherNodes
, specProps :: Map String ExtVar
specProps = forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ExtVar -> ExtVar
renamingExtF (TransSys -> Map String ExtVar
specProps TransSys
spec) }
where
nodes :: [Node]
nodes = TransSys -> [Node]
specNodes TransSys
spec
([Node]
toMerge, [Node]
otherNodes) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ((forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
toMergeIds) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Node -> String
nodeId) [Node]
nodes
newNodeId :: String
newNodeId
| TransSys -> String
specTopNodeId TransSys
spec forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
toMergeIds = TransSys -> String
specTopNodeId TransSys
spec
| Bool
otherwise = forall a. [a] -> [[a]] -> [a]
intercalate String
ncNodeIdSep (forall a. Ord a => [a] -> [a]
sort [String]
toMergeIds)
newNode :: Node
newNode = Node
{ nodeId :: String
nodeId = String
newNodeId
, nodeDependencies :: [String]
nodeDependencies = [String]
dependencies
, nodeImportedVars :: Bimap Var ExtVar
nodeImportedVars = Bimap Var ExtVar
importedVars
, nodeLocalVars :: Map Var VarDescr
nodeLocalVars = Map Var VarDescr
localVars
, nodeConstrs :: [Expr Bool]
nodeConstrs = [Expr Bool]
constrs }
dependencies :: [String]
dependencies = forall a. Ord a => [a] -> [a]
nub'
[ String
id |
Node
n <- [Node]
toMerge
, String
id <- Node -> [String]
nodeDependencies Node
n
, String
id forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [String]
toMergeIds ]
(Bimap Var ExtVar
importedVars, ExtVar -> Var
renamingF) = forall a. Renaming a -> (a, ExtVar -> Var)
runRenaming forall a b. (a -> b) -> a -> b
$ do
[Node] -> Renaming ()
renameLocalVars [Node]
toMerge
[Node] -> Renaming ()
redirectLocalImports [Node]
toMerge
[Node] -> [Node] -> [String] -> Renaming (Bimap Var ExtVar)
selectImportedVars [Node]
toMerge [Node]
otherNodes [String]
dependencies
localVars :: Map Var VarDescr
localVars = [Node] -> (ExtVar -> Var) -> Map Var VarDescr
mergeVarsDescrs [Node]
toMerge ExtVar -> Var
renamingF
renamingExtF :: ExtVar -> ExtVar
renamingExtF (gv :: ExtVar
gv@(ExtVar String
nId Var
_))
| String
nId forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
toMergeIds = String -> Var -> ExtVar
ExtVar String
newNodeId (ExtVar -> Var
renamingF ExtVar
gv)
| Bool
otherwise = ExtVar
gv
constrs :: [Expr Bool]
constrs = [Node] -> (ExtVar -> Var) -> [Expr Bool]
mergeConstrs [Node]
toMerge ExtVar -> Var
renamingF
updateOtherNode :: NodeId -> [NodeId] -> (ExtVar -> ExtVar) -> Node -> Node
updateOtherNode :: String -> [String] -> (ExtVar -> ExtVar) -> Node -> Node
updateOtherNode String
newNodeId [String]
mergedNodesIds ExtVar -> ExtVar
renamingF Node
n = Node
n
{ nodeDependencies :: [String]
nodeDependencies =
let ds :: [String]
ds = Node -> [String]
nodeDependencies Node
n
ds' :: [String]
ds' = [String]
ds forall a. Eq a => [a] -> [a] -> [a]
\\ [String]
mergedNodesIds
in if forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
ds' forall a. Ord a => a -> a -> Bool
< forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
ds then String
newNodeId forall a. a -> [a] -> [a]
: [String]
ds' else [String]
ds
, nodeImportedVars :: Bimap Var ExtVar
nodeImportedVars =
forall a b. (Ord a, Ord b) => [(a, b)] -> Bimap a b
Bimap.fromList [ (Var
lv, ExtVar -> ExtVar
renamingF ExtVar
gv)
| (Var
lv, ExtVar
gv) <- forall a b. Bimap a b -> [(a, b)]
Bimap.toList forall a b. (a -> b) -> a -> b
$ Node -> Bimap Var ExtVar
nodeImportedVars Node
n ]
}
updateExpr :: NodeId -> (ExtVar -> Var) -> Expr t -> Expr t
updateExpr :: forall t. String -> (ExtVar -> Var) -> Expr t -> Expr t
updateExpr String
nId ExtVar -> Var
renamingF = forall t. (forall a. Expr a -> Expr a) -> Expr t -> Expr t
transformExpr forall a. Expr a -> Expr a
aux
where
aux :: forall t. Expr t -> Expr t
aux :: forall a. Expr a -> Expr a
aux (VarE Type t
t Var
v) = forall t. Type t -> Var -> Expr t
VarE Type t
t (ExtVar -> Var
renamingF (String -> Var -> ExtVar
ExtVar String
nId Var
v))
aux Expr t
e = Expr t
e
mergeVarsDescrs :: [Node] -> (ExtVar -> Var) -> Map Var VarDescr
mergeVarsDescrs :: [Node] -> (ExtVar -> Var) -> Map Var VarDescr
mergeVarsDescrs [Node]
toMerge ExtVar -> Var
renamingF = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ do
Node
n <- [Node]
toMerge
let nId :: String
nId = Node -> String
nodeId Node
n
(Var
v, VarDescr Type t
t VarDef t
def) <- forall k a. Map k a -> [(k, a)]
Map.toList forall a b. (a -> b) -> a -> b
$ Node -> Map Var VarDescr
nodeLocalVars Node
n
let d' :: VarDescr
d' = case VarDef t
def of
Pre t
val Var
v' -> forall t. Type t -> VarDef t -> VarDescr
VarDescr Type t
t forall a b. (a -> b) -> a -> b
$
forall t. t -> Var -> VarDef t
Pre t
val forall a b. (a -> b) -> a -> b
$ ExtVar -> Var
renamingF (String -> Var -> ExtVar
ExtVar String
nId Var
v')
Expr Expr t
e -> forall t. Type t -> VarDef t -> VarDescr
VarDescr Type t
t forall a b. (a -> b) -> a -> b
$
forall t. Expr t -> VarDef t
Expr forall a b. (a -> b) -> a -> b
$ forall t. String -> (ExtVar -> Var) -> Expr t -> Expr t
updateExpr String
nId ExtVar -> Var
renamingF Expr t
e
Constrs [Expr Bool]
cs -> forall t. Type t -> VarDef t -> VarDescr
VarDescr Type t
t forall a b. (a -> b) -> a -> b
$
forall t. [Expr Bool] -> VarDef t
Constrs forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall t. String -> (ExtVar -> Var) -> Expr t -> Expr t
updateExpr String
nId ExtVar -> Var
renamingF) [Expr Bool]
cs
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtVar -> Var
renamingF forall a b. (a -> b) -> a -> b
$ String -> Var -> ExtVar
ExtVar String
nId Var
v, VarDescr
d')
mergeConstrs :: [Node] -> (ExtVar -> Var) -> [Expr Bool]
mergeConstrs :: [Node] -> (ExtVar -> Var) -> [Expr Bool]
mergeConstrs [Node]
toMerge ExtVar -> Var
renamingF =
[ forall t. String -> (ExtVar -> Var) -> Expr t -> Expr t
updateExpr (Node -> String
nodeId Node
n) ExtVar -> Var
renamingF Expr Bool
c | Node
n <- [Node]
toMerge, Expr Bool
c <- Node -> [Expr Bool]
nodeConstrs Node
n ]
renameLocalVars :: [Node] -> Renaming ()
renameLocalVars :: [Node] -> Renaming ()
renameLocalVars [Node]
toMerge =
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(String, Var)]
niVars forall a b. (a -> b) -> a -> b
$ \(String
n, Var
v) -> do
Var
v' <- [Var] -> Renaming Var
getFreshName [String
n String -> Var -> Var
`prefix` Var
v]
String -> Var -> Var -> Renaming ()
rename String
n Var
v Var
v'
where
niVars :: [(String, Var)]
niVars = [ (Node -> String
nodeId Node
n, Var
v)
| Node
n <- [Node]
toMerge, (Var
v, VarDescr
_) <- forall k a. Map k a -> [(k, a)]
Map.toList (Node -> Map Var VarDescr
nodeLocalVars Node
n) ]
selectImportedVars :: [Node] -> [Node] -> [NodeId]
-> Renaming (Bimap Var ExtVar)
selectImportedVars :: [Node] -> [Node] -> [String] -> Renaming (Bimap Var ExtVar)
selectImportedVars [Node]
toMerge [Node]
otherNodes [String]
dependencies =
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Bimap Var ExtVar -> (String, Var) -> Renaming (Bimap Var ExtVar)
checkImport forall a b. Bimap a b
Bimap.empty [(String, Var)]
depsVars
where
otherNodesMap :: Map String Node
otherNodesMap = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Node -> String
nodeId Node
n, Node
n) | Node
n <- [Node]
otherNodes]
depsVars :: [(String, Var)]
depsVars = [ (String
nId, Var
v)
| String
nId <- [String]
dependencies, let n :: Node
n = Map String Node
otherNodesMap forall k a. Ord k => Map k a -> k -> a
! String
nId
, Var
v <- forall k a. Map k a -> [k]
Map.keys (Node -> Map Var VarDescr
nodeLocalVars Node
n)]
checkImport :: Bimap Var ExtVar -> (String, Var) -> Renaming (Bimap Var ExtVar)
checkImport Bimap Var ExtVar
acc (String
nId, Var
v) = do
Var
v' <- [Var] -> Renaming Var
getFreshName [String
nId String -> Var -> Var
`prefix` Var
v]
[Bool]
bmap <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Node]
toMerge forall a b. (a -> b) -> a -> b
$ \Node
n' ->
case forall a b (m :: * -> *).
(Ord a, Ord b, MonadThrow m) =>
b -> Bimap a b -> m a
Bimap.lookupR (String -> Var -> ExtVar
ExtVar String
nId Var
v)
(Node -> Bimap Var ExtVar
nodeImportedVars Node
n') of
Just Var
lv -> String -> Var -> Var -> Renaming ()
rename (Node -> String
nodeId Node
n') Var
lv Var
v' forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Maybe Var
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
if Bool
True forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Bool]
bmap
then forall a b. (Ord a, Ord b) => a -> b -> Bimap a b -> Bimap a b
Bimap.insert Var
v' (String -> Var -> ExtVar
ExtVar String
nId Var
v) Bimap Var ExtVar
acc
else Bimap Var ExtVar
acc
redirectLocalImports :: [Node] -> Renaming ()
redirectLocalImports :: [Node] -> Renaming ()
redirectLocalImports [Node]
toMerge = do
ExtVar -> Var
renamingF <- Renaming (ExtVar -> Var)
getRenamingF
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(String, Var, String, Var)]
x forall a b. (a -> b) -> a -> b
$ \(String
n, Var
alias, String
n', Var
v) ->
String -> Var -> Var -> Renaming ()
rename String
n Var
alias (ExtVar -> Var
renamingF (String -> Var -> ExtVar
ExtVar String
n' Var
v))
where
mergedNodesSet :: Set String
mergedNodesSet = forall a. Ord a => [a] -> Set a
Set.fromList [Node -> String
nodeId Node
n | Node
n <- [Node]
toMerge]
x :: [(String, Var, String, Var)]
x = do
Node
n <- [Node]
toMerge
let nId :: String
nId = Node -> String
nodeId Node
n
(Var
alias, ExtVar String
n' Var
v) <- forall a b. Bimap a b -> [(a, b)]
Bimap.toList (Node -> Bimap Var ExtVar
nodeImportedVars Node
n)
forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ String
n' forall a. Ord a => a -> Set a -> Bool
`member` Set String
mergedNodesSet
forall (m :: * -> *) a. Monad m => a -> m a
return (String
nId, Var
alias, String
n', Var
v)
inline :: TransSys -> TransSys
inline :: TransSys -> TransSys
inline TransSys
spec = [String] -> TransSys -> TransSys
mergeNodes [Node -> String
nodeId Node
n | Node
n <- TransSys -> [Node]
specNodes TransSys
spec] TransSys
spec
removeCycles :: TransSys -> TransSys
removeCycles :: TransSys -> TransSys
removeCycles TransSys
spec =
TransSys -> TransSys
topoSort forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SCC String -> TransSys -> TransSys
mergeComp TransSys
spec (forall {node}. (Node -> node) -> [Node] -> [SCC node]
buildScc Node -> String
nodeId forall a b. (a -> b) -> a -> b
$ TransSys -> [Node]
specNodes TransSys
spec)
where
mergeComp :: SCC String -> TransSys -> TransSys
mergeComp (Graph.AcyclicSCC String
_) TransSys
s = TransSys
s
mergeComp (Graph.CyclicSCC [String]
ids) TransSys
s = [String] -> TransSys -> TransSys
mergeNodes [String]
ids TransSys
s
buildScc :: (Node -> node) -> [Node] -> [SCC node]
buildScc Node -> node
nrep [Node]
ns =
let depGraph :: [(node, String, [String])]
depGraph = forall a b. (a -> b) -> [a] -> [b]
map (\Node
n -> (Node -> node
nrep Node
n, Node -> String
nodeId Node
n, Node -> [String]
nodeDependencies Node
n)) [Node]
ns
in forall key node. Ord key => [(node, key, [key])] -> [SCC node]
Graph.stronglyConnComp [(node, String, [String])]
depGraph
topoSort :: TransSys -> TransSys
topoSort TransSys
s = TransSys
s { specNodes :: [Node]
specNodes =
forall a b. (a -> b) -> [a] -> [b]
map (\(Graph.AcyclicSCC Node
n) -> Node
n) forall a b. (a -> b) -> a -> b
$ forall {node}. (Node -> node) -> [Node] -> [SCC node]
buildScc forall a. a -> a
id (TransSys -> [Node]
specNodes TransSys
s) }
complete :: TransSys -> TransSys
complete :: TransSys -> TransSys
complete TransSys
spec =
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (TransSys -> Bool
isTopologicallySorted TransSys
spec) forall a b. (a -> b) -> a -> b
$ TransSys
spec { specNodes :: [Node]
specNodes = [Node]
specNodes' }
where
specNodes' :: [Node]
specNodes' =
forall a. [a] -> [a]
reverse
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl [Node] -> Node -> [Node]
completeNode []
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TransSys -> [Node]
specNodes
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TransSys -> TransSys
completeTopNodeDeps
forall a b. (a -> b) -> a -> b
$ TransSys
spec
completeTopNodeDeps :: TransSys -> TransSys
completeTopNodeDeps TransSys
spec = TransSys
spec { specNodes :: [Node]
specNodes = forall a b. (a -> b) -> [a] -> [b]
map Node -> Node
aux [Node]
nodes }
where
nodes :: [Node]
nodes = TransSys -> [Node]
specNodes TransSys
spec
aux :: Node -> Node
aux Node
n
| Node -> String
nodeId Node
n forall a. Eq a => a -> a -> Bool
== TransSys -> String
specTopNodeId TransSys
spec =
Node
n { nodeDependencies :: [String]
nodeDependencies = forall a b. (a -> b) -> [a] -> [b]
map Node -> String
nodeId [Node]
nodes forall a. Eq a => [a] -> [a] -> [a]
\\ [Node -> String
nodeId Node
n] }
| Bool
otherwise = Node
n
completeNode :: [Node] -> Node -> [Node]
completeNode :: [Node] -> Node -> [Node]
completeNode [Node]
ns Node
n = (Node
n { nodeDependencies :: [String]
nodeDependencies = [String]
dependencies'
, nodeImportedVars :: Bimap Var ExtVar
nodeImportedVars = Bimap Var ExtVar
importedVars' }) forall a. a -> [a] -> [a]
: [Node]
ns
where
nsMap :: Map String Node
nsMap = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Node -> String
nodeId Node
n, Node
n) | Node
n <- [Node]
ns]
dependencies' :: [String]
dependencies' =
let newDeps :: [String]
newDeps = do
String
dId <- Node -> [String]
nodeDependencies Node
n
let d :: Node
d = Map String Node
nsMap forall k a. Ord k => Map k a -> k -> a
! String
dId
Node -> [String]
nodeDependencies Node
d
in forall a. Ord a => [a] -> [a]
nub' forall a b. (a -> b) -> a -> b
$ Node -> [String]
nodeDependencies Node
n forall a. [a] -> [a] -> [a]
++ [String]
newDeps
importedVars' :: Bimap Var ExtVar
importedVars' = forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Renaming a -> (a, ExtVar -> Var)
runRenaming forall a b. (a -> b) -> a -> b
$ do
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ Node -> Set Var
nodeVarsSet Node
n) Var -> Renaming ()
addReservedName
let toImportVars :: [ExtVar]
toImportVars = forall a. Ord a => [a] -> [a]
nub' [ String -> Var -> ExtVar
ExtVar String
nId Var
v
| String
nId <- [String]
dependencies'
, let n' :: Node
n' = Map String Node
nsMap forall k a. Ord k => Map k a -> k -> a
! String
nId
, Var
v <- forall k a. Map k a -> [k]
Map.keys (Node -> Map Var VarDescr
nodeLocalVars Node
n') ]
tryImport :: Bimap Var ExtVar -> ExtVar -> Renaming (Bimap Var ExtVar)
tryImport Bimap Var ExtVar
acc ev :: ExtVar
ev@(ExtVar String
n' Var
v) = do
let preferedName :: Var
preferedName
| forall a. [a] -> a
head String
ncNodeIdSep forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
n' = Var
v
| Bool
otherwise = String
n' String -> Var -> Var
`prefix` Var
v
Var
alias <- [Var] -> Renaming Var
getFreshName [Var
preferedName, String
n' String -> Var -> Var
`prefix` Var
v]
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. (Ord a, Ord b) => a -> b -> Bimap a b -> Bimap a b
Bimap.tryInsert Var
alias ExtVar
ev Bimap Var ExtVar
acc
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Bimap Var ExtVar -> ExtVar -> Renaming (Bimap Var ExtVar)
tryImport (Node -> Bimap Var ExtVar
nodeImportedVars Node
n) [ExtVar]
toImportVars