Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.TopLevelModuleName

Synopsis

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

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 #

NFData RawTopLevelModuleName Source #

The Range is not forced.

Instance details

Defined in Agda.Syntax.TopLevelModuleName

Methods

rnf :: RawTopLevelModuleName -> ()

Generic RawTopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

Associated Types

type Rep RawTopLevelModuleName 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

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

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

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.20240714-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 Module 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