--------------------------------------------------------------------------------

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

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 :: [Char]
ncSep         = [Char]
"."
ncMain :: [Char]
ncMain        = [Char]
"out"
ncNode :: a -> [Char]
ncNode a
i      = [Char]
"s" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
i
ncPropNode :: [Char] -> [Char]
ncPropNode [Char]
s  = [Char]
"prop-" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s
ncTopNode :: [Char]
ncTopNode     = [Char]
"top"
ncAnonInput :: [Char]
ncAnonInput   = [Char]
"in"
ncLocal :: [Char] -> [Char]
ncLocal [Char]
s     = [Char]
"l" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Char -> Bool) -> [Char] -> [Char]
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) [Char]
s

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

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

ncTimeAnnot :: String -> Int -> String
ncTimeAnnot :: [Char] -> Int -> [Char]
ncTimeAnnot [Char]
s Int
d
  | Int
d Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0    = [Char]
s
  | Bool
otherwise = [Char]
s [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
ncSep [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
d

--------------------------------------------------------------------------------

translate :: C.Spec -> TransSys
translate :: Spec -> TransSys
translate Spec
cspec =

  TransSys :: [Node] -> [Char] -> Map [Char] ExtVar -> TransSys
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 :: [Char]
specTopNodeId = [Char]
topNodeId
       , specProps :: Map [Char] ExtVar
specProps = Map [Char] ExtVar
propBindings }

  where

    topNodeId :: [Char]
topNodeId = [Char]
ncTopNode

    cprops :: [C.Property]
    cprops :: [Property]
cprops = Spec -> [Property]
C.specProperties Spec
cspec

    propBindings :: Map PropId ExtVar
    propBindings :: Map [Char] ExtVar
propBindings = [([Char], ExtVar)] -> Map [Char] ExtVar
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([([Char], ExtVar)] -> Map [Char] ExtVar)
-> [([Char], ExtVar)] -> Map [Char] ExtVar
forall a b. (a -> b) -> a -> b
$ do
      [Char]
pid <- (Property -> [Char]) -> [Property] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map Property -> [Char]
C.propertyName [Property]
cprops
      ([Char], ExtVar) -> [([Char], ExtVar)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char]
pid, [Char] -> [Char] -> ExtVar
mkExtVar [Char]
topNodeId [Char]
pid)

    (([Node]
modelNodes, [Node]
propNodes), [([Char], U Type)]
extvarNodesNames) = Trans ([Node], [Node]) -> (([Node], [Node]), [([Char], U Type)])
forall a. Trans a -> (a, [([Char], U Type)])
runTrans (Trans ([Node], [Node]) -> (([Node], [Node]), [([Char], U Type)]))
-> Trans ([Node], [Node]) -> (([Node], [Node]), [([Char], 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)
mapM Stream -> StateT TransSt Identity Node
stream (Spec -> [Stream]
C.specStreams Spec
cspec)) ([Property] -> StateT TransSt Identity [Node]
mkPropNodes [Property]
cprops)

    topNode :: Node
topNode = [Char] -> [[Char]] -> [Property] -> Node
mkTopNode [Char]
topNodeId ((Node -> [Char]) -> [Node] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map Node -> [Char]
nodeId [Node]
propNodes) [Property]
cprops
    extVarNodes :: [Node]
extVarNodes = (([Char], U Type) -> Node) -> [([Char], U Type)] -> [Node]
forall a b. (a -> b) -> [a] -> [b]
map ([Char], U Type) -> Node
mkExtVarNode [([Char], U Type)]
extvarNodesNames

--------------------------------------------------------------------------------


mkTopNode :: String -> [NodeId] -> [C.Property] -> Node
mkTopNode :: [Char] -> [[Char]] -> [Property] -> Node
mkTopNode [Char]
topNodeId [[Char]]
dependencies [Property]
cprops =
  Node :: [Char]
-> [[Char]]
-> Map Var VarDescr
-> Bimap Var ExtVar
-> [Expr Bool]
-> Node
Node { nodeId :: [Char]
nodeId = [Char]
topNodeId
       , nodeDependencies :: [[Char]]
nodeDependencies = [[Char]]
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
      [ ([Char] -> Var
Var [Char]
cp, [Char] -> [Char] -> ExtVar
mkExtVar ([Char] -> [Char]
ncPropNode [Char]
cp) [Char]
ncMain)
      | [Char]
cp <- Property -> [Char]
C.propertyName (Property -> [Char]) -> [Property] -> [[Char]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Property]
cprops ]



mkExtVarNode :: ([Char], U Type) -> Node
mkExtVarNode ([Char]
name, U Type t
t) =
  Node :: [Char]
-> [[Char]]
-> Map Var VarDescr
-> Bimap Var ExtVar
-> [Expr Bool]
-> Node
Node { nodeId :: [Char]
nodeId = [Char]
name
       , nodeDependencies :: [[Char]]
nodeDependencies = []
       , nodeLocalVars :: Map Var VarDescr
nodeLocalVars = Var -> VarDescr -> Map Var VarDescr
forall k a. k -> a -> Map k a
Map.singleton ([Char] -> Var
Var [Char]
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)
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 (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 :: [Char]
nodeId = [Char] -> [Char]
ncPropNode (Property -> [Char]
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 =
  Stream :: forall a.
(Typeable a, Typed a) =>
Int -> [a] -> Expr a -> Type a -> Stream
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 -> StateT TransSt Identity 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 })

  = 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 :: [Char]
nodeId = Int -> [Char]
forall a. Show a => a -> [Char]
ncNode Int
streamId
        outvar :: Int -> Var
outvar Int
i = [Char] -> Var
Var ([Char]
ncMain [Char] -> Int -> [Char]
`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
. Type a -> a -> Dyn
forall (t :: * -> *) a. t a -> a -> Dynamic t
toDyn Type a
streamExprType) [a]
streamBuffer

    (Expr t'
e, Map Var VarDescr
nodeAuxVars, Bimap Var ExtVar
nodeImportedVars, [[Char]]
nodeDependencies) <-
      Type t'
-> [Char]
-> Expr a
-> Trans (Expr t', Map Var VarDescr, Bimap Var ExtVar, [[Char]])
forall t a.
Type t
-> [Char]
-> Expr a
-> Trans (Expr t, Map Var VarDescr, Bimap Var ExtVar, [[Char]])
runExprTrans Type t'
t [Char]
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 (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 (m :: * -> *) a. Monad m => a -> m a
return Node :: [Char]
-> [[Char]]
-> Map Var VarDescr
-> Bimap Var ExtVar
-> [Expr Bool]
-> Node
Node
      { [Char]
nodeId :: [Char]
nodeId :: [Char]
nodeId, [[Char]]
nodeDependencies :: [[Char]]
nodeDependencies :: [[Char]]
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 :: Type t -> Expr t' -> Trans (Expr t)
expr Type t
t (C.Const Type t'
t' t'
v) = Expr t -> Trans (Expr t)
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 -> 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
$ Type t' -> t' -> Dyn
forall (t :: * -> *) a. t a -> a -> Dynamic t
toDyn Type t'
t' 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 :: [Char]
node = Int -> [Char]
forall a. Show a => a -> [Char]
ncNode Int
id
  Bool
selfRef <- ([Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== [Char]
node) ([Char] -> Bool)
-> StateT TransSt Identity [Char] -> StateT TransSt Identity Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT TransSt Identity [Char]
curNode
  let varName :: [Char]
varName = [Char]
ncMain [Char] -> Int -> [Char]
`ncTimeAnnot` Int
k
  let var :: Var
var = [Char] -> Var
Var ([Char] -> Var) -> [Char] -> Var
forall a b. (a -> b) -> a -> b
$ if Bool
selfRef then [Char]
varName else [Char] -> [Char] -> [Char]
ncImported [Char]
node [Char]
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
    [Char] -> StateT TransSt Identity ()
forall (m :: * -> *). MonadState TransSt m => [Char] -> m ()
newDep [Char]
node
    Var -> ExtVar -> StateT TransSt Identity ()
forall (m :: * -> *). MonadState TransSt m => Var -> ExtVar -> m ()
newImportedVar Var
var ([Char] -> [Char] -> ExtVar
mkExtVar [Char]
node [Char]
varName)
  Expr t -> Trans (Expr t)
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 Var
var

expr Type t
t (C.Label Type t'
_ [Char]
_ Expr t'
e) = Type t -> Expr t' -> Trans (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 [Char]
id Expr a1
l Expr t'
e) = Type a1 -> (forall t'. Type t' -> Trans (Expr t)) -> Trans (Expr t)
forall t a. Type t -> (forall t'. Type t' -> a) -> a
casting Type a1
tl ((forall t'. Type t' -> Trans (Expr t)) -> Trans (Expr t))
-> (forall t'. Type t' -> Trans (Expr t)) -> Trans (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 ([Char] -> Var
Var ([Char] -> Var) -> [Char] -> Var
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
ncLocal [Char]
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' -> Trans (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' [Char]
id) = Expr t -> Trans (Expr t)
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 ([Char] -> Var
Var ([Char] -> Var) -> [Char] -> Var
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
ncLocal [Char]
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 -> Trans (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 -> Trans (Expr t)
forall t t'. Type t -> Expr t' -> Trans (Expr t)
expr Type t
t    Expr c
e2
  Expr t -> Trans (Expr t)
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 -> 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'
_ [Char]
name Maybe [t']
_) = do
  let nodeName :: [Char]
nodeName = [Char] -> [Char]
ncExternVarNode [Char]
name
  let localAlias :: Var
localAlias = [Char] -> Var
Var [Char]
nodeName
  [Char] -> U Type -> StateT TransSt Identity ()
forall (m :: * -> *).
MonadState TransSt m =>
[Char] -> U Type -> m ()
newExtVarNode [Char]
nodeName (Type t -> U Type
forall (f :: * -> *) t. f t -> U f
U Type t
t)
  [Char] -> StateT TransSt Identity ()
forall (m :: * -> *). MonadState TransSt m => [Char] -> m ()
newDep [Char]
nodeName
  Var -> ExtVar -> StateT TransSt Identity ()
forall (m :: * -> *). MonadState TransSt m => Var -> ExtVar -> m ()
newImportedVar Var
localAlias ([Char] -> Var -> ExtVar
ExtVar [Char]
nodeName ([Char] -> Var
Var [Char]
ncMain))
  Expr t -> Trans (Expr t)
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 Var
localAlias

-- TODO : Use uninterpreted functions to handle
-- * Unhandled operators
-- * Extern functions
-- * Extern arrays
-- For now, the result of these operations is a new unconstrained variable

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 -> Trans (Expr t))
-> (forall t. Type t -> Op1 t -> Expr t -> Expr t)
-> Trans (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) forall t t'. Type t -> Expr t' -> Trans (Expr t)
expr UnhandledOp1 -> Trans (Expr t)
notHandled forall t. Type t -> Op1 t -> Expr t -> Expr t
Op1
  where
    notHandled :: UnhandledOp1 -> Trans (Expr t)
notHandled (UnhandledOp1 [Char]
_opName Type a
_ta Type b
_tb) =
      Type t -> Trans (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 -> Trans (Expr t))
-> (forall t a. Type t -> Op2 a t -> Expr a -> Expr a -> Expr t)
-> (Expr Bool -> Expr Bool)
-> Trans (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) forall t t'. Type t -> Expr t' -> Trans (Expr t)
expr UnhandledOp2 -> Trans (Expr t)
notHandled 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 -> Trans (Expr t)
notHandled (UnhandledOp2 [Char]
_opName Type a
_ta Type b
_tb Type c
_tc) =
      Type t -> Trans (Expr t)
forall t. Type t -> Trans (Expr t)
newUnconstrainedVar Type t
t

newUnconstrainedVar :: Type t -> Trans (Expr t)
newUnconstrainedVar :: Type t -> Trans (Expr t)
newUnconstrainedVar Type t
t = do
  [Char]
newNode <- StateT TransSt Identity [Char]
getFreshNodeName
  Var -> VarDescr -> StateT TransSt Identity ()
forall (m :: * -> *).
MonadState TransSt m =>
Var -> VarDescr -> m ()
newLocal ([Char] -> Var
Var [Char]
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 []
  [Char] -> StateT TransSt Identity ()
forall (m :: * -> *). MonadState TransSt m => [Char] -> m ()
newDep [Char]
newNode
  Expr t -> Trans (Expr t)
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 ([Char] -> Var
Var [Char]
newNode)

--------------------------------------------------------------------------------

runTrans :: Trans a -> (a, [(NodeId, U Type)])
runTrans :: Trans a -> (a, [([Char], U Type)])
runTrans Trans a
mx =
  (a
x, (([Char], U Type) -> ([Char], U Type) -> Ordering)
-> [([Char], U Type)] -> [([Char], U Type)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
nubBy' ([Char] -> [Char] -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ([Char] -> [Char] -> Ordering)
-> (([Char], U Type) -> [Char])
-> ([Char], U Type)
-> ([Char], U Type)
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` ([Char], U Type) -> [Char]
forall a b. (a, b) -> a
fst) ([([Char], U Type)] -> [([Char], U Type)])
-> [([Char], U Type)] -> [([Char], U Type)]
forall a b. (a -> b) -> a -> b
$ TransSt -> [([Char], 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 :: Map Var VarDescr
-> Bimap Var ExtVar
-> [[Char]]
-> [([Char], U Type)]
-> [Char]
-> Int
-> TransSt
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 :: [[Char]]
_dependencies = []
      , _extVarsNodes :: [([Char], U Type)]
_extVarsNodes = []
      , _curNode :: [Char]
_curNode      = [Char]
""
      , _nextUid :: Int
_nextUid      = Int
0 }

runExprTrans ::
  Type t -> NodeId -> C.Expr a ->
  Trans (Expr t, Map Var VarDescr, Bimap Var ExtVar, [NodeId])

runExprTrans :: Type t
-> [Char]
-> Expr a
-> Trans (Expr t, Map Var VarDescr, Bimap Var ExtVar, [[Char]])
runExprTrans Type t
t [Char]
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 :: [Char]
_curNode = [Char]
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 :: Int
_nextUid = Int
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, [[Char]]
dps) <- State TransSt (Map Var VarDescr, Bimap Var ExtVar, [[Char]])
popLocalInfos
  (Expr t, Map Var VarDescr, Bimap Var ExtVar, [[Char]])
-> Trans (Expr t, Map Var VarDescr, Bimap Var ExtVar, [[Char]])
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr t
e', Map Var VarDescr
lvs, Bimap Var ExtVar
ivs, [[Char]]
dps)

data TransSt = TransSt
  { TransSt -> Map Var VarDescr
_lvars        :: Map Var VarDescr
  , TransSt -> Bimap Var ExtVar
_importedVars :: Bimap Var ExtVar
  , TransSt -> [[Char]]
_dependencies :: [NodeId]
  , TransSt -> [([Char], U Type)]
_extVarsNodes :: [(NodeId, U Type)]
  , TransSt -> [Char]
_curNode      :: NodeId
  , TransSt -> Int
_nextUid      :: Int }

type Trans a = State TransSt a

newDep :: [Char] -> m ()
newDep [Char]
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 :: [[Char]]
_dependencies = [Char]
d [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: TransSt -> [[Char]]
_dependencies TransSt
s }

popLocalInfos :: State TransSt (Map Var VarDescr, Bimap Var ExtVar, [NodeId])
popLocalInfos :: State TransSt (Map Var VarDescr, Bimap Var ExtVar, [[Char]])
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
  [[Char]]
dps <- TransSt -> [[Char]]
_dependencies (TransSt -> [[Char]])
-> StateT TransSt Identity TransSt
-> StateT TransSt Identity [[Char]]
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 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 :: [[Char]]
_dependencies = [] }
  (Map Var VarDescr, Bimap Var ExtVar, [[Char]])
-> State TransSt (Map Var VarDescr, Bimap Var ExtVar, [[Char]])
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Var VarDescr
lvs, Bimap Var ExtVar
ivs, [[Char]] -> [[Char]]
forall a. Ord a => [a] -> [a]
nub' [[Char]]
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 :: Int
_nextUid = Int
uid Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 }
  Int -> Trans Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
uid

getFreshNodeName :: Trans NodeId
getFreshNodeName :: StateT TransSt Identity [Char]
getFreshNodeName = (Int -> [Char]) -> Trans Int -> StateT TransSt Identity [Char]
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (([Char]
"_" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++) ([Char] -> [Char]) -> (Int -> [Char]) -> Int -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [Char]
forall a. Show a => a -> [Char]
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 Var ExtVar
_importedVars = Var -> ExtVar -> Bimap Var ExtVar -> Bimap Var ExtVar
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  =  (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 Var VarDescr
_lvars = Var -> VarDescr -> Map Var VarDescr -> Map Var VarDescr
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Var
l VarDescr
d (Map Var VarDescr -> Map Var VarDescr)
-> Map Var VarDescr -> Map Var VarDescr
forall a b. (a -> b) -> a -> b
$ TransSt -> Map Var VarDescr
_lvars TransSt
s }

curNode :: StateT TransSt Identity [Char]
curNode = TransSt -> [Char]
_curNode (TransSt -> [Char])
-> StateT TransSt Identity TransSt
-> StateT TransSt Identity [Char]
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 :: [Char] -> U Type -> m ()
newExtVarNode [Char]
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 :: [([Char], U Type)]
_extVarsNodes = ([Char]
id, U Type
t) ([Char], U Type) -> [([Char], U Type)] -> [([Char], U Type)]
forall a. a -> [a] -> [a]
: TransSt -> [([Char], U Type)]
_extVarsNodes TransSt
st }

--------------------------------------------------------------------------------