1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
\contentsline {chapter}{\numberline {1}The parser Library}{1}
\contentsline {section}{\numberline {1.1}Introduction}{1}
\contentsline {section}{\numberline {1.2}Syntax}{1}
\contentsline {section}{\numberline {1.3}Generating Parsers}{2}
\contentsline {subsection}{\numberline {1.3.1}Auxiliary Files}{3}
\contentsline {subsection}{\numberline {1.3.2}Running the Generated Parser}{5}
\contentsline {section}{\numberline {1.4}Error Messages}{6}
\contentsline {section}{\numberline {1.5}Internals}{6}
\contentsline {section}{\numberline {1.6}Reserved Words}{7}
\contentsline {section}{\numberline {1.7}Action Symbols}{9}
\contentsline {section}{\numberline {1.8}Examples}{10}
\contentsline {subsection}{\numberline {1.8.1}Terminal Input and Errors}{10}
\contentsline {subsection}{\numberline {1.8.2}HOL Types}{11}
\contentsline {subsubsection}{\numberline {1.8.2.1}The Grammar}{11}
\contentsline {subsubsection}{\numberline {1.8.2.2}Running the Generator}{12}
\contentsline {subsubsection}{\numberline {1.8.2.3}Auxiliary Files}{12}
\contentsline {subsubsection}{\numberline {1.8.2.4}Running the Generated Parser}{14}
\contentsline {subsection}{\numberline {1.8.3}Blocks}{15}
\contentsline {subsubsection}{\numberline {1.8.3.1}The Grammar}{16}
\contentsline {subsubsection}{\numberline {1.8.3.2}Running the Generated Parser}{16}
\contentsline {subsection}{\numberline {1.8.4}Other Examples}{16}
\contentsline {section}{\numberline {1.9}The Parser-Generating Language}{18}
\contentsline {chapter}{\numberline {2}ML Functions in the parser Library}{19}
\contentsline {chapter}{\numberline {3}Pre-proved Theorems}{21}
\contentsline {chapter}{References}{23}
\contentsline {chapter}{Index}{24}
|
