g-integer-length

(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"))

(set-inhibit-warnings "theory")

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

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

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

(local (defthm non-integerp-integer-length
    (implies (not (integerp x))
      (equal (integer-length x) 0))
    :rule-classes ((:rewrite :backchain-limit-lst 1))))

(local (defthm eval-g-base-booleanp
    (implies (booleanp x)
      (equal (eval-g-base x env) x))
    :hints (("Goal" :in-theory (enable eval-g-base booleanp)))))

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

(local (defthm general-concrete-obj-integer
    (implies (integerp x)
      (equal (general-concrete-obj x) x))
    :hints (("Goal" :in-theory (enable general-concrete-obj)))))

(local (defthm eval-g-base-integer
    (implies (integerp x)
      (equal (eval-g-base x env) x))
    :hints (("Goal" :in-theory (enable eval-g-base)))))

(def-g-correct-thm integer-length
  eval-g-base
  :hints `(("Goal" :in-theory (e/d nil
       ((:definition ,GL::GFN) general-concretep-def
         eval-g-base-alt-def
         integer-length))
     :induct (,GL::GFN i . ,GL::PARAMS)
     :expand ((,GL::GFN i . ,GL::PARAMS))) (and stable-under-simplificationp
      '(:expand ((:with eval-g-base (eval-g-base i env)))))))