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

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

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]

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

data Style = Inlined | Modular

toKind2 :: Style -> [PropId] -> [PropId] -> TransSys -> K.File
toKind2 :: Style -> [PropId] -> [PropId] -> TransSys -> File
toKind2 Style
style [PropId]
assumptions [PropId]
checkedProps TransSys
spec =
  TransSys -> [PropId] -> File -> File
addAssumptions TransSys
spec [PropId]
assumptions
  (File -> File) -> File -> File
forall a b. (a -> b) -> a -> b
$ TransSys -> DepGraph -> [PropId] -> [PropId] -> File
trSpec (TransSys -> TransSys
complete TransSys
spec') DepGraph
predCallsGraph [PropId]
assumptions [PropId]
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 -> [PropId] -> [PropId] -> File
trSpec TransSys
spec DepGraph
predCallsGraph [PropId]
_assumptions [PropId]
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 = ((PropId, ExtVar) -> Prop) -> [(PropId, ExtVar)] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map (PropId, ExtVar) -> Prop
trProp ([(PropId, ExtVar)] -> [Prop]) -> [(PropId, ExtVar)] -> [Prop]
forall a b. (a -> b) -> a -> b
$
          ((PropId, ExtVar) -> Bool)
-> [(PropId, ExtVar)] -> [(PropId, ExtVar)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((PropId -> [PropId] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [PropId]
checkedProps) (PropId -> Bool)
-> ((PropId, ExtVar) -> PropId) -> (PropId, ExtVar) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PropId, ExtVar) -> PropId
forall a b. (a, b) -> a
fst) ([(PropId, ExtVar)] -> [(PropId, ExtVar)])
-> [(PropId, ExtVar)] -> [(PropId, ExtVar)]
forall a b. (a -> b) -> a -> b
$
          Map PropId ExtVar -> [(PropId, ExtVar)]
forall k a. Map k a -> [(k, a)]
Map.toList (TransSys -> Map PropId ExtVar
specProps TransSys
spec)

trProp :: (PropId, ExtVar) -> K.Prop
trProp :: (PropId, ExtVar) -> Prop
trProp (PropId
pId, ExtVar
var) = PropId -> Term -> Prop
K.Prop PropId
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 =
  PredDef :: PropId -> [StateVarDef] -> Term -> Term -> PredDef
K.PredDef { PropId
predId :: PropId
predId :: PropId
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 :: PropId
predId = Node -> PropId
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 -> [PropId] -> File -> File
addAssumptions TransSys
spec [PropId]
assumptions (K.File {[PredDef]
filePreds :: File -> [PredDef]
filePreds :: [PredDef]
K.filePreds, [Prop]
fileProps :: File -> [Prop]
fileProps :: [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
      []     -> PropId -> [a]
forall a. HasCallStack => PropId -> a
error PropId
"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]
: (PropId -> Term) -> [PropId] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map PropId -> Term
K.StateVar [PropId]
vars )
          trans' :: Term
trans' = [Term] -> Term
mkConj ( PredDef -> Term
K.predTrans PredDef
pred Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: (PropId -> Term) -> [PropId] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map PropId -> Term
K.PrimedStateVar [PropId]
vars )
      in PredDef
pred { predInit :: Term
K.predInit = Term
init', predTrans :: Term
K.predTrans = Term
trans' }

    vars :: [PropId]
vars =
      let bindings :: Bimap Var ExtVar
bindings   = Node -> Bimap Var ExtVar
nodeImportedVars (TransSys -> Node
specTopNode TransSys
spec)
          toExtVar :: PropId -> ExtVar
toExtVar PropId
a = Maybe ExtVar -> ExtVar
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe ExtVar -> ExtVar) -> Maybe ExtVar -> ExtVar
forall a b. (a -> b) -> a -> b
$ PropId -> Map PropId ExtVar -> Maybe ExtVar
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup PropId
a (TransSys -> Map PropId ExtVar
specProps TransSys
spec)
          toTopVar :: ExtVar -> Var
toTopVar (ExtVar PropId
nId Var
v) = Bool -> Var -> Var
forall a. HasCallStack => Bool -> a -> a
assert (PropId
nId PropId -> PropId -> Bool
forall a. Eq a => a -> a -> Bool
== TransSys -> PropId
specTopNodeId TransSys
spec) Var
v
      in (PropId -> PropId) -> [PropId] -> [PropId]
forall a b. (a -> b) -> [a] -> [b]
map (Var -> PropId
varName (Var -> PropId) -> (PropId -> Var) -> PropId -> PropId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtVar -> Var
toTopVar (ExtVar -> Var) -> (PropId -> ExtVar) -> PropId -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PropId -> ExtVar
toExtVar) [PropId]
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 PropId Node
nodesMap = [(PropId, Node)] -> Map PropId Node
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Node -> PropId
nodeId Node
n, Node
n) | Node
n <- TransSys -> [Node]
specNodes TransSys
spec]
    extVarType :: ExtVar -> K.Type
    extVarType :: ExtVar -> Type
extVarType (ExtVar PropId
n Var
v) =
      case Node -> Map Var VarDescr
nodeLocalVars (Map PropId Node
nodesMap Map PropId Node -> PropId -> Node
forall k a. Ord k => Map k a -> k -> a
! PropId
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 -> PropId -> Type -> [StateVarFlag] -> StateVarDef
K.StateVarDef (Var -> PropId
varName Var
v)
              (ExtVar -> Type
extVarType (ExtVar -> Type) -> ExtVar -> Type
forall a b. (a -> b) -> a -> b
$ PropId -> Var -> ExtVar
ExtVar (Node -> PropId
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) -> PropId -> Type -> [StateVarFlag] -> StateVarDef
K.StateVarDef (Var -> PropId
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  = PropId -> [Term] -> Term
K.FunApp PropId
"and" [Term]
xs

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

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

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

trConst :: Type t -> t -> K.Term
trConst :: Type t -> t -> Term
trConst Type t
Integer t
v     = PropId -> Term
K.ValueLiteral (t -> PropId
forall a. Show a => a -> PropId
show t
v)
trConst Type t
Real    t
v     = PropId -> Term
K.ValueLiteral (t -> PropId
forall a. Show a => a -> PropId
show t
v)
trConst Type t
Bool    t
True  = PropId -> Term
K.ValueLiteral PropId
"true"
trConst Type t
Bool    t
False = PropId -> Term
K.ValueLiteral PropId
"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 =
  (PropId -> Term) -> [PropId] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map PropId -> Term
mkCall [PropId]
toCall
  where
    nid :: PropId
nid = Node -> PropId
nodeId Node
node
    toCall :: [PropId]
toCall = DepGraph
predCallsGraph DepGraph -> PropId -> [PropId]
forall k a. Ord k => Map k a -> k -> a
! PropId
nid
    nodesMap :: Map PropId Node
nodesMap = [(PropId, Node)] -> Map PropId Node
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Node -> PropId
nodeId Node
n, Node
n) | Node
n <- TransSys -> [Node]
specNodes TransSys
spec]

    nodeLocals :: PropId -> [ExtVar]
nodeLocals PropId
n =
      (Var -> ExtVar) -> [Var] -> [ExtVar]
forall a b. (a -> b) -> [a] -> [b]
map (PropId -> Var -> ExtVar
ExtVar PropId
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 PropId Node
nodesMap Map PropId Node -> PropId -> Node
forall k a. Ord k => Map k a -> k -> a
! PropId
n)

    mkCall :: PropId -> Term
mkCall PropId
callee
      | Bool
isInitCall =
          PropId -> PredType -> [Term] -> Term
K.PredApp PropId
callee PredType
K.Init ((Var -> Term) -> [Term]
argsSeq Var -> Term
trVar)
      | Bool
otherwise  =
          PropId -> PredType -> [Term] -> Term
K.PredApp PropId
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 = PropId -> [ExtVar]
nodeLocals PropId
callee
        calleeImported :: [ExtVar]
calleeImported =
          ((PropId -> [ExtVar]) -> [PropId] -> [ExtVar]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap PropId -> [ExtVar]
nodeLocals ([PropId] -> [ExtVar]) -> (Node -> [PropId]) -> Node -> [ExtVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [PropId] -> [PropId]
forall a. Ord a => [a] -> [a]
sort ([PropId] -> [PropId]) -> (Node -> [PropId]) -> Node -> [PropId]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Node -> [PropId]
nodeDependencies) (Node -> [ExtVar]) -> Node -> [ExtVar]
forall a b. (a -> b) -> a -> b
$ Map PropId Node
nodesMap Map PropId Node -> PropId -> Node
forall k a. Ord k => Map k a -> k -> a
! PropId
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 -> PropId -> Term
forall a. HasCallStack => PropId -> a
error (PropId -> Term) -> PropId -> Term
forall a b. (a -> b) -> a -> b
$
              PropId
"This spec is not complete : "
              PropId -> PropId -> PropId
forall a. [a] -> [a] -> [a]
++ ExtVar -> PropId
forall a. Show a => a -> PropId
show ExtVar
ev PropId -> PropId -> PropId
forall a. [a] -> [a] -> [a]
++ PropId
" should be imported in " PropId -> PropId -> PropId
forall a. [a] -> [a] -> [a]
++ PropId
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 :: 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 :: 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) = PropId -> [Term] -> Term
K.FunApp PropId
"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) = PropId -> [Term] -> Term
K.FunApp (Op1 t -> PropId
forall a. Show a => a -> PropId
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) = PropId -> [Term] -> Term
K.FunApp (Op2 a t -> PropId
forall a. Show a => a -> PropId
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

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