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