Agda.Unused.Types.Name

Names and qualified names.

Definitions

data NamePart

Mixfix identifiers are composed of words and holes, e.g. _+_ or if_then_else_ or [_/_].

Constructors

Hole

_ part.

Id RawName

Identifier part.

Instances

Eq NamePart

Defined in Agda.Syntax.Concrete.Name

Methods

(==) :: NamePart -> NamePart -> Bool

(/=) :: NamePart -> NamePart -> Bool

Data NamePart

Defined in Agda.Syntax.Concrete.Name

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NamePart -> c NamePart

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NamePart

toConstr :: NamePart -> Constr

dataTypeOf :: NamePart -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NamePart)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NamePart)

gmapT :: (forall b. Data b => b -> b) -> NamePart -> NamePart

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NamePart -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NamePart -> r

gmapQ :: (forall d. Data d => d -> u) -> NamePart -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> NamePart -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> NamePart -> m NamePart

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NamePart -> m NamePart

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NamePart -> m NamePart

Ord NamePart

Defined in Agda.Syntax.Concrete.Name

Methods

compare :: NamePart -> NamePart -> Ordering

(<) :: NamePart -> NamePart -> Bool

(<=) :: NamePart -> NamePart -> Bool

(>) :: NamePart -> NamePart -> Bool

(>=) :: NamePart -> NamePart -> Bool

max :: NamePart -> NamePart -> NamePart

min :: NamePart -> NamePart -> NamePart

Show NamePart

Defined in Agda.Syntax.Concrete.Name

Methods

showsPrec :: Int -> NamePart -> ShowS

show :: NamePart -> String

showList :: [NamePart] -> ShowS

Generic NamePart

Defined in Agda.Syntax.Concrete.Name

Associated Types

type Rep NamePart :: Type -> Type

Methods

from :: NamePart -> Rep NamePart x

to :: Rep NamePart x -> NamePart

Pretty NamePart

Defined in Agda.Syntax.Concrete.Name

Methods

pretty :: NamePart -> Doc

prettyPrec :: Int -> NamePart -> Doc

prettyList :: [NamePart] -> Doc

NFData NamePart

Defined in Agda.Syntax.Concrete.Name

Methods

rnf :: NamePart -> ()

NumHoles [NamePart]

Defined in Agda.Syntax.Concrete.Name

Methods

numHoles :: [NamePart] -> Int

type Rep NamePart

Defined in Agda.Syntax.Concrete.Name

type Rep NamePart = D1 ('MetaData "NamePart" "Agda.Syntax.Concrete.Name" "Agda-2.6.1.3-2WluKmOFu84Cr2Fuyr5biZ" 'False) (C1 ('MetaCons "Hole" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Id" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RawName)))

newtype Name

An unqualified name, represented as a list of name parts.

Constructors

Name

Fields

• nameParts :: [NamePart]

Instances

Eq Name

Defined in Agda.Unused.Types.Name

Methods

(==) :: Name -> Name -> Bool

(/=) :: Name -> Name -> Bool

Ord Name

Defined in Agda.Unused.Types.Name

Methods

compare :: Name -> Name -> Ordering

(<) :: Name -> Name -> Bool

(<=) :: Name -> Name -> Bool

(>) :: Name -> Name -> Bool

(>=) :: Name -> Name -> Bool

max :: Name -> Name -> Name

min :: Name -> Name -> Name

Show Name

Defined in Agda.Unused.Types.Name

Methods

showsPrec :: Int -> Name -> ShowS

show :: Name -> String

showList :: [Name] -> ShowS

data QName where

A qualified name.

Constructors

QName :: !Name -> QName

Qual :: !Name -> !QName -> QName

Instances

Eq QName

Defined in Agda.Unused.Types.Name

Methods

(==) :: QName -> QName -> Bool

(/=) :: QName -> QName -> Bool

Ord QName

Defined in Agda.Unused.Types.Name

Methods

compare :: QName -> QName -> Ordering

(<) :: QName -> QName -> Bool

(<=) :: QName -> QName -> Bool

(>) :: QName -> QName -> Bool

(>=) :: QName -> QName -> Bool

max :: QName -> QName -> QName

min :: QName -> QName -> QName

Show QName

Defined in Agda.Unused.Types.Name

Methods

showsPrec :: Int -> QName -> ShowS

show :: QName -> String

showList :: [QName] -> ShowS

Interface

nameIds :: Name -> [String]

Get the non-hole parts of a Name.

stripPrefix

Arguments

:: QName

The prefix to strip

-> QName

-> Maybe QName

If the first module name is a prefix of the second module name, then strip the prefix, otherwise return Nothing.

Conversion

fromName :: Name -> Maybe Name

Conversion from Agda name type.

fromNameRange :: Name -> Maybe (Range, Name)

Like fromName, but also return a Range.

fromQName :: QName -> Maybe QName

Conversion from Agda qualified name type.

fromQNameRange :: QName -> Maybe (Range, QName)

Like fromQName, but also return a Range.

fromAsName :: AsName -> Maybe Name

Conversion from Agda as-name type.

fromModuleName :: TopLevelModuleName -> Maybe QName

Conversion from Agda top level module name type.

toName :: Name -> Name

Conversion to Agda name type.

toQName :: QName -> QName

Conversion to Agda qualified name type.

Paths

qNamePath :: QName -> FilePath

Convert a module name to a FilePath.

pathQName

Arguments

:: FilePath

The project root directory.

-> FilePath

The path to the module.

-> Maybe QName

Convert a FilePath to a module name.

Match

matchOperators

Arguments

:: [String]

A string of tokens found in a raw application.

-> [Name]

A list of names to consider.

-> [Name]

Given a string of tokens found in a raw application, filter the given list of names by whether each name's identifiers appear in order.