diff options
Diffstat (limited to 'books/workshops/2000/moore-manolios/partial-functions')
12 files changed, 2824 insertions, 0 deletions
diff --git a/books/workshops/2000/moore-manolios/partial-functions/LICENSE b/books/workshops/2000/moore-manolios/partial-functions/LICENSE new file mode 100644 index 0000000..3558a4e --- /dev/null +++ b/books/workshops/2000/moore-manolios/partial-functions/LICENSE @@ -0,0 +1,282 @@ + GNU GENERAL PUBLIC LICENSE + Version 2, June 1991 + + Copyright (C) 1989, 1991 Free Software Foundation, Inc. + 675 Mass Ave, Cambridge, MA 02139, USA + Everyone is permitted to copy and distribute verbatim copies + of this license document, but changing it is not allowed. + + Preamble + + The licenses for most software are designed to take away your +freedom to share and change it. By contrast, the GNU General Public +License is intended to guarantee your freedom to share and change free +software--to make sure the software is free for all its users. This +General Public License applies to most of the Free Software +Foundation's software and to any other program whose authors commit to +using it. (Some other Free Software Foundation software is covered by +the GNU Library General Public License instead.) You can apply it to +your programs, too. + + When we speak of free software, we are referring to freedom, not +price. Our General Public Licenses are designed to make sure that you +have the freedom to distribute copies of free software (and charge for +this service if you wish), that you receive source code or can get it +if you want it, that you can change the software or use pieces of it +in new free programs; and that you know you can do these things. + + To protect your rights, we need to make restrictions that forbid +anyone to deny you these rights or to ask you to surrender the rights. +These restrictions translate to certain responsibilities for you if you +distribute copies of the software, or if you modify it. + + For example, if you distribute copies of such a program, whether +gratis or for a fee, you must give the recipients all the rights that +you have. You must make sure that they, too, receive or can get the +source code. And you must show them these terms so they know their +rights. + + We protect your rights with two steps: (1) copyright the software, and +(2) offer you this license which gives you legal permission to copy, +distribute and/or modify the software. + + Also, for each author's protection and ours, we want to make certain +that everyone understands that there is no warranty for this free +software. If the software is modified by someone else and passed on, we +want its recipients to know that what they have is not the original, so +that any problems introduced by others will not reflect on the original +authors' reputations. + + Finally, any free program is threatened constantly by software +patents. We wish to avoid the danger that redistributors of a free +program will individually obtain patent licenses, in effect making the +program proprietary. To prevent this, we have made it clear that any +patent must be licensed for everyone's free use or not licensed at all. + + The precise terms and conditions for copying, distribution and +modification follow. + + GNU GENERAL PUBLIC LICENSE + TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION + + 0. This License applies to any program or other work which contains +a notice placed by the copyright holder saying it may be distributed +under the terms of this General Public License. The "Program", below, +refers to any such program or work, and a "work based on the Program" +means either the Program or any derivative work under copyright law: +that is to say, a work containing the Program or a portion of it, +either verbatim or with modifications and/or translated into another +language. (Hereinafter, translation is included without limitation in +the term "modification".) Each licensee is addressed as "you". + +Activities other than copying, distribution and modification are not +covered by this License; they are outside its scope. The act of +running the Program is not restricted, and the output from the Program +is covered only if its contents constitute a work based on the +Program (independent of having been made by running the Program). +Whether that is true depends on what the Program does. + + 1. You may copy and distribute verbatim copies of the Program's +source code as you receive it, in any medium, provided that you +conspicuously and appropriately publish on each copy an appropriate +copyright notice and disclaimer of warranty; keep intact all the +notices that refer to this License and to the absence of any warranty; +and give any other recipients of the Program a copy of this License +along with the Program. + +You may charge a fee for the physical act of transferring a copy, and +you may at your option offer warranty protection in exchange for a fee. + + 2. You may modify your copy or copies of the Program or any portion +of it, thus forming a work based on the Program, and copy and +distribute such modifications or work under the terms of Section 1 +above, provided that you also meet all of these conditions: + + a) You must cause the modified files to carry prominent notices + stating that you changed the files and the date of any change. + + b) You must cause any work that you distribute or publish, that in + whole or in part contains or is derived from the Program or any + part thereof, to be licensed as a whole at no charge to all third + parties under the terms of this License. + + c) If the modified program normally reads commands interactively + when run, you must cause it, when started running for such + interactive use in the most ordinary way, to print or display an + announcement including an appropriate copyright notice and a + notice that there is no warranty (or else, saying that you provide + a warranty) and that users may redistribute the program under + these conditions, and telling the user how to view a copy of this + License. (Exception: if the Program itself is interactive but + does not normally print such an announcement, your work based on + the Program is not required to print an announcement.) + +These requirements apply to the modified work as a whole. If +identifiable sections of that work are not derived from the Program, +and can be reasonably considered independent and separate works in +themselves, then this License, and its terms, do not apply to those +sections when you distribute them as separate works. But when you +distribute the same sections as part of a whole which is a work based +on the Program, the distribution of the whole must be on the terms of +this License, whose permissions for other licensees extend to the +entire whole, and thus to each and every part regardless of who wrote it. + +Thus, it is not the intent of this section to claim rights or contest +your rights to work written entirely by you; rather, the intent is to +exercise the right to control the distribution of derivative or +collective works based on the Program. + +In addition, mere aggregation of another work not based on the Program +with the Program (or with a work based on the Program) on a volume of +a storage or distribution medium does not bring the other work under +the scope of this License. + + 3. You may copy and distribute the Program (or a work based on it, +under Section 2) in object code or executable form under the terms of +Sections 1 and 2 above provided that you also do one of the following: + + a) Accompany it with the complete corresponding machine-readable + source code, which must be distributed under the terms of Sections + 1 and 2 above on a medium customarily used for software interchange; or, + + b) Accompany it with a written offer, valid for at least three + years, to give any third party, for a charge no more than your + cost of physically performing source distribution, a complete + machine-readable copy of the corresponding source code, to be + distributed under the terms of Sections 1 and 2 above on a medium + customarily used for software interchange; or, + + c) Accompany it with the information you received as to the offer + to distribute corresponding source code. (This alternative is + allowed only for noncommercial distribution and only if you + received the program in object code or executable form with such + an offer, in accord with Subsection b above.) + +The source code for a work means the preferred form of the work for +making modifications to it. For an executable work, complete source +code means all the source code for all modules it contains, plus any +associated interface definition files, plus the scripts used to +control compilation and installation of the executable. However, as a +special exception, the source code distributed need not include +anything that is normally distributed (in either source or binary +form) with the major components (compiler, kernel, and so on) of the +operating system on which the executable runs, unless that component +itself accompanies the executable. + +If distribution of executable or object code is made by offering +access to copy from a designated place, then offering equivalent +access to copy the source code from the same place counts as +distribution of the source code, even though third parties are not +compelled to copy the source along with the object code. + + 4. You may not copy, modify, sublicense, or distribute the Program +except as expressly provided under this License. Any attempt +otherwise to copy, modify, sublicense or distribute the Program is +void, and will automatically terminate your rights under this License. +However, parties who have received copies, or rights, from you under +this License will not have their licenses terminated so long as such +parties remain in full compliance. + + 5. You are not required to accept this License, since you have not +signed it. However, nothing else grants you permission to modify or +distribute the Program or its derivative works. These actions are +prohibited by law if you do not accept this License. Therefore, by +modifying or distributing the Program (or any work based on the +Program), you indicate your acceptance of this License to do so, and +all its terms and conditions for copying, distributing or modifying +the Program or works based on it. + + 6. Each time you redistribute the Program (or any work based on the +Program), the recipient automatically receives a license from the +original licensor to copy, distribute or modify the Program subject to +these terms and conditions. You may not impose any further +restrictions on the recipients' exercise of the rights granted herein. +You are not responsible for enforcing compliance by third parties to +this License. + + 7. If, as a consequence of a court judgment or allegation of patent +infringement or for any other reason (not limited to patent issues), +conditions are imposed on you (whether by court order, agreement or +otherwise) that contradict the conditions of this License, they do not +excuse you from the conditions of this License. If you cannot +distribute so as to satisfy simultaneously your obligations under this +License and any other pertinent obligations, then as a consequence you +may not distribute the Program at all. For example, if a patent +license would not permit royalty-free redistribution of the Program by +all those who receive copies directly or indirectly through you, then +the only way you could satisfy both it and this License would be to +refrain entirely from distribution of the Program. + +If any portion of this section is held invalid or unenforceable under +any particular circumstance, the balance of the section is intended to +apply and the section as a whole is intended to apply in other +circumstances. + +It is not the purpose of this section to induce you to infringe any +patents or other property right claims or to contest validity of any +such claims; this section has the sole purpose of protecting the +integrity of the free software distribution system, which is +implemented by public license practices. Many people have made +generous contributions to the wide range of software distributed +through that system in reliance on consistent application of that +system; it is up to the author/donor to decide if he or she is willing +to distribute software through any other system and a licensee cannot +impose that choice. + +This section is intended to make thoroughly clear what is believed to +be a consequence of the rest of this License. + + 8. If the distribution and/or use of the Program is restricted in +certain countries either by patents or by copyrighted interfaces, the +original copyright holder who places the Program under this License +may add an explicit geographical distribution limitation excluding +those countries, so that distribution is permitted only in or among +countries not thus excluded. In such case, this License incorporates +the limitation as if written in the body of this License. + + 9. The Free Software Foundation may publish revised and/or new versions +of the General Public License from time to time. Such new versions will +be similar in spirit to the present version, but may differ in detail to +address new problems or concerns. + +Each version is given a distinguishing version number. If the Program +specifies a version number of this License which applies to it and "any +later version", you have the option of following the terms and conditions +either of that version or of any later version published by the Free +Software Foundation. If the Program does not specify a version number of +this License, you may choose any version ever published by the Free Software +Foundation. + + 10. If you wish to incorporate parts of the Program into other free +programs whose distribution conditions are different, write to the author +to ask for permission. For software which is copyrighted by the Free +Software Foundation, write to the Free Software Foundation; we sometimes +make exceptions for this. Our decision will be guided by the two goals +of preserving the free status of all derivatives of our free software and +of promoting the sharing and reuse of software generally. + + NO WARRANTY + + 11. BECAUSE THE PROGRAM IS LICENSED FREE OF CHARGE, THERE IS NO WARRANTY +FOR THE PROGRAM, TO THE EXTENT PERMITTED BY APPLICABLE LAW. EXCEPT WHEN +OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR OTHER PARTIES +PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED +OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF +MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE ENTIRE RISK AS +TO THE QUALITY AND PERFORMANCE OF THE PROGRAM IS WITH YOU. SHOULD THE +PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING, +REPAIR OR CORRECTION. + + 12. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING +WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY AND/OR +REDISTRIBUTE THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, +INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING +OUT OF THE USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED +TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY +YOU OR THIRD PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER +PROGRAMS), EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE +POSSIBILITY OF SUCH DAMAGES. + + END OF TERMS AND CONDITIONS + + diff --git a/books/workshops/2000/moore-manolios/partial-functions/README b/books/workshops/2000/moore-manolios/partial-functions/README new file mode 100644 index 0000000..955cf1b --- /dev/null +++ b/books/workshops/2000/moore-manolios/partial-functions/README @@ -0,0 +1,50 @@ +; To reproduce the results shown in the paper, get the following files from +; this directory +; tjvm.lisp +; examples.lisp +; tjvm-examples.lisp +; mod-1-property.lisp +; report.lisp + +; The top level results are in report.lisp. + +; The Makefile allows you to type make to certify all the books. Otherwise, +; you can follow the original instructions, included here now: + +; To recertify all these books, edit the form below, replacing the full +; path names by the full path of the directory on which you have down loaded +; these files. Then execute the expression below in an ACL2 in which the +; connected book directory is set to the full path name of that directory. + +(ld '( + (certify-book "defpun") + (ubt! 1) + + (DEFPKG "TJVM" + (set-difference-equal + (union-eq '(ASSOC-EQUAL LEN NTH ZP SYNTAXP + QUOTEP FIX NFIX E0-ORDINALP E0-ORD-<) + (union-eq *acl2-exports* + *common-lisp-symbols-from-main-lisp-package*)) + '(PC PROGRAM PUSH POP REVERSE STEP ++))) + + (certify-book "tjvm" 1) + (ubt! 1) + + (include-book "/dir/tjvm") + (certify-book "examples" 1) + (ubt! 1) + + (include-book "/dir/examples") + (certify-book "tjvm-examples" 1) + (ubt! 1) + + (certify-book "mod-1-property") + (ubt! 1) + + (certify-book "report") + (ubt! 1)) + :ld-pre-eval-print t) + + + diff --git a/books/workshops/2000/moore-manolios/partial-functions/defpun-original.lisp b/books/workshops/2000/moore-manolios/partial-functions/defpun-original.lisp new file mode 100644 index 0000000..737e912 --- /dev/null +++ b/books/workshops/2000/moore-manolios/partial-functions/defpun-original.lisp @@ -0,0 +1,500 @@ +; Copyright (C) 2000 Panagiotis Manolios and J Strother Moore + +; This program is free software; you can redistribute it and/or modify +; it under the terms of the GNU General Public License as published by +; the Free Software Foundation; either version 2 of the License, or +; (at your option) any later version. + +; This program is distributed in the hope that it will be useful, +; but WITHOUT ANY WARRANTY; without even the implied warranty of +; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +; GNU General Public License for more details. + +; You should have received a copy of the GNU General Public License +; along with this program; if not, write to the Free Software +; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. + +; Written by Panagiotis Manolios and J Strother Moore who can be +; reached as follows. + +; Email: pete@cs.utexas.edu, moore@cs.utexas.edu + +; Postal Mail: +; Department of Computer Science +; The University of Texas at Austin +; Austin, TX 78701 USA + +; To introduce an arbitrary tail-recursive function we proceed in +; three steps. First is the proof that we can admit the generic one +; argument tail recursive function. This ``generic theorem'' is +; proved once; the proof is not redone for each new function. Second, +; the generic theorem is used to introduce the arity one version of +; the desired function. Third, we prove that the arity one version is +; a witness for the desired equation. + +; Here is an example. Suppose we wish to admit the tail recursive +; factorial. + +; (defun trfact (n a) +; (if (equal n 0) +; a +; (trfact (- n 1) (* n a)))) + +; We first recognize that this is probably tail recursive (without +; checking that trfact is new, that the vars are distinct, etc. +; Successful recognition produces + +; (mv '((n (car x)) +; (a (cadr x))) +; '(equal n 0) +; 'a +; '(list (- n 1) (* n a))) + +; Using the output of this check, we introduce three defuns + +; (defun test1 (x) +; (let ((n (car x)) +; (a (cadr x))) +; (equal n 0))) + +; (defun base1 (x) +; (let ((n (car x)) +; (a (cadr x))) +; a)) + +; (defun step1 (x) +; (let ((n (car x)) +; (a (cadr x))) +; (list (- n 1) (* n a)))) + +; We then use the generic theorem to introduce + +; (defun trfact1 (x) +; (if (test1 x) +; (base1 x) +; (trfact1 (step1 x)))) + +; We then define + +; (defun trfact (n a) +; (trfact1 (list n a))) + +; and we prove that it satisfies the constraint + +; (equal (trfact n a) +; (if (equal n 0) +; a +; (trfact (- n 1) (* n a)))) + +; Now we write the code to do all this. + +; First, we prove the generic theorem. We use the proof Pete +; developed in his prototype implementation of defpartial but for the +; generic case. + +(in-package "ACL2") + +(defstub test (x) t) +(defstub base (x) t) +(defstub st (x) t) + +(defun stn (x n) + (if (zp n) x (stn (st x) (1- n)))) + +(defchoose fch (n) + (x) + (test (stn x n))) + +(defun fn (x n) + (declare (xargs :measure (nfix n))) + (if (or (zp n) (test x)) + (base x) + (fn (st x) (1- n)))) + +(defun f (x) + (if (test (stn x (fch x))) + (fn x (fch x)) + nil)) + +; The following encapsulate exports one constrained function, namely, +; f, with the constraint + +; (DEFTHM GENERIC-TAIL-RECURSIVE-F +; (EQUAL (F X) +; (IF (TEST X) (BASE X) (F (ST X)))) +; :RULE-CLASSES NIL) + +; Nothing else is exported. + +(encapsulate nil + (local (defthm test-fch + (implies (test x) + (test (stn x (fch x)))) + :hints + (("goal" :use ((:instance fch (n 0))))))) + (local (defthm test-f-def + (implies (test x) + (equal (f x) (base x))))) + (local (defthm open-stn + (implies (and (integerp n) (< 0 n)) + (equal (stn x n) (stn (st x) (1- n)))))) + + (local (defthm +1-1 (equal (+ -1 +1 x) (fix x)))) + + (local (defthm st-stn-fch + (implies (test (stn (st x) (fch (st x)))) + (test (stn x (fch x)))) + :hints + (("goal" :use + ((:instance fch (n (1+ (nfix (fch (st x)))))) + (:instance fch (n 1))))) + :rule-classes :forward-chaining)) + (local (defthm test-nil-fch + (implies (not (test x)) + (iff (test (stn (st x) (fch (st x)))) + (test (stn x (fch x))))) + :hints + (("subgoal 2" :expand (stn x (fch x)) + :use + ((:instance fch (x (st x)) + (n (+ -1 (fch x))))))))) + (local (defthm fn-st + (implies (and (test (stn x n)) (test (stn x m))) + (equal (fn x n) (fn x m))) + :rule-classes nil)) + (defthm generic-tail-recursive-f + (equal (f x) + (if (test x) (base x) (f (st x)))) + :hints + (("subgoal 1" :expand (fn x (fch x))) + ("subgoal 1.2'" :use + ((:instance fn-st (x (st x)) + (n (+ -1 (fch x))) + (m (fch (st x))))))) + :rule-classes nil)) + +(defun arity-1-tail-recursive-encap (f test base st) + +; Execution of this function produces an encapsulation that introduces +; a constrained tail recursive f with the constraint +; (equal (f x) (if (test x) (base x) (f (st x)))), +; where test, base and st are previously defined functions of arity 1. + + (declare (xargs :mode :program)) + + (let ((stn (packn-pos (list f "-stn") f)) + (fch (packn-pos (list f "-fch") f)) + (fn (packn-pos (list f "-fn") f))) + + `(encapsulate + ((,f (x) t)) + + (local (in-theory (disable ,test ,base ,st))) + + (local (defun ,stn (x n) + (if (zp n) + x + (,stn (,st x) (1- n))))) + + (local (defchoose ,fch (n) (x) + (,test (,stn x n)))) + + (local (defun ,fn (x n) + (declare (xargs :measure (nfix n))) + (if (or (zp n) + (,test x)) + (,base x) + (,fn (,st x) (1- n))))) + + (local (defun ,f (x) + (if (,test (,stn x (,fch x))) + (,fn x (,fch x)) + nil))) + + (local (in-theory '(,f ,test ,base ,st ,stn ,fn))) + (defthm ,(packn-pos (list f "-DEF") f) + (equal (,f x) + (if (,test x) + (,base x) + (,f (,st x)))) + :hints (("Goal" + :use + (:functional-instance GENERIC-TAIL-RECURSIVE-F + (f ,f) + (test ,test) + (base ,base) + (st ,st) + (stn ,stn) + (fch ,fch) + (fn ,fn) + )) + ("Subgoal 3" :use ,fch) ; added after 3.0.1 for new defchoose + ("Subgoal 2" :use ,fch)) + + :rule-classes nil) + ) + )) + +; Second, we recognize probably tail-recursive definitions and introduce +; the appropriate functions of arity 1. + +; Note that probably-tail-recursivep and destructure-tail-recursion should be +; kept in sync. + +(defun probably-tail-recursivep (f vars body) + (and (symbolp f) + (symbol-listp vars) + (true-listp body) + (eq (car body) 'IF) + (or (and (consp (caddr body)) + (eq (car (caddr body)) f)) + (and (consp (cadddr body)) + (eq (car (cadddr body)) f))))) + +(defun destructure-tail-recursion-aux (vars x) + (declare (xargs :mode :program)) + (cond ((endp vars) nil) + (t (cons (list (car vars) + (list 'car x)) + (destructure-tail-recursion-aux (cdr vars) + (list 'cdr x)))))) + +(defun destructure-tail-recursion (f vars body) + (declare (xargs :mode :program)) + (cond + ((and (consp (caddr body)) + (eq (car (caddr body)) f)) + (mv (destructure-tail-recursion-aux vars 'x) + (list 'NOT (cadr body)) + (cadddr body) + (cons 'LIST (cdr (caddr body))))) + (t + (mv (destructure-tail-recursion-aux vars 'x) + (cadr body) + (caddr body) + (cons 'LIST (cdr (cadddr body))))))) + +(defun arbitrary-tail-recursive-encap (f vars body) + (declare (xargs :mode :program)) + (mv-let + (bindings test-body base-body step-body) + (destructure-tail-recursion f vars body) + (let ((f1 (packn-pos (list f "-arity-1") f)) + (test1 (packn-pos (list f "-arity-1-test") f)) + (base1 (packn-pos (list f "-arity-1-base") f)) + (step1 (packn-pos (list f "-arity-1-step") f))) + `(encapsulate + ((,f ,vars t)) + (set-ignore-ok t) + (set-irrelevant-formals-ok t) + (local (defun ,test1 (x) (let ,bindings ,test-body))) + (local (defun ,base1 (x) (let ,bindings ,base-body))) + (local (defun ,step1 (x) (let ,bindings ,step-body))) + (local ,(arity-1-tail-recursive-encap f1 test1 base1 step1)) + (local (defun ,f ,vars (,f1 (list ,@vars)))) + (defthm ,(packn-pos (list f "-DEF") f) + (equal (,f ,@vars) ,body) + :hints (("Goal" :use (:instance ,(packn-pos (list f1 "-DEF") f) + (x (list ,@vars))))) + :rule-classes :definition))))) + +(defun remove-xargs-domain-and-measure (dcl) + (case-match dcl + (('declare ('xargs ':domain dom-expr + ':measure measure-expr + . rest)) + (mv nil dom-expr measure-expr rest)) + (('declare ('xargs ':gdomain dom-expr + ':measure measure-expr + . rest)) + (mv t dom-expr measure-expr rest)) + (& (mv nil nil 0 nil)))) + +(mutual-recursion + (defun subst-fn-into-pseudo-term (new-fn old-fn pterm) + (declare (xargs :mode :program)) + (cond + ((atom pterm) pterm) + ((eq (car pterm) 'quote) pterm) + ((or (eq (car pterm) 'let) + (eq (car pterm) 'let*)) + (list (car pterm) + (subst-fn-into-pseudo-bindings new-fn old-fn (cadr pterm)) + (subst-fn-into-pseudo-term new-fn old-fn (caddr pterm)))) + ((eq (car pterm) 'cond) + (cons 'cond + (subst-fn-into-pseudo-cond-clauses new-fn old-fn (cdr pterm)))) + (t + (cons (if (eq (car pterm) old-fn) + new-fn + (car pterm)) + (subst-fn-into-pseudo-term-list new-fn old-fn (cdr pterm)))))) + + (defun subst-fn-into-pseudo-bindings (new-fn old-fn pbindings) + (declare (xargs :mode :program)) + (cond + ((atom pbindings) pbindings) + (t (cons (list (car (car pbindings)) + (subst-fn-into-pseudo-term new-fn old-fn + (cadr (car pbindings)))) + (subst-fn-into-pseudo-bindings new-fn old-fn (cdr pbindings)))))) + + (defun subst-fn-into-pseudo-cond-clauses (new-fn old-fn pclauses) + (declare (xargs :mode :program)) + (cond + ((atom pclauses) pclauses) + (t (cons (list (subst-fn-into-pseudo-term new-fn old-fn + (car (car pclauses))) + (subst-fn-into-pseudo-term new-fn old-fn + (cadr (car pclauses)))) + (subst-fn-into-pseudo-cond-clauses new-fn old-fn + (cdr pclauses)))))) + + (defun subst-fn-into-pseudo-term-list (new-fn old-fn list) + (declare (xargs :mode :program)) + (cond + ((atom list) list) + (t (cons (subst-fn-into-pseudo-term new-fn old-fn (car list)) + (subst-fn-into-pseudo-term-list new-fn old-fn (cdr list))))))) + +(defun default-defpun-rule-classes (keyword-alist) + +; We add :rule-classes :definition to keyword-alist if :rule-classes is +; not mentioned in it. + + (cond + ((keyword-value-listp keyword-alist) + (cond ((assoc-keyword :rule-classes keyword-alist) + keyword-alist) + (t (list* :rule-classes :definition keyword-alist)))) + (t keyword-alist))) + +(defun destructure-dcl-body-keypairs (lst) + +; Lst is the tail of some defpun. It optionally contains a DECLARE +; form, a body, and some keyword binding pairs, in that order. We +; return the three components. Body must be present, and if keyword +; binding pairs are present, the length of that part of the list must +; be even. So the parity of the length of the list determines which +; optional components are present. + +; 0. illegal - never allowed to happen +; 1. body +; 2. dcl body +; 3. body :rule-classes classes +; 4. dcl body :rule-classes classes +; 5. body :rule-classes classes :hints hints +; 6. dcl body :rule-classes classes :hints hints +; etc. +; If rule-classes is unspecified it defaults to :definition. + + (cond + ((evenp (length lst)) + (mv (car lst) + (cadr lst) + (default-defpun-rule-classes (cddr lst)))) + (t (mv nil + (car lst) + (default-defpun-rule-classes (cdr lst)))))) + +(defun defpun-syntax-er nil + '(er soft 'defpun + "The proper shape of a defpun event is~%~ + (defpun g (v1 ... vn) body).~%~ + A single optional declare form may be present ~ + before the body. If present, the form must be one of three:~%~ + (DECLARE (XARGS :witness fn))~%~ + or~%~ + (DECLARE (XARGS :domain dom-expr :measure m . rest))~%~ + or~%~ + (DECLARE (XARGS :gdomain dom-expr :measure m . rest)).~%~ + An optional keyword alist may be ~ + present after the body. The declare form is used during the ~ + admission of the witness function. The keyword alist is ~ + attached to the equality axiom constraining the new function ~ + symbol. If the :rule-classes keyword is not specified by the ~ + keyword alist, :definition is used.")) + +(defmacro defpun (g vars &rest rest) + (cond + ((and (symbolp g) + (symbol-listp vars) + (not (endp rest))) + +; This form may be legal, so we will destructure it and proceed. Otherwise, +; we will cause an error. + + (mv-let + (dcl body keypairs) + (destructure-dcl-body-keypairs rest) + (cond + ((not (keyword-value-listp keypairs)) + (defpun-syntax-er)) + ((and (not dcl) + (probably-tail-recursivep g vars body)) + (arbitrary-tail-recursive-encap g vars body)) + ((and dcl + (match dcl + ('declare ('xargs ':witness &)))) + `(encapsulate + ((,g ,vars t)) + (local (defun ,g ,vars (,(caddr (cadr dcl)) + ,@vars))) + (defthm ,(packn-pos (list g "-DEF") g) + (equal (,g ,@vars) + ,body) + ,@keypairs))) + ((not (and (consp dcl) + (eq (car dcl) 'declare))) + (defpun-syntax-er)) + (t + (mv-let + (closed-domp dom-expr measure-expr rest-of-xargs) + (remove-xargs-domain-and-measure dcl) + (cond + (closed-domp + (let ((gwit (packn-pos (list "THE-" g) g))) + `(encapsulate + nil + (defun ,gwit ,vars + (declare (xargs :measure + (if ,dom-expr + ,measure-expr + 0) + :guard ,dom-expr + :verify-guards nil + ,@rest-of-xargs)) + (if ,dom-expr + ,(subst-fn-into-pseudo-term gwit g body) + 'undef)) + (encapsulate + ((,g ,vars t)) + (local (defun ,g ,vars (,gwit ,@vars))) + (defthm ,(packn-pos (list g "-DEF") g) + (implies ,dom-expr + (equal (,g ,@vars) + ,body)) + ,@keypairs)) + (defthm ,(packn-pos (list g "-IS-UNIQUE") g) + (implies ,dom-expr + (equal (,g ,@vars) + (,gwit ,@vars)))) + (in-theory (disable ,(packn-pos (list g "-IS-UNIQUE") g))) + (verify-guards ,gwit)))) + (t `(encapsulate + ((,g ,vars t)) + (local (defun ,g ,vars + (declare (xargs :measure + (if ,dom-expr + ,measure-expr + 0) + ,@rest-of-xargs)) + (if ,dom-expr + ,body + 'undef))) + (defthm ,(packn-pos (list g "-DEF") g) + (implies ,dom-expr + (equal (,g ,@vars) + ,body)) + ,@keypairs))))))))) + (t (defpun-syntax-er)))) diff --git a/books/workshops/2000/moore-manolios/partial-functions/defpun.lisp b/books/workshops/2000/moore-manolios/partial-functions/defpun.lisp new file mode 100644 index 0000000..e973659 --- /dev/null +++ b/books/workshops/2000/moore-manolios/partial-functions/defpun.lisp @@ -0,0 +1,7 @@ +(in-package "ACL2") + +; Please see defpun-original.lisp if you are working through the paper and +; wishsee the example and look at the macros exactly as they originally +; appeared. + +(include-book "misc/defpun" :dir :system) diff --git a/books/workshops/2000/moore-manolios/partial-functions/examples.acl2 b/books/workshops/2000/moore-manolios/partial-functions/examples.acl2 new file mode 100644 index 0000000..afbb5e5 --- /dev/null +++ b/books/workshops/2000/moore-manolios/partial-functions/examples.acl2 @@ -0,0 +1,4 @@ +(value :q) +(lp) +(include-book "tjvm") +(certify-book "examples" ? t) diff --git a/books/workshops/2000/moore-manolios/partial-functions/examples.lisp b/books/workshops/2000/moore-manolios/partial-functions/examples.lisp new file mode 100644 index 0000000..eb517a0 --- /dev/null +++ b/books/workshops/2000/moore-manolios/partial-functions/examples.lisp @@ -0,0 +1,662 @@ +; Copyright (C) 1999 J Strother Moore + +; This book is free software; you can redistribute it and/or modify +; it under the terms of the GNU General Public License as published by +; the Free Software Foundation; either version 2 of the License, or +; (at your option) any later version. + +; This book is distributed in the hope that it will be useful, +; but WITHOUT ANY WARRANTY; without even the implied warranty of +; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +; GNU General Public License for more details. + +; You should have received a copy of the GNU General Public License +; along with this book; if not, write to the Free Software +; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. + +; This book proves the theorems about the ``Toy Java Virtual Machine'' +; tjvm, discussed in the paper + +; Proving Theorems about Java-like Byte Code +; by J Strother Moore + + +(in-package "TJVM") + +(include-book "tjvm") + +; Here we develop the general theory for proving things about tjvm. + +; Simplest of Arithmetic + +(defthm constant-fold-+ + (implies (syntaxp (and (quotep x) (quotep y))) + (equal (+ x (+ y z)) (+ (+ x y) z)))) + +(defthm commutativity2-of-+ + (equal (+ x y z) (+ y x z)) + :hints (("Goal" :use ((:instance acl2::associativity-of-+ + (acl2::x y) + (acl2::y x) + (acl2::z z)) + (:instance acl2::associativity-of-+ + (acl2::x x) + (acl2::y y) + (acl2::z z)) + (:instance acl2::commutativity-of-+ + (acl2::x x) + (acl2::y y))) + :in-theory (disable acl2::associativity-of-+ + acl2::commutativity-of-+)))) + +(defthm commutativity2-of-* + (equal (* x y z) (* y x z)) + :hints (("Goal" :use ((:instance acl2::associativity-of-* + (acl2::x y) + (acl2::y x) + (acl2::z z)) + (:instance acl2::associativity-of-* + (acl2::x x) + (acl2::y y) + (acl2::z z)) + (:instance acl2::commutativity-of-* + (acl2::x x) + (acl2::y y))) + :in-theory (disable acl2::associativity-of-* + acl2::commutativity-of-*)))) + +(defthm plus-right-id + (equal (+ x 0) (fix x))) + +(defthm *-0 (equal (* 0 x) 0)) + +(defthm +-cancellation1 + (equal (+ i j (* -1 i) k) + (+ j k))) + +; Abstract Data Type Stuff + +(defthm stacks + (and (equal (top (push x s)) x) + (equal (pop (push x s)) s))) + +(in-theory (disable push top pop)) + +(defthm states + (and (equal (call-stack (make-state s h c)) s) + (equal (heap (make-state s h c)) h) + (equal (class-table (make-state s h c)) c))) + +(in-theory (disable make-state call-stack heap class-table)) + +(defthm frames + (and (equal (pc (make-frame pc l s prog)) pc) + (equal (locals (make-frame pc l s prog)) l) + (equal (stack (make-frame pc l s prog)) s) + (equal (program (make-frame pc l s prog)) prog))) + +(in-theory (disable make-frame pc locals stack program)) + +; Step Stuff + +(defthm step-opener + (implies (consp (next-inst s)) + (equal (step s) (do-inst (next-inst s) s)))) + +(in-theory (disable step)) + +; Clocks + +(defun c+ (i j) + (if (zp i) + (nfix j) + (+ 1 (c+ (- i 1) j)))) + +(defun c* (i j) + (if (zp i) 0 (c+ j (c* (- i 1) j)))) + +(defmacro ++ (&rest args) + (if (endp args) + 0 + (if (endp (cdr args)) + (car args) + `(c+ ,(car args) (++ ,@(cdr args)))))) + +(defthm c+-revealed + (implies (and (natp i) (natp j)) + (equal (c+ i j) (+ i j)))) + +(defthm c*-revealed + (implies (and (natp i) (natp j)) + (equal (c* i j) (* i j)))) + +(in-theory (disable c+-revealed c*-revealed)) + +(defthm tjvm-c+ + (implies (and (natp i) (natp j)) + (equal (tjvm s (c+ i j)) + (tjvm (tjvm s i) j)))) + +; Sometimes we get tjvm expressions such as (tjvm s (+ 4 (c+ ...))). The +; following lemma produces (tjvm (tjvm s 4) (c+ ...)). + +(defthm tjvm-+ + (implies (and (natp i) (natp j)) + (equal (tjvm s (+ i j)) + (tjvm (tjvm s i) j))) + :hints (("Goal" :use tjvm-c+ + :in-theory (enable c+-revealed)))) + +; Then we finally hit the (tjvm s 4) repeatedly with the following lemma to +; step s 4 times. + +(defthm tjvm-opener + (and (equal (tjvm s 0) s) + (implies (natp i) + (equal (tjvm s (+ 1 i)) + (tjvm (step s) i))))) + +(in-theory (disable tjvm)) + +; Alist Stuff + +(defthm assoc-equal-bind + (equal (assoc-equal key1 (bind key2 val alist)) + (if (equal key1 key2) + (cons key1 val) + (assoc-equal key1 alist)))) + +(defthm bind-formals-cons + (and (equal (bind-formals nil stack) nil) + (equal (bind-formals (cons var formals) stack) + (cons (cons var (top stack)) + (bind-formals formals (pop stack)))))) + +; Stack Stuff + +; We normalize all POPNs away. + +(defthm popn-opener + (and (equal (popn 0 stack) stack) + (implies (and (integerp n) + (<= 0 n)) + (equal (popn (+ 1 n) stack) + (popn n (pop stack)))))) + +; Applications + +(defun fact (n) + (if (zp n) + 1 + (* n (fact (- n 1))))) + +(defun \bf_fact () + '("fact" (n) + (load n) + (ifle 8) + (load n) + (load n) + (push 1) + (sub) + (invokestatic "Math" "fact" 1) + (mul) + (xreturn) + (push 1) + (xreturn))) + +(defun \bfMath-class () + (make-class-decl "Math" + '("Object") + nil + (list (\bf_fact)))) + +(defun fact-clock (n) + (if (zp n) + 5 + (++ 7 + (fact-clock (- n 1)) + 2))) + +(defthm example1 + (equal (top + (stack + (top-frame + (tjvm (make-state + (push (make-frame 0 + nil + nil + '((push 5) + (invokestatic "Math" "fact" 1) + (halt))) + nil) + nil + (list (\bfMath-class))) + (++ 1 (fact-clock 5) 1))))) + 120) + :rule-classes nil) + +(defthm fact-clock-revealed + (implies (natp n) (equal (fact-clock n) (+ 5 (* 9 n)))) + :hints (("Goal" :in-theory (enable c+-revealed))) + :rule-classes nil) + +(defun example2-hint (s0 n) + (if (zp n) + s0 + (example2-hint + (make-state + (push (make-frame 6 + (list (cons 'n (top (stack (top-frame s0))))) + (push (- (top (stack (top-frame s0))) 1) + (push (top (stack (top-frame s0))) + nil)) + (method-program (\bf_fact))) + (push (make-frame (+ 1 (pc (top (call-stack s0)))) + (locals (top (call-stack s0))) + (pop (stack (top (call-stack s0)))) + (program (top (call-stack s0)))) + (pop (call-stack s0)))) + (heap s0) + (class-table s0)) + (- n 1)))) + +(defthm example2 + (implies (and (equal (next-inst s0) '(invokestatic "Math" "fact" 1)) + (equal (assoc-equal "Math" (class-table s0)) + (\bfMath-class)) + (equal n (top (stack (top-frame s0)))) + (natp n)) + (equal + (tjvm s0 (fact-clock n)) + (make-state + (push (make-frame (+ 1 (pc (top-frame s0))) + (locals (top-frame s0)) + (push (fact n) + (pop (stack (top-frame s0)))) + (program (top-frame s0))) + (pop (call-stack s0))) + (heap s0) + (class-table s0)))) + :hints (("Goal" :induct (example2-hint s0 n))) + :rule-classes nil) + +(defun \bf_xIncrement () + '("xIncrement" (dx) + (load this) + (load this) + (getfield "Point" "x") + (load dx) + (add) + (putfield "Point" "x") + (return))) + +(defun xIncrement-clock () 8) + +(defun \bf_inBox () + '("inBox" (p1 p2) + (load p1) + (getfield "Point" "x") + (load this) + (getfield "Point" "x") + (sub) + (ifgt 21) + (load this) + (getfield "Point" "x") + (load p2) + (getfield "Point" "x") + (sub) + (ifgt 15) + (load p1) + (getfield "Point" "y") + (load this) + (getfield "Point" "y") + (sub) + (ifgt 9) + (load this) + (getfield "Point" "y") + (load p2) + (getfield "Point" "y") + (sub) + (ifgt 3) + (push 1) + (xreturn) + (push 0) + (xreturn))) + +(defun \bfPoint-class () + (make-class-decl "Point" + '("Object") + '("x" "y") + (list (\bf_xIncrement) + (\bf_inBox)))) + +(defun \bf_setColor () + '("setColor" (c) + (load this) + (load c) + (putfield "ColoredPoint" "color") + (return))) + +(defun setColor-clock () 5) + +(defun \bf_setColorBox () + '("setColorBox" (p1 p2 color) + (load this) + (load p1) + (load p2) + (invokevirtual "ColoredPoint" "inBox" 2) + (ifeq 4) + (load this) + (load color) + (putfield "ColoredPoint" "color") + (return))) + +(defun \bfColoredPoint-class () + (make-class-decl "ColoredPoint" + '("Point" "Object") + '("color") + (list (\bf_setColor) + (\bf_setColorBox)))) + + +(defthm example3 + (let ((s (tjvm (make-state + (push + (make-frame 0 + '((p . nil)) + nil + '((new "ColoredPoint") + (store p) + (load p) + (push -23) + (invokevirtual "ColoredPoint" "xIncrement" 1) + (load p) + (push "Green") + (invokevirtual "ColoredPoint" "setColor" 1) + (load p) + (halt))) + nil) + nil + (list (\bfPoint-class) + (\bfColoredPoint-class))) + (++ 4 + (xIncrement-clock) + 2 + (setColor-clock) + 2)))) + (equal (deref (top (stack (top-frame s))) + (heap s)) + '(("ColoredPoint" ("color" . "Green")) + ("Point" ("x" . -23) ("y" . 0)) + ("Object"))))) + +(defun instance-of (ref class-name s) + (assoc-equal class-name + (deref ref (heap s)))) + +(defun Point.x (ref s) + (field-value "Point" "x" (deref ref (heap s)))) + +(defun Point.y (ref s) + (field-value "Point" "y" (deref ref (heap s)))) + +(defun inBox-clock (this p1 p2 s) + (cond ((> (Point.x p1 s) + (Point.x this s)) + 9) + ((> (Point.x this s) + (Point.x p2 s)) + 15) + ((> (Point.y p1 s) + (Point.y this s)) + 21) + (t 27))) + +(defun inBox (this p1 p2 s) + (and (<= (Point.x p1 s) + (Point.x this s)) + (<= (Point.x this s) + (Point.x p2 s)) + (<= (Point.y p1 s) + (Point.y this s)) + (<= (Point.y this s) + (Point.y p2 s)))) + +(defun setColorBox-clock (this p1 p2 c s) + (declare (ignore c)) + (++ 4 + (inBox-clock this p1 p2 s) + (if (inBox this p1 p2 s) + 5 + 2))) + +(defun setColorBox-heap (this p1 p2 c s) + +; This function returns the new heap. + + (if (inBox this p1 p2 s) + (let ((instance (deref this (heap s))) + (address (cadr this))) + (bind + address + (set-instance-field "ColoredPoint" "color" c instance) + (heap s))) + (heap s))) + +(defthm example4 + (implies (and (consp (next-inst s0)) + (equal (car (next-inst s0)) 'invokevirtual) + (equal (caddr (next-inst s0)) "inBox") + (equal (cadddr (next-inst s0)) 2) + + (equal this (top (pop (pop (stack (top-frame s0)))))) + (equal p1 (top (pop (stack (top-frame s0))))) + (equal p2 (top (stack (top-frame s0)))) + +; This next hyp is necessary because even if I know that the THIS object +; is an instance-of class "Point" I do not know that the "inBox" method +; hasn't been overridden! + + (equal (lookup-method "inBox" + (class-name-of-ref this (heap s0)) + (class-table s0)) + (\bf_inBox))) + (equal + (tjvm s0 (inBox-clock this p1 p2 s0)) + (make-state + (push (make-frame (+ 1 (pc (top-frame s0))) + (locals (top-frame s0)) + (push (if (inBox this p1 p2 s0) 1 0) + (popn 3 (stack (top-frame s0)))) + (program (top-frame s0))) + (pop (call-stack s0))) + (heap s0) + (class-table s0)))) + + :rule-classes + ((:rewrite + :corollary + (implies (and (consp (next-inst s0)) + (equal (car (next-inst s0)) 'invokevirtual) + (equal (caddr (next-inst s0)) "inBox") + (equal (cadddr (next-inst s0)) 2) + + (equal this (top (pop (pop (stack (top-frame s0)))))) + (equal p1 (top (pop (stack (top-frame s0))))) + (equal p2 (top (stack (top-frame s0)))) + +; This next hyp is necessary because even if I know that the THIS object +; is an instance-of class "Point" I do not know that the "inBox" method +; hasn't been overridden! + + (equal (lookup-method "inBox" + (class-name-of-ref this (heap s0)) + (class-table s0)) + (\bf_inBox)) + (equal (inBox-clock this p1 p2 s1) + (inBox-clock this p1 p2 s0))) + (equal + (tjvm s0 (inBox-clock this p1 p2 s1)) + (make-state + (push (make-frame (+ 1 (pc (top-frame s0))) + (locals (top-frame s0)) + (push (if (inBox this p1 p2 s0) 1 0) + (popn 3 (stack (top-frame s0)))) + (program (top-frame s0))) + (pop (call-stack s0))) + (heap s0) + (class-table s0)))) + :hints (("Goal" :in-theory (disable tjvm-opener)))))) + + +(in-theory (disable inBox-clock inBox)) + +(defthm hackish-lemma1 + (equal + (inbox-clock + (top (pop (pop (pop (stack (top (call-stack s0))))))) + (top (pop (pop (stack (top (call-stack s0)))))) + (top (pop (stack (top (call-stack s0))))) + (make-state + (push + (make-frame + '3 + (cons (cons 'this + (top (pop (pop (pop (stack (top (call-stack s0)))))))) + (cons (cons 'p1 + (top (pop (pop (stack (top (call-stack s0))))))) + (cons (cons 'p2 + (top (pop (stack (top (call-stack s0)))))) + (cons (cons 'color + (top (stack (top (call-stack s0))))) + 'nil)))) + (push (top (pop (stack (top (call-stack s0))))) + (push (top (pop (pop (stack (top (call-stack s0)))))) + (push (top (pop (pop (pop (stack (top (call-stack s0))))))) + 'nil))) + '((load this) + (load p1) + (load p2) + (invokevirtual "ColoredPoint" "inBox" 2) + (ifeq 4) + (load this) + (load color) + (putfield "ColoredPoint" "color") + (return))) + (push (make-frame (+ 1 (pc (top (call-stack s0)))) + (locals (top (call-stack s0))) + (pop (pop (pop (pop (stack (top (call-stack s0))))))) + (program (top (call-stack s0)))) + (pop (call-stack s0)))) + (heap s0) + (class-table s0))) + (inbox-clock (top (pop (pop (pop (stack (top (call-stack s0))))))) + (top (pop (pop (stack (top (call-stack s0)))))) + (top (pop (stack (top (call-stack s0))))) + s0)) + :hints (("goal" :in-theory (enable inbox-clock)))) + +(defthm hackish-lemma2 + (equal + (inbox + (top (pop (pop (pop (stack (top (call-stack s0))))))) + (top (pop (pop (stack (top (call-stack s0)))))) + (top (pop (stack (top (call-stack s0))))) + (make-state + (push + (make-frame + '3 + (cons (cons 'this + (top (pop (pop (pop (stack (top (call-stack s0)))))))) + (cons (cons 'p1 + (top (pop (pop (stack (top (call-stack s0))))))) + (cons (cons 'p2 + (top (pop (stack (top (call-stack s0)))))) + (cons (cons 'color + (top (stack (top (call-stack s0))))) + 'nil)))) + (push (top (pop (stack (top (call-stack s0))))) + (push (top (pop (pop (stack (top (call-stack s0)))))) + (push (top (pop (pop (pop (stack (top (call-stack s0))))))) + 'nil))) + '((load this) + (load p1) + (load p2) + (invokevirtual "ColoredPoint" "inBox" 2) + (ifeq 4) + (load this) + (load color) + (putfield "ColoredPoint" "color") + (return))) + (push (make-frame (+ 1 (pc (top (call-stack s0)))) + (locals (top (call-stack s0))) + (pop (pop (pop (pop (stack (top (call-stack s0))))))) + (program (top (call-stack s0)))) + (pop (call-stack s0)))) + (heap s0) + (class-table s0))) + (inbox (top (pop (pop (pop (stack (top (call-stack s0))))))) + (top (pop (pop (stack (top (call-stack s0)))))) + (top (pop (stack (top (call-stack s0))))) + s0)) + :hints (("goal" :in-theory (enable inbox)))) + +; This lemma is not stated generally enough to allow it to be used. +; We need to introduce s1 in the lhs of the concl, as in example4. + +(defthm example5 + (implies (and (consp (next-inst s0)) + (equal (car (next-inst s0)) 'invokevirtual) + (equal (caddr (next-inst s0)) "setColorBox") + (equal (cadddr (next-inst s0)) 3) + + (equal this (top (pop (pop (pop (stack (top-frame s0))))))) + (equal p1 (top (pop (pop (stack (top-frame s0)))))) + (equal p2 (top (pop (stack (top-frame s0))))) + (equal color (top (stack (top-frame s0)))) + + (equal (lookup-method "inBox" + (class-name-of-ref this (heap s0)) + (class-table s0)) + (\bf_inBox)) + (equal (lookup-method "setColorBox" + (class-name-of-ref this (heap s0)) + (class-table s0)) + (\bf_setColorBox))) + (equal + (tjvm s0 (setColorBox-clock this p1 p2 color s0)) + (make-state + (push (make-frame (+ 1 (pc (top-frame s0))) + (locals (top-frame s0)) + (popn 4 (stack (top-frame s0))) + (program (top-frame s0))) + (pop (call-stack s0))) + (setColorBox-heap this p1 p2 color s0) + (class-table s0))))) + +; The above lemma may not look very interesting. But the following observation +; shows that it is: + +(defthm setColorBox-heap-property + (implies (and (refp ref) + (refp this)) + (equal (deref ref + (setColorBox-heap this p1 p2 color s)) + (if (and (equal ref this) + (inBox this p1 p2 s)) + (set-instance-field "ColoredPoint" "color" color + (deref this (heap s))) + (deref ref (heap s)))))) + +; Several problems have come to light. +; (1) The role of s1 in example4. +; (2) The more general difficulty of counting cycles in the presence of +; of overriding. I really need a predicate that says "this clock +; is appropriate for this method body" +; (3) Lack of evidence that something meaningful can be done with the heap. +; By this I mean to suggest work on extracting abstract objects from +; the heap. If the abstract object is an object in ACL2, this is +; probably straightforward. If it is some circular object, it must +; be represented more or less as a heap object. That being the case, +; it seems that this problem is really one of just getting used to +; a suitable bunch of primitives like deref and get-instance-field. diff --git a/books/workshops/2000/moore-manolios/partial-functions/mod-1-property.lisp b/books/workshops/2000/moore-manolios/partial-functions/mod-1-property.lisp new file mode 100644 index 0000000..3c25b47 --- /dev/null +++ b/books/workshops/2000/moore-manolios/partial-functions/mod-1-property.lisp @@ -0,0 +1,48 @@ +; Copyright (C) 2000 Panagiotis Manolios and J Strother Moore + +; This program is free software; you can redistribute it and/or modify +; it under the terms of the GNU General Public License as published by +; the Free Software Foundation; either version 2 of the License, or +; (at your option) any later version. + +; This program is distributed in the hope that it will be useful, +; but WITHOUT ANY WARRANTY; without even the implied warranty of +; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +; GNU General Public License for more details. + +; You should have received a copy of the GNU General Public License +; along with this program; if not, write to the Free Software +; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. + +; Written by Panagiotis Manolios who can be reached as follows. + +; Email: pete@cs.utexas.edu, moore@cs.utexas.edu + +; Postal Mail: +; Department of Computer Science +; The University of Texas at Austin +; Austin, TX 78701 USA + +; (certify-book "mod-1-property") + +(in-package "ACL2") + +(local (include-book "../../../../ihs/quotient-remainder-lemmas")) +(local (include-book "../../../../arithmetic/top-with-meta")) + +(defthm floor-int-1 + (implies (integerp x) + (equal (floor x 1) x))) + +(defthm floor-x-1 + (implies (rationalp x) + (equal (floor (- x 1) 1) + (- (floor x 1) 1))) + :hints (("Goal" :in-theory (disable floor)))) + +(defthm mod-1-property + (implies (and (rationalp x) + (not (integerp x))) + (and (< 0 (mod x 1)) + (< (mod x 1) 1))) + :rule-classes nil) diff --git a/books/workshops/2000/moore-manolios/partial-functions/report.lisp b/books/workshops/2000/moore-manolios/partial-functions/report.lisp new file mode 100644 index 0000000..d72d171 --- /dev/null +++ b/books/workshops/2000/moore-manolios/partial-functions/report.lisp @@ -0,0 +1,440 @@ +; Copyright (C) 2000 Panagiotis Manolios and J Strother Moore + +; This program is free software; you can redistribute it and/or modify +; it under the terms of the GNU General Public License as published by +; the Free Software Foundation; either version 2 of the License, or +; (at your option) any later version. + +; This program is distributed in the hope that it will be useful, +; but WITHOUT ANY WARRANTY; without even the implied warranty of +; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +; GNU General Public License for more details. + +; You should have received a copy of the GNU General Public License +; along with this program; if not, write to the Free Software +; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. + +; Written by Panagiotis Manolios who can be reached as follows. + +; Email: pete@cs.utexas.edu, moore@cs.utexas.edu + +; Postal Mail: +; Department of Computer Science +; The University of Texas at Austin +; Austin, TX 78701 USA + +; (certify-book "report") + +(in-package "ACL2") +(include-book "defpun") +(include-book "../../../../ihs/quotient-remainder-lemmas") +(include-book "../../../../arithmetic/top-with-meta") +(include-book "mod-1-property") + +; Section: Example Results + +(defpun offset (n) + (declare (xargs :witness fix)) + (if (equal n 0) + 0 + (+ 1 (offset (- n 1))))) + +(defun quotm (i j) + (let ((temp (floor (/ i j) 1))) + (if (< temp 0) + 0 + (+ 1 temp)))) + +(in-theory (disable floor)) + +; The next two events illustrate a little trick. To prove that the +; domain in quot, below, is closed, i.e., to do the guard proof for +; quot, I need to know that the-quot ``always'' returns a rational. +; But we have implemented no means of providing hints to be inserted +; between the admission of the automatically generated the-quot and +; its guard verification. So I define the-quot now and prove what I +; need. Then I do the defpun which will REDUNDANTLY define it. Cool. + +(defun the-quot (i j) + (declare (xargs :guard (and (rationalp i) + (rationalp j) + (< 0 j)) + +; Modified by Matt K. after Version 3.0.1: This measure was formerly +; (quotm i j), but it needed to change so that the introduction of +; the-quote in the defpun below would be redundant, after the fix for +; the soundness bug in the redundancy criterion for defun. + + :measure (if (and (rationalp i) + (rationalp j) + (< 0 j)) + (quotm i j) + 0) + :verify-guards nil)) + (if (and (rationalp i) + (rationalp j) + (< 0 j)) + (if (<= i 0) 0 (+ 1 (the-quot (- i j) j))) + 'undef)) + +(defthm rationalp-the-quot + (implies (and (rationalp i) + (rationalp j) + (< 0 j)) + (rationalp (the-quot i j))) + :rule-classes :type-prescription) + +(defpun quot (i j) + (declare (xargs :gdomain (and (rationalp i) + (rationalp j) + (< 0 j)) + :measure (quotm i j))) + (if (<= i 0) 0 (+ 1 (quot (- i j) j)))) + +(defpun 3n+1 (n) + (if (<= n 1) + n + (3n+1 (if (evenp n) + (/ n 2) + (+ (* 3 n) 1))))) + + +(defstub haltedp (s) t) +(defstub step1 (s) t) + +(defpun stepw (s) + (if (haltedp s) + s + (stepw (step1 s)))) + +; Section: Consistency + +(defun natural-induction (n) + (if (zp n) + t + (natural-induction (- n 1)))) + +(defmacro show-g-inconsistent nil + '(ld '((defstub g (n) t) + + (defaxiom g-axiom + (equal (g n) + (if (equal n 0) + nil + (cons nil (g (- n 1))))) + :rule-classes :definition) + + (defthm g-induction + t + :rule-classes ((:induction + :pattern (g n) + :scheme (natural-induction n)))) + + (defthm len-of-g + (implies (natp n) + (equal (len (g n)) n))) + + (defun bad-lemma-hint (k n) + (if (zp k) + (list k n) + (bad-lemma-hint (- k 1) (- n 1)))) + + (defthm bad-lemma + (implies (and (natpp k) + (integerp n) + (< n 0)) + (< k (len (g n)))) + :hints (("Goal" :induct (bad-lemma-hint k n)) + ("Subgoal *1/1" :use g-axiom))) + + (defthm bad-theorem + nil + :rule-classes nil + :hints (("Goal" :use (:instance bad-lemma + (k (len (g -1))) + (n -1))))) + (ubt! 'g)) + :ld-pre-eval-print t)) + +(defpun undef (x) + (declare (xargs :witness car)) + (undef x) + :rule-classes nil) + +; Section: Witnessing Equations + +(defpun h (n) + (declare (xargs :witness fix)) + (if (equal n 0) 0 (+ 1 (h (- n 1))))) + +(defthm h-induction + t + :rule-classes ((:induction + :pattern (h n) + :scheme (natural-induction n)))) + +(defthm h-is-id-on-naturals + (implies (natp n) + (equal (h n) n))) + +(defun h22/7 (n) + (if (natp n) + n + (+ 22/7 n))) + +(defthm h22/7-satisfies-h-def + (equal (h22/7 n) + (if (equal n 0) 0 (+ 1 (h22/7 (- n 1))))) + :rule-classes nil) + +(defthm h-prop-0 + (acl2-numberp (h n)) + :rule-classes :type-prescription + :hints (("Goal" :use h-def))) + +(encapsulate + nil + (local + (defthm lemma1 + (implies (natp n) + (equal (h n) n)) + :rule-classes nil + :hints (("Goal" :induct (natural-induction n))))) + + (local + (defthm lemma2 + (implies (and (integerp n) + (< 0 n)) + (equal (h (- n)) (+ (- (h -1) -1) (- n)))) + :rule-classes nil + :hints (("Goal" :induct (natural-induction n))))) + + (defun hconst () (+ 1 (h -1) )) + + (defthm acl2-numberp-hconst + (acl2-numberp (hconst))) + + (in-theory (disable (:executable-counterpart hconst))) + + (defthm h-prop-1 + (implies (integerp n) + (equal (h n) + (if (<= 0 n) + n + (+ n (hconst))))) + :rule-classes nil + :hints (("Goal" :use ((:instance lemma1) + (:instance lemma2 (n (- n)))))))) + +(encapsulate + nil + (local + (defthm lemma1 + (implies (and (acl2-numberp x) + (not (integerp x)) + (natp n)) + (equal (h (+ n x)) + (+ n (h x)))) + :rule-classes nil + :hints (("Goal" :induct (natural-induction n))))) + + (local + (defthm lemma2 + (implies (and (acl2-numberp x) + (not (integerp x)) + (integerp n) + (< 0 n)) + (equal (h (+ (- n) x)) + (+ (- n) (h x)))) + :rule-classes nil + :hints (("Goal" :induct (natural-induction n))))) + + (local + (defthm lemma3 + (implies (and (acl2-numberp x) + (not (integerp x)) + (integerp n)) + (equal (h (+ n x)) + (+ n (h x)))) + :rule-classes nil + :hints (("Goal" :use ((:instance lemma1) + (:instance lemma2 (n (- n)))))))) + +; Consider any rational x. It can be represented by an integer n plus some +; epsilon between 0 and 1. H-prop-5 tells us that (h x) is n+(h epsilon). + + (defthm h-prop-2 + (implies (and (rationalp x) + (not (integerp x))) + (equal (h x) + (+ (floor x 1) (h (mod x 1))))) + :rule-classes nil + :hints (("Goal" :use (:instance lemma3 + (x (mod x 1)) + (n (floor x 1)))))) + + ) + +; Here is a witness for h that demonstrates that it is not just a linear +; offset. + +(encapsulate ((arbitrary-constant (x) t)) + (local (defun arbitrary-constant (x) (fix x))) + (defthm acl2-numberp-arbitrary-constant + (acl2-numberp (arbitrary-constant x)) + :rule-classes :type-prescription)) + +(defun hv (x) + (if (integerp x) + x + (if (rationalp x) + (+ (floor x 1) (arbitrary-constant (mod x 1))) + (fix x)))) + +(defthm hv-satisfies-h-def + (equal (hv n) + (if (equal n 0) 0 (+ 1 (hv (- n 1))))) + :hints (("Goal" :in-theory (disable floor))) + :rule-classes nil) + +; We can make this general observation very concrete by letting the +; arbitrary-constant be a particular function. + +(defun concrete-arbitrary-constant (x) + (case x + (1/2 100) + (1/3 -273) + (1/4 57) + (1/5 123) + (otherwise (* x x)))) + +(defun concrete-hv (x) + (if (integerp x) + x + (if (rationalp x) + (+ (floor x 1) (concrete-arbitrary-constant (mod x 1))) + (fix x)))) + +(defthm concrete-hv-satisfies-h-def + (equal (concrete-hv n) + (if (equal n 0) 0 (+ 1 (concrete-hv (- n 1))))) + :hints (("Goal" :in-theory (disable floor concrete-arbitrary-constant))) + :rule-classes nil) + +(set-ignore-ok t) +(set-irrelevant-formals-ok t) + +(defpun z (x) + (declare (xargs :witness (lambda (x) 0))) + (if (zip x) + 0 + (* (z (- x 1)) + (z (+ x 1))))) + +(defun integer-induction (i) + (if (integerp i) + (if (equal i 0) + t + (if (< i 0) + (integer-induction (+ i 1)) + (integer-induction (- i 1)))) + t)) + +(defthm z-induction + t + :rule-classes ((:induction + :pattern (z i) + :scheme (integer-induction i)))) + +(defthm z-is-0 + (equal (z x) 0)) + +(defpun three (x) + (declare (xargs :witness (lambda (x) 1))) + (if (equal x nil) + (let ((i (three x))) + (if (and (integerp i) (<= 1 i) (<= i 3)) + i + 1)) + 1) + :rule-classes nil) + +(defun three1 (x) (if (equal x nil) 1 1)) +(defun three2 (x) (if (equal x nil) 2 1)) +(defun three3 (x) (if (equal x nil) 3 1)) + +(defthm three-and-only-three + (and (equal (three1 x) + (if (equal x nil) + (let ((i (three1 x))) + (if (and (<= 1 i) (<= i 3)) + i + 1)) + 1)) + (equal (three2 x) + (if (equal x nil) + (let ((i (three2 x))) + (if (and (<= 1 i) (<= i 3)) + i + 1)) + 1)) + (equal (three3 x) + (if (equal x nil) + (let ((i (three3 x))) + (if (and (<= 1 i) (<= i 3)) + i + 1)) + 1)) + (or (equal (three x) (three1 x)) + (equal (three x) (three2 x)) + (equal (three x) (three3 x)))) + :hints (("Goal" :use three-def)) + :rule-classes nil) + +; Section: Domains + +(defpun gnat (n) + (declare (xargs :domain (natp n) :measure n)) + (if (equal n 0) + nil + (cons nil (gnat (- n 1))))) + + +(defpun gsev (n) + (declare (xargs :domain (and (integerp n) (<= -7 n)) :measure (+ 8 n))) + (if (equal n 0) + nil + (cons nil (gsev (- n 1))))) + +; Tail Recursion + +(defpun trfact (n a) + (if (equal n 0) + a + (trfact (- n 1) (* n a)))) + +(defun fact (n) (if (zp n) 1 (* n (fact (- n 1))))) + +(defun fact1 (n a) (if (zp n) a (fact1 (- n 1) (* n a)))) +(defthm trfact-induction + t + :rule-classes ((:induction + :pattern (trfact n a) + :scheme (fact1 n a)))) + +(defthm trfact-is-fact-on-nats + (implies (and (natp n) + (acl2-numberp a)) + (equal (trfact n a) (* a (fact n))))) + + +; It would be nice if we could switch packages now from "ACL2" to "TJVM" +; and prove some theorems about the tjvm using its partial function semantics. +; But it is not permitted by Common Lisp to switch packages in the middle of a +; file. So we proved the results we wanted in tjvm-examples.lisp. + +(include-book "tjvm-examples") + +; We recommend that you visit that file to see the tjvm results cited +; in the paper. + diff --git a/books/workshops/2000/moore-manolios/partial-functions/tjvm-examples.acl2 b/books/workshops/2000/moore-manolios/partial-functions/tjvm-examples.acl2 new file mode 100644 index 0000000..c4f9e31 --- /dev/null +++ b/books/workshops/2000/moore-manolios/partial-functions/tjvm-examples.acl2 @@ -0,0 +1,4 @@ +(value :q) +(lp) +(include-book "examples") +(certify-book "tjvm-examples" ? t) diff --git a/books/workshops/2000/moore-manolios/partial-functions/tjvm-examples.lisp b/books/workshops/2000/moore-manolios/partial-functions/tjvm-examples.lisp new file mode 100644 index 0000000..3ec1703 --- /dev/null +++ b/books/workshops/2000/moore-manolios/partial-functions/tjvm-examples.lisp @@ -0,0 +1,195 @@ +; Copyright (C) 2000 Panagiotis Manolios and J Strother Moore + +; This program is free software; you can redistribute it and/or modify +; it under the terms of the GNU General Public License as published by +; the Free Software Foundation; either version 2 of the License, or +; (at your option) any later version. + +; This program is distributed in the hope that it will be useful, +; but WITHOUT ANY WARRANTY; without even the implied warranty of +; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +; GNU General Public License for more details. + +; You should have received a copy of the GNU General Public License +; along with this program; if not, write to the Free Software +; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. + +; Written by Panagiotis Manolios who can be reached as follows. + +; Email: pete@cs.utexas.edu, moore@cs.utexas.edu + +; Postal Mail: +; Department of Computer Science +; The University of Texas at Austin +; Austin, TX 78701 USA + +; (include-book "/v/hank/v104/text/tjvm/examples") +; (certify-book "tjvm-examples" 1) +(in-package "TJVM") + +(include-book "defpun") + +(defmacro defpun (&rest rest) (cons 'acl2::defpun rest)) + +(defun haltedp (s) (equal s (step s))) + +(defpun stepw (s) + (if (haltedp s) + s + (stepw (step s)))) + +(defun == (a b)(equal (stepw a) (stepw b))) + +(defequiv ==) + +(in-theory (disable step-opener)) + +(defthm stepw-step + (equal (stepw s) (stepw (step s))) + :rule-classes nil) + +; This event is here only so we can exhibit it in the paper. + +(defthm ==-step + (== (make-state call-stack heap class-table) + (step (make-state call-stack heap class-table))) + :rule-classes nil) + +(defthm ==-stepper + (implies (and (consp (NTH (PC (TOP call-stack)) + (PROGRAM (TOP call-stack)))) + (not (equal (car (NTH (PC (TOP call-stack)) + (PROGRAM (TOP call-stack)))) + 'invokestatic))) + (== (make-state + call-stack + heap + class-table) + (step (make-state + call-stack + heap + class-table)))) + :hints (("Goal" :in-theory (disable step)))) + +(defthm general-==-stepper + (implies (equal call-stack call-stack) ; not an abbreviation rule! + (== (make-state call-stack + heap + class-table) + (step (make-state call-stack + heap + class-table))))) +(defun stepn (s n) + (if (zp n) + s + (stepn (step s) (- n 1)))) + +(defthm ==-stepn + (== (stepn s n) s)) + +(defthm ==-Y + (implies (== (stepn s1 n) + (stepn s2 m)) + (== s1 s2)) + :rule-classes nil) + +(in-theory (disable general-==-stepper ==)) +(in-theory (enable step)) + +(defun next-instruction (call-stack) + (nth (pc (top call-stack)) + (program (top call-stack)))) + +; A consequence of this setup is that for every primitive instruction +; except for invokestatic we have a theorem like: + +(defthm ==-load + (implies (and (equal (next-instruction call-stack) + `(load ,var))) + (== (make-state call-stack + heap + class-table) + (make-state + (push (make-frame (+ 1 (pc (top call-stack))) + (locals (top call-stack)) + (push (binding var (locals (top call-stack))) + (stack (top call-stack))) + (program (top call-stack))) + (pop call-stack)) + heap + class-table))) + :rule-classes nil) + +; Ok, that completes the general work. Now let's deal with fact. + +(defun fact-==-hint (call-stack heap table n) + (if (zp n) + (list call-stack heap table) + (fact-==-hint + (push (make-frame 6 + (list (cons 'n (top (stack (top call-stack))))) + (push (- (top (stack (top call-stack))) 1) + (push (top (stack (top call-stack))) + nil)) + (method-program (\bf_fact))) + (push (make-frame (+ 1 (pc (top call-stack))) + (locals (top call-stack)) + (pop (stack (top call-stack))) + (program (top call-stack))) + (pop call-stack))) + heap + table + (- n 1)))) + +(defun Math-class-loadedp (class-table) + (equal (assoc-equal "Math" class-table) + (\bfMath-class))) + +; The following lemma is proved just so we can prove the next +; theorem without any hints. The hintless version is shown in the paper. + +(defthm ==-invokestatic-fact-lemma + (implies (and (equal (next-instruction call-stack) + '(invokestatic "Math" "fact" 1)) + (Math-class-loadedp class-table) + (equal n (top (stack (top call-stack)))) + (natp n)) + (== (make-state call-stack + heap + class-table) + (make-state + (push (make-frame (+ 1 (pc (top call-stack))) + (locals (top call-stack)) + (push (fact n) + (pop (stack (top call-stack)))) + (program (top call-stack))) + (pop call-stack)) + heap + class-table))) + :hints (("Goal" :in-theory (enable general-==-stepper top-frame) + :restrict ((general-==-STEPPER + ((call-stack call-stack) + (heap heap) + (class-table class-table)))) + :induct (fact-==-hint call-stack heap class-table n)))) + +(defthm ==-invokestatic-fact + (implies (and (equal (next-instruction call-stack) + '(invokestatic "Math" "fact" 1)) + (Math-class-loadedp class-table) + (equal n (top (stack (top call-stack)))) + (natp n)) + (== (make-state call-stack + heap + class-table) + (make-state + (push (make-frame (+ 1 (pc (top call-stack))) + (locals (top call-stack)) + (push (fact n) + (pop (stack (top call-stack)))) + (program (top call-stack))) + (pop call-stack)) + heap + class-table)))) + + diff --git a/books/workshops/2000/moore-manolios/partial-functions/tjvm.acl2 b/books/workshops/2000/moore-manolios/partial-functions/tjvm.acl2 new file mode 100644 index 0000000..80e1ab5 --- /dev/null +++ b/books/workshops/2000/moore-manolios/partial-functions/tjvm.acl2 @@ -0,0 +1,12 @@ +(value :q) +(lp) + + (DEFPKG "TJVM" + (set-difference-equal + (union-eq '(ASSOC-EQUAL LEN NTH ZP SYNTAXP + QUOTEP FIX NFIX E0-ORDINALP E0-ORD-<) + (union-eq *acl2-exports* + *common-lisp-symbols-from-main-lisp-package*)) + '(PC PROGRAM PUSH POP REVERSE STEP ++))) + +(certify-book "tjvm" ? t) diff --git a/books/workshops/2000/moore-manolios/partial-functions/tjvm.lisp b/books/workshops/2000/moore-manolios/partial-functions/tjvm.lisp new file mode 100644 index 0000000..0e515a2 --- /dev/null +++ b/books/workshops/2000/moore-manolios/partial-functions/tjvm.lisp @@ -0,0 +1,620 @@ +; Copyright (C) 1999 J Strother Moore + +; This book is free software; you can redistribute it and/or modify +; it under the terms of the GNU General Public License as published by +; the Free Software Foundation; either version 2 of the License, or +; (at your option) any later version. + +; This book is distributed in the hope that it will be useful, +; but WITHOUT ANY WARRANTY; without even the implied warranty of +; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +; GNU General Public License for more details. + +; You should have received a copy of the GNU General Public License +; along with this book; if not, write to the Free Software +; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. + +; This book defines the ``Toy Java Virtual Machine'' tjvm, discussed in the +; paper + +; Proving Theorems about Java-like Byte Code +; by J Strother Moore + +#| +; Certification Instructions. + +; To certify this book, connect to the directory containing this file, fire +; up ACL2 and execute + +(DEFPKG "TJVM" + (set-difference-equal (union-eq '(ASSOC-EQUAL LEN NTH ZP SYNTAXP + QUOTEP FIX NFIX E0-ORDINALP E0-ORD-<) + (union-eq *acl2-exports* + *common-lisp-symbols-from-main-lisp-package*)) + '(PC PROGRAM PUSH POP REVERSE STEP ++))) + +; Notes on the Imports Above + +; The first set of symbols, ASSOC-EQUAL, NTH, ..., NFIX are among many +; useful function symbols defined in ACL2 that have been omitted from +; *acl2-exports*! I delete PUSH, ..., ++ because they are defined in +; Common Lisp in ways different than I wish to define them below. + +; Then do + +(certify-book "tjvm" 1) + +|# +(in-package "TJVM") + +; ----------------------------------------------------------------------------- +; Utilities + +(defun push (obj stack) (cons obj stack)) +(defun top (stack) (car stack)) +(defun pop (stack) (cdr stack)) + +;(defun assoc-equal (x alist) +; (cond ((endp alist) nil) +; ((equal x (car (car alist))) +; (car alist)) +; (t (assoc-equal x (cdr alist))))) + +(defun bound? (x alist) (assoc-equal x alist)) + +(defun bind (x y alist) + (cond ((endp alist) (list (cons x y))) + ((equal x (car (car alist))) + (cons (cons x y) (cdr alist))) + (t (cons (car alist) (bind x y (cdr alist)))))) + +(defun binding (x alist) (cdr (assoc-equal x alist))) + +(defun op-code (inst) (car inst)) +(defun arg1 (inst) (car (cdr inst))) +(defun arg2 (inst) (car (cdr (cdr inst)))) +(defun arg3 (inst) (car (cdr (cdr (cdr inst))))) + +;(defun nth (i lst) +; (if (zp i) +; (car lst) +; (nth (- i 1) (cdr lst)))) + +(defun reverse (x) + (if (consp x) + (append (reverse (cdr x)) (list (car x))) + nil)) + +; ----------------------------------------------------------------------------- +; States + +(defun make-state (call-stack heap class-table) + (list call-stack heap class-table)) +(defun call-stack (s) (nth 0 s)) +(defun heap (s) (nth 1 s)) +(defun class-table (s) (nth 2 s)) + +; ----------------------------------------------------------------------------- +; Frames + +(defun make-frame (pc locals stack program) + (list pc locals stack program)) + +(defun pc (frame) (nth 0 frame)) +(defun locals (frame) (nth 1 frame)) +(defun stack (frame) (nth 2 frame)) +(defun program (frame) (nth 3 frame)) + +(defun top-frame (s) (top (call-stack s))) + +; ----------------------------------------------------------------------------- +; Class Declarations and the Class Table + +; The class table of a state is an alist. Each entry in a class table is +; a "class declaration" and is of the form + +; (class-name super-class-names fields defs) + +(defun make-class-decl (name superclasses fields methods) + (list name superclasses fields methods)) + +(defun class-decl-name (dcl) + (nth 0 dcl)) +(defun class-decl-superclasses (dcl) + (nth 1 dcl)) +(defun class-decl-fields (dcl) + (nth 2 dcl)) +(defun class-decl-methods (dcl) + (nth 3 dcl)) + +; ----------------------------------------------------------------------------- +; Method Declarations + +; The methods component of a class declaration is a list of method definitions. +; A method definition is a list of the form + +; (name formals . program) + +; We never build these declarations but just enter list constants for them, + +; Note the similarity to our old notion of a program definition. We +; will use strings to name methods now. + +; Method definitions will be constructed by expressions such as: + +; ("move" (dx dy) +; (load this) +; (load this) +; (getfield "Point" "x") +; (load dx) +; (add) +; (putfield "Point" "x") ; this.x = this.x + dx; +; (load this) +; (load this) +; (getfield "Point" "y") +; (load dy) +; (add) +; (putfield "Point" "y") ; this.y = this.y + dy; +; (push 1) +; (xreturn))) ; return 1; + +; Provided this method is defined in the class "Point" it can be invoked by + +; (invokevirtual "Point" "move" 2) + +; This assumes that the stack, at the time of invocation, contains an +; reference to an object of type "Point" and two numbers, dx and dy. + +; The accessors for methods are: + +(defun method-name (m) + (nth 0 m)) +(defun method-formals (m) + (nth 1 m)) +(defun method-program (m) + (cddr m)) + +; ----------------------------------------------------------------------------- +; (PUSH const) Instruction + +(defun execute-PUSH (inst s) + (make-state + (push (make-frame (+ 1 (pc (top-frame s))) + (locals (top-frame s)) + (push (arg1 inst) + (stack (top-frame s))) + (program (top-frame s))) + (pop (call-stack s))) + (heap s) + (class-table s))) + +; ----------------------------------------------------------------------------- +; (POP) Instruction + +(defun execute-POP (inst s) + (declare (ignore inst)) + (make-state + (push (make-frame (+ 1 (pc (top-frame s))) + (locals (top-frame s)) + (pop (stack (top-frame s))) + (program (top-frame s))) + (pop (call-stack s))) + (heap s) + (class-table s))) + +; ----------------------------------------------------------------------------- +; (LOAD var) Instruction + +(defun execute-LOAD (inst s) + (make-state + (push (make-frame (+ 1 (pc (top-frame s))) + (locals (top-frame s)) + (push (binding (arg1 inst) + (locals (top-frame s))) + (stack (top-frame s))) + (program (top-frame s))) + (pop (call-stack s))) + (heap s) + (class-table s))) + +; ----------------------------------------------------------------------------- +; (STORE var) Instruction + +(defun execute-STORE (inst s) + (make-state + (push (make-frame (+ 1 (pc (top-frame s))) + (bind (arg1 inst) + (top (stack (top-frame s))) + (locals (top-frame s))) + (pop (stack (top-frame s))) + (program (top-frame s))) + (pop (call-stack s))) + (heap s) + (class-table s))) + +; ----------------------------------------------------------------------------- +; (ADD) Instruction + +(defun execute-ADD (inst s) + (declare (ignore inst)) + (make-state + (push (make-frame (+ 1 (pc (top-frame s))) + (locals (top-frame s)) + (push (+ (top (pop (stack (top-frame s)))) + (top (stack (top-frame s)))) + (pop (pop (stack (top-frame s))))) + (program (top-frame s))) + (pop (call-stack s))) + (heap s) + (class-table s))) + +; ----------------------------------------------------------------------------- +; (SUB) Instruction + +(defun execute-SUB (inst s) + (declare (ignore inst)) + (make-state + (push (make-frame (+ 1 (pc (top-frame s))) + (locals (top-frame s)) + (push (- (top (pop (stack (top-frame s)))) + (top (stack (top-frame s)))) + (pop (pop (stack (top-frame s))))) + (program (top-frame s))) + (pop (call-stack s))) + (heap s) + (class-table s))) + +; ----------------------------------------------------------------------------- +; (MUL) Instruction + +(defun execute-MUL (inst s) + (declare (ignore inst)) + (make-state + (push (make-frame (+ 1 (pc (top-frame s))) + (locals (top-frame s)) + (push (* (top (pop (stack (top-frame s)))) + (top (stack (top-frame s)))) + (pop (pop (stack (top-frame s))))) + (program (top-frame s))) + (pop (call-stack s))) + (heap s) + (class-table s))) + +; ----------------------------------------------------------------------------- +; (GOTO pc) Instruction + +(defun execute-GOTO (inst s) + (make-state + (push (make-frame (+ (arg1 inst) (pc (top-frame s))) + (locals (top-frame s)) + (stack (top-frame s)) + (program (top-frame s))) + (pop (call-stack s))) + (heap s) + (class-table s))) + +; ----------------------------------------------------------------------------- +; (IFEQ pc) Instruction + +(defun execute-IFEQ (inst s) + (make-state + (push (make-frame (if (equal (top (stack (top-frame s))) 0) + (+ (arg1 inst) (pc (top-frame s))) + (+ 1 (pc (top-frame s)))) + (locals (top-frame s)) + (pop (stack (top-frame s))) + (program (top-frame s))) + (pop (call-stack s))) + (heap s) + (class-table s))) + +; ----------------------------------------------------------------------------- +; (IFGT pc) Instruction + +(defun execute-IFGT (inst s) + (make-state + (push (make-frame (if (> (top (stack (top-frame s))) 0) + (+ (arg1 inst) (pc (top-frame s))) + (+ 1 (pc (top-frame s)))) + (locals (top-frame s)) + (pop (stack (top-frame s))) + (program (top-frame s))) + (pop (call-stack s))) + (heap s) + (class-table s))) + +; ----------------------------------------------------------------------------- +; (IFLE pc) Instruction + +(defun execute-IFLE (inst s) + (make-state + (push (make-frame (if (<= (top (stack (top-frame s))) 0) + (+ (arg1 inst) (pc (top-frame s))) + (+ 1 (pc (top-frame s)))) + (locals (top-frame s)) + (pop (stack (top-frame s))) + (program (top-frame s))) + (pop (call-stack s))) + (heap s) + (class-table s))) + + +; ----------------------------------------------------------------------------- +; (NEW "class") Instruction + +(defun build-class-field-bindings (field-names) + (if (endp field-names) + nil + (cons (cons (car field-names) 0) + (build-class-field-bindings (cdr field-names))))) + +(defun build-immediate-instance-data (class-name class-table) + (cons class-name + (build-class-field-bindings + (class-decl-fields + (bound? class-name class-table))))) + +(defun build-an-instance (class-names class-table) + (if (endp class-names) + nil + (cons (build-immediate-instance-data (car class-names) class-table) + (build-an-instance (cdr class-names) class-table)))) + +(defun refp (x) + (and (consp x) + (equal (car x) 'ref) + (consp (cdr x)) + (integerp (cadr x)) + (equal (cddr x) nil))) + +(defun execute-NEW (inst s) + (let* ((class-name (arg1 inst)) + (class-table (class-table s)) + (new-object (build-an-instance + (cons class-name + (class-decl-superclasses + (bound? class-name class-table))) + class-table)) + (new-address (len (heap s)))) + (make-state + (push (make-frame (+ 1 (pc (top-frame s))) + (locals (top-frame s)) + (push (list 'REF new-address) + (stack (top-frame s))) + (program (top-frame s))) + (pop (call-stack s))) + (bind new-address new-object (heap s)) + (class-table s)))) + + +; ----------------------------------------------------------------------------- +; (GETFIELD "class" "field") Instruction + +(defun deref (ref heap) + (binding (cadr ref) heap)) + +(defun field-value (class-name field-name instance) + (binding field-name + (binding class-name instance))) + +(defun execute-GETFIELD (inst s) + (let* ((class-name (arg1 inst)) + (field-name (arg2 inst)) + (instance (deref (top (stack (top-frame s))) (heap s))) + (field-value (field-value class-name field-name instance))) + (make-state + (push (make-frame (+ 1 (pc (top-frame s))) + (locals (top-frame s)) + (push field-value + (pop (stack (top-frame s)))) + (program (top-frame s))) + (pop (call-stack s))) + (heap s) + (class-table s)))) + +; ----------------------------------------------------------------------------- +; (PUTFIELD "class" "field") Instruction + +(defun set-instance-field (class-name field-name value instance) + (bind class-name + (bind field-name value + (binding class-name instance)) + instance)) + +(defun execute-PUTFIELD (inst s) + (let* ((class-name (arg1 inst)) + (field-name (arg2 inst)) + (value (top (stack (top-frame s)))) + (instance (deref (top (pop (stack (top-frame s)))) (heap s))) + (address (cadr (top (pop (stack (top-frame s))))))) + (make-state + (push (make-frame (+ 1 (pc (top-frame s))) + (locals (top-frame s)) + (pop (pop (stack (top-frame s)))) + (program (top-frame s))) + (pop (call-stack s))) + (bind address + (set-instance-field class-name field-name value instance) + (heap s)) + (class-table s)))) + + +; ----------------------------------------------------------------------------- +; (INSTANCEOF "class") + +(defun execute-INSTANCEOF (inst s) + (let* ((class-name (arg1 inst)) + (instance (deref (top (stack (top-frame s))) (heap s)))) + (make-state + (push (make-frame (+ 1 (pc (top-frame s))) + (locals (top-frame s)) + (push (if (bound? class-name instance) + 1 + 0) + (pop (stack (top-frame s)))) + (program (top-frame s))) + (pop (call-stack s))) + (heap s) + (class-table s)))) + + + +; ----------------------------------------------------------------------------- +; (INVOKEVIRTUAL "class" "name" n) Instruction + +(defun bind-formals (rformals stack) + (if (endp rformals) + nil + (cons (cons (car rformals) (top stack)) + (bind-formals (cdr rformals) (pop stack))))) + +(defun popn (n stack) + (if (zp n) + stack + (popn (- n 1) (pop stack)))) + +(defun class-name-of-ref (ref heap) + (car (car (deref ref heap)))) + +(defun lookup-method-in-superclasses (name classes class-table) + (cond ((endp classes) nil) + (t (let* ((class-name (car classes)) + (class-decl (bound? class-name class-table)) + (method (bound? name (class-decl-methods class-decl)))) + (if method + method + (lookup-method-in-superclasses name (cdr classes) + class-table)))))) + +(defun lookup-method (name class-name class-table) + (lookup-method-in-superclasses name + (cons class-name + (class-decl-superclasses + (bound? class-name class-table))) + class-table)) + +(defun execute-INVOKEVIRTUAL (inst s) + (let* ((method-name (arg2 inst)) + (nformals (arg3 inst)) + (obj-ref (top (popn nformals (stack (top-frame s))))) + (obj-class-name (class-name-of-ref obj-ref (heap s))) + (closest-method + (lookup-method method-name + obj-class-name + (class-table s))) + (vars (cons 'this (method-formals closest-method))) + (prog (method-program closest-method))) + (make-state + (push (make-frame 0 + (reverse + (bind-formals (reverse vars) + (stack (top-frame s)))) + nil + prog) + (push (make-frame (+ 1 (pc (top-frame s))) + (locals (top-frame s)) + (popn (len vars) + (stack (top-frame s))) + (program (top-frame s))) + (pop (call-stack s)))) + (heap s) + (class-table s)))) + +; ----------------------------------------------------------------------------- +; (INVOKESTATIC "class" "name" n) Instruction + +(defun execute-INVOKESTATIC (inst s) + (let* ((class-name (arg1 inst)) + (method-name (arg2 inst)) + (closest-method + (lookup-method method-name + class-name + (class-table s))) + (vars (method-formals closest-method)) + (prog (method-program closest-method))) + (make-state + (push (make-frame 0 + (reverse + (bind-formals (reverse vars) + (stack (top-frame s)))) + nil + prog) + (push (make-frame (+ 1 (pc (top-frame s))) + (locals (top-frame s)) + (popn (len vars) + (stack (top-frame s))) + (program (top-frame s))) + (pop (call-stack s)))) + (heap s) + (class-table s)))) + +; ----------------------------------------------------------------------------- +; (RETURN) Instruction + +(defun execute-RETURN (inst s) + (declare (ignore inst)) + (let ((caller-frame (top (pop (call-stack s))))) + (make-state + (push (make-frame (pc caller-frame) + (locals caller-frame) + (stack caller-frame) + (program caller-frame)) + (pop (pop (call-stack s)))) + (heap s) + (class-table s)))) + +; ----------------------------------------------------------------------------- +; (XRETURN) Instruction + +(defun execute-XRETURN (inst s) + (declare (ignore inst)) + (let ((val (top (stack (top-frame s)))) + (caller-frame (top (pop (call-stack s))))) + (make-state + (push (make-frame (pc caller-frame) + (locals caller-frame) + (push val (stack caller-frame)) + (program caller-frame)) + (pop (pop (call-stack s)))) + (heap s) + (class-table s)))) + +; ----------------------------------------------------------------------------- +; Putting it all together + +(defun next-inst (s) + (nth (pc (top-frame s)) + (program (top-frame s)))) + +(defun do-inst (inst s) + (case (op-code inst) + (PUSH (execute-PUSH inst s)) + (POP (execute-POP inst s)) + (LOAD (execute-LOAD inst s)) + (STORE (execute-STORE inst s)) + (ADD (execute-ADD inst s)) + (SUB (execute-SUB inst s)) + (MUL (execute-MUL inst s)) + (GOTO (execute-GOTO inst s)) + (IFEQ (execute-IFEQ inst s)) + (IFGT (execute-IFGT inst s)) + (IFLE (execute-IFLE inst s)) + (INVOKEVIRTUAL (execute-INVOKEVIRTUAL inst s)) + (INVOKESTATIC (execute-INVOKESTATIC inst s)) + (RETURN (execute-RETURN inst s)) + (XRETURN (execute-XRETURN inst s)) + (NEW (execute-NEW inst s)) + (GETFIELD (execute-GETFIELD inst s)) + (PUTFIELD (execute-PUTFIELD inst s)) + (INSTANCEOF (execute-INSTANCEOF inst s)) + (HALT s) + (otherwise s))) + +(defun step (s) + (do-inst (next-inst s) s)) + +(defun tjvm (s n) + (if (zp n) + s + (tjvm (step s) (- n 1)))) + |