Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.Syntax.TopLevelModuleName

Contents

Orphan instances

Synopsis

type TopLevelModuleName = TopLevelModuleName' Range
data RawTopLevelModuleName = RawTopLevelModuleName {
- rawModuleNameRange :: Range
- rawModuleNameParts :: TopLevelModuleNameParts
}
projectRoot :: AbsolutePath -> TopLevelModuleName -> AbsolutePath
rawTopLevelModuleNameToString :: RawTopLevelModuleName -> String
hashRawTopLevelModuleName :: RawTopLevelModuleName -> ModuleNameHash
rawTopLevelModuleNameForQName :: QName -> RawTopLevelModuleName
rawTopLevelModuleNameForModuleName :: ModuleName -> RawTopLevelModuleName
rawTopLevelModuleNameForModule :: Module -> RawTopLevelModuleName
rawTopLevelModuleName :: TopLevelModuleName -> RawTopLevelModuleName
lensTopLevelModuleNameParts :: Lens' TopLevelModuleName TopLevelModuleNameParts
unsafeTopLevelModuleName :: RawTopLevelModuleName -> ModuleNameHash -> TopLevelModuleName
topLevelModuleNameToQName :: TopLevelModuleName -> QName
moduleNameToFileName :: TopLevelModuleName -> String -> FilePath
module Agda.Syntax.TopLevelModuleName.Boot

Documentation

type TopLevelModuleName = TopLevelModuleName' Range Source #

Top-level module names (with constant-time comparisons).

data RawTopLevelModuleName Source #

Raw top-level module names (with linear-time comparisons).

Constructors

RawTopLevelModuleName
Fields rawModuleNameRange :: Range rawModuleNameParts :: TopLevelModuleNameParts

Instances

Instances details

Pretty RawTopLevelModuleName Source #
Instance details Defined in Agda.Syntax.TopLevelModuleName Methods pretty :: RawTopLevelModuleName -> Doc Source # prettyPrec :: Int -> RawTopLevelModuleName -> Doc Source # prettyList :: [RawTopLevelModuleName] -> Doc Source #
IsNoName RawTopLevelModuleName Source #
Instance details Defined in Agda.Syntax.TopLevelModuleName Methods isNoName :: RawTopLevelModuleName -> Bool Source #
HasRange RawTopLevelModuleName Source #
Instance details Defined in Agda.Syntax.TopLevelModuleName Methods getRange :: RawTopLevelModuleName -> Range Source #
KillRange RawTopLevelModuleName Source #
Instance details Defined in Agda.Syntax.TopLevelModuleName Methods killRange :: KillRangeT RawTopLevelModuleName Source #
SetRange RawTopLevelModuleName Source #
Instance details Defined in Agda.Syntax.TopLevelModuleName Methods setRange :: Range -> RawTopLevelModuleName -> RawTopLevelModuleName Source #
Sized RawTopLevelModuleName Source #
Instance details Defined in Agda.Syntax.TopLevelModuleName Methods size :: RawTopLevelModuleName -> Int Source # natSize :: RawTopLevelModuleName -> Peano Source #
Generic RawTopLevelModuleName Source #
Instance details Defined in Agda.Syntax.TopLevelModuleName Associated Types type Rep RawTopLevelModuleName :: Type -> Type Methods from :: RawTopLevelModuleName -> Rep RawTopLevelModuleName x to :: Rep RawTopLevelModuleName x -> RawTopLevelModuleName
Show RawTopLevelModuleName Source #
Instance details Defined in Agda.Syntax.TopLevelModuleName Methods showsPrec :: Int -> RawTopLevelModuleName -> ShowS show :: RawTopLevelModuleName -> String showList :: [RawTopLevelModuleName] -> ShowS
NFData RawTopLevelModuleName Source #	The `Range'` is not forced.
Instance details Defined in Agda.Syntax.TopLevelModuleName Methods rnf :: RawTopLevelModuleName -> ()
Eq RawTopLevelModuleName Source #
Instance details Defined in Agda.Syntax.TopLevelModuleName Methods (==) :: RawTopLevelModuleName -> RawTopLevelModuleName -> Bool (/=) :: RawTopLevelModuleName -> RawTopLevelModuleName -> Bool
Ord RawTopLevelModuleName Source #
Instance details Defined in Agda.Syntax.TopLevelModuleName Methods compare :: RawTopLevelModuleName -> RawTopLevelModuleName -> Ordering (<) :: RawTopLevelModuleName -> RawTopLevelModuleName -> Bool (<=) :: RawTopLevelModuleName -> RawTopLevelModuleName -> Bool (>) :: RawTopLevelModuleName -> RawTopLevelModuleName -> Bool (>=) :: RawTopLevelModuleName -> RawTopLevelModuleName -> Bool max :: RawTopLevelModuleName -> RawTopLevelModuleName -> RawTopLevelModuleName min :: RawTopLevelModuleName -> RawTopLevelModuleName -> RawTopLevelModuleName
NFData (BiMap RawTopLevelModuleName ModuleNameHash)
Instance details Defined in Agda.TypeChecking.Monad.Base Methods rnf :: BiMap RawTopLevelModuleName ModuleNameHash -> ()
type Rep RawTopLevelModuleName Source #
Instance details Defined in Agda.Syntax.TopLevelModuleName type Rep RawTopLevelModuleName = D1 ('MetaData "RawTopLevelModuleName" "Agda.Syntax.TopLevelModuleName" "Agda-2.6.4-inplace" 'False) (C1 ('MetaCons "RawTopLevelModuleName" 'PrefixI 'True) (S1 ('MetaSel ('Just "rawModuleNameRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Just "rawModuleNameParts") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TopLevelModuleNameParts)))

projectRoot :: AbsolutePath -> TopLevelModuleName -> AbsolutePath Source #

Finds the current project's "root" directory, given a project file and the corresponding top-level module name.

Example: If the module "A.B.C" is located in the file "fooABC.agda", then the root is "foo".

Precondition: The module name must be well-formed.

rawTopLevelModuleNameToString :: RawTopLevelModuleName -> String Source #

Turns a raw top-level module name into a string.

hashRawTopLevelModuleName :: RawTopLevelModuleName -> ModuleNameHash Source #

Hashes a raw top-level module name.

rawTopLevelModuleNameForQName :: QName -> RawTopLevelModuleName Source #

Turns a qualified name into a RawTopLevelModuleName. The qualified name is assumed to represent a top-level module name.

rawTopLevelModuleNameForModuleName :: ModuleName -> RawTopLevelModuleName Source #

Computes the RawTopLevelModuleName corresponding to the given module name, which is assumed to represent a top-level module name.

Precondition: The module name must be well-formed.

rawTopLevelModuleNameForModule :: Module -> RawTopLevelModuleName Source #

Computes the top-level module name.

Precondition: The Declaration has to be well-formed. This means that there are only allowed declarations before the first module declaration, typically import declarations. See spanAllowedBeforeModule.

rawTopLevelModuleName :: TopLevelModuleName -> RawTopLevelModuleName Source #

Converts a top-level module name to a raw top-level module name.

lensTopLevelModuleNameParts :: Lens' TopLevelModuleName TopLevelModuleNameParts Source #

A lens focusing on the moduleNameParts.

unsafeTopLevelModuleName :: RawTopLevelModuleName -> ModuleNameHash -> TopLevelModuleName Source #

Converts a raw top-level module name and a hash to a top-level module name.

This function does not ensure that there are no hash collisions, that is taken care of by topLevelModuleName.

topLevelModuleNameToQName :: TopLevelModuleName -> QName Source #

A corresponding QName. The range of each Name part is the whole range of the TopLevelModuleName.

moduleNameToFileName :: TopLevelModuleName -> String -> FilePath Source #

Turns a top-level module name into a file name with the given suffix.

module Agda.Syntax.TopLevelModuleName.Boot

Orphan instances

Pretty TopLevelModuleName Source #
Instance details Methods pretty :: TopLevelModuleName -> Doc Source # prettyPrec :: Int -> TopLevelModuleName -> Doc Source # prettyList :: [TopLevelModuleName] -> Doc Source #
Sized TopLevelModuleName Source #
Instance details Methods size :: TopLevelModuleName -> Int Source # natSize :: TopLevelModuleName -> Peano Source #