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

    -- | Convert modular transition systems ('TransSys') into Kind2 file
    -- specifications.
    module Copilot.Theorem.Kind2.Translate
      ( toKind2
      , Style (..)
      ) where

    import Copilot.Theorem.TransSys
    import qualified Copilot.Theorem.Kind2.AST as K

    import Control.Exception.Base (assert)

    import Data.Function (on)
    import Data.Maybe (fromJust)

    import Data.List (sort, sortBy)
    import Data.Map (Map, (!))

    import qualified Data.Map as Map
    import qualified Data.Bimap as Bimap

    -- The following properties MUST hold for the given transition system :
    -- * Nodes are sorted by topological order
    -- * Nodes are `completed`, which means the dependency graph is transitive
    --   and each node imports all the local variables of its dependencies
    --

    type DepGraph = Map NodeId [NodeId]

    -- | Style of the Kind2 files produced: modular (with multiple separate nodes),
    -- or all inlined (with only one node).
    --
    -- In the modular style, the graph is simplified to remove cycles by collapsing
    -- all nodes participating in a strongly connected components.
    --
    -- In the inlined style, the structure of the modular transition system is
    -- discarded and the graph is first turned into a /non-modular transition/
    -- /system/ with only one node, which can be then converted into a Kind2 file.
    data Style = Inlined | Modular

    -- | Produce a Kind2 file that checks the properties specified.
    toKind2 :: Style     -- ^ Style of the file (modular or inlined).
            -> [PropId]  -- ^ Assumptions
            -> [PropId]  -- ^ Properties to be checked
            -> TransSys  -- ^ Modular transition system holding the system spec
            -> K.File
    toKind2 :: Style -> [NodeId] -> [NodeId] -> TransSys -> File
    toKind2 Style
    style [NodeId]
    assumptions [NodeId]
    checkedProps TransSys
    spec =
      TransSys -> [NodeId] -> File -> File
    addAssumptions TransSys
    spec [NodeId]
    assumptions
      (File -> File) -> File -> File
    forall a b. (a -> b) -> a -> b
    $ TransSys -> DepGraph -> [NodeId] -> [NodeId] -> File
    trSpec (TransSys -> TransSys
    complete TransSys
    spec') DepGraph
    predCallsGraph [NodeId]
    assumptions [NodeId]
    checkedProps
      where
        predCallsGraph :: DepGraph
    predCallsGraph = TransSys -> DepGraph
    specDependenciesGraph TransSys
    spec'
        spec' :: TransSys
    spec' = case Style
    style of
          Style
    Inlined -> TransSys -> TransSys
    inline TransSys
    spec
          Style
    Modular -> TransSys -> TransSys
    removeCycles TransSys
    spec

    trSpec :: TransSys -> DepGraph -> [PropId] -> [PropId] -> K.File
    trSpec :: TransSys -> DepGraph -> [NodeId] -> [NodeId] -> File
    trSpec TransSys
    spec DepGraph
    predCallsGraph [NodeId]
    _assumptions [NodeId]
    checkedProps = [PredDef] -> [Prop] -> File
    K.File [PredDef]
    preds [Prop]
    props
      where
        preds :: [PredDef]
    preds = (Node -> PredDef) -> [Node] -> [PredDef]
    forall a b. (a -> b) -> [a] -> [b]
    map (TransSys -> DepGraph -> Node -> PredDef
    trNode TransSys
    spec DepGraph
    predCallsGraph) (TransSys -> [Node]
    specNodes TransSys
    spec)
        props :: [Prop]
    props = ((NodeId, ExtVar) -> Prop) -> [(NodeId, ExtVar)] -> [Prop]
    forall a b. (a -> b) -> [a] -> [b]
    map (NodeId, ExtVar) -> Prop
    trProp ([(NodeId, ExtVar)] -> [Prop]) -> [(NodeId, ExtVar)] -> [Prop]
    forall a b. (a -> b) -> a -> b
    $
          ((NodeId, ExtVar) -> Bool)
    -> [(NodeId, ExtVar)] -> [(NodeId, ExtVar)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ((NodeId -> [NodeId] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [NodeId]
    checkedProps) (NodeId -> Bool)
    -> ((NodeId, ExtVar) -> NodeId) -> (NodeId, ExtVar) -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (NodeId, ExtVar) -> NodeId
    forall a b. (a, b) -> a
    fst) ([(NodeId, ExtVar)] -> [(NodeId, ExtVar)])
    -> [(NodeId, ExtVar)] -> [(NodeId, ExtVar)]
    forall a b. (a -> b) -> a -> b
    $
            Map NodeId ExtVar -> [(NodeId, ExtVar)]
    forall k a. Map k a -> [(k, a)]
    Map.toList (Map NodeId ExtVar -> [(NodeId, ExtVar)])
    -> Map NodeId ExtVar -> [(NodeId, ExtVar)]
    forall a b. (a -> b) -> a -> b
    $ ((ExtVar, Prop) -> ExtVar)
    -> Map NodeId (ExtVar, Prop) -> Map NodeId ExtVar
    forall a b k. (a -> b) -> Map k a -> Map k b
    Map.map (ExtVar, Prop) -> ExtVar
    forall a b. (a, b) -> a
    fst (Map NodeId (ExtVar, Prop) -> Map NodeId ExtVar)
    -> Map NodeId (ExtVar, Prop) -> Map NodeId ExtVar
    forall a b. (a -> b) -> a -> b
    $ TransSys -> Map NodeId (ExtVar, Prop)
    specProps TransSys
    spec

    trProp :: (PropId, ExtVar) -> K.Prop
    trProp :: (NodeId, ExtVar) -> Prop
    trProp (NodeId
    pId, ExtVar
    var) = NodeId -> Term -> Prop
    K.Prop NodeId
    pId (Var -> Term
    trVar (Var -> Term) -> (ExtVar -> Var) -> ExtVar -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ExtVar -> Var
    extVarLocalPart (ExtVar -> Term) -> ExtVar -> Term
    forall a b. (a -> b) -> a -> b
    $ ExtVar
    var)

    trNode :: TransSys -> DepGraph -> Node -> K.PredDef
    trNode :: TransSys -> DepGraph -> Node -> PredDef
    trNode TransSys
    spec DepGraph
    predCallsGraph Node
    node =
      K.PredDef { NodeId
    predId :: NodeId
    predId :: NodeId
    K.predId, [StateVarDef]
    predStateVars :: [StateVarDef]
    predStateVars :: [StateVarDef]
    K.predStateVars, Term
    predInit :: Term
    predInit :: Term
    K.predInit, Term
    predTrans :: Term
    predTrans :: Term
    K.predTrans }
      where
        predId :: NodeId
    predId = Node -> NodeId
    nodeId Node
    node
        predStateVars :: [StateVarDef]
    predStateVars = TransSys -> Node -> [StateVarDef]
    gatherPredStateVars TransSys
    spec Node
    node
        predInit :: Term
    predInit  = [Term] -> Term
    mkConj ([Term] -> Term) -> [Term] -> Term
    forall a b. (a -> b) -> a -> b
    $ Node -> [Term]
    initLocals  Node
    node
                             [Term] -> [Term] -> [Term]
    forall a. [a] -> [a] -> [a]
    ++ (Expr Bool -> Term) -> [Expr Bool] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map (Bool -> Expr Bool -> Term
    forall t. Bool -> Expr t -> Term
    trExpr Bool
    False) (Node -> [Expr Bool]
    nodeConstrs Node
    node)
                             [Term] -> [Term] -> [Term]
    forall a. [a] -> [a] -> [a]
    ++ Bool -> TransSys -> DepGraph -> Node -> [Term]
    predCalls Bool
    True TransSys
    spec DepGraph
    predCallsGraph Node
    node
        predTrans :: Term
    predTrans = [Term] -> Term
    mkConj ([Term] -> Term) -> [Term] -> Term
    forall a b. (a -> b) -> a -> b
    $ Node -> [Term]
    transLocals Node
    node
                             [Term] -> [Term] -> [Term]
    forall a. [a] -> [a] -> [a]
    ++ (Expr Bool -> Term) -> [Expr Bool] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map (Bool -> Expr Bool -> Term
    forall t. Bool -> Expr t -> Term
    trExpr Bool
    True) (Node -> [Expr Bool]
    nodeConstrs Node
    node)
                             [Term] -> [Term] -> [Term]
    forall a. [a] -> [a] -> [a]
    ++ Bool -> TransSys -> DepGraph -> Node -> [Term]
    predCalls Bool
    False TransSys
    spec DepGraph
    predCallsGraph Node
    node

    addAssumptions :: TransSys -> [PropId] -> K.File -> K.File
    addAssumptions :: TransSys -> [NodeId] -> File -> File
    addAssumptions TransSys
    spec [NodeId]
    assumptions (K.File {[PredDef]
    filePreds :: [PredDef]
    filePreds :: File -> [PredDef]
    K.filePreds, [Prop]
    fileProps :: [Prop]
    fileProps :: File -> [Prop]
    K.fileProps}) =
      [PredDef] -> [Prop] -> File
    K.File ((PredDef -> PredDef) -> [PredDef] -> [PredDef]
    forall {a}. (a -> a) -> [a] -> [a]
    changeTail PredDef -> PredDef
    aux [PredDef]
    filePreds) [Prop]
    fileProps
      where
        changeTail :: (a -> a) -> [a] -> [a]
    changeTail a -> a
    f ([a] -> [a]
    forall a. [a] -> [a]
    reverse -> [a]
    l) = case [a]
    l of
          []     -> NodeId -> [a]
    forall a. HasCallStack => NodeId -> a
    error NodeId
    "impossible"
          a
    x : [a]
    xs -> [a] -> [a]
    forall a. [a] -> [a]
    reverse ([a] -> [a]) -> [a] -> [a]
    forall a b. (a -> b) -> a -> b
    $ a -> a
    f a
    x a -> [a] -> [a]
    forall a. a -> [a] -> [a]
    : [a]
    xs

        aux :: PredDef -> PredDef
    aux PredDef
    pred =
          let init' :: Term
    init'  = [Term] -> Term
    mkConj ( PredDef -> Term
    K.predInit  PredDef
    pred Term -> [Term] -> [Term]
    forall a. a -> [a] -> [a]
    : (NodeId -> Term) -> [NodeId] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map NodeId -> Term
    K.StateVar [NodeId]
    vars )
              trans' :: Term
    trans' = [Term] -> Term
    mkConj ( PredDef -> Term
    K.predTrans PredDef
    pred Term -> [Term] -> [Term]
    forall a. a -> [a] -> [a]
    : (NodeId -> Term) -> [NodeId] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map NodeId -> Term
    K.PrimedStateVar [NodeId]
    vars )
          in PredDef
    pred { K.predInit = init', K.predTrans = trans' }

        vars :: [NodeId]
    vars =
          let bindings :: Bimap Var ExtVar
    bindings   = Node -> Bimap Var ExtVar
    nodeImportedVars (TransSys -> Node
    specTopNode TransSys
    spec)
              toExtVar :: NodeId -> ExtVar
    toExtVar NodeId
    a = (ExtVar, Prop) -> ExtVar
    forall a b. (a, b) -> a
    fst ((ExtVar, Prop) -> ExtVar) -> (ExtVar, Prop) -> ExtVar
    forall a b. (a -> b) -> a -> b
    $ Maybe (ExtVar, Prop) -> (ExtVar, Prop)
    forall a. HasCallStack => Maybe a -> a
    fromJust (Maybe (ExtVar, Prop) -> (ExtVar, Prop))
    -> Maybe (ExtVar, Prop) -> (ExtVar, Prop)
    forall a b. (a -> b) -> a -> b
    $ NodeId -> Map NodeId (ExtVar, Prop) -> Maybe (ExtVar, Prop)
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup NodeId
    a (Map NodeId (ExtVar, Prop) -> Maybe (ExtVar, Prop))
    -> Map NodeId (ExtVar, Prop) -> Maybe (ExtVar, Prop)
    forall a b. (a -> b) -> a -> b
    $ TransSys -> Map NodeId (ExtVar, Prop)
    specProps TransSys
    spec
              toTopVar :: ExtVar -> Var
    toTopVar (ExtVar NodeId
    nId Var
    v) = Bool -> Var -> Var
    forall a. HasCallStack => Bool -> a -> a
    assert (NodeId
    nId NodeId -> NodeId -> Bool
    forall a. Eq a => a -> a -> Bool
    == TransSys -> NodeId
    specTopNodeId TransSys
    spec) Var
    v
          in (NodeId -> NodeId) -> [NodeId] -> [NodeId]
    forall a b. (a -> b) -> [a] -> [b]
    map (Var -> NodeId
    varName (Var -> NodeId) -> (NodeId -> Var) -> NodeId -> NodeId
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ExtVar -> Var
    toTopVar (ExtVar -> Var) -> (NodeId -> ExtVar) -> NodeId -> Var
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NodeId -> ExtVar
    toExtVar) [NodeId]
    assumptions

    -- The ordering really matters here because the variables
    -- have to be given in this order in a pred call
    -- Our convention :
    -- * First the local variables, sorted by alphabetical order
    -- * Then the imported variables, by alphabetical order on
    --   the father node then by alphabetical order on the variable name

    gatherPredStateVars :: TransSys -> Node -> [K.StateVarDef]
    gatherPredStateVars :: TransSys -> Node -> [StateVarDef]
    gatherPredStateVars TransSys
    spec Node
    node = [StateVarDef]
    locals [StateVarDef] -> [StateVarDef] -> [StateVarDef]
    forall a. [a] -> [a] -> [a]
    ++ [StateVarDef]
    imported
      where
        nodesMap :: Map NodeId Node
    nodesMap = [(NodeId, Node)] -> Map NodeId Node
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList [(Node -> NodeId
    nodeId Node
    n, Node
    n) | Node
    n <- TransSys -> [Node]
    specNodes TransSys
    spec]
        extVarType :: ExtVar -> K.Type
        extVarType :: ExtVar -> Type
    extVarType (ExtVar NodeId
    n Var
    v) =
          case Node -> Map Var VarDescr
    nodeLocalVars (Map NodeId Node
    nodesMap Map NodeId Node -> NodeId -> Node
    forall k a. Ord k => Map k a -> k -> a
    ! NodeId
    n) Map Var VarDescr -> Var -> VarDescr
    forall k a. Ord k => Map k a -> k -> a
    ! Var
    v of
            VarDescr Type t
    Integer VarDef t
    _ -> Type
    K.Int
            VarDescr Type t
    Bool    VarDef t
    _ -> Type
    K.Bool
            VarDescr Type t
    Real    VarDef t
    _ -> Type
    K.Real

        locals :: [StateVarDef]
    locals =
          (Var -> StateVarDef) -> [Var] -> [StateVarDef]
    forall a b. (a -> b) -> [a] -> [b]
    map (\Var
    v -> NodeId -> Type -> [StateVarFlag] -> StateVarDef
    K.StateVarDef (Var -> NodeId
    varName Var
    v)
                  (ExtVar -> Type
    extVarType (ExtVar -> Type) -> ExtVar -> Type
    forall a b. (a -> b) -> a -> b
    $ NodeId -> Var -> ExtVar
    ExtVar (Node -> NodeId
    nodeId Node
    node) Var
    v) [])
             ([Var] -> [StateVarDef])
    -> (Map Var VarDescr -> [Var]) -> Map Var VarDescr -> [StateVarDef]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Var] -> [Var]
    forall a. Ord a => [a] -> [a]
    sort ([Var] -> [Var])
    -> (Map Var VarDescr -> [Var]) -> Map Var VarDescr -> [Var]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Map Var VarDescr -> [Var]
    forall k a. Map k a -> [k]
    Map.keys (Map Var VarDescr -> [StateVarDef])
    -> Map Var VarDescr -> [StateVarDef]
    forall a b. (a -> b) -> a -> b
    $ Node -> Map Var VarDescr
    nodeLocalVars Node
    node

        imported :: [StateVarDef]
    imported =
          ((Var, ExtVar) -> StateVarDef) -> [(Var, ExtVar)] -> [StateVarDef]
    forall a b. (a -> b) -> [a] -> [b]
    map (\(Var
    v, ExtVar
    ev) -> NodeId -> Type -> [StateVarFlag] -> StateVarDef
    K.StateVarDef (Var -> NodeId
    varName Var
    v) (ExtVar -> Type
    extVarType ExtVar
    ev) [])
          ([(Var, ExtVar)] -> [StateVarDef])
    -> (Bimap Var ExtVar -> [(Var, ExtVar)])
    -> Bimap Var ExtVar
    -> [StateVarDef]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((Var, ExtVar) -> (Var, ExtVar) -> Ordering)
    -> [(Var, ExtVar)] -> [(Var, ExtVar)]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    sortBy (ExtVar -> ExtVar -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (ExtVar -> ExtVar -> Ordering)
    -> ((Var, ExtVar) -> ExtVar)
    -> (Var, ExtVar)
    -> (Var, ExtVar)
    -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` (Var, ExtVar) -> ExtVar
    forall a b. (a, b) -> b
    snd) ([(Var, ExtVar)] -> [(Var, ExtVar)])
    -> (Bimap Var ExtVar -> [(Var, ExtVar)])
    -> Bimap Var ExtVar
    -> [(Var, ExtVar)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Bimap Var ExtVar -> [(Var, ExtVar)]
    forall a b. Bimap a b -> [(a, b)]
    Bimap.toList (Bimap Var ExtVar -> [StateVarDef])
    -> Bimap Var ExtVar -> [StateVarDef]
    forall a b. (a -> b) -> a -> b
    $ Node -> Bimap Var ExtVar
    nodeImportedVars Node
    node

    mkConj :: [K.Term] -> K.Term
    mkConj :: [Term] -> Term
    mkConj []  = Type Bool -> Bool -> Term
    forall t. Type t -> t -> Term
    trConst Type Bool
    Bool Bool
    True
    mkConj [Term
    x] = Term
    x
    mkConj [Term]
    xs  = NodeId -> [Term] -> Term
    K.FunApp NodeId
    "and" [Term]
    xs

    mkEquality :: K.Term -> K.Term -> K.Term
    mkEquality :: Term -> Term -> Term
    mkEquality Term
    t1 Term
    t2 = NodeId -> [Term] -> Term
    K.FunApp NodeId
    "=" [Term
    t1, Term
    t2]

    trVar :: Var -> K.Term
    trVar :: Var -> Term
    trVar Var
    v = NodeId -> Term
    K.StateVar (Var -> NodeId
    varName Var
    v)

    trPrimedVar :: Var -> K.Term
    trPrimedVar :: Var -> Term
    trPrimedVar Var
    v = NodeId -> Term
    K.PrimedStateVar (Var -> NodeId
    varName Var
    v)

    trConst :: Type t -> t -> K.Term
    trConst :: forall t. Type t -> t -> Term
    trConst Type t
    Integer t
    v     = NodeId -> Term
    K.ValueLiteral (t -> NodeId
    forall a. Show a => a -> NodeId
    show t
    v)
    trConst Type t
    Real    t
    v     = NodeId -> Term
    K.ValueLiteral (t -> NodeId
    forall a. Show a => a -> NodeId
    show t
    v)
    trConst Type t
    Bool    t
    Bool
    True  = NodeId -> Term
    K.ValueLiteral NodeId
    "true"
    trConst Type t
    Bool    t
    Bool
    False = NodeId -> Term
    K.ValueLiteral NodeId
    "false"

    initLocals :: Node -> [K.Term]
    initLocals :: Node -> [Term]
    initLocals Node
    node =
      ((Var, VarDescr) -> [Term]) -> [(Var, VarDescr)] -> [Term]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (Var, VarDescr) -> [Term]
    f (Map Var VarDescr -> [(Var, VarDescr)]
    forall k a. Map k a -> [(k, a)]
    Map.toList (Map Var VarDescr -> [(Var, VarDescr)])
    -> Map Var VarDescr -> [(Var, VarDescr)]
    forall a b. (a -> b) -> a -> b
    $ Node -> Map Var VarDescr
    nodeLocalVars Node
    node)
      where
        f :: (Var, VarDescr) -> [Term]
    f (Var
    v, VarDescr Type t
    t VarDef t
    def) =
          case VarDef t
    def of
            Pre     t
    c Var
    _ -> [Term -> Term -> Term
    mkEquality (Var -> Term
    trVar Var
    v) (Type t -> t -> Term
    forall t. Type t -> t -> Term
    trConst Type t
    t t
    c)]
            Expr    Expr t
    e   -> [Term -> Term -> Term
    mkEquality (Var -> Term
    trVar Var
    v) (Bool -> Expr t -> Term
    forall t. Bool -> Expr t -> Term
    trExpr Bool
    False Expr t
    e)]
            Constrs [Expr Bool]
    cs  -> (Expr Bool -> Term) -> [Expr Bool] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map (Bool -> Expr Bool -> Term
    forall t. Bool -> Expr t -> Term
    trExpr Bool
    False) [Expr Bool]
    cs

    transLocals :: Node -> [K.Term]
    transLocals :: Node -> [Term]
    transLocals Node
    node =
      ((Var, VarDescr) -> [Term]) -> [(Var, VarDescr)] -> [Term]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (Var, VarDescr) -> [Term]
    f (Map Var VarDescr -> [(Var, VarDescr)]
    forall k a. Map k a -> [(k, a)]
    Map.toList (Map Var VarDescr -> [(Var, VarDescr)])
    -> Map Var VarDescr -> [(Var, VarDescr)]
    forall a b. (a -> b) -> a -> b
    $ Node -> Map Var VarDescr
    nodeLocalVars Node
    node)
      where
       f :: (Var, VarDescr) -> [Term]
    f (Var
    v, VarDescr Type t
    _ VarDef t
    def) =
          case VarDef t
    def of
            Pre t
    _ Var
    v' -> [Term -> Term -> Term
    mkEquality (Var -> Term
    trPrimedVar Var
    v) (Var -> Term
    trVar Var
    v')]
            Expr Expr t
    e   -> [Term -> Term -> Term
    mkEquality (Var -> Term
    trPrimedVar Var
    v) (Bool -> Expr t -> Term
    forall t. Bool -> Expr t -> Term
    trExpr Bool
    True Expr t
    e)]
            Constrs [Expr Bool]
    cs  -> (Expr Bool -> Term) -> [Expr Bool] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map (Bool -> Expr Bool -> Term
    forall t. Bool -> Expr t -> Term
    trExpr Bool
    True) [Expr Bool]
    cs

    predCalls :: Bool -> TransSys -> DepGraph -> Node -> [K.Term]
    predCalls :: Bool -> TransSys -> DepGraph -> Node -> [Term]
    predCalls Bool
    isInitCall TransSys
    spec DepGraph
    predCallsGraph Node
    node =
      (NodeId -> Term) -> [NodeId] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map NodeId -> Term
    mkCall [NodeId]
    toCall
      where
        nid :: NodeId
    nid = Node -> NodeId
    nodeId Node
    node
        toCall :: [NodeId]
    toCall = DepGraph
    predCallsGraph DepGraph -> NodeId -> [NodeId]
    forall k a. Ord k => Map k a -> k -> a
    ! NodeId
    nid
        nodesMap :: Map NodeId Node
    nodesMap = [(NodeId, Node)] -> Map NodeId Node
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList [(Node -> NodeId
    nodeId Node
    n, Node
    n) | Node
    n <- TransSys -> [Node]
    specNodes TransSys
    spec]

        nodeLocals :: NodeId -> [ExtVar]
    nodeLocals NodeId
    n =
          (Var -> ExtVar) -> [Var] -> [ExtVar]
    forall a b. (a -> b) -> [a] -> [b]
    map (NodeId -> Var -> ExtVar
    ExtVar NodeId
    n) ([Var] -> [ExtVar]) -> (Node -> [Var]) -> Node -> [ExtVar]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Var] -> [Var]
    forall a. Ord a => [a] -> [a]
    sort ([Var] -> [Var]) -> (Node -> [Var]) -> Node -> [Var]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Map Var VarDescr -> [Var]
    forall k a. Map k a -> [k]
    Map.keys
          (Map Var VarDescr -> [Var])
    -> (Node -> Map Var VarDescr) -> Node -> [Var]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Node -> Map Var VarDescr
    nodeLocalVars (Node -> [ExtVar]) -> Node -> [ExtVar]
    forall a b. (a -> b) -> a -> b
    $ (Map NodeId Node
    nodesMap Map NodeId Node -> NodeId -> Node
    forall k a. Ord k => Map k a -> k -> a
    ! NodeId
    n)

        mkCall :: NodeId -> Term
    mkCall NodeId
    callee
          | Bool
    isInitCall =
              NodeId -> PredType -> [Term] -> Term
    K.PredApp NodeId
    callee PredType
    K.Init ((Var -> Term) -> [Term]
    argsSeq Var -> Term
    trVar)
          | Bool
    otherwise  =
              NodeId -> PredType -> [Term] -> Term
    K.PredApp NodeId
    callee PredType
    K.Trans ((Var -> Term) -> [Term]
    argsSeq Var -> Term
    trVar [Term] -> [Term] -> [Term]
    forall a. [a] -> [a] -> [a]
    ++ (Var -> Term) -> [Term]
    argsSeq Var -> Term
    trPrimedVar)
          where

            calleeLocals :: [ExtVar]
    calleeLocals = NodeId -> [ExtVar]
    nodeLocals NodeId
    callee
            calleeImported :: [ExtVar]
    calleeImported =
              ((NodeId -> [ExtVar]) -> [NodeId] -> [ExtVar]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap NodeId -> [ExtVar]
    nodeLocals ([NodeId] -> [ExtVar]) -> (Node -> [NodeId]) -> Node -> [ExtVar]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [NodeId] -> [NodeId]
    forall a. Ord a => [a] -> [a]
    sort ([NodeId] -> [NodeId]) -> (Node -> [NodeId]) -> Node -> [NodeId]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Node -> [NodeId]
    nodeDependencies) (Node -> [ExtVar]) -> Node -> [ExtVar]
    forall a b. (a -> b) -> a -> b
    $ Map NodeId Node
    nodesMap Map NodeId Node -> NodeId -> Node
    forall k a. Ord k => Map k a -> k -> a
    ! NodeId
    callee

            localAlias :: (Var -> Term) -> ExtVar -> Term
    localAlias Var -> Term
    trVarF ExtVar
    ev =
              case ExtVar -> Bimap Var ExtVar -> Maybe Var
    forall a b (m :: * -> *).
    (Ord a, Ord b, MonadThrow m) =>
    b -> Bimap a b -> m a
    Bimap.lookupR ExtVar
    ev (Bimap Var ExtVar -> Maybe Var) -> Bimap Var ExtVar -> Maybe Var
    forall a b. (a -> b) -> a -> b
    $ Node -> Bimap Var ExtVar
    nodeImportedVars Node
    node of
                Maybe Var
    Nothing -> NodeId -> Term
    forall a. HasCallStack => NodeId -> a
    error (NodeId -> Term) -> NodeId -> Term
    forall a b. (a -> b) -> a -> b
    $
                  NodeId
    "This spec is not complete : "
                  NodeId -> NodeId -> NodeId
    forall a. [a] -> [a] -> [a]
    ++ ExtVar -> NodeId
    forall a. Show a => a -> NodeId
    show ExtVar
    ev NodeId -> NodeId -> NodeId
    forall a. [a] -> [a] -> [a]
    ++ NodeId
    " should be imported in " NodeId -> NodeId -> NodeId
    forall a. [a] -> [a] -> [a]
    ++ NodeId
    nid
                Just Var
    v -> Var -> Term
    trVarF Var
    v

            argsSeq :: (Var -> Term) -> [Term]
    argsSeq Var -> Term
    trVarF =
              (ExtVar -> Term) -> [ExtVar] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Var -> Term) -> ExtVar -> Term
    localAlias Var -> Term
    trVarF) ([ExtVar]
    calleeLocals [ExtVar] -> [ExtVar] -> [ExtVar]
    forall a. [a] -> [a] -> [a]
    ++ [ExtVar]
    calleeImported)

    trExpr :: Bool -> Expr t -> K.Term
    trExpr :: forall t. Bool -> Expr t -> Term
    trExpr Bool
    primed = Expr t -> Term
    forall t. Expr t -> Term
    tr
      where
        tr :: forall t . Expr t -> K.Term
        tr :: forall t. Expr t -> Term
    tr (Const Type t
    t t
    c) = Type t -> t -> Term
    forall t. Type t -> t -> Term
    trConst Type t
    t t
    c
        tr (Ite Type t
    _ Expr Bool
    c Expr t
    e1 Expr t
    e2) = NodeId -> [Term] -> Term
    K.FunApp NodeId
    "ite" [Expr Bool -> Term
    forall t. Expr t -> Term
    tr Expr Bool
    c, Expr t -> Term
    forall t. Expr t -> Term
    tr Expr t
    e1, Expr t -> Term
    forall t. Expr t -> Term
    tr Expr t
    e2]
        tr (Op1 Type t
    _ Op1 t
    op Expr t
    e) = NodeId -> [Term] -> Term
    K.FunApp (Op1 t -> NodeId
    forall a. Show a => a -> NodeId
    show Op1 t
    op) [Expr t -> Term
    forall t. Expr t -> Term
    tr Expr t
    e]
        tr (Op2 Type t
    _ Op2 a t
    op Expr a
    e1 Expr a
    e2) = NodeId -> [Term] -> Term
    K.FunApp (Op2 a t -> NodeId
    forall a. Show a => a -> NodeId
    show Op2 a t
    op) [Expr a -> Term
    forall t. Expr t -> Term
    tr Expr a
    e1, Expr a -> Term
    forall t. Expr t -> Term
    tr Expr a
    e2]
        tr (VarE Type t
    _ Var
    v) = if Bool
    primed then Var -> Term
    trPrimedVar Var
    v else Var -> Term
    trVar Var
    v