g-logops

(in-package "GL")

(include-book "g-if")

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

(include-book "symbolic-arithmetic")

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

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

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

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

(local (include-book "arithmetic/top-with-meta" :dir :system))

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

(defconst *binary-logop-template*
  '(encapsulate nil
    (defund g-binary-<logop>-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 (bfr-<logop>-ss xbits ybits))))
    (local (in-theory (enable g-binary-<logop>-of-integers)))
    (defthm deps-of-g-binary-<logop>-of-integers
      (implies (and (not (gobj-depends-on k p x))
          (not (gobj-depends-on k p y))
          (general-integerp x)
          (general-integerp y))
        (not (gobj-depends-on k
            p
            (g-binary-<logop>-of-integers x y)))))
    (local (defthm g-binary-<logop>-of-integers-correct
        (implies (and (general-integerp x)
            (general-integerp y))
          (equal (eval-g-base (g-binary-<logop>-of-integers x y)
              env)
            (<logop> (eval-g-base x env)
              (eval-g-base y env))))
        :hints (("goal" :in-theory (e/d* ((:ruleset general-object-possibilities))
             (general-integerp))
           :do-not-induct t))))
    (local (in-theory (disable g-binary-<logop>-of-integers)))
    (def-g-binary-op <binary-logop>
      (b* ((i-num (if (general-integerp i)
             i
             0)) (j-num (if (general-integerp j)
              j
              0)))
        (gret (g-binary-<logop>-of-integers i-num j-num))))
    (verify-g-guards <binary-logop>
      :hints `(("Goal" :in-theory (e/d* (g-if-fn g-or-fn)
           (,GL::GFN general-concretep-def)))))
    (def-gobj-dependency-thm <binary-logop>
      :hints `(("goal" :induct ,GL::GCALL
         :expand (,GL::GCALL)
         :in-theory (disable (:d ,GL::GFN)))))
    (local (defthm <logop>-non-integers
        (and (implies (not (integerp i))
            (equal (<logop> i j) (<logop> 0 j)))
          (implies (not (integerp j))
            (equal (<logop> i j) (<logop> i 0))))))
    (with-output :off (prove)
      (def-g-correct-thm <binary-logop>
        eval-g-base
        :hints `(("Goal" :in-theory (e/d* (general-concretep-atom (:ruleset general-object-possibilities)
               not-general-integerp-not-integerp)
             ((:definition ,GL::GFN) general-concretep-def
               <binary-logop>
               bfr-list->s
               bfr-list->u
               equal-of-booleans-rewrite
               double-containment
               hons-assoc-equal
               default-car
               default-cdr
               (:rules-of-class :type-prescription :here)))
           :induct (,GL::GFN i j . ,GL::PARAMS)
           :do-not-induct t
           :expand ((,GL::GFN i j . ,GL::PARAMS))))))))

(defmacro def-g-binary-logop
  (logop)
  (template-subst *binary-logop-template*
    :atom-alist `((<logop> . ,GL::LOGOP) (<binary-logop> . ,(GL::INTERN$ (STR::CAT "BINARY-" (SYMBOL-NAME GL::LOGOP)) "ACL2")))
    :str-alist `(("<LOGOP>" . ,(SYMBOL-NAME GL::LOGOP)))
    :pkg-sym 'foo))

(def-g-binary-logop logand)

(def-g-binary-logop logior)

(def-g-binary-logop logeqv)

(def-g-binary-logop logxor)

(def-g-fn lognot
  `(let ((x i))
    (if (atom x)
      (gret (lognot (ifix x)))
      (pattern-match x
        ((g-ite test then else) (if (zp clk)
            (gret (g-apply 'lognot (gl-list x)))
            (g-if (gret test)
              (,GL::GFN then . ,GL::PARAMS)
              (,GL::GFN else . ,GL::PARAMS))))
        ((g-apply & &) (gret (g-apply 'lognot (gl-list x))))
        ((g-concrete obj) (gret (lognot (ifix obj))))
        ((g-var &) (gret (g-apply 'lognot (gl-list x))))
        ((g-boolean &) (gret -1))
        ((g-integer bits) (gret (mk-g-integer (bfr-lognot-s (list-fix bits)))))
        (& (gret -1))))))

(verify-g-guards lognot
  :hints `(("Goal" :in-theory (disable ,GL::GFN))))

(def-gobj-dependency-thm lognot
  :hints `(("goal" :induct ,GL::GCALL
     :expand (,GL::GCALL)
     :in-theory (disable (:d ,GL::GFN)))))

(local (progn (defthm lognot-non-acl2-numberp
      (implies (not (acl2-numberp n))
        (equal (lognot n) (lognot 0))))
    (defthm lognot-non-integer
      (implies (not (integerp n))
        (equal (lognot n) (lognot 0))))
    (local (include-book "arithmetic/top-with-meta" :dir :system))))

(def-g-correct-thm lognot
  eval-g-base
  :hints `(("Goal" :in-theory (e/d* (general-concrete-obj)
       ((:definition ,GL::GFN) (force) lognot))
     :induct (,GL::GFN i . ,GL::PARAMS)
     :expand ((,GL::GFN i . ,GL::PARAMS) (:with eval-g-base (eval-g-base i env))))))