diff options
Diffstat (limited to 'books/workshops/2004/davis/support/instance.lisp')
| -rw-r--r-- | books/workshops/2004/davis/support/instance.lisp | 675 |
1 files changed, 675 insertions, 0 deletions
diff --git a/books/workshops/2004/davis/support/instance.lisp b/books/workshops/2004/davis/support/instance.lisp new file mode 100644 index 0000000..cd6d922 --- /dev/null +++ b/books/workshops/2004/davis/support/instance.lisp @@ -0,0 +1,675 @@ +; Fully Ordered Finite Sets, Version 0.9 +; Copyright (C) 2003, 2004 Kookamara LLC +; +; Contact: +; +; Kookamara LLC +; 11410 Windermere Meadows +; Austin, TX 78759, USA +; http://www.kookamara.com/ +; +; License: (An MIT/X11-style license) +; +; Permission is hereby granted, free of charge, to any person obtaining a +; copy of this software and associated documentation files (the "Software"), +; to deal in the Software without restriction, including without limitation +; the rights to use, copy, modify, merge, publish, distribute, sublicense, +; and/or sell copies of the Software, and to permit persons to whom the +; Software is furnished to do so, subject to the following conditions: +; +; The above copyright notice and this permission notice shall be included in +; all copies or substantial portions of the Software. +; +; THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +; IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +; FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +; AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +; LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING +; FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER +; DEALINGS IN THE SOFTWARE. +; +; Original author: Jared Davis <jared@kookamara.com> +; +; instance.lisp +; +; This is a system for dynamically instantiating ACL2 "theories" (which are +; represented as constants) to create new, concrete "theories". + +(in-package "INSTANCE") + + +; Everything in this file is in program mode. We do not intend to +; reason about these functions -- instead, we intend to use these +; functions to create new functions, which the user will reason +; about. + +(program) + + +; Introduction +; +; +; The following work has been motivated by my work with quantification +; over sets. When I started on this file, I had roughly 2000 lines of +; complicted macros in order to be able to instantiate generic and +; concrete theories for this work, and it was just becoming +; unmanageable. My hope was that rewriting the definitions and +; theorems into concrete forms would provide a more concise way of +; instantiating the theory, and make it easier to keep everything +; consistent. +; +; Originally, I wanted to extract the definitions for generic +; functions from ACL2's state (well, actually from the current world). +; But, to do so becomes very complicated, because of the restrictions +; on macros that they cannot take state as a parameter. So, the best +; that I could ever accomplish that way would be to display a list of +; events, which a user could copy into a file. But, that is wholly +; unsatisfying, because it would mean that the resulting theories +; could never be "automagically" updated when new theorems are added +; to the generic theory. +; +; So, instead of doing things that way, I now simply store events in +; constants. These constants can then be rewritten to create new but +; related theories. +; +; A first step towards this is to introduce a simple rewriter. +; Originally I had based my rewriter on the built in one-way-unify +; function in ACL2, but it operates only on pseudo-terms, and +; pseudo-terms cannot contain atoms other than symbols. This gave me +; serious trouble when trying to rewrite theorems involving constants, +; e.g., to say that something was an integerp and greater than zero. +; So, instead of using one-way-unify, I introduce a simple unification +; algorithm which has been adapted from Warren Hunt's work. + +; The system treats all symbols beginning with a ? as variables, and +; all other atoms as literals. + +(defun instance-variablep (x) + (and (symbolp x) + (equal (car (explode-atom x 10)) #\?))) + + + +; We return two values: a boolean flag which indicates if we are +; successful in finding a match, and a list of substitutions of the +; form (variable . value). This is all be fairly standard stuff. +; +; For example: +; +; (instance-unify-term '(predicate ?x) '(predicate (car a)) nil) +; ==> +; (t ((?x . (car a)))) + +(mutual-recursion + + (defun instance-unify-term (pattern term sublist) + (if (atom pattern) + (if (instance-variablep pattern) + (let ((value (assoc pattern sublist))) + (if (consp value) + (if (equal term (cdr value)) + (mv t sublist) + (mv nil nil)) + (mv t (acons pattern term sublist)))) + (if (equal term pattern) + (mv t sublist) + (mv nil nil))) + (if (or (atom term) + (not (eq (car term) (car pattern)))) + (mv nil nil) + (if (or (eq (car term) 'quote) + (eq (car pattern) 'quote)) + (if (equal term pattern) + (mv t sublist) + (mv nil nil)) + (instance-unify-list (cdr pattern) (cdr term) sublist))))) + + (defun instance-unify-list (pattern-list term-list sublist) + (if (or (atom term-list) + (atom pattern-list)) + (if (and (atom term-list) + (atom pattern-list)) + (mv t sublist) + (mv nil nil)) + (mv-let (successp new-sublist) + (instance-unify-term (car pattern-list) + (car term-list) + sublist) + (if successp + (instance-unify-list (cdr pattern-list) + (cdr term-list) + new-sublist) + (mv nil nil))))) +) + + +; After a list of substitutions has been generated, we typically want +; to apply them to a term. We recur over the list of substitutions, +; simply calling subst to do our work throughout a term. +; +; For example: +; +; (instance-substitute '((?x . (car a))) '(not (predicate ?x))) +; ==> +; (not (predicate (car a))) + +(defun instance-substitute (sublist term) + (if (endp sublist) + term + (let* ((old (car (car sublist))) + (new (cdr (car sublist))) + (result (subst new old term))) + (instance-substitute (cdr sublist) result)))) + + + +; We now introduce our actual rewriter. We take three arguments: pat +; is the pattern to look for throughout the term, e.g., (predicate +; ?x), repl is the replacement to use, e.g., (not (predicate ?x)), and +; term is the term to match the pattern against in order to get the +; substitutions. +; +; For Example: +; +; (instance-rewrite1 '(predicate ?x) +; '(not (predicate ?x)) +; '(if (predicate (car x)) t nil)) +; => +; (if (not (predicate (car x))) t nil) + +(mutual-recursion + + (defun instance-rewrite1 (pat repl term) + (mv-let (successful sublist) + (instance-unify-term pat term nil) + (if successful + (instance-substitute sublist repl) + (if (atom term) + term + (cons (instance-rewrite1 pat repl (car term)) + (instance-rewrite-lst1 pat repl (cdr term))))))) + + (defun instance-rewrite-lst1 (pat repl lst) + (if (endp lst) + nil + (cons (instance-rewrite1 pat repl (car lst)) + (instance-rewrite-lst1 pat repl (cdr lst))))) +) + + + +; Finally, given that we can apply a rewrite a term with a single +; replacement, we go ahead and extend this notion to multiple +; replacements. In other words, we walk through a list of +; substitutions, sequentially rewriting the term using each +; substitution. + +(defun instance-rewrite (term subs) + (if (endp subs) + term + (let ((first-sub (car subs))) + (instance-rewrite (instance-rewrite1 (first first-sub) + (second first-sub) + term) + (cdr subs))))) + + + + +; Instantiating Defuns +; +; +; Theories consist mainly of definitions and theorems. Given generic +; theorems, we will want to rewrite them so that they perform +; different functions. For example, a generic "all" function might +; need to be rewritten so that its calls to (predicate x) are replaced +; with calls to (not (predicate x)) for all x. +; +; To begin, we instantiate the function's declarations (e.g., comment +; strings, xargs, ignores, and so forth). We simply duplicate comment +; strings, but for declare forms we allow rewriting to occur. + +(defun instance-decls (decls subs) + (if (endp decls) + nil + (if (pseudo-termp (car decls)) + (cons (instance-rewrite (car decls) subs) + (instance-decls (cdr decls) subs)) + (cons (car decls) + (instance-decls (cdr decls) subs))))) + + +; For the defun itself, we retain the same defun symbol (e.g., defun +; or defund), but we change the name and args of the function by first +; creating the list '(oldname oldarg1 oldarg2 ...) then applying our +; substitutions to the new function. +; +; As a trivial example, +; (instance-defun '(defun f (x) (+ x 1)) '(((f x) (g x)))) +; => +; (defun g (x) (+ x 1)) + +(defun instance-defun (defun subs) + (let* ((defun-symbol (first defun)) + (defun-name (second defun)) + (defun-args (third defun)) + (defun-decls (butlast (cdddr defun) 1)) + (defun-body (car (last defun))) + (name/args (cons defun-name defun-args)) + (new-body (instance-rewrite defun-body subs)) + (new-name/args (instance-rewrite name/args subs)) + (new-decls (instance-decls defun-decls subs)) + (new-name (car new-name/args)) + (new-args (cdr new-name/args))) + `(,defun-symbol + ,new-name ,new-args + ,@new-decls + ,new-body))) + +; We also provide a convenience function that allows you to instance +; a list of defuns. + +(defun instance-defuns (defun-list subs) + (if (endp defun-list) + nil + (cons (instance-defun (car defun-list) subs) + (instance-defuns (cdr defun-list) subs)))) + + + +; Renaming theorems + +(defun defthm-names (event-list) + (if (endp event-list) + nil + (let* ((first-event (car event-list)) + (event-type (first first-event))) + (cond ((or (eq event-type 'defthm) + (eq event-type 'defthmd)) + (cons (second first-event) + (defthm-names (cdr event-list)))) + ((eq event-type 'encapsulate) + (append (defthm-names (cddr first-event)) + (defthm-names (cdr event-list)))) + (t (defthm-names (cdr event-list))))))) + +(defun create-new-names (name-list suffix) + (if (endp name-list) + nil + (acons (car name-list) + (intern-in-package-of-symbol (string-append (symbol-name (car name-list)) + (symbol-name suffix)) + suffix) + (create-new-names (cdr name-list) suffix)))) + +(defun rename-defthms (event-list suffix) + (sublis (create-new-names (defthm-names event-list) suffix) + event-list)) + + + +; Instantiating Theorems +; +; +; To instantiate defthms, we will want to be able to provide +; functional instantiations of the generic theory. This is much +; more complicated than instancing definitions, and involves: +; +; a) determining what functional substitutions to make +; b) determining the theory in which to conduct the proofs +; c) handling rule classes and other optional components +; d) generating the actual defthm event +; +; My idea is essentially that if a substitution list can be used for +; functionally instantiating theorems, then it can also be used for +; creating the new theorem. +; +; (a) Determining what functional substitutions to make. +; +; I pass in a list of substitutions of the following form. +; +; (((predicate ?x) (not (in ?x y))) +; ((all ?x) (all-not-in ?x y)) +; ((exists ?x) (exists-not-in ?x y))) +; +; From this list we can generate the functional instantiation hints. +; So, for example, we simply convert ((predicate ?x) (not (in ?x y))) +; into the substitution: +; +; (predicate (lambda (?x) (not (in ?x y)))) +; +; This is easy to do with the following functions: + +(defun sub-to-lambda (sub) + (let ((term (first sub)) + (repl (second sub))) + (let ((function-symbol (car term)) + (lambda-args (cdr term))) + `(,function-symbol (lambda ,lambda-args ,repl))))) + +(defun subs-to-lambdas (subs) + (if (endp subs) + nil + (cons (sub-to-lambda (car subs)) + (subs-to-lambdas (cdr subs))))) + + +; (b) Determining the theory in which to conduct the proofs. +; +; When we prove the functional instantiation constraints, ideally we +; should work in an environment where the only definitions that are +; enabled are the definitions used in the functional instantiation +; hints. +; +; Well, the definitions we need are (almost) simply all of the +; function symbols in the right-hand side of the substitution list. +; In other words, for the above substitutions, I would want to have +; the definitions of not, in, all-not-in, and exists-not-in available. +; +; Now, the problem with this approach is, what if those symbols don't +; have definitions? This can occur if, for example, we are using a +; constrained function in the substitution list. This is actually +; useful, e.g., for substituting (predicate ?x) -> (not (predicate +; ?x)). +; +; My solution is a stupid hack. We simply pass in the names of the +; generic functions for which we do not want to generate definitions +; along with the substitutinos. +; +; To begin, the following function will extract all function symbols +; that occur within a term. + +(mutual-recursion + + (defun term-functions (term) + (if (atom term) + nil + (cons (car term) + (term-list-functions (cdr term))))) + + (defun term-list-functions (list) + (if (endp list) + nil + (append (term-functions (car list)) + (term-list-functions (cdr list))))) +) + +; Next, I wrote the following function, which walks over the +; substitution list and extracts the function symbols from each right +; hand side, using term-functions. The net result is the list of all +; functions that were used in replacements. + +(defun subs-repl-functions (subs) + (if (endp subs) + nil + (let* ((sub1 (car subs)) + (repl (second sub1))) + (append (term-functions repl) + (subs-repl-functions (cdr subs)))))) + +; Given the above, we could then convert the list of function symbols +; into a list of (:definition f)'s with the following function. + +(defun function-list-to-definitions (funcs) + (if (endp funcs) + nil + (cons `(:definition ,(car funcs)) + (function-list-to-definitions (cdr funcs))))) + +; And finally, here is a function that does "all of the work", calling +; function-list-to-definitions for all of the functions found in the +; substitution list, minus all of the generic functions that we don't +; want to generate :definition hints for. + +(defun subs-to-defs (subs generics) + (let* ((all-fns (subs-repl-functions subs)) + (real-fns (set-difference-eq all-fns generics))) + (function-list-to-definitions real-fns))) + + +; (c) Handling rule classes and other optional components. +; +; We are interested in several parts of a defthm. In addition to the +; conjecture itself, we need to consider the rule-classes used by the +; theorem, and the other optional attributes such as the :hints, :doc, +; :otf-flg, etc. We parse these attributes into a five-tuple of pairs +; of the form (present . value), where present is a boolean that says +; whether or not the flag has been seen, value is its value, and the +; order of the elements is rule-classes, instructions, hints, otf-flg, +; and finally doc. We parse these options with the following code: + +(defconst *default-parse-values* + '((nil . nil) (nil . nil) (nil . nil) (nil . nil) (nil . nil))) + +(defun parse-defthm-option (option return-value) + (cond ((equal (first option) :rule-classes) + (update-nth 0 (list t (second option)) return-value)) + ((equal (first option) :instructions) + (update-nth 1 (list t (second option)) return-value)) + ((equal (first option) :hints) + (update-nth 2 (list t (second option)) return-value)) + ((equal (first option) :otf-flg) + (update-nth 3 (list t (second option)) return-value)) + ((equal (first option) :doc) + (update-nth 4 (list t (second option)) return-value)) + (t (er hard "Unknown flag in defthm options ~x0." (first option))))) + +(defun parse-defthm-options (options return-value) + (if (endp options) + return-value + (parse-defthm-options (cddr options) + (parse-defthm-option options return-value)))) + + +; (d) Generating the actual defthm event. +; +; When we are ready to instance a defthm event, we combine the above +; work with a few new things. First of all, we need the original +; theorem event, a new name to use, the substitutions to use, and the +; list of generic function symbols in use so that we do not create +; (:definition f) entries for them. +; +; We begin by making our substitutions in the body of the theorem. We +; then parse the optional components of the defthm, but we only are +; interested in the rule-classes. (Hints, instructions, and otf-flg +; will not be needed, because we will be proving this via functional +; instantiation. Doc we ignore for no good reason.) We construct a +; new theorem that has our new name and body, replicating the rule +; classes if necessary. We also provide a functional instantiation +; hint of the generic theorem's name, along with a list of lambda +; substitutions to make. + +(defun instance-defthm (event new-name subs generics extra-defs) + (let* ((defthm-symbol (first event)) + (defthm-name (second event)) + (defthm-body (third event)) + (new-body (instance-rewrite defthm-body subs)) + (options (parse-defthm-options (cdddr event) + *default-parse-values*)) + (rc-opt (first options))) + `(,defthm-symbol ,new-name + ,new-body + :hints(("Goal" + :use (:functional-instance ,defthm-name + ,@(subs-to-lambdas subs)) + :in-theory (union-theories (theory 'minimal-theory) + (union-theories ',extra-defs + ',(subs-to-defs subs generics))))) + ,@(if (car rc-opt) `(:rule-classes ,(cdr rc-opt)) nil)))) + + + +; Instantiating Encapsulates +; +; +; There are two reasons that I typically use encapsulation. The first +; is as a purely structural/organizational purpose, where I am trying +; to prove some theorem is true, but I need some lemmas to do so. In +; this case I use an (encapsulate nil ...) and wrap my lemmas in local +; forms. The other reason is to actually go ahead and introduce +; constrained functions. +; +; Two strategies will be necessary for handling these situations. In +; particular, if we are in an encapsulate which has no constrained +; function symbols, we will want to skip all local events and only add +; the non-local events (using functional instantiation to create the +; theorems). On the other hand, for the case when we are introducing +; constrained functions, we will want to introduce new constrained +; functions based on the encapsulate. +; +; So, encapsulates are handled separately based on whether or not any +; functions are constrained. +; +; Within an (encapsulate nil ...), local events will be skipped and +; defthm events will be proven using the functional instantiation of +; their generic counterparts. +; +; Within an (encapsulate (...) ...), local events will not be skipped +; but will instead be reintroduced with new names. Further, defthm +; events will be copied using new names and will not be proven using +; functional instantiation. +; +; The only "extra" thing we really need for handling encapsulates is a +; system to make the substitutions within the signatures. We do that +; here by simple rewriting. Note that we do not allow the number of +; return values to change. I don't really think of this as a major +; limitation, since almost always my constrained functions return a +; single value. If you have an example of where this would be useful, +; it would be interesting to see it. + +(defun instance-signature (signature subs) + (let ((name (first signature)) + (rest (rest signature))) + (cons (instance-rewrite subs name) rest))) + +(defun instance-signatures (signatures subs) + (if (endp signatures) + nil + (cons (instance-signature (car signatures) subs) + (instance-signatures (cdr signatures) subs)))) + +; Because encapsulates can contain many events within them, it is +; natural to make them mutually recursive with the main event list +; handler, which we are now ready to introduce. + + + + + +; Instantiating Entire Theories +; +; +; We are now ready to introduce the functions which will walk through +; a theory and call the appropriate instancing functions on each of +; the forms we encounter. To support encapsulation, our functions +; here are all mutually recursive. +; +; The arguments that we pass around are the following: +; +; - The event or event list to instantiate +; +; - The global list of substitutions used to derive the instance +; +; - A suffix which will be appended to generate new names +; +; - A list of generic functions which have no definitions +; +; - A mode, which is either 'constrained to indicate that the +; nearest encapsulate event has constrained functions, or is nil +; to indicate that the nearest encapsulate is merely a structural +; wrapper for local lemmas. +; +; Finally, we overload our behavior based on suffix, so that if no +; suffix is given, we simply replicate the generic theory instead +; of instantiating a concrete instance of it. + + +(mutual-recursion + + (defun instance-event (event subs suffix generics mode extra-defs) + (if (null suffix) + event + (cond ((or (eq (car event) 'defun) + (eq (car event) 'defund)) + (instance-defun event subs)) + ((or (eq (car event) 'defthm) + (eq (car event) 'defthmd)) + (let* ((name (second event)) + (new-name (intern-in-package-of-symbol + (string-upcase + (concatenate 'string + (symbol-name name) + (symbol-name suffix))) + suffix))) + (instance-defthm event new-name subs generics extra-defs))) + ((equal (car event) 'local) + (if (eq mode 'constrained) + (instance-event (second event) subs suffix generics mode extra-defs) + nil)) + ((equal (car event) 'encapsulate) + (instance-encapsulate event subs suffix generics mode extra-defs)) + (t (er hard "Don't know how to handle ~x0" (car event)))))) + + (defun instance-event-list (events subs suffix generics mode extra-defs) + (if (endp events) + nil + (let ((first (instance-event (car events) subs suffix generics mode extra-defs)) + (rest (instance-event-list (cdr events) subs suffix generics mode extra-defs))) + (if first + (cons first rest) + rest)))) + + (defun instance-encapsulate (event subs suffix generics mode extra-defs) + (declare (ignore mode)) + (let* ((signatures (second event)) + (new-sigs (if signatures + (instance-signatures subs signatures) + nil)) + (new-events (instance-event-list (cddr event) subs suffix generics + (if signatures + 'constrained + nil) + extra-defs))) + `(encapsulate ,new-sigs ,@new-events))) + +) + + +; To be able to actually introduce the events, we need to emit a macro that +; can be used to actually perform substitutions. + +(defmacro instance (theory) + (let ((macro-name (intern-in-package-of-symbol + (string-upcase (concatenate 'string + "instance-" (string theory))) + theory))) + `(defmacro ,macro-name (&key subs suffix generics extra-defs) + (list* 'encapsulate + nil + (instance-event-list ,theory subs suffix generics nil extra-defs))))) + + + + +; Some thoughts +; +; A fundamental issue seems to be that a function and its arguments +; are not always used in a consistent manner. For example, say we +; want to rewrite (all ?x) to (all-foo ?x y) and we want to rewrite +; (predicate ?x) to (not (foo ?x y)). How can we accurately say just +; what it is that we want to rewrite in each case? +; +; Right now our substitutions are based on +; ( (predicate ?x) (not (foo ?x y)) ) +; ( (all ?x) (all-foo ?x y) ) +; +; We can easily pick out and say "all" is replaced by "all-foo", +; but if we try to just use the car of the term as its symbol +; replacement, then "predicate" would be "not". +; +; OK, so we could do some kind of preprocessing step where we fill +; in argument guards. The "generics" list right now is a big huge +; hack that allows us to ignore the fact that :predicate doens't +; have a definition. Really the issue that this is trying to solve +; is to tell us how to build our :in-theory event. Right now the +; :in-theory event is just a hack that we don't really understand. |