common-meta

(defun zfix
  (x)
  (if (and (acl2-numberp x) (not (eql x 0)))
    x
    1))

(defun package-witness nil t)

(defun intern-name
  (lst)
  (declare (xargs :mode :program))
  (intern-in-package-of-symbol (coerce (packn1 lst) 'string)
    'package-witness))

(defun un-hide-* (x y) (* x y))

(defun un-hide-+ (x y) (+ x y))

(defun collect-* (x y) (* x y))

(defun collect-+ (x y) (+ x y))

(defun addend-pattern
  (addend)
  (cond ((variablep addend) addend)
    ((fquotep addend) (if (equal addend ''0)
        nil
        (unquote addend)))
    ((eq (ffn-symb addend) 'unary--) (addend-pattern (arg1 addend)))
    ((and (eq (ffn-symb addend) 'binary-*)
       (acl2-nump (arg1 addend))) (addend-pattern (arg2 addend)))
    (t addend)))

(defun factor-pattern-gather-exponents
  (factor)
  (cond ((variablep factor) factor)
    ((fquotep factor) (let ((c (unquote factor)))
        (cond ((eql c 0) 0)
          ((rationalp c) (if (< (abs c) 1)
              (/ c)
              c))
          (t c))))
    ((eq (ffn-symb factor) 'unary-/) (factor-pattern-gather-exponents (arg1 factor)))
    ((eq (ffn-symb factor) 'expt) (let ((base (arg1 factor)) (exponent (arg2 factor)))
        (cond ((quotep base) (let ((c (unquote base)))
              (cond ((eql c 0) nil)
                ((rationalp c) (if (< (abs c) 1)
                    (list :mark1 (/ c) exponent)
                    (list :mark1 c exponent)))
                (t (list :mark1 c exponent)))))
          ((member-eq (fn-symb base) '(unary-- unary-/)) (factor-pattern-gather-exponents (arg1 base)))
          (t base))))
    (t factor)))

(defun factor-pattern-exponent2
  (addend weight)
  (let ((weight (zfix weight)))
    (if (and (eq (fn-symb addend) 'binary-*) (quotep (arg1 addend)))
      (if (eql (unquote (arg1 addend)) weight)
        (arg2 addend)
        `(binary-* ,(KWOTE (/ (ZFIX (UNQUOTE (ARG1 ADDEND))) WEIGHT))
          ,(ARG2 ADDEND)))
      `(binary-* ,(KWOTE (/ WEIGHT)) ,ADDEND))))

(defun factor-pattern-exponent1
  (exponent weight)
  (if (eq (fn-symb exponent) 'binary-+)
    `(binary-+ ,(FACTOR-PATTERN-EXPONENT2 (ARG1 EXPONENT) WEIGHT)
      ,(FACTOR-PATTERN-EXPONENT1 (ARG2 EXPONENT) WEIGHT))
    (factor-pattern-exponent2 exponent weight)))

(defun factor-pattern-exponent
  (exponent)
  (cond ((or (variablep exponent) (fquotep exponent)) (mv 1 exponent))
    ((eq (ffn-symb exponent) 'binary-*) (if (quotep (arg1 exponent))
        (mv (arg1 exponent) (arg2 exponent))
        (mv 1 exponent)))
    ((eq (ffn-symb exponent) 'binary-+) (if (and (eq (fn-symb (arg1 exponent)) 'binary-*)
          (acl2-nump (arg1 (arg1 exponent))))
        (let ((weight (unquote (arg1 (arg1 exponent)))))
          (mv weight (factor-pattern-exponent1 exponent weight)))
        (mv 1 exponent)))
    (t (mv 1 exponent))))

(defun factor-pattern-scatter-exponents
  (factor)
  (cond ((variablep factor) factor)
    ((fquotep factor) (let ((c (unquote factor)))
        (cond ((eql c 0) 0)
          ((rationalp c) (if (< (abs c) 1)
              (/ c)
              c))
          (t c))))
    ((eq (ffn-symb factor) 'unary-/) (factor-pattern-scatter-exponents (arg1 factor)))
    ((eq (ffn-symb factor) 'expt) (let ((base (cond ((quotep (arg1 factor)) (unquote factor))
             ((member-eq (fn-symb (arg1 factor)) '(unary-- unary-/)) (arg1 (arg1 factor)))
             (t (arg1 factor)))) (exponent (arg2 factor)))
        (if (acl2-numberp base)
          (cond ((variablep exponent) `(:mark2 ,BASE 1 ,EXPONENT))
            ((fquotep exponent) `(:mark2 ,BASE 1 ,EXPONENT))
            ((eq (ffn-symb exponent) 'binary-*) (if (quotep (arg1 exponent))
                `(:mark2 ,BASE ,(UNQUOTE (ARG1 EXPONENT)) ,(ARG2 EXPONENT))
                `(:mark2 ,BASE 1 ,(ARG2 EXPONENT))))
            ((eq (ffn-symb exponent) 'binary-+) (mv-let (weight new-exponent)
                (factor-pattern-exponent exponent)
                `(:mark2 ,BASE ,WEIGHT ,NEW-EXPONENT)))
            (t `(:mark2 ,BASE 1 ,EXPONENT)))
          (cond ((variablep exponent) `(expt ,BASE ,EXPONENT))
            ((fquotep exponent) base)
            ((eq (ffn-symb exponent) 'binary-*) (if (quotep (arg1 exponent))
                `(expt ,BASE ,(ARG2 EXPONENT))
                factor))
            ((eq (ffn-symb exponent) 'binary-+) (mv-let (weight new-exponent)
                (factor-pattern-exponent exponent)
                (declare (ignore weight))
                `(expt ,BASE ,NEW-EXPONENT)))
            (t `(expt ,BASE ,EXPONENT))))))
    (t factor)))

(defun pattern-matchp
  (x y)
  (cond ((or (eq x nil) (eq y nil)) nil)
    ((or (eq x t) (eq y t)) t)
    ((or (eql x 0) (eql y 0)) (not (and (eql x 0) (eql y 0))))
    ((acl2-numberp x) (or (acl2-numberp y)
        (and (consp y) (eq (car y) :mark1) (equal (cadr y) x))))
    ((and (consp x) (eq (car x) :mark1)) (or (equal y (cadr x))
        (and (consp y)
          (eq (car y) :mark)
          (or (equal (cadr y) (cadr x)) (equal (caddr y) (caddr x))))))
    ((and (consp x) (eq (car x) :mark2)) (and (consp y)
        (eq (car y) :mark2)
        (equal (cadr x) (cadr y))
        (equal (cadddr x) (cadddr y))))
    (t (equal x y))))

(defun assoc-pattern-matchp
  (key alist)
  (cond ((endp alist) nil)
    ((pattern-matchp key (caar alist)) (car alist))
    (t (assoc-pattern-matchp key (cdr alist)))))

(defun fix-val
  (x)
  (let ((temp (rfix (unquote x))))
    (if (eql temp 0)
      0
      (/ temp))))

(defun addend-val
  (addend)
  (cond ((variablep addend) 1)
    ((fquotep addend) (fix-val addend))
    ((eq (ffn-symb addend) 'unary--) -1)
    ((and (eq (ffn-symb addend) 'binary-*)
       (quotep (arg1 addend))) (fix-val (arg1 addend)))
    (t 1)))

(defun factor-val1
  (exponent)
  (cond ((variablep exponent) 1)
    ((fquotep exponent) (fix-val exponent))
    ((eq (ffn-symb exponent) 'binary-*) (if (quotep (arg1 exponent))
        (fix-val (arg1 exponent))
        1))
    ((eq (ffn-symb exponent) 'binary-+) (+ (factor-val1 (arg1 exponent))
        (factor-val1 (arg2 exponent))))
    (t 1)))

(defun factor-val
  (factor)
  (cond ((variablep factor) 1)
    ((fquotep factor) (if (or (equal factor ''0) (equal factor ''1))
        0
        1))
    ((eq (ffn-symb factor) 'unary-/) -1)
    ((eq (ffn-symb factor) 'expt) (factor-val1 (arg2 factor)))
    (t 1)))

(defun use-firstp
  (val1 val2 bin-op)
  (declare (ignore bin-op))
  (cond ((eql (abs val1) (abs val2)) (< val1 0))
    (t (< (abs val2) (abs val1)))))

(defun my-apply-1
  (fun arg)
  (case fun
    (addend-pattern (addend-pattern arg))
    (factor-pattern-gather-exponents (factor-pattern-gather-exponents arg))
    (factor-pattern-scatter-exponents (factor-pattern-scatter-exponents arg))
    (addend-val (addend-val arg))
    (factor-val (factor-val arg))))

(defun pull-piece-out
  (term pattern pattern-fun bin-op)
  (cond ((or (variablep term) (fquotep term)) (mv nil nil term))
    ((pattern-matchp (my-apply-1 pattern-fun (arg1 term))
       pattern) (mv t (arg1 term) (arg2 term)))
    ((eq (fn-symb (arg2 term)) bin-op) (mv-let (flag piece rest)
        (pull-piece-out (arg2 term) pattern pattern-fun bin-op)
        (if flag
          (mv t piece `(,BIN-OP ,(ARG1 TERM) ,REST))
          (mv nil nil term))))
    ((pattern-matchp (my-apply-1 pattern-fun (arg2 term))
       pattern) (mv t (arg2 term) (arg1 term)))
    (t (mv nil nil term))))

(defun new-term1
  (term new-piece pattern pattern-fun bin-op)
  (if (member-eq bin-op '(binary-+ binary-*))
    (cond ((eq (fn-symb term) bin-op) (mv-let (flag piece rest)
          (pull-piece-out term pattern pattern-fun bin-op)
          (if flag
            (case bin-op
              ((binary-+) (mv t
                  `(un-hide-+ (collect-+ (hide ,NEW-PIECE) (hide ,PIECE))
                    (hide ,REST))))
              ((binary-*) (mv t
                  `(un-hide-* (collect-* (hide ,NEW-PIECE) (hide ,PIECE))
                    (hide ,REST))))
              (otherwise (mv t `(,BIN-OP ,NEW-PIECE ,TERM))))
            (mv nil `(,BIN-OP ,NEW-PIECE ,TERM)))))
      ((pattern-matchp (my-apply-1 pattern-fun term) pattern) (if (eq bin-op 'binary-+)
          (mv t `(collect-+ (hide ,NEW-PIECE) (hide ,TERM)))
          (mv t `(collect-* (hide ,NEW-PIECE) (hide ,TERM)))))
      (t (mv nil `(,BIN-OP ,NEW-PIECE ,TERM))))
    (mv nil `(,BIN-OP ,NEW-PIECE ,TERM))))

(defun new-term
  (term new-piece pattern pattern-fun bin-op)
  (if (and (eq bin-op 'binary-*) (eq (fn-symb term) 'binary-+))
    (mv-let (flag1 new-term1)
      (new-term1 (arg1 term) new-piece pattern pattern-fun bin-op)
      (mv-let (flag2 new-term2)
        (new-term (arg2 term) new-piece pattern pattern-fun bin-op)
        (mv (or flag1 flag2) `(binary-+ ,NEW-TERM1 ,NEW-TERM2))))
    (new-term1 term new-piece pattern pattern-fun bin-op)))