Safe Haskell	None
Language	Haskell2010

Agda.Syntax.Concrete.Name

Contents

Operations on Name and NamePart
Operations on qualified names
Operations on TopLevelModuleName
No name stuff
Showing names
Printing names
Range instances
NFData instances

Description

Names in the concrete syntax are just strings (or lists of strings for qualified names).

Synopsis

data Name
- = Name Range [NamePart]
- | NoName Range NameId
isOpenMixfix :: Name -> Bool
data NamePart
- = Hole
- | Id RawName
data QName
- = Qual Name QName
- | QName Name
data TopLevelModuleName = TopLevelModuleName {
- moduleNameRange :: Range
- moduleNameParts :: [String]
}
nameToRawName :: Name -> RawName
nameParts :: Name -> [NamePart]
nameStringParts :: Name -> [RawName]
stringNameParts :: String -> [NamePart]
class NumHoles a where
isOperator :: Name -> Bool
isHole :: NamePart -> Bool
isPrefix :: Name -> Bool
isPostfix :: Name -> Bool
isInfix :: Name -> Bool
isNonfix :: Name -> Bool
qualify :: QName -> Name -> QName
unqualify :: QName -> Name
qnameParts :: QName -> [Name]
isQualified :: QName -> Bool
toTopLevelModuleName :: QName -> TopLevelModuleName
moduleNameToFileName :: TopLevelModuleName -> String -> FilePath
projectRoot :: AbsolutePath -> TopLevelModuleName -> AbsolutePath
noName_ :: Name
noName :: Range -> Name
class IsNoName a where

Documentation

data Name #

A name is a non-empty list of alternating Ids and Holes. A normal name is represented by a singleton list, and operators are represented by a list with Holes where the arguments should go. For instance: [Hole,Id "+",Hole] is infix addition.

Equality and ordering on Names are defined to ignore range so same names in different locations are equal.

Constructors

Name Range [NamePart]	A (mixfix) identifier.
NoName Range NameId	`_`.

Instances

Eq Name #	Define equality on `Name` to ignore range so same names in different locations are equal. Is there a reason not to do this? -Jeff No. But there are tons of reasons to do it. For instance, when using names as keys in maps you really don't want to have to get the range right to be able to do a lookup. -Ulf
Instance details Defined in Agda.Syntax.Concrete.Name Methods (==) :: Name -> Name -> Bool # (/=) :: Name -> Name -> Bool #
Data Name #
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) -> Name -> c Name # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Name # toConstr :: Name -> Constr # dataTypeOf :: Name -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Name) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Name) # gmapT :: (forall b. Data b => b -> b) -> Name -> Name # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r # gmapQ :: (forall d. Data d => d -> u) -> Name -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Name -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Name -> m Name # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Name -> m Name # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Name -> m Name #
Ord Name #
Instance details Defined in Agda.Syntax.Concrete.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 #
Instance details Defined in Agda.Syntax.Concrete.Name Methods showsPrec :: Int -> Name -> ShowS # show :: Name -> String # showList :: [Name] -> ShowS #
NFData Name #	Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete.Name Methods rnf :: Name -> () #
Pretty Name #
Instance details Defined in Agda.Syntax.Concrete.Name Methods pretty :: Name -> Doc # prettyPrec :: Int -> Name -> Doc # prettyList :: [Name] -> Doc #
KillRange Name #
Instance details Defined in Agda.Syntax.Concrete.Name Methods killRange :: KillRangeT Name #
SetRange Name #
Instance details Defined in Agda.Syntax.Concrete.Name Methods setRange :: Range -> Name -> Name #
HasRange Name #
Instance details Defined in Agda.Syntax.Concrete.Name Methods getRange :: Name -> Range #
Underscore Name #
Instance details Defined in Agda.Syntax.Concrete.Name Methods underscore :: Name # isUnderscore :: Name -> Bool #
IsNoName Name #
Instance details Defined in Agda.Syntax.Concrete.Name Methods isNoName :: Name -> Bool #
NumHoles Name #
Instance details Defined in Agda.Syntax.Concrete.Name Methods numHoles :: Name -> Int #
ExprLike Name #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> Name -> Name # traverseExpr :: Monad m => (Expr -> m Expr) -> Name -> m Name # foldExpr :: Monoid m => (Expr -> m) -> Name -> m #
SubstExpr Name #
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name0, Expr)] -> Name -> Name #
EmbPrj Name #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Name -> S Int32 # icod_ :: Name -> S Int32 # value :: Int32 -> R Name #
PrettyTCM Name #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Name -> TCM Doc #
ToConcrete Name Name #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: Name -> AbsToCon Name0 # bindToConcrete :: Name -> (Name0 -> AbsToCon b) -> AbsToCon b #
ToConcrete BindName Name #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: BindName -> AbsToCon Name # bindToConcrete :: BindName -> (Name -> AbsToCon b) -> AbsToCon b #
Pretty (ThingWithFixity Name) #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: ThingWithFixity Name -> Doc # prettyPrec :: Int -> ThingWithFixity Name -> Doc # prettyList :: [ThingWithFixity Name] -> Doc #
ToAbstract (NewName Name) Name #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: NewName Name0 -> ScopeM Name #
ToConcrete (Maybe QName) (Maybe Name) #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: Maybe QName -> AbsToCon (Maybe Name) # bindToConcrete :: Maybe QName -> (Maybe Name -> AbsToCon b) -> AbsToCon b #

isOpenMixfix :: Name -> Bool #

An open mixfix identifier is either prefix, infix, or suffix. That is to say: at least one of its extremities is a Hole

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 #
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 :: (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 :: * -> * # Methods from :: NamePart -> Rep NamePart x # to :: Rep NamePart x -> NamePart #
NFData NamePart #
Instance details Defined in Agda.Syntax.Concrete.Name Methods rnf :: NamePart -> () #
Pretty NamePart #
Instance details Defined in Agda.Syntax.Concrete.Name Methods pretty :: NamePart -> Doc # prettyPrec :: Int -> NamePart -> Doc # prettyList :: [NamePart] -> Doc #
EmbPrj NamePart #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: NamePart -> S Int32 # icod_ :: NamePart -> S Int32 # value :: Int32 -> R 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.5.4-BdDHVHYPm5JDI57G7c5E26" False) (C1 (MetaCons "Hole" PrefixI False) (U1 :: * -> *) :+: C1 (MetaCons "Id" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 RawName)))

data QName #

QName is a list of namespaces and the name of the constant. For the moment assumes namespaces are just Names and not explicitly applied modules. Also assumes namespaces are generative by just using derived equality. We will have to define an equality instance to non-generative namespaces (as well as having some sort of lookup table for namespace names).

Constructors

Qual Name QName	`A.rest`.
QName Name	`x`.

Instances

Eq QName #
Instance details Defined in Agda.Syntax.Concrete.Name Methods (==) :: QName -> QName -> Bool # (/=) :: QName -> QName -> Bool #
Data QName #
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) -> QName -> c QName # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c QName # toConstr :: QName -> Constr # dataTypeOf :: QName -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c QName) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QName) # gmapT :: (forall b. Data b => b -> b) -> QName -> QName # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QName -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QName -> r # gmapQ :: (forall d. Data d => d -> u) -> QName -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> QName -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> QName -> m QName # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> QName -> m QName # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> QName -> m QName #
Ord QName #
Instance details Defined in Agda.Syntax.Concrete.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 #
Instance details Defined in Agda.Syntax.Concrete.Name Methods showsPrec :: Int -> QName -> ShowS # show :: QName -> String # showList :: [QName] -> ShowS #
NFData QName #
Instance details Defined in Agda.Syntax.Concrete.Name Methods rnf :: QName -> () #
Pretty QName #
Instance details Defined in Agda.Syntax.Concrete.Name Methods pretty :: QName -> Doc # prettyPrec :: Int -> QName -> Doc # prettyList :: [QName] -> Doc #
KillRange QName #
Instance details Defined in Agda.Syntax.Concrete.Name Methods killRange :: KillRangeT QName #
SetRange QName #
Instance details Defined in Agda.Syntax.Concrete.Name Methods setRange :: Range -> QName -> QName #
HasRange QName #
Instance details Defined in Agda.Syntax.Concrete.Name Methods getRange :: QName -> Range #
Underscore QName #
Instance details Defined in Agda.Syntax.Concrete.Name Methods underscore :: QName # isUnderscore :: QName -> Bool #
IsNoName QName #
Instance details Defined in Agda.Syntax.Concrete.Name Methods isNoName :: QName -> Bool #
NumHoles QName #
Instance details Defined in Agda.Syntax.Concrete.Name Methods numHoles :: QName -> Int #
ExprLike QName #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> QName -> QName # traverseExpr :: Monad m => (Expr -> m Expr) -> QName -> m QName # foldExpr :: Monoid m => (Expr -> m) -> QName -> m #
EmbPrj QName #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: QName -> S Int32 # icod_ :: QName -> S Int32 # value :: Int32 -> R QName #
PrettyTCM QName #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: QName -> TCM Doc #
ToConcrete ModuleName QName #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: ModuleName -> AbsToCon QName # bindToConcrete :: ModuleName -> (QName -> AbsToCon b) -> AbsToCon b #
ToConcrete QName QName #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: QName -> AbsToCon QName0 # bindToConcrete :: QName -> (QName0 -> AbsToCon b) -> AbsToCon b #
ToConcrete ResolvedName QName #	Assumes name is not `UnknownName`.
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: ResolvedName -> AbsToCon QName # bindToConcrete :: ResolvedName -> (QName -> AbsToCon b) -> AbsToCon b #
ToConcrete AbstractName QName #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: AbstractName -> AbsToCon QName # bindToConcrete :: AbstractName -> (QName -> AbsToCon b) -> AbsToCon b #

data TopLevelModuleName #

Top-level module names. Used in connection with the file system.

Invariant: The list must not be empty.

Constructors

TopLevelModuleName
Fields moduleNameRange :: Range moduleNameParts :: [String]

Instances

Eq TopLevelModuleName #
Instance details Defined in Agda.Syntax.Concrete.Name Methods (==) :: TopLevelModuleName -> TopLevelModuleName -> Bool # (/=) :: TopLevelModuleName -> TopLevelModuleName -> Bool #
Data TopLevelModuleName #
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) -> TopLevelModuleName -> c TopLevelModuleName # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TopLevelModuleName # toConstr :: TopLevelModuleName -> Constr # dataTypeOf :: TopLevelModuleName -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TopLevelModuleName) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TopLevelModuleName) # gmapT :: (forall b. Data b => b -> b) -> TopLevelModuleName -> TopLevelModuleName # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TopLevelModuleName -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TopLevelModuleName -> r # gmapQ :: (forall d. Data d => d -> u) -> TopLevelModuleName -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> TopLevelModuleName -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> TopLevelModuleName -> m TopLevelModuleName # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TopLevelModuleName -> m TopLevelModuleName # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TopLevelModuleName -> m TopLevelModuleName #
Ord TopLevelModuleName #
Instance details Defined in Agda.Syntax.Concrete.Name 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 #
Show TopLevelModuleName #
Instance details Defined in Agda.Syntax.Concrete.Name Methods showsPrec :: Int -> TopLevelModuleName -> ShowS # show :: TopLevelModuleName -> String # showList :: [TopLevelModuleName] -> ShowS #
Pretty TopLevelModuleName #
Instance details Defined in Agda.Syntax.Concrete.Name Methods pretty :: TopLevelModuleName -> Doc # prettyPrec :: Int -> TopLevelModuleName -> Doc # prettyList :: [TopLevelModuleName] -> Doc #
Sized TopLevelModuleName #
Instance details Defined in Agda.Syntax.Concrete.Name Methods size :: TopLevelModuleName -> Int #
KillRange TopLevelModuleName #
Instance details Defined in Agda.Syntax.Concrete.Name Methods killRange :: KillRangeT TopLevelModuleName #
SetRange TopLevelModuleName #
Instance details Defined in Agda.Syntax.Concrete.Name Methods setRange :: Range -> TopLevelModuleName -> TopLevelModuleName #
HasRange TopLevelModuleName #
Instance details Defined in Agda.Syntax.Concrete.Name Methods getRange :: TopLevelModuleName -> Range #
EmbPrj TopLevelModuleName #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: TopLevelModuleName -> S Int32 # icod_ :: TopLevelModuleName -> S Int32 # value :: Int32 -> R TopLevelModuleName #

Operations on `Name` and `NamePart`

nameToRawName :: Name -> RawName #

nameParts :: Name -> [NamePart] #

nameStringParts :: Name -> [RawName] #

stringNameParts :: String -> [NamePart] #

Parse a string to parts of a concrete name.

Note: stringNameParts "_" == [Id "_"] == nameParts NoName{}

class NumHoles a where #

Number of holes in a Name (i.e., arity of a mixfix-operator).

Minimal complete definition

numHoles

Methods

numHoles :: a -> Int #

Instances

NumHoles QName #
Instance details Defined in Agda.Syntax.Concrete.Name Methods numHoles :: QName -> Int #
NumHoles Name #
Instance details Defined in Agda.Syntax.Concrete.Name Methods numHoles :: Name -> Int #
NumHoles AmbiguousQName #	We can have an instance for ambiguous names as all share a common concrete name.
Instance details Defined in Agda.Syntax.Abstract.Name Methods numHoles :: AmbiguousQName -> Int #
NumHoles QName #
Instance details Defined in Agda.Syntax.Abstract.Name Methods numHoles :: QName -> Int #
NumHoles Name #
Instance details Defined in Agda.Syntax.Abstract.Name Methods numHoles :: Name -> Int #
NumHoles [NamePart] #
Instance details Defined in Agda.Syntax.Concrete.Name Methods numHoles :: [NamePart] -> Int #

isOperator :: Name -> Bool #

Is the name an operator?

isHole :: NamePart -> Bool #

isPrefix :: Name -> Bool #

isPostfix :: Name -> Bool #

isInfix :: Name -> Bool #

isNonfix :: Name -> Bool #

Operations on qualified names

qualify :: QName -> Name -> QName #

qualify A.B x == A.B.x

unqualify :: QName -> Name #

unqualify A.B.x == x

The range is preserved.

qnameParts :: QName -> [Name] #

qnameParts A.B.x = [A, B, x]

isQualified :: QName -> Bool #

Is the name qualified?

Operations on `TopLevelModuleName`

toTopLevelModuleName :: QName -> TopLevelModuleName #

Turns a qualified name into a TopLevelModuleName. The qualified name is assumed to represent a top-level module name.

moduleNameToFileName :: TopLevelModuleName -> String -> FilePath #

Turns a top-level module name into a file name with the given suffix.

projectRoot :: AbsolutePath -> TopLevelModuleName -> AbsolutePath #

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.

No name stuff

noName_ :: Name #

noName_ = noName noRange

noName :: Range -> Name #

class IsNoName a where #

Check whether a name is the empty name "_".

Minimal complete definition

isNoName

Methods

isNoName :: a -> Bool #

Instances

IsNoName String #
Instance details Defined in Agda.Syntax.Concrete.Name Methods isNoName :: String -> Bool #
IsNoName ByteString #
Instance details Defined in Agda.Syntax.Concrete.Name Methods isNoName :: ByteString -> Bool #
IsNoName QName #
Instance details Defined in Agda.Syntax.Concrete.Name Methods isNoName :: QName -> Bool #
IsNoName Name #
Instance details Defined in Agda.Syntax.Concrete.Name Methods isNoName :: Name -> Bool #
IsNoName Name #	An abstract name is empty if its concrete name is empty.
Instance details Defined in Agda.Syntax.Abstract.Name Methods isNoName :: Name -> Bool #

Documentation

Operations on Name and NamePart

Operations on qualified names

Operations on TopLevelModuleName

No name stuff

Showing names

Printing names

Range instances

NFData instances

Operations on `Name` and `NamePart`

Operations on `TopLevelModuleName`