    {-# 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, Prop)
    specProps = Map NodeId (ExtVar, Prop)
    propBindings }

      where

        topNodeId :: NodeId
    topNodeId = NodeId
    ncTopNode

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

        propBindings :: Map PropId (ExtVar, C.Prop)
        propBindings :: Map NodeId (ExtVar, Prop)
    propBindings = [(NodeId, (ExtVar, Prop))] -> Map NodeId (ExtVar, Prop)
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList ([(NodeId, (ExtVar, Prop))] -> Map NodeId (ExtVar, Prop))
    -> [(NodeId, (ExtVar, Prop))] -> Map NodeId (ExtVar, Prop)
    forall a b. (a -> b) -> a -> b
    $ do
          cprop <- [Property]
    cprops
          let pid  = Property -> NodeId
    C.propertyName Property
    cprop
              prop = Property -> Prop
    C.propertyProp Property
    cprop
          return (pid, (mkExtVar topNodeId pid, prop))

        (([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
          s <- Stream -> StateT TransSt Identity Node
    stream (Property -> Stream
    streamOfProp Property
    p)
          return $ 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 = []
                 -- TransSys encodes all properties using universal quantification.
                 -- Therefore, in order to encode an existentially quantified
                 -- property ∃x.P(x), we must first convert it to ¬(∀x.¬(P(x))).
                 -- The `Exists` case below handles the ∀x.¬(P(x)) part by adding
                 -- an `Op1 Not` around the property. The outermost negation is
                 -- handled elsewhere (e.g., in Copilot.Theorem.Kind2.Output.parse).
               , streamExpr :: Expr Bool
    C.streamExpr = case Property -> Prop
    C.propertyProp Property
    prop of
                                  C.Forall Expr Bool
    p -> Expr Bool
    p
                                  C.Exists Expr Bool
    p -> Op1 Bool Bool -> Expr Bool -> Expr Bool
    forall a1 a. Typeable a1 => Op1 a1 a -> Expr a1 -> Expr a
    C.Op1 Op1 Bool Bool
    C.Not Expr Bool
    p
               , 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

        (e, nodeAuxVars, nodeImportedVars, 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 =
              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 -> 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 = (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]

        return Node
          { nodeId, nodeDependencies, nodeLocalVars
          , nodeImportedVars, 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
      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
    ncMain NodeId -> Int -> NodeId
    `ncTimeAnnot` Int
    k
      let 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
      unless selfRef $ do
        newDep node
        newImportedVar var (mkExtVar node varName)
      return $ VarE t 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
      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
      newLocal (Var $ ncLocal id) $ VarDescr tl' $ Expr l'
      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
      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
      e1'   <- expr t    e1
      e2'   <- expr t    e2
      return $ Ite t cond' e1' 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
      newNode <- StateT TransSt Identity NodeId
    getFreshNodeName
      newLocal (Var newNode) $ VarDescr t $ Constrs []
      newDep newNode
      return $ VarE t (Var 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 }
      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
      (lvs, ivs, dps) <- popLocalInfos
      return (e', lvs, ivs, 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
      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
      ivs <- _importedVars <$> get
      dps <- _dependencies <$> get
      modify $ \TransSt
    st -> TransSt
    st
        { _lvars = Map.empty
        , _importedVars = Bimap.empty
        , _dependencies = [] }
      return (lvs, ivs, nub' dps)

    getUid :: Trans Int
    getUid :: Trans Int
    getUid = do
      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
      modify $ \TransSt
    st -> TransSt
    st { _nextUid = uid + 1 }
      return 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 }