g-binary-+

(in-package "GL")

(include-book "g-if")

(include-book "g-primitives-help")

(include-book "symbolic-arithmetic")

(include-book "eval-g-base")

(include-book "centaur/misc/starlogic" :dir :system)

(include-book "tools/templates" :dir :system)

(local (include-book "eval-g-base-help"))

(local (include-book "hyp-fix"))

(local (include-book "clause-processors/just-expand" :dir :system))

(local (defcong number-equiv equal (+ a b) 1))

(local (defcong number-equiv equal (+ a b) 2))

(local (defcong number-equiv equal (- x) 1))

(defconst *plusminus-template*
  '(progn (defun g-<fn>-of-integers
      (x y)
      (declare (xargs :guard (and (general-integerp x)
            (general-integerp y))))
      (b* ((xbits (general-integer-bits x)) (ybits (general-integer-bits y)))
        (mk-g-integer <sum-expr>)))
    (in-theory (disable (g-<fn>-of-integers)))
    (local (defthm g-<fn>-of-integers-correct
        (implies (and (general-integerp x)
            (general-integerp y))
          (equal (eval-g-base (g-<fn>-of-integers x y)
              env)
            (<fn> (eval-g-base x env)
              (eval-g-base y env))))
        :hints (("goal" :in-theory (e/d* ((:ruleset general-object-possibilities))
             (general-integerp general-integer-bits))
           :do-not-induct t))))
    (local (defthm dependencies-of-g-<fn>-of-integers
        (implies (and (general-integerp x)
            (general-integerp y)
            (not (gobj-depends-on n p x))
            (not (gobj-depends-on n p y)))
          (not (gobj-depends-on n
              p
              (g-<fn>-of-integers x y))))
        :hints (("goal" :do-not-induct t))
        :otf-flg t))
    (in-theory (disable g-<fn>-of-integers))
    (def-g-binary-op <fn>
      (b* ((x (general-number-fix x)) (y (general-number-fix y))
          ((when (and** (general-integerp x)
               (general-integerp y))) (gret (g-<fn>-of-integers x y)))
          ((when (and** (general-concretep x)
               (eql (general-concrete-obj x) 0))) (gret <returnval-for-x-0>))
          ((when (and** (general-concretep y)
               (eql (general-concrete-obj y) 0))) (gret x)))
        (gret (g-apply '<fn> (list x y)))))
    (verify-g-guards <fn>
      :hints `(("goal" :in-theory (disable* ,GL::GFN
           (:rules-of-class :type-prescription :here)))))
    (def-gobj-dependency-thm <fn>
      :hints `(("goal" :in-theory (disable (:d ,GL::GFN) gobj-depends-on)
         :induct ,GL::GCALL
         :expand (,GL::GCALL))))
    (def-g-correct-thm <fn>
      eval-g-base
      :hints `(("goal" :in-theory (enable* eval-g-base-list)
         :induct ,GL::GCALL
         :do-not-induct t
         :expand (,GL::GCALL))))))

(defmacro def-g-plusminus
  (fn &key return-when-x-is-0 sum-expr)
  (template-subst *plusminus-template*
    :atom-alist `((<fn> . ,GL::FN) (<returnval-for-x-0> . ,GL::RETURN-WHEN-X-IS-0)
      (<sum-expr> . ,GL::SUM-EXPR))
    :str-alist `(("<FN>" . ,(SYMBOL-NAME GL::FN)))
    :pkg-sym 'foo))

(def-g-plusminus binary-+
  :return-when-x-is-0 y
  :sum-expr (bfr-+-ss nil xbits ybits))

(def-g-plusminus binary-minus-for-gl
  :return-when-x-is-0 (if (general-concretep y)
    (mk-g-concrete (- (general-concrete-obj y)))
    (mk-g-integer (bfr-unary-minus-s (general-integer-bits y))))
  :sum-expr (bfr-+-ss t xbits (bfr-lognot-s ybits)))