    -- 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.

    -- | Formally analyze specifications and provide information about them.
    module Data.Spec.Analysis
        ( AnalysisResult(..)
        , specAnalyze
        )
      where

    -- External imports
    import qualified Copilot.Core as Core
    import           Data.List    (intercalate, lookup)
    import           Data.Maybe   (fromMaybe)

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

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

    -- Internal imports
    import Copilot.Core.Analysis        (exprIsConstant)
    import Copilot.Language.Reify.Extra (reifySpec)

    -- * Analysis of Specs

    -- | Result of analyzing a specification.
    data AnalysisResult = AnalysisResult
      { AnalysisResult -> Int
    numAlwaysTrue  :: Int      -- ^ Number of always true requirements.
      , AnalysisResult -> Int
    numAlwaysFalse :: Int      -- ^ Number of always false requirements.
      , AnalysisResult -> [String]
    alwaysTrueReq  :: [String] -- ^ List of always true requirements.
      , AnalysisResult -> [String]
    alwaysFalseReq :: [String] -- ^ List of always false requirements.
      , AnalysisResult -> Bool
    consistent     :: Bool     -- ^ Whether requirements are mutually
                                   -- consistent.
      }

    -- | Formally analyze a specification for redundancies, conflicts, etc.
    specAnalyze :: [(String, String)]             -- Type substitution table
                -> ([(String, String)] -> a -> a) -- Expr substitution function
                -> (a -> String)                  -- Expr show function
                -> Spec a                         -- Specification
                -> IO (Either String AnalysisResult)
    specAnalyze :: forall a.
    [(String, String)]
    -> ([(String, String)] -> a -> a)
    -> (a -> String)
    -> Spec a
    -> IO (Either String AnalysisResult)
    specAnalyze [(String, String)]
    typeMaps [(String, String)] -> a -> a
    exprTransform a -> String
    showExpr Spec a
    spec = do
      let structuredSpec :: CopilotSpec
    structuredSpec =
            [(String, String)]
    -> ([(String, String)] -> a -> a)
    -> (a -> String)
    -> Spec a
    -> CopilotSpec
    forall a.
    [(String, String)]
    -> ([(String, String)] -> a -> a)
    -> (a -> String)
    -> Spec a
    -> CopilotSpec
    spec2Copilot [(String, String)]
    typeMaps [(String, String)] -> a -> a
    exprTransform a -> String
    showExpr Spec a
    spec

      coreSpec <- [(String, Maybe String)] -> String -> IO Spec
    reifySpec [(String, Maybe String)]
    defaultSpecImports (String -> IO Spec) -> String -> IO Spec
    forall a b. (a -> b) -> a -> b
    $ CopilotSpec -> String
    showSpec CopilotSpec
    structuredSpec

      let properties     = [String] -> [Expr Bool] -> [(String, Expr Bool)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [String]
    propertyNames [Expr Bool]
    propertyGuards
          propertyNames  = ((String, String, String, String, String) -> String)
    -> [(String, String, String, String, String)] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (\(String
    _, String
    p, String
    _, String
    _, String
    _) -> String
    p)
                         ([(String, String, String, String, String)] -> [String])
    -> [(String, String, String, String, String)] -> [String]
    forall a b. (a -> b) -> a -> b
    $ CopilotSpec -> [(String, String, String, String, String)]
    copilotProperties CopilotSpec
    structuredSpec
          propertyGuards = (Trigger -> Expr Bool) -> [Trigger] -> [Expr Bool]
    forall a b. (a -> b) -> [a] -> [b]
    map Trigger -> Expr Bool
    Core.triggerGuard ([Trigger] -> [Expr Bool]) -> [Trigger] -> [Expr Bool]
    forall a b. (a -> b) -> a -> b
    $ Spec -> [Trigger]
    Core.specTriggers Spec
    coreSpec

      constantProperties <- mapM (uncurry $ exprIsConstant coreSpec) properties

      let constantProperties' = [String] -> [(Bool, Bool)] -> [(String, (Bool, Bool))]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [String]
    propertyNames [(Bool, Bool)]
    constantProperties

      let numTrue  = [(Bool, Bool)] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length ([(Bool, Bool)] -> Int) -> [(Bool, Bool)] -> Int
    forall a b. (a -> b) -> a -> b
    $ ((Bool, Bool) -> Bool) -> [(Bool, Bool)] -> [(Bool, Bool)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Bool, Bool) -> Bool
    forall a b. (a, b) -> a
    fst [(Bool, Bool)]
    constantProperties
          numFalse = [(Bool, Bool)] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length ([(Bool, Bool)] -> Int) -> [(Bool, Bool)] -> Int
    forall a b. (a -> b) -> a -> b
    $ ((Bool, Bool) -> Bool) -> [(Bool, Bool)] -> [(Bool, Bool)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Bool, Bool) -> Bool
    forall a b. (a, b) -> b
    snd [(Bool, Bool)]
    constantProperties

          trueReqs  = ((String, (Bool, Bool)) -> String)
    -> [(String, (Bool, Bool))] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (String, (Bool, Bool)) -> String
    forall a b. (a, b) -> a
    fst ([(String, (Bool, Bool))] -> [String])
    -> [(String, (Bool, Bool))] -> [String]
    forall a b. (a -> b) -> a -> b
    $ ((String, (Bool, Bool)) -> Bool)
    -> [(String, (Bool, Bool))] -> [(String, (Bool, Bool))]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ((Bool, Bool) -> Bool
    forall a b. (a, b) -> a
    fst ((Bool, Bool) -> Bool)
    -> ((String, (Bool, Bool)) -> (Bool, Bool))
    -> (String, (Bool, Bool))
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (String, (Bool, Bool)) -> (Bool, Bool)
    forall a b. (a, b) -> b
    snd) [(String, (Bool, Bool))]
    constantProperties'
          falseReqs = ((String, (Bool, Bool)) -> String)
    -> [(String, (Bool, Bool))] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (String, (Bool, Bool)) -> String
    forall a b. (a, b) -> a
    fst ([(String, (Bool, Bool))] -> [String])
    -> [(String, (Bool, Bool))] -> [String]
    forall a b. (a -> b) -> a -> b
    $ ((String, (Bool, Bool)) -> Bool)
    -> [(String, (Bool, Bool))] -> [(String, (Bool, Bool))]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ((Bool, Bool) -> Bool
    forall a b. (a, b) -> b
    snd ((Bool, Bool) -> Bool)
    -> ((String, (Bool, Bool)) -> (Bool, Bool))
    -> (String, (Bool, Bool))
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (String, (Bool, Bool)) -> (Bool, Bool)
    forall a b. (a, b) -> b
    snd) [(String, (Bool, Bool))]
    constantProperties'

      let negatedConjunction = Op1 Bool Bool -> Expr Bool -> Expr Bool
    forall a1 a. Typeable a1 => Op1 a1 a -> Expr a1 -> Expr a
    Core.Op1 Op1 Bool Bool
    Core.Not
                             (Expr Bool -> Expr Bool) -> Expr Bool -> Expr Bool
    forall a b. (a -> b) -> a -> b
    $ (Expr Bool -> Expr Bool -> Expr Bool)
    -> Expr Bool -> [Expr Bool] -> Expr Bool
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (Op2 Bool Bool Bool -> Expr Bool -> Expr Bool -> Expr Bool
    forall a1 b a.
    (Typeable a1, Typeable b) =>
    Op2 a1 b a -> Expr a1 -> Expr b -> Expr a
    Core.Op2 Op2 Bool Bool Bool
    Core.And) Expr Bool
    true [Expr Bool]
    propertyGuards
          true               = Type Bool -> Bool -> Expr Bool
    forall a. Typeable a => Type a -> a -> Expr a
    Core.Const Type Bool
    Core.Bool Bool
    True

      provedNegatedConjunction <-
        exprIsConstant coreSpec "ogma_inc" negatedConjunction

      -- The requirements are considered consistent if it was *not* possible to
      -- prove that their conjunction is always false.
      let consistent = Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ (Bool, Bool) -> Bool
    forall a b. (a, b) -> a
    fst (Bool, Bool)
    provedNegatedConjunction

      return $ Right $
        AnalysisResult numTrue numFalse trueReqs falseReqs consistent

    -- * Auxiliary

    -- ** Structured Copilot specifications

    -- | A structured Copilot specification.
    data CopilotSpec = CopilotSpec
      { CopilotSpec -> [(String, String, String, String, String)]
    copilotProperties :: [(String, String, String, String, String)]
                          -- ^ Requirement name, property name, handler name,
                          -- implementation and arguments.

      , CopilotSpec -> [(String, String, String)]
    copilotAuxDefs    :: [(String, String, String)]
                          -- ^ Name, type, implementation
      }

    -- | Given a 'Spec', return a structured version the corresponding Copilot spec
    -- that differentiates between the auxiliary definitions (inputs, outputs) and
    -- the properties or requirements to check.
    --
    -- 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 :: [(String, String)]             -- Type substitution table
                 -> ([(String, String)] -> a -> a) -- Expr substitution function
                 -> (a -> String)                  -- Expr show function
                 -> Spec a                         -- Specification
                 -> CopilotSpec
    spec2Copilot :: forall a.
    [(String, String)]
    -> ([(String, String)] -> a -> a)
    -> (a -> String)
    -> Spec a
    -> CopilotSpec
    spec2Copilot [(String, String)]
    typeMaps [(String, String)] -> a -> a
    exprTransform a -> String
    showExpr Spec a
    spec = [(String, String, String, String, String)]
    -> [(String, String, String)] -> CopilotSpec
    CopilotSpec [(String, String, String, String, String)]
    reqs [(String, String, String)]
    auxDefs
      where
        -- Encoding of requirements as boolean streams
        reqs :: [(String, String, String, String, String)]
        reqs :: [(String, String, String, String, String)]
    reqs = (Requirement a -> (String, String, String, String, String))
    -> [Requirement a] -> [(String, String, String, String, String)]
    forall a b. (a -> b) -> [a] -> [b]
    map Requirement a -> (String, String, String, String, String)
    reqToDecl (Spec a -> [Requirement a]
    forall a. Spec a -> [Requirement a]
    requirements Spec a
    spec)
          where
            reqToDecl :: Requirement a -> (String, String, String, String, String)
    reqToDecl Requirement a
    i =
                ( String
    reqName
                , String
    propName
                , String
    handlerName
                , [(String, String)] -> String
    reqBody [(String, String)]
    nameSubstitutions
                , String
    handlerArg
                )
              where
                reqName :: String
    reqName = Requirement a -> String
    forall a. Requirement a -> String
    requirementName Requirement a
    i

                propName :: String
    propName = [(String, String)] -> String -> String
    forall k. Eq k => [(k, k)] -> k -> k
    safeMap [(String, String)]
    nameSubstitutions (Requirement a -> String
    forall a. Requirement a -> String
    requirementName Requirement a
    i)

                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
    i)

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

                handlerArg :: String
    handlerArg  =
                  case (Requirement a -> Maybe String
    forall a. Requirement a -> Maybe String
    requirementResultType Requirement a
    i, Requirement a -> Maybe a
    forall a. Requirement a -> Maybe a
    requirementResultExpr Requirement a
    i) of
                    (Just String
    _, 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
    "[]"

        auxDefs :: [(String, String, String)]
        auxDefs :: [(String, String, String)]
    auxDefs = [(String, String, String)]
    externs [(String, String, String)]
    -> [(String, String, String)] -> [(String, String, String)]
    forall a. [a] -> [a] -> [a]
    ++ [(String, String, String)]
    internals

        externs :: [(String, String, String)]
        externs :: [(String, String, String)]
    externs = (ExternalVariableDef -> (String, String, String))
    -> [ExternalVariableDef] -> [(String, String, String)]
    forall a b. (a -> b) -> [a] -> [b]
    map ExternalVariableDef -> (String, String, String)
    externVarToDecl (Spec a -> [ExternalVariableDef]
    forall a. Spec a -> [ExternalVariableDef]
    externalVariables Spec a
    spec)
          where
            externVarToDecl :: ExternalVariableDef -> (String, String, String)
    externVarToDecl ExternalVariableDef
    i = (String
    propName, String
    streamType, String
    implementation)
              where
                propName :: String
    propName = [(String, String)] -> String -> String
    forall k. Eq k => [(k, k)] -> k -> k
    safeMap [(String, String)]
    nameSubstitutions (ExternalVariableDef -> String
    externalVariableName ExternalVariableDef
    i)

                streamType :: String
    streamType = String
    "Stream " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    valueType String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                valueType :: String
    valueType  = [(String, String)] -> String -> String
    forall k. Eq k => [(k, k)] -> k -> k
    safeMap [(String, String)]
    typeMaps (ExternalVariableDef -> String
    externalVariableType ExternalVariableDef
    i)

                implementation :: String
    implementation = 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"

        -- Internal stream definitions
        internals :: [(String, String, String)]
        internals :: [(String, String, String)]
    internals = (InternalVariableDef -> (String, String, String))
    -> [InternalVariableDef] -> [(String, String, String)]
    forall a b. (a -> b) -> [a] -> [b]
    map InternalVariableDef -> (String, String, String)
    internalVarToDecl (Spec a -> [InternalVariableDef]
    forall a. Spec a -> [InternalVariableDef]
    internalVariables Spec a
    spec)
          where
            internalVarToDecl :: InternalVariableDef -> (String, String, String)
    internalVarToDecl InternalVariableDef
    i = (String
    propName, String
    streamType, String
    implementation)
              where
                propName :: String
    propName = [(String, String)] -> String -> String
    forall k. Eq k => [(k, k)] -> k -> k
    safeMap [(String, String)]
    nameSubstitutions (InternalVariableDef -> String
    internalVariableName InternalVariableDef
    i)

                streamType :: String
    streamType = String
    "Stream " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    valueType String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                valueType :: String
    valueType  = [(String, String)] -> String -> String
    forall k. Eq k => [(k, k)] -> k -> k
    safeMap [(String, String)]
    typeMaps (InternalVariableDef -> String
    internalVariableType InternalVariableDef
    i)

                implementation :: String
    implementation = InternalVariableDef -> String
    internalVariableExpr InternalVariableDef
    i

        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

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

    -- | Render a 'CopilotSpec' as a Haskell definition of a 'Copilot.Spec',
    -- listing the elements in the spec with the necessary indentation.
    --
    -- The shown 'Copilot.Spec' has a list of top-level triggers, as well as
    -- several auxiliary definitions.
    showSpec :: CopilotSpec -> String
    showSpec :: CopilotSpec -> String
    showSpec CopilotSpec
    spec = String
    template String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "\n" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    extra String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "\n" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    triggers
      where
        -- Initial template used for analysis purposes.
        template :: String
        template :: String
    template = [String] -> String
    unlines
          [ String
    "do let"
          , String
    ""
          , String
    "       clock :: Stream Int64"
          , String
    "       clock = [0] ++ (clock + 1)"
          , String
    ""
          , String
    "       ftp :: Stream Bool"
          , String
    "       ftp = [True] ++ false"
          , String
    ""
          , String
    "       pre :: Stream Bool -> Stream Bool"
          , String
    "       pre = ([False] ++)"
          , String
    ""
          , String
    "       tpre :: Stream Bool -> Stream Bool"
          , String
    "       tpre = ([True] ++)"
          , String
    ""
          , String
    "       notPreviousNot :: Stream Bool -> Stream Bool"
          , String
    "       notPreviousNot = not . PTLTL.previous . not"
          ]

        extra :: String
    extra = [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
    $ ((String, String, String) -> [String])
    -> [(String, String, String)] -> [[String]]
    forall a b. (a -> b) -> [a] -> [b]
    map (String, String, String) -> [String]
    formatDef
              ([(String, String, String)] -> [[String]])
    -> [(String, String, String)] -> [[String]]
    forall a b. (a -> b) -> a -> b
    $ CopilotSpec -> [(String, String, String)]
    copilotAuxDefs CopilotSpec
    spec

        triggers :: String
    triggers = [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
    $ ((String, String, String, String, String) -> [String])
    -> [(String, String, String, String, String)] -> [[String]]
    forall a b. (a -> b) -> [a] -> [b]
    map (String, String, String, String, String) -> [String]
    forall {a} {a} {b}. Show a => (a, b, a, String, String) -> [String]
    formatTrigger
                 ([(String, String, String, String, String)] -> [[String]])
    -> [(String, String, String, String, String)] -> [[String]]
    forall a b. (a -> b) -> a -> b
    $ CopilotSpec -> [(String, String, String, String, String)]
    copilotProperties CopilotSpec
    spec

        formatDef :: (String, String, String) -> [String]
    formatDef (String
    n, String
    t, String
    i) =
          (String -> String) -> [String] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (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]
    ++ String
    t, String
    n String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    i ]

        formatTrigger :: (a, b, a, String, String) -> [String]
    formatTrigger (a
    _, b
    _, a
    h, String
    g, String
    a) =
          (String -> String) -> [String] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (String
    "   " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++) [ String
    "trigger " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    h String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " (" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    g String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    a ]

    -- | Default imports for a 'Spec' that was converted into a 'Copilot.Spec'.
    defaultSpecImports :: [(String, Maybe String)]
    defaultSpecImports :: [(String, Maybe String)]
    defaultSpecImports =
      [ (String
    "Control.Monad.Writer",  Maybe String
    forall a. Maybe a
    Nothing)
      , (String
    "Copilot.Language",      Maybe String
    forall a. Maybe a
    Nothing)
      , (String
    "Copilot.Language.Spec", Maybe String
    forall a. Maybe a
    Nothing)
      , (String
    "Data.Functor.Identity", Maybe String
    forall a. Maybe a
    Nothing)
      , (String
    "Language.Copilot",      Maybe String
    forall a. Maybe a
    Nothing)
      , (String
    "Copilot.Library.PTLTL", String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "PTLTL")
      , (String
    "Prelude",               String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "P")
      ]

    -- ** Auxiliary list functions

    -- | Substitute a key based on a given substitution table from key to
    -- alternative key.
    --
    -- They key is left unchanged if it cannot be found in the substitution table.
    safeMap :: Eq k => [(k, k)] -> k -> k
    safeMap :: forall k. Eq k => [(k, k)] -> k -> k
    safeMap [(k, k)]
    ls k
    k = k -> Maybe k -> k
    forall a. a -> Maybe a -> a
    fromMaybe k
    k (Maybe k -> k) -> Maybe k -> k
    forall a b. (a -> b) -> a -> b
    $ k -> [(k, k)] -> Maybe k
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup k
    k [(k, k)]
    ls