; Simple, Pattern-Based Untranslation for ACL2 ; Copyright (C) 2005 by Jared Davis ; ; 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. (in-package "ACL2") (include-book "symbol-btree") ; Simple, Pattern-Based Untranslation ; ; This is an untranslate preprocessor [1] that allows you to add custom, ; pattern-driven untranslation rules very easily. Patterns and replacements ; are stored as rules in a database [2], and this database can be extended ; using the add-untranslate-pattern [3] function. The database itself is ; stored as a symbol-btree [4], so you may occasionally want to rebalance it ; [5]. ; ; [1] :doc user-defined-functions-table, in ACL2 2.9.2 or above ; [2] :doc untranslate-patterns-database, after loading this file ; [3] :doc add-untranslate-pattern, after loading this file ; [4] see acl2-sources/books/misc/symbol-btree.lisp ; [5] :doc optimize-untranslate-patterns, after loading this file (defdoc untranslate-patterns-table ":Doc-Section Events a database used to extend untranslate with pattern-based rules~/ This database provides a simplistic way to extend the untranslate function with pattern-based rules, so that whenever some term would occur in a proof output, you will instead see some other term.~/ Although this table has nothing to do with soundness, the rules it lists are intended to obey the untranslate contract -- that is, the replacements listed for each pattern should macro-expand to their targets. If this property is violated, proof output might become very confusing! For example, a rule that displays calls to ~ilc[member] as if they were calls to ~ilc[subsetp] would be disasterous for your ability to understand proofs. We do nothing to enforce this contract, so any sensible user must ensure that their use of this table is disciplined. EXAMPLE 1: MUTUALLY RECURSIVE EVEN/ODD-P This function is just an inefficient check for if a natural number is even or odd, using a flag-based mutual recursion scheme. ~bv[] (defun even/odd-p (flg x) (declare (xargs :guard (and (or (eq flg 'even) (eq flg 'odd)) (natp x)))) (if (eq flg 'even) (if (zp x) t (even/odd-p 'odd (1- x))) (if (zp x) nil (even/odd-p 'even (1- x))))) ~ev[] Something simple you might want to do with this is 'hide' the flag function with macros such as the following: ~bv[] (defmacro even-p (x) `(even/odd-p 'even ,x)) (defmacro odd-p (x) `(even/odd-p 'odd ,x)) ~ev[] But of course in proofs you will still see the flag functions. My patch allows you to call a new macro, ~c[add-untranslate-pattern]. For this example, you would want to add the following patterns: ~bv[] (add-untranslate-pattern (even/odd-p 'even ?x) (even-p ?x)) (add-untranslate-pattern (even/odd-p 'odd ?x) (odd-p ?x)) ~ev[] After adding these patterns, let's submit the following trivially true theorem to ACL2 and see what happens. We will disable the type prescription of ~c[even/odd-p] and its definition, so that ACL2 will generate a lot of terms involving ~c[even/odd-p]. ~bv[] (in-theory (disable (:definition even/odd-p) (:type-prescription even/odd-p))) (thm (equal (+ (even-p x) (even-p y)) (+ (odd-p y) (odd-p x)))) ~ev[] This gives us many nice subgoals to show off our untranslation in. Here are a couple of examples: ~bv[] Subgoal *1/2 (IMPLIES (AND (NOT (EQ 'ODD 'EVEN)) (NOT (ZP X)) (EQUAL (+ (EVEN-P (+ -1 X)) (EVEN-P Y)) (+ (ODD-P (+ -1 X)) (ODD-P Y)))) (EQUAL (+ (EVEN-P X) (EVEN-P Y)) (+ (ODD-P X) (ODD-P Y)))). Subgoal *1/2' (IMPLIES (AND (NOT (ZP X)) (EQUAL (+ (EVEN-P (+ -1 X)) (EVEN-P Y)) (+ (ODD-P (+ -1 X)) (ODD-P Y)))) (EQUAL (+ (EVEN-P X) (EVEN-P Y)) (+ (ODD-P X) (ODD-P Y)))). ~ev[] So as you can see, ~c[even/odd-p] is now nicely untranslated into these macro calls, as we intended. EXAMPLE 2: MATT'S CHALLENGE Matt Kaufmann gave me the following challenge problem, which a custom untranslate function written for the RTL library can handle relatively easily. The untranslate-table approach can also handle it very easily. Here is the common code that both share: ~bv[] (defun foo$ (n $path) (cons n $path)) (defmacro foo (x) `(foo$ ,x $path)) (add-macro-alias foo foo$) (in-theory (disable foo)) ~ev[] The theorem Matt proposed looking at was the following: ~bv[] (thm (equal (list (foo x) (foo$ x $path) (foo$ x other-path)) (car (cons a b)))) ~ev[] With no support for untranslate, this theorem ends up producing the following goal: ~bv[] Goal' (EQUAL (LIST (FOO$ X $PATH) (FOO$ X $PATH) (FOO$ X OTHER-PATH)) A). ~ev[] And, with the custom untranslate function, the following command was needed: ~bv[] (table rtl-tbl 'sigs-btree (symbol-alist-to-btree (dollar-alist '(foo) nil))) ~ev[] Which yielded the following alternate goal: (which is nice) ~bv[] Goal' (EQUAL (LIST (FOO X) (FOO X) (FOO$ X OTHER-PATH)) A). ~ev[] Matt challenged me to come up with a system that would rewrite only $path. Using the untranslate pattern table, here is the command: ~bv[] (add-untranslate-pattern (foo$ ?n $path) (foo ?n)) ~ev[] As you can see, it produces exactly the same output: ~bv[] Goal' (EQUAL (LIST (FOO X) (FOO X) (FOO$ X OTHER-PATH)) A). ~ev[] THE PATTERN MATCHING SYNTAX The syntax for these patterns is as follows: Any quoted constant matches with a quoted constant. Note that numbers and so forth must be MANUALLY quoted. Unquoted symbols behave as follows: ~bq[] If the symbol has no leading ~c[?] character, then the symbol matches only with variables of exactly the same name. For example, if you were using a stobj named $path, you could use the symbol $path in your pattern and it would match only with $path. Symbols beginning with a leading ~c[?] character are treated as match variables. For example, ~c[?x] in the above patterns behaves as a wildcard and will match with any term. ~eq[] So, for example, the pattern ~c[(even/odd-p 'even ?x)] above matches exactly those terms whose function symbol is ~c[even/odd-p], whose first argument is the quoted constant symbol even, and whose second argument is any term. Similarly, the pattern ~c[(foo$ ?n $path)] matches exactly those terms whose function symbol is ~c[foo$], whose first argument is any term, and whose second argument is exactly the variable $path.") (table untranslate-patterns-table 'patterns-database nil) (defun untranslate-patterns-btree (wrld) "Retrieve the untranslate patterns btree." (declare (xargs :guard (and (worldp wrld) (alistp (table-alist 'untranslate-patterns-table wrld))))) (cdr (assoc-eq 'patterns-database (table-alist 'untranslate-patterns-table wrld)))) (defmacro add-untranslate-pattern (target replacement) ":Doc-Section Events add a new pattern to the untranslate patterns table~/ ~bv[] Example: (add-untranslate-pattern (f$ ?a ?b mystobj) (f a b)) ~ev[] This example adds a new pattern to the untranslate patterns table. As a result, whenever ~c[(f$ ?a ?b mystobj)] occurs as a term in proof attempts, it will instead be displayed as ~c[(f a b)].~/ ~l[untranslate-patterns-table] for more details. ~bv[] General Form: (add-untranslate-pattern target replacement) ~ev[]~/" `(table untranslate-patterns-table 'patterns-database (let* ((function ',(ffn-symb target)) (pat-database (untranslate-patterns-btree world)) (curr-subs (symbol-btree-lookup function pat-database)) (new-subs (acons ',target ',replacement curr-subs))) (symbol-btree-update function new-subs pat-database)))) (defmacro optimize-untranslate-patterns () ":Doc-Section Events optimize the untranslate patterns table~/ ~bv[] Usage: (optimize-untranslate-patterns) ~ev[] This macro rebalances the untranslate-patterns-table btree to optimize search. You only need to call it if you added a lot of untranslate patterns and want to make sure that untranslation is being done more efficiencly.~/ ~l[add-untranslate-pattern] for more details.~/" `(table untranslate-patterns-table 'patterns-database (rebalance-symbol-btree (untranslate-patterns-btree world)))) ; UNTRANSLATE EXTENSION ------------------------------------------------------- ; We begin by introducing a really simple rewriter. We define our variables as ; symbols which begin with question marks, e.g., ?x, ?y, etc. (defun jared-variablep (x) (declare (xargs :mode :program)) (and (symbolp x) (let ((name (symbol-name x))) (and (not (equal name "")) (equal (char name 0) #\?))))) ; We now introduce a simple one-way unification / matching function. 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). ; ; For example: ; ; (jared-unify-term '(predicate ?x) '(predicate (car a)) nil) ; ==> ; (t ((?x . (car a)))) (mutual-recursion (defun jared-unify-term (pattern term sublist) (declare (xargs :mode :program)) (if (atom pattern) (if (jared-variablep pattern) (let ((value (assoc-eq 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 (eq (car term) 'quote) ; hence also (eq (car pattern) 'quote) (if (equal term pattern) (mv t sublist) (mv nil nil)) (jared-unify-list (cdr pattern) (cdr term) sublist))))) (defun jared-unify-list (pattern-list term-list sublist) (declare (xargs :mode :program)) (if (or (atom term-list) (atom pattern-list)) (if (equal term-list pattern-list) ; same atom (mv t sublist) (mv nil nil)) (mv-let (successp new-sublist) (jared-unify-term (car pattern-list) (car term-list) sublist) (if successp (jared-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: ; ; (jared-substitute '((?x . (car a))) '(not (predicate ?x))) ; ==> ; (not (predicate (car a))) (defun jared-substitute (sublist term) (declare (xargs :mode :program)) (if (endp sublist) term (let* ((old (car (car sublist))) (new (cdr (car sublist))) (result (subst new old term))) (jared-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: ; ; (jared-rewrite1 '(predicate ?x) ; '(not (predicate ?x)) ; '(if (predicate (car x)) t nil)) ; => ; (if (not (predicate (car x))) t nil) (mutual-recursion (defun jared-rewrite1 (pat repl term) (declare (xargs :mode :program)) (mv-let (successful sublist) (jared-unify-term pat term nil) (if successful (jared-substitute sublist repl) (cond ((atom term) term) ((eq (car term) 'quote) term) (t (cons (jared-rewrite1 pat repl (car term)) (jared-rewrite-lst1 pat repl (cdr term)))))))) (defun jared-rewrite-lst1 (pat repl lst) (declare (xargs :mode :program)) (if (endp lst) nil (cons (jared-rewrite1 pat repl (car lst)) (jared-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 jared-rewrite (term subs) (declare (xargs :mode :program)) (if (endp subs) term (let* ((first-sub (car subs)) (newterm (jared-rewrite1 (car first-sub) (cdr first-sub) term))) (if (equal term newterm) (jared-rewrite term (cdr subs)) newterm)))) ; Now we define a really simple untranslate preprocessor that simply returns ; variables, constants, and lambdas in tact, but looks up function applications ; in the database and rewrites them if there is a matching rule. (defun untranslate-pattern-preprocessor (term world) (declare (xargs :mode :program)) (if (or (variablep term) (fquotep term) (flambda-applicationp term)) term (let ((subs (symbol-btree-lookup (ffn-symb term) (untranslate-patterns-btree world)))) (if subs (jared-rewrite term subs) term)))) ; And all that's left to do is install the new preprocessor! (table user-defined-functions-table 'untranslate-preprocess 'untranslate-pattern-preprocessor)