g-logapp

(in-package "GL")

(include-book "g-if")

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

(include-book "symbolic-arithmetic")

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

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

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

(local (include-book "centaur/bitops/ihsext-basics" :dir :system))

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

(defun g-logapp-of-integers
  (n x y)
  (declare (xargs :guard (and (general-integerp n)
        (general-integerp x)
        (general-integerp y))))
  (b* ((nbits (general-integer-bits n)) (negp (bfr-sign-s nbits)))
    (mk-g-integer (bfr-ite-bss-fn negp
        (general-integer-bits y)
        (bfr-logapp-russ (rev nbits)
          (general-integer-bits x)
          (general-integer-bits y))))))

(in-theory (disable (g-logapp-of-integers)))

(local (defthm depends-on-of-append
    (implies (and (not (pbfr-list-depends-on k p x))
        (not (pbfr-list-depends-on k p y)))
      (not (pbfr-list-depends-on k p (append x y))))
    :hints (("Goal" :in-theory (enable pbfr-list-depends-on)))))

(local (defthm depends-on-of-rev
    (implies (not (pbfr-list-depends-on k p x))
      (not (pbfr-list-depends-on k p (rev x))))
    :hints (("Goal" :in-theory (enable rev pbfr-list-depends-on)))))

(defthm deps-of-g-logapp-of-integers
  (implies (and (not (gobj-depends-on k p n))
      (not (gobj-depends-on k p x))
      (not (gobj-depends-on k p y))
      (general-integerp n)
      (general-integerp x)
      (general-integerp y))
    (not (gobj-depends-on k
        p
        (g-logapp-of-integers n x y)))))

(local (defthm logapp-zp-n
    (implies (zp n)
      (equal (logapp n x y) (ifix y)))
    :hints (("Goal" :in-theory (enable logapp**)))
    :rule-classes ((:rewrite :backchain-limit-lst 0))))

(local (defthm logapp-zip-x
    (implies (and (syntaxp (not (equal x ''0))) (zip x))
      (equal (logapp n x y)
        (logapp n 0 y)))
    :hints (("Goal" :in-theory (enable logapp**)))
    :rule-classes ((:rewrite :backchain-limit-lst 0))))

(local (defthm logapp-zip-y
    (implies (and (syntaxp (not (equal y ''0))) (zip y))
      (equal (logapp n x y)
        (logapp n x 0)))
    :hints (("Goal" :in-theory (enable logapp**)))
    :rule-classes ((:rewrite :backchain-limit-lst 0))))

(local (defthm bfr-list->s-when-gte-0
    (implies (<= 0 (bfr-list->s x env))
      (equal (bfr-list->s x env)
        (bfr-list->u x env)))
    :hints (("Goal" :in-theory (enable scdr s-endp)))))

(defthm g-logapp-of-integers-correct
  (implies (and (general-integerp n)
      (general-integerp x)
      (general-integerp y))
    (equal (eval-g-base (g-logapp-of-integers n x y)
        env)
      (logapp (eval-g-base n env)
        (eval-g-base x env)
        (eval-g-base y env))))
  :hints (("goal" :in-theory (e/d* ((:ruleset general-object-possibilities))
       (general-integerp bfr-list->s))
     :do-not-induct t)))

(in-theory (disable g-logapp-of-integers))

(def-g-fn logapp
  `(let ((size size))
    (b* (((when (and (general-concretep size)
            (general-concretep i)
            (general-concretep j))) (gret (ec-call (logapp (general-concrete-obj size)
               (general-concrete-obj i)
               (general-concrete-obj j))))) ((when (mbe :logic (eq (tag size) :g-ite)
             :exec (and (consp size) (eq (tag size) :g-ite)))) (let* ((test (g-ite->test size)) (then (g-ite->then size))
              (else (g-ite->else size)))
            (g-if (gret test)
              (,GL::GFN then i j . ,GL::PARAMS)
              (,GL::GFN else i j . ,GL::PARAMS))))
        ((when (mbe :logic (eq (tag i) :g-ite)
             :exec (and (consp i) (eq (tag i) :g-ite)))) (if (zp clk)
            (gret (g-apply 'logapp (gl-list size i j)))
            (let* ((test (g-ite->test i)) (then (g-ite->then i))
                (else (g-ite->else i)))
              (g-if (gret test)
                (,GL::GFN size then j . ,GL::PARAMS)
                (,GL::GFN size else j . ,GL::PARAMS)))))
        ((when (mbe :logic (eq (tag j) :g-ite)
             :exec (and (consp j) (eq (tag j) :g-ite)))) (if (zp clk)
            (gret (g-apply 'logapp (gl-list size i j)))
            (let* ((test (g-ite->test j)) (then (g-ite->then j))
                (else (g-ite->else j)))
              (g-if (gret test)
                (,GL::GFN size i then . ,GL::PARAMS)
                (,GL::GFN size i else . ,GL::PARAMS)))))
        ((unless (mbe :logic (not (member-eq (tag size) '(:g-var :g-apply)))
             :exec (or (atom size)
               (not (member-eq (tag size) '(:g-var :g-apply)))))) (gret (g-apply 'logapp (gl-list size i j))))
        ((unless (mbe :logic (not (member-eq (tag i) '(:g-var :g-apply)))
             :exec (or (atom i)
               (not (member-eq (tag i) '(:g-var :g-apply)))))) (gret (g-apply 'logapp (gl-list size i j))))
        ((unless (mbe :logic (not (member-eq (tag j) '(:g-var :g-apply)))
             :exec (or (atom j)
               (not (member-eq (tag j) '(:g-var :g-apply)))))) (gret (g-apply 'logapp (gl-list size i j))))
        (size (if (general-integerp size)
            size
            0))
        (i (if (general-integerp i)
            i
            0))
        (j (if (general-integerp j)
            j
            0)))
      (gret (g-logapp-of-integers size i j)))))

(verify-g-guards logapp
  :hints `(("Goal" :in-theory (disable* ,GL::GFN general-concretep-def))))

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

(local (defthm logapp-non-integers
    (and (implies (not (integerp size))
        (equal (logapp size i j) (ifix j)))
      (implies (not (integerp i))
        (equal (logapp size i j)
          (logapp size 0 j)))
      (implies (not (integerp j))
        (equal (logapp size i j)
          (logapp size i 0))))))

(def-g-correct-thm logapp
  eval-g-base
  :hints `(("goal" :in-theory (e/d* (eval-g-base-list))
     :induct ,GL::GCALL
     :expand (,GL::GCALL)
     :do-not-induct t)))