		Search-engine friendly clone of the ACL2 documentation.

Unicode-characters

String=>unicode

Convert an ACL2 string to a Java Unicode character list.

Signature
(string=>unicode string) → unicode
Arguments: string — Guard (stringp string).
Returns: unicode — Type (unicode-listp unicode).

This converts each ACL2 character in the string to a Unicode character whose value is the code of the character. In at last some of the Lisps on which ACL2 runs, strings may include non-ASCII Unicode characters, but ACL2's view of these strings is that of the sequence of ACL2 characters whose codes are the bytes that form the UTF-8 encoding of the string. This is as expected for ASCII, but not necessarily for non-ASCII. We plan to restrict this ACL2 function to operate only on ACL2 strings consisting of ASCII characters.

Definitions and Theorems

Function: string=>unicode

(defun string=>unicode (string)
  (declare (xargs :guard (stringp string)))
  (let ((__function__ 'string=>unicode))
    (declare (ignorable __function__))
    (string=>nats string)))

Theorem: unicode-listp-of-string=>unicode

(defthm unicode-listp-of-string=>unicode
  (b* ((unicode (string=>unicode string)))
    (unicode-listp unicode))
  :rule-classes :rewrite)

Theorem: string=>unicode-of-str-fix-string

(defthm string=>unicode-of-str-fix-string
  (equal (string=>unicode (str-fix string))
         (string=>unicode string)))

Theorem: string=>unicode-streqv-congruence-on-string

(defthm string=>unicode-streqv-congruence-on-string
  (implies (acl2::streqv string string-equiv)
           (equal (string=>unicode string)
                  (string=>unicode string-equiv)))
  :rule-classes :congruence)