gtypes

(in-package "GL")

(include-book "generic-geval")

(defund gobject-hierarchy-lite
  (x)
  (declare (xargs :guard t))
  (if (atom x)
    'concrete
    (mbe :logic (cond ((g-concrete-p x) 'general)
        ((g-boolean-p x) nil)
        ((g-integer-p x) nil)
        ((g-ite-p x) nil)
        ((g-apply-p x) nil)
        ((g-var-p x) nil)
        (t (let ((car (gobject-hierarchy-lite (car x))))
            (and car
              (let ((cdr (gobject-hierarchy-lite (cdr x))))
                (and cdr
                  (if (or (eq car 'general) (eq cdr 'general))
                    'general
                    'concrete)))))))
      :exec (if (symbolp (tag x))
        (case (tag x)
          (:g-concrete 'general)
          (:g-boolean nil)
          (:g-integer nil)
          (:g-ite nil)
          (:g-apply nil)
          (:g-var nil)
          (otherwise (gobject-hierarchy-lite (cdr x))))
        (let ((car (gobject-hierarchy-lite (car x))))
          (and car
            (let ((cdr (gobject-hierarchy-lite (cdr x))))
              (and cdr
                (if (or (eq car 'general) (eq cdr 'general))
                  'general
                  'concrete)))))))))

(encapsulate nil
  (local (in-theory (enable gobject-hierarchy-lite)))
  (local (defthm crock
      (implies (and (gobject-hierarchy-lite x)
          (not (equal (gobject-hierarchy-lite x) 'general)))
        (equal (gobject-hierarchy-lite x) 'concrete))))
  (memoize 'gobject-hierarchy-lite
    :condition '(and (consp x)
      (not (g-keyword-symbolp (car x))))))

(defn concrete-gobjectp
  (x)
  (eq (gobject-hierarchy-lite x) 'concrete))

(in-theory (disable concrete-gobjectp))

(defn mk-g-concrete
  (x)
  (if (concrete-gobjectp x)
    x
    (g-concrete x)))

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

(defn g-concrete-quote
  (x)
  (if (and (atom x) (not (g-keyword-symbolp x)))
    x
    (g-concrete x)))

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

(defun mk-g-ite
  (c x y)
  (declare (xargs :guard t))
  (cond ((atom c) (if c
        x
        y))
    ((hqual x y) x)
    ((not (g-keyword-symbolp (tag c))) x)
    ((eq (tag c) :g-integer) x)
    ((eq (tag c) :g-concrete) (if (g-concrete->obj c)
        x
        y))
    (t (g-ite c x y))))

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

(defun mk-g-boolean
  (bdd)
  (declare (xargs :guard t))
  (if (booleanp bdd)
    bdd
    (g-boolean bdd)))

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

(define mk-g-integer
  (bits)
  (if (boolean-listp bits)
    (bfr-list->s bits nil)
    (g-integer bits)))

(defun gl-list-macro
  (lst)
  (if (atom lst)
    nil
    `(gl-cons ,(CAR GL::LST)
      ,(GL::GL-LIST-MACRO (CDR GL::LST)))))

(defmacro gl-list
  (&rest args)
  (gl-list-macro args))

(defsection gobj-listp
  (defund gobj-listp
    (x)
    (declare (xargs :guard t))
    (if (atom x)
      (eq x nil)
      (and (not (g-keyword-symbolp (car x)))
        (gobj-listp (cdr x)))))
  (local (in-theory (enable gobj-listp)))
  (defthm gobj-listp-of-gl-cons
    (implies (gobj-listp x)
      (gobj-listp (gl-cons k x)))
    :hints (("Goal" :in-theory (enable gl-cons tag)))))

(mutual-recursion (defun gobj-depends-on
    (k p x)
    (if (atom x)
      nil
      (pattern-match x
        ((g-boolean b) (pbfr-depends-on k p b))
        ((g-integer bits) (pbfr-list-depends-on k p bits))
        ((g-ite test then else) (or (gobj-depends-on k p test)
            (gobj-depends-on k p then)
            (gobj-depends-on k p else)))
        ((g-concrete &) nil)
        ((g-var &) nil)
        ((g-apply & args) (gobj-list-depends-on k p args))
        (& (or (gobj-depends-on k p (car x))
            (gobj-depends-on k p (cdr x)))))))
  (defun gobj-list-depends-on
    (k p x)
    (if (atom x)
      nil
      (or (gobj-depends-on k p (car x))
        (gobj-list-depends-on k p (cdr x))))))