Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.TopLevelModuleName

Contents

- Orphan instances

Synopsis

- type TopLevelModuleName = TopLevelModuleName' Range
- projectRoot :: AbsolutePath -> TopLevelModuleName -> AbsolutePath
- data RawTopLevelModuleName = RawTopLevelModuleName {
  - rawModuleNameRange :: Range
  - rawModuleNameParts :: TopLevelModuleNameParts
  - rawModuleNameInferred :: !Bool
  }
- rawTopLevelModuleNameToString :: RawTopLevelModuleName -> String
- hashRawTopLevelModuleName :: RawTopLevelModuleName -> ModuleNameHash
- rawTopLevelModuleNameForQName :: QName -> RawTopLevelModuleName
- rawTopLevelModuleNameForModuleName :: ModuleName -> RawTopLevelModuleName
- rawTopLevelModuleNameForModule :: Module -> RawTopLevelModuleName
- rawTopLevelModuleName :: TopLevelModuleName -> RawTopLevelModuleName
- lensTopLevelModuleNameParts :: Lens' TopLevelModuleName TopLevelModuleNameParts
- unsafeTopLevelModuleName :: RawTopLevelModuleName -> ModuleNameHash -> TopLevelModuleName
- topLevelModuleNameToQName :: TopLevelModuleName -> QName
- moduleNameToFileName :: TopLevelModuleName -> String -> FilePath
- module Agda.Syntax.TopLevelModuleName.Boot

# Documentation

type TopLevelModuleName = TopLevelModuleName' Range Source #

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

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.

data RawTopLevelModuleName Source #

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

Constructors

RawTopLevelModuleName |

Fields

- rawModuleNameRange :: Range
- rawModuleNameParts :: TopLevelModuleNameParts
- rawModuleNameInferred :: !Bool

  Was this module name constructed from a file name rather than declared in the file?

#### 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 -> () Source #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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))))

Methods

from :: RawTopLevelModuleName -> Rep RawTopLevelModuleName x Source #

to :: Rep RawTopLevelModuleName x -> RawTopLevelModuleName Source #

Show RawTopLevelModuleName Source # |
Instance details Defined in Agda.Syntax.TopLevelModuleName Methods showsPrec :: Int -> RawTopLevelModuleName -> ShowS Source # show :: RawTopLevelModuleName -> String Source # showList :: [RawTopLevelModuleName] -> ShowS Source #
Eq RawTopLevelModuleName Source # |
Instance details Defined in Agda.Syntax.TopLevelModuleName Methods (==) :: RawTopLevelModuleName -> RawTopLevelModuleName -> Bool Source # (/=) :: RawTopLevelModuleName -> RawTopLevelModuleName -> Bool Source #
Ord RawTopLevelModuleName Source # |

Instance details

Defined in Agda.Syntax.TopLevelModuleName

Methods

compare :: RawTopLevelModuleName -> RawTopLevelModuleName -> Ordering Source #

(<) :: RawTopLevelModuleName -> RawTopLevelModuleName -> Bool Source #

(<=) :: RawTopLevelModuleName -> RawTopLevelModuleName -> Bool Source #

(>) :: RawTopLevelModuleName -> RawTopLevelModuleName -> Bool Source #

(>=) :: RawTopLevelModuleName -> RawTopLevelModuleName -> Bool Source #

max :: RawTopLevelModuleName -> RawTopLevelModuleName -> RawTopLevelModuleName Source #

min :: RawTopLevelModuleName -> RawTopLevelModuleName -> RawTopLevelModuleName Source #

NFData (BiMap RawTopLevelModuleName ModuleNameHash) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods rnf :: BiMap RawTopLevelModuleName ModuleNameHash -> () Source #
type Rep RawTopLevelModuleName Source # |

Instance details

Defined in Agda.Syntax.TopLevelModuleName

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

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

Pretty TopLevelModuleName Source # |
Instance details Methods pretty :: TopLevelModuleName -> Doc Source # prettyPrec :: Int -> TopLevelModuleName -> Doc Source # prettyList :: [TopLevelModuleName] -> Doc Source #
Sized TopLevelModuleName Source # |
Instance details Methods size :: TopLevelModuleName -> Int Source # natSize :: TopLevelModuleName -> Peano Source #