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

Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Abstract.Name

Contents

Description

Abstract names carry unique identifiers and stuff.

Synopsis

Documentation

data Name #

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 # 

Methods

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

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

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

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 #

NFData Name #

The range is not forced.

Methods

rnf :: Name -> () #

Hashable Name # 

Methods

hashWithSalt :: Int -> Name -> Int

hash :: Name -> Int

Pretty Name # 

Methods

pretty :: Name -> Doc #

prettyPrec :: Int -> Name -> Doc #

KillRange Name # 
SetRange Name # 

Methods

setRange :: Range -> Name -> Name #

HasRange Name # 

Methods

getRange :: Name -> Range #

IsNoName Name #

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

Methods

isNoName :: Name -> Bool #

NumHoles Name # 

Methods

numHoles :: Name -> Int #

AddContext Name # 

Methods

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

contextSize :: Name -> Nat #

PrettyTCM Name # 

Methods

prettyTCM :: Name -> TCM Doc #

InstantiateFull Name # 
ToConcrete Name Name # 
Reify Name Name # 

Methods

reify :: Name -> TCM Name #

reifyWhen :: Bool -> Name -> TCM Name #

Suggest Name (Abs b) # 

Methods

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

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

Methods

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

contextSize :: Dom (Name, Type) -> Nat #

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

Methods

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

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

Methods

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

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

AddContext ([WithHiding Name], Dom Type) # 

Methods

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

contextSize :: ([WithHiding Name], Dom Type) -> Nat #

AddContext ([Name], Dom Type) # 

Methods

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

contextSize :: ([Name], Dom Type) -> Nat #

AddContext (Name, Dom Type) # 

Methods

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

contextSize :: (Name, Dom Type) -> Nat #

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

data QName #

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 # 

Methods

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

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

Ord QName # 

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 #

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 #

NFData QName # 

Methods

rnf :: QName -> () #

Hashable QName # 

Methods

hashWithSalt :: Int -> QName -> Int

hash :: QName -> Int

Pretty QName # 

Methods

pretty :: QName -> Doc #

prettyPrec :: Int -> QName -> Doc #

Sized QName # 

Methods

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

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

Methods

setRange :: Range -> QName -> QName #

HasRange QName # 

Methods

getRange :: QName -> Range #

NumHoles QName # 

Methods

numHoles :: QName -> Int #

AllNames QName # 

Methods

allNames :: QName -> Seq QName #

ExprLike QName # 

Methods

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

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

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

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

TermLike QName # 

Methods

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

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

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

NamesIn QName # 

Methods

namesIn :: QName -> Set QName #

PrettyTCM QName # 

Methods

prettyTCM :: QName -> TCM Doc #

InstantiateFull QName # 
Occurs QName # 
FromTerm QName # 
ToTerm QName # 

Methods

toTerm :: TCM (QName -> Term) #

toTermR :: TCM (QName -> ReduceM Term) #

PrimTerm QName # 

Methods

primTerm :: QName -> TCM Term #

Unquote QName # 

Methods

unquote :: Term -> UnquoteM QName #

UniverseBi Declaration QName # 

Methods

universeBi :: Declaration -> [QName] #

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

data QNamed a #

Something preceeded by a qualified name.

Constructors

QNamed 

Fields

Instances

Functor QNamed # 

Methods

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

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

Foldable QNamed # 

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 # 

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

Show a => Show (QNamed a) # 

Methods

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

show :: QNamed a -> String #

showList :: [QNamed a] -> ShowS #

Pretty a => Pretty (QNamed a) # 

Methods

pretty :: QNamed a -> Doc #

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

PrettyTCM (QNamed Clause) # 
ToAbstract (QNamed Clause) Clause # 
Reify (QNamed Clause) Clause # 
ToAbstract [QNamed Clause] [Clause] # 

newtype ModuleName #

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 # 
Ord ModuleName # 
Show ModuleName #

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

NFData ModuleName # 

Methods

rnf :: ModuleName -> () #

Pretty ModuleName # 
Sized ModuleName # 

Methods

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

KillRange ModuleName # 
KillRange Sections # 
SetRange ModuleName # 
HasRange ModuleName # 

Methods

getRange :: ModuleName -> Range #

SubstExpr ModuleName # 

Methods

substExpr :: [(Name, Expr)] -> ModuleName -> ModuleName #

ExprLike ModuleName # 

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> ModuleName -> m ModuleName #

foldExpr :: Monoid m => (Expr -> m) -> ModuleName -> m #

traverseExpr :: Monad m => (Expr -> m Expr) -> ModuleName -> m ModuleName #

mapExpr :: (Expr -> Expr) -> ModuleName -> ModuleName #

PrettyTCM ModuleName # 
InstantiateFull ModuleName # 
UniverseBi Declaration ModuleName # 
ToConcrete ModuleName QName # 
ToAbstract OldModuleName ModuleName # 
ToAbstract NewModuleQName ModuleName # 
ToAbstract NewModuleName ModuleName # 
ToAbstract ModuleAssignment (ModuleName, [LetBinding]) # 

newtype AmbiguousQName #

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

class IsProjP a where #

Check whether we are a projection pattern.

Minimal complete definition

isProjP

isAnonymousModuleName :: ModuleName -> Bool #

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

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

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 #

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

class MkName a where #

Make a Name from some kind of string.

Minimal complete definition

mkName

Methods

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

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

mkName_ :: NameId -> a -> Name #

Instances

qnameToConcrete :: QName -> QName #

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 #

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 #

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

isOperator :: QName -> Bool #

Is the name an operator?

nextName :: Name -> Name #

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

NFData instances

class IsNoName a where #

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

Minimal complete definition

isNoName

Methods

isNoName :: a -> Bool #

Instances

IsNoName String # 

Methods

isNoName :: String -> Bool #

IsNoName ByteString # 

Methods

isNoName :: ByteString -> Bool #

IsNoName QName # 

Methods

isNoName :: QName -> Bool #

IsNoName Name # 

Methods

isNoName :: Name -> Bool #

IsNoName Name #

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

Methods

isNoName :: Name -> Bool #