Safe Haskell | None |
---|---|
Language | Haskell2010 |
Agda.Syntax.Concrete.Name
Contents
Description
Names in the concrete syntax are just strings (or lists of strings for qualified names).
Synopsis
- data Name
- isOpenMixfix :: Name -> Bool
- data NamePart
- data QName
- 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
- 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
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
| |
NoName |
|
Instances
Eq Name Source # | Define equality on 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 |
Data Name Source # | |
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 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 Source # | |
Show Name Source # | |
NFData Name Source # | |
Defined in Agda.Syntax.Concrete.Name | |
NFData AsName | Ranges are not forced. |
Defined in Agda.Syntax.Concrete | |
Pretty Name Source # | |
KillRange Name Source # | |
Defined in Agda.Syntax.Concrete.Name Methods | |
KillRange AsName Source # | |
Defined in Agda.Syntax.Concrete Methods | |
SetRange Name Source # | |
HasRange Name Source # | |
HasRange AsName Source # | |
Underscore Name Source # | |
Defined in Agda.Syntax.Concrete.Name | |
IsNoName Name Source # | |
Defined in Agda.Syntax.Concrete.Name | |
LensInScope Name Source # | |
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 # | |
Defined in Agda.Syntax.Concrete.Name | |
ExprLike Name Source # | |
SubstExpr Name Source # | |
EmbPrj Name Source # | |
PrettyTCM Name Source # | |
ToConcrete Name Name Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete | |
Pretty (ThingWithFixity Name) Source # | |
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 # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract | |
ToConcrete (Maybe QName) (Maybe Name) Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete |
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
Mixfix identifiers are composed of words and holes,
e.g. _+_
or if_then_else_
or [_/_]
.
Instances
Eq NamePart Source # | |
Data NamePart Source # | |
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 Source # | |
Defined in Agda.Syntax.Concrete.Name | |
Show NamePart Source # | |
Generic NamePart Source # | |
NFData NamePart Source # | |
Defined in Agda.Syntax.Concrete.Name | |
Pretty NamePart Source # | |
EmbPrj NamePart Source # | |
NumHoles [NamePart] Source # | |
Defined in Agda.Syntax.Concrete.Name | |
type Rep NamePart Source # | |
Defined in Agda.Syntax.Concrete.Name type Rep NamePart = D1 (MetaData "NamePart" "Agda.Syntax.Concrete.Name" "Agda-2.6.0.1-B0t7sLPZhcP4jvj0wGvNPO" False) (C1 (MetaCons "Hole" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Id" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 RawName))) |
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).
Instances
data TopLevelModuleName Source #
Top-level module names. Used in connection with the file system.
Invariant: The list must not be empty.
Constructors
TopLevelModuleName | |
Fields
|
Instances
Operations on Name
and NamePart
nameToRawName :: Name -> RawName 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).
Instances
NumHoles QName Source # | |
Defined in Agda.Syntax.Concrete.Name | |
NumHoles Name Source # | |
Defined in Agda.Syntax.Concrete.Name | |
NumHoles AmbiguousQName Source # | We can have an instance for ambiguous names as all share a common concrete name. |
Defined in Agda.Syntax.Abstract.Name Methods numHoles :: AmbiguousQName -> Int Source # | |
NumHoles QName Source # | |
Defined in Agda.Syntax.Abstract.Name | |
NumHoles Name Source # | |
Defined in Agda.Syntax.Abstract.Name | |
NumHoles [NamePart] Source # | |
Defined in Agda.Syntax.Concrete.Name |
isOperator :: Name -> Bool Source #
Is the name an operator?
Keeping track of which names are (not) in scope
data NameInScope Source #
Constructors
InScope | |
NotInScope |
Instances
Eq NameInScope Source # | |
Defined in Agda.Syntax.Concrete.Name | |
Data NameInScope Source # | |
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 gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NameInScope toConstr :: NameInScope -> Constr dataTypeOf :: NameInScope -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NameInScope) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NameInScope) gmapT :: (forall b. Data b => b -> b) -> NameInScope -> NameInScope gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NameInScope -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NameInScope -> r gmapQ :: (forall d. Data d => d -> u) -> NameInScope -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> NameInScope -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> NameInScope -> m NameInScope gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NameInScope -> m NameInScope gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NameInScope -> m NameInScope | |
Show NameInScope Source # | |
Defined in Agda.Syntax.Concrete.Name Methods showsPrec :: Int -> NameInScope -> ShowS show :: NameInScope -> String showList :: [NameInScope] -> ShowS | |
NFData NameInScope Source # | Ranges are not forced. |
Defined in Agda.Syntax.Concrete.Name Methods rnf :: NameInScope -> () | |
LensInScope NameInScope Source # | |
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 # | |
EmbPrj NameInScope Source # | |
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
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
Generating fresh names
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
.
Operations on qualified names
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
class IsNoName a where Source #
Check whether a name is the empty name "_".
Instances
IsNoName String Source # | |
Defined in Agda.Syntax.Concrete.Name | |
IsNoName ByteString Source # | |
Defined in Agda.Syntax.Concrete.Name | |
IsNoName QName Source # | |
Defined in Agda.Syntax.Concrete.Name | |
IsNoName Name Source # | |
Defined in Agda.Syntax.Concrete.Name | |
IsNoName Name Source # | An abstract name is empty if its concrete name is empty. |
Defined in Agda.Syntax.Abstract.Name |