		Search-engine friendly clone of the ACL2 documentation.

Unicode-escapes

Uniescape-process

Perform Java's first lexical translation step.

Signature
(uniescape-process unicodes) → (mv errorp new-unicodes)
Arguments: unicodes — Guard (unicode-listp unicodes).
Returns: errorp — Type (booleanp errorp).; new-unicodes — Type (unicode-listp new-unicodes).

We parse the Unicode characters into trees, and then we abstract the trees into Unicode characters. We also check that there no invalid Unicode escape candidates, returning an error if there are any.

We propagate any errors from the parser, even though there should never be any. See comments in uniescape-parse about this.

Definitions and Theorems

Function: uniescape-process

(defun uniescape-process (unicodes)
  (declare (xargs :guard (unicode-listp unicodes)))
  (let ((__function__ 'uniescape-process))
    (declare (ignorable __function__))
    (b* (((when (some-uniescape-candidate-invalid-p unicodes))
          (mv t nil))
         ((mv errorp trees)
          (uniescape-parse unicodes))
         ((when errorp) (mv t nil)))
      (mv nil
          (abs-unicode-input-character-list trees)))))

Theorem: booleanp-of-uniescape-process.errorp

(defthm booleanp-of-uniescape-process.errorp
  (b* (((mv ?errorp ?new-unicodes)
        (uniescape-process unicodes)))
    (booleanp errorp))
  :rule-classes :rewrite)

Theorem: unicode-listp-of-uniescape-process.new-unicodes

(defthm unicode-listp-of-uniescape-process.new-unicodes
  (b* (((mv ?errorp ?new-unicodes)
        (uniescape-process unicodes)))
    (unicode-listp new-unicodes))
  :rule-classes :rewrite)