Agda.Interaction.Imports

This module deals with finding imported modules and loading their interface files.

Documentation

data SourceInfo

Some information about the source code.

Constructors

SourceInfo

Fields

• siSource :: Text

  Source code.

• siFileType :: FileType

  Source file type

• siModule :: Module

  The parsed module.

• siModuleName :: TopLevelModuleName

  The top-level module name.

sourceInfo :: SourceFile -> TCM SourceInfo

Computes a SourceInfo record for the given file.

data Mode

Is the aim to type-check the top-level module, or only to scope-check it?

Constructors

ScopeCheck

TypeCheck

Instances

Eq Mode

Defined in Agda.Interaction.Imports

Methods

(==) :: Mode -> Mode -> Bool

(/=) :: Mode -> Mode -> Bool

Show Mode

Defined in Agda.Interaction.Imports

Methods

showsPrec :: Int -> Mode -> ShowS

show :: Mode -> String

showList :: [Mode] -> ShowS

data MainInterface

Are we loading the interface for the user-loaded file or for an import?

Constructors

MainInterface Mode

For the main file.

In this case state changes inflicted by createInterface are preserved.

NotMainInterface

For an imported file.

In this case state changes inflicted by createInterface are not preserved.

Instances

Eq MainInterface

Defined in Agda.Interaction.Imports

Methods

(==) :: MainInterface -> MainInterface -> Bool

(/=) :: MainInterface -> MainInterface -> Bool

Show MainInterface

Defined in Agda.Interaction.Imports

Methods

showsPrec :: Int -> MainInterface -> ShowS

show :: MainInterface -> String

showList :: [MainInterface] -> ShowS

includeStateChanges :: MainInterface -> Bool

Should state changes inflicted by createInterface be preserved?

mergeInterface :: Interface -> TCM ()

Merge an interface into the current proof state.

addImportedThings

Arguments

:: Signature

-> BuiltinThings PrimFun

-> PatternSynDefns

-> DisplayForms

-> Map QName String

Imported user warnings

-> Set QName

Name of imported definitions which are partial

-> [TCWarning]

-> TCM ()

scopeCheckImport :: ModuleName -> TCM (ModuleName, Map ModuleName Scope)

Scope checks the given module. A proper version of the module name (with correct definition sites) is returned.

data MaybeWarnings' a

Constructors

NoWarnings

SomeWarnings a

Instances

Functor MaybeWarnings'

Defined in Agda.Interaction.Imports

Methods

fmap :: (a -> b) -> MaybeWarnings' a -> MaybeWarnings' b

(<$) :: a -> MaybeWarnings' b -> MaybeWarnings' a

Foldable MaybeWarnings'

Defined in Agda.Interaction.Imports

Methods

fold :: Monoid m => MaybeWarnings' m -> m

foldMap :: Monoid m => (a -> m) -> MaybeWarnings' a -> m

foldMap' :: Monoid m => (a -> m) -> MaybeWarnings' a -> m

foldr :: (a -> b -> b) -> b -> MaybeWarnings' a -> b

foldr' :: (a -> b -> b) -> b -> MaybeWarnings' a -> b

foldl :: (b -> a -> b) -> b -> MaybeWarnings' a -> b

foldl' :: (b -> a -> b) -> b -> MaybeWarnings' a -> b

foldr1 :: (a -> a -> a) -> MaybeWarnings' a -> a

foldl1 :: (a -> a -> a) -> MaybeWarnings' a -> a

toList :: MaybeWarnings' a -> [a]

null :: MaybeWarnings' a -> Bool

length :: MaybeWarnings' a -> Int

elem :: Eq a => a -> MaybeWarnings' a -> Bool

maximum :: Ord a => MaybeWarnings' a -> a

minimum :: Ord a => MaybeWarnings' a -> a

sum :: Num a => MaybeWarnings' a -> a

product :: Num a => MaybeWarnings' a -> a

Traversable MaybeWarnings'

Defined in Agda.Interaction.Imports

Methods

traverse :: Applicative f => (a -> f b) -> MaybeWarnings' a -> f (MaybeWarnings' b)

sequenceA :: Applicative f => MaybeWarnings' (f a) -> f (MaybeWarnings' a)

mapM :: Monad m => (a -> m b) -> MaybeWarnings' a -> m (MaybeWarnings' b)

sequence :: Monad m => MaybeWarnings' (m a) -> m (MaybeWarnings' a)

Show a => Show (MaybeWarnings' a)

Defined in Agda.Interaction.Imports

Methods

showsPrec :: Int -> MaybeWarnings' a -> ShowS

show :: MaybeWarnings' a -> String

showList :: [MaybeWarnings' a] -> ShowS

Null a => Null (MaybeWarnings' a)

Defined in Agda.Interaction.Imports

Methods

empty :: MaybeWarnings' a

null :: MaybeWarnings' a -> Bool

type MaybeWarnings = MaybeWarnings' [TCWarning]

applyFlagsToMaybeWarnings :: MaybeWarnings -> TCM MaybeWarnings

hasWarnings :: MaybeWarnings -> Bool

alreadyVisited :: TopLevelModuleName -> MainInterface -> PragmaOptions -> TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)

If the module has already been visited (without warnings), then its interface is returned directly. Otherwise the computation is used to find the interface and the computed interface is stored for potential later use (unless the MainInterface is MainInterface ScopeCheck).

typeCheckMain

Arguments

:: SourceFile

The path to the file.

-> Mode

Should the file be type-checked, or only scope-checked?

-> SourceInfo

Information about the source code.

-> TCM (Interface, MaybeWarnings)

Type checks the main file of the interaction. This could be the file loaded in the interacting editor (emacs), or the file passed on the command line.

First, the primitive modules are imported. Then, getInterface' is called to do the main work.

If the Mode is ScopeCheck, then type-checking is not performed, only scope-checking. (This may include type-checking of imported modules.) In this case the generated, partial interface is not stored in the state (stDecodedModules). Note, however, that if the file has already been type-checked, then a complete interface is returned.

getInterface :: ModuleName -> TCM Interface

Tries to return the interface associated to the given (imported) module. The time stamp of the relevant interface file is also returned. Calls itself recursively for the imports of the given module. May type check the module. An error is raised if a warning is encountered.

Do not use this for the main file, use typeCheckMain instead.

getInterface_

Arguments

:: TopLevelModuleName

-> Maybe SourceInfo

Optional information about the source code.

-> TCM Interface

See getInterface.

getInterface'

Arguments

:: TopLevelModuleName

-> MainInterface

-> Maybe SourceInfo

Optional information about the source code.

-> TCM (Interface, MaybeWarnings)

A more precise variant of getInterface. If warnings are encountered then they are returned instead of being turned into errors.

checkOptionsCompatible :: PragmaOptions -> PragmaOptions -> ModuleName -> TCM Bool

Check if the options used for checking an imported module are compatible with the current options. Raises Non-fatal errors if not.

isCached

Arguments

:: TopLevelModuleName

Module name of file we process.

-> SourceFile

File we process.

-> MaybeT TCM Interface

Check whether interface file exists and is in cache in the correct version (as testified by the interface file hash).

getStoredInterface

Arguments

:: TopLevelModuleName

Module name of file we process.

-> SourceFile

File we process.

-> MainInterface

-> Maybe SourceInfo

Optional information about the source code.

-> TCM (Bool, (Interface, MaybeWarnings))

Bool is: do we have to merge the interface?

Try to get the interface from interface file or cache.

typeCheck

Arguments

:: TopLevelModuleName

Module name of file we process.

-> SourceFile

File we process.

-> MainInterface

-> Maybe SourceInfo

Optional information about the source code.

-> TCM (Bool, (Interface, MaybeWarnings))

Bool is: do we have to merge the interface?

Run the type checker on a file and create an interface.

Mostly, this function calls createInterface. But if it is not the main module we check, we do it in a fresh state, suitably initialize, in order to forget some state changes after successful type checking.

chaseMsg

Arguments

:: String

The prefix, like Checking, Finished, Loading .

-> TopLevelModuleName

The module name.

-> Maybe String

Optionally: the file name.

-> TCM ()

Formats and outputs the Checking, Finished and "Loading " messages.

highlightFromInterface

Arguments

:: Interface

-> SourceFile

The corresponding file.

-> TCM ()

Print the highlighting information contained in the given interface.

readInterface :: AbsolutePath -> TCM (Maybe Interface)

Read interface file corresponding to a module.

readInterface' :: InterfaceFile -> TCM (Maybe Interface)

writeInterface :: AbsolutePath -> Interface -> TCM Interface

Writes the given interface to the given file.

The written interface is decoded and returned.

removePrivates :: ScopeInfo -> ScopeInfo

concreteOptionsToOptionPragmas :: [Pragma] -> TCM [OptionsPragma]

createInterface

Arguments

:: SourceFile

The file to type check.

-> TopLevelModuleName

The expected module name.

-> MainInterface

Are we dealing with the main module?

-> Maybe SourceInfo

Optional information about the source code.

-> TCM (Interface, MaybeWarnings)

Tries to type check a module and write out its interface. The function only writes out an interface file if it does not encounter any warnings.

If appropriate this function writes out syntax highlighting information.

getUniqueMetasRanges :: [MetaId] -> TCM [Range]

getUnsolvedMetas :: TCM [Range]

getAllUnsolved :: TCM [TCWarning]

getAllWarnings :: WhichWarnings -> TCM [TCWarning]

Collect all warnings that have accumulated in the state.

getAllWarnings' :: MainInterface -> WhichWarnings -> TCM [TCWarning]

Expert version of getAllWarnings; if isMain is a MainInterface, the warnings definitely include also unsolved warnings.

getMaybeWarnings :: WhichWarnings -> TCM MaybeWarnings

getMaybeWarnings' :: MainInterface -> WhichWarnings -> TCM MaybeWarnings

getAllWarningsOfTCErr :: TCErr -> TCM [TCWarning]

constructIScope :: Interface -> Interface

Reconstruct the iScope (not serialized) from the iInsideScope (serialized).

buildInterface

Arguments

:: Text

Source code.

-> FileType

Agda file? Literate Agda file?

-> TopLevelInfo

TopLevelInfo for the current module.

-> [OptionsPragma]

Options set in OPTIONS pragmas.

-> TCM Interface

Builds an interface for the current module, which should already have been successfully type checked.

getInterfaceFileHashes :: AbsolutePath -> TCM (Maybe (Hash, Hash))

Returns (iSourceHash, iFullHash) We do not need to check that the file exist because we only accept InterfaceFile as an input and not arbitrary AbsolutePath!

getInterfaceFileHashes' :: InterfaceFile -> TCM (Maybe (Hash, Hash))

moduleHash :: ModuleName -> TCM Hash

isNewerThan :: FilePath -> FilePath -> IO Bool

True if the first file is newer than the second file. If a file doesn't exist it is considered to be infinitely old.