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

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Concrete.Name

Contents

- Operations on `Name` and `NamePart`
- Keeping track of which names are (not) in scope
- Generating fresh names
- 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 {
    - nameRange :: Range
    - nameInScope :: NameInScope
    - nameNameParts :: [NamePart]
    }
  - | NoName {
    - nameRange :: Range
    - nameId :: 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
  - numHoles :: a -> Int
- isOperator :: Name -> Bool
- isHole :: NamePart -> Bool
- isPrefix :: Name -> Bool
- isPostfix :: Name -> Bool
- isInfix :: Name -> Bool
- isNonfix :: Name -> Bool
- data NameInScope
  - = InScope
  - | NotInScope
- class LensInScope a where
  - lensInScope :: Lens' NameInScope a
  - isInScope :: a -> NameInScope
  - mapInScope :: (NameInScope -> NameInScope) -> a -> a
  - setInScope :: a -> a
  - setNotInScope :: a -> a
- nextStr :: String -> String
- nextName :: Name -> Name
- firstNonTakenName :: (Name -> Bool) -> Name -> Name
- nameRoot :: Name -> RawName
- sameRoot :: Name -> 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
  - isNoName :: a -> Bool

# Documentation

data Name Source #

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

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

Constructors

Name | A (mixfix) identifier.

Fields

- nameRange :: Range
- nameInScope :: NameInScope
- nameNameParts :: [NamePart]

NoName | `_`.

Fields

- nameRange :: Range
- nameId :: NameId

Instances

Eq Name Source # | 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 Source # (/=) :: Name -> Name -> Bool Source #
Data Name Source # |

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 Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Name Source #

toConstr :: Name -> Constr Source #

dataTypeOf :: Name -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Name) Source #

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

gmapT :: (forall b. Data b => b -> b) -> Name -> Name Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Name -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Name -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Name -> m Name Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Name -> m Name Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Name -> m Name Source #

Ord Name Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods compare :: Name -> Name -> Ordering Source # (<) :: Name -> Name -> Bool Source # (<=) :: Name -> Name -> Bool Source # (>) :: Name -> Name -> Bool Source # (>=) :: Name -> Name -> Bool Source # max :: Name -> Name -> Name Source # min :: Name -> Name -> Name Source #
Show Name Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods showsPrec :: Int -> Name -> ShowS Source # show :: Name -> String Source # showList :: [Name] -> ShowS Source #
NFData Name Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods rnf :: Name -> () Source #
NFData AsName Source # | Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: AsName -> () Source #
Pretty Name Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods pretty :: Name -> Doc Source # prettyPrec :: Int -> Name -> Doc Source # prettyList :: [Name] -> Doc Source #
KillRange Name Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods killRange :: KillRangeT Name Source #
KillRange AsName Source # |
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT AsName Source #
SetRange Name Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods setRange :: Range -> Name -> Name Source #
HasRange Name Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods getRange :: Name -> Range Source #
HasRange AsName Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: AsName -> Range Source #
Underscore Name Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods underscore :: Name Source # isUnderscore :: Name -> Bool Source #
IsNoName Name Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods isNoName :: Name -> Bool Source #
LensInScope Name Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods lensInScope :: Lens' NameInScope Name Source # isInScope :: Name -> NameInScope Source # mapInScope :: (NameInScope -> NameInScope) -> Name -> Name Source # setInScope :: Name -> Name Source # setNotInScope :: Name -> Name Source #
NumHoles Name Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods numHoles :: Name -> Int Source #
ExprLike Name Source # |
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> Name -> Name Source # traverseExpr :: Monad m => (Expr -> m Expr) -> Name -> m Name Source # foldExpr :: Monoid m => (Expr -> m) -> Name -> m Source #
SubstExpr Name Source # |
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name0, Expr)] -> Name -> Name Source #
EmbPrj Name Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Name -> S Int32 Source # icod_ :: Name -> S Int32 Source # value :: Int32 -> R Name Source #
PrettyTCM Name Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Name -> TCM Doc Source #
ToConcrete Name Name Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: Name -> AbsToCon Name0 Source # bindToConcrete :: Name -> (Name0 -> AbsToCon b) -> AbsToCon b Source #
Pretty (ThingWithFixity Name) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: ThingWithFixity Name -> Doc Source # prettyPrec :: Int -> ThingWithFixity Name -> Doc Source # prettyList :: [ThingWithFixity Name] -> Doc Source #
ToAbstract (NewName Name) Name Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: NewName Name0 -> ScopeM Name Source #
ToConcrete (Maybe QName) (Maybe Name) Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: Maybe QName -> AbsToCon (Maybe Name) Source # bindToConcrete :: Maybe QName -> (Maybe Name -> AbsToCon b) -> AbsToCon b Source #

isOpenMixfix :: Name -> Bool Source #

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 Source #

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 Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods (==) :: NamePart -> NamePart -> Bool Source # (/=) :: NamePart -> NamePart -> Bool Source #
Data NamePart Source # |

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 Source #

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

toConstr :: NamePart -> Constr Source #

dataTypeOf :: NamePart -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Ord NamePart Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods compare :: NamePart -> NamePart -> Ordering Source # (<) :: NamePart -> NamePart -> Bool Source # (<=) :: NamePart -> NamePart -> Bool Source # (>) :: NamePart -> NamePart -> Bool Source # (>=) :: NamePart -> NamePart -> Bool Source # max :: NamePart -> NamePart -> NamePart Source # min :: NamePart -> NamePart -> NamePart Source #
Show NamePart Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods showsPrec :: Int -> NamePart -> ShowS Source # show :: NamePart -> String Source # showList :: [NamePart] -> ShowS Source #
Generic NamePart Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Associated Types type Rep NamePart :: Type -> Type Source # Methods from :: NamePart -> Rep NamePart x Source # to :: Rep NamePart x -> NamePart Source #
NFData NamePart Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods rnf :: NamePart -> () Source #
Pretty NamePart Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods pretty :: NamePart -> Doc Source # prettyPrec :: Int -> NamePart -> Doc Source # prettyList :: [NamePart] -> Doc Source #
EmbPrj NamePart Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: NamePart -> S Int32 Source # icod_ :: NamePart -> S Int32 Source # value :: Int32 -> R NamePart Source #
NumHoles [NamePart] Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods numHoles :: [NamePart] -> Int Source #
type Rep NamePart Source # |
Instance details Defined in Agda.Syntax.Concrete.Name type Rep NamePart = D1 (MetaData "NamePart" "Agda.Syntax.Concrete.Name" "Agda-2.6.0.1-1X7fHcR3xPHzuc9vp1IMb" False) (C1 (MetaCons "Hole" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Id" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 RawName)))

data QName Source #

`QName` is a list of namespaces and the name of the constant. For the moment assumes namespaces are just `Name`s 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 Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods (==) :: QName -> QName -> Bool Source # (/=) :: QName -> QName -> Bool Source #
Data QName Source # |

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 Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c QName Source #

toConstr :: QName -> Constr Source #

dataTypeOf :: QName -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c QName) Source #

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

gmapT :: (forall b. Data b => b -> b) -> QName -> QName Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QName -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QName -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> QName -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> QName -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> QName -> m QName Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> QName -> m QName Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> QName -> m QName Source #

Ord QName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods compare :: QName -> QName -> Ordering Source # (<) :: QName -> QName -> Bool Source # (<=) :: QName -> QName -> Bool Source # (>) :: QName -> QName -> Bool Source # (>=) :: QName -> QName -> Bool Source # max :: QName -> QName -> QName Source # min :: QName -> QName -> QName Source #
Show QName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods showsPrec :: Int -> QName -> ShowS Source # show :: QName -> String Source # showList :: [QName] -> ShowS Source #
NFData QName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods rnf :: QName -> () Source #
Pretty QName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods pretty :: QName -> Doc Source # prettyPrec :: Int -> QName -> Doc Source # prettyList :: [QName] -> Doc Source #
KillRange QName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods killRange :: KillRangeT QName Source #
SetRange QName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods setRange :: Range -> QName -> QName Source #
HasRange QName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods getRange :: QName -> Range Source #
Underscore QName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods underscore :: QName Source # isUnderscore :: QName -> Bool Source #
IsNoName QName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods isNoName :: QName -> Bool Source #
LensInScope QName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods lensInScope :: Lens' NameInScope QName Source # isInScope :: QName -> NameInScope Source # mapInScope :: (NameInScope -> NameInScope) -> QName -> QName Source # setInScope :: QName -> QName Source # setNotInScope :: QName -> QName Source #
NumHoles QName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods numHoles :: QName -> Int Source #
ExprLike QName Source # |
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> QName -> QName Source # traverseExpr :: Monad m => (Expr -> m Expr) -> QName -> m QName Source # foldExpr :: Monoid m => (Expr -> m) -> QName -> m Source #
EmbPrj QName Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: QName -> S Int32 Source # icod_ :: QName -> S Int32 Source # value :: Int32 -> R QName Source #
PrettyTCM QName Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: QName -> TCM Doc Source #
ToConcrete ModuleName QName Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: ModuleName -> AbsToCon QName Source # bindToConcrete :: ModuleName -> (QName -> AbsToCon b) -> AbsToCon b Source #
ToConcrete QName QName Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: QName -> AbsToCon QName0 Source # bindToConcrete :: QName -> (QName0 -> AbsToCon b) -> AbsToCon b Source #
ToConcrete ResolvedName QName Source # | Assumes name is not `UnknownName`.
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: ResolvedName -> AbsToCon QName Source # bindToConcrete :: ResolvedName -> (QName -> AbsToCon b) -> AbsToCon b Source #
ToConcrete AbstractName QName Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: AbstractName -> AbsToCon QName Source # bindToConcrete :: AbstractName -> (QName -> AbsToCon b) -> AbsToCon b Source #

data TopLevelModuleName Source #

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 Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods (==) :: TopLevelModuleName -> TopLevelModuleName -> Bool Source # (/=) :: TopLevelModuleName -> TopLevelModuleName -> Bool Source #
Data TopLevelModuleName Source # |

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 Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TopLevelModuleName Source #

toConstr :: TopLevelModuleName -> Constr Source #

dataTypeOf :: TopLevelModuleName -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TopLevelModuleName) Source #

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

gmapT :: (forall b. Data b => b -> b) -> TopLevelModuleName -> TopLevelModuleName Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TopLevelModuleName -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TopLevelModuleName -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> TopLevelModuleName -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> TopLevelModuleName -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> TopLevelModuleName -> m TopLevelModuleName Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TopLevelModuleName -> m TopLevelModuleName Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TopLevelModuleName -> m TopLevelModuleName Source #

Ord TopLevelModuleName Source # |

Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

compare :: TopLevelModuleName -> TopLevelModuleName -> Ordering Source #

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

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

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

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

max :: TopLevelModuleName -> TopLevelModuleName -> TopLevelModuleName Source #

min :: TopLevelModuleName -> TopLevelModuleName -> TopLevelModuleName Source #

Show TopLevelModuleName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods showsPrec :: Int -> TopLevelModuleName -> ShowS Source # show :: TopLevelModuleName -> String Source # showList :: [TopLevelModuleName] -> ShowS Source #
Pretty TopLevelModuleName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods pretty :: TopLevelModuleName -> Doc Source # prettyPrec :: Int -> TopLevelModuleName -> Doc Source # prettyList :: [TopLevelModuleName] -> Doc Source #
Sized TopLevelModuleName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods size :: TopLevelModuleName -> Int Source #
KillRange TopLevelModuleName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods killRange :: KillRangeT TopLevelModuleName Source #
SetRange TopLevelModuleName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods setRange :: Range -> TopLevelModuleName -> TopLevelModuleName Source #
HasRange TopLevelModuleName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods getRange :: TopLevelModuleName -> Range Source #
EmbPrj TopLevelModuleName Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: TopLevelModuleName -> S Int32 Source # icod_ :: TopLevelModuleName -> S Int32 Source # value :: Int32 -> R TopLevelModuleName Source #

# Operations on `Name` and `NamePart`

nameToRawName :: Name -> RawName Source #

nameParts :: Name -> [NamePart] Source #

nameStringParts :: Name -> [RawName] Source #

stringNameParts :: String -> [NamePart] Source #

Parse a string to parts of a concrete name.

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

class NumHoles a where Source #

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

Methods

numHoles :: a -> Int Source #

Instances

NumHoles QName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods numHoles :: QName -> Int Source #
NumHoles Name Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods numHoles :: Name -> Int Source #
NumHoles AmbiguousQName Source # | 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 Source #
NumHoles QName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods numHoles :: QName -> Int Source #
NumHoles Name Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods numHoles :: Name -> Int Source #
NumHoles [NamePart] Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods numHoles :: [NamePart] -> Int Source #

isOperator :: Name -> Bool Source #

Is the name an operator?

isHole :: NamePart -> Bool Source #

isPrefix :: Name -> Bool Source #

isPostfix :: Name -> Bool Source #

isInfix :: Name -> Bool Source #

isNonfix :: Name -> Bool Source #

# Keeping track of which names are (not) in scope

data NameInScope Source #

Constructors

InScope |
NotInScope |

Instances

Eq NameInScope Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods (==) :: NameInScope -> NameInScope -> Bool Source # (/=) :: NameInScope -> NameInScope -> Bool Source #
Data NameInScope Source # |

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) -> NameInScope -> c NameInScope Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NameInScope Source #

toConstr :: NameInScope -> Constr Source #

dataTypeOf :: NameInScope -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NameInScope) Source #

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

gmapT :: (forall b. Data b => b -> b) -> NameInScope -> NameInScope Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NameInScope -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NameInScope -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> NameInScope -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> NameInScope -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> NameInScope -> m NameInScope Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NameInScope -> m NameInScope Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NameInScope -> m NameInScope Source #

Show NameInScope Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods showsPrec :: Int -> NameInScope -> ShowS Source # show :: NameInScope -> String Source # showList :: [NameInScope] -> ShowS Source #
NFData NameInScope Source # | Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete.Name Methods rnf :: NameInScope -> () Source #
LensInScope NameInScope Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods lensInScope :: Lens' NameInScope NameInScope Source # isInScope :: NameInScope -> NameInScope Source # mapInScope :: (NameInScope -> NameInScope) -> NameInScope -> NameInScope Source # setInScope :: NameInScope -> NameInScope Source # setNotInScope :: NameInScope -> NameInScope Source #
EmbPrj NameInScope Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: NameInScope -> S Int32 Source # icod_ :: NameInScope -> S Int32 Source # value :: Int32 -> R NameInScope Source #

class LensInScope a where Source #

Minimal complete definition

lensInScope

Methods

lensInScope :: Lens' NameInScope a Source #

isInScope :: a -> NameInScope Source #

mapInScope :: (NameInScope -> NameInScope) -> a -> a Source #

setInScope :: a -> a Source #

setNotInScope :: a -> a Source #

Instances

LensInScope NameInScope Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods lensInScope :: Lens' NameInScope NameInScope Source # isInScope :: NameInScope -> NameInScope Source # mapInScope :: (NameInScope -> NameInScope) -> NameInScope -> NameInScope Source # setInScope :: NameInScope -> NameInScope Source # setNotInScope :: NameInScope -> NameInScope Source #
LensInScope QName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods lensInScope :: Lens' NameInScope QName Source # isInScope :: QName -> NameInScope Source # mapInScope :: (NameInScope -> NameInScope) -> QName -> QName Source # setInScope :: QName -> QName Source # setNotInScope :: QName -> QName Source #
LensInScope Name Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods lensInScope :: Lens' NameInScope Name Source # isInScope :: Name -> NameInScope Source # mapInScope :: (NameInScope -> NameInScope) -> Name -> Name Source # setInScope :: Name -> Name Source # setNotInScope :: Name -> Name Source #
LensInScope QName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods lensInScope :: Lens' NameInScope QName Source # isInScope :: QName -> NameInScope Source # mapInScope :: (NameInScope -> NameInScope) -> QName -> QName Source # setInScope :: QName -> QName Source # setNotInScope :: QName -> QName Source #
LensInScope Name Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods lensInScope :: Lens' NameInScope Name Source # isInScope :: Name -> NameInScope Source # mapInScope :: (NameInScope -> NameInScope) -> Name -> Name Source # setInScope :: Name -> Name Source # setNotInScope :: Name -> Name Source #

# Generating fresh names

nextStr :: String -> String Source #

nextName :: Name -> Name Source #

Get the next version of the concrete name. For instance, `nextName "x" = "x₁"`. The name must not be a `NoName`.

firstNonTakenName :: (Name -> Bool) -> Name -> Name Source #

Get the first version of the concrete name that does not satisfy the given predicate.

nameRoot :: Name -> RawName Source #

Get a raw version of the name with all suffixes removed. For instance, `nameRoot "x₁₂₃" = "x"`. The name must not be a `NoName`.

sameRoot :: Name -> Name -> Bool Source #

# Operations on qualified names

qualify :: QName -> Name -> QName Source #

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

unqualify :: QName -> Name Source #

    unqualify A.B.x == x

The range is preserved.

qnameParts :: QName -> [Name] Source #

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

isQualified :: QName -> Bool Source #

Is the name qualified?

# Operations on `TopLevelModuleName`

toTopLevelModuleName :: QName -> TopLevelModuleName Source #

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

moduleNameToFileName :: TopLevelModuleName -> String -> FilePath Source #

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

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.

# No name stuff

noName_ :: Name Source #

    noName_ = noName noRange

noName :: Range -> Name Source #

class IsNoName a where Source #

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

Methods

isNoName :: a -> Bool Source #

Instances

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

# Showing names

# Printing names

# Range instances

# NFData instances