Safe Haskell | None |
---|
This module deals with finding imported modules and loading their interface files.
- mergeInterface :: Interface -> TCM ()
- addImportedThings :: Signature -> BuiltinThings PrimFun -> Set String -> PatternSynDefns -> TCM ()
- scopeCheckImport :: ModuleName -> TCM (ModuleName, Map ModuleName Scope)
- data MaybeWarnings
- hasWarnings :: MaybeWarnings -> Bool
- alreadyVisited :: TopLevelModuleName -> TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
- typeCheckMain :: AbsolutePath -> TCM (Interface, MaybeWarnings)
- typeCheck :: AbsolutePath -> TCM (Interface, MaybeWarnings)
- getInterface :: ModuleName -> TCM Interface
- getInterface_ :: TopLevelModuleName -> TCM Interface
- getInterface' :: TopLevelModuleName -> Bool -> TCM (Interface, MaybeWarnings)
- highlightFromInterface :: Interface -> AbsolutePath -> TCM ()
- readInterface :: FilePath -> TCM (Maybe Interface)
- writeInterface :: FilePath -> Interface -> TCM ()
- createInterface :: AbsolutePath -> TopLevelModuleName -> TCM (Interface, MaybeWarnings)
- buildInterface :: AbsolutePath -> TopLevelInfo -> HighlightingInfo -> Set String -> [OptionsPragma] -> TCM Interface
- getInterfaceFileHashes :: FilePath -> TCM (Maybe (Hash, Hash))
- safeReadInterface :: FilePath -> TCM (Maybe Interface)
- moduleHash :: ModuleName -> TCM Hash
- isNewerThan :: FilePath -> FilePath -> IO Bool
Documentation
mergeInterface :: Interface -> TCM ()Source
Merge an interface into the current proof state.
addImportedThings :: Signature -> BuiltinThings PrimFun -> Set String -> PatternSynDefns -> 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.
hasWarnings :: MaybeWarnings -> BoolSource
alreadyVisited :: TopLevelModuleName -> 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.
typeCheckMain :: AbsolutePath -> TCM (Interface, MaybeWarnings)Source
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, typeCheck
is called to do the main work.
typeCheck :: AbsolutePath -> TCM (Interface, MaybeWarnings)Source
Type checks the given module (if necessary).
Called recursively for imported modules.
getInterface :: ModuleName -> TCM InterfaceSource
Tries to return the interface associated to the given module. The time stamp of the relevant interface file is also returned. May type check the module. An error is raised if a warning is encountered.
:: TopLevelModuleName | |
-> Bool | If type checking is necessary, should all
state changes inflicted by |
-> TCM (Interface, MaybeWarnings) |
A more precise variant of getInterface
. If warnings are
encountered then they are returned instead of being turned into
errors.
:: 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. Returns the file's
new modification time stamp, or Nothing
if the write failed.
:: AbsolutePath | The file to type check. |
-> TopLevelModuleName | The expected module name. |
-> 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.
:: AbsolutePath | |
-> TopLevelInfo |
|
-> HighlightingInfo | Syntax highlighting info for the module. |
-> Set String | Haskell modules imported in imported modules (transitively). |
-> [OptionsPragma] | Options set in |
-> 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)
safeReadInterface :: FilePath -> TCM (Maybe Interface)Source
moduleHash :: ModuleName -> TCM HashSource
isNewerThan :: FilePath -> FilePath -> IO BoolSource
True if the first file is newer than the second file. If a file doesn't exist it is considered to be infinitely old.