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 and separates parts of qualified names

`(' `)'

parentheses, for grouping terms

`[' `]'

brackets, for lambda abstraction

`{' `}'

braces, for quantification (dependent function types), and as begin/end delimiters in module system expressions

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 a small number of 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

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

Qualified names of the form s.c refer to the constant c of the structure s. Qualified names of the form S..c refer to the constant c of the included signature S. Qualifed names referring to blocks or structures are formed accordingly.

This document was generated by Florian Rabe on April, 3 2009 using texi2html 1.76.