    -- Copyright 2020 United States Government as represented by the Administrator
    -- of the National Aeronautics and Space Administration. All Rights Reserved.
    --
    -- Disclaimers
    --
    -- Licensed under the Apache License, Version 2.0 (the "License"); you may
    -- not use this file except in compliance with the License. You may obtain a
    -- copy of the License at
    --
    --      https://www.apache.org/licenses/LICENSE-2.0
    --
    -- Unless required by applicable law or agreed to in writing, software
    -- distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
    -- WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
    -- License for the specific language governing permissions and limitations
    -- under the License.
    --

    -- | 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