		Search-engine friendly clone of the ACL2 documentation.

Parser

Parse-function-parameter

Parse a function-parameter.

Signature
(parse-function-parameter token input) → (mv tree next-token rest-input)
Arguments: token — Guard (abnf::tree-optionp token).; input — Guard (abnf::tree-listp input).
Returns: tree — Type (abnf::tree-resultp tree).; next-token — Type (abnf::tree-optionp next-token).; rest-input — Type (abnf::tree-listp rest-input).

Definitions and Theorems

Function: parse-function-parameter

(defun parse-function-parameter (token input)
 (declare (xargs :guard (and (abnf::tree-optionp token)
                             (abnf::tree-listp input))))
 (let ((__function__ 'parse-function-parameter))
  (declare (ignorable __function__))
  (b*
   (((pok tree1)
     (cond
       ((token-stringp "const" token)
        (b* (((pok tree)
              (parse-keyword "const" token input)))
          (mv (abnf::make-tree-nonleaf :rulename? nil
                                       :branches (list (list tree)))
              token input)))
       ((token-stringp "constant" token)
        (b* (((pok tree)
              (parse-keyword "constant" token input)))
          (mv (abnf::make-tree-nonleaf :rulename? nil
                                       :branches (list (list tree)))
              token input)))
       ((token-stringp "public" token)
        (b* (((pok tree)
              (parse-keyword "public" token input)))
          (mv (abnf::make-tree-nonleaf :rulename? nil
                                       :branches (list (list tree)))
              token input)))
       (t (mv (abnf::make-tree-nonleaf :rulename? nil
                                       :branches nil)
              token input))))
    ((pok tree2)
     (parse-identifier token input))
    ((pok tree3)
     (parse-symbol ":" token input))
    ((pok tree4) (parse-type token input)))
   (mv (abnf::make-tree-nonleaf
            :rulename? (abnf::rulename "function-parameter")
            :branches (list (list tree1)
                            (list tree2)
                            (list tree3)
                            (list tree4)))
       token input))))

Theorem: tree-resultp-of-parse-function-parameter.tree

(defthm tree-resultp-of-parse-function-parameter.tree
  (b* (((mv ?tree ?next-token ?rest-input)
        (parse-function-parameter token input)))
    (abnf::tree-resultp tree))
  :rule-classes :rewrite)

Theorem: tree-optionp-of-parse-function-parameter.next-token

(defthm tree-optionp-of-parse-function-parameter.next-token
  (b* (((mv ?tree ?next-token ?rest-input)
        (parse-function-parameter token input)))
    (abnf::tree-optionp next-token))
  :rule-classes :rewrite)

Theorem: tree-listp-of-parse-function-parameter.rest-input

(defthm tree-listp-of-parse-function-parameter.rest-input
  (b* (((mv ?tree ?next-token ?rest-input)
        (parse-function-parameter token input)))
    (abnf::tree-listp rest-input))
  :rule-classes :rewrite)

Theorem: parsize-of-parse-function-parameter-<=

(defthm parsize-of-parse-function-parameter-<=
  (b* (((mv ?tree ?next-token ?rest-input)
        (parse-function-parameter token input)))
    (<= (parsize next-token rest-input)
        (parsize token input)))
  :rule-classes :linear)

Theorem: parsize-of-parse-function-parameter-<

(defthm parsize-of-parse-function-parameter-<
  (b* (((mv ?tree ?next-token ?rest-input)
        (parse-function-parameter token input)))
    (implies (not (reserrp tree))
             (< (parsize next-token rest-input)
                (parsize token input))))
  :rule-classes :linear)

Theorem: parse-function-parameter-of-tree-option-fix-token

(defthm parse-function-parameter-of-tree-option-fix-token
  (equal (parse-function-parameter (abnf::tree-option-fix token)
                                   input)
         (parse-function-parameter token input)))

Theorem: parse-function-parameter-tree-option-equiv-congruence-on-token

(defthm
     parse-function-parameter-tree-option-equiv-congruence-on-token
  (implies (abnf::tree-option-equiv token token-equiv)
           (equal (parse-function-parameter token input)
                  (parse-function-parameter token-equiv input)))
  :rule-classes :congruence)

Theorem: parse-function-parameter-of-tree-list-fix-input

(defthm parse-function-parameter-of-tree-list-fix-input
 (equal (parse-function-parameter token (abnf::tree-list-fix input))
        (parse-function-parameter token input)))

Theorem: parse-function-parameter-tree-list-equiv-congruence-on-input

(defthm parse-function-parameter-tree-list-equiv-congruence-on-input
  (implies (abnf::tree-list-equiv input input-equiv)
           (equal (parse-function-parameter token input)
                  (parse-function-parameter token input-equiv)))
  :rule-classes :congruence)