{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ViewPatterns #-}
module Copilot.Theorem.TransSys.Translate ( translate ) where
import Copilot.Theorem.TransSys.Spec
import Copilot.Theorem.TransSys.Cast
import Copilot.Theorem.Misc.Utils
import Control.Monad.State.Lazy
import Data.Char (isNumber)
import Data.Function (on)
import Data.Map (Map)
import Data.Bimap (Bimap)
import qualified Copilot.Core as C
import qualified Data.Map as Map
import qualified Data.Bimap as Bimap
ncSep :: NodeId
ncSep = NodeId
"."
ncMain :: NodeId
ncMain = NodeId
"out"
ncNode :: a -> NodeId
ncNode a
i = NodeId
"s" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> NodeId
show a
i
ncPropNode :: NodeId -> NodeId
ncPropNode NodeId
s = NodeId
"prop-" forall a. [a] -> [a] -> [a]
++ NodeId
s
ncTopNode :: NodeId
ncTopNode = NodeId
"top"
ncAnonInput :: NodeId
ncAnonInput = NodeId
"in"
ncLocal :: NodeId -> NodeId
ncLocal NodeId
s = NodeId
"l" forall a. [a] -> [a] -> [a]
++ forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Bool
isNumber) NodeId
s
ncExternVarNode :: NodeId -> NodeId
ncExternVarNode NodeId
name = NodeId
"ext-" forall a. [a] -> [a] -> [a]
++ NodeId
name
ncImported :: NodeId -> String -> String
ncImported :: NodeId -> NodeId -> NodeId
ncImported NodeId
n NodeId
s = NodeId
n forall a. [a] -> [a] -> [a]
++ NodeId
ncSep forall a. [a] -> [a] -> [a]
++ NodeId
s
ncTimeAnnot :: String -> Int -> String
ncTimeAnnot :: NodeId -> Int -> NodeId
ncTimeAnnot NodeId
s Int
d
| Int
d forall a. Eq a => a -> a -> Bool
== Int
0 = NodeId
s
| Bool
otherwise = NodeId
s forall a. [a] -> [a] -> [a]
++ NodeId
ncSep forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> NodeId
show Int
d
translate :: C.Spec -> TransSys
translate :: Spec -> TransSys
translate Spec
cspec =
TransSys { specNodes :: [Node]
specNodes = [Node
topNode] forall a. [a] -> [a] -> [a]
++ [Node]
modelNodes forall a. [a] -> [a] -> [a]
++ [Node]
propNodes forall a. [a] -> [a] -> [a]
++ [Node]
extVarNodes
, specTopNodeId :: NodeId
specTopNodeId = NodeId
topNodeId
, specProps :: Map NodeId ExtVar
specProps = Map NodeId ExtVar
propBindings }
where
topNodeId :: NodeId
topNodeId = NodeId
ncTopNode
cprops :: [C.Property]
cprops :: [Property]
cprops = Spec -> [Property]
C.specProperties Spec
cspec
propBindings :: Map PropId ExtVar
propBindings :: Map NodeId ExtVar
propBindings = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ do
NodeId
pid <- forall a b. (a -> b) -> [a] -> [b]
map Property -> NodeId
C.propertyName [Property]
cprops
forall (m :: * -> *) a. Monad m => a -> m a
return (NodeId
pid, NodeId -> NodeId -> ExtVar
mkExtVar NodeId
topNodeId NodeId
pid)
(([Node]
modelNodes, [Node]
propNodes), [(NodeId, U Type)]
extvarNodesNames) = forall a. Trans a -> (a, [(NodeId, U Type)])
runTrans forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (,) (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Stream -> Trans Node
stream (Spec -> [Stream]
C.specStreams Spec
cspec)) ([Property] -> Trans [Node]
mkPropNodes [Property]
cprops)
topNode :: Node
topNode = NodeId -> [NodeId] -> [Property] -> Node
mkTopNode NodeId
topNodeId (forall a b. (a -> b) -> [a] -> [b]
map Node -> NodeId
nodeId [Node]
propNodes) [Property]
cprops
extVarNodes :: [Node]
extVarNodes = forall a b. (a -> b) -> [a] -> [b]
map (NodeId, U Type) -> Node
mkExtVarNode [(NodeId, U Type)]
extvarNodesNames
mkTopNode :: String -> [NodeId] -> [C.Property] -> Node
mkTopNode :: NodeId -> [NodeId] -> [Property] -> Node
mkTopNode NodeId
topNodeId [NodeId]
dependencies [Property]
cprops =
Node { nodeId :: NodeId
nodeId = NodeId
topNodeId
, nodeDependencies :: [NodeId]
nodeDependencies = [NodeId]
dependencies
, nodeLocalVars :: Map Var VarDescr
nodeLocalVars = forall k a. Map k a
Map.empty
, nodeImportedVars :: Bimap Var ExtVar
nodeImportedVars = Bimap Var ExtVar
importedVars
, nodeConstrs :: [Expr Bool]
nodeConstrs = []}
where
importedVars :: Bimap Var ExtVar
importedVars = forall a b. (Ord a, Ord b) => [(a, b)] -> Bimap a b
Bimap.fromList
[ (NodeId -> Var
Var NodeId
cp, NodeId -> NodeId -> ExtVar
mkExtVar (NodeId -> NodeId
ncPropNode NodeId
cp) NodeId
ncMain)
| NodeId
cp <- Property -> NodeId
C.propertyName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Property]
cprops ]
mkExtVarNode :: (NodeId, U Type) -> Node
mkExtVarNode (NodeId
name, U Type t
t) =
Node { nodeId :: NodeId
nodeId = NodeId
name
, nodeDependencies :: [NodeId]
nodeDependencies = []
, nodeLocalVars :: Map Var VarDescr
nodeLocalVars = forall k a. k -> a -> Map k a
Map.singleton (NodeId -> Var
Var NodeId
ncMain) (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 [])
, nodeImportedVars :: Bimap Var ExtVar
nodeImportedVars = forall a b. Bimap a b
Bimap.empty
, nodeConstrs :: [Expr Bool]
nodeConstrs = []}
mkPropNodes :: [C.Property] -> Trans [Node]
mkPropNodes :: [Property] -> Trans [Node]
mkPropNodes = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Property -> Trans Node
propNode
where
propNode :: Property -> Trans Node
propNode Property
p = do
Node
s <- Stream -> Trans Node
stream (Property -> Stream
streamOfProp Property
p)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Node
s {nodeId :: NodeId
nodeId = NodeId -> NodeId
ncPropNode (Property -> NodeId
C.propertyName Property
p)}
streamOfProp :: C.Property -> C.Stream
streamOfProp :: Property -> Stream
streamOfProp Property
prop =
C.Stream { streamId :: Int
C.streamId = Int
42
, streamBuffer :: [Bool]
C.streamBuffer = []
, streamExpr :: Expr Bool
C.streamExpr = Property -> Expr Bool
C.propertyExpr Property
prop
, streamExprType :: Type Bool
C.streamExprType = Type Bool
C.Bool }
stream :: C.Stream -> Trans Node
stream :: Stream -> Trans Node
stream (C.Stream { Int
streamId :: Int
streamId :: Stream -> Int
C.streamId
, [a]
streamBuffer :: [a]
streamBuffer :: ()
C.streamBuffer
, Expr a
streamExpr :: Expr a
streamExpr :: ()
C.streamExpr
, Type a
streamExprType :: Type a
streamExprType :: ()
C.streamExprType })
= forall t a. Type t -> (forall t'. Type t' -> a) -> a
casting Type a
streamExprType forall a b. (a -> b) -> a -> b
$ \Type t'
t -> do
let nodeId :: NodeId
nodeId = forall a. Show a => a -> NodeId
ncNode Int
streamId
outvar :: Int -> Var
outvar Int
i = NodeId -> Var
Var (NodeId
ncMain NodeId -> Int -> NodeId
`ncTimeAnnot` Int
i)
buf :: [t']
buf = forall a b. (a -> b) -> [a] -> [b]
map (forall t. Type t -> Dyn -> t
cast Type t'
t forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Typeable a => a -> Dyn
toDyn) [a]
streamBuffer
(Expr t'
e, Map Var VarDescr
nodeAuxVars, Bimap Var ExtVar
nodeImportedVars, [NodeId]
nodeDependencies) <-
forall t a.
Type t
-> NodeId
-> Expr a
-> Trans (Expr t, Map Var VarDescr, Bimap Var ExtVar, [NodeId])
runExprTrans Type t'
t NodeId
nodeId Expr a
streamExpr
let outputLocals :: Map Var VarDescr
outputLocals =
let from :: Int -> [t'] -> Map Var VarDescr
from Int
i [] = forall k a. k -> a -> Map k a
Map.singleton (Int -> Var
outvar Int
i) (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 Expr t'
e)
from Int
i (t'
b : [t']
bs) =
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Int -> Var
outvar Int
i)
(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'
b forall a b. (a -> b) -> a -> b
$ Int -> Var
outvar (Int
i forall a. Num a => a -> a -> a
+ Int
1))
forall a b. (a -> b) -> a -> b
$ Int -> [t'] -> Map Var VarDescr
from (Int
i forall a. Num a => a -> a -> a
+ Int
1) [t']
bs
in Int -> [t'] -> Map Var VarDescr
from Int
0 [t']
buf
nodeLocalVars :: Map Var VarDescr
nodeLocalVars = forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map Var VarDescr
nodeAuxVars Map Var VarDescr
outputLocals
nodeOutputs :: [Var]
nodeOutputs = forall a b. (a -> b) -> [a] -> [b]
map Int -> Var
outvar [Int
0 .. forall (t :: * -> *) a. Foldable t => t a -> Int
length [t']
buf forall a. Num a => a -> a -> a
- Int
1]
forall (m :: * -> *) a. Monad m => a -> m a
return Node
{ NodeId
nodeId :: NodeId
nodeId :: NodeId
nodeId, [NodeId]
nodeDependencies :: [NodeId]
nodeDependencies :: [NodeId]
nodeDependencies, Map Var VarDescr
nodeLocalVars :: Map Var VarDescr
nodeLocalVars :: Map Var VarDescr
nodeLocalVars
, Bimap Var ExtVar
nodeImportedVars :: Bimap Var ExtVar
nodeImportedVars :: Bimap Var ExtVar
nodeImportedVars, nodeConstrs :: [Expr Bool]
nodeConstrs = [] }
expr :: Type t -> C.Expr t' -> Trans (Expr t)
expr :: forall t t'. Type t -> Expr t' -> Trans (Expr t)
expr Type t
t (C.Const Type t'
_ t'
v) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. Type t -> t -> Expr t
Const Type t
t (forall t. Type t -> Dyn -> t
cast Type t
t forall a b. (a -> b) -> a -> b
$ forall a. Typeable a => a -> Dyn
toDyn t'
v)
expr Type t
t (C.Drop Type t'
_ (forall a b. (Integral a, Num b) => a -> b
fromIntegral -> Int
k :: Int) Int
id) = do
let node :: NodeId
node = forall a. Show a => a -> NodeId
ncNode Int
id
Bool
selfRef <- (forall a. Eq a => a -> a -> Bool
== NodeId
node) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT TransSt Identity NodeId
curNode
let varName :: NodeId
varName = NodeId
ncMain NodeId -> Int -> NodeId
`ncTimeAnnot` Int
k
let var :: Var
var = NodeId -> Var
Var forall a b. (a -> b) -> a -> b
$ if Bool
selfRef then NodeId
varName else NodeId -> NodeId -> NodeId
ncImported NodeId
node NodeId
varName
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
selfRef forall a b. (a -> b) -> a -> b
$ do
forall {m :: * -> *}. MonadState TransSt m => NodeId -> m ()
newDep NodeId
node
forall {m :: * -> *}. MonadState TransSt m => Var -> ExtVar -> m ()
newImportedVar Var
var (NodeId -> NodeId -> ExtVar
mkExtVar NodeId
node NodeId
varName)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. Type t -> Var -> Expr t
VarE Type t
t Var
var
expr Type t
t (C.Label Type t'
_ NodeId
_ Expr t'
e) = forall t t'. Type t -> Expr t' -> Trans (Expr t)
expr Type t
t Expr t'
e
expr Type t
t (C.Local Type a1
tl Type t'
_tr NodeId
id Expr a1
l Expr t'
e) = forall t a. Type t -> (forall t'. Type t' -> a) -> a
casting Type a1
tl forall a b. (a -> b) -> a -> b
$ \Type t'
tl' -> do
Expr t'
l' <- forall t t'. Type t -> Expr t' -> Trans (Expr t)
expr Type t'
tl' Expr a1
l
forall {m :: * -> *}.
MonadState TransSt m =>
Var -> VarDescr -> m ()
newLocal (NodeId -> Var
Var forall a b. (a -> b) -> a -> b
$ NodeId -> NodeId
ncLocal NodeId
id) forall a b. (a -> b) -> a -> b
$ forall t. Type t -> VarDef t -> VarDescr
VarDescr Type t'
tl' forall a b. (a -> b) -> a -> b
$ forall t. Expr t -> VarDef t
Expr Expr t'
l'
forall t t'. Type t -> Expr t' -> Trans (Expr t)
expr Type t
t Expr t'
e
expr Type t
t (C.Var Type t'
_t' NodeId
id) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. Type t -> Var -> Expr t
VarE Type t
t (NodeId -> Var
Var forall a b. (a -> b) -> a -> b
$ NodeId -> NodeId
ncLocal NodeId
id)
expr Type t
t (C.Op3 (C.Mux Type b
_) Expr a1
cond Expr b
e1 Expr c
e2) = do
Expr Bool
cond' <- forall t t'. Type t -> Expr t' -> Trans (Expr t)
expr Type Bool
Bool Expr a1
cond
Expr t
e1' <- forall t t'. Type t -> Expr t' -> Trans (Expr t)
expr Type t
t Expr b
e1
Expr t
e2' <- forall t t'. Type t -> Expr t' -> Trans (Expr t)
expr Type t
t Expr c
e2
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. Type t -> Expr Bool -> Expr t -> Expr t -> Expr t
Ite Type t
t Expr Bool
cond' Expr t
e1' Expr t
e2'
expr Type t
t (C.ExternVar Type t'
_ NodeId
name Maybe [t']
_) = do
let nodeName :: NodeId
nodeName = NodeId -> NodeId
ncExternVarNode NodeId
name
let localAlias :: Var
localAlias = NodeId -> Var
Var NodeId
nodeName
forall {m :: * -> *}.
MonadState TransSt m =>
NodeId -> U Type -> m ()
newExtVarNode NodeId
nodeName (forall (f :: * -> *) t. f t -> U f
U Type t
t)
forall {m :: * -> *}. MonadState TransSt m => NodeId -> m ()
newDep NodeId
nodeName
forall {m :: * -> *}. MonadState TransSt m => Var -> ExtVar -> m ()
newImportedVar Var
localAlias (NodeId -> Var -> ExtVar
ExtVar NodeId
nodeName (NodeId -> Var
Var NodeId
ncMain))
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. Type t -> Var -> Expr t
VarE Type t
t Var
localAlias
expr Type t
t (C.Op1 Op1 a1 t'
op Expr a1
e) = forall (m :: * -> *) (expr :: * -> *) _a _b resT.
Functor m =>
Type resT
-> (Op1 _a _b, Expr _a)
-> (forall t t'. Type t -> Expr t' -> m (expr t))
-> (UnhandledOp1 -> m (expr resT))
-> (forall t. Type t -> Op1 t -> expr t -> expr t)
-> m (expr resT)
handleOp1
Type t
t (Op1 a1 t'
op, Expr a1
e) forall t t'. Type t -> Expr t' -> Trans (Expr t)
expr UnhandledOp1 -> StateT TransSt Identity (Expr t)
notHandled forall t. Type t -> Op1 t -> Expr t -> Expr t
Op1
where
notHandled :: UnhandledOp1 -> StateT TransSt Identity (Expr t)
notHandled (UnhandledOp1 NodeId
_opName Type a
_ta Type b
_tb) =
forall t. Type t -> Trans (Expr t)
newUnconstrainedVar Type t
t
expr Type t
t (C.Op2 Op2 a1 b t'
op Expr a1
e1 Expr b
e2) = forall (m :: * -> *) (expr :: * -> *) _a _b _c resT.
Monad m =>
Type resT
-> (Op2 _a _b _c, Expr _a, Expr _b)
-> (forall t t'. Type t -> Expr t' -> m (expr t))
-> (UnhandledOp2 -> m (expr resT))
-> (forall t a. Type t -> Op2 a t -> expr a -> expr a -> expr t)
-> (expr Bool -> expr Bool)
-> m (expr resT)
handleOp2
Type t
t (Op2 a1 b t'
op, Expr a1
e1, Expr b
e2) forall t t'. Type t -> Expr t' -> Trans (Expr t)
expr UnhandledOp2 -> StateT TransSt Identity (Expr t)
notHandled forall t a. Type t -> Op2 a t -> Expr a -> Expr a -> Expr t
Op2 (forall t. Type t -> Op1 t -> Expr t -> Expr t
Op1 Type Bool
Bool Op1 Bool
Not)
where
notHandled :: UnhandledOp2 -> StateT TransSt Identity (Expr t)
notHandled (UnhandledOp2 NodeId
_opName Type a
_ta Type b
_tb Type c
_tc) =
forall t. Type t -> Trans (Expr t)
newUnconstrainedVar Type t
t
newUnconstrainedVar :: Type t -> Trans (Expr t)
newUnconstrainedVar :: forall t. Type t -> Trans (Expr t)
newUnconstrainedVar Type t
t = do
NodeId
newNode <- StateT TransSt Identity NodeId
getFreshNodeName
forall {m :: * -> *}.
MonadState TransSt m =>
Var -> VarDescr -> m ()
newLocal (NodeId -> Var
Var NodeId
newNode) forall a b. (a -> b) -> a -> b
$ 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 {m :: * -> *}. MonadState TransSt m => NodeId -> m ()
newDep NodeId
newNode
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. Type t -> Var -> Expr t
VarE Type t
t (NodeId -> Var
Var NodeId
newNode)
runTrans :: Trans a -> (a, [(NodeId, U Type)])
runTrans :: forall a. Trans a -> (a, [(NodeId, U Type)])
runTrans Trans a
mx =
(a
x, forall a. (a -> a -> Ordering) -> [a] -> [a]
nubBy' (forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b. (a, b) -> a
fst) forall a b. (a -> b) -> a -> b
$ TransSt -> [(NodeId, U Type)]
_extVarsNodes TransSt
st)
where
(a
x, TransSt
st) = forall s a. State s a -> s -> (a, s)
runState Trans a
mx TransSt
initState
initState :: TransSt
initState = TransSt
{ _lvars :: Map Var VarDescr
_lvars = forall k a. Map k a
Map.empty
, _importedVars :: Bimap Var ExtVar
_importedVars = forall a b. Bimap a b
Bimap.empty
, _dependencies :: [NodeId]
_dependencies = []
, _extVarsNodes :: [(NodeId, U Type)]
_extVarsNodes = []
, _curNode :: NodeId
_curNode = NodeId
""
, _nextUid :: Int
_nextUid = Int
0 }
runExprTrans ::
Type t -> NodeId -> C.Expr a ->
Trans (Expr t, Map Var VarDescr, Bimap Var ExtVar, [NodeId])
runExprTrans :: forall t a.
Type t
-> NodeId
-> Expr a
-> Trans (Expr t, Map Var VarDescr, Bimap Var ExtVar, [NodeId])
runExprTrans Type t
t NodeId
curNode Expr a
e = do
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \TransSt
st -> TransSt
st { _curNode :: NodeId
_curNode = NodeId
curNode }
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \TransSt
st -> TransSt
st { _nextUid :: Int
_nextUid = Int
0 }
Expr t
e' <- forall t t'. Type t -> Expr t' -> Trans (Expr t)
expr Type t
t Expr a
e
(Map Var VarDescr
lvs, Bimap Var ExtVar
ivs, [NodeId]
dps) <- State TransSt (Map Var VarDescr, Bimap Var ExtVar, [NodeId])
popLocalInfos
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr t
e', Map Var VarDescr
lvs, Bimap Var ExtVar
ivs, [NodeId]
dps)
data TransSt = TransSt
{ TransSt -> Map Var VarDescr
_lvars :: Map Var VarDescr
, TransSt -> Bimap Var ExtVar
_importedVars :: Bimap Var ExtVar
, TransSt -> [NodeId]
_dependencies :: [NodeId]
, TransSt -> [(NodeId, U Type)]
_extVarsNodes :: [(NodeId, U Type)]
, TransSt -> NodeId
_curNode :: NodeId
, TransSt -> Int
_nextUid :: Int }
type Trans a = State TransSt a
newDep :: NodeId -> m ()
newDep NodeId
d = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \TransSt
s -> TransSt
s { _dependencies :: [NodeId]
_dependencies = NodeId
d forall a. a -> [a] -> [a]
: TransSt -> [NodeId]
_dependencies TransSt
s }
popLocalInfos :: State TransSt (Map Var VarDescr, Bimap Var ExtVar, [NodeId])
popLocalInfos :: State TransSt (Map Var VarDescr, Bimap Var ExtVar, [NodeId])
popLocalInfos = do
Map Var VarDescr
lvs <- TransSt -> Map Var VarDescr
_lvars forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *). MonadState s m => m s
get
Bimap Var ExtVar
ivs <- TransSt -> Bimap Var ExtVar
_importedVars forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *). MonadState s m => m s
get
[NodeId]
dps <- TransSt -> [NodeId]
_dependencies forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *). MonadState s m => m s
get
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \TransSt
st -> TransSt
st
{ _lvars :: Map Var VarDescr
_lvars = forall k a. Map k a
Map.empty
, _importedVars :: Bimap Var ExtVar
_importedVars = forall a b. Bimap a b
Bimap.empty
, _dependencies :: [NodeId]
_dependencies = [] }
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Var VarDescr
lvs, Bimap Var ExtVar
ivs, forall a. Ord a => [a] -> [a]
nub' [NodeId]
dps)
getUid :: Trans Int
getUid :: Trans Int
getUid = do
Int
uid <- TransSt -> Int
_nextUid forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *). MonadState s m => m s
get
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \TransSt
st -> TransSt
st { _nextUid :: Int
_nextUid = Int
uid forall a. Num a => a -> a -> a
+ Int
1 }
forall (m :: * -> *) a. Monad m => a -> m a
return Int
uid
getFreshNodeName :: Trans NodeId
getFreshNodeName :: StateT TransSt Identity NodeId
getFreshNodeName = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM ((NodeId
"_" forall a. [a] -> [a] -> [a]
++) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> NodeId
show) Trans Int
getUid
newImportedVar :: Var -> ExtVar -> m ()
newImportedVar Var
l ExtVar
g = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$
\TransSt
s -> TransSt
s { _importedVars :: Bimap Var ExtVar
_importedVars = forall a b. (Ord a, Ord b) => a -> b -> Bimap a b -> Bimap a b
Bimap.insert Var
l ExtVar
g (TransSt -> Bimap Var ExtVar
_importedVars TransSt
s) }
newLocal :: Var -> VarDescr -> m ()
newLocal Var
l VarDescr
d = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \TransSt
s -> TransSt
s { _lvars :: Map Var VarDescr
_lvars = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Var
l VarDescr
d forall a b. (a -> b) -> a -> b
$ TransSt -> Map Var VarDescr
_lvars TransSt
s }
curNode :: StateT TransSt Identity NodeId
curNode = TransSt -> NodeId
_curNode forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *). MonadState s m => m s
get
newExtVarNode :: NodeId -> U Type -> m ()
newExtVarNode NodeId
id U Type
t =
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \TransSt
st -> TransSt
st { _extVarsNodes :: [(NodeId, U Type)]
_extVarsNodes = (NodeId
id, U Type
t) forall a. a -> [a] -> [a]
: TransSt -> [(NodeId, U Type)]
_extVarsNodes TransSt
st }