This reference manual is organized as follows. Section 2 overviews the general features of Prop. Section 3 describes the lexer and parser specification formalisms. Section 4 describes the algebraic datatypes and pattern matching features. Section 6 describes the tree rewriting mechanism. Finally, section 9 describes the process of running the Prop translator.
We'll use the following extended BNF notation to specify the syntax
of the language. Terminals are typeset in typewriter font,
while non-terminals are typeset in itallics font.
Given a syntactic class S, we use S, 
, S to denote one
or more occurrences of S separated by commas. Similarly,
S; ; S denotes one or more occurrences of S separated by
semi-colons. Slanted brackets are used to denote an optional occurrence
of a syntactic class. We'll combined the two forms when we
want to denote zero or more occurrences of some term.
For example, [ S, , S ] denotes
zero or more occurrences of S.