Safe Haskell	None
Language	Haskell2010

Agda.Unused.Types.Name

Contents

Definitions
Interface
Conversion
Paths
Match

Description

Names and qualified names.

Synopsis

data NamePart
- = Hole
- | Id RawName
newtype Name = Name {
- nameParts :: [NamePart]
}
data QName where
- QName :: !Name -> QName
- Qual :: !Name -> !QName -> QName
nameIds :: Name -> [String]
stripPrefix :: QName -> QName -> Maybe QName
fromName :: Name -> Maybe Name
fromNameRange :: Name -> Maybe (Range, Name)
fromQName :: QName -> Maybe QName
fromQNameRange :: QName -> Maybe (Range, QName)
fromAsName :: AsName -> Maybe Name
fromModuleName :: TopLevelModuleName -> Maybe QName
toName :: Name -> Name
toQName :: QName -> QName
qNamePath :: QName -> FilePath
pathQName :: FilePath -> FilePath -> Maybe QName
matchOperators :: [String] -> [Name] -> [Name]

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

Instances details

Eq NamePart
Instance details Defined in Agda.Syntax.Concrete.Name Methods (==) :: NamePart -> NamePart -> Bool # (/=) :: NamePart -> NamePart -> Bool #
Data NamePart
Instance details 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
Instance details 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
Instance details Defined in Agda.Syntax.Concrete.Name Methods showsPrec :: Int -> NamePart -> ShowS # show :: NamePart -> String # showList :: [NamePart] -> ShowS #
Generic NamePart
Instance details 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
Instance details Defined in Agda.Syntax.Concrete.Name Methods pretty :: NamePart -> Doc # prettyPrec :: Int -> NamePart -> Doc # prettyList :: [NamePart] -> Doc #
NFData NamePart
Instance details Defined in Agda.Syntax.Concrete.Name Methods rnf :: NamePart -> () #
NumHoles [NamePart]
Instance details Defined in Agda.Syntax.Concrete.Name Methods numHoles :: [NamePart] -> Int #
type Rep NamePart
Instance details 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 Source #

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

Constructors

Name
Fields nameParts :: [NamePart]

Instances

Instances details

Eq Name Source #
Instance details Defined in Agda.Unused.Types.Name Methods (==) :: Name -> Name -> Bool # (/=) :: Name -> Name -> Bool #
Ord Name Source #
Instance details 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 Source #
Instance details Defined in Agda.Unused.Types.Name Methods showsPrec :: Int -> Name -> ShowS # show :: Name -> String # showList :: [Name] -> ShowS #

data QName where Source #

A qualified name.

Constructors

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

Instances

Instances details

Eq QName Source #
Instance details Defined in Agda.Unused.Types.Name Methods (==) :: QName -> QName -> Bool # (/=) :: QName -> QName -> Bool #
Ord QName Source #
Instance details 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 Source #
Instance details Defined in Agda.Unused.Types.Name Methods showsPrec :: Int -> QName -> ShowS # show :: QName -> String # showList :: [QName] -> ShowS #