		Search-engine friendly clone of the ACL2 documentation.

Atj-name-translation

Atj-char-to-jchars-id

Turn an ACL2 character into one or more Java characters for an ASCII Java identifier.

Signature
(atj-char-to-jchars-id char startp uscore flip-case-p) → jchars
Arguments: char — Guard (characterp char).; startp — Guard (booleanp startp).; uscore — Guard (member-eq uscore '(nil :dash :space)).; flip-case-p — Guard (booleanp flip-case-p).
Returns: jchars — Type (character-listp jchars), given (characterp char).

This is used to translate ACL2 variable, function, and package names to Java identifiers in the shallow embedding approach. It is also used to map ACL2 characters and strings to parts of Java identifiers.

ACL2 symbol names may consist of arbitrary sequences of 8-bit characters, while Java identifiers may only contain certain Unicode characters; when Unicode is restricted to ASCII, Java identifiers are much more restricted than ACL2 symbols. They are also more restricted than ACL2 package names, although ACL2 package names have restrictions of their own compared to Java identifiers, notably the uppercase restriction.

If an ACL2 character (part of an ACL2 symbol name or package name) is a letter, we keep it unchanged in forming the Java identifier, but we flip it from uppercase to lowercase or from lowercase to uppercase if the flip-case-p flag is t: since ACL2 symbols often have uppercase letters, by flipping them to lowercase we generate more readable and idiomatic Java identifiers; and flipping lowercase letters to uppercase letters avoids conflicts with ACL2 symbols that already have lowercase letters. On the other hand, since ACL2 package names cannot use lowercase letters, the flip-case-p is nil when we translate package names.

If the ACL2 character is a digit, we keep it unchanged only if it is not at the start of the Java identifier: this is indicated by the startp flag. If the digit is at the start of the Java identifier, we turn it into an ``escape'' $<digit>$: see the *atj-char-to-jchars-id* alist.

If the ACL2 character is neither a letter or a digit, by default we turn it into an ``escape'' of the form $.... For the printable ASCII characters that are not letters, we use the readable descriptions in the *atj-char-to-jchars-id* alist, e.g. HASH for #. For each of the other ISO 8859-1 characters (non-ASCII, or non-printable ASCII), we use a description that consists of x (for `hexadecimal') followed by the two hex digits that form the code of the character. The hexadecimal digits greater than 9 are all uppercase.

However, if the uscore parameter is non-nil, we turn the character indicated by uscore into an underscore instead. The possible non-nil values of uscore are :dash and :space. The value :dash is used when translating ACL2 names to Java names: in ACL2 names, dash is a very common ``separator''; thus, we map that to an underscore in Java, which fulfills a similar separation role. The value :space is used when translating ACL2 strings to parts of Java identifiers: in strings, space is perhaps a common character (at least for human-readable strings), and so by mapping that to an underscore, we retain some of the readability.

Definition: *atj-char-to-jchars-id*

(defconst *atj-char-to-jchars-id*
  '((#\Space . "$SPACE")
    (#\! . "$BANG")
    (#\" . "$DQUOTE")
    (#\# . "$HASH")
    (#\$ . "$DOLLAR")
    (#\% . "$PCENT")
    (#\& . "$AMPER")
    (#\' . "$SQUOTE")
    (#\( . "$OROUND")
    (#\) . "$CROUND")
    (#\* . "$STAR")
    (#\+ . "$PLUS")
    (#\, . "$COMMA")
    (#\- . "$DASH")
    (#\. . "$DOT")
    (#\/ . "$SLASH")
    (#\: . "$COLON")
    (#\; . "$SCOLON")
    (#\< . "$LT")
    (#\= . "$EQ")
    (#\> . "$GT")
    (#\? . "$QMARK")
    (#\@ . "$AT")
    (#\[ . "$OSQUARE")
    (#\\ . "$BSLASH")
    (#\] . "$CSQUARE")
    (#\^ . "$CARET")
    (#\_ . "$USCORE")
    (#\` . "$BQUOTE")
    (#\{ . "$OCURLY")
    (#\| . "$BAR")
    (#\} . "$CCURLY")
    (#\~ . "$TILDE")
    (#\0 . "$0$")
    (#\1 . "$1$")
    (#\2 . "$2$")
    (#\3 . "$3$")
    (#\4 . "$4$")
    (#\5 . "$5$")
    (#\6 . "$6$")
    (#\7 . "$7$")
    (#\8 . "$8$")
    (#\9 . "$9$")))

Definitions and Theorems

Function: atj-char-to-jchars-id

(defun atj-char-to-jchars-id (char startp uscore flip-case-p)
  (declare (xargs :guard (and (characterp char)
                              (booleanp startp)
                              (member-eq uscore '(nil :dash :space))
                              (booleanp flip-case-p))))
  (let ((__function__ 'atj-char-to-jchars-id))
    (declare (ignorable __function__))
    (b* (((when (str::up-alpha-p char))
          (if flip-case-p (list (str::downcase-char char))
            (list char)))
         ((when (str::down-alpha-p char))
          (if flip-case-p (list (str::upcase-char char))
            (list char)))
         ((when (and (digit-char-p char) (not startp)))
          (list char))
         ((when (or (and (eq uscore :dash) (eql char #\-))
                    (and (eq uscore :space)
                         (eql char #\Space))))
          (list #\_))
         (pair? (assoc char *atj-char-to-jchars-id*))
         ((when (consp pair?))
          (explode (cdr pair?)))
         (code (char-code char))
         ((mv hi-char lo-char)
          (ubyte8=>hexchars code)))
      (list #\$ #\x hi-char lo-char))))

Theorem: character-listp-of-atj-char-to-jchars-id

(defthm character-listp-of-atj-char-to-jchars-id
 (implies
  (characterp char)
  (b*
   ((jchars (atj-char-to-jchars-id char startp uscore flip-case-p)))
   (character-listp jchars)))
 :rule-classes :rewrite)