		Search-engine friendly clone of the ACL2 documentation.

Parser

Parsize

Size of the parser input.

Signature
(parsize token? input) → size
Arguments: token? — Guard (abnf::tree-optionp token?).; input — Guard (abnf::tree-listp input).
Returns: size — Type (natp size).

As discussed in parser, most parsing functions take the input with the next token (if present) prefetched. Thus, when considering the size of the input, and how it decreases during parsing, we need to take into account the next token. We count it as 1 if present, as 0 if absent.

Definitions and Theorems

Function: parsize

(defun parsize (token? input)
  (declare (xargs :guard (and (abnf::tree-optionp token?)
                              (abnf::tree-listp input))))
  (let ((__function__ 'parsize))
    (declare (ignorable __function__))
    (+ (abnf::tree-option-case token?
                               :some 1
                               :none 0)
       (len input))))

Theorem: natp-of-parsize

(defthm natp-of-parsize
  (b* ((size (parsize token? input)))
    (natp size))
  :rule-classes :rewrite)

Theorem: parsize-of-tree-option-fix-token?

(defthm parsize-of-tree-option-fix-token?
  (equal (parsize (abnf::tree-option-fix token?)
                  input)
         (parsize token? input)))

Theorem: parsize-tree-option-equiv-congruence-on-token?

(defthm parsize-tree-option-equiv-congruence-on-token?
  (implies (abnf::tree-option-equiv token? token?-equiv)
           (equal (parsize token? input)
                  (parsize token?-equiv input)))
  :rule-classes :congruence)

Theorem: parsize-of-tree-list-fix-input

(defthm parsize-of-tree-list-fix-input
  (equal (parsize token? (abnf::tree-list-fix input))
         (parsize token? input)))

Theorem: parsize-tree-list-equiv-congruence-on-input

(defthm parsize-tree-list-equiv-congruence-on-input
  (implies (abnf::tree-list-equiv input input-equiv)
           (equal (parsize token? input)
                  (parsize token? input-equiv)))
  :rule-classes :congruence)