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