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

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

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 # 

Methods

showsPrec :: Int -> Name -> ShowS #

show :: Name -> String #

showList :: [Name] -> ShowS #

NFData Name Source #

Ranges are not forced.

Methods

rnf :: Name -> () #

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

Methods

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

HasRange Name Source # 

Methods

getRange :: Name -> Range Source #

Underscore Name Source # 
IsNoName Name Source # 

Methods

isNoName :: Name -> Bool Source #

NumHoles Name Source # 

Methods

numHoles :: Name -> Int Source #

ExprLike Name Source # 

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 # 

Methods

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

PrettyTCM Name Source # 

Methods

prettyTCM :: Name -> TCM Doc Source #

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

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.

data QName Source #

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.

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 # 

Methods

showsPrec :: Int -> QName -> ShowS #

show :: QName -> String #

showList :: [QName] -> ShowS #

NFData QName Source # 

Methods

rnf :: QName -> () #

Pretty QName Source # 
KillRange QName Source # 
SetRange QName Source # 

Methods

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

HasRange QName Source # 

Methods

getRange :: QName -> Range Source #

Underscore QName Source # 
IsNoName QName Source # 

Methods

isNoName :: QName -> Bool Source #

NumHoles QName Source # 

Methods

numHoles :: QName -> Int Source #

ExprLike QName Source # 

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 #

PrettyTCM QName Source # 

Methods

prettyTCM :: QName -> TCM Doc Source #

ToConcrete ModuleName QName Source # 
ToConcrete QName QName Source # 

Operations on Name and NamePart

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

Minimal complete definition

numHoles

Methods

numHoles :: a -> Int Source #

Instances

NumHoles QName Source # 

Methods

numHoles :: QName -> Int Source #

NumHoles Name Source # 

Methods

numHoles :: Name -> Int Source #

NumHoles AmbiguousQName Source #

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

NumHoles QName Source # 

Methods

numHoles :: QName -> Int Source #

NumHoles Name Source # 

Methods

numHoles :: Name -> Int Source #

NumHoles [NamePart] Source # 

Methods

numHoles :: [NamePart] -> Int Source #

isOperator :: Name -> Bool Source #

Is the name an operator?

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]

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.

fromTopLevelModuleName :: TopLevelModuleName -> QName Source #

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

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 "_".

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 #

Showing names

Printing names

Range instances

NFData instances