g-unary--

(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 "arithmetic/top-with-meta" :dir :system))

(set-inhibit-warnings "theory")

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

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

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

(def-g-correct-thm unary--
  eval-g-base
  :hints `(("Goal" :in-theory (e/d* (general-concrete-obj natp)
       ((:definition ,GL::GFN) general-integer-bits-correct))
     :induct (,GL::GFN x . ,GL::PARAMS)
     :do-not-induct t
     :expand ((,GL::GFN x . ,GL::PARAMS) (:with eval-g-base (eval-g-base x env))))))