    -- 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 a Lustre specification, extended with temporal logic operators,
    -- 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.Lustre2Copilot (boolSpec2Copilot, boolSpecNames) where

    -- Internal imports
    import Language.Lustre.AbsLustre (BoolConst (..), BoolNumOp (..), BoolSpec (..),
                                      Ident (..), NumExpr (..), NumOp2In (..),
                                      Op1Pre (..), Op2In (..), Op2Pre (..))

    -- | Return the Copilot representation of a Lustre '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
      BoolSpecPar BoolSpec
    bs                 -> String
    "( " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ BoolSpec -> String
    boolSpec2Copilot BoolSpec
    bs String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " )"
      BoolSpecConstI Integer
    bc              -> Integer -> String
    forall a. Show a => a -> String
    show Integer
    bc
      BoolSpecConstD Double
    bc              -> Double -> String
    forall a. Show a => a -> String
    show Double
    bc
      BoolSpecConstB BoolConst
    bc              -> BoolConst -> String
    const2Copilot BoolConst
    bc
      BoolSpecSignal Ident
    i               -> Ident -> String
    ident2Copilot Ident
    i
      BoolSpecOp1Pre Op1Pre
    op BoolSpec
    spec         -> Op1Pre -> String
    opOnePre2Copilot Op1Pre
    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
    ")"

      BoolSpecOp2In BoolSpec
    spec1 Op2In
    Op2InPre (BoolSpecOp1Pre Op1Pre
    Op1Pre BoolSpec
    spec2)
        -> String
    "[" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ BoolSpec -> String
    lit2Copilot BoolSpec
    spec1 String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "] ++ " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ BoolSpec -> String
    boolSpec2Copilot BoolSpec
    spec2

      BoolSpecOp2In BoolSpec
    spec1 Op2In
    Op2InPre BoolSpec
    spec2
        -> String
    "mux ftp (constant " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ BoolSpec -> String
    lit2Copilot BoolSpec
    spec1 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
    ")"

      BoolSpecOp2In BoolSpec
    spec1 Op2In
    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]
    ++ Op2In -> String
    opTwoIn2Copilot Op2In
    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
    ")"

      BoolSpecOp2Pre Op2Pre
    op2 BoolSpec
    spec1 BoolSpec
    spec2 -> Op2Pre -> String
    opTwoPre2Copilot Op2Pre
    op2 String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ 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]
    ++ BoolSpec -> String
    boolSpec2Copilot BoolSpec
    spec2

      BoolSpecOp2HT  NumExpr
    num1 NumExpr
    num2 BoolSpec
    spec  -> String
    "MTL.alwaysBeen"
                                           String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ NumExpr -> String
    numExpr2Copilot NumExpr
    num2
                                           String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ NumExpr -> String
    numExpr2Copilot NumExpr
    num1
                                           String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " clock 1" -- clock and min time distance
                                           String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ BoolSpec -> String
    boolSpec2Copilot BoolSpec
    spec

      BoolSpecOp2OT  NumExpr
    num1 NumExpr
    num2 BoolSpec
    spec  -> String
    "MTL.eventuallyPrev"
                                           String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ NumExpr -> String
    numExpr2Copilot NumExpr
    num2
                                           String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ NumExpr -> String
    numExpr2Copilot NumExpr
    num1
                                           String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " clock 1" -- clock and min time distance
                                           String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ BoolSpec -> String
    boolSpec2Copilot BoolSpec
    spec

      BoolSpecOp2ST  NumExpr
    num1 NumExpr
    num2 BoolSpec
    spec1 BoolSpec
    spec2 -> String
    "MTL.since"
                                                 String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ NumExpr -> String
    numExpr2Copilot NumExpr
    num1
                                                 String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ NumExpr -> String
    numExpr2Copilot NumExpr
    num2
                                                 String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " clock 1" -- clock and min time distance
                                                 String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ 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]
    ++ BoolSpec -> String
    boolSpec2Copilot BoolSpec
    spec2

    -- | Return the Copilot representation of a Lustre numeric
    -- expression.
    --
    -- This function returns the expression only. The string does not contain any
    -- top-level names, any imports, or auxiliary definitions that may be required.
    numExpr2Copilot :: NumExpr -> String
    numExpr2Copilot :: NumExpr -> String
    numExpr2Copilot NumExpr
    expr = case NumExpr
    expr of
      NumExprNum Integer
    i                  -> Integer -> String
    forall a. Show a => a -> String
    show Integer
    i
      NumExprPar NumExpr
    iExpr              -> String
    "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ NumExpr -> String
    numExpr2Copilot NumExpr
    iExpr  String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
      NumExprOp2In NumExpr
    iExpr1 NumOp2In
    op NumExpr
    iExpr2 -> String
    "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ NumExpr -> String
    numExpr2Copilot NumExpr
    iExpr1 String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " "
                                           String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ NumOp2In -> String
    numOpTwoIn2Copilot NumOp2In
    op    String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " "
                                           String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ NumExpr -> String
    numExpr2Copilot NumExpr
    iExpr2 String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
      NumExprId Ident
    i                   -> Ident -> String
    ident2Copilot Ident
    i

    -- | Return the Copilot representation of a numeric Lustre arithmetic
    -- operator.
    numOpTwoIn2Copilot :: NumOp2In -> String
    numOpTwoIn2Copilot :: NumOp2In -> String
    numOpTwoIn2Copilot NumOp2In
    NumOp2Plus  = String
    "+"
    numOpTwoIn2Copilot NumOp2In
    NumOp2Minus = String
    "-"
    numOpTwoIn2Copilot NumOp2In
    NumOp2Mult  = String
    "*"

    -- | Return the Copilot representation of a numeric Lustre comparison
    -- operator.
    opTwoNum2Copilot :: BoolNumOp -> String
    opTwoNum2Copilot :: BoolNumOp -> String
    opTwoNum2Copilot BoolNumOp
    BoolNumOp2Eq = String
    "=="
    opTwoNum2Copilot BoolNumOp
    BoolNumOp2Ne = String
    "/="
    opTwoNum2Copilot BoolNumOp
    BoolNumOp2Le = String
    "<="
    opTwoNum2Copilot BoolNumOp
    BoolNumOp2Lt = String
    "<"
    opTwoNum2Copilot BoolNumOp
    BoolNumOp2Gt = String
    ">="
    opTwoNum2Copilot BoolNumOp
    BoolNumOp2Ge = String
    ">"

    -- | Return the Copilot representation of a Lustre boolean
    -- constant.
    const2Copilot :: BoolConst -> String
    const2Copilot :: BoolConst -> String
    const2Copilot BoolConst
    BoolConstTrue  = String
    "true"
    const2Copilot BoolConst
    BoolConstFalse = String
    "false"
    const2Copilot BoolConst
    BoolConstFTP   = String
    "ftp"

    -- | Return the Copilot representation of a Lustre logical
    -- operator.
    opOnePre2Copilot :: Op1Pre -> String
    opOnePre2Copilot :: Op1Pre -> String
    opOnePre2Copilot Op1Pre
    Op1Pre    = String
    "pre"
    opOnePre2Copilot Op1Pre
    Op1YtoPre = String
    "pre"
    opOnePre2Copilot Op1Pre
    Op1ZtoPre = String
    "tpre"
    opOnePre2Copilot Op1Pre
    Op1Once   = String
    "PTLTL.eventuallyPrev"
    opOnePre2Copilot Op1Pre
    Op1Hist   = String
    "PTLTL.alwaysBeen"
    opOnePre2Copilot Op1Pre
    Op1Y      = String
    "PTLTL.previous"
    opOnePre2Copilot Op1Pre
    Op1Not    = String
    "not"
    opOnePre2Copilot Op1Pre
    Op1Bang   = String
    "not"

    -- | Return the Copilot representation of a Lustre logical
    -- operator.
    opTwoIn2Copilot :: Op2In -> String
    opTwoIn2Copilot :: Op2In -> String
    opTwoIn2Copilot Op2In
    Op2Amp   = String
    "&&"
    opTwoIn2Copilot Op2In
    Op2And   = String
    "&&"
    opTwoIn2Copilot Op2In
    Op2Or    = String
    "||"
    opTwoIn2Copilot Op2In
    Op2Impl  = String
    "==>"
    opTwoIn2Copilot Op2In
    Op2InPre = String
    "pre"
    opTwoIn2Copilot (Op2NumOp NumOp2In
    n) = NumOp2In -> String
    numOpTwoIn2Copilot NumOp2In
    n
    opTwoIn2Copilot (Op2NumCmp BoolNumOp
    n) = BoolNumOp -> String
    opTwoNum2Copilot BoolNumOp
    n

    -- | Return the Copilot representation of a Lustre logical
    -- operator.
    opTwoPre2Copilot :: Op2Pre -> String
    opTwoPre2Copilot :: Op2Pre -> String
    opTwoPre2Copilot Op2Pre
    Op2SI = String
    "since"
    opTwoPre2Copilot Op2Pre
    Op2OT = String
    "ot"

    -- | Return the Copilot representation of a Lustre identifier.
    ident2Copilot :: Ident -> String
    ident2Copilot :: Ident -> String
    ident2Copilot (Ident String
    "FTP") = String
    "ftp"
    ident2Copilot (Ident String
    s)     = String
    s

    -- | Return all identifiers used in a BoolSpec that are not reserved keywords.
    boolSpecNames :: BoolSpec -> [String]
    boolSpecNames :: BoolSpec -> [String]
    boolSpecNames (BoolSpecPar BoolSpec
    bs)                  = BoolSpec -> [String]
    boolSpecNames BoolSpec
    bs
    boolSpecNames (BoolSpecConstI Integer
    _bc)              = []
    boolSpecNames (BoolSpecConstD Double
    _bc)              = []
    boolSpecNames (BoolSpecConstB BoolConst
    _bc)              = []
    boolSpecNames (BoolSpecSignal (Ident String
    i))        = [String
    i]
    boolSpecNames (BoolSpecOp1Pre Op1Pre
    _op BoolSpec
    spec)         = BoolSpec -> [String]
    boolSpecNames BoolSpec
    spec
    boolSpecNames (BoolSpecOp2In  BoolSpec
    spec1 Op2In
    _op2 BoolSpec
    spec2) = BoolSpec -> [String]
    boolSpecNames BoolSpec
    spec1 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ BoolSpec -> [String]
    boolSpecNames BoolSpec
    spec2
    boolSpecNames (BoolSpecOp2Pre Op2Pre
    _op2 BoolSpec
    spec1 BoolSpec
    spec2) = BoolSpec -> [String]
    boolSpecNames BoolSpec
    spec1 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ BoolSpec -> [String]
    boolSpecNames BoolSpec
    spec2
    boolSpecNames (BoolSpecOp2HT  NumExpr
    num1 NumExpr
    num2 BoolSpec
    spec)   =
      NumExpr -> [String]
    numExprNames NumExpr
    num1 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ NumExpr -> [String]
    numExprNames NumExpr
    num2 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ BoolSpec -> [String]
    boolSpecNames BoolSpec
    spec
    boolSpecNames (BoolSpecOp2OT  NumExpr
    num1 NumExpr
    num2 BoolSpec
    spec)   =
      NumExpr -> [String]
    numExprNames NumExpr
    num1 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ NumExpr -> [String]
    numExprNames NumExpr
    num2 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ BoolSpec -> [String]
    boolSpecNames BoolSpec
    spec
    boolSpecNames (BoolSpecOp2ST  NumExpr
    num1 NumExpr
    num2 BoolSpec
    spec1 BoolSpec
    spec2)   =
      NumExpr -> [String]
    numExprNames NumExpr
    num1 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ NumExpr -> [String]
    numExprNames NumExpr
    num2 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ BoolSpec -> [String]
    boolSpecNames BoolSpec
    spec1 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ BoolSpec -> [String]
    boolSpecNames BoolSpec
    spec2

    -- | Return all identifiers used in a NumExpr that are not reserved keywords.
    numExprNames :: NumExpr -> [String]
    numExprNames :: NumExpr -> [String]
    numExprNames (NumExprNum Integer
    _i)                = []
    numExprNames (NumExprPar NumExpr
    expr)              = NumExpr -> [String]
    numExprNames NumExpr
    expr
    numExprNames (NumExprOp2In NumExpr
    expr1 NumOp2In
    _op NumExpr
    expr2) =
      NumExpr -> [String]
    numExprNames NumExpr
    expr1 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ NumExpr -> [String]
    numExprNames NumExpr
    expr2
    numExprNames (NumExprId (Ident String
    i))          = [String
    i]

    -- | Return the Copilot representation of a Lustre literal.
    lit2Copilot :: BoolSpec -> String
    lit2Copilot :: BoolSpec -> String
    lit2Copilot BoolSpec
    b = case BoolSpec
    b of
        BoolSpecConstI Integer
    bc -> Integer -> String
    forall a. Show a => a -> String
    show Integer
    bc
        BoolSpecConstD Double
    bc -> Double -> String
    forall a. Show a => a -> String
    show Double
    bc
        BoolSpecConstB BoolConst
    bc -> BoolConst -> String
    litConst2Copilot BoolConst
    bc
        BoolSpecSignal Ident
    i  -> Ident -> String
    ident2Copilot Ident
    i
        BoolSpec
    _                 -> String
    ":error converting literal:"
      where
        -- | Return the Copilot representation of a Lustre boolean
        -- constant.
        litConst2Copilot :: BoolConst -> String
        litConst2Copilot :: BoolConst -> String
    litConst2Copilot BoolConst
    BoolConstTrue  = String
    "True"
        litConst2Copilot BoolConst
    BoolConstFalse = String
    "False"
        litConst2Copilot BoolConst
    _              = String
    ":error converting literal boolean:"