untranslate-patterns

(in-package "ACL2")

(defxdoc untranslate-patterns
  :parents (macros user-defined-functions-table)
  :short "A database used to extend @('untranslate'), ACL2's function for
displaying terms during proofs, with pattern-based rules."
  :long "<p>The @('untranslate-patterns-table') is an ACL2 @(see 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.</p>

<p>Although this table has nothing to do with soundness, the rules it lists are
intended to obey the untranslate contract&mdash;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 @(see member) as if they were calls to @(see subsetp)
would make proof output very difficult to understand.</p>

<p>We do nothing to enforce this contract.  Hence, a sensible user must ensure
that their use of this table is disciplined.</p>


<h3>Example 1: Mutually Recursive even/odd-p</h3>

<p>This function is just an inefficient check for if a natural number is even
or odd, using a flag-based mutual recursion scheme.</p>

@({
    (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)))))
})

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

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

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

<p>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:</p>

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

<p>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').</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))))
})

<p>Some of the proof output generated is now as follows:</p>

@({
    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)))).
})

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


<h3>Example 2: Matt's Challenge</h3>

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

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

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

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

<p>The theorem Matt proposed looking at was the following:</p>

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

<p>With no support for untranslate, this theorem ends up producing the
following goal:</p>

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

<p>The RTL untranslator can handle this given the following command:</p>

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

<p>This yields the following, nice goal:</p>

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

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

@({
    (add-untranslate-pattern (foo$ ?n $path) (foo ?n))
})

<p>As you can see, it produces exactly the same output:</p>

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


<h3>The Pattern Matching Syntax</h3>

<p>The syntax for these patterns is as follows:</p>

<p>Any quoted constant matches with a quoted constant.  Note that numbers and
so forth must be MANUALLY quoted.</p>

<p>Unquoted symbols behave as follows:</p>

<ul>

<li>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.</li>

<li>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.</li>

</ul>

<p>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.</p>

<p>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.</p>")

(table untranslate-patterns-table 'functions-database nil)

(table untranslate-patterns-table 'constants-database nil)

(defsection add-untranslate-pattern
  :parents (untranslate-patterns)
  :short "Add a new pattern to the untranslate patterns table."
  :long "<p>General Form:</p>

@({
    (add-untranslate-pattern target replacement)
})

<p>Examples:</p>

@({
    (add-untranslate-pattern '(1 2 3) *myconst*)
    (add-untranslate-pattern (f$ ?a ?b mystobj) (f ?a ?b))
})

<p>We add a new pattern to the untranslate patterns table.  The target should
be either a quoted constant (which must be fully expanded, it does not get
evaluated), or an unquoted function call.</p>

<p>The first example above changes proof output so that the constant '(1 2 3)
is instead printed as *myconst*.  The second example changes proof output so
that for all @('x,y'), @('(f$ x y mystobj)') is printed as @('(f x y)').  Note
that the printing of @('(f$ x y yourstobj)') will not be altered.</p>"
  (defmacro add-untranslate-pattern
    (target replacement)
    (if (and (consp target) (eq (car target) 'quote))
      `(add-untranslate-pattern-constant ,(CADR TARGET)
        ,REPLACEMENT)
      `(add-untranslate-pattern-function ,TARGET ,REPLACEMENT))))

(defsection optimize-untranslate-patterns
  :parents (untranslate-patterns)
  :short "Optimize the untranslate patterns table."
  :long "<p>Usage:</p>
@({
    (optimize-untranslate-patterns)
})

<p>This macro improves the efficiency of the untranslate-patterns-table by
rebalancing the btree used to internally store patterns for functions and by
cleaning up the alist used to store patterns for constants.  You only need to
call it after adding lots of untranslate patterns, and only if you want to
ensure that untranslation is being done as efficiently as possible.</p>"
  (defmacro optimize-untranslate-patterns
    nil
    `(progn (table untranslate-patterns-table
        'functions-database
        (rebalance-symbol-btree (untranslate-patterns-functions-btree world)))
      (table untranslate-patterns-table
        'constants-database
        (clean-up-alist (untranslate-patterns-constants-alist world)
          nil)))))

(table user-defined-functions-table
  'untranslate-preprocess
  'untranslate-pattern-preprocessor)