(in-package "ACL2")

(defun nat->string (n)
  (coerce (explode-nonnegative-integer n 10 nil) 'string))

(defun integer->string (i)
  (if (natp i) (nat->string i)
    (concatenate 'string
                 "-"
                 (nat->string (abs i)))))

(defun rational->string (r)
  (if (integerp r) (integer->string r)
    (concatenate 'string
                 (integer->string (numerator r))
                 "/"
                 (integer->string (denominator r)))))

(defun acl2-number->string (n)
  (if (rationalp n) (rational->string n)
    (concatenate 'string
                 "(complex "
                 (rational->string (realpart n))
                 " "
                 (rational->string (imagpart n))
                 ")")))

(defun atom->string (a)
  (cond
   ((acl2-numberp a)
    (acl2-number->string a))
   ((characterp a) (coerce (list #\# #\\ a) 'string))
   ((stringp a) (concatenate 'string "\"" a "\""))
   (t (string a))))

(mutual-recursion
 (defun cdr->string (l)
   (declare (xargs :measure (acl2-count l)))
   (cond
    ((null l) "")
    ((atom l) (concatenate 'string " . " (atom->string l)))
    ((consp l)
     (concatenate 'string
                  " "
                  (sexp->string (car l))
                  (cdr->string (cdr l))))))

 (defun sexp->string (sexp)
   (declare (xargs :measure (acl2-count sexp)))
   (if (atom sexp) (atom->string sexp)
     (concatenate 'string
                  "("
                  (sexp->string (car sexp))
                  (cdr->string (cdr sexp))
                  ")"))))

(defun sexp->symbol (sexp)
  (intern (sexp->string sexp) "ACL2"))