-- Copyright 2020 United States Government as represented by the Administrator
-- of the National Aeronautics and Space Administration. All Rights Reserved.
--
-- Disclaimers
--
-- No Warranty: THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY
-- OF ANY KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
-- LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
-- SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A
-- PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT THE
-- SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT DOCUMENTATION, IF
-- PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE. THIS AGREEMENT DOES NOT, IN
-- ANY MANNER, CONSTITUTE AN ENDORSEMENT BY GOVERNMENT AGENCY OR ANY PRIOR
-- RECIPIENT OF ANY RESULTS, RESULTING DESIGNS, HARDWARE, SOFTWARE PRODUCTS OR
-- ANY OTHER APPLICATIONS RESULTING FROM USE OF THE SUBJECT SOFTWARE. FURTHER,
-- GOVERNMENT AGENCY DISCLAIMS ALL WARRANTIES AND LIABILITIES REGARDING
-- THIRD-PARTY SOFTWARE, IF PRESENT IN THE ORIGINAL SOFTWARE, AND DISTRIBUTES
-- IT "AS IS."
--
-- Waiver and Indemnity: RECIPIENT AGREES TO WAIVE ANY AND ALL CLAIMS AGAINST
-- THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS
-- ANY PRIOR RECIPIENT. IF RECIPIENT'S USE OF THE SUBJECT SOFTWARE RESULTS IN
-- ANY LIABILITIES, DEMANDS, DAMAGES, EXPENSES OR LOSSES ARISING FROM SUCH USE,
-- INCLUDING ANY DAMAGES FROM PRODUCTS BASED ON, OR RESULTING FROM, RECIPIENT'S
-- USE OF THE SUBJECT SOFTWARE, RECIPIENT SHALL INDEMNIFY AND HOLD HARMLESS THE
-- UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS ANY
-- PRIOR RECIPIENT, TO THE EXTENT PERMITTED BY LAW. RECIPIENT'S SOLE REMEDY
-- FOR ANY SUCH MATTER SHALL BE THE IMMEDIATE, UNILATERAL TERMINATION OF THIS
-- AGREEMENT.
--

-- | Transform an SMV TL specification into a Copilot specification.
--
-- Normally, this module would be implemented as a conversion between ASTs,
-- but we want to add comments to the generated code, which are not
-- representable in the abstract syntax tree.
module Language.Trans.SMV2Copilot where

import Language.SMV.AbsSMV (AdditiveOp (..), BoolConst (..), BoolSpec (..),
                            Ident (..), MultOp (..), NumExpr (..), Number (..),
                            Op1Name (..), OpOne (..), OpTwo (..), OrdOp (..))

-- | Return the Copilot representation of an SMV BoolSpec.
--
-- This function returns the temporal property only. The string does not
-- contain any top-level names, any imports, or auxiliary definitions that may
-- be required.
boolSpec2Copilot :: BoolSpec -> String
boolSpec2Copilot :: BoolSpec -> String
boolSpec2Copilot BoolSpec
b = case BoolSpec
b of
  BoolSpecConst BoolConst
bc -> BoolConst -> String
const2Copilot BoolConst
bc

  BoolSpecNum NumExpr
nc -> NumExpr -> String
numExpr2Copilot NumExpr
nc

  BoolSpecSignal Ident
i -> Ident -> String
ident2Copilot Ident
i

  BoolSpecCmp BoolSpec
spec1 OrdOp
op2 BoolSpec
spec2 -> String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ BoolSpec -> String
boolSpec2Copilot BoolSpec
spec1
                              String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ OrdOp -> String
ordOp2Copilot OrdOp
op2
                              String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ BoolSpec -> String
boolSpec2Copilot BoolSpec
spec2
                              String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

  BoolSpecNeg BoolSpec
spec -> String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"not"
                   String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ BoolSpec -> String
boolSpec2Copilot BoolSpec
spec
                   String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

  BoolSpecAnd BoolSpec
spec1 BoolSpec
spec2 -> String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ BoolSpec -> String
boolSpec2Copilot BoolSpec
spec1
                          String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"&&"
                          String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ BoolSpec -> String
boolSpec2Copilot BoolSpec
spec2
                          String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

  BoolSpecOr BoolSpec
spec1 BoolSpec
spec2 -> String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ BoolSpec -> String
boolSpec2Copilot BoolSpec
spec1
                         String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"||"
                         String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ BoolSpec -> String
boolSpec2Copilot BoolSpec
spec2
                         String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

  BoolSpecXor BoolSpec
spec1 BoolSpec
spec2 -> String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ BoolSpec -> String
boolSpec2Copilot BoolSpec
spec1
                          String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"`xor`"
                          String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ BoolSpec -> String
boolSpec2Copilot BoolSpec
spec2
                          String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

  BoolSpecImplies BoolSpec
spec1 BoolSpec
spec2 -> String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ BoolSpec -> String
boolSpec2Copilot BoolSpec
spec1
                              String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"==>"
                              String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ BoolSpec -> String
boolSpec2Copilot BoolSpec
spec2
                              String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

  BoolSpecEquivs BoolSpec
spec1 BoolSpec
spec2 -> String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ BoolSpec -> String
boolSpec2Copilot BoolSpec
spec1
                             String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"=="
                             String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ BoolSpec -> String
boolSpec2Copilot BoolSpec
spec2
                             String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

  BoolSpecOp1 OpOne
op BoolSpec
spec -> String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ OpOne -> String
opOne2Copilot OpOne
op
                      String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ BoolSpec -> String
boolSpec2Copilot BoolSpec
spec
                      String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

  BoolSpecOp2 BoolSpec
spec1 OpTwo
op2 BoolSpec
spec2 -> String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ BoolSpec -> String
boolSpec2Copilot BoolSpec
spec1
                              String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ OpTwo -> String
opTwo2Copilot OpTwo
op2
                              String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ BoolSpec -> String
boolSpec2Copilot BoolSpec
spec2
                              String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

-- | Return the Copilot representation of an SMV boolean constant.
const2Copilot :: BoolConst -> String
const2Copilot :: BoolConst -> String
const2Copilot BoolConst
BoolConstTrue  = String
"true"
const2Copilot BoolConst
BoolConstFalse = String
"false"
const2Copilot BoolConst
BoolConstFTP   = String
"ftp"
const2Copilot BoolConst
BoolConstLAST  = String
"last"

-- | Return the Copilot representation of a numeric expression.
numExpr2Copilot :: NumExpr -> String
numExpr2Copilot :: NumExpr -> String
numExpr2Copilot (NumId Ident
i)        = Ident -> String
ident2Copilot Ident
i
numExpr2Copilot (NumConstI Integer
i)    = Integer -> String
forall a. Show a => a -> String
show Integer
i
numExpr2Copilot (NumConstD Double
i)    = Double -> String
forall a. Show a => a -> String
show Double
i
numExpr2Copilot (NumAdd NumExpr
x AdditiveOp
op NumExpr
y)  = String
"("
                                   String -> String -> String
forall a. [a] -> [a] -> [a]
++ NumExpr -> String
numExpr2Copilot NumExpr
x
                                   String -> String -> String
forall a. [a] -> [a] -> [a]
++ AdditiveOp -> String
additiveOp2Copilot AdditiveOp
op
                                   String -> String -> String
forall a. [a] -> [a] -> [a]
++ NumExpr -> String
numExpr2Copilot NumExpr
y
                                   String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
numExpr2Copilot (NumMult NumExpr
x MultOp
op NumExpr
y) = String
"("
                                   String -> String -> String
forall a. [a] -> [a] -> [a]
++ NumExpr -> String
numExpr2Copilot NumExpr
x
                                   String -> String -> String
forall a. [a] -> [a] -> [a]
++ MultOp -> String
multOp2Copilot MultOp
op
                                   String -> String -> String
forall a. [a] -> [a] -> [a]
++ NumExpr -> String
numExpr2Copilot NumExpr
y
                                   String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

-- | Return the Copilot representation of an SMV additive operator.
additiveOp2Copilot :: AdditiveOp -> String
additiveOp2Copilot :: AdditiveOp -> String
additiveOp2Copilot AdditiveOp
OpPlus  = String
"+"
additiveOp2Copilot AdditiveOp
OpMinus = String
"-"

-- | Return the Copilot representation of an SMV multiplicative operator.
multOp2Copilot :: MultOp -> String
multOp2Copilot :: MultOp -> String
multOp2Copilot MultOp
OpTimes = String
"*"
multOp2Copilot MultOp
OpDiv   = String
"/"

-- | Return the Copilot representation of an SMV comparison operator.
ordOp2Copilot :: OrdOp -> String
ordOp2Copilot :: OrdOp -> String
ordOp2Copilot OrdOp
OrdOpLT = String
"<"
ordOp2Copilot OrdOp
OrdOpLE = String
"<="
ordOp2Copilot OrdOp
OrdOpEQ = String
"=="
ordOp2Copilot OrdOp
OrdOpNE = String
"/="
ordOp2Copilot OrdOp
OrdOpGT = String
">"
ordOp2Copilot OrdOp
OrdOpGE = String
">="

-- | Return the Copilot representation of a unary logical SMV operator.
opOne2Copilot :: OpOne -> String
opOne2Copilot :: OpOne -> String
opOne2Copilot (Op1Alone Op1Name
x)    = Op1Name -> String
opOneAlone2Copilot Op1Name
x
opOne2Copilot (Op1MTL Op1Name
x OrdOp
op Number
v) = Op1Name -> OrdOp -> Number -> String
opOneMTL2Copilot Op1Name
x OrdOp
op Number
v
opOne2Copilot (Op1MTLRange Op1Name
op Number
mn Number
mx) = Op1Name -> Number -> Number -> String
opOneMTLRange2Copilot Op1Name
op Number
mn Number
mx

-- | Return the Copilot representation of a unary logical non-MTL SMV
-- operator.
opOneAlone2Copilot :: Op1Name -> String
opOneAlone2Copilot :: Op1Name -> String
opOneAlone2Copilot Op1Name
Op1Pre  = String
"pre"
opOneAlone2Copilot Op1Name
Op1X    = String
"next"
opOneAlone2Copilot Op1Name
Op1G    = String
"always"
opOneAlone2Copilot Op1Name
Op1F    = String
"eventually"
opOneAlone2Copilot Op1Name
Op1Y    = String
"PTLTL.previous"
opOneAlone2Copilot Op1Name
Op1Z    = String
"notPreviousNot"
opOneAlone2Copilot Op1Name
Op1Hist = String
"PTLTL.alwaysBeen"
opOneAlone2Copilot Op1Name
Op1O    = String
"PTLTL.eventuallyPrev"

-- | Return the Copilot representation of a unary logical MTL SMV operator.
opOneMTL2Copilot :: Op1Name -> OrdOp -> Number -> String
opOneMTL2Copilot :: Op1Name -> OrdOp -> Number -> String
opOneMTL2Copilot Op1Name
operator OrdOp
_comparison Number
number =
  Op1Name -> String
opOneMTL2Copilot' Op1Name
operator String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Int
0 :: Int)
                             String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Number -> String
number2Copilot Number
number
                             String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"clock" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" "
                             String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Int
1 :: Int)

-- | Return the Copilot representation of a unary logical MTL SMV operator
-- that uses an explicit range.
opOneMTLRange2Copilot :: Op1Name -> Number -> Number -> String
opOneMTLRange2Copilot :: Op1Name -> Number -> Number -> String
opOneMTLRange2Copilot Op1Name
operator Number
mn Number
mx =
  Op1Name -> String
opOneMTL2Copilot' Op1Name
operator String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Number -> String
number2Copilot Number
mn
                             String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Number -> String
number2Copilot Number
mx
                             String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"clock" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" "
                             String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Int
1 :: Int)

-- | Return the Copilot representation of a unary logical possibly MTL SMV
-- operator.
opOneMTL2Copilot' :: Op1Name -> String
opOneMTL2Copilot' :: Op1Name -> String
opOneMTL2Copilot' Op1Name
Op1Pre  = String
"pre"
opOneMTL2Copilot' Op1Name
Op1X    = String
"next"
opOneMTL2Copilot' Op1Name
Op1G    = String
"always"
opOneMTL2Copilot' Op1Name
Op1F    = String
"eventually"
opOneMTL2Copilot' Op1Name
Op1Y    = String
"MTL.previous"
opOneMTL2Copilot' Op1Name
Op1Z    = String
"notPreviousNot"
opOneMTL2Copilot' Op1Name
Op1Hist = String
"MTL.alwaysBeen"
opOneMTL2Copilot' Op1Name
Op1O    = String
"MTL.eventuallyPrev"

-- | Return the Copilot representation of an SMV number.
number2Copilot :: Number -> String
number2Copilot :: Number -> String
number2Copilot (NumberInt Integer
n) = Integer -> String
forall a. Show a => a -> String
show Integer
n

-- | Return the Copilot representation of a binary logical non-MTL SMV
-- operator.
opTwo2Copilot :: OpTwo -> String
opTwo2Copilot :: OpTwo -> String
opTwo2Copilot OpTwo
Op2S = String
"`since`"
opTwo2Copilot OpTwo
Op2T = String
"`triggers`"
opTwo2Copilot OpTwo
Op2V = String
"`releases`"
opTwo2Copilot OpTwo
Op2U = String
"`until`"

-- | Return the Copilot representation of an SMV identifier.
ident2Copilot :: Ident -> String
ident2Copilot :: Ident -> String
ident2Copilot (Ident String
i) = String
i

-- | Return all identifiers used in a BoolSpec that are not reserved keywords.
boolSpecNames :: BoolSpec -> [String]
boolSpecNames :: BoolSpec -> [String]
boolSpecNames BoolSpec
b = case BoolSpec
b of
  BoolSpecConst BoolConst
_bc            -> []
  BoolSpecSignal (Ident String
i)     -> [String
i]
  BoolSpecNum NumExpr
e                -> NumExpr -> [String]
numExprNames NumExpr
e
  BoolSpecCmp BoolSpec
spec1 OrdOp
_op2 BoolSpec
spec2 -> BoolSpec -> [String]
boolSpecNames BoolSpec
spec1 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ BoolSpec -> [String]
boolSpecNames BoolSpec
spec2
  BoolSpecNeg BoolSpec
spec             -> BoolSpec -> [String]
boolSpecNames BoolSpec
spec
  BoolSpecAnd BoolSpec
spec1 BoolSpec
spec2      -> BoolSpec -> [String]
boolSpecNames BoolSpec
spec1 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ BoolSpec -> [String]
boolSpecNames BoolSpec
spec2
  BoolSpecOr  BoolSpec
spec1 BoolSpec
spec2      -> BoolSpec -> [String]
boolSpecNames BoolSpec
spec1 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ BoolSpec -> [String]
boolSpecNames BoolSpec
spec2
  BoolSpecXor BoolSpec
spec1 BoolSpec
spec2      -> BoolSpec -> [String]
boolSpecNames BoolSpec
spec1 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ BoolSpec -> [String]
boolSpecNames BoolSpec
spec2
  BoolSpecImplies BoolSpec
spec1 BoolSpec
spec2  -> BoolSpec -> [String]
boolSpecNames BoolSpec
spec1 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ BoolSpec -> [String]
boolSpecNames BoolSpec
spec2
  BoolSpecEquivs BoolSpec
spec1 BoolSpec
spec2   -> BoolSpec -> [String]
boolSpecNames BoolSpec
spec1 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ BoolSpec -> [String]
boolSpecNames BoolSpec
spec2
  BoolSpecOp1 OpOne
_op BoolSpec
spec         -> BoolSpec -> [String]
boolSpecNames BoolSpec
spec
  BoolSpecOp2 BoolSpec
spec1 OpTwo
_op2 BoolSpec
spec2 -> BoolSpec -> [String]
boolSpecNames BoolSpec
spec1 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ BoolSpec -> [String]
boolSpecNames BoolSpec
spec2

-- | Return all identifiers used in a numeric expression.
numExprNames :: NumExpr -> [String]
numExprNames :: NumExpr -> [String]
numExprNames NumExpr
numExpr = case NumExpr
numExpr of
  NumId (Ident String
i)         -> [String
i]
  NumConstI Integer
_c            -> []
  NumConstD Double
_c            -> []
  NumAdd NumExpr
expr1 AdditiveOp
_op NumExpr
expr2  -> NumExpr -> [String]
numExprNames NumExpr
expr1 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ NumExpr -> [String]
numExprNames NumExpr
expr2
  NumMult NumExpr
expr1 MultOp
_op NumExpr
expr2 -> NumExpr -> [String]
numExprNames NumExpr
expr1 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ NumExpr -> [String]
numExprNames NumExpr
expr2