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

Safe HaskellNone
LanguageHaskell98

Agda.Syntax.Abstract.Name

Contents

Description

Abstract names carry unique identifiers and stuff.

Synopsis

Documentation

data Name Source #

A name is a unique identifier and a suggestion for a concrete name. The concrete name contains the source location (if any) of the name. The source location of the binding site is also recorded.

Instances

Eq Name Source # 

Methods

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

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

Ord Name Source # 

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 #

Only use this show function in debugging! To convert an abstract Name into a string use prettyShow.

Methods

showsPrec :: Int -> Name -> ShowS #

show :: Name -> String #

showList :: [Name] -> ShowS #

Arbitrary Name Source #

The generated names all have the same Fixity': noFixity'.

Methods

arbitrary :: Gen Name #

shrink :: Name -> [Name] #

CoArbitrary Name Source # 

Methods

coarbitrary :: Name -> Gen b -> Gen b #

NFData Name Source #

The range is not forced.

Methods

rnf :: Name -> () #

Hashable Name Source # 

Methods

hashWithSalt :: Int -> Name -> Int #

hash :: Name -> Int #

Pretty Name Source # 
KillRange Name Source # 
SetRange Name Source # 

Methods

setRange :: Range -> Name -> Name Source #

HasRange Name Source # 

Methods

getRange :: Name -> Range Source #

IsNoName Name Source #

An abstract name is empty if its concrete name is empty.

Methods

isNoName :: Name -> Bool Source #

NumHoles Name Source # 

Methods

numHoles :: Name -> Int Source #

AddContext Name Source # 

Methods

addContext :: MonadTCM tcm => Name -> tcm a -> tcm a Source #

PrettyTCM Name Source # 

Methods

prettyTCM :: Name -> TCM Doc Source #

InstantiateFull Name Source # 
Subst Term Name Source # 
ToConcrete Name Name Source # 
Reify Name Name Source # 
Suggest Name (Abs b) Source # 

Methods

suggest :: Name -> Abs b -> String Source #

ToAbstract Pattern (Names, Pattern) Source # 
AddContext (Dom (Name, Type)) Source # 

Methods

addContext :: MonadTCM tcm => Dom (Name, Type) -> tcm a -> tcm a Source #

ToAbstract (NewName Name) Name Source # 
ToAbstract (NewName BoundName) Name Source # 
ToAbstract r a => ToAbstract (Abs r) (a, Name) Source # 

Methods

toAbstract :: Abs r -> WithNames (a, Name) Source #

(Free i, Reify i a) => Reify (Abs i) (Name, a) Source # 

Methods

reify :: Abs i -> TCM (Name, a) Source #

reifyWhen :: Bool -> Abs i -> TCM (Name, a) Source #

AddContext ([WithHiding Name], Dom Type) Source # 

Methods

addContext :: MonadTCM tcm => ([WithHiding Name], Dom Type) -> tcm a -> tcm a Source #

AddContext ([Name], Dom Type) Source # 

Methods

addContext :: MonadTCM tcm => ([Name], Dom Type) -> tcm a -> tcm a Source #

AddContext (Name, Dom Type) Source # 

Methods

addContext :: MonadTCM tcm => (Name, Dom Type) -> tcm a -> tcm a Source #

ToAbstract r Expr => ToAbstract (Dom r, Name) TypedBindings Source # 

data QName Source #

Qualified names are non-empty lists of names. Equality on qualified names are just equality on the last name, i.e. the module part is just for show.

The SetRange instance for qualified names sets all individual ranges (including those of the module prefix) to the given one.

Constructors

QName 

Instances

Eq QName Source # 

Methods

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

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

Ord QName Source # 

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 #

Only use this show function in debugging! To convert an abstract QName into a string use prettyShow.

Methods

showsPrec :: Int -> QName -> ShowS #

show :: QName -> String #

showList :: [QName] -> ShowS #

Arbitrary QName Source # 

Methods

arbitrary :: Gen QName #

shrink :: QName -> [QName] #

CoArbitrary QName Source # 

Methods

coarbitrary :: QName -> Gen b -> Gen b #

NFData QName Source # 

Methods

rnf :: QName -> () #

Hashable QName Source # 

Methods

hashWithSalt :: Int -> QName -> Int #

hash :: QName -> Int #

Pretty QName Source # 
Sized QName Source # 

Methods

size :: Integral n => QName -> n Source #

KillRange QName Source # 
KillRange RewriteRuleMap Source # 
KillRange Definitions Source # 
SetRange QName Source # 

Methods

setRange :: Range -> QName -> QName Source #

HasRange QName Source # 

Methods

getRange :: QName -> Range Source #

NumHoles QName Source # 

Methods

numHoles :: QName -> Int Source #

AllNames QName Source # 
ExprLike QName Source # 

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> QName -> m QName Source #

foldExpr :: Monoid m => (Expr -> m) -> QName -> m Source #

traverseExpr :: Monad m => (Expr -> m Expr) -> QName -> m QName Source #

mapExpr :: (Expr -> Expr) -> QName -> QName Source #

TermLike QName Source # 

Methods

traverseTerm :: (Term -> Term) -> QName -> QName Source #

traverseTermM :: Monad m => (Term -> m Term) -> QName -> m QName Source #

foldTerm :: Monoid m => (Term -> m) -> QName -> m Source #

NamesIn QName Source # 

Methods

namesIn :: QName -> Set QName Source #

PrettyTCM QName Source # 

Methods

prettyTCM :: QName -> TCM Doc Source #

InstantiateFull QName Source # 
Occurs QName Source # 
FromTerm QName Source # 
ToTerm QName Source # 
PrimTerm QName Source # 

Methods

primTerm :: QName -> TCM Term Source #

Unquote QName Source # 
UniverseBi Declaration QName # 

Methods

universeBi :: Declaration -> [QName] #

ShrinkC DefName QName Source # 
ToConcrete QName QName Source # 
(Show a, ToQName a) => ToAbstract (OldName a) QName Source # 
ToConcrete (Maybe QName) (Maybe Name) Source # 

data QNamed a Source #

Something preceeded by a qualified name.

Constructors

QNamed 

Fields

Instances

Functor QNamed Source # 

Methods

fmap :: (a -> b) -> QNamed a -> QNamed b #

(<$) :: a -> QNamed b -> QNamed a #

Foldable QNamed Source # 

Methods

fold :: Monoid m => QNamed m -> m #

foldMap :: Monoid m => (a -> m) -> QNamed a -> m #

foldr :: (a -> b -> b) -> b -> QNamed a -> b #

foldr' :: (a -> b -> b) -> b -> QNamed a -> b #

foldl :: (b -> a -> b) -> b -> QNamed a -> b #

foldl' :: (b -> a -> b) -> b -> QNamed a -> b #

foldr1 :: (a -> a -> a) -> QNamed a -> a #

foldl1 :: (a -> a -> a) -> QNamed a -> a #

toList :: QNamed a -> [a] #

null :: QNamed a -> Bool #

length :: QNamed a -> Int #

elem :: Eq a => a -> QNamed a -> Bool #

maximum :: Ord a => QNamed a -> a #

minimum :: Ord a => QNamed a -> a #

sum :: Num a => QNamed a -> a #

product :: Num a => QNamed a -> a #

Traversable QNamed Source # 

Methods

traverse :: Applicative f => (a -> f b) -> QNamed a -> f (QNamed b) #

sequenceA :: Applicative f => QNamed (f a) -> f (QNamed a) #

mapM :: Monad m => (a -> m b) -> QNamed a -> m (QNamed b) #

sequence :: Monad m => QNamed (m a) -> m (QNamed a) #

PrettyTCM NamedClause Source # 
Reify NamedClause Clause Source # 
Show a => Show (QNamed a) Source # 

Methods

showsPrec :: Int -> QNamed a -> ShowS #

show :: QNamed a -> String #

showList :: [QNamed a] -> ShowS #

Pretty a => Pretty (QNamed a) Source # 

Methods

pretty :: QNamed a -> Doc Source #

prettyPrec :: Int -> QNamed a -> Doc Source #

ToAbstract (QNamed Clause) Clause Source # 
ToAbstract [QNamed Clause] [Clause] Source # 

newtype ModuleName Source #

A module name is just a qualified name.

The SetRange instance for module names sets all individual ranges to the given one.

Constructors

MName 

Fields

Instances

Eq ModuleName Source # 
Ord ModuleName Source # 
Show ModuleName Source #

Only use this show function in debugging! To convert an abstract ModuleName into a string use prettyShow.

NFData ModuleName Source # 

Methods

rnf :: ModuleName -> () #

Pretty ModuleName Source # 
Sized ModuleName Source # 

Methods

size :: Integral n => ModuleName -> n Source #

KillRange ModuleName Source # 
KillRange Sections Source # 
SetRange ModuleName Source # 
HasRange ModuleName Source # 
SubstExpr ModuleName Source # 
ExprLike ModuleName Source # 
PrettyTCM ModuleName Source # 
InstantiateFull ModuleName Source # 
UniverseBi Declaration ModuleName # 
ToConcrete ModuleName QName Source # 
ToAbstract OldModuleName ModuleName Source # 
ToAbstract NewModuleQName ModuleName Source # 
ToAbstract NewModuleName ModuleName Source # 
ToAbstract ModuleAssignment (ModuleName, [LetBinding]) Source # 

newtype AmbiguousQName Source #

Ambiguous qualified names. Used for overloaded constructors.

Invariant: All the names in the list must have the same concrete, unqualified name. (This implies that they all have the same Range).

Constructors

AmbQ 

Fields

isAnonymousModuleName :: ModuleName -> Bool Source #

A module is anonymous if the qualification path ends in an underscore.

withRangesOf :: ModuleName -> [Name] -> ModuleName Source #

Sets the ranges of the individual names in the module name to match those of the corresponding concrete names. If the concrete names are fewer than the number of module name name parts, then the initial name parts get the range noRange.

C.D.E `withRangesOf` [A, B] returns C.D.E but with ranges set as follows:

  • C: noRange.
  • D: the range of A.
  • E: the range of B.

Precondition: The number of module name name parts has to be at least as large as the length of the list.

withRangesOfQ :: ModuleName -> QName -> ModuleName Source #

Like withRangesOf, but uses the name parts (qualifier + name) of the qualified name as the list of concrete names.

class MkName a where Source #

Make a Name from some kind of string.

Minimal complete definition

mkName

Methods

mkName :: Range -> NameId -> a -> Name Source #

The Range sets the definition site of the name, not the use site.

mkName_ :: NameId -> a -> Name Source #

qnameToConcrete :: QName -> QName Source #

Turn a qualified name into a concrete name. This should only be used as a fallback when looking up the right concrete name in the scope fails.

toTopLevelModuleName :: ModuleName -> TopLevelModuleName Source #

Computes the TopLevelModuleName corresponding to the given module name, which is assumed to represent a top-level module name.

Precondition: The module name must be well-formed.

qualify_ :: Name -> QName Source #

Convert a Name to a QName (add no module name).

isOperator :: QName -> Bool Source #

Is the name an operator?

nextName :: Name -> Name Source #

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

Important instances: Eq, Ord, Hashable

IsNoName instances (checking for "_")

Show instances

Pretty instances

Range instances

HasRange

SetRange

KillRange

Sized instances

Arbitrary instances

NFData instances

class IsNoName a where Source #

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

Minimal complete definition

isNoName

Methods

isNoName :: a -> Bool Source #

Instances

IsNoName String Source # 

Methods

isNoName :: String -> Bool Source #

IsNoName ByteString Source # 
IsNoName QName Source # 

Methods

isNoName :: QName -> Bool Source #

IsNoName Name Source # 

Methods

isNoName :: Name -> Bool Source #

IsNoName Name Source #

An abstract name is empty if its concrete name is empty.

Methods

isNoName :: Name -> Bool Source #