		Search-engine friendly clone of the ACL2 documentation.

Untranslate-patterns

A database used to extend untranslate, ACL2's function for displaying terms during proofs, with pattern-based rules.

The untranslate-patterns-table is an ACL2 table that stores patterns and replacements for use at untranslate time. That is, during proof output, this table is consulted before printing terms, allowing for custom printing of particular terms.

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 member as if they were calls to subsetp would make proof output very difficult to understand.

We do nothing to enforce this contract. Hence, a 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.

(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)))))

Something simple you might want to do with this is 'hide' the flag function with macros such as the following:

(defmacro even-p (x)
  `(even/odd-p 'even ,x))

(defmacro odd-p (x)
  `(even/odd-p 'odd ,x))

But of course in proofs you will still see the flag functions. To hide these flags, you can call the macro add-untranslate-pattern as follows:

(add-untranslate-pattern (even/odd-p 'even ?x) (even-p ?x))
(add-untranslate-pattern (even/odd-p 'odd ?x)  (odd-p ?x))

The effect of these patterns can be seen by submitting the following commands. We first disable the type prescription of even/odd-p and its definition, so that ACL2 will generate terms involving even/odd-p.

(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))))

Some of the proof output generated is now as follows:

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)))).

As you can see, even/odd-p is now nicely untranslated into these macro calls, as we intended, and the flag argument is hidden.

Example 2: Matt's Challenge

Matt Kaufmann suggested the following challenge problem, inspired by the hand-written untranslation routine for the RTL library. We begin with the following code:

(defun foo$ (n $path)
  (cons n $path))

(defmacro foo (x)
  `(foo$ ,x $path))

(add-macro-alias foo foo$)
(in-theory (disable foo))

The theorem Matt proposed looking at was the following:

(thm (equal (list (foo x) (foo$ x $path) (foo$ x other-path))
            (car (cons a b))))

With no support for untranslate, this theorem ends up producing the following goal:

Goal'
(EQUAL (LIST (FOO$ X $PATH)
             (FOO$ X $PATH)
             (FOO$ X OTHER-PATH))
       A).

The RTL untranslator can handle this given the following command:

(table rtl-tbl 'sigs-btree
       (symbol-alist-to-btree
        (dollar-alist '(foo) nil)))

This yields the following, nice goal:

Goal'
(EQUAL (LIST (FOO X)
             (FOO X)
             (FOO$ X OTHER-PATH))
       A).

Matt challenged me to come up with a system that would rewrite only $path. Using the untranslate pattern table, here is the command:

(add-untranslate-pattern (foo$ ?n $path) (foo ?n))

As you can see, it produces exactly the same output:

Goal'
(EQUAL (LIST (FOO X)
             (FOO X)
             (FOO$ X OTHER-PATH))
       A).

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:

If the symbol has no leading ? 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 ? character are treated as match variables. For example, ?x in the above patterns behaves as a wildcard and will match with any term.

So, for example, the pattern (even/odd-p 'even ?x) above matches exactly those terms whose function symbol is even/odd-p, whose first argument is the quoted constant symbol even, and whose second argument is any term.

Similarly, the pattern (foo$ ?n $path) matches exactly those terms whose function symbol is foo$, whose first argument is any term, and whose second argument is exactly the variable $path.

Subtopics

Add-untranslate-pattern: Add a new pattern to the untranslate patterns table.
Optimize-untranslate-patterns: Optimize the untranslate patterns table.