		Search-engine friendly clone of the ACL2 documentation.

Concrete-syntax

Parsep

Declarative parsing specification.

Signature
(parsep ucodes tree) → yes/no
Arguments: ucodes — Guard (leo-early::unicode-listp ucodes).; tree — Guard (abnf::treep tree).
Returns: yes/no — Type (booleanp yes/no).

For now we just define this as the grammatical parsing captured by grammar-parsep.

If for each ucodes there were always at most one tree such that that predicate holds, the grammar would be unambiguous, and parsing requirements would be completely defined by this predicate. However, the grammar is currently ambiguous. We plan to refine the grammar, and/or add extra-grammatical requirements, to refine this specification to one that unambiguously defines at one tree for each syntactically valid sequence of Unicode characters.

Definitions and Theorems

Function: parsep

(defun parsep (ucodes tree)
  (declare (xargs :guard (and (leo-early::unicode-listp ucodes)
                              (abnf::treep tree))))
  (let ((__function__ 'parsep))
    (declare (ignorable __function__))
    (grammar-parsep ucodes tree)))

Theorem: booleanp-of-parsep

(defthm booleanp-of-parsep
  (b* ((yes/no (parsep ucodes tree)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: parsep-of-unicode-list-fix-ucodes

(defthm parsep-of-unicode-list-fix-ucodes
  (equal (parsep (leo-early::unicode-list-fix ucodes)
                 tree)
         (parsep ucodes tree)))

Theorem: parsep-unicode-list-equiv-congruence-on-ucodes

(defthm parsep-unicode-list-equiv-congruence-on-ucodes
  (implies (leo-early::unicode-list-equiv ucodes ucodes-equiv)
           (equal (parsep ucodes tree)
                  (parsep ucodes-equiv tree)))
  :rule-classes :congruence)

Theorem: parsep-of-tree-fix-tree

(defthm parsep-of-tree-fix-tree
  (equal (parsep ucodes (abnf::tree-fix tree))
         (parsep ucodes tree)))

Theorem: parsep-tree-equiv-congruence-on-tree

(defthm parsep-tree-equiv-congruence-on-tree
  (implies (abnf::tree-equiv tree tree-equiv)
           (equal (parsep ucodes tree)
                  (parsep ucodes tree-equiv)))
  :rule-classes :congruence)