    module Agda.TypeChecking.Monad.Options where

    import Prelude hiding (null)

    import Control.Monad          ( unless, when )
    import Control.Monad.IO.Class ( MonadIO(..) )
    import Control.Monad.Except
    import Control.Monad.Reader
    import Control.Monad.State
    import Control.Monad.Writer

    import qualified Data.Graph as Graph
    import Data.List (sort)
    import Data.Map (Map)
    import qualified Data.Map as Map
    import qualified Data.Set as Set

    import System.Directory
    import System.FilePath

    import Agda.Syntax.Common
    import Agda.Syntax.TopLevelModuleName

    import Agda.TypeChecking.Monad.Debug (reportSDoc)
    import Agda.TypeChecking.Warnings
    import Agda.TypeChecking.Monad.Base
    import Agda.TypeChecking.Monad.Imports
    import Agda.TypeChecking.Monad.State
    import Agda.TypeChecking.Monad.Benchmark
    import Agda.TypeChecking.Monad.Trace

    import Agda.Interaction.FindFile
    import Agda.Interaction.Options hiding (setPragmaOptions)
    import qualified Agda.Interaction.Options.Lenses as Lens
    import Agda.Interaction.Library
    import Agda.Interaction.Library.Base (LibCache(LibCache), libAbove, libFile, runLibM)

    import Agda.Utils.FileName
    import qualified Agda.Utils.Graph.AdjacencyMap.Unidirectional as G
    import Agda.Utils.Lens
    import Agda.Utils.List
    import Agda.Utils.List1 (List1)
    import qualified Agda.Utils.List1 as List1
    import Agda.Utils.Null
    import Agda.Syntax.Common.Pretty
    import Agda.Utils.Size
    import Agda.Utils.WithDefault

    import Agda.Utils.Impossible

    -- | Sets the pragma options.
    --   Checks for unsafe combinations.
    setPragmaOptions :: PragmaOptions -> TCM ()
    setPragmaOptions :: PragmaOptions -> TCM ()
    setPragmaOptions PragmaOptions
    opts = do
      -- Check for unsafe pragma options if @--safe@ is on.
      Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (PragmaOptions -> Bool
    forall a. LensSafeMode a => a -> Bool
    Lens.getSafeMode PragmaOptions
    opts) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
        [FilePath] -> ([FilePath] -> TCM ()) -> TCM ()
    forall (m :: * -> *) a.
    (Monad m, Null a) =>
    a -> (a -> m ()) -> m ()
    unlessNull (PragmaOptions -> [FilePath]
    unsafePragmaOptions PragmaOptions
    opts) (([FilePath] -> TCM ()) -> TCM ())
    -> ([FilePath] -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ [FilePath]
    unsafe ->
          Warning -> TCM ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> TCM ()) -> Warning -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Set FilePath -> Warning
    SafeFlagPragma (Set FilePath -> Warning) -> Set FilePath -> Warning
    forall a b. (a -> b) -> a -> b
    $ [FilePath] -> Set FilePath
    forall a. Ord a => [a] -> Set a
    Set.fromList [FilePath]
    unsafe

      (PragmaOptions -> f PragmaOptions) -> TCState -> f TCState
    Lens' TCState PragmaOptions
    stPragmaOptions Lens' TCState PragmaOptions -> PragmaOptions -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> a -> m ()
    `setTCLens` PragmaOptions
    opts
      TCM ()
    updateBenchmarkingStatus

    -- | Check that that you don't turn on inconsistent options. For instance, if --a implies --b and
    --   you have both --a and --no-b. Only warn for things that have changed compared to the old
    --   options.
    checkPragmaOptionConsistency :: PragmaOptions -> PragmaOptions -> TCM ()
    checkPragmaOptionConsistency :: PragmaOptions -> PragmaOptions -> TCM ()
    checkPragmaOptionConsistency PragmaOptions
    oldOpts PragmaOptions
    newOpts = do
      (ImpliedPragmaOption -> TCM ()) -> [ImpliedPragmaOption] -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ ImpliedPragmaOption -> TCM ()
    check [ImpliedPragmaOption]
    impliedPragmaOptions
      where
        -- Only warn if both flags are set explicitly (Value rather than Default)
        check :: ImpliedPragmaOption -> TCM ()
    check (ImpliesPragmaOption FilePath
    nameA Bool
    valA PragmaOptions -> WithDefault a
    flagA FilePath
    nameB Bool
    valB PragmaOptions -> WithDefault b
    flagB)
          | PragmaOptions -> WithDefault a
    flagA PragmaOptions
    newOpts WithDefault a -> WithDefault a -> Bool
    forall a. Eq a => a -> a -> Bool
    == PragmaOptions -> WithDefault a
    flagA PragmaOptions
    oldOpts
          , PragmaOptions -> WithDefault b
    flagB PragmaOptions
    newOpts WithDefault b -> WithDefault b -> Bool
    forall a. Eq a => a -> a -> Bool
    == PragmaOptions -> WithDefault b
    flagB PragmaOptions
    oldOpts  = () -> TCM ()
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure () -- Nothing changed, don't check again.
          | Value Bool
    vA <- PragmaOptions -> WithDefault a
    flagA PragmaOptions
    newOpts, Bool
    vA Bool -> Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    == Bool
    valA
          , Value Bool
    vB <- PragmaOptions -> WithDefault b
    flagB PragmaOptions
    newOpts, Bool
    vB Bool -> Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Bool
    valB = Warning -> TCM ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> TCM ()) -> Warning -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ FilePath -> FilePath -> Warning
    ConflictingPragmaOptions (FilePath
    nameA FilePath -> Bool -> FilePath
    .= Bool
    valA) (FilePath
    nameB FilePath -> Bool -> FilePath
    .= Bool
    valB)
          | Bool
    otherwise                 = () -> TCM ()
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()
          where
            FilePath
    name .= :: FilePath -> Bool -> FilePath
    .= Bool
    True  = FilePath
    name
            FilePath
    name .= Bool
    False = FilePath
    "no-" FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    name

    -- | Sets the command line options (both persistent and pragma options
    -- are updated).
    --
    -- Relative include directories are made absolute with respect to the
    -- current working directory. If the include directories have changed
    -- then the state is reset (partly, see 'setIncludeDirs').
    --
    -- An empty list of relative include directories (@'Left' []@) is
    -- interpreted as @["."]@.
    setCommandLineOptions :: CommandLineOptions -> TCM ()
    setCommandLineOptions :: CommandLineOptions -> TCM ()
    setCommandLineOptions CommandLineOptions
    opts = do
      root <- IO AbsolutePath -> TCMT IO AbsolutePath
    forall a. IO a -> TCMT IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (FilePath -> IO AbsolutePath
    absolute (FilePath -> IO AbsolutePath) -> IO FilePath -> IO AbsolutePath
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< IO FilePath
    getCurrentDirectory)
      setCommandLineOptions' root opts

    setCommandLineOptions'
      :: AbsolutePath
         -- ^ The base directory of relative paths.
      -> CommandLineOptions
      -> TCM ()
    setCommandLineOptions' :: AbsolutePath -> CommandLineOptions -> TCM ()
    setCommandLineOptions' AbsolutePath
    root CommandLineOptions
    opts = do
      -- Andreas, 2022-11-19: removed a call to checkOpts which did nothing.
          incs <- case CommandLineOptions -> [AbsolutePath]
    optAbsoluteIncludePaths CommandLineOptions
    opts of
            [] -> do
              opts' <- AbsolutePath -> CommandLineOptions -> TCM CommandLineOptions
    setLibraryPaths AbsolutePath
    root CommandLineOptions
    opts
              let incs = CommandLineOptions -> [FilePath]
    optIncludePaths CommandLineOptions
    opts'
              setIncludeDirs incs root
              List1.toList <$> getIncludeDirs
            [AbsolutePath]
    incs -> [AbsolutePath] -> TCMT IO [AbsolutePath]
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [AbsolutePath]
    incs
          modifyTC $ Lens.setCommandLineOptions opts{ optAbsoluteIncludePaths = incs }
          setPragmaOptions (optPragmaOptions opts)
          updateBenchmarkingStatus

    libToTCM :: LibM a -> TCM a
    libToTCM :: forall a. LibM a -> TCM a
    libToTCM LibM a
    m = do
      libCache <- Lens' TCState LibState -> TCMT IO LibState
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC (LibState -> f LibState) -> TCState -> f TCState
    Lens' TCState LibState
    stLibCache
      ((z, warns), libCache') <- liftIO $ runLibM m libCache

      setTCLens stLibCache libCache'

      List1.unlessNull warns \ List1 LibWarning
    warns -> List1 Warning -> TCM ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    List1 Warning -> m ()
    warnings (List1 Warning -> TCM ()) -> List1 Warning -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ (LibWarning -> Warning) -> List1 LibWarning -> List1 Warning
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap LibWarning -> Warning
    LibraryWarning List1 LibWarning
    warns
      case z of
        Left LibErrors
    s  -> TypeError -> TCMT IO a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO a) -> TypeError -> TCMT IO a
    forall a b. (a -> b) -> a -> b
    $ LibErrors -> TypeError
    LibraryError LibErrors
    s
        Right a
    x -> a -> TCMT IO a
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    x

    -- | Returns the library files for a given file.
    --
    -- Nothing is returned if 'optUseLibs' is 'False'.
    --
    -- An error is raised if 'optUseLibs' is 'True' and a library file is
    -- located too far down the directory hierarchy (see
    -- 'checkLibraryFileNotTooFarDown').

    getAgdaLibFiles
      :: AbsolutePath        -- ^ The file name.
      -> TopLevelModuleName  -- ^ The top-level module name.
      -> TCM [AgdaLibFile]
    getAgdaLibFiles :: AbsolutePath -> TopLevelModuleName -> TCM [AgdaLibFile]
    getAgdaLibFiles AbsolutePath
    f TopLevelModuleName
    m = do
      ls <- AbsolutePath -> TCM [AgdaLibFile]
    getAgdaLibFilesWithoutTopLevelModuleName AbsolutePath
    f
      mapM_ (checkLibraryFileNotTooFarDown m) ls
      return ls

    -- | Returns potential library files for a file without a known
    -- top-level module name.
    --
    -- Once the top-level module name is known one can use
    -- 'checkLibraryFileNotTooFarDown' to check that the potential library
    -- files were not located too far down the directory hierarchy.
    --
    -- Nothing is returned if 'optUseLibs' is 'False'.

    getAgdaLibFilesWithoutTopLevelModuleName
      :: AbsolutePath  -- ^ The file.
      -> TCM [AgdaLibFile]
    getAgdaLibFilesWithoutTopLevelModuleName :: AbsolutePath -> TCM [AgdaLibFile]
    getAgdaLibFilesWithoutTopLevelModuleName AbsolutePath
    f = do
      useLibs <- CommandLineOptions -> Bool
    optUseLibs (CommandLineOptions -> Bool)
    -> TCM CommandLineOptions -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCM CommandLineOptions
    forall (m :: * -> *). HasOptions m => m CommandLineOptions
    commandLineOptions
      if | useLibs   -> libToTCM $ getAgdaLibFile root
         | otherwise -> return []
      where
      root :: FilePath
    root = FilePath -> FilePath
    takeDirectory (FilePath -> FilePath) -> FilePath -> FilePath
    forall a b. (a -> b) -> a -> b
    $ AbsolutePath -> FilePath
    filePath AbsolutePath
    f

    -- | Checks that a library file for the module @A.B.C@ (say) in the
    -- directory @dir/A/B@ is located at least two directories above the
    -- file (not in @dir/A@ or @dir/A/B@).

    checkLibraryFileNotTooFarDown ::
      TopLevelModuleName ->
      AgdaLibFile ->
      TCM ()
    checkLibraryFileNotTooFarDown :: TopLevelModuleName -> AgdaLibFile -> TCM ()
    checkLibraryFileNotTooFarDown TopLevelModuleName
    m AgdaLibFile
    lib =
      Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (AgdaLibFile
    lib AgdaLibFile -> Lens' AgdaLibFile Int -> Int
    forall o i. o -> Lens' o i -> i
    ^. (Int -> f Int) -> AgdaLibFile -> f AgdaLibFile
    Lens' AgdaLibFile Int
    libAbove Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < TopLevelModuleName -> Int
    forall a. Sized a => a -> Int
    size TopLevelModuleName
    m Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TopLevelModuleName -> AgdaLibFile -> TypeError
    LibTooFarDown TopLevelModuleName
    m AgdaLibFile
    lib

    -- | Returns the library options for a given file.

    getLibraryOptions
      :: AbsolutePath        -- ^ The file name.
      -> TopLevelModuleName  -- ^ The top-level module name.
      -> TCM [OptionsPragma]
    getLibraryOptions :: AbsolutePath -> TopLevelModuleName -> TCM [OptionsPragma]
    getLibraryOptions AbsolutePath
    f TopLevelModuleName
    m = (AgdaLibFile -> OptionsPragma) -> [AgdaLibFile] -> [OptionsPragma]
    forall a b. (a -> b) -> [a] -> [b]
    map AgdaLibFile -> OptionsPragma
    _libPragmas ([AgdaLibFile] -> [OptionsPragma])
    -> TCM [AgdaLibFile] -> TCM [OptionsPragma]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> AbsolutePath -> TopLevelModuleName -> TCM [AgdaLibFile]
    getAgdaLibFiles AbsolutePath
    f TopLevelModuleName
    m

    setLibraryPaths
      :: AbsolutePath
         -- ^ The base directory of relative paths.
      -> CommandLineOptions
      -> TCM CommandLineOptions
    setLibraryPaths :: AbsolutePath -> CommandLineOptions -> TCM CommandLineOptions
    setLibraryPaths AbsolutePath
    root CommandLineOptions
    o =
      CommandLineOptions -> TCM CommandLineOptions
    setLibraryIncludes (CommandLineOptions -> TCM CommandLineOptions)
    -> TCM CommandLineOptions -> TCM CommandLineOptions
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< AbsolutePath -> CommandLineOptions -> TCM CommandLineOptions
    addDefaultLibraries AbsolutePath
    root CommandLineOptions
    o

    setLibraryIncludes :: CommandLineOptions -> TCM CommandLineOptions
    setLibraryIncludes :: CommandLineOptions -> TCM CommandLineOptions
    setLibraryIncludes CommandLineOptions
    o
      | Bool -> Bool
    not (CommandLineOptions -> Bool
    optUseLibs CommandLineOptions
    o) = CommandLineOptions -> TCM CommandLineOptions
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CommandLineOptions
    o
      | Bool
    otherwise = do
        let libs :: [LibName]
    libs = CommandLineOptions -> [LibName]
    optLibraries CommandLineOptions
    o
        installed <- LibM [AgdaLibFile] -> TCM [AgdaLibFile]
    forall a. LibM a -> TCM a
    libToTCM (LibM [AgdaLibFile] -> TCM [AgdaLibFile])
    -> LibM [AgdaLibFile] -> TCM [AgdaLibFile]
    forall a b. (a -> b) -> a -> b
    $ Maybe FilePath -> LibM [AgdaLibFile]
    getInstalledLibraries (CommandLineOptions -> Maybe FilePath
    optOverrideLibrariesFile CommandLineOptions
    o)
        paths     <- libToTCM $ libraryIncludePaths (optOverrideLibrariesFile o) installed libs
        return o{ optIncludePaths = paths ++ optIncludePaths o }

    addDefaultLibraries
      :: AbsolutePath
         -- ^ The base directory of relative paths.
      -> CommandLineOptions
      -> TCM CommandLineOptions
    addDefaultLibraries :: AbsolutePath -> CommandLineOptions -> TCM CommandLineOptions
    addDefaultLibraries AbsolutePath
    root CommandLineOptions
    o
      | Bool -> Bool
    not ([LibName] -> Bool
    forall a. Null a => a -> Bool
    null ([LibName] -> Bool) -> [LibName] -> Bool
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions -> [LibName]
    optLibraries CommandLineOptions
    o) Bool -> Bool -> Bool
    || Bool -> Bool
    not (CommandLineOptions -> Bool
    optUseLibs CommandLineOptions
    o) = CommandLineOptions -> TCM CommandLineOptions
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CommandLineOptions
    o
      | Bool
    otherwise = do
      (libs, incs) <- LibM ([LibName], [FilePath]) -> TCM ([LibName], [FilePath])
    forall a. LibM a -> TCM a
    libToTCM (LibM ([LibName], [FilePath]) -> TCM ([LibName], [FilePath]))
    -> LibM ([LibName], [FilePath]) -> TCM ([LibName], [FilePath])
    forall a b. (a -> b) -> a -> b
    $ FilePath -> Bool -> LibM ([LibName], [FilePath])
    getDefaultLibraries (AbsolutePath -> FilePath
    filePath AbsolutePath
    root) (CommandLineOptions -> Bool
    optDefaultLibs CommandLineOptions
    o)
      return o{ optIncludePaths = incs ++ optIncludePaths o, optLibraries = libs }

    -- This function is only called when an interactor exists
    -- (i.e. when Agda actually does something).
    addTrustedExecutables
      :: CommandLineOptions
      -> TCM CommandLineOptions
    addTrustedExecutables :: CommandLineOptions -> TCM CommandLineOptions
    addTrustedExecutables CommandLineOptions
    o = do
      trustedExes <- LibM (Map ExeName FilePath) -> TCM (Map ExeName FilePath)
    forall a. LibM a -> TCM a
    libToTCM (LibM (Map ExeName FilePath) -> TCM (Map ExeName FilePath))
    -> LibM (Map ExeName FilePath) -> TCM (Map ExeName FilePath)
    forall a b. (a -> b) -> a -> b
    $ LibM (Map ExeName FilePath)
    getTrustedExecutables
      -- Wen, 2020-06-03
      -- Replace the map wholesale instead of computing the union because this function
      -- should never be called more than once, and doing so either has the same result
      -- or is a security risk.
      return o{ optTrustedExecutables = trustedExes }

    -- | Set pragma options without checking for consistency.
    setOptionsFromPragma :: OptionsPragma -> TCM ()
    setOptionsFromPragma :: OptionsPragma -> TCM ()
    setOptionsFromPragma = Bool -> OptionsPragma -> TCM ()
    setOptionsFromPragma' Bool
    False

    -- | Set pragma options and check them for consistency.
    checkAndSetOptionsFromPragma :: OptionsPragma -> TCM ()
    checkAndSetOptionsFromPragma :: OptionsPragma -> TCM ()
    checkAndSetOptionsFromPragma = Bool -> OptionsPragma -> TCM ()
    setOptionsFromPragma' Bool
    True

    setOptionsFromPragma' :: Bool -> OptionsPragma -> TCM ()
    setOptionsFromPragma' :: Bool -> OptionsPragma -> TCM ()
    setOptionsFromPragma' Bool
    checkConsistency OptionsPragma
    ps = Range -> TCM () -> TCM ()
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange (OptionsPragma -> Range
    pragmaRange OptionsPragma
    ps) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
        opts <- TCM CommandLineOptions
    forall (m :: * -> *). HasOptions m => m CommandLineOptions
    commandLineOptions
        let (z, warns) = runOptM (parsePragmaOptions ps opts)
        mapM_ (warning . OptionWarning) warns
        case z of
          Left FilePath
    err    -> TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ FilePath -> TypeError
    OptionError FilePath
    err
          Right PragmaOptions
    opts' -> do

            -- Check consistency of implied options
            Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    checkConsistency (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
              oldOpts <- TCMT IO PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions
              checkPragmaOptionConsistency oldOpts opts'

            PragmaOptions -> TCM ()
    setPragmaOptions PragmaOptions
    opts'

    -- | Disable display forms.
    enableDisplayForms :: MonadTCEnv m => m a -> m a
    enableDisplayForms :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    enableDisplayForms =
      (TCEnv -> TCEnv) -> m a -> m a
    forall a. (TCEnv -> TCEnv) -> m a -> m a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> m a -> m a) -> (TCEnv -> TCEnv) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ \TCEnv
    e -> TCEnv
    e { envDisplayFormsEnabled = True }

    -- | Disable display forms.
    disableDisplayForms :: MonadTCEnv m => m a -> m a
    disableDisplayForms :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    disableDisplayForms =
      (TCEnv -> TCEnv) -> m a -> m a
    forall a. (TCEnv -> TCEnv) -> m a -> m a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> m a -> m a) -> (TCEnv -> TCEnv) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ \TCEnv
    e -> TCEnv
    e { envDisplayFormsEnabled = False }

    -- | Check if display forms are enabled.
    displayFormsEnabled :: MonadTCEnv m => m Bool
    displayFormsEnabled :: forall (m :: * -> *). MonadTCEnv m => m Bool
    displayFormsEnabled = (TCEnv -> Bool) -> m Bool
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Bool
    envDisplayFormsEnabled

    -- | Gets the include directories.
    --
    -- Precondition: 'optAbsoluteIncludePaths' must be nonempty (i.e.
    -- 'setCommandLineOptions' must have run).

    getIncludeDirs :: HasOptions m => m (List1 AbsolutePath)
    getIncludeDirs :: forall (m :: * -> *). HasOptions m => m (NonEmpty AbsolutePath)
    getIncludeDirs = do
      NonEmpty AbsolutePath -> [AbsolutePath] -> NonEmpty AbsolutePath
    forall a. List1 a -> [a] -> List1 a
    List1.fromListSafe NonEmpty AbsolutePath
    forall a. HasCallStack => a
    __IMPOSSIBLE__ ([AbsolutePath] -> NonEmpty AbsolutePath)
    -> (CommandLineOptions -> [AbsolutePath])
    -> CommandLineOptions
    -> NonEmpty AbsolutePath
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CommandLineOptions -> [AbsolutePath]
    optAbsoluteIncludePaths (CommandLineOptions -> NonEmpty AbsolutePath)
    -> m CommandLineOptions -> m (NonEmpty AbsolutePath)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m CommandLineOptions
    forall (m :: * -> *). HasOptions m => m CommandLineOptions
    commandLineOptions

    -- | Makes the given directories absolute and stores them as include
    -- directories.
    --
    -- If the include directories change, then the state is reset
    -- (completely, except for the include directories and some other
    -- things).
    --
    -- An empty list is interpreted as @["."]@.

    setIncludeDirs :: [FilePath]    -- ^ New include directories.
                   -> AbsolutePath  -- ^ The base directory of relative paths.
                   -> TCM ()
    setIncludeDirs :: [FilePath] -> AbsolutePath -> TCM ()
    setIncludeDirs [FilePath]
    incs AbsolutePath
    root = do
      -- save the previous include dirs
      oldIncs <- (TCState -> [AbsolutePath]) -> TCMT IO [AbsolutePath]
    forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
    getsTC TCState -> [AbsolutePath]
    forall a. LensIncludePaths a => a -> [AbsolutePath]
    Lens.getAbsoluteIncludePaths

      -- Add the current dir if no include path is given
      incs <- return $ List1.fromListSafe (List1.singleton ".") incs
      -- Make paths absolute
      incs <- return $ fmap (mkAbsolute . (filePath root </>)) incs

      -- Andreas, 2013-10-30  Add default include dir
      primdir <- useTC stPrimitiveLibDir
          -- We add the default dir at the end, since it is then
          -- printed last in error messages.
          -- Might also be useful to overwrite default imports...
      incs <- return $ List1.fromListSafe __IMPOSSIBLE__ $ nubOn id $ List1.toList $ incs <> List1.singleton primdir

      reportSDoc "setIncludeDirs" 10 $ return $ vcat
        [ "Old include directories:"
        , nest 2 $ vcat $ map pretty oldIncs
        , "New include directories:"
        , nest 2 $ vcat $ fmap pretty incs
        ]

      -- Check whether the include dirs have changed.  If yes, reset state.
      -- Andreas, 2013-10-30 comments:
      -- The logic, namely using the include-dirs variable as a driver
      -- for the interaction, qualifies for a code-obfuscation contest.
      -- I guess one Boolean more in the state cost 10.000 EUR at the time
      -- of this implementation...
      --
      -- Andreas, perhaps you have misunderstood something: If the include
      -- directories have changed and we do not reset the decoded modules,
      -- then we might (depending on how the rest of the code works) end
      -- up in a situation in which we use the contents of the file
      -- "old-path/M.agda", when the user actually meant
      -- "new-path/M.agda".
      when (sort oldIncs /= sort (List1.toList incs)) $ do
        ho <- getInteractionOutputCallback
        tcWarnings <- useTC stTCWarnings -- restore already generated warnings
        libCache   <- useTC stLibCache   -- restore cached project configs & .agda-lib files, since they use absolute paths
        decodedModules <- getDecodedModules
        (keptDecodedModules, modFile) <- modulesToKeep incs decodedModules
        resetAllState
        setTCLens stTCWarnings tcWarnings
        setTCLens stLibCache libCache
        setInteractionOutputCallback ho
        setDecodedModules keptDecodedModules
        setTCLens stModuleToSourceId modFile

      Lens.putAbsoluteIncludePaths $ List1.toList incs
      where
      -- A decoded module is kept if its top-level module name is resolved
      -- to the same absolute path using the old and the new include
      -- directories, and the same applies to all dependencies.
      --
      -- File system accesses are cached using the ModuleToSource data
      -- structure: For the old include directories this should mean that
      -- the file system is not accessed, but the file system is accessed
      -- for the new include directories, and certain changes to the file
      -- system could lead to interfaces being discarded. A new
      -- ModuleToSource structure, constructed using the new include
      -- directories, is returned.
      modulesToKeep
        :: List1 AbsolutePath -- New include directories.
        -> DecodedModules  -- Old decoded modules.
        -> TCM (DecodedModules, ModuleToSourceId)
      modulesToKeep :: NonEmpty AbsolutePath
    -> DecodedModules -> TCM (DecodedModules, ModuleToSourceId)
    modulesToKeep NonEmpty AbsolutePath
    incs DecodedModules
    old = DecodedModules
    -> ModuleToSourceId
    -> [ModuleInfo]
    -> TCM (DecodedModules, ModuleToSourceId)
    process DecodedModules
    forall k a. Map k a
    Map.empty ModuleToSourceId
    forall k a. Map k a
    Map.empty [ModuleInfo]
    modules
        where
        -- A graph with one node per module in old, and an edge from m to
        -- n if the module corresponding to m imports the module
        -- corresponding to n.
        dependencyGraph :: G.Graph TopLevelModuleName ()
        dependencyGraph :: Graph TopLevelModuleName ()
    dependencyGraph =
          [TopLevelModuleName] -> Graph TopLevelModuleName ()
    forall n e. Ord n => [n] -> Graph n e
    G.fromNodes
            [ Interface -> TopLevelModuleName
    iTopLevelModuleName (Interface -> TopLevelModuleName)
    -> Interface -> TopLevelModuleName
    forall a b. (a -> b) -> a -> b
    $ ModuleInfo -> Interface
    miInterface ModuleInfo
    m
            | ModuleInfo
    m <- DecodedModules -> [ModuleInfo]
    forall k a. Map k a -> [a]
    Map.elems DecodedModules
    old
            ]
            Graph TopLevelModuleName ()
    -> Graph TopLevelModuleName () -> Graph TopLevelModuleName ()
    forall n e. Ord n => Graph n e -> Graph n e -> Graph n e
    `G.union`
          [Edge TopLevelModuleName ()] -> Graph TopLevelModuleName ()
    forall n e. Ord n => [Edge n e] -> Graph n e
    G.fromEdges
            [ G.Edge
                { source :: TopLevelModuleName
    source = Interface -> TopLevelModuleName
    iTopLevelModuleName (Interface -> TopLevelModuleName)
    -> Interface -> TopLevelModuleName
    forall a b. (a -> b) -> a -> b
    $ ModuleInfo -> Interface
    miInterface ModuleInfo
    m
                , target :: TopLevelModuleName
    target = TopLevelModuleName
    d
                , label :: ()
    label = ()
                }
            | ModuleInfo
    m      <- DecodedModules -> [ModuleInfo]
    forall k a. Map k a -> [a]
    Map.elems DecodedModules
    old
            , (TopLevelModuleName
    d, Hash
    _) <- Interface -> [(TopLevelModuleName, Hash)]
    iImportedModules (Interface -> [(TopLevelModuleName, Hash)])
    -> Interface -> [(TopLevelModuleName, Hash)]
    forall a b. (a -> b) -> a -> b
    $ ModuleInfo -> Interface
    miInterface ModuleInfo
    m
            ]

        -- All the modules from old, sorted so that all of a module's
        -- dependencies precede it in the list.
        modules :: [ModuleInfo]
        modules :: [ModuleInfo]
    modules =
          (SCC TopLevelModuleName -> ModuleInfo)
    -> [SCC TopLevelModuleName] -> [ModuleInfo]
    forall a b. (a -> b) -> [a] -> [b]
    map (\case
                  Graph.CyclicSCC{} ->
                    -- Agda does not allow cycles in the dependency graph.
                    ModuleInfo
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                  Graph.AcyclicSCC TopLevelModuleName
    m ->
                    case TopLevelModuleName -> DecodedModules -> Maybe ModuleInfo
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup TopLevelModuleName
    m DecodedModules
    old of
                      Just ModuleInfo
    m  -> ModuleInfo
    m
                      Maybe ModuleInfo
    Nothing -> ModuleInfo
    forall a. HasCallStack => a
    __IMPOSSIBLE__) ([SCC TopLevelModuleName] -> [ModuleInfo])
    -> [SCC TopLevelModuleName] -> [ModuleInfo]
    forall a b. (a -> b) -> a -> b
    $
          Graph TopLevelModuleName () -> [SCC TopLevelModuleName]
    forall n e. Ord n => Graph n e -> [SCC n]
    G.sccs' Graph TopLevelModuleName ()
    dependencyGraph

        process ::
          Map TopLevelModuleName ModuleInfo -> ModuleToSourceId ->
          [ModuleInfo] -> TCM (DecodedModules, ModuleToSourceId)
        process :: DecodedModules
    -> ModuleToSourceId
    -> [ModuleInfo]
    -> TCM (DecodedModules, ModuleToSourceId)
    process !DecodedModules
    keep !ModuleToSourceId
    modFile [] = (DecodedModules, ModuleToSourceId)
    -> TCM (DecodedModules, ModuleToSourceId)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return
          ( [(TopLevelModuleName, ModuleInfo)] -> DecodedModules
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList ([(TopLevelModuleName, ModuleInfo)] -> DecodedModules)
    -> [(TopLevelModuleName, ModuleInfo)] -> DecodedModules
    forall a b. (a -> b) -> a -> b
    $
            DecodedModules -> [(TopLevelModuleName, ModuleInfo)]
    forall k a. Map k a -> [(k, a)]
    Map.toList DecodedModules
    keep
          , ModuleToSourceId
    modFile
          )
        process DecodedModules
    keep ModuleToSourceId
    modFile (ModuleInfo
    m : [ModuleInfo]
    ms) = do
          let deps :: [TopLevelModuleName]
    deps     = ((TopLevelModuleName, Hash) -> TopLevelModuleName)
    -> [(TopLevelModuleName, Hash)] -> [TopLevelModuleName]
    forall a b. (a -> b) -> [a] -> [b]
    map (TopLevelModuleName, Hash) -> TopLevelModuleName
    forall a b. (a, b) -> a
    fst ([(TopLevelModuleName, Hash)] -> [TopLevelModuleName])
    -> [(TopLevelModuleName, Hash)] -> [TopLevelModuleName]
    forall a b. (a -> b) -> a -> b
    $ Interface -> [(TopLevelModuleName, Hash)]
    iImportedModules (Interface -> [(TopLevelModuleName, Hash)])
    -> Interface -> [(TopLevelModuleName, Hash)]
    forall a b. (a -> b) -> a -> b
    $ ModuleInfo -> Interface
    miInterface ModuleInfo
    m
              depsKept :: Bool
    depsKept = (TopLevelModuleName -> Bool) -> [TopLevelModuleName] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (TopLevelModuleName -> DecodedModules -> Bool
    forall k a. Ord k => k -> Map k a -> Bool
    `Map.member` DecodedModules
    keep) [TopLevelModuleName]
    deps
          (keep, modFile) <-
            if Bool -> Bool
    not Bool
    depsKept then (DecodedModules, ModuleToSourceId)
    -> TCM (DecodedModules, ModuleToSourceId)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DecodedModules
    keep, ModuleToSourceId
    modFile) else do
            let t :: TopLevelModuleName
    t = Interface -> TopLevelModuleName
    iTopLevelModuleName (Interface -> TopLevelModuleName)
    -> Interface -> TopLevelModuleName
    forall a b. (a -> b) -> a -> b
    $ ModuleInfo -> Interface
    miInterface ModuleInfo
    m
            oldF            <- TopLevelModuleName -> TCM (Either FindError SourceFile)
    findFile' TopLevelModuleName
    t
            (newF, modFile) <- runStateT (findFile'_ incs t) modFile
            return $ case (oldF, newF) of
              (Right SourceFile
    f1, Right SourceFile
    f2) | SourceFile
    f1 SourceFile -> SourceFile -> Bool
    forall a. Eq a => a -> a -> Bool
    == SourceFile
    f2 ->
                (TopLevelModuleName
    -> ModuleInfo -> DecodedModules -> DecodedModules
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert TopLevelModuleName
    t ModuleInfo
    m DecodedModules
    keep, ModuleToSourceId
    modFile)
              (Either FindError SourceFile, Either FindError SourceFile)
    _ -> (DecodedModules
    keep, ModuleToSourceId
    modFile)
          process keep modFile ms

    isPropEnabled :: HasOptions m => m Bool
    isPropEnabled :: forall (m :: * -> *). HasOptions m => m Bool
    isPropEnabled = PragmaOptions -> Bool
    optProp (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions

    isLevelUniverseEnabled :: HasOptions m => m Bool
    isLevelUniverseEnabled :: forall (m :: * -> *). HasOptions m => m Bool
    isLevelUniverseEnabled = PragmaOptions -> Bool
    optLevelUniverse (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions

    isTwoLevelEnabled :: HasOptions m => m Bool
    isTwoLevelEnabled :: forall (m :: * -> *). HasOptions m => m Bool
    isTwoLevelEnabled = PragmaOptions -> Bool
    optTwoLevel (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions

    {-# SPECIALIZE hasUniversePolymorphism :: TCM Bool #-}
    hasUniversePolymorphism :: HasOptions m => m Bool
    hasUniversePolymorphism :: forall (m :: * -> *). HasOptions m => m Bool
    hasUniversePolymorphism = PragmaOptions -> Bool
    optUniversePolymorphism (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions

    showImplicitArguments :: HasOptions m => m Bool
    showImplicitArguments :: forall (m :: * -> *). HasOptions m => m Bool
    showImplicitArguments = PragmaOptions -> Bool
    optShowImplicit (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions

    showGeneralizedArguments :: HasOptions m => m Bool
    showGeneralizedArguments :: forall (m :: * -> *). HasOptions m => m Bool
    showGeneralizedArguments = (\PragmaOptions
    opt -> PragmaOptions -> Bool
    optShowGeneralized PragmaOptions
    opt) (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions

    showIrrelevantArguments :: HasOptions m => m Bool
    showIrrelevantArguments :: forall (m :: * -> *). HasOptions m => m Bool
    showIrrelevantArguments = PragmaOptions -> Bool
    optShowIrrelevant (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions

    showIdentitySubstitutions :: HasOptions m => m Bool
    showIdentitySubstitutions :: forall (m :: * -> *). HasOptions m => m Bool
    showIdentitySubstitutions = PragmaOptions -> Bool
    optShowIdentitySubstitutions (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions

    -- | Switch on printing of implicit and irrelevant arguments.
    --   E.g. for reification in with-function generation.
    --
    --   Restores all 'PragmaOptions' after completion.
    --   Thus, do not attempt to make persistent 'PragmaOptions'
    --   changes in a `withShowAllArguments` bracket.

    withShowAllArguments :: ReadTCState m => m a -> m a
    withShowAllArguments :: forall (m :: * -> *) a. ReadTCState m => m a -> m a
    withShowAllArguments = Bool -> m a -> m a
    forall (m :: * -> *) a. ReadTCState m => Bool -> m a -> m a
    withShowAllArguments' Bool
    True

    withShowAllArguments' :: ReadTCState m => Bool -> m a -> m a
    withShowAllArguments' :: forall (m :: * -> *) a. ReadTCState m => Bool -> m a -> m a
    withShowAllArguments' Bool
    yes = (PragmaOptions -> PragmaOptions) -> m a -> m a
    forall (m :: * -> *) a.
    ReadTCState m =>
    (PragmaOptions -> PragmaOptions) -> m a -> m a
    withPragmaOptions ((PragmaOptions -> PragmaOptions) -> m a -> m a)
    -> (PragmaOptions -> PragmaOptions) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ \ PragmaOptions
    opts ->
      PragmaOptions
    opts { _optShowImplicit = Value yes, _optShowIrrelevant = Value yes }

    withoutPrintingGeneralization :: ReadTCState m => m a -> m a
    withoutPrintingGeneralization :: forall (m :: * -> *) a. ReadTCState m => m a -> m a
    withoutPrintingGeneralization = (PragmaOptions -> PragmaOptions) -> m a -> m a
    forall (m :: * -> *) a.
    ReadTCState m =>
    (PragmaOptions -> PragmaOptions) -> m a -> m a
    withPragmaOptions ((PragmaOptions -> PragmaOptions) -> m a -> m a)
    -> (PragmaOptions -> PragmaOptions) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ \ PragmaOptions
    opts ->
      PragmaOptions
    opts { _optShowGeneralized = Value False }

    -- | Change 'PragmaOptions' for a computation and restore afterwards.
    withPragmaOptions :: ReadTCState m => (PragmaOptions -> PragmaOptions) -> m a -> m a
    withPragmaOptions :: forall (m :: * -> *) a.
    ReadTCState m =>
    (PragmaOptions -> PragmaOptions) -> m a -> m a
    withPragmaOptions = Lens' TCState PragmaOptions
    -> (PragmaOptions -> PragmaOptions) -> m a -> m a
    forall a b. Lens' TCState a -> (a -> a) -> m b -> m b
    forall (m :: * -> *) a b.
    ReadTCState m =>
    Lens' TCState a -> (a -> a) -> m b -> m b
    locallyTCState (PragmaOptions -> f PragmaOptions) -> TCState -> f TCState
    Lens' TCState PragmaOptions
    stPragmaOptions

    positivityCheckEnabled :: HasOptions m => m Bool
    positivityCheckEnabled :: forall (m :: * -> *). HasOptions m => m Bool
    positivityCheckEnabled = PragmaOptions -> Bool
    optPositivityCheck (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions

    {-# SPECIALIZE typeInType :: TCM Bool #-}
    typeInType :: HasOptions m => m Bool
    typeInType :: forall (m :: * -> *). HasOptions m => m Bool
    typeInType = Bool -> Bool
    not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Bool
    optUniverseCheck (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions

    etaEnabled :: HasOptions m => m Bool
    etaEnabled :: forall (m :: * -> *). HasOptions m => m Bool
    etaEnabled = PragmaOptions -> Bool
    optEta (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions

    maxInstanceSearchDepth :: HasOptions m => m Int
    maxInstanceSearchDepth :: forall (m :: * -> *). HasOptions m => m Int
    maxInstanceSearchDepth = PragmaOptions -> Int
    optInstanceSearchDepth (PragmaOptions -> Int) -> m PragmaOptions -> m Int
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions

    maxInversionDepth :: HasOptions m => m Int
    maxInversionDepth :: forall (m :: * -> *). HasOptions m => m Int
    maxInversionDepth = PragmaOptions -> Int
    optInversionMaxDepth (PragmaOptions -> Int) -> m PragmaOptions -> m Int
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions

    -- | Returns the 'Language' currently in effect.

    getLanguage :: HasOptions m => m Language
    getLanguage :: forall (m :: * -> *). HasOptions m => m Language
    getLanguage = do
      opts <- m PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions
      return $
        if not (optWithoutK opts) then WithK else
        case optCubical opts of
          Just Cubical
    variant -> Cubical -> Language
    Cubical Cubical
    variant
          Maybe Cubical
    Nothing      -> Language
    WithoutK