Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Interaction.Imports

Description

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

Synopsis

- data SourceInfo = SourceInfo {
  - siSource :: Text
  - siFileType :: FileType
  - siModule :: Module
  - siModuleName :: TopLevelModuleName
  }
- sourceInfo :: AbsolutePath -> TCM SourceInfo
- data Mode
  - = ScopeCheck
  - | TypeCheck
- data MainInterface
  - = MainInterface Mode
  - | NotMainInterface
- includeStateChanges :: MainInterface -> Bool
- mergeInterface :: Interface -> TCM ()
- addImportedThings :: Signature -> BuiltinThings PrimFun -> PatternSynDefns -> DisplayForms -> Map QName String -> [TCWarning] -> TCM ()
- scopeCheckImport :: ModuleName -> TCM (ModuleName, Map ModuleName Scope)
- data MaybeWarnings' a
  - = NoWarnings
  - | SomeWarnings a
- type MaybeWarnings = MaybeWarnings' [TCWarning]
- applyFlagsToMaybeWarnings :: MaybeWarnings -> TCM MaybeWarnings
- hasWarnings :: MaybeWarnings -> Bool
- alreadyVisited :: TopLevelModuleName -> MainInterface -> PragmaOptions -> TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
- typeCheckMain :: AbsolutePath -> Mode -> SourceInfo -> TCM (Interface, MaybeWarnings)
- getInterface :: ModuleName -> TCM Interface
- getInterface_ :: TopLevelModuleName -> Maybe SourceInfo -> TCM Interface
- getInterface' :: TopLevelModuleName -> MainInterface -> Maybe SourceInfo -> TCM (Interface, MaybeWarnings)
- checkOptionsCompatible :: PragmaOptions -> PragmaOptions -> ModuleName -> TCM Bool
- isCached :: TopLevelModuleName -> AbsolutePath -> MaybeT TCM Interface
- getStoredInterface :: TopLevelModuleName -> AbsolutePath -> MainInterface -> Maybe SourceInfo -> TCM (Bool, (Interface, MaybeWarnings))
- typeCheck :: TopLevelModuleName -> AbsolutePath -> MainInterface -> Maybe SourceInfo -> TCM (Bool, (Interface, MaybeWarnings))
- chaseMsg :: String -> TopLevelModuleName -> Maybe String -> TCM ()
- highlightFromInterface :: Interface -> AbsolutePath -> TCM ()
- readInterface :: FilePath -> TCM (Maybe Interface)
- writeInterface :: FilePath -> Interface -> TCM ()
- removePrivates :: ScopeInfo -> ScopeInfo
- concreteOptionsToOptionPragmas :: [Pragma] -> TCM [OptionsPragma]
- createInterface :: AbsolutePath -> TopLevelModuleName -> MainInterface -> Maybe SourceInfo -> TCM (Interface, MaybeWarnings)
- getUniqueMetasRanges :: [MetaId] -> TCM [Range]
- getUnsolvedMetas :: TCM [Range]
- getAllUnsolved :: TCM [TCWarning]
- getAllWarnings :: WhichWarnings -> TCM [TCWarning]
- getAllWarnings' :: MainInterface -> WhichWarnings -> TCM [TCWarning]
- getMaybeWarnings :: WhichWarnings -> TCM MaybeWarnings
- getMaybeWarnings' :: MainInterface -> WhichWarnings -> TCM MaybeWarnings
- getAllWarningsOfTCErr :: TCErr -> TCM [TCWarning]
- constructIScope :: Interface -> Interface
- buildInterface :: Text -> FileType -> TopLevelInfo -> [OptionsPragma] -> TCM Interface
- getInterfaceFileHashes :: FilePath -> TCM (Maybe (Hash, Hash))
- moduleHash :: ModuleName -> TCM Hash
- isNewerThan :: FilePath -> FilePath -> IO Bool

# Documentation

data SourceInfo Source #

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 :: AbsolutePath -> TCM SourceInfo Source #

Computes a `SourceInfo` record for the given file.

data Mode Source #

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

Constructors

ScopeCheck |
TypeCheck |

Instances

Eq Mode Source # |
Instance details Defined in Agda.Interaction.Imports Methods (==) :: Mode -> Mode -> Bool Source # (/=) :: Mode -> Mode -> Bool Source #
Show Mode Source # |
Instance details Defined in Agda.Interaction.Imports Methods showsPrec :: Int -> Mode -> ShowS Source # show :: Mode -> String Source # showList :: [Mode] -> ShowS Source #

data MainInterface Source #

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 Source # |
Instance details Defined in Agda.Interaction.Imports Methods (==) :: MainInterface -> MainInterface -> Bool Source # (/=) :: MainInterface -> MainInterface -> Bool Source #
Show MainInterface Source # |
Instance details Defined in Agda.Interaction.Imports Methods showsPrec :: Int -> MainInterface -> ShowS Source # show :: MainInterface -> String Source # showList :: [MainInterface] -> ShowS Source #

includeStateChanges :: MainInterface -> Bool Source #

Should state changes inflicted by `createInterface` be preserved?

mergeInterface :: Interface -> TCM () Source #

Merge an interface into the current proof state.

addImportedThings :: Signature -> BuiltinThings PrimFun -> PatternSynDefns -> DisplayForms -> Map QName String -> [TCWarning] -> TCM () Source #

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

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

data MaybeWarnings' a Source #

Constructors

NoWarnings |
SomeWarnings a |

Instances

Functor MaybeWarnings' Source # |
Instance details Defined in Agda.Interaction.Imports Methods fmap :: (a -> b) -> MaybeWarnings' a -> MaybeWarnings' b Source # (<$) :: a -> MaybeWarnings' b -> MaybeWarnings' a Source #
Foldable MaybeWarnings' Source # |

Instance details

Defined in Agda.Interaction.Imports

Methods

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

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

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

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

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

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

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

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

toList :: MaybeWarnings' a -> [a] Source #

null :: MaybeWarnings' a -> Bool Source #

length :: MaybeWarnings' a -> Int Source #

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

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

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

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

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

Traversable MaybeWarnings' Source # |
Instance details Defined in Agda.Interaction.Imports Methods traverse :: Applicative f => (a -> f b) -> MaybeWarnings' a -> f (MaybeWarnings' b) Source # sequenceA :: Applicative f => MaybeWarnings' (f a) -> f (MaybeWarnings' a) Source # mapM :: Monad m => (a -> m b) -> MaybeWarnings' a -> m (MaybeWarnings' b) Source # sequence :: Monad m => MaybeWarnings' (m a) -> m (MaybeWarnings' a) Source #
Show a => Show (MaybeWarnings' a) Source # |
Instance details Defined in Agda.Interaction.Imports Methods showsPrec :: Int -> MaybeWarnings' a -> ShowS Source # show :: MaybeWarnings' a -> String Source # showList :: [MaybeWarnings' a] -> ShowS Source #
Null a => Null (MaybeWarnings' a) Source # |
Instance details Defined in Agda.Interaction.Imports Methods empty :: MaybeWarnings' a Source # null :: MaybeWarnings' a -> Bool Source #

type MaybeWarnings = MaybeWarnings' [TCWarning] Source #

applyFlagsToMaybeWarnings :: MaybeWarnings -> TCM MaybeWarnings Source #

hasWarnings :: MaybeWarnings -> Bool Source #

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

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

Arguments

:: AbsolutePath | 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 Source #

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_ Source #

Arguments

:: TopLevelModuleName |
-> Maybe SourceInfo | Optional information about the source code.
-> TCM Interface |

See `getInterface`.

getInterface' Source #

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

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

isCached Source #

Arguments

:: TopLevelModuleName | Module name of file we process.
-> AbsolutePath | 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 Source #

Arguments

:: TopLevelModuleName | Module name of file we process.
-> AbsolutePath | 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 Source #

Arguments

:: TopLevelModuleName | Module name of file we process.
-> AbsolutePath | 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 Source #

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

Arguments

:: Interface |
-> AbsolutePath | The corresponding file.
-> TCM () |

Print the highlighting information contained in the given interface.

readInterface :: FilePath -> TCM (Maybe Interface) Source #

writeInterface :: FilePath -> Interface -> TCM () Source #

Writes the given interface to the given file.

removePrivates :: ScopeInfo -> ScopeInfo Source #

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

createInterface Source #

Arguments

:: AbsolutePath | 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] Source #

getUnsolvedMetas :: TCM [Range] Source #

getAllUnsolved :: TCM [TCWarning] Source #

getAllWarnings :: WhichWarnings -> TCM [TCWarning] Source #

Collect all warnings that have accumulated in the state.

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

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

getMaybeWarnings :: WhichWarnings -> TCM MaybeWarnings Source #

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

getAllWarningsOfTCErr :: TCErr -> TCM [TCWarning] Source #

constructIScope :: Interface -> Interface Source #

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

buildInterface Source #

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 :: FilePath -> TCM (Maybe (Hash, Hash)) Source #

Returns (iSourceHash, iFullHash)

moduleHash :: ModuleName -> TCM Hash Source #

isNewerThan :: FilePath -> FilePath -> IO Bool Source #

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