{-# LANGUAGE ScopedTypeVariables #-}
-- Copyright 2024 United States Government as represented by the Administrator
-- Copyright 2024 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 Ogma specification into a standalone 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.Spec2Copilot where

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

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

-- External imports: ogma-spec
import Data.OgmaSpec (ExternalVariableDef (..), InternalVariableDef (..),
                      Requirement (..), Spec (..))

-- | For a given spec, 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
-- specification and any definitions in Haskell's Prelude or in Copilot.
spec2Copilot :: forall a
             .  String                         -- Spec / target file name
             -> [(String, String)]             -- Type substitution table
             -> ([(String, String)] -> a -> a) -- Expr subsitution function
             -> (a -> String)                  -- Expr show function
             -> Spec a                         -- Specification
             -> Either String (String, String, String, String, String)
spec2Copilot :: forall a.
String
-> [(String, String)]
-> ([(String, String)] -> a -> a)
-> (a -> String)
-> Spec a
-> Either String (String, String, String, String, String)
spec2Copilot String
specName [(String, String)]
typeMaps [(String, String)] -> a -> a
exprTransform a -> String
showExpr Spec a
spec =
    (String, String, String, String, String)
-> Either String (String, String, String, String, String)
forall a. a -> Either String a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
externs, String
internals, String
reqs, String
triggers, String
specName)

  where

    -- Extern streams
    externs :: String
externs = [String] -> String
unlines'
            ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [String] -> [[String]] -> [String]
forall a. [a] -> [[a]] -> [a]
intercalate [String
""]
            ([[String]] -> [String]) -> [[String]] -> [String]
forall a b. (a -> b) -> a -> b
$ (ExternalVariableDef -> [String])
-> [ExternalVariableDef] -> [[String]]
forall a b. (a -> b) -> [a] -> [b]
map ExternalVariableDef -> [String]
externVarToDecl
                  (Spec a -> [ExternalVariableDef]
forall a. Spec a -> [ExternalVariableDef]
externalVariables Spec a
spec)
      where
        externVarToDecl :: ExternalVariableDef -> [String]
externVarToDecl ExternalVariableDef
i = [ String
propName
                                String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" :: Stream "
                                String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"("
                                String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(String, String)] -> String -> String
safeMap [(String, String)]
typeMaps (ExternalVariableDef -> String
externalVariableType ExternalVariableDef
i)
                                String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

                            , String
propName
                                String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" = "
                                String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"extern"
                                String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" "
                                String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show (ExternalVariableDef -> String
externalVariableName ExternalVariableDef
i)
                                String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" "
                                String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"Nothing"
                            ]
          where
            propName :: String
propName = [(String, String)] -> String -> String
safeMap [(String, String)]
nameSubstitutions (ExternalVariableDef -> String
externalVariableName ExternalVariableDef
i)

    -- Internal stream definitions
    internals :: String
internals = [String] -> String
unlines'
              ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [String] -> [[String]] -> [String]
forall a. [a] -> [[a]] -> [a]
intercalate [String
""]
              ([[String]] -> [String]) -> [[String]] -> [String]
forall a b. (a -> b) -> a -> b
$ (InternalVariableDef -> [String])
-> [InternalVariableDef] -> [[String]]
forall a b. (a -> b) -> [a] -> [b]
map InternalVariableDef -> [String]
internalVarToDecl
                    (Spec a -> [InternalVariableDef]
forall a. Spec a -> [InternalVariableDef]
internalVariables Spec a
spec)
      where
        internalVarToDecl :: InternalVariableDef -> [String]
internalVarToDecl InternalVariableDef
i = (\String
implem ->
                                [ String
propName
                                    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" :: Stream "
                                    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"("
                                    String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(String, String)] -> String -> String
safeMap [(String, String)]
typeMaps (InternalVariableDef -> String
internalVariableType InternalVariableDef
i)
                                    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

                                , String
propName
                                    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" = "
                                    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
implem
                                ]) String
implementation
          where
            propName :: String
propName = [(String, String)] -> String -> String
safeMap [(String, String)]
nameSubstitutions (InternalVariableDef -> String
internalVariableName InternalVariableDef
i)
            implementation :: String
implementation = (InternalVariableDef -> String
internalVariableExpr InternalVariableDef
i)

    -- Encoding of requirements as boolean streams
    reqs :: String
    reqs :: String
reqs = [String] -> String
unlines'
         ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [String] -> [[String]] -> [String]
forall a. [a] -> [[a]] -> [a]
intercalate [String
""]
         ([[String]] -> [String]) -> [[String]] -> [String]
forall a b. (a -> b) -> a -> b
$ (Requirement a -> [String]) -> [Requirement a] -> [[String]]
forall a b. (a -> b) -> [a] -> [b]
map Requirement a -> [String]
reqToDecl (Spec a -> [Requirement a]
forall a. Spec a -> [Requirement a]
requirements Spec a
spec)
      where
        reqToDecl :: Requirement a -> [String]
reqToDecl Requirement a
i = [ String
reqComment, String
reqSignature
                      , [(String, String)] -> String
reqBody [(String, String)]
nameSubstitutions
                      ]
          where
            reqName :: String
reqName = [(String, String)] -> String -> String
safeMap [(String, String)]
nameSubstitutions (Requirement a -> String
forall a. Requirement a -> String
requirementName Requirement a
i)

            -- Definition comment, which includes the requirement for
            -- traceability purposes.
            reqComment :: String
reqComment = String
"-- | "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ Requirement a -> String
forall a. Requirement a -> String
requirementName Requirement a
i    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                         String
"--   @"                                  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                         String
"--   "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ Requirement a -> String
forall a. Requirement a -> String
requirementDescription Requirement a
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                         String
"--   @"

            -- Definition type signature.
            reqSignature :: String
reqSignature = String
reqName
                             String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" :: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"Stream" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"Bool"

            -- Definition implementation. We use an auxiliary function to
            -- transform the implementation into Copilot, applying a
            -- substitution.
            reqBody :: [(String, String)] -> String
reqBody [(String, String)]
subs = String
reqName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" = " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                             (a -> String
showExpr ([(String, String)] -> a -> a
exprTransform [(String, String)]
subs (Requirement a -> a
forall a. Requirement a -> a
requirementExpr Requirement a
i)))


    -- Main specification triggers
    triggers :: String
    triggers :: String
triggers = [String] -> String
unlines' ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (Requirement a -> String) -> [Requirement a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Requirement a -> String
reqTrigger (Spec a -> [Requirement a]
forall a. Spec a -> [Requirement a]
requirements Spec a
spec)
      where
        reqTrigger :: Requirement a -> String
        reqTrigger :: Requirement a -> String
reqTrigger Requirement a
r = String
"  trigger " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
handlerName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" (not "
                       String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
propName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
handlerArg
          where
            handlerName :: String
handlerName = String
"handler" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
sanitizeUCIdentifier (Requirement a -> String
forall a. Requirement a -> String
requirementName Requirement a
r)
            propName :: String
propName    = [(String, String)] -> String -> String
safeMap [(String, String)]
nameSubstitutions (Requirement a -> String
forall a. Requirement a -> String
requirementName Requirement a
r)
            handlerArg :: String
handlerArg  =
              case (Requirement a -> Maybe String
forall a. Requirement a -> Maybe String
requirementResultType Requirement a
r, Requirement a -> Maybe a
forall a. Requirement a -> Maybe a
requirementResultExpr Requirement a
r) of
                (Just String
ty, Just a
ex) -> String
"[ arg (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
showExpr a
ex String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ) ]"
                (Maybe String, Maybe a)
_                  -> String
"[]"

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

    externalVariableMap :: [(String, String)]
externalVariableMap =
      (String -> (String, String)) -> [String] -> [(String, String)]
forall a b. (a -> b) -> [a] -> [b]
map (\String
x -> (String
x, String -> String
sanitizeLCIdentifier String
x)) [String]
externalVariableNames

    requirementNameMap :: [(String, String)]
requirementNameMap =
      (String -> (String, String)) -> [String] -> [(String, String)]
forall a b. (a -> b) -> [a] -> [b]
map (\String
x -> (String
x, String
"prop" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
sanitizeUCIdentifier String
x)) [String]
requirementNames

    nameSubstitutions :: [(String, String)]
nameSubstitutions = [(String, String)]
internalVariableMap
                     [(String, String)] -> [(String, String)] -> [(String, String)]
forall a. [a] -> [a] -> [a]
++ [(String, String)]
externalVariableMap
                     [(String, String)] -> [(String, String)] -> [(String, String)]
forall a. [a] -> [a] -> [a]
++ [(String, String)]
requirementNameMap

    -- Variable/requirement names used in the input spec.
    internalVariableNames :: [String]
internalVariableNames = (InternalVariableDef -> String)
-> [InternalVariableDef] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map InternalVariableDef -> String
internalVariableName
                          ([InternalVariableDef] -> [String])
-> [InternalVariableDef] -> [String]
forall a b. (a -> b) -> a -> b
$ Spec a -> [InternalVariableDef]
forall a. Spec a -> [InternalVariableDef]
internalVariables Spec a
spec

    externalVariableNames :: [String]
externalVariableNames = (ExternalVariableDef -> String)
-> [ExternalVariableDef] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ExternalVariableDef -> String
externalVariableName
                          ([ExternalVariableDef] -> [String])
-> [ExternalVariableDef] -> [String]
forall a b. (a -> b) -> a -> b
$ Spec a -> [ExternalVariableDef]
forall a. Spec a -> [ExternalVariableDef]
externalVariables Spec a
spec

    requirementNames :: [String]
requirementNames = (Requirement a -> String) -> [Requirement a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Requirement a -> String
forall a. Requirement a -> String
requirementName
                     ([Requirement a] -> [String]) -> [Requirement a] -> [String]
forall a b. (a -> b) -> a -> b
$ Spec a -> [Requirement a]
forall a. Spec a -> [Requirement a]
requirements Spec a
spec

specAnalyze :: Spec a -> Either String (Spec a)
specAnalyze :: forall a. Spec a -> Either String (Spec a)
specAnalyze Spec a
spec
    | Bool -> Bool
not ([String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
evnClash)
    = String -> Either String (Spec a)
forall a b. a -> Either a b
Left (String -> Either String (Spec a))
-> String -> Either String (Spec a)
forall a b. (a -> b) -> a -> b
$ String
"Name clash detected: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. Show a => a -> String
show [String]
evnClash

    | Bool -> Bool
not ([String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
ivnClash)
    = String -> Either String (Spec a)
forall a b. a -> Either a b
Left (String -> Either String (Spec a))
-> String -> Either String (Spec a)
forall a b. (a -> b) -> a -> b
$ String
"Name clash detected: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. Show a => a -> String
show [String]
ivnClash

    | Bool -> Bool
not ([String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
reqClash)
    = String -> Either String (Spec a)
forall a b. a -> Either a b
Left (String -> Either String (Spec a))
-> String -> Either String (Spec a)
forall a b. (a -> b) -> a -> b
$ String
"Name clash detected: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. Show a => a -> String
show [String]
reqClash

    | Bool
otherwise
    = Spec a -> Either String (Spec a)
forall a b. b -> Either a b
Right Spec a
spec

  where

    -- Sets containing name clashes
    ivnClash :: [String]
ivnClash = [String]
internalVariableNames'
                 [String] -> [String] -> [String]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` ([String]
externalVariableNames' [String] -> [String] -> [String]
forall a. Eq a => [a] -> [a] -> [a]
`union` [String]
requirementNames')

    evnClash :: [String]
evnClash = [String]
externalVariableNames'
                 [String] -> [String] -> [String]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` ([String]
internalVariableNames' [String] -> [String] -> [String]
forall a. Eq a => [a] -> [a] -> [a]
`union` [String]
requirementNames')

    reqClash :: [String]
reqClash = [String]
requirementNames'
                 [String] -> [String] -> [String]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` ([String]
internalVariableNames'
                                [String] -> [String] -> [String]
forall a. Eq a => [a] -> [a] -> [a]
`union` [String]
externalVariableNames')

    -- Names used.
    internalVariableNames' :: [String]
internalVariableNames' = ((String, String) -> String) -> [(String, String)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, String) -> String
forall a b. (a, b) -> b
snd [(String, String)]
internalVariableMap
    externalVariableNames' :: [String]
externalVariableNames' = ((String, String) -> String) -> [(String, String)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, String) -> String
forall a b. (a, b) -> b
snd [(String, String)]
externalVariableMap
    requirementNames' :: [String]
requirementNames'      = ((String, String) -> String) -> [(String, String)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, String) -> String
forall a b. (a, b) -> b
snd [(String, String)]
requirementNameMap

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

    externalVariableMap :: [(String, String)]
externalVariableMap =
      (String -> (String, String)) -> [String] -> [(String, String)]
forall a b. (a -> b) -> [a] -> [b]
map (\String
x -> (String
x, String -> String
sanitizeLCIdentifier String
x)) [String]
externalVariableNames

    requirementNameMap :: [(String, String)]
requirementNameMap =
      (String -> (String, String)) -> [String] -> [(String, String)]
forall a b. (a -> b) -> [a] -> [b]
map (\String
x -> (String
x, String
"prop" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
sanitizeUCIdentifier String
x)) [String]
requirementNames

    -- Variable/requirement names used in the input spec.
    internalVariableNames :: [String]
internalVariableNames = (InternalVariableDef -> String)
-> [InternalVariableDef] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map InternalVariableDef -> String
internalVariableName
                          ([InternalVariableDef] -> [String])
-> [InternalVariableDef] -> [String]
forall a b. (a -> b) -> a -> b
$ Spec a -> [InternalVariableDef]
forall a. Spec a -> [InternalVariableDef]
internalVariables Spec a
spec

    externalVariableNames :: [String]
externalVariableNames = (ExternalVariableDef -> String)
-> [ExternalVariableDef] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ExternalVariableDef -> String
externalVariableName
                          ([ExternalVariableDef] -> [String])
-> [ExternalVariableDef] -> [String]
forall a b. (a -> b) -> a -> b
$ Spec a -> [ExternalVariableDef]
forall a. Spec a -> [ExternalVariableDef]
externalVariables Spec a
spec

    requirementNames :: [String]
requirementNames = (Requirement a -> String) -> [Requirement a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Requirement a -> String
forall a. Requirement a -> String
requirementName
                     ([Requirement a] -> [String]) -> [Requirement a] -> [String]
forall a b. (a -> b) -> a -> b
$ Spec a -> [Requirement a]
forall a. Spec a -> [Requirement a]
requirements Spec a
spec

-- * Auxiliary

-- | Substitute a string based on a given substitution table.
--
-- This function leaves the key unchanged if it cannot be found in the
-- substitution table.
safeMap :: [(String, String)] -> String -> String
safeMap :: [(String, String)] -> String -> String
safeMap [(String, String)]
ls String
k = String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe String
k (Maybe String -> String) -> Maybe String -> String
forall a b. (a -> b) -> a -> b
$ String -> [(String, String)] -> Maybe String
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
k [(String, String)]
ls

-- | Create a string from a list of strings, inserting new line characters
-- between them. Unlike 'Prelude.unlines', this function does not insert
-- an end of line character at the end of the last string.
unlines' :: [String] -> String
unlines' :: [String] -> String
unlines' = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n"