    -- Copyright 2022 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.
    --
    -- | Auxiliary functions for working with values of type 'Spec'.
    module Data.Spec.Extra
        ( addMissingIdentifiers )
      where

    -- External imports
    import Data.List (nub, (\\))

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

    -- | Add to a spec external variables for all identifiers mentioned in
    -- expressions that are not defined anywhere.
    addMissingIdentifiers :: (a -> [String]) -> Spec a -> Spec a
    addMissingIdentifiers :: forall a. (a -> [String]) -> Spec a -> Spec a
    addMissingIdentifiers a -> [String]
    f Spec a
    s = Spec a
    s { externalVariables = vars' }
      where
        vars' :: [ExternalVariableDef]
    vars'   = Spec a -> [ExternalVariableDef]
    forall a. Spec a -> [ExternalVariableDef]
    externalVariables Spec a
    s [ExternalVariableDef]
    -> [ExternalVariableDef] -> [ExternalVariableDef]
    forall a. [a] -> [a] -> [a]
    ++ [ExternalVariableDef]
    newVars
        newVars :: [ExternalVariableDef]
    newVars = (String -> ExternalVariableDef)
    -> [String] -> [ExternalVariableDef]
    forall a b. (a -> b) -> [a] -> [b]
    map (\String
    n -> String -> String -> ExternalVariableDef
    ExternalVariableDef String
    n String
    "") [String]
    newVarNames

        -- Names that are not defined anywhere
        newVarNames :: [String]
    newVarNames = [String]
    identifiers [String] -> [String] -> [String]
    forall a. Eq a => [a] -> [a] -> [a]
    \\ [String]
    existingNames

        -- Identifiers being mentioned in the requirements.
        identifiers :: [String]
    identifiers = [String] -> [String]
    forall a. Eq a => [a] -> [a]
    nub ([String] -> [String]) -> [String] -> [String]
    forall a b. (a -> b) -> a -> b
    $ (Requirement a -> [String]) -> [Requirement a] -> [String]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (a -> [String]
    f (a -> [String])
    -> (Requirement a -> a) -> Requirement a -> [String]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Requirement a -> a
    forall a. Requirement a -> a
    requirementExpr) (Spec a -> [Requirement a]
    forall a. Spec a -> [Requirement a]
    requirements Spec a
    s)

        -- Names that are defined in variables.
        existingNames :: [String]
    existingNames = (ExternalVariableDef -> String)
    -> [ExternalVariableDef] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map ExternalVariableDef -> String
    externalVariableName (Spec a -> [ExternalVariableDef]
    forall a. Spec a -> [ExternalVariableDef]
    externalVariables Spec a
    s)
                     [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ (InternalVariableDef -> String)
    -> [InternalVariableDef] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map InternalVariableDef -> String
    internalVariableName (Spec a -> [InternalVariableDef]
    forall a. Spec a -> [InternalVariableDef]
    internalVariables Spec a
    s)