    {-# 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
    --
    -- 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 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"