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

Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Concrete.Name

Contents

Description

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

Synopsis

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

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 # 

Methods

showsPrec :: Int -> Name -> ShowS #

show :: Name -> String #

showList :: [Name] -> ShowS #

NFData Name #

Ranges are not forced.

Methods

rnf :: Name -> () #

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 #

Underscore Name # 
IsNoName Name # 

Methods

isNoName :: Name -> Bool #

NumHoles Name # 

Methods

numHoles :: Name -> Int #

ExprLike Name # 

Methods

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

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

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

SubstExpr Name # 

Methods

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

PrettyTCM Name # 

Methods

prettyTCM :: Name -> TCM Doc #

ToConcrete Name Name # 
ToAbstract (NewName Name) Name # 
ToConcrete (Maybe QName) (Maybe Name) # 

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 # 
Ord NamePart # 
Show NamePart # 
Generic NamePart # 

Associated Types

type Rep NamePart :: * -> * #

Methods

from :: NamePart -> Rep NamePart x #

to :: Rep NamePart x -> NamePart #

NFData NamePart # 

Methods

rnf :: NamePart -> () #

Pretty NamePart # 

Methods

pretty :: NamePart -> Doc #

prettyPrec :: Int -> NamePart -> Doc #

NumHoles [NamePart] # 

Methods

numHoles :: [NamePart] -> Int #

type Rep NamePart # 
type Rep NamePart = D1 (MetaData "NamePart" "Agda.Syntax.Concrete.Name" "Agda-2.5.2-75ei4uCcbjhBaJJCNAC8Q3" False) ((:+:) (C1 (MetaCons "Hole" PrefixI False) U1) (C1 (MetaCons "Id" PrefixI False) (S1 (MetaSel (Nothing 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.

Operations on Name and NamePart

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 # 

Methods

numHoles :: QName -> Int #

NumHoles Name # 

Methods

numHoles :: Name -> Int #

NumHoles AmbiguousQName #

We can have an instance for ambiguous names as all share a common concrete name.

NumHoles QName # 

Methods

numHoles :: QName -> Int #

NumHoles Name # 

Methods

numHoles :: Name -> Int #

NumHoles [NamePart] # 

Methods

numHoles :: [NamePart] -> Int #

isOperator :: Name -> Bool #

Is the name an operator?

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]

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.

fromTopLevelModuleName :: TopLevelModuleName -> QName #

Turns a top level module into a qualified name with noRange.

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

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 #

Showing names

Printing names

Range instances

NFData instances