Go to the first, previous, next, last section, table of contents.


2 Lexical Conventions

Lexical analysis of Twelf has purposely been kept simple, with few reserved characters and identifiers. As a result one may need to use more whitespace to separate identifiers than in other languages. For example, `A->B' or `A+B' are single identifiers, while `A -> B' and `A + B' both consist of 3 identifiers.

During parsing, identifiers are resolved as reserved identifiers, constants, bound variables, or free variables, following the usual rules of static scoping in lambda-calculi.

2.1 Reserved Characters

The following table lists the reserved characters in Twelf.

`:'
colon, constant declaration or ascription
`.'
period, terminates declarations
`(' `)'
parentheses, for grouping terms
`[' `]'
brackets, for lambda abstraction
`{' `}'
braces, for quantification (dependent function types)
whitespace
separates identifiers; one of space, newline, tab, carriage return, vertical tab or formfeed
`%'
introduces comments or special keyword declarations
`%whitespace' `%%'
comment terminated by the end of the line, may contain any characters
`%{' `}%'
delimited comment, nested `%{' and `}%' must match
`%keyword'
various declarations
`%.'
end of input stream
`"'
doublequote, disallowed
other printing characters
identifier constituents

2.2 Identifiers

All printing characters that are not reserved can be included in identifiers, which are separated by whitespace or reserved characters. In particular, A->B is an identifier, whereas A -> B stands for the type of functions from A to B.

An uppercase identifier is one which begins with an underscore `_' or a letter in the range `A' through `Z'. A lowercase identifier begins with any other character except a reserved one. Numbers also count as lowercase identifiers and are not interpreted specially. Free variables in a declaration must be uppercase, bound variables and constants may be either uppercase or lowercase identifiers.

There are also four reserved identifiers with a predefined meaning which cannot be changed. Keep in mind that these can be constituents of other identifers which are not interpreted specially.

`->'
function type
`<-'
reverse function type
`_'
hole, to be filled by term reconstruction
`='
definition
`type'
the kind type

Constants have static scope, which means that they can be shadowed by subsequent declarations. A shadowed identifier (which can no longer be referred to in input) is printed as %id%. The printer for terms renames bound variables so they do not shadow constants.

Free uppercase identifiers in declarations represent schematic variables. In order to distinguish them from other kinds of variables and constants they are printed as `'id' (backquote, followed by the identifer name) in error messages.


Go to the first, previous, next, last section, table of contents.