Hashes a raw top-level module name.
ModuleAgda-2.8.0.2Haskell2010
Agda.Syntax.TopLevelModuleName
Synopsis
- value hashRawTopLevelModuleName
- value lensTopLevelModuleNameParts
- value moduleNameToFileName
- value projectRoot
- value rawTopLevelModuleName
- value rawTopLevelModuleNameForModule
- value rawTopLevelModuleNameForModuleName
- value rawTopLevelModuleNameForQName
- value rawTopLevelModuleNameToString
- value topLevelModuleNameToQName
- value unsafeTopLevelModuleName
- data RawTopLevelModuleName
- type TopLevelModuleName
- PackageAgda-2.8.0.2
- Exports13
- LanguageHaskell2010
- LicenceMIT
- SourceTopLevelModuleName.hs
A lens focusing on the moduleNameParts.
Turns a top-level module name into a file name with the given suffix.
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.
Converts a top-level module name to a raw top-level module name.
Computes the top-level module name.
Precondition: The Module has to be well-formed.
This means that there are only allowed declarations before the
first module declaration, typically import declarations.
See spanAllowedBeforeModule.
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.
Turns a qualified name into a RawTopLevelModuleName. The qualified name is assumed to represent a top-level module name.
Turns a raw top-level module name into a string.
A corresponding QName. The range of each Name part is the
whole range of the TopLevelModuleName.
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.
Raw top-level module names (with linear-time comparisons).
Constructors
RawTopLevelModuleNamerawModuleNameRange :: RangerawModuleNameParts :: TopLevelModuleNamePartsrawModuleNameInferred :: !BoolWas this module name constructed from a file name rather than declared in the file?
Instances13Eq, Ord, Show, Generic, Pretty, IsNoName, …
Eq RawTopLevelModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.TopLevelModuleNameOrd RawTopLevelModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.TopLevelModuleNameShow RawTopLevelModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.TopLevelModuleNameGeneric RawTopLevelModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.TopLevelModuleNameNFData RawTopLevelModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.TopLevelModuleNameThe Range is not forced.
Pretty RawTopLevelModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.TopLevelModuleNameIsNoName RawTopLevelModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.TopLevelModuleNameSized RawTopLevelModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.TopLevelModuleNameHasRange RawTopLevelModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.TopLevelModuleNameKillRange RawTopLevelModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.TopLevelModuleNameSetRange RawTopLevelModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.TopLevelModuleNameNFData (BiMap RawTopLevelModuleName ModuleNameHash)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base · orphantype Rep RawTopLevelModuleName = D1 ('MetaDataDefined in Agda-2.8.0.2 · Agda.Syntax.TopLevelModuleName"RawTopLevelModuleName"
"Agda.Syntax.TopLevelModuleName"
"Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP"
'False) (C1 ('MetaCons"RawTopLevelModuleName"
'PrefixI 'True) (S1 ('MetaSel ('Just"rawModuleNameRange"
) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: (S1 ('MetaSel ('Just"rawModuleNameParts"
) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TopLevelModuleNameParts) :*: S1 ('MetaSel ('Just"rawModuleNameInferred"
) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bool))))
Top-level module names (with constant-time comparisons).