Agda-2.6.2.2.20230105: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Syntax.TopLevelModuleName

Synopsis

Documentation

type TopLevelModuleNameParts = List1 Text Source #

A top-level module name has one or more name parts.

data RawTopLevelModuleName Source #

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

Instances

Instances details
IsNoName RawTopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

HasRange RawTopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

KillRange RawTopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

SetRange RawTopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

Pretty RawTopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

Sized RawTopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

Generic RawTopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

Associated Types

type Rep RawTopLevelModuleName :: Type -> Type #

Show RawTopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

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

Ord RawTopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

NFData (BiMap RawTopLevelModuleName ModuleNameHash) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

type Rep RawTopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

type Rep RawTopLevelModuleName = D1 ('MetaData "RawTopLevelModuleName" "Agda.Syntax.TopLevelModuleName" "Agda-2.6.2.2.20230105-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)))

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.

data TopLevelModuleName Source #

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

Instances

Instances details
HasRange TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

KillRange TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

SetRange TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

PrettyTCM TopLevelModuleName Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

EmbPrj TopLevelModuleName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

HasTag TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

Associated Types

type Tag TopLevelModuleName Source #

Pretty TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

Sized TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

Generic TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

Associated Types

type Rep TopLevelModuleName :: Type -> Type #

Show TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

NFData TopLevelModuleName Source #

The Range' is not forced.

Instance details

Defined in Agda.Syntax.TopLevelModuleName

Methods

rnf :: TopLevelModuleName -> () #

Eq TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

Ord TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

Hashable TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

type Tag TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

type Rep TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

type Rep TopLevelModuleName = D1 ('MetaData "TopLevelModuleName" "Agda.Syntax.TopLevelModuleName" "Agda-2.6.2.2.20230105-inplace" 'False) (C1 ('MetaCons "TopLevelModuleName" 'PrefixI 'True) (S1 ('MetaSel ('Just "moduleNameRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: (S1 ('MetaSel ('Just "moduleNameId") 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 ModuleNameHash) :*: S1 ('MetaSel ('Just "moduleNameParts") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TopLevelModuleNameParts))))

rawTopLevelModuleName :: TopLevelModuleName -> RawTopLevelModuleName Source #

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

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.

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.