		Search-engine friendly clone of the ACL2 documentation.

Unicode-escapes

Uniescape-tree-constraints-p

Sufficient condition for parsed trees to be Unicode escapes.

See the discussion in even-backslashes-tree-constraints-p regarding the declarative definition of the Unicode escape parser. This predicate captures another constraint, besides the grammar constraint: namely, that if there is a Unicode escape at some position in the Unicode character list (the string at the leaves of the tree), then the corresponding tree must be of a Unicode escape, i.e. its (only) subtree must be a unicode-escape tree.

Note that the position in question is expressed not directly, but indirectly via an index in the list of trees. There is no ``loss'' in doing that, because the string has to be decomposed into trees according to the grammar anyhow.

Definitions and Theorems

Theorem: uniescape-tree-constraints-p-necc

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

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

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