g-cons

(in-package "GL")

(include-book "g-if")

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

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

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

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

(def-g-fn cdr
  `(if (atom x)
    (gret nil)
    (pattern-match x
      ((g-ite test then else) (if (zp clk)
          (gret (g-apply 'cdr (gl-list x)))
          (g-if (gret test)
            (,GL::GFN then . ,GL::PARAMS)
            (,GL::GFN else . ,GL::PARAMS))))
      ((g-boolean &) (gret nil))
      ((g-integer &) (gret nil))
      ((g-apply & &) (gret (g-apply 'cdr (gl-list x))))
      ((g-var &) (gret (g-apply 'cdr (gl-list x))))
      ((g-concrete obj) (gret (mk-g-concrete (ec-call (cdr obj)))))
      ((cons & b) (gret b))
      (& (gret nil)))))

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

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

(def-g-correct-thm cdr
  eval-g-base
  :hints `(("goal" :in-theory (e/d (eval-g-base general-concrete-obj)
       ((:definition ,GL::GFN) logcons
         bfr-list->s
         bfr-list->u
         eval-g-base-alt-def
         equal-of-booleans-rewrite
         default-car
         double-containment))
     :induct (,GL::GFN x . ,GL::PARAMS)
     :expand ((,GL::GFN x . ,GL::PARAMS)))))

(def-g-fn car
  `(if (atom x)
    (gret nil)
    (pattern-match x
      ((g-ite test then else) (if (zp clk)
          (gret (g-apply 'car (gl-list x)))
          (g-if (gret test)
            (,GL::GFN then . ,GL::PARAMS)
            (,GL::GFN else . ,GL::PARAMS))))
      ((g-boolean &) (gret nil))
      ((g-integer &) (gret nil))
      ((g-apply & &) (gret (g-apply 'car (gl-list x))))
      ((g-var &) (gret (g-apply 'car (gl-list x))))
      ((g-concrete obj) (gret (mk-g-concrete (ec-call (car obj)))))
      ((cons a &) (gret a))
      (& (gret nil)))))

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

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

(def-g-correct-thm car
  eval-g-base
  :hints `(("goal" :in-theory (e/d (eval-g-base general-concrete-obj)
       ((:definition ,GL::GFN) eval-g-base-alt-def logcons))
     :induct (,GL::GFN x . ,GL::PARAMS)
     :expand ((,GL::GFN x . ,GL::PARAMS)))))

(def-g-fn cons `(gret (gl-cons x y)))

(verify-g-guards cons)

(def-gobj-dependency-thm cons
  :hints `(("Goal" :in-theory (enable ,GL::GFN))))

(def-g-correct-thm cons
  eval-g-base
  :hints `(("Goal" :in-theory (enable ,GL::GFN))))