gobject-types

(in-package "GL")

(include-book "defagg")

(include-book "tools/pattern-match" :dir :system)

(include-book "misc/untranslate-patterns" :dir :system)

(include-book "centaur/misc/numlist" :dir :system)

(defagg g-concrete (obj))

(defagg g-boolean (bool))

(defagg g-integer (bits))

(defagg g-ite (test then else))

(defagg g-apply (fn args) :notinline t)

(defagg g-var (name))

(defsection g-int
  :parents (shape-specs)
  :short "Create a g-binding for an integer."
  :long "<p>This is a low-level way to create a custom shape specifier for a
signed integer.  You might generally prefer higher-level tools like @(see
auto-bindings).</p>"
  (defun g-int
    (start by n)
    (declare (xargs :guard (and (acl2-numberp start)
          (acl2-numberp by)
          (natp n))))
    (g-integer (numlist start by n))))

(defconst *g-keywords*
  '(:g-boolean :g-integer :g-concrete :g-ite :g-apply :g-var))

(defun g-keyword-symbolp
  (x)
  (declare (xargs :guard t))
  (and (symbolp x)
    (mbe :logic (if (member x *g-keywords*)
        t
        nil)
      :exec (or (eq x :g-boolean)
        (eq x :g-integer)
        (eq x :g-concrete)
        (eq x :g-ite)
        (eq x :g-apply)
        (eq x :g-var)))))

(in-theory (disable g-keyword-symbolp))

(defthmd g-keyword-symbolp-def
  (equal (g-keyword-symbolp x)
    (if (member-equal x *g-keywords*)
      t
      nil))
  :hints (("Goal" :in-theory (enable g-keyword-symbolp))))

(defthm not-g-keyword-symbol-when-not-symbol
  (implies (not (symbolp x))
    (not (g-keyword-symbolp x)))
  :hints (("Goal" :in-theory (enable g-keyword-symbolp)))
  :rule-classes ((:rewrite :backchain-limit-lst 0) :type-prescription))

(defun gl-cons
  (x y)
  (declare (xargs :guard t))
  (cons (if (g-keyword-symbolp x)
      (g-concrete x)
      x)
    y))