pack - ACL2 Book

Included Books

nat-to-string coerce explode-nonnegative-integer explode-atom append character-listp

other

(in-package "ACL2")

include-book

(include-book "nat-to-string")

local

(local (include-book "coerce"))

local

(local (include-book "explode-nonnegative-integer"))

local

(local (include-book "explode-atom"))

local

(local (include-book "kestrel/lists-light/append" :dir :system))

local

(local (include-book "kestrel/typed-lists-light/character-listp" :dir :system))

to-stringfunction

(defund to-string
  (item)
  (declare (type t item))
  (if (symbolp item)
    (symbol-name item)
    (if (natp item)
      (nat-to-string item)
      (if (stringp item)
        item
        (if (characterp item)
          (coerce (list item) 'string)
          (prog2$ (hard-error 'to-string
              "Found ~x0, which is not a symbol, string, character, or natural number.~%"
              (acons #\0 item nil))
            ""))))))

to-string-when-stringptheorem

(defthm to-string-when-stringp
  (implies (stringp x) (equal (to-string x) x))
  :hints (("Goal" :in-theory (enable to-string))))

equal-of-to-string-and-to-string-when-natpstheorem

(defthm equal-of-to-string-and-to-string-when-natps
  (implies (and (natp item1) (natp item2))
    (equal (equal (to-string item1) (to-string item2))
      (equal item1 item2)))
  :hints (("Goal" :in-theory (enable to-string))))

binary-packfunction

(defund binary-pack
  (x y)
  (declare (xargs :guard t))
  (concatenate 'string (to-string x) (to-string y)))

equal-of-binary-pack-and-binary-pack-same-arg1theorem

(defthm equal-of-binary-pack-and-binary-pack-same-arg1
  (equal (equal (binary-pack x y1) (binary-pack x y2))
    (equal (to-string y1) (to-string y2)))
  :hints (("Goal" :in-theory (e/d (binary-pack) (to-string)))))

pack$-fnfunction

(defun pack$-fn
  (lst)
  (declare (xargs :guard (true-listp lst)))
  (if (not lst)
    (prog2$ (hard-error 'pack$-fn "pack needs at least 1 argument" nil)
      "")
    (if (not (cdr lst))
      `(to-string ,(CAR LST))
      (xxxjoin 'binary-pack lst))))

pack$macro

(defmacro pack$
  (&rest rst)
  `(intern ,(PACK$-FN RST) "ACL2"))

pack-in-package-of-symbolmacro

(defmacro pack-in-package-of-symbol
  (sym &rest rst)
  `(intern-in-package-of-symbol ,(PACK$-FN RST) ,SYM))

pack-in-package-of-first-symbolmacro

(defmacro pack-in-package-of-first-symbol
  (sym &rest rst)
  `(pack-in-package-of-symbol ,SYM ,SYM ,@RST))

packtostringmacro

(defmacro packtostring (&rest rst) (pack$-fn rst))

to-string-form-for-itemfunction

(defun to-string-form-for-item
  (item)
  (declare (xargs :guard t))
  (if (and (quotep item) (consp (cdr item)))
    (to-string (unquote item))
    (if (atom item)
      (if (not (legal-variablep item))
        (to-string item)
        `(to-string ,ITEM))
      `(to-string ,ITEM))))

to-string-forms-for-itemsfunction

(defun to-string-forms-for-items
  (items)
  (declare (xargs :guard (true-listp items)))
  (if (endp items)
    nil
    (let ((first-form (to-string-form-for-item (first items))) (rest-forms (to-string-forms-for-items (rest items))))
      (if (and (stringp first-form)
          (consp rest-forms)
          (stringp (first rest-forms)))
        (cons (concatenate 'string first-form (first rest-forms))
          (rest rest-forms))
        (cons first-form rest-forms)))))

pack-in-package-fnfunction

(defund pack-in-package-fn
  (package items)
  (declare (xargs :guard (and (true-listp items))))
  (let ((forms (to-string-forms-for-items items)))
    (if (endp forms)
      (er hard? 'pack-in-package-fn "Nothing to concatenate.")
      (if (endp (rest forms))
        `(intern$ ,(FIRST FORMS) ,PACKAGE)
        `(intern$ (concatenate 'string ,@FORMS) ,PACKAGE)))))

pack-in-packagemacro

(defmacro pack-in-package
  (package &rest items)
  (pack-in-package-fn package items))