names

(in-package "SMT")

(include-book "centaur/fty/top" :dir :system)

(include-book "xdoc/top" :dir :system)

(include-book "std/util/define" :dir :system)

(include-book "std/strings/top" :dir :system)

(include-book "std/strings/eqv" :dir :system)

(defsection smt-names
  :parents (z3-py)
  :short "SMT-names generates SMT solver friendly names."
  (define character-fix
    (x)
    (declare (xargs :guard (characterp x)))
    (mbe :logic (if (characterp x)
        x
        (code-char 0))
      :exec x))
  (defthm character-fix-idempotent-lemma
    (equal (character-fix (character-fix x))
      (character-fix x))
    :hints (("Goal" :in-theory (enable character-fix))))
  (deffixtype character
    :fix character-fix
    :pred characterp
    :equiv character-equiv
    :define t)
  (local (in-theory (enable character-fix)))
  (defalist special-char-alist
    :key-type character
    :val-type character-listp
    :pred special-char-alistp
    :verbosep t)
  (define special-list
    nil
    (declare (xargs :guard t))
    :returns (special-list special-char-alistp)
    '((#\_ #\_ #\u #\s #\c #\_) (#\- #\_ #\s #\u #\b #\_)
      (#\+ #\_ #\a #\d #\d #\_)
      (#\* #\_ #\m #\l #\t #\_)
      (#\/ #\_ #\d #\i #\v #\_)
      (#\< #\_ #\l #\t #\_)
      (#\> #\_ #\g #\t #\_)
      (#\= #\_ #\e #\q #\l #\_)
      (#\! #\_ #\e #\x #\c #\_)
      (#\@ #\_ #\a #\t #\_)
      (#\# #\_ #\h #\s #\h #\_)
      (#\$ #\_ #\d #\l #\r #\_)
      (#\% #\_ #\p #\c #\t #\_)
      (#\^ #\_ #\c #\a #\r #\_)
      (#\& #\_ #\a #\m #\p #\_)))
  (define special-char
    ((char characterp))
    :returns (special-char? booleanp)
    (if (assoc char (special-list))
      t
      nil))
  (define transform-special
    ((char characterp))
    :returns (special character-listp)
    (cdr (assoc char (special-list))))
  (define to-hex
    ((n natp))
    :returns (hex hex-digit-char-list*p)
    (nat-to-hex-chars n))
  (define construct-hex
    ((char characterp))
    :returns (hex character-listp)
    (append '(#\_) (to-hex (char-code char)) '(#\_)))
  (define char-is-number
    ((char characterp))
    :returns (is-number? booleanp)
    (cond ((not (characterp char)) nil)
      ((and (>= (char-code char) 48) (<= (char-code char) 57)) t)
      (t nil))
    ///
    (more-returns (is-number? (implies is-number? (characterp char))
        :name characterp-of-char-is-number)))
  (define char-is-letter
    ((char characterp))
    :returns (is-letter? booleanp)
    (cond ((not (characterp char)) nil)
      ((or (and (>= (char-code char) 65) (<= (char-code char) 90))
         (and (>= (char-code char) 97) (<= (char-code char) 122))) t)
      (t nil))
    ///
    (more-returns (is-letter? (implies is-letter? (characterp char))
        :name characterp-of-char-is-letter)))
  (define lisp-to-python-names-char
    ((char characterp))
    :returns (expanded-char character-listp)
    (cond ((or (char-is-number char) (char-is-letter char)) (list char))
      ((special-char char) (transform-special char))
      (t (construct-hex char))))
  (encapsulate nil
    (local (defthm lemma
        (implies (and (character-listp a)
            (character-listp b))
          (character-listp (append a b)))))
    (define lisp-to-python-names-list
      ((var-char character-listp))
      :returns (new-name character-listp)
      (if (endp var-char)
        nil
        (append (lisp-to-python-names-char (car var-char))
          (lisp-to-python-names-list (cdr var-char))))))
  (define lisp-to-python-names-list-top
    ((var-char character-listp))
    :returns (new-name character-listp)
    :guard-debug t
    (cond ((endp var-char) nil)
      ((char-is-number (car var-char)) (cons #\_ (lisp-to-python-names-list var-char)))
      (t (lisp-to-python-names-list var-char))))
  (define string-or-symbol-p
    (name)
    :returns (p? booleanp)
    (or (stringp name) (symbolp name)))
  (define string-or-symbol-fix
    ((x string-or-symbol-p))
    (mbe :logic (if (string-or-symbol-p x)
        x
        nil)
      :exec x))
  (local (in-theory (enable string-or-symbol-fix)))
  (deffixtype string-or-symbol
    :fix string-or-symbol-fix
    :pred string-or-symbol-p
    :equiv string-or-symbol-equiv
    :define t)
  (local (in-theory (enable characterp string-or-symbol-p)))
  (define lisp-to-python-names
    ((var string-or-symbol-p))
    :returns (name stringp)
    (b* ((var (string-or-symbol-fix var)) (var (if (stringp var)
            var
            (string var)))
        (var-char (coerce var 'list)))
      (coerce (lisp-to-python-names-list-top var-char)
        'string))))