		Search-engine friendly clone of the ACL2 documentation.

Unicode-escapes

Uniescape-parse

Parse the Unicode escapes in a list of Unicode characters.

Signature
(uniescape-parse unicodes) → (mv errorp trees)
Arguments: unicodes — Guard (unicode-listp unicodes).
Returns: errorp — Type (booleanp errorp).; trees — Type (abnf-tree-list-with-root-p trees "unicode-input-character").

This parser is declaratively defined in terms of the witness of uniescape-parse-p. If the list of Unicode characters has a corresponding list of parse trees (i.e. such that the input/output constraints are satisified), they are returned; otherwise the parser fails. This parser should never fail, but this remains to be proved formally.

Generally a parser returns a single parse trees, but Java's first lexical translation step must take place before any further parsing. Therefore, it is appropriate for this parser to return a list of unicode-input-character trees.

Definitions and Theorems

Function: uniescape-parse

(defun uniescape-parse (unicodes)
  (declare (xargs :guard (unicode-listp unicodes)))
  (let ((__function__ 'uniescape-parse))
    (declare (ignorable __function__))
    (if (uniescape-parse-p unicodes)
        (mv nil (uniescape-parse-witness unicodes))
      (mv t nil))))

Theorem: booleanp-of-uniescape-parse.errorp

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

Theorem: return-type-of-uniescape-parse.trees

(defthm return-type-of-uniescape-parse.trees
  (b* (((mv ?errorp ?trees)
        (uniescape-parse unicodes)))
    (abnf-tree-list-with-root-p trees "unicode-input-character"))
  :rule-classes :rewrite)