{-# 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            (liftM, liftM2, unless)
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" NodeId -> NodeId -> NodeId
forall a. [a] -> [a] -> [a]
++ a -> NodeId
forall a. Show a => a -> NodeId
show a
i
ncPropNode :: NodeId -> NodeId
ncPropNode NodeId
s  = NodeId
"prop-" NodeId -> NodeId -> NodeId
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" NodeId -> NodeId -> NodeId
forall a. [a] -> [a] -> [a]
++ (Char -> Bool) -> NodeId -> NodeId
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Bool -> Bool
not (Bool -> Bool) -> (Char -> Bool) -> Char -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Bool
isNumber) NodeId
s

ncExternVarNode :: NodeId -> NodeId
ncExternVarNode NodeId
name = NodeId
"ext-" NodeId -> NodeId -> NodeId
forall a. [a] -> [a] -> [a]
++ NodeId
name

ncImported :: NodeId -> String -> String
ncImported :: NodeId -> NodeId -> NodeId
ncImported NodeId
n NodeId
s = NodeId
n NodeId -> NodeId -> NodeId
forall a. [a] -> [a] -> [a]
++ NodeId
ncSep NodeId -> NodeId -> NodeId
forall a. [a] -> [a] -> [a]
++ NodeId
s

ncTimeAnnot :: String -> Int -> String
ncTimeAnnot :: NodeId -> Int -> NodeId
ncTimeAnnot NodeId
s Int
d
  | Int
d Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0    = NodeId
s
  | Bool
otherwise = NodeId
s NodeId -> NodeId -> NodeId
forall a. [a] -> [a] -> [a]
++ NodeId
ncSep NodeId -> NodeId -> NodeId
forall a. [a] -> [a] -> [a]
++ Int -> NodeId
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] [Node] -> [Node] -> [Node]
forall a. [a] -> [a] -> [a]
++ [Node]
modelNodes [Node] -> [Node] -> [Node]
forall a. [a] -> [a] -> [a]
++ [Node]
propNodes [Node] -> [Node] -> [Node]
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 = [(NodeId, ExtVar)] -> Map NodeId ExtVar
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(NodeId, ExtVar)] -> Map NodeId ExtVar)
-> [(NodeId, ExtVar)] -> Map NodeId ExtVar
forall a b. (a -> b) -> a -> b
$ do
      NodeId
pid <- (Property -> NodeId) -> [Property] -> [NodeId]
forall a b. (a -> b) -> [a] -> [b]
map Property -> NodeId
C.propertyName [Property]
cprops
      (NodeId, ExtVar) -> [(NodeId, ExtVar)]
forall a. a -> [a]
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) = Trans ([Node], [Node]) -> (([Node], [Node]), [(NodeId, U Type)])
forall a. Trans a -> (a, [(NodeId, U Type)])
runTrans (Trans ([Node], [Node]) -> (([Node], [Node]), [(NodeId, U Type)]))
-> Trans ([Node], [Node]) -> (([Node], [Node]), [(NodeId, U Type)])
forall a b. (a -> b) -> a -> b
$
      ([Node] -> [Node] -> ([Node], [Node]))
-> StateT TransSt Identity [Node]
-> StateT TransSt Identity [Node]
-> Trans ([Node], [Node])
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (,) ((Stream -> StateT TransSt Identity Node)
-> [Stream] -> StateT TransSt Identity [Node]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Stream -> StateT TransSt Identity Node
stream (Spec -> [Stream]
C.specStreams Spec
cspec)) ([Property] -> StateT TransSt Identity [Node]
mkPropNodes [Property]
cprops)

    topNode :: Node
topNode = NodeId -> [NodeId] -> [Property] -> Node
mkTopNode NodeId
topNodeId ((Node -> NodeId) -> [Node] -> [NodeId]
forall a b. (a -> b) -> [a] -> [b]
map Node -> NodeId
nodeId [Node]
propNodes) [Property]
cprops
    extVarNodes :: [Node]
extVarNodes = ((NodeId, U Type) -> Node) -> [(NodeId, U Type)] -> [Node]
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 = Map Var VarDescr
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 = [(Var, ExtVar)] -> Bimap Var ExtVar
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 (Property -> NodeId) -> [Property] -> [NodeId]
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 = Var -> VarDescr -> Map Var VarDescr
forall k a. k -> a -> Map k a
Map.singleton (NodeId -> Var
Var NodeId
ncMain) (Type t -> VarDef t -> VarDescr
forall t. Type t -> VarDef t -> VarDescr
VarDescr Type t
t (VarDef t -> VarDescr) -> VarDef t -> VarDescr
forall a b. (a -> b) -> a -> b
$ [Expr Bool] -> VarDef t
forall t. [Expr Bool] -> VarDef t
Constrs [])
       , nodeImportedVars :: Bimap Var ExtVar
nodeImportedVars = Bimap Var ExtVar
forall a b. Bimap a b
Bimap.empty
       , nodeConstrs :: [Expr Bool]
nodeConstrs = []}

mkPropNodes :: [C.Property] -> Trans [Node]
mkPropNodes :: [Property] -> StateT TransSt Identity [Node]
mkPropNodes = (Property -> StateT TransSt Identity Node)
-> [Property] -> StateT TransSt Identity [Node]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Property -> StateT TransSt Identity Node
propNode
  where
    propNode :: Property -> StateT TransSt Identity Node
propNode Property
p = do
      Node
s <- Stream -> StateT TransSt Identity Node
stream (Property -> Stream
streamOfProp Property
p)
      Node -> StateT TransSt Identity Node
forall a. a -> StateT TransSt Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Node -> StateT TransSt Identity Node)
-> Node -> StateT TransSt Identity Node
forall a b. (a -> b) -> a -> b
$ Node
s {nodeId = ncPropNode (C.propertyName 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 = Prop -> Expr Bool
C.extractProp (Property -> Prop
C.propertyProp Property
prop)
           , streamExprType :: Type Bool
C.streamExprType = Type Bool
C.Bool }

stream :: C.Stream -> Trans Node
stream :: Stream -> StateT TransSt Identity Node
stream (C.Stream { Int
streamId :: Stream -> Int
streamId :: Int
C.streamId
                 , [a]
streamBuffer :: ()
streamBuffer :: [a]
C.streamBuffer
                 , Expr a
streamExpr :: ()
streamExpr :: Expr a
C.streamExpr
                 , Type a
streamExprType :: ()
streamExprType :: Type a
C.streamExprType })

  = Type a
-> (forall {t'}. Type t' -> StateT TransSt Identity Node)
-> StateT TransSt Identity Node
forall t a. Type t -> (forall t'. Type t' -> a) -> a
casting Type a
streamExprType ((forall {t'}. Type t' -> StateT TransSt Identity Node)
 -> StateT TransSt Identity Node)
-> (forall {t'}. Type t' -> StateT TransSt Identity Node)
-> StateT TransSt Identity Node
forall a b. (a -> b) -> a -> b
$ \Type t'
t -> do

    let nodeId :: NodeId
nodeId = Int -> 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 = (a -> t') -> [a] -> [t']
forall a b. (a -> b) -> [a] -> [b]
map (Type t' -> Dyn -> t'
forall t. Type t -> Dyn -> t
cast Type t'
t (Dyn -> t') -> (a -> Dyn) -> a -> t'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Dyn
forall a. Typeable a => a -> Dyn
toDyn) [a]
streamBuffer

    (Expr t'
e, Map Var VarDescr
nodeAuxVars, Bimap Var ExtVar
nodeImportedVars, [NodeId]
nodeDependencies) <-
      Type t'
-> NodeId
-> Expr a
-> Trans (Expr t', Map Var VarDescr, Bimap Var ExtVar, [NodeId])
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 [] = Var -> VarDescr -> Map Var VarDescr
forall k a. k -> a -> Map k a
Map.singleton (Int -> Var
outvar Int
i) (Type t' -> VarDef t' -> VarDescr
forall t. Type t -> VarDef t -> VarDescr
VarDescr Type t'
t (VarDef t' -> VarDescr) -> VarDef t' -> VarDescr
forall a b. (a -> b) -> a -> b
$ Expr t' -> VarDef t'
forall t. Expr t -> VarDef t
Expr Expr t'
e)
              from Int
i (t'
b : [t']
bs) =
                 Var -> VarDescr -> Map Var VarDescr -> Map Var VarDescr
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Int -> Var
outvar Int
i)
                 (Type t' -> VarDef t' -> VarDescr
forall t. Type t -> VarDef t -> VarDescr
VarDescr Type t'
t (VarDef t' -> VarDescr) -> VarDef t' -> VarDescr
forall a b. (a -> b) -> a -> b
$ t' -> Var -> VarDef t'
forall t. t -> Var -> VarDef t
Pre t'
b (Var -> VarDef t') -> Var -> VarDef t'
forall a b. (a -> b) -> a -> b
$ Int -> Var
outvar (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1))
                 (Map Var VarDescr -> Map Var VarDescr)
-> Map Var VarDescr -> Map Var VarDescr
forall a b. (a -> b) -> a -> b
$ Int -> [t'] -> Map Var VarDescr
from (Int
i Int -> Int -> Int
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 = Map Var VarDescr -> Map Var VarDescr -> Map Var VarDescr
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 = (Int -> Var) -> [Int] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Var
outvar [Int
0 .. [t'] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [t']
buf Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]

    Node -> StateT TransSt Identity Node
forall a. a -> StateT TransSt Identity a
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) = Expr t -> StateT TransSt Identity (Expr t)
forall a. a -> StateT TransSt Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr t -> StateT TransSt Identity (Expr t))
-> Expr t -> StateT TransSt Identity (Expr t)
forall a b. (a -> b) -> a -> b
$ Type t -> t -> Expr t
forall t. Type t -> t -> Expr t
Const Type t
t (Type t -> Dyn -> t
forall t. Type t -> Dyn -> t
cast Type t
t (Dyn -> t) -> Dyn -> t
forall a b. (a -> b) -> a -> b
$ t' -> Dyn
forall a. Typeable a => a -> Dyn
toDyn t'
v)

expr Type t
t (C.Drop Type t'
_ (DropIdx -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral -> Int
k :: Int) Int
id) = do
  let node :: NodeId
node = Int -> NodeId
forall a. Show a => a -> NodeId
ncNode Int
id
  Bool
selfRef <- (NodeId -> NodeId -> Bool
forall a. Eq a => a -> a -> Bool
== NodeId
node) (NodeId -> Bool)
-> StateT TransSt Identity NodeId -> StateT TransSt Identity Bool
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 (NodeId -> Var) -> NodeId -> Var
forall a b. (a -> b) -> a -> b
$ if Bool
selfRef then NodeId
varName else NodeId -> NodeId -> NodeId
ncImported NodeId
node NodeId
varName
  Bool -> StateT TransSt Identity () -> StateT TransSt Identity ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
selfRef (StateT TransSt Identity () -> StateT TransSt Identity ())
-> StateT TransSt Identity () -> StateT TransSt Identity ()
forall a b. (a -> b) -> a -> b
$ do
    NodeId -> StateT TransSt Identity ()
forall {m :: * -> *}. MonadState TransSt m => NodeId -> m ()
newDep NodeId
node
    Var -> ExtVar -> StateT TransSt Identity ()
forall {m :: * -> *}. MonadState TransSt m => Var -> ExtVar -> m ()
newImportedVar Var
var (NodeId -> NodeId -> ExtVar
mkExtVar NodeId
node NodeId
varName)
  Expr t -> StateT TransSt Identity (Expr t)
forall a. a -> StateT TransSt Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr t -> StateT TransSt Identity (Expr t))
-> Expr t -> StateT TransSt Identity (Expr t)
forall a b. (a -> b) -> a -> b
$ Type t -> Var -> Expr t
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) = Type t -> Expr t' -> StateT TransSt Identity (Expr t)
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) = Type a1
-> (forall {t'}. Type t' -> StateT TransSt Identity (Expr t))
-> StateT TransSt Identity (Expr t)
forall t a. Type t -> (forall t'. Type t' -> a) -> a
casting Type a1
tl ((forall {t'}. Type t' -> StateT TransSt Identity (Expr t))
 -> StateT TransSt Identity (Expr t))
-> (forall {t'}. Type t' -> StateT TransSt Identity (Expr t))
-> StateT TransSt Identity (Expr t)
forall a b. (a -> b) -> a -> b
$ \Type t'
tl' -> do
  Expr t'
l' <- Type t' -> Expr a1 -> Trans (Expr t')
forall t t'. Type t -> Expr t' -> Trans (Expr t)
expr Type t'
tl' Expr a1
l
  Var -> VarDescr -> StateT TransSt Identity ()
forall {m :: * -> *}.
MonadState TransSt m =>
Var -> VarDescr -> m ()
newLocal (NodeId -> Var
Var (NodeId -> Var) -> NodeId -> Var
forall a b. (a -> b) -> a -> b
$ NodeId -> NodeId
ncLocal NodeId
id) (VarDescr -> StateT TransSt Identity ())
-> VarDescr -> StateT TransSt Identity ()
forall a b. (a -> b) -> a -> b
$ Type t' -> VarDef t' -> VarDescr
forall t. Type t -> VarDef t -> VarDescr
VarDescr Type t'
tl' (VarDef t' -> VarDescr) -> VarDef t' -> VarDescr
forall a b. (a -> b) -> a -> b
$ Expr t' -> VarDef t'
forall t. Expr t -> VarDef t
Expr Expr t'
l'
  Type t -> Expr t' -> StateT TransSt Identity (Expr t)
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) = Expr t -> StateT TransSt Identity (Expr t)
forall a. a -> StateT TransSt Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr t -> StateT TransSt Identity (Expr t))
-> Expr t -> StateT TransSt Identity (Expr t)
forall a b. (a -> b) -> a -> b
$ Type t -> Var -> Expr t
forall t. Type t -> Var -> Expr t
VarE Type t
t (NodeId -> Var
Var (NodeId -> Var) -> NodeId -> 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' <- Type Bool -> Expr a1 -> Trans (Expr Bool)
forall t t'. Type t -> Expr t' -> Trans (Expr t)
expr Type Bool
Bool Expr a1
cond
  Expr t
e1'   <- Type t -> Expr b -> StateT TransSt Identity (Expr t)
forall t t'. Type t -> Expr t' -> Trans (Expr t)
expr Type t
t    Expr b
e1
  Expr t
e2'   <- Type t -> Expr c -> StateT TransSt Identity (Expr t)
forall t t'. Type t -> Expr t' -> Trans (Expr t)
expr Type t
t    Expr c
e2
  Expr t -> StateT TransSt Identity (Expr t)
forall a. a -> StateT TransSt Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr t -> StateT TransSt Identity (Expr t))
-> Expr t -> StateT TransSt Identity (Expr t)
forall a b. (a -> b) -> a -> b
$ 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
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
  NodeId -> U Type -> StateT TransSt Identity ()
forall {m :: * -> *}.
MonadState TransSt m =>
NodeId -> U Type -> m ()
newExtVarNode NodeId
nodeName (Type t -> U Type
forall (f :: * -> *) t. f t -> U f
U Type t
t)
  NodeId -> StateT TransSt Identity ()
forall {m :: * -> *}. MonadState TransSt m => NodeId -> m ()
newDep NodeId
nodeName
  Var -> ExtVar -> StateT TransSt Identity ()
forall {m :: * -> *}. MonadState TransSt m => Var -> ExtVar -> m ()
newImportedVar Var
localAlias (NodeId -> Var -> ExtVar
ExtVar NodeId
nodeName (NodeId -> Var
Var NodeId
ncMain))
  Expr t -> StateT TransSt Identity (Expr t)
forall a. a -> StateT TransSt Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr t -> StateT TransSt Identity (Expr t))
-> Expr t -> StateT TransSt Identity (Expr t)
forall a b. (a -> b) -> a -> b
$ Type t -> Var -> Expr t
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) = Type t
-> (Op1 a1 t', Expr a1)
-> (forall t t'. Type t -> Expr t' -> Trans (Expr t))
-> (UnhandledOp1 -> StateT TransSt Identity (Expr t))
-> (forall t. Type t -> Op1 t -> Expr t -> Expr t)
-> StateT TransSt Identity (Expr t)
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) Type t -> Expr t' -> Trans (Expr t)
forall t t'. Type t -> Expr t' -> Trans (Expr t)
expr UnhandledOp1 -> StateT TransSt Identity (Expr t)
notHandled Type t -> Op1 t -> Expr t -> Expr t
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) =
      Type t -> StateT TransSt Identity (Expr t)
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) = Type t
-> (Op2 a1 b t', Expr a1, Expr b)
-> (forall t t'. Type t -> Expr t' -> Trans (Expr t))
-> (UnhandledOp2 -> StateT TransSt Identity (Expr t))
-> (forall t a. Type t -> Op2 a t -> Expr a -> Expr a -> Expr t)
-> (Expr Bool -> Expr Bool)
-> StateT TransSt Identity (Expr t)
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) Type t -> Expr t' -> Trans (Expr t)
forall t t'. Type t -> Expr t' -> Trans (Expr t)
expr UnhandledOp2 -> StateT TransSt Identity (Expr t)
notHandled 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 Bool -> Op1 Bool -> Expr Bool -> Expr Bool
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) =
      Type t -> StateT TransSt Identity (Expr t)
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
  Var -> VarDescr -> StateT TransSt Identity ()
forall {m :: * -> *}.
MonadState TransSt m =>
Var -> VarDescr -> m ()
newLocal (NodeId -> Var
Var NodeId
newNode) (VarDescr -> StateT TransSt Identity ())
-> VarDescr -> StateT TransSt Identity ()
forall a b. (a -> b) -> a -> b
$ Type t -> VarDef t -> VarDescr
forall t. Type t -> VarDef t -> VarDescr
VarDescr Type t
t (VarDef t -> VarDescr) -> VarDef t -> VarDescr
forall a b. (a -> b) -> a -> b
$ [Expr Bool] -> VarDef t
forall t. [Expr Bool] -> VarDef t
Constrs []
  NodeId -> StateT TransSt Identity ()
forall {m :: * -> *}. MonadState TransSt m => NodeId -> m ()
newDep NodeId
newNode
  Expr t -> Trans (Expr t)
forall a. a -> StateT TransSt Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr t -> Trans (Expr t)) -> Expr t -> Trans (Expr t)
forall a b. (a -> b) -> a -> b
$ Type t -> Var -> Expr t
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, ((NodeId, U Type) -> (NodeId, U Type) -> Ordering)
-> [(NodeId, U Type)] -> [(NodeId, U Type)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
nubBy' (NodeId -> NodeId -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (NodeId -> NodeId -> Ordering)
-> ((NodeId, U Type) -> NodeId)
-> (NodeId, U Type)
-> (NodeId, U Type)
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (NodeId, U Type) -> NodeId
forall a b. (a, b) -> a
fst) ([(NodeId, U Type)] -> [(NodeId, U Type)])
-> [(NodeId, U Type)] -> [(NodeId, U Type)]
forall a b. (a -> b) -> a -> b
$ TransSt -> [(NodeId, U Type)]
_extVarsNodes TransSt
st)
  where
    (a
x, TransSt
st) = Trans a -> TransSt -> (a, TransSt)
forall s a. State s a -> s -> (a, s)
runState Trans a
mx TransSt
initState
    initState :: TransSt
initState = TransSt
      { _lvars :: Map Var VarDescr
_lvars        = Map Var VarDescr
forall k a. Map k a
Map.empty
      , _importedVars :: Bimap Var ExtVar
_importedVars = Bimap Var ExtVar
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
  (TransSt -> TransSt) -> StateT TransSt Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((TransSt -> TransSt) -> StateT TransSt Identity ())
-> (TransSt -> TransSt) -> StateT TransSt Identity ()
forall a b. (a -> b) -> a -> b
$ \TransSt
st -> TransSt
st { _curNode = curNode }
  (TransSt -> TransSt) -> StateT TransSt Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((TransSt -> TransSt) -> StateT TransSt Identity ())
-> (TransSt -> TransSt) -> StateT TransSt Identity ()
forall a b. (a -> b) -> a -> b
$ \TransSt
st -> TransSt
st { _nextUid = 0 }
  Expr t
e' <- Type t -> Expr a -> Trans (Expr t)
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
  (Expr t, Map Var VarDescr, Bimap Var ExtVar, [NodeId])
-> Trans (Expr t, Map Var VarDescr, Bimap Var ExtVar, [NodeId])
forall a. a -> StateT TransSt Identity a
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 =  (TransSt -> TransSt) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((TransSt -> TransSt) -> m ()) -> (TransSt -> TransSt) -> m ()
forall a b. (a -> b) -> a -> b
$ \TransSt
s -> TransSt
s { _dependencies = d : _dependencies 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 (TransSt -> Map Var VarDescr)
-> StateT TransSt Identity TransSt
-> StateT TransSt Identity (Map Var VarDescr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT TransSt Identity TransSt
forall s (m :: * -> *). MonadState s m => m s
get
  Bimap Var ExtVar
ivs <- TransSt -> Bimap Var ExtVar
_importedVars (TransSt -> Bimap Var ExtVar)
-> StateT TransSt Identity TransSt
-> StateT TransSt Identity (Bimap Var ExtVar)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT TransSt Identity TransSt
forall s (m :: * -> *). MonadState s m => m s
get
  [NodeId]
dps <- TransSt -> [NodeId]
_dependencies (TransSt -> [NodeId])
-> StateT TransSt Identity TransSt
-> StateT TransSt Identity [NodeId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT TransSt Identity TransSt
forall s (m :: * -> *). MonadState s m => m s
get
  (TransSt -> TransSt) -> StateT TransSt Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((TransSt -> TransSt) -> StateT TransSt Identity ())
-> (TransSt -> TransSt) -> StateT TransSt Identity ()
forall a b. (a -> b) -> a -> b
$ \TransSt
st -> TransSt
st
    { _lvars = Map.empty
    , _importedVars = Bimap.empty
    , _dependencies = [] }
  (Map Var VarDescr, Bimap Var ExtVar, [NodeId])
-> State TransSt (Map Var VarDescr, Bimap Var ExtVar, [NodeId])
forall a. a -> StateT TransSt Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Var VarDescr
lvs, Bimap Var ExtVar
ivs, [NodeId] -> [NodeId]
forall a. Ord a => [a] -> [a]
nub' [NodeId]
dps)

getUid :: Trans Int
getUid :: Trans Int
getUid = do
  Int
uid <- TransSt -> Int
_nextUid (TransSt -> Int) -> StateT TransSt Identity TransSt -> Trans Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT TransSt Identity TransSt
forall s (m :: * -> *). MonadState s m => m s
get
  (TransSt -> TransSt) -> StateT TransSt Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((TransSt -> TransSt) -> StateT TransSt Identity ())
-> (TransSt -> TransSt) -> StateT TransSt Identity ()
forall a b. (a -> b) -> a -> b
$ \TransSt
st -> TransSt
st { _nextUid = uid + 1 }
  Int -> Trans Int
forall a. a -> StateT TransSt Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
uid

getFreshNodeName :: Trans NodeId
getFreshNodeName :: StateT TransSt Identity NodeId
getFreshNodeName = (Int -> NodeId) -> Trans Int -> StateT TransSt Identity NodeId
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM ((NodeId
"_" NodeId -> NodeId -> NodeId
forall a. [a] -> [a] -> [a]
++) (NodeId -> NodeId) -> (Int -> NodeId) -> Int -> NodeId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> NodeId
forall a. Show a => a -> NodeId
show) Trans Int
getUid

newImportedVar :: Var -> ExtVar -> m ()
newImportedVar Var
l ExtVar
g = (TransSt -> TransSt) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((TransSt -> TransSt) -> m ()) -> (TransSt -> TransSt) -> m ()
forall a b. (a -> b) -> a -> b
$
  \TransSt
s -> TransSt
s { _importedVars = Bimap.insert l g (_importedVars s) }

newLocal :: Var -> VarDescr -> m ()
newLocal Var
l VarDescr
d  =  (TransSt -> TransSt) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((TransSt -> TransSt) -> m ()) -> (TransSt -> TransSt) -> m ()
forall a b. (a -> b) -> a -> b
$ \TransSt
s -> TransSt
s { _lvars = Map.insert l d $ _lvars s }

curNode :: StateT TransSt Identity NodeId
curNode = TransSt -> NodeId
_curNode (TransSt -> NodeId)
-> StateT TransSt Identity TransSt
-> StateT TransSt Identity NodeId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT TransSt Identity TransSt
forall s (m :: * -> *). MonadState s m => m s
get

newExtVarNode :: NodeId -> U Type -> m ()
newExtVarNode NodeId
id U Type
t =
  (TransSt -> TransSt) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((TransSt -> TransSt) -> m ()) -> (TransSt -> TransSt) -> m ()
forall a b. (a -> b) -> a -> b
$ \TransSt
st -> TransSt
st { _extVarsNodes = (id, t) : _extVarsNodes st }