		Search-engine friendly clone of the ACL2 documentation.

Unicode-escapes

Even-backslashes-tree-constraints-p

Necessary condition for parsed trees to be Unicode escapes.

This is used to constrain the result of the declaratively defined parser for Unicode escapes. The parser maps a list of Unicode characters to a list of unicode-input-character trees (when successful), such that the string at the leaves of the output trees is the input Unicode character list (this is the constraint expressed by the grammar alone), and such that some additional constrains are satisfied. This predicates expresses one such additional constraint, namely that if the (only) subtree of any parsed tree is a unicode-escape tree (i.e. if a Unicode escape is parsed), then the backslash that starts the Unicode escape must be eligible, i.e. preceded by an even number of backslashes in the character list.

Since, as mentioned above, the input of the parser is the string at the leaves of the trees (as stated in subsequent predicates), this predicate only takes a list of trees as argument: the Unicode character list can be derived from the list of trees.

Note that we do not need to use uniescapep here, because the implicit grammar constraint, namely that the string at the leaves of the tree is the parser input, captures most of uniescapep, except for the requirement on preceding backslashes.

Definitions and Theorems

Theorem: even-backslashes-tree-constraints-p-necc

(defthm even-backslashes-tree-constraints-p-necc
 (implies
  (even-backslashes-tree-constraints-p trees)
  (implies
      (and (integer-range-p 0 (len trees) i)
           (unicode-input-character-tree-is-escape-p (nth i trees)))
      (even-backslashes-before-p
           (len (abnf::tree-list->string (take i trees)))
           (abnf::tree-list->string trees)))))

Theorem: booleanp-of-even-backslashes-tree-constraints-p

(defthm booleanp-of-even-backslashes-tree-constraints-p
  (b* ((yes/no (even-backslashes-tree-constraints-p trees)))
    (booleanp yes/no))
  :rule-classes :rewrite)