{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE Safe       #-}

-- | Helper module to manipulate and simplify TransSys graphs.
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
"-"

-- | Merge all the given nodes, replacing all references to the given node Ids
-- with a reference to a fresh node id (unless the nodes given as argument
-- contain the top node), in which case its ID is chosen instead.
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

    -- Choosing the new node ID. If the top node is merged,
    -- its name is kept
    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 }

    -- Computing the dependencies of the new node
    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 ]

    -- All the work of renaming is done in the 'Misc.Renaming' monad. Some code
    -- complexity has been added so the variable names remains as clear as
    -- possible after merging two nodes.
    (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

    -- Converting the variables descriptors
    localVars :: Map Var VarDescr
localVars = [Node] -> (ExtVar -> Var) -> Map Var VarDescr
mergeVarsDescrs [Node]
toMerge ExtVar -> Var
renamingF

    -- Computing the global renaming function
    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)

-- | Discard all the structure of a /modular transition system/ and turn it
-- into a /non-modular transition system/ with only one node.
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

-- | Remove cycles by merging nodes participating in strongly connected
-- components.
--
-- The transition system obtained by the 'TransSys.Translate' module is
-- perfectly consistent. However, it can't be directly translated into the
-- /Kind2 native file format/. Indeed, it is natural to bind each node to a
-- predicate but the Kind2 file format requires that each predicate only uses
-- previously defined predicates. However, some nodes in our transition system
-- could be mutually recursive. Therefore, the goal of 'removeCycles' is to
-- remove such dependency cycles.
--
-- The function 'removeCycles' computes the strongly connected components of
-- the dependency graph and merge each one into a single node using
-- 'mergeNodes'. The complexity of this process is high in the worst case (the
-- square of the total size of the system times the size of the biggest node)
-- but good in practice as few nodes are to be merged in most practical cases.
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) }

-- | Completes each node of a specification with imported variables such that
-- each node contains a copy of all its dependencies.
--
-- The given specification should have its node sorted by topological order.
--
-- The top nodes should have all the other nodes as its dependencies.

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

    -- Takes a list of nodes 'ns', 'n' whose dependencies are in 'ns', and
    -- returns 'n2:ns' where 'n2' is 'n' completed
    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

                -- To get readable names, we don't prefix variables
                -- which come from merged nodes as they are already
                -- decorated
                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