		Search-engine friendly clone of the ACL2 documentation.

Unicode-escapes

Uniescape-parse-constraints-p

All the input/output constraints for the Unicode escape parser.

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

The Unicode escape parser takes as input a list of Unicode characters and returns as output a list of parsed unicode-input-character trees. This predicate characterizes the parser's input/output relationship: it says when, given the input, the parser is successful, and what the output is.

As motivated in the overview, the parser omits the check that some-uniescape-candidate-invalid-p does not hold, which does not involve the output anyhow. This check in the top-level function that formalizes Unicode escape processing, of which he parser is a component.

Here we express the constraints of the output with respect to the input. The string at the leaves of the trees must be the input string: this is the grammatical constraint. The other constraints are the necessary and sufficient conditions for parsed Unicode escape trees:

Necessary condition: if a tree is a parsed Unicode escape, then there is a Unicode escape in the input (where it suffices to say that there is an even number of preceding backslashes, as explained in even-backslashes-tree-constraints-p.
Sufficient condition: if there is a Unicode escape in the input, there must be a corresponding Unicode escapa tree.

These constraints should uniquely characterize the output for every possible input, but this remains to be proved formally.

Definitions and Theorems

Function: uniescape-parse-constraints-p

(defun uniescape-parse-constraints-p (unicodes trees)
 (declare
  (xargs
   :guard
   (and
     (unicode-listp unicodes)
     (abnf-tree-list-with-root-p trees "unicode-input-character"))))
 (and (equal (abnf::tree-list->string trees)
             unicodes)
      (even-backslashes-tree-constraints-p trees)
      (uniescape-tree-constraints-p trees)))

Theorem: booleanp-of-uniescape-parse-constraints-p

(defthm booleanp-of-uniescape-parse-constraints-p
  (b* ((yes/no (uniescape-parse-constraints-p unicodes trees)))
    (booleanp yes/no))
  :rule-classes :rewrite)