Event files for the scanner and parser proofs

This is the init.lsp file I use (giving the load order). You will want to adjust the path.

The event files are given here in alphabetical order.

• actions.events is a set of definitions for parsing actions and the action and goto tables. Part of all.events.
• all.events is the collection of all files in load order needed to obtain the scanner proofs and the parsing invariants. It uses four axioms for theorems from the naturals library delivered with NQTHM-1992.
• all-with-library.events is the collection of all files in load order using the naturals library from NQTHM-1992. Three functions from the library must be disabled to avoid an infinite rewrite chain. The proof is much slower with the library, as it has to consider many more rules at each step.
• boot is just an event to bootstrap NQTHM into its ground-zero state. It is used in making the all.events file
• configuration.events is part of all.events.
• derivation.events is part of all.events.
• epsilon.events is the NFSA=DFSA proof including epsilon-closure. It uses three axioms. It is a stand-alone script as it begins with a boot-strap form.
• fsa.events is the NFSA=DFSA proof without epsilon transitions. It is a stand-alone script as it begins with a boot-strap form.
• grammar.events is part of all.events.
• lists.events is part of all.events.
• make-all is a shell script to construct all.events.
• make-all-with-library is a shell script to construct all-with-library.events.
• parser.events is part of all.events and is the parsing function. Two lines have been commented out of function accepts-is that are not commented out in the dissertation appendix. This is not critical, as the invariants are concerned with a parsing step and not with acceptance.
• parsing-inv.events is part of all.events and contains the invariants. The proof goes through until the event (high-tide) is reached. After that there are a number of lemmata that have been formulated but not proven.
• pl0r.events is a "how-to" guide for using these events to construct a scanner and a parser.
• scanning.events is part of all.events and consists of the scanning functions.
• sets.events is part of all.events.
• stack.events is part of all.events.
• table-generator.events is used to create parsing tables. In order to run this script, one must first bootstrap NQTHM, then load the set, list and grammar scripts, then load this script. Note that this is not a proper NQTHM script, as LISP functions are also introduced for doing some calculations.
• tiny.pl0r is a silly little program in PL0R and the bytecode representation of it. A large PL0R program is available, but not scannable in reasonable time.
• token.events is part of all.events.
• toktrans-1.events is part of all.events.
• toktrans-2.events is part of all.events.
• toktrans-3.events is part of all.events.
• toktrans-4.events is part of all.events.
• toktrans-5.events is part of all.events.
• toktrans-6.events is part of all.events.
• toktrans-7.events is part of all.events and contains the de-indentation functions
• tree.events is part of all.events.

1. Obtain the prover.
2. Make sure that pc-nqthm-1992 and nqthm-1992 are installed on your machine and is running. pc-nqthm-1992 is necessary as some proofs were only conductable using the INSTRUCTIONS mechanism found there. Make sure that the nqthm-1992/examples/numbers/naturals.events files has been successfully processed.
3. Obtain the all.events or all-with-naturals.events file. If you are using all-with-naturals.events, edit the note-lib line so that the directory points to the examples directory of nqthm-1992.
4. Start pc-nqthm-1992 and load the all.events file (or the all-with-naturals.events file):

   weberwu@dip6027: > pc-nqthm-1992
   GCL (GNU Common Lisp)  Version(2.1) Mon Jun  5 09:34:54 MET DST 1995
   Licensed under GNU Public Library License
   Contains Enhancements by W. Schelter
   
   Pc-Nqthm-1992.
   Initialized with (BOOT-STRAP NQTHM) on June 16, 1995  14:12:23.
   
   >(load "all.events")
   
   

A tarred and compressed file containing all of the above files can be found here (events.tar.Z)