general-objects

(in-package "GL")

(include-book "gtypes")

(defun general-booleanp
  (x)
  (declare (xargs :guard t))
  (or (booleanp x)
    (and (consp x)
      (or (eq (tag x) :g-boolean)
        (and (eq (tag x) :g-concrete)
          (booleanp (g-concrete->obj x)))))))

(in-theory (disable (general-booleanp)))

(defund general-boolean-value
  (x)
  (declare (xargs :guard (general-booleanp x)))
  (if (atom x)
    x
    (cdr x)))

(defun general-concrete-atom
  (x)
  (declare (xargs :guard t))
  (if (atom x)
    t
    (and (eq (tag x) :g-concrete)
      (atom (g-concrete->obj x)))))

(defun general-concrete-atom-val
  (x)
  (declare (xargs :guard (general-concrete-atom x)))
  (if (atom x)
    x
    (g-concrete->obj x)))

(in-theory (disable (general-concrete-atom)
    (general-concrete-atom-val)))

(defn general-concretep
  (x)
  (if (gobject-hierarchy-lite x)
    t
    nil))

(defun general-concrete-obj
  (x)
  (declare (xargs :guard (general-concretep x)
      :verify-guards nil))
  (cond ((atom x) x)
    ((g-concrete-p x) (g-concrete->obj x))
    ((concrete-gobjectp x) x)
    (t (cons (general-concrete-obj (car x))
        (general-concrete-obj (cdr x))))))

(in-theory (disable (general-concrete-obj)))

(defn general-integerp
  (x)
  (declare (xargs :guard t))
  (or (integerp x)
    (and (consp x)
      (or (eq (tag x) :g-integer)
        (and (eq (tag x) :g-concrete)
          (integerp (g-concrete->obj x)))))))

(in-theory (disable (general-integerp)))

(defthm general-integerp-of-atomic-constants
  (implies (and (syntaxp (quotep x)) (atom x))
    (equal (general-integerp x) (integerp x))))

(defn general-integer-bits
  (x)
  (declare (xargs :guard (general-integerp x)))
  (if (atom x)
    (i2v x)
    (if (eq (tag x) :g-concrete)
      (i2v (g-concrete->obj x))
      (list-fix (g-integer->bits x)))))

(defun general-consp
  (x)
  (declare (xargs :guard t))
  (and (consp x)
    (if (eq (tag x) :g-concrete)
      (consp (g-concrete->obj x))
      (not (g-keyword-symbolp (tag x))))))

(in-theory (disable (general-consp)))

(defun general-consp-car
  (x)
  (declare (xargs :guard (general-consp x)))
  (if (eq (tag x) :g-concrete)
    (mk-g-concrete (car (g-concrete->obj x)))
    (car x)))

(defun general-consp-cdr
  (x)
  (declare (xargs :guard (general-consp x)))
  (if (eq (tag x) :g-concrete)
    (mk-g-concrete (cdr (g-concrete->obj x)))
    (cdr x)))

(in-theory (disable (general-consp-car)
    (general-consp-cdr)))

(defun bool-cond-itep
  (x)
  (declare (xargs :guard t))
  (and (consp x)
    (eq (tag x) :g-ite)
    (general-booleanp (g-ite->test x))))

(defun bool-cond-itep-cond
  (x)
  (declare (xargs :guard (bool-cond-itep x)))
  (general-boolean-value (g-ite->test x)))

(defun bool-cond-itep-truebr
  (x)
  (declare (xargs :guard (bool-cond-itep x)))
  (g-ite->then x))

(defun bool-cond-itep-falsebr
  (x)
  (declare (xargs :guard (bool-cond-itep x)))
  (g-ite->else x))

(local (defthm acl2-count-cdr-weak
    (<= (acl2-count (cdr x)) (acl2-count x))
    :rule-classes :linear))

(defthm bool-cond-itep-cond-measure
  (implies (bool-cond-itep x)
    (< (acl2-count (bool-cond-itep-cond x))
      (acl2-count x)))
  :hints (("Goal" :in-theory (enable bool-cond-itep
       bool-cond-itep-cond
       general-boolean-value
       general-booleanp)))
  :rule-classes :linear)

(in-theory (disable (bool-cond-itep)
    (bool-cond-itep-cond)
    (bool-cond-itep-truebr)
    (bool-cond-itep-falsebr)))

(defund general-number-fix
  (x)
  (declare (xargs :guard t))
  (if (atom x)
    (fix x)
    (case (tag x)
      (:g-boolean 0)
      (:g-integer x)
      (:g-concrete (mk-g-concrete (fix (g-concrete->obj x))))
      (t 0))))