Top-level module names (with constant-time comparisons).
ModuleAgda-2.7.0.1Haskell2010
Agda.Syntax.TopLevelModuleName
- 2 types
- 11 values
- PackageAgda-2.7.0.1
- Exports13
- LanguageHaskell2010
- LicenceMIT
- SourceTopLevelModuleName.hs
Raw top-level module names (with linear-time comparisons).
Instances13Eq, Ord, Show, Generic, Pretty, IsNoName, …
Eq RawTopLevelModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.TopLevelModuleNameOrd RawTopLevelModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.TopLevelModuleNameShow RawTopLevelModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.TopLevelModuleNameGeneric RawTopLevelModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.TopLevelModuleNameNFData RawTopLevelModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.TopLevelModuleNameThe Range is not forced.
Pretty RawTopLevelModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.TopLevelModuleNameIsNoName RawTopLevelModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.TopLevelModuleNameHasRange RawTopLevelModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.TopLevelModuleNameKillRange RawTopLevelModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.TopLevelModuleNameSetRange RawTopLevelModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.TopLevelModuleNameSized RawTopLevelModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.TopLevelModuleNameNFData (BiMap RawTopLevelModuleName ModuleNameHash)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Base · orphantype Rep RawTopLevelModuleName = D1 ('MetaDataDefined in Agda-2.7.0.1 · Agda.Syntax.TopLevelModuleName"RawTopLevelModuleName"
"Agda.Syntax.TopLevelModuleName"
"Agda-2.7.0.1-DbbZpETDDF1KkwuzEZvfn8"
'False) (C1 ('MetaCons"RawTopLevelModuleName"
'PrefixI 'True) (S1 ('MetaSel ('Just"rawModuleNameRange"
) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Just"rawModuleNameParts"
) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TopLevelModuleNameParts)))
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.
Turns a raw top-level module name into a string.
Hashes a raw top-level module name.
Turns a qualified name into a RawTopLevelModuleName. The qualified name is assumed to represent a top-level module name.
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.
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.
Converts a top-level module name to a raw top-level module name.
A lens focusing on the moduleNameParts.
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.
A corresponding QName. The range of each Name part is the
whole range of the TopLevelModuleName.
Turns a top-level module name into a file name with the given suffix.