collect-terms-meta

Included Books

other

(in-package "ACL2")

include-book

(include-book "common-meta")

local

(local (include-book "../pass1/top"))

local

(local (in-theory (disable my-apply-1)))

local

(local (defthm hide-revealed
    (equal (hide x) x)
    :hints (("Goal" :expand (hide x)))))

make-collecting-metamacro

(defmacro make-collecting-meta
  (name pattern-fun bin-op)
  (let ((fn-name (intern-name (list name "-FN"))) (thm-name (intern-name (list name "-THM"))))
    `(progn (defun ,FN-NAME
        (term)
        (if (and (nvariablep term)
            (not (fquotep term))
            (eq (ffn-symb term) ,BIN-OP))
          (let ((pattern (my-apply-1 ,PATTERN-FUN (arg1 term))))
            (mv-let (flag new-term)
              (new-term (arg2 term)
                (arg1 term)
                pattern
                ,PATTERN-FUN
                ,BIN-OP)
              (if flag
                new-term
                term)))
          term))
      (defthm ,THM-NAME
        (equal (eva term a) (eva (,FN-NAME term) a))
        :rule-classes ((:meta :trigger-fns (,(UNQUOTE BIN-OP)))))
      (local (in-theory (disable ,THM-NAME))))))

other

(make-collecting-meta collect-addends
  'addend-pattern
  'binary-+)

other

(make-collecting-meta collect-factors-gather-exponents
  'factor-pattern-gather-exponents
  'binary-*)

other

(make-collecting-meta collect-factors-scatter-exponents
  'factor-pattern-scatter-exponents
  'binary-*)