{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE NamedFieldPuns      #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE Safe                #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ViewPatterns        #-}

-- | Translate Copilot specifications into a modular transition system.
--
-- Each stream is associated to a node. The most significant task of this
-- translation process is to /flatten/ the copilot specification so the value
-- of all streams at time @n@ only depends on the values of all the streams at
-- time @n - 1@. For example, for the following Fibonacci implementation in
-- Copilot:
--
-- @
-- fib = [1, 1] ++ (fib + drop 1 fib)
-- @
--
-- the translation, converts it into:
--
-- @
-- fib0 = [1] ++ fib1
-- fib1 = [1] ++ (fib1 + fib0)
-- @
--
-- and then into the node:
--
-- @
-- NODE 'fib' DEPENDS ON []
-- DEFINES
--     out : Int =
--         1 -> pre out.1
--     out.1 : Int =
--         1 -> pre out.2
--     out.2 : Int =
--         (out) + (out.1)
-- @
--
-- This flattening process is made easier by the fact that the @++@ Copilot
-- operator only occurs leftmost in a stream definition after the reification
-- process.
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

-- Naming conventions
-- These are important in order to avoid name conflicts

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 Copilot specifications into a modular transition system.
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)}

-- A dummy ID is given to this stream, which is not a problem
-- because this ID will never be used
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 }