other
(in-package "GL")
other
(include-book "centaur/gl/g-primitives-help" :dir :system)
other
(include-book "centaur/gl/eval-g-base" :dir :system)
other
(include-book "centaur/gl/g-if" :dir :system)
other
(local (include-book "centaur/gl/eval-g-base-help" :dir :system))
other
(def-g-fn make-fast-alist
`(let ((x alist))
(if (general-concretep x)
(gret (mk-g-concrete (make-fast-alist (general-concrete-obj x))))
(pattern-match x
((g-ite test then else) (if (zp clk)
(gret x)
(g-if (gret test)
(,GL::GFN then . ,GL::PARAMS)
(,GL::GFN else . ,GL::PARAMS))))
((g-apply & &) (gret x))
((g-var &) (gret x))
((g-boolean &) (gret x))
((g-number &) (gret x))
(& (gret (make-fast-alist x)))))))
other
(verify-g-guards make-fast-alist)
other
(def-gobj-dependency-thm make-fast-alist :hints `(("goal" :induct ,GL::GCALL :expand (,GL::GCALL) :in-theory (disable (:d ,GL::GFN)))))
other
(def-g-correct-thm make-fast-alist eval-g-base :hints `(("Goal" :induct (,GL::GFN alist . ,GL::PARAMS) :expand (,GL::GFN alist . ,GL::PARAMS) :in-theory (disable (:definition ,GL::GFN))) (and stable-under-simplificationp '(:expand ((:with eval-g-base (eval-g-base alist env)))))))