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).

Constructors

RawTopLevelModuleName 

Fields

Instances

Instances details
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 #

Pretty RawTopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

Methods

pretty :: RawTopLevelModuleName -> Doc Source #

prettyPrec :: Int -> RawTopLevelModuleName -> Doc Source #

prettyList :: [RawTopLevelModuleName] -> Doc Source #

Sized RawTopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

Methods

size :: RawTopLevelModuleName -> Int 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) Source # 
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.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).

Constructors

TopLevelModuleName 

Fields

Instances

Instances details
HasRange TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

Methods

getRange :: TopLevelModuleName -> Range Source #

KillRange TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

Methods

killRange :: KillRangeT TopLevelModuleName Source #

SetRange TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

Methods

setRange :: Range -> TopLevelModuleName -> TopLevelModuleName Source #

PrettyTCM TopLevelModuleName Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => TopLevelModuleName -> m Doc Source #

EmbPrj TopLevelModuleName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: TopLevelModuleName -> S Int32 Source #

icod_ :: TopLevelModuleName -> S Int32 Source #

value :: Int32 -> R TopLevelModuleName Source #

HasTag TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

Associated Types

type Tag TopLevelModuleName Source #

Methods

tag :: TopLevelModuleName -> Maybe (Tag TopLevelModuleName) Source #

Pretty TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

Methods

pretty :: TopLevelModuleName -> Doc Source #

prettyPrec :: Int -> TopLevelModuleName -> Doc Source #

prettyList :: [TopLevelModuleName] -> Doc Source #

Sized TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

Methods

size :: TopLevelModuleName -> Int Source #

Generic TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

Associated Types

type Rep TopLevelModuleName :: Type -> Type #

Methods

from :: TopLevelModuleName -> Rep TopLevelModuleName x #

to :: Rep TopLevelModuleName x -> TopLevelModuleName #

Show TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

Methods

showsPrec :: Int -> TopLevelModuleName -> ShowS #

show :: TopLevelModuleName -> String #

showList :: [TopLevelModuleName] -> ShowS #

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

Methods

(==) :: TopLevelModuleName -> TopLevelModuleName -> Bool #

(/=) :: TopLevelModuleName -> TopLevelModuleName -> Bool #

Ord TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

Methods

compare :: TopLevelModuleName -> TopLevelModuleName -> Ordering #

(<) :: TopLevelModuleName -> TopLevelModuleName -> Bool #

(<=) :: TopLevelModuleName -> TopLevelModuleName -> Bool #

(>) :: TopLevelModuleName -> TopLevelModuleName -> Bool #

(>=) :: TopLevelModuleName -> TopLevelModuleName -> Bool #

max :: TopLevelModuleName -> TopLevelModuleName -> TopLevelModuleName #

min :: TopLevelModuleName -> TopLevelModuleName -> TopLevelModuleName #

Hashable TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

Methods

hashWithSalt :: Int -> TopLevelModuleName -> Int

hash :: TopLevelModuleName -> Int

type Tag TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

type Tag TopLevelModuleName = ModuleNameHash
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))))

lensTopLevelModuleNameParts :: Lens' TopLevelModuleNameParts TopLevelModuleName Source #

A lens focusing on the moduleNameParts.

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.