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 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
import qualified Agda.Interaction.Options.Lenses as Lens
import Agda.Interaction.Library
import Agda.Interaction.Library.Base (libAbove, libFile)

import Agda.Utils.FileName
import qualified Agda.Utils.Graph.AdjacencyMap.Unidirectional as G
import Agda.Utils.Lens
import Agda.Utils.List
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
$ [FilePath] -> Warning
SafeFlagPragma [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
  AbsolutePath
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)
  AbsolutePath -> CommandLineOptions -> TCM ()
setCommandLineOptions' AbsolutePath
root CommandLineOptions
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.
      [AbsolutePath]
incs <- case CommandLineOptions -> [AbsolutePath]
optAbsoluteIncludePaths CommandLineOptions
opts of
        [] -> do
          CommandLineOptions
opts' <- AbsolutePath -> CommandLineOptions -> TCM CommandLineOptions
setLibraryPaths AbsolutePath
root CommandLineOptions
opts
          let incs :: [FilePath]
incs = CommandLineOptions -> [FilePath]
optIncludePaths CommandLineOptions
opts'
          [FilePath] -> AbsolutePath -> TCM ()
setIncludeDirs [FilePath]
incs AbsolutePath
root
          TCMT IO [AbsolutePath]
forall (m :: * -> *). HasOptions m => m [AbsolutePath]
getIncludeDirs
        [AbsolutePath]
incs -> [AbsolutePath] -> TCMT IO [AbsolutePath]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [AbsolutePath]
incs
      (TCState -> TCState) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC ((TCState -> TCState) -> TCM ()) -> (TCState -> TCState) -> TCM ()
forall a b. (a -> b) -> a -> b
$ CommandLineOptions -> TCState -> TCState
forall a. LensCommandLineOptions a => CommandLineOptions -> a -> a
Lens.setCommandLineOptions CommandLineOptions
opts{ optAbsoluteIncludePaths = incs }
      PragmaOptions -> TCM ()
setPragmaOptions (CommandLineOptions -> PragmaOptions
optPragmaOptions CommandLineOptions
opts)
      TCM ()
updateBenchmarkingStatus

libToTCM :: LibM a -> TCM a
libToTCM :: forall a. LibM a -> TCM a
libToTCM LibM a
m = do
  Map FilePath ProjectConfig
cachedConfs <- Lens' TCState (Map FilePath ProjectConfig)
-> TCMT IO (Map FilePath ProjectConfig)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (Map FilePath ProjectConfig -> f (Map FilePath ProjectConfig))
-> TCState -> f TCState
Lens' TCState (Map FilePath ProjectConfig)
stProjectConfigs
  Map FilePath AgdaLibFile
cachedLibs  <- Lens' TCState (Map FilePath AgdaLibFile)
-> TCMT IO (Map FilePath AgdaLibFile)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (Map FilePath AgdaLibFile -> f (Map FilePath AgdaLibFile))
-> TCState -> f TCState
Lens' TCState (Map FilePath AgdaLibFile)
stAgdaLibFiles

  ((Either LibErrors a
z, [LibWarning]
warns), (Map FilePath ProjectConfig
cachedConfs', Map FilePath AgdaLibFile
cachedLibs')) <- IO
  ((Either LibErrors a, [LibWarning]),
   (Map FilePath ProjectConfig, Map FilePath AgdaLibFile))
-> TCMT
     IO
     ((Either LibErrors a, [LibWarning]),
      (Map FilePath ProjectConfig, Map FilePath AgdaLibFile))
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO
   ((Either LibErrors a, [LibWarning]),
    (Map FilePath ProjectConfig, Map FilePath AgdaLibFile))
 -> TCMT
      IO
      ((Either LibErrors a, [LibWarning]),
       (Map FilePath ProjectConfig, Map FilePath AgdaLibFile)))
-> IO
     ((Either LibErrors a, [LibWarning]),
      (Map FilePath ProjectConfig, Map FilePath AgdaLibFile))
-> TCMT
     IO
     ((Either LibErrors a, [LibWarning]),
      (Map FilePath ProjectConfig, Map FilePath AgdaLibFile))
forall a b. (a -> b) -> a -> b
$
    (StateT
  (Map FilePath ProjectConfig, Map FilePath AgdaLibFile)
  IO
  (Either LibErrors a, [LibWarning])
-> (Map FilePath ProjectConfig, Map FilePath AgdaLibFile)
-> IO
     ((Either LibErrors a, [LibWarning]),
      (Map FilePath ProjectConfig, Map FilePath AgdaLibFile))
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
`runStateT` (Map FilePath ProjectConfig
cachedConfs, Map FilePath AgdaLibFile
cachedLibs)) (StateT
   (Map FilePath ProjectConfig, Map FilePath AgdaLibFile)
   IO
   (Either LibErrors a, [LibWarning])
 -> IO
      ((Either LibErrors a, [LibWarning]),
       (Map FilePath ProjectConfig, Map FilePath AgdaLibFile)))
-> StateT
     (Map FilePath ProjectConfig, Map FilePath AgdaLibFile)
     IO
     (Either LibErrors a, [LibWarning])
-> IO
     ((Either LibErrors a, [LibWarning]),
      (Map FilePath ProjectConfig, Map FilePath AgdaLibFile))
forall a b. (a -> b) -> a -> b
$ WriterT
  [LibWarning]
  (StateT (Map FilePath ProjectConfig, Map FilePath AgdaLibFile) IO)
  (Either LibErrors a)
-> StateT
     (Map FilePath ProjectConfig, Map FilePath AgdaLibFile)
     IO
     (Either LibErrors a, [LibWarning])
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (WriterT
   [LibWarning]
   (StateT (Map FilePath ProjectConfig, Map FilePath AgdaLibFile) IO)
   (Either LibErrors a)
 -> StateT
      (Map FilePath ProjectConfig, Map FilePath AgdaLibFile)
      IO
      (Either LibErrors a, [LibWarning]))
-> WriterT
     [LibWarning]
     (StateT (Map FilePath ProjectConfig, Map FilePath AgdaLibFile) IO)
     (Either LibErrors a)
-> StateT
     (Map FilePath ProjectConfig, Map FilePath AgdaLibFile)
     IO
     (Either LibErrors a, [LibWarning])
forall a b. (a -> b) -> a -> b
$ LibM a
-> WriterT
     [LibWarning]
     (StateT (Map FilePath ProjectConfig, Map FilePath AgdaLibFile) IO)
     (Either LibErrors a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT LibM a
m

  Lens' TCState (Map FilePath ProjectConfig)
-> (Map FilePath ProjectConfig -> Map FilePath ProjectConfig)
-> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
modifyTCLens (Map FilePath ProjectConfig -> f (Map FilePath ProjectConfig))
-> TCState -> f TCState
Lens' TCState (Map FilePath ProjectConfig)
stProjectConfigs ((Map FilePath ProjectConfig -> Map FilePath ProjectConfig)
 -> TCM ())
-> (Map FilePath ProjectConfig -> Map FilePath ProjectConfig)
-> TCM ()
forall a b. (a -> b) -> a -> b
$ Map FilePath ProjectConfig
-> Map FilePath ProjectConfig -> Map FilePath ProjectConfig
forall a b. a -> b -> a
const Map FilePath ProjectConfig
cachedConfs'
  Lens' TCState (Map FilePath AgdaLibFile)
-> (Map FilePath AgdaLibFile -> Map FilePath AgdaLibFile) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
modifyTCLens (Map FilePath AgdaLibFile -> f (Map FilePath AgdaLibFile))
-> TCState -> f TCState
Lens' TCState (Map FilePath AgdaLibFile)
stAgdaLibFiles   ((Map FilePath AgdaLibFile -> Map FilePath AgdaLibFile) -> TCM ())
-> (Map FilePath AgdaLibFile -> Map FilePath AgdaLibFile) -> TCM ()
forall a b. (a -> b) -> a -> b
$ Map FilePath AgdaLibFile
-> Map FilePath AgdaLibFile -> Map FilePath AgdaLibFile
forall a b. a -> b -> a
const Map FilePath AgdaLibFile
cachedLibs'

  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([LibWarning] -> Bool
forall a. Null a => a -> Bool
null [LibWarning]
warns) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Warning] -> TCM ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
[Warning] -> m ()
warnings ([Warning] -> TCM ()) -> [Warning] -> TCM ()
forall a b. (a -> b) -> a -> b
$ (LibWarning -> Warning) -> [LibWarning] -> [Warning]
forall a b. (a -> b) -> [a] -> [b]
map LibWarning -> Warning
LibraryWarning [LibWarning]
warns
  case Either LibErrors a
z of
    Left LibErrors
s  -> TypeError -> TCM a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM a) -> TypeError -> TCM a
forall a b. (a -> b) -> a -> b
$ LibErrors -> TypeError
LibraryError LibErrors
s
    Right a
x -> a -> TCM 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
  [AgdaLibFile]
ls <- AbsolutePath -> TCM [AgdaLibFile]
getAgdaLibFilesWithoutTopLevelModuleName AbsolutePath
f
  (AgdaLibFile -> TCM ()) -> [AgdaLibFile] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TopLevelModuleName -> AgdaLibFile -> TCM ()
checkLibraryFileNotTooFarDown TopLevelModuleName
m) [AgdaLibFile]
ls
  [AgdaLibFile] -> TCM [AgdaLibFile]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [AgdaLibFile]
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
  Bool
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 | Bool
useLibs   -> 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
$ [AgdaLibFile] -> LibErrorIO [AgdaLibFile] -> LibM [AgdaLibFile]
forall a. [AgdaLibFile] -> LibErrorIO a -> LibM a
mkLibM [] (LibErrorIO [AgdaLibFile] -> LibM [AgdaLibFile])
-> LibErrorIO [AgdaLibFile] -> LibM [AgdaLibFile]
forall a b. (a -> b) -> a -> b
$ FilePath -> LibErrorIO [AgdaLibFile]
getAgdaLibFiles' FilePath
root
     | Bool
otherwise -> [AgdaLibFile] -> TCM [AgdaLibFile]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
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
$ FilePath -> TypeError
GenericError (FilePath -> TypeError) -> FilePath -> TypeError
forall a b. (a -> b) -> a -> b
$
    FilePath
"A .agda-lib file for " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ TopLevelModuleName -> FilePath
forall a. Pretty a => a -> FilePath
prettyShow TopLevelModuleName
m FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
    FilePath
" must not be located in the directory " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
    FilePath -> FilePath
takeDirectory (AgdaLibFile
lib AgdaLibFile -> Lens' AgdaLibFile FilePath -> FilePath
forall o i. o -> Lens' o i -> i
^. (FilePath -> f FilePath) -> AgdaLibFile -> f AgdaLibFile
Lens' AgdaLibFile FilePath
libFile)

-- | 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 :: [FilePath]
libs = CommandLineOptions -> [FilePath]
optLibraries CommandLineOptions
o
    [AgdaLibFile]
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)
    [FilePath]
paths     <- LibM [FilePath] -> TCM [FilePath]
forall a. LibM a -> TCM a
libToTCM (LibM [FilePath] -> TCM [FilePath])
-> LibM [FilePath] -> TCM [FilePath]
forall a b. (a -> b) -> a -> b
$ Maybe FilePath -> [AgdaLibFile] -> [FilePath] -> LibM [FilePath]
libraryIncludePaths (CommandLineOptions -> Maybe FilePath
optOverrideLibrariesFile CommandLineOptions
o) [AgdaLibFile]
installed [FilePath]
libs
    CommandLineOptions -> TCM CommandLineOptions
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return CommandLineOptions
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 ([FilePath] -> Bool
forall a. Null a => a -> Bool
null ([FilePath] -> Bool) -> [FilePath] -> Bool
forall a b. (a -> b) -> a -> b
$ CommandLineOptions -> [FilePath]
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
  ([FilePath]
libs, [FilePath]
incs) <- LibM ([FilePath], [FilePath]) -> TCM ([FilePath], [FilePath])
forall a. LibM a -> TCM a
libToTCM (LibM ([FilePath], [FilePath]) -> TCM ([FilePath], [FilePath]))
-> LibM ([FilePath], [FilePath]) -> TCM ([FilePath], [FilePath])
forall a b. (a -> b) -> a -> b
$ FilePath -> Bool -> LibM ([FilePath], [FilePath])
getDefaultLibraries (AbsolutePath -> FilePath
filePath AbsolutePath
root) (CommandLineOptions -> Bool
optDefaultLibs CommandLineOptions
o)
  CommandLineOptions -> TCM CommandLineOptions
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return CommandLineOptions
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
  Map ExeName FilePath
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.
  CommandLineOptions -> TCM CommandLineOptions
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return CommandLineOptions
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
    CommandLineOptions
opts <- TCM CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
    let (Either FilePath PragmaOptions
z, OptionWarnings
warns) = OptM PragmaOptions
-> (Either FilePath PragmaOptions, OptionWarnings)
forall opts. OptM opts -> (Either FilePath opts, OptionWarnings)
runOptM (OptionsPragma -> CommandLineOptions -> OptM PragmaOptions
parsePragmaOptions OptionsPragma
ps CommandLineOptions
opts)
    (OptionWarning -> TCM ()) -> OptionWarnings -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Warning -> TCM ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCM ())
-> (OptionWarning -> Warning) -> OptionWarning -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OptionWarning -> Warning
OptionWarning) OptionWarnings
warns
    case Either FilePath PragmaOptions
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
GenericError 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
          PragmaOptions
oldOpts <- TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
          PragmaOptions -> PragmaOptions -> TCM ()
checkPragmaOptionConsistency PragmaOptions
oldOpts PragmaOptions
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 [AbsolutePath]
getIncludeDirs :: forall (m :: * -> *). HasOptions m => m [AbsolutePath]
getIncludeDirs = do
  [AbsolutePath]
incs <- CommandLineOptions -> [AbsolutePath]
optAbsoluteIncludePaths (CommandLineOptions -> [AbsolutePath])
-> m CommandLineOptions -> m [AbsolutePath]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
  case [AbsolutePath]
incs of
    [] -> m [AbsolutePath]
forall a. HasCallStack => a
__IMPOSSIBLE__
    [AbsolutePath]
_  -> [AbsolutePath] -> m [AbsolutePath]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return [AbsolutePath]
incs

-- | 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
  [AbsolutePath]
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
  [FilePath]
incs <- [FilePath] -> TCM [FilePath]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([FilePath] -> TCM [FilePath]) -> [FilePath] -> TCM [FilePath]
forall a b. (a -> b) -> a -> b
$ if [FilePath] -> Bool
forall a. Null a => a -> Bool
null [FilePath]
incs then [FilePath
"."] else [FilePath]
incs
  -- Make paths absolute
  [AbsolutePath]
incs <- [AbsolutePath] -> TCMT IO [AbsolutePath]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([AbsolutePath] -> TCMT IO [AbsolutePath])
-> [AbsolutePath] -> TCMT IO [AbsolutePath]
forall a b. (a -> b) -> a -> b
$  (FilePath -> AbsolutePath) -> [FilePath] -> [AbsolutePath]
forall a b. (a -> b) -> [a] -> [b]
map (FilePath -> AbsolutePath
mkAbsolute (FilePath -> AbsolutePath)
-> (FilePath -> FilePath) -> FilePath -> AbsolutePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AbsolutePath -> FilePath
filePath AbsolutePath
root FilePath -> FilePath -> FilePath
</>)) [FilePath]
incs

  -- Andreas, 2013-10-30  Add default include dir
      -- NB: This is an absolute file name, but
      -- Agda.Utils.FilePath wants to check absoluteness anyway.
  AbsolutePath
primdir <- IO AbsolutePath -> TCMT IO AbsolutePath
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO AbsolutePath -> TCMT IO AbsolutePath)
-> IO AbsolutePath -> TCMT IO AbsolutePath
forall a b. (a -> b) -> a -> b
$ FilePath -> AbsolutePath
mkAbsolute (FilePath -> AbsolutePath) -> IO FilePath -> IO AbsolutePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO FilePath
getPrimitiveLibDir
      -- 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...
  [AbsolutePath]
incs <- [AbsolutePath] -> TCMT IO [AbsolutePath]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([AbsolutePath] -> TCMT IO [AbsolutePath])
-> [AbsolutePath] -> TCMT IO [AbsolutePath]
forall a b. (a -> b) -> a -> b
$ (AbsolutePath -> AbsolutePath) -> [AbsolutePath] -> [AbsolutePath]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn AbsolutePath -> AbsolutePath
forall a. a -> a
id ([AbsolutePath] -> [AbsolutePath])
-> [AbsolutePath] -> [AbsolutePath]
forall a b. (a -> b) -> a -> b
$ [AbsolutePath]
incs [AbsolutePath] -> [AbsolutePath] -> [AbsolutePath]
forall a. [a] -> [a] -> [a]
++ [AbsolutePath
primdir]

  FilePath -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
FilePath -> Int -> TCM Doc -> m ()
reportSDoc FilePath
"setIncludeDirs" Int
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Doc -> TCM Doc
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> TCM Doc) -> Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
    [ Doc
"Old include directories:"
    , Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (AbsolutePath -> Doc) -> [AbsolutePath] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map AbsolutePath -> Doc
forall a. Pretty a => a -> Doc
pretty [AbsolutePath]
oldIncs
    , Doc
"New include directories:"
    , Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (AbsolutePath -> Doc) -> [AbsolutePath] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map AbsolutePath -> Doc
forall a. Pretty a => a -> Doc
pretty [AbsolutePath]
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".
  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([AbsolutePath] -> [AbsolutePath]
forall a. Ord a => [a] -> [a]
sort [AbsolutePath]
oldIncs [AbsolutePath] -> [AbsolutePath] -> Bool
forall a. Eq a => a -> a -> Bool
/= [AbsolutePath] -> [AbsolutePath]
forall a. Ord a => [a] -> [a]
sort [AbsolutePath]
incs) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    InteractionOutputCallback
ho <- TCMT IO InteractionOutputCallback
forall (m :: * -> *). ReadTCState m => m InteractionOutputCallback
getInteractionOutputCallback
    [TCWarning]
tcWarnings <- Lens' TCState [TCWarning] -> TCMT IO [TCWarning]
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC ([TCWarning] -> f [TCWarning]) -> TCState -> f TCState
Lens' TCState [TCWarning]
stTCWarnings -- restore already generated warnings
    Map FilePath ProjectConfig
projectConfs <- Lens' TCState (Map FilePath ProjectConfig)
-> TCMT IO (Map FilePath ProjectConfig)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (Map FilePath ProjectConfig -> f (Map FilePath ProjectConfig))
-> TCState -> f TCState
Lens' TCState (Map FilePath ProjectConfig)
stProjectConfigs  -- restore cached project configs & .agda-lib
    Map FilePath AgdaLibFile
agdaLibFiles <- Lens' TCState (Map FilePath AgdaLibFile)
-> TCMT IO (Map FilePath AgdaLibFile)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (Map FilePath AgdaLibFile -> f (Map FilePath AgdaLibFile))
-> TCState -> f TCState
Lens' TCState (Map FilePath AgdaLibFile)
stAgdaLibFiles    -- files, since they use absolute paths
    DecodedModules
decodedModules <- TCM DecodedModules
getDecodedModules
    (DecodedModules
keptDecodedModules, ModuleToSource
modFile) <- [AbsolutePath]
-> DecodedModules -> TCM (DecodedModules, ModuleToSource)
modulesToKeep [AbsolutePath]
incs DecodedModules
decodedModules
    TCM ()
resetAllState
    Lens' TCState [TCWarning] -> [TCWarning] -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
setTCLens ([TCWarning] -> f [TCWarning]) -> TCState -> f TCState
Lens' TCState [TCWarning]
stTCWarnings [TCWarning]
tcWarnings
    Lens' TCState (Map FilePath ProjectConfig)
-> Map FilePath ProjectConfig -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
setTCLens (Map FilePath ProjectConfig -> f (Map FilePath ProjectConfig))
-> TCState -> f TCState
Lens' TCState (Map FilePath ProjectConfig)
stProjectConfigs Map FilePath ProjectConfig
projectConfs
    Lens' TCState (Map FilePath AgdaLibFile)
-> Map FilePath AgdaLibFile -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
setTCLens (Map FilePath AgdaLibFile -> f (Map FilePath AgdaLibFile))
-> TCState -> f TCState
Lens' TCState (Map FilePath AgdaLibFile)
stAgdaLibFiles Map FilePath AgdaLibFile
agdaLibFiles
    InteractionOutputCallback -> TCM ()
setInteractionOutputCallback InteractionOutputCallback
ho
    DecodedModules -> TCM ()
setDecodedModules DecodedModules
keptDecodedModules
    Lens' TCState ModuleToSource -> ModuleToSource -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
setTCLens (ModuleToSource -> f ModuleToSource) -> TCState -> f TCState
Lens' TCState ModuleToSource
stModuleToSource ModuleToSource
modFile

  [AbsolutePath] -> TCM ()
forall (m :: * -> *). MonadTCState m => [AbsolutePath] -> m ()
Lens.putAbsoluteIncludePaths [AbsolutePath]
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
    :: [AbsolutePath]  -- New include directories.
    -> DecodedModules  -- Old decoded modules.
    -> TCM (DecodedModules, ModuleToSource)
  modulesToKeep :: [AbsolutePath]
-> DecodedModules -> TCM (DecodedModules, ModuleToSource)
modulesToKeep [AbsolutePath]
incs DecodedModules
old = DecodedModules
-> ModuleToSource
-> [ModuleInfo]
-> TCM (DecodedModules, ModuleToSource)
process DecodedModules
forall k a. Map k a
Map.empty ModuleToSource
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 -> ModuleToSource ->
      [ModuleInfo] -> TCM (DecodedModules, ModuleToSource)
    process :: DecodedModules
-> ModuleToSource
-> [ModuleInfo]
-> TCM (DecodedModules, ModuleToSource)
process !DecodedModules
keep !ModuleToSource
modFile [] = (DecodedModules, ModuleToSource)
-> TCM (DecodedModules, ModuleToSource)
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
      , ModuleToSource
modFile
      )
    process DecodedModules
keep ModuleToSource
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
      (DecodedModules
keep, ModuleToSource
modFile) <-
        if Bool -> Bool
not Bool
depsKept then (DecodedModules, ModuleToSource)
-> TCM (DecodedModules, ModuleToSource)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (DecodedModules
keep, ModuleToSource
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
        Either FindError SourceFile
oldF            <- TopLevelModuleName -> TCM (Either FindError SourceFile)
findFile' TopLevelModuleName
t
        (Either FindError SourceFile
newF, ModuleToSource
modFile) <- IO (Either FindError SourceFile, ModuleToSource)
-> TCMT IO (Either FindError SourceFile, ModuleToSource)
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either FindError SourceFile, ModuleToSource)
 -> TCMT IO (Either FindError SourceFile, ModuleToSource))
-> IO (Either FindError SourceFile, ModuleToSource)
-> TCMT IO (Either FindError SourceFile, ModuleToSource)
forall a b. (a -> b) -> a -> b
$ [AbsolutePath]
-> TopLevelModuleName
-> ModuleToSource
-> IO (Either FindError SourceFile, ModuleToSource)
findFile'' [AbsolutePath]
incs TopLevelModuleName
t ModuleToSource
modFile
        (DecodedModules, ModuleToSource)
-> TCM (DecodedModules, ModuleToSource)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((DecodedModules, ModuleToSource)
 -> TCM (DecodedModules, ModuleToSource))
-> (DecodedModules, ModuleToSource)
-> TCM (DecodedModules, ModuleToSource)
forall a b. (a -> b) -> a -> b
$ case (Either FindError SourceFile
oldF, Either FindError SourceFile
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, ModuleToSource
modFile)
          (Either FindError SourceFile, Either FindError SourceFile)
_ -> (DecodedModules
keep, ModuleToSource
modFile)
      DecodedModules
-> ModuleToSource
-> [ModuleInfo]
-> TCM (DecodedModules, ModuleToSource)
process DecodedModules
keep ModuleToSource
modFile [ModuleInfo]
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
  PragmaOptions
opts <- m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
  Language -> m Language
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Language -> m Language) -> Language -> m Language
forall a b. (a -> b) -> a -> b
$
    if Bool -> Bool
not (PragmaOptions -> Bool
optWithoutK PragmaOptions
opts) then Language
WithK else
    case PragmaOptions -> Maybe Cubical
optCubical PragmaOptions
opts of
      Just Cubical
variant -> Cubical -> Language
Cubical Cubical
variant
      Maybe Cubical
Nothing      -> Language
WithoutK