stringify

(in-package "STR")

(include-book "cat")

(include-book "decimal")

(defun stringify-integer
  (x)
  (declare (xargs :guard (integerp x)))
  (if (and (mbt (integerp x)) (< x 0))
    (cat "-" (nat-to-dec-string (- x)))
    (nat-to-dec-string x)))

(encapsulate nil
  (local (defthm nat-to-dec-chars-of-non-natp
      (implies (not (natp x))
        (equal (nat-to-dec-chars x) '(#\0)))
      :hints (("Goal" :in-theory (enable nat-to-dec-chars)))))
  (defthmd nat-to-dec-string-of-non-natp
    (implies (not (natp x))
      (equal (nat-to-dec-string x) "0"))
    :hints (("Goal" :in-theory (enable nat-to-dec-string)))))

(encapsulate nil
  (local (defthm not-member-minus-char-dec-digit-char-list*p
      (implies (dec-digit-char-list*p x)
        (not (member-equal #\- x)))))
  (local (defthm not-equal-cons-when-not-member-equal
      (implies (not (member-equal a b))
        (not (equal b (cons a c))))))
  (local (defthm switch-coerce-cons-string
      (implies (and (syntaxp (not (quotep b)))
          (characterp a)
          (character-listp b)
          (stringp c))
        (and (equal (equal (implode (cons a b)) c)
            (equal (cons a b) (explode c)))
          (equal (equal c (implode (cons a b)))
            (equal (cons a b) (explode c)))))))
  (defthm stringify-integer-one-to-one
    (equal (equal (stringify-integer x)
        (stringify-integer y))
      (equal (ifix x) (ifix y)))
    :hints (("goal" :use ((:instance not-member-minus-char-dec-digit-char-list*p
          (x (coerce (nat-to-dec-string x) 'list))) (:instance not-member-minus-char-dec-digit-char-list*p
           (x (coerce (nat-to-dec-string y) 'list)))
         (:instance nat-to-dec-string-one-to-one
           (n x)
           (m 0))
         (:instance nat-to-dec-string-one-to-one
           (n y)
           (m 0)))
       :in-theory (disable not-member-minus-char-dec-digit-char-list*p)))))

(defthm stringify-integer-of-non-integer
  (implies (not (integerp x))
    (equal (stringify-integer x) "0"))
  :hints (("Goal" :in-theory (enable nat-to-dec-string-of-non-natp))))

(encapsulate nil
  (local (defthm not-member-slash-char-dec-digit-char-list*p
      (implies (dec-digit-char-list*p x)
        (not (member-equal #\/ x)))))
  (defthm not-member-/-stringify-integer
    (not (member-equal #\/
        (explode (stringify-integer i)))))
  (defthm not-member-/-nat-to-dec-string
    (not (member-equal #\/
        (explode (nat-to-dec-string i))))))

(in-theory (disable stringify-integer))

(defun stringify-rational
  (x)
  (declare (xargs :guard (rationalp x)))
  (if (or (integerp x)
      (mbe :logic (not (rationalp x)) :exec nil))
    (stringify-integer x)
    (cat (stringify-integer (numerator x))
      "/"
      (nat-to-dec-string (denominator x)))))

(local (defthm member-equal-append
    (iff (member-equal k (append a b))
      (or (member-equal k a)
        (member-equal k b)))))

(local (defun cdr-both-equal
    (a b)
    (if (or (atom a) (atom b))
      nil
      (and (and (consp a)
          (consp b)
          (equal (car a) (car b)))
        (cdr-both-equal (cdr a) (cdr b))))))

(local (defthm equal-appends-with-nonmembers-implies-components-equal
    (implies (and (not (member-equal x a))
        (not (member-equal x b))
        (not (member-equal x c))
        (not (member-equal x d))
        (true-listp a)
        (true-listp c))
      (equal (equal (append a (cons x b))
          (append c (cons x d)))
        (and (equal a c) (equal b d))))
    :hints ((and stable-under-simplificationp
       `(:induct (cdr-both-equal a c)
         :expand ((append a (cons x b)) (append c (cons x d))))))
    :otf-flg t))

(encapsulate nil
  (local (defthm switch-coerce-append-string
      (implies (and (character-listp a)
          (character-listp b)
          (stringp c))
        (and (equal (equal (implode (append a b)) c)
            (equal (append a b) (explode c)))
          (equal (equal c (implode (append a b)))
            (equal (append a b) (explode c)))))))
  (local (defthm not-equal-if-not-members-append-cons
      (implies (not (member-equal a c))
        (not (equal (append b (cons a d)) c)))))
  (defthm stringify-rational-one-to-one
    (equal (equal (stringify-rational x)
        (stringify-rational y))
      (equal (rfix x) (rfix y)))
    :hints (("goal" :use ((:instance not-member-/-stringify-integer
          (i x)) (:instance not-member-/-stringify-integer
           (i y))
         (:instance not-member-/-stringify-integer
           (i (numerator x)))
         (:instance not-member-/-stringify-integer
           (i (numerator y)))
         (:instance stringify-integer-one-to-one
           (x y)
           (y 0))
         (:instance stringify-integer-one-to-one
           (x x)
           (y 0))
         (:instance rational-implies2)
         (:instance rational-implies2 (x y)))
       :in-theory (disable not-member-/-stringify-integer
         rational-implies2)))))

(encapsulate nil
  (local (defthm not-member-sharp-char-dec-digit-char-list*p
      (implies (dec-digit-char-list*p x)
        (not (member-equal #\# x)))))
  (defthm not-member-sharp-nat-to-dec-string
    (not (member-equal #\#
        (explode (nat-to-dec-string i)))))
  (defthm not-member-sharp-stringify-integer
    (not (member-equal #\#
        (explode (stringify-integer i))))
    :hints (("Goal" :in-theory (enable stringify-integer))))
  (defthm not-member-sharp-stringify-rational
    (not (member-equal #\#
        (explode (stringify-rational r))))))

(encapsulate nil
  (local (defthm not-member-space-char-dec-digit-char-list*p
      (implies (dec-digit-char-list*p x)
        (not (member-equal #\  x)))))
  (defthm not-member-space-nat-to-dec-string
    (not (member-equal #\ 
        (explode (nat-to-dec-string i)))))
  (defthm not-member-space-stringify-integer
    (not (member-equal #\ 
        (explode (stringify-integer i))))
    :hints (("Goal" :in-theory (enable stringify-integer))))
  (defthm not-member-space-stringify-rational
    (not (member-equal #\ 
        (explode (stringify-rational r))))))

(in-theory (disable stringify-rational))

(defun stringify-number
  (x)
  (declare (xargs :guard (acl2-numberp x)))
  (if (or (rationalp x)
      (mbe :logic (not (acl2-numberp x)) :exec nil))
    (stringify-rational x)
    (cat "#C("
      (stringify-rational (realpart x))
      " "
      (stringify-rational (imagpart x))
      ")")))

(encapsulate nil
  (local (defthm switch-coerce-list*-append-string
      (implies (and (character-listp a)
          (character-listp b)
          (characterp e)
          (characterp f)
          (characterp g)
          (stringp c))
        (and (equal (equal (implode (list* e f g (append a b)))
              c)
            (equal (list* e f g (append a b))
              (explode c)))
          (equal (equal c
              (implode (list* e f g (append a b))))
            (equal (list* e f g (append a b))
              (explode c)))))))
  (local (defthmd not-equal-by-len
      (implies (not (equal (len x) (len y)))
        (not (equal x y)))))
  (local (defthm len-append-linear
      (<= (len x) (len (append z x)))
      :rule-classes :linear))
  (local (defthm not-equal-x-cons-y-append-z-x
      (not (equal x (cons y (append z x))))
      :hints (("goal" :in-theory (enable not-equal-by-len)))))
  (local (defthm equal-append-to-tail
      (implies (and (true-listp a) (true-listp b))
        (equal (equal (append a c) (append b c))
          (equal a b)))
      :hints (("goal" :induct (cdr-both-equal a b)
         :expand ((append a c) (append b c))))))
  (defthm stringify-number-one-to-one
    (equal (equal (stringify-number x)
        (stringify-number y))
      (equal (fix x) (fix y)))
    :hints (("goal" :use ((:instance not-member-space-stringify-rational
          (r x)) (:instance not-member-space-stringify-rational
           (r y))
         (:instance not-member-space-stringify-rational
           (r (realpart x)))
         (:instance not-member-space-stringify-rational
           (r (realpart y)))
         (:instance not-member-space-stringify-rational
           (r (imagpart x)))
         (:instance not-member-space-stringify-rational
           (r (imagpart y)))
         (:instance stringify-rational-one-to-one
           (x y)
           (y 0))
         (:instance stringify-rational-one-to-one
           (x x)
           (y 0))
         (:instance realpart-imagpart-elim)
         (:instance realpart-imagpart-elim (x y)))
       :in-theory (disable not-member-space-stringify-rational
         realpart-imagpart-elim)))))

(defun upper-case-or-dec-digit-char-list*p
  (x)
  (declare (xargs :guard (character-listp x)))
  (if (atom x)
    t
    (and (or (up-alpha-p (car x))
        (dec-digit-char-p (car x)))
      (upper-case-or-dec-digit-char-list*p (cdr x)))))

(in-theory (disable upper-case-or-dec-digit-char-list*p
    up-alpha-p))

(local (defthm characterp-car-of-character-listp
    (implies (and (character-listp x) (consp x))
      (characterp (car x)))))

(local (defthm character-listp-cdr-of-character-listp
    (implies (character-listp x)
      (character-listp (cdr x)))))

(defun escape-free-symnamep
  (x)
  (declare (xargs :guard (stringp x)))
  (let ((lst (explode x)))
    (and (consp lst)
      (up-alpha-p (car lst))
      (upper-case-or-dec-digit-char-list*p (cdr lst)))))

(local (defthm assoc-append
    (equal (append (append a b) c)
      (append a b c))))

(local (defthm fold-constants-append
    (implies (syntaxp (and (quotep a) (quotep b)))
      (equal (append a b c)
        (append (append a b) c)))))

(defun stringify-symbol
  (x)
  (declare (type symbol x))
  (let ((name (symbol-name x)) (pkg (symbol-package-name x)))
    (mbe :logic (if (symbolp x)
        (let ((pkg-string (if (equal pkg "ACL2")
               ""
               (if (escape-free-symnamep pkg)
                 (cat pkg "::")
                 (cat "|" pkg "|::")))) (name-string (if (escape-free-symnamep name)
                name
                (cat "|" name "|"))))
          (cat pkg-string name-string))
        "COMMON-LISP::NIL")
      :exec (if (equal pkg "ACL2")
        (if (escape-free-symnamep name)
          name
          (cat "|" name "|"))
        (if (escape-free-symnamep pkg)
          (if (escape-free-symnamep name)
            (cat pkg "::" name)
            (cat pkg "::|" name "|"))
          (if (escape-free-symnamep name)
            (cat "|" pkg "|::" name)
            (cat "|" pkg "|::|" name "|")))))))

(in-theory (disable escape-free-symnamep))

(defun stringify-atom
  (x)
  (declare (xargs :guard (atom x)))
  (cond ((symbolp x) (stringify-symbol x))
    ((stringp x) (cat """ x """))
    ((acl2-numberp x) (stringify-number x))
    ((characterp x) (cat "#\" (implode (list x))))
    (t "##**BAD-ATOM**##")))