This directory contains the original files by Goerigk, and the modified files I created from them. The file "demo-output" has the raw output. Run "demo" to do the demo, which in turn runs demo-shell.cl. Requires the "clisp" implementation of Common Lisp. ================= Files downloaded from From: http://www.cs.utexas.edu/users/moore/acl2/v3-1/distrib/acl2-sources/books/workshops/1999/compiler/ They were downloaded via the web, and then had their dates reset to those posted on the web: Index of /users/moore/acl2/v3-1/distrib/acl2-sources/books/workshops/1999/compiler Icon Name Last modified Size Description[DIR] Parent Directory - [ ] Makefile 20-Sep-2004 20:24 587 [ ] compiler.lisp 16-Apr-2000 11:04 60K [ ] evaluator.lisp 19-Jan-2004 16:28 22K [ ] exercises.lisp 16-Apr-2000 08:50 14K [ ] machine.lisp 15-Sep-2003 11:46 18K [ ] proof.lisp 15-Sep-2003 11:48 41K [ ] proof1.lisp 10-Apr-2001 22:34 16K "compiler.lisp" and "machine.lisp" converted from ACL2 to straight Common Lisp, so that any Common Lisp implementation can handle it directly (no need to depend on ACL2). This just required: * removing the "defthm" (define theorem) statements, * removing the mutual-recursion declarations (ACL2 requires that mutually-recursive functions be declared as such, something not required by Common Lisp). * Renaming "execute" to "execute-am" (CLISP has "execute" predefined). * Defined a few functions in ACL2, but not in CL. clisp -v -on-error debug demo-shell.cl (type ":bt" for backtrace)