{-# LANGUAGE GADTs #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE ViewPatterns #-}
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
type DepGraph = Map NodeId [NodeId]
data Style = Inlined | Modular
toKind2 :: Style
-> [PropId]
-> [PropId]
-> TransSys
-> 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
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 = 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 = forall a b. (a -> b) -> [a] -> [b]
map (NodeId, ExtVar) -> Prop
trProp forall a b. (a -> b) -> a -> b
$
forall a. (a -> Bool) -> [a] -> [a]
filter ((forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [NodeId]
checkedProps) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) forall a b. (a -> b) -> a -> b
$
forall k a. Map k a -> [(k, a)]
Map.toList (TransSys -> Map NodeId ExtVar
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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtVar -> Var
extVarLocalPart 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 forall a b. (a -> b) -> a -> b
$ Node -> [Term]
initLocals Node
node
forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (forall t. Bool -> Expr t -> Term
trExpr Bool
False) (Node -> [Expr Bool]
nodeConstrs Node
node)
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 forall a b. (a -> b) -> a -> b
$ Node -> [Term]
transLocals Node
node
forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (forall t. Bool -> Expr t -> Term
trExpr Bool
True) (Node -> [Expr Bool]
nodeConstrs Node
node)
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 :: File -> [PredDef]
filePreds :: [PredDef]
K.filePreds, [Prop]
fileProps :: File -> [Prop]
fileProps :: [Prop]
K.fileProps}) =
[PredDef] -> [Prop] -> File
K.File (forall {a}. (a -> a) -> [a] -> [a]
changeTail PredDef -> PredDef
aux [PredDef]
filePreds) [Prop]
fileProps
where
changeTail :: (a -> a) -> [a] -> [a]
changeTail a -> a
f (forall a. [a] -> [a]
reverse -> [a]
l) = case [a]
l of
[] -> forall a. HasCallStack => NodeId -> a
error NodeId
"impossible"
a
x : [a]
xs -> forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ a -> a
f a
x 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 forall a. a -> [a] -> [a]
: 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 forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map NodeId -> Term
K.PrimedStateVar [NodeId]
vars )
in PredDef
pred { predInit :: Term
K.predInit = Term
init', predTrans :: Term
K.predTrans = Term
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 = forall a. HasCallStack => Maybe a -> a
fromJust forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup NodeId
a (TransSys -> Map NodeId ExtVar
specProps TransSys
spec)
toTopVar :: ExtVar -> Var
toTopVar (ExtVar NodeId
nId Var
v) = forall a. HasCallStack => Bool -> a -> a
assert (NodeId
nId forall a. Eq a => a -> a -> Bool
== TransSys -> NodeId
specTopNodeId TransSys
spec) Var
v
in forall a b. (a -> b) -> [a] -> [b]
map (Var -> NodeId
varName forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtVar -> Var
toTopVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. NodeId -> ExtVar
toExtVar) [NodeId]
assumptions
gatherPredStateVars :: TransSys -> Node -> [K.StateVarDef]
gatherPredStateVars :: TransSys -> Node -> [StateVarDef]
gatherPredStateVars TransSys
spec Node
node = [StateVarDef]
locals forall a. [a] -> [a] -> [a]
++ [StateVarDef]
imported
where
nodesMap :: Map NodeId Node
nodesMap = 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 forall k a. Ord k => Map k a -> k -> a
! NodeId
n) 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 =
forall a b. (a -> b) -> [a] -> [b]
map (\Var
v -> NodeId -> Type -> [StateVarFlag] -> StateVarDef
K.StateVarDef (Var -> NodeId
varName Var
v)
(ExtVar -> Type
extVarType forall a b. (a -> b) -> a -> b
$ NodeId -> Var -> ExtVar
ExtVar (Node -> NodeId
nodeId Node
node) Var
v) [])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> [a]
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [k]
Map.keys forall a b. (a -> b) -> a -> b
$ Node -> Map Var VarDescr
nodeLocalVars Node
node
imported :: [StateVarDef]
imported =
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) [])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b. (a, b) -> b
snd) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. Bimap a b -> [(a, b)]
Bimap.toList forall a b. (a -> b) -> a -> b
$ Node -> Bimap Var ExtVar
nodeImportedVars Node
node
mkConj :: [K.Term] -> K.Term
mkConj :: [Term] -> Term
mkConj [] = 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 (forall a. Show a => a -> NodeId
show t
v)
trConst Type t
Real t
v = NodeId -> Term
K.ValueLiteral (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 =
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Var, VarDescr) -> [Term]
f (forall k a. Map k a -> [(k, a)]
Map.toList 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) (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) (forall t. Bool -> Expr t -> Term
trExpr Bool
False Expr t
e)]
Constrs [Expr Bool]
cs -> forall a b. (a -> b) -> [a] -> [b]
map (forall t. Bool -> Expr t -> Term
trExpr Bool
False) [Expr Bool]
cs
transLocals :: Node -> [K.Term]
transLocals :: Node -> [Term]
transLocals Node
node =
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Var, VarDescr) -> [Term]
f (forall k a. Map k a -> [(k, a)]
Map.toList 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) (forall t. Bool -> Expr t -> Term
trExpr Bool
True Expr t
e)]
Constrs [Expr Bool]
cs -> forall a b. (a -> b) -> [a] -> [b]
map (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 =
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 forall k a. Ord k => Map k a -> k -> a
! NodeId
nid
nodesMap :: Map NodeId Node
nodesMap = 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 =
forall a b. (a -> b) -> [a] -> [b]
map (NodeId -> Var -> ExtVar
ExtVar NodeId
n) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> [a]
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [k]
Map.keys
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Node -> Map Var VarDescr
nodeLocalVars forall a b. (a -> b) -> a -> b
$ (Map NodeId Node
nodesMap 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 forall a. [a] -> [a] -> [a]
++ (Var -> Term) -> [Term]
argsSeq Var -> Term
trPrimedVar)
where
calleeLocals :: [ExtVar]
calleeLocals = NodeId -> [ExtVar]
nodeLocals NodeId
callee
calleeImported :: [ExtVar]
calleeImported =
(forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap NodeId -> [ExtVar]
nodeLocals forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> [a]
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Node -> [NodeId]
nodeDependencies) forall a b. (a -> b) -> a -> b
$ Map NodeId Node
nodesMap forall k a. Ord k => Map k a -> k -> a
! NodeId
callee
localAlias :: (Var -> Term) -> ExtVar -> Term
localAlias Var -> Term
trVarF ExtVar
ev =
case forall a b (m :: * -> *).
(Ord a, Ord b, MonadThrow m) =>
b -> Bimap a b -> m a
Bimap.lookupR ExtVar
ev forall a b. (a -> b) -> a -> b
$ Node -> Bimap Var ExtVar
nodeImportedVars Node
node of
Maybe Var
Nothing -> forall a. HasCallStack => NodeId -> a
error forall a b. (a -> b) -> a -> b
$
NodeId
"This spec is not complete : "
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> NodeId
show ExtVar
ev forall a. [a] -> [a] -> [a]
++ NodeId
" should be imported in " forall a. [a] -> [a] -> [a]
++ NodeId
nid
Just Var
v -> Var -> Term
trVarF Var
v
argsSeq :: (Var -> Term) -> [Term]
argsSeq Var -> Term
trVarF =
forall a b. (a -> b) -> [a] -> [b]
map ((Var -> Term) -> ExtVar -> Term
localAlias Var -> Term
trVarF) ([ExtVar]
calleeLocals forall a. [a] -> [a] -> [a]
++ [ExtVar]
calleeImported)
trExpr :: Bool -> Expr t -> K.Term
trExpr :: forall t. Bool -> Expr t -> Term
trExpr Bool
primed = 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) = 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" [forall t. Expr t -> Term
tr Expr Bool
c, forall t. Expr t -> Term
tr Expr t
e1, forall t. Expr t -> Term
tr Expr t
e2]
tr (Op1 Type t
_ Op1 t
op Expr t
e) = NodeId -> [Term] -> Term
K.FunApp (forall a. Show a => a -> NodeId
show Op1 t
op) [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 (forall a. Show a => a -> NodeId
show Op2 a t
op) [forall t. Expr t -> Term
tr Expr a
e1, 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