g-unary-concrete

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

(in-theory (disable (mk-g-concrete)))

(defthm mk-g-concrete-of-atomic-constant
  (implies (and (syntaxp (quotep x))
      (atom x)
      (not (g-keyword-symbolp x)))
    (equal (mk-g-concrete x) x))
  :hints (("Goal" :in-theory (enable mk-g-concrete
       concrete-gobjectp
       gobject-hierarchy-lite))))

(program)

(defun def-g-unary-concrete-fn
  (fn integer-case
    boolean-case
    cons-case
    hints
    world)
  (let ((x (car (wgetprop fn 'formals))))
    `(progn (def-g-fn ,GL::FN
        (let ((x ',GL::X) (fn ',GL::FN))
          `(if (atom ,GL::X)
            (gret (mk-g-concrete (ec-call (,GL::FN ,GL::X))))
            (pattern-match ,GL::X
              ((g-concrete obj) (gret (mk-g-concrete (ec-call (,GL::FN obj)))))
              ((g-ite test then else) (if (zp clk)
                  (gret (g-apply ',GL::FN (gl-list ,GL::X)))
                  (g-if (gret test)
                    (,GL::GFN then . ,GL::PARAMS)
                    (,GL::GFN else . ,GL::PARAMS))))
              ((g-apply & &) (gret (g-apply ',GL::FN (gl-list ,GL::X))))
              ((g-var &) (gret (g-apply ',GL::FN (gl-list ,GL::X))))
              ((g-integer &) ,',GL::INTEGER-CASE)
              ((g-boolean &) ,',GL::BOOLEAN-CASE)
              (& ,',GL::CONS-CASE)))))
      (verify-g-guards ,GL::FN
        :hints `(("Goal" :in-theory (disable ,GL::GFN))))
      (def-gobj-dependency-thm ,GL::FN
        :hints `(("goal" :induct ,GL::GCALL
           :expand (,GL::GCALL)
           :in-theory (disable (:d ,GL::GFN)))))
      (def-g-correct-thm ,GL::FN
        eval-g-base
        :hints `(("Goal" :in-theory (e/d ((:induction ,GL::GFN) general-concrete-obj)
             ((:definition ,GL::GFN)))
           :induct (,GL::GFN ,',GL::X . ,GL::PARAMS)
           :expand ((,GL::GFN ,',GL::X . ,GL::PARAMS) (:with eval-g-base (eval-g-base ,',GL::X env)))) . ,',GL::HINTS)))))

(defmacro def-g-unary-concrete
  (fn &key
    integer-case
    boolean-case
    cons-case
    hints)
  `(make-event (def-g-unary-concrete-fn ',GL::FN
      ',GL::INTEGER-CASE
      ',GL::BOOLEAN-CASE
      ',GL::CONS-CASE
      ',GL::HINTS
      (w state))))

(logic)

(local (defthm pbfr-list-depends-on-of-cons
    (implies (and (not (pbfr-depends-on k p x1))
        (not (pbfr-list-depends-on k p x2)))
      (not (pbfr-list-depends-on k p (cons x1 x2))))
    :hints (("Goal" :in-theory (enable pbfr-list-depends-on)))))

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

(local (defthm bfr-list->s-of-cons
    (implies (consp x2)
      (equal (bfr-list->s (cons x1 x2) env)
        (logcons (bool->bit (bfr-eval x1 env))
          (bfr-list->s x2 env))))
    :hints (("Goal" :expand ((bfr-list->s (cons x1 x2) env))
       :in-theory (enable scdr s-endp)))))

(local (defthm bfr-list->s-of-singleton
    (equal (bfr-list->s (list x1) env)
      (bool->sign (bfr-eval x1 env)))
    :hints (("Goal" :expand ((bfr-list->s (cons x1 x2) env))
       :in-theory (enable scdr s-endp)))))

(def-g-unary-concrete bool->bit$inline
  :integer-case (gret 1)
  :boolean-case (gret (mk-g-integer (list (g-boolean->bool x) nil)))
  :cons-case (gret 1)
  :hints ((and stable-under-simplificationp
     '(:in-theory (enable bool->bit)))))

(def-g-unary-concrete bool->sign
  :integer-case (gret -1)
  :boolean-case (gret (mk-g-integer (list (g-boolean->bool x))))
  :cons-case (gret -1)
  :hints ((and stable-under-simplificationp
     '(:cases ((eval-g-base (g-ite->test x) env))))))

(def-g-unary-concrete symbol-name
  :integer-case (gret "")
  :boolean-case (g-if (gret x) (gret "T") (gret "NIL"))
  :cons-case (gret ""))

(def-g-unary-concrete symbol-package-name
  :integer-case (gret "")
  :boolean-case (gret "COMMON-LISP")
  :cons-case (gret "")
  :hints ((and stable-under-simplificationp
     '(:use ((:instance (:type-prescription bfr-eval)
          (x (g-boolean->bool x))
          (env (car env))))
       :in-theory (disable (:type-prescription bfr-eval))))))

(def-g-unary-concrete char-code
  :integer-case (gret 0)
  :boolean-case (gret 0)
  :cons-case (gret 0))

(def-g-unary-concrete code-char
  :integer-case (gret (g-apply 'code-char (list x)))
  :boolean-case (gret (code-char 0))
  :cons-case (gret (code-char 0))
  :hints ((and stable-under-simplificationp
     '(:in-theory (enable eval-g-base-list)))))

(local (defthm pkg-witness-of-non-stringp
    (implies (not (stringp x))
      (equal (pkg-witness x) (pkg-witness "ACL2")))
    :hints (("goal" :use ((:instance symbol-equality
          (s1 'acl2-pkg-witness)
          (s2 (pkg-witness x))))))))

(def-g-unary-concrete pkg-witness
  :integer-case (gret (mk-g-concrete (pkg-witness "ACL2")))
  :boolean-case (gret (mk-g-concrete (pkg-witness "ACL2")))
  :cons-case (gret (mk-g-concrete (pkg-witness "ACL2"))))

(def-g-unary-concrete realpart
  :integer-case (gret x)
  :boolean-case (gret 0)
  :cons-case (gret 0))

(def-g-unary-concrete imagpart
  :integer-case (gret 0)
  :boolean-case (gret 0)
  :cons-case (gret 0))