FRETComponentSpec2Copilot.hs

-- 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.
--
{-# LANGUAGE OverloadedStrings #-}

-- | Transform a FRET Component 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.FRETComponentSpec2Copilot where

-- External imports
import Data.List  ( intersect, union )
import Data.Maybe ( fromMaybe )

-- External imports: auxiliary
import Data.String.Extra ( sanitizeLCIdentifier, sanitizeUCIdentifier )

-- Internal imports: language ASTs, transformers
import qualified Language.CoCoSpec.ParCoCoSpec   as CoCoSpec ( myLexer,
                                                               pBoolSpec )
import           Language.FRETComponentSpec.AST  as FRET
import qualified Language.Trans.CoCoSpec2Copilot as CoCoSpec ( boolSpec2Copilot )
import           Language.Trans.SMV2Copilot      as SMV ( boolSpec2Copilot )

-- | Options used to customize the conversion of FRET Component Specifications
-- to Copilot code.
data FRETComponentSpec2CopilotOptions = FRETComponentSpec2CopilotOptions
  { fretCS2CopilotUseCoCoSpec :: Bool
  , fretCS2CopilotIntType     :: String
  , fretCS2CopilotRealType    :: String
  , fretCS2CopilotFilename    :: String
  }

-- | Transform a FRET TL specification into a Copilot specification.
--
-- This function may fail with a 'Left' value if the resulting Copilot
-- specification would contain name clashes or other errors.
fretComponentSpec2Copilot :: FRETComponentSpec2CopilotOptions
                          -> FRETComponentSpec
                          -> Either String String
fretComponentSpec2Copilot prefs parseResult =
  fretComponentSpec2Copilot' prefs =<< fret2CopilotAnalyze parseResult

-- | For a given FRET file, return the corresponding Copilot file, or an error
-- message if such file cannot be generated.
--
-- PRE: there are no name clashes between the variables and names used in the
-- FRET specification and any definitions in Haskell's Prelude or in Copilot.
fretComponentSpec2Copilot' :: FRETComponentSpec2CopilotOptions
                           -> FRETComponentSpec
                           -> Either String String
fretComponentSpec2Copilot' prefs fretComponentSpec =
    unlines . concat <$> sequence
      [ pure imports
      , pure externs
      , internals
      , reqs
      , pure clock
      , pure ftp
      , pure pre
      , pure tpre
      , pure spec
      , pure main'
      ]

  where

    -- Import header block
    imports :: [String]
    imports =
      [ "import           Copilot.Compile.C99"
      , "import           Copilot.Language          hiding (prop)"
      , "import           Copilot.Language.Prelude"
      , "import           Copilot.Library.LTL       (next)"
      , "import           Copilot.Library.MTL       hiding (since,"
        ++ " alwaysBeen, trigger)"
      , "import           Copilot.Library.PTLTL     (since, previous,"
        ++ " alwaysBeen)"
      , "import qualified Copilot.Library.PTLTL     as PTLTL"
      , "import qualified Copilot.Library.MTL       as MTL"
      , "import           Language.Copilot          (reify)"
      , "import           Prelude                   hiding ((&&), (||), (++),"
        ++ " (<=), (>=), (<), (>), (==), (/=), not)"
      , ""
      ]

    -- Extern streams
    externs = concatMap externVarToDecl
                        (FRET.fretExternalVariables fretComponentSpec)
      where
        externVarToDecl i = [ FRET.fretExternalVariableName i
                                ++ " :: Stream "
                                ++ "("
                                ++ fretTypeToCopilotType
                                     prefs
                                     (FRET.fretExternalVariableType i)
                                ++ ")"

                            , FRET.fretExternalVariableName i
                                ++ " = "
                                ++ "extern"
                                ++ " "
                                ++ show (FRET.fretExternalVariableName i)
                                ++ " "
                                ++ "Nothing"
                            , ""
                            ]

    -- Internal stream definitions
    internals = concat
             <$> mapM internalVarToDecl
                      (FRET.fretInternalVariables fretComponentSpec)
      where
        internalVarToDecl i = fmap (\implem ->
                                [ FRET.fretInternalVariableName i
                                    ++ " :: Stream "
                                    ++ "("
                                    ++ fretTypeToCopilotType
                                         prefs
                                         (FRET.fretInternalVariableType i)
                                    ++ ")"

                                , FRET.fretInternalVariableName i
                                    ++ " = "
                                    ++ implem

                                , ""
                                ]) implementation
          where
            implementation = if null (FRET.fretInternalVariableCopilot i)
                               then CoCoSpec.boolSpec2Copilot
                                      <$> CoCoSpec.pBoolSpec
                                            ( CoCoSpec.myLexer
                                            $ FRET.fretInternalVariableLustre i
                                            )
                               else pure (FRET.fretInternalVariableCopilot i)

    -- Encoding of requirements as boolean streams
    reqs :: Either String [String]
    reqs = concat <$> mapM reqToDecl (FRET.fretRequirements fretComponentSpec)
      where
        reqToDecl i = sequence
                        [ pure reqComment, pure reqSignature, reqBody, pure "" ]
          where
            -- Definition comment, which includes the requirement for
            -- traceability purposes.
            reqComment = "-- | "  ++ FRET.fretRequirementName i    ++ "\n" ++
                         "--   @"                                  ++ "\n" ++
                         "--   "  ++ FRET.fretRequirementFretish i ++ "\n" ++
                         "--   @"

            -- Definition type signature.
            reqSignature = FRET.fretRequirementName i
                             ++ " :: " ++ "Stream" ++ " " ++ "Bool"

            -- Definition implementation, either in SMV or in CoCoSpec
            reqBody = if fretCS2CopilotUseCoCoSpec prefs
                        then reqBodyCoCo
                        else reqBodyPT

            reqBodyPT = fmap (\e -> FRET.fretRequirementName i ++ " = "
                                      ++ SMV.boolSpec2Copilot e
                             )
                             (fromMaybe (Left $ "No requirement for " ++ show i)
                                        (FRET.fretRequirementPTExpanded i))

            reqBodyCoCo = fmap
                            (\e -> FRET.fretRequirementName i ++ " = "
                                     ++ CoCoSpec.boolSpec2Copilot e
                            )
                            (fromMaybe (Left $ "No requirement for " ++ show i)
                                       (FRET.fretRequirementCoCoSpec i))

    -- Auxiliary streams: clock
    clock :: [String]
    clock = [ ""
            , "-- | Clock that increases in one-unit steps."
            , "clock :: Stream Int64"
            , "clock = [0] ++ (clock + 1)"
            , ""
            ]

    -- Auxiliary streams: first time point
    ftp :: [String]
    ftp = [ ""
          , "-- | First Time Point"
          , "ftp :: Stream Bool"
          , "ftp = [True] ++ false"
          , ""
          ]

    -- Auxiliary streams: pre
    pre = [ ""
          , "pre :: Stream Bool -> Stream Bool"
          , "pre = ([False] ++)"
          ]

    -- Auxiliary streams: tpre
    tpre = [ ""
           , "tpre :: Stream Bool -> Stream Bool"
           , "tpre = ([True] ++)"
           ]

    -- Main specification
    spec :: [String]
    spec = [ ""
           , "-- | Complete specification. Calls the C function void "
             ++ " handler(); when"
           , "-- the property is violated."
           , "spec :: Spec"
           , "spec = do"
           ]
           ++ triggers
           ++ [ "" ]
      where
        triggers :: [String]
        triggers = fmap reqTrigger (FRET.fretRequirements fretComponentSpec)

        reqTrigger :: FRETRequirement -> String
        reqTrigger r = "  trigger " ++ show handlerName ++ " (not "
                       ++ propName ++ ") " ++ "[]"
          where
            handlerName = "handler" ++ FRET.fretRequirementName r
            propName    = FRET.fretRequirementName r

    -- Main program that compiles specification to C in two files (code and
    -- header).
    main' :: [String]
    main' = [ ""
            , "main :: IO ()"
            , "main = reify spec >>= compile \""
                 ++ fretCS2CopilotFilename prefs ++ "\""
            ]

-- | Return the corresponding type in Copilot matching a given FRET type.
fretTypeToCopilotType :: FRETComponentSpec2CopilotOptions -> String -> String
fretTypeToCopilotType _options "bool"    = "Bool"
fretTypeToCopilotType options  "int"     = fretCS2CopilotIntType options
fretTypeToCopilotType options  "integer" = fretCS2CopilotIntType options
fretTypeToCopilotType options  "real"    = fretCS2CopilotRealType options
fretTypeToCopilotType _options "string"  = "String"
fretTypeToCopilotType _options x         = x

-- | Analyze a FRET-Copilot file and determine if there will be any name
-- clashes after the conversion to Copilot.
--
-- This function does not compare against Haskell's prelude or Copilot's
-- modules. It simply makes simple conversions to comply with Copilot/Haskell's
-- grammar (e.g., variable/function names start with lowercase) and determines
-- if the conversion would make two definitions in the given specification
-- produce name clashes between them.
fret2CopilotAnalyze :: FRETComponentSpec -> Either String FRETComponentSpec
fret2CopilotAnalyze fretComponentSpec
    | not (null evnClash)
    = Left $ "Name clash detected: " ++ show evnClash

    | not (null ivnClash)
    = Left $ "Name clash detected: " ++ show ivnClash

    | not (null reqClash)
    = Left $ "Name clash detected: " ++ show reqClash

    | otherwise
    = Right $ foldr applySubstitution fretComponentSpec nameSubstitutions

  where

    -- Sets containing name clashes
    ivnClash = internalVariableNames'
                 `intersect` (externalVariableNames' `union` requirementNames')

    evnClash = externalVariableNames'
                 `intersect` (internalVariableNames' `union` requirementNames')

    reqClash = requirementNames'
                 `intersect` (internalVariableNames'
                                `union` externalVariableNames')

    -- Names used.
    internalVariableNames' = map snd internalVariableMap
    externalVariableNames' = map snd externalVariableMap
    requirementNames'      = map snd requirementNameMap

    -- Map from a variable name to its desired identifier in the code
    -- generated.
    internalVariableMap =
      map (\x -> (x, sanitizeLCIdentifier x)) internalVariableNames

    externalVariableMap =
      map (\x -> (x, sanitizeLCIdentifier x)) externalVariableNames

    requirementNameMap =
      map (\x -> (x, "prop" ++ sanitizeUCIdentifier x)) requirementNames

    nameSubstitutions = internalVariableMap
                     ++ externalVariableMap
                     ++ requirementNameMap

    -- Variable/requirement names used in the component spec.
    internalVariableNames = map fretInternalVariableName
                          $ fretInternalVariables fretComponentSpec

    externalVariableNames = map fretExternalVariableName
                          $ fretExternalVariables fretComponentSpec

    requirementNames = map fretRequirementName
                     $ fretRequirements fretComponentSpec