		Search-engine friendly clone of the ACL2 documentation.

Input-parser

Parse-public/private/constants/constant/const

Parse a ( %s"public" / %s"private" / %s"constants" / %s"constant" / %s"const" ).

Signature
(parse-public/private/constants/constant/const 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).

Note that private and constants are identifiers, while the other three are keywords.

Definitions and Theorems

Function: parse-public/private/constants/constant/const

(defun parse-public/private/constants/constant/const (token input)
 (declare (xargs :guard (and (abnf::tree-optionp token)
                             (abnf::tree-listp input))))
 (let
    ((__function__ 'parse-public/private/constants/constant/const))
  (declare (ignorable __function__))
  (cond
   ((token-stringp "private" token)
    (b*
     (((pok tree)
       (parse-identifier token input))
      (tree (abnf::make-tree-nonleaf :rulename? nil
                                     :branches (list (list tree)))))
     (mv tree token input)))
   ((token-stringp "public" token)
    (b*
     (((pok tree)
       (parse-keyword "public" token input))
      (tree (abnf::make-tree-nonleaf :rulename? nil
                                     :branches (list (list tree)))))
     (mv tree token input)))
   ((token-stringp "constants" token)
    (b*
     (((pok tree)
       (parse-identifier token input))
      (tree (abnf::make-tree-nonleaf :rulename? nil
                                     :branches (list (list tree)))))
     (mv tree token input)))
   ((token-stringp "constant" token)
    (b*
     (((pok tree)
       (parse-keyword "constant" token input))
      (tree (abnf::make-tree-nonleaf :rulename? nil
                                     :branches (list (list tree)))))
     (mv tree token input)))
   ((token-stringp "const" token)
    (b*
     (((pok tree)
       (parse-keyword "const" token input))
      (tree (abnf::make-tree-nonleaf :rulename? nil
                                     :branches (list (list tree)))))
     (mv tree token input)))
   (t (mv (reserrf (list :found (abnf::tree-option-fix token)))
          (abnf::tree-option-fix token)
          (abnf::tree-list-fix input))))))

Theorem: tree-resultp-of-parse-public/private/constants/constant/const.tree

(defthm
 tree-resultp-of-parse-public/private/constants/constant/const.tree
 (b* (((mv ?tree ?next-token ?rest-input)
       (parse-public/private/constants/constant/const token input)))
   (abnf::tree-resultp tree))
 :rule-classes :rewrite)

Theorem: tree-optionp-of-parse-public/private/constants/constant/const.next-token

(defthm
 tree-optionp-of-parse-public/private/constants/constant/const.next-token
 (b* (((mv ?tree ?next-token ?rest-input)
       (parse-public/private/constants/constant/const token input)))
   (abnf::tree-optionp next-token))
 :rule-classes :rewrite)

Theorem: tree-listp-of-parse-public/private/constants/constant/const.rest-input

(defthm
 tree-listp-of-parse-public/private/constants/constant/const.rest-input
 (b* (((mv ?tree ?next-token ?rest-input)
       (parse-public/private/constants/constant/const token input)))
   (abnf::tree-listp rest-input))
 :rule-classes :rewrite)

Theorem: parsize-of-parse-public/private/constants/constant/const-<=

(defthm parsize-of-parse-public/private/constants/constant/const-<=
 (b* (((mv ?tree ?next-token ?rest-input)
       (parse-public/private/constants/constant/const token input)))
   (<= (parsize next-token rest-input)
       (parsize token input)))
 :rule-classes :linear)

Theorem: parsize-of-parse-public/private/constants/constant/const-<

(defthm parsize-of-parse-public/private/constants/constant/const-<
 (b* (((mv ?tree ?next-token ?rest-input)
       (parse-public/private/constants/constant/const token input)))
   (implies (not (reserrp tree))
            (< (parsize next-token rest-input)
               (parsize token input))))
 :rule-classes :linear)

Theorem: parse-public/private/constants/constant/const-of-tree-option-fix-token

(defthm
 parse-public/private/constants/constant/const-of-tree-option-fix-token
 (equal
      (parse-public/private/constants/constant/const
           (abnf::tree-option-fix token)
           input)
      (parse-public/private/constants/constant/const token input)))

Theorem: parse-public/private/constants/constant/const-tree-option-equiv-congruence-on-token

(defthm
 parse-public/private/constants/constant/const-tree-option-equiv-congruence-on-token
 (implies
  (abnf::tree-option-equiv token token-equiv)
  (equal (parse-public/private/constants/constant/const token input)
         (parse-public/private/constants/constant/const
              token-equiv input)))
 :rule-classes :congruence)

Theorem: parse-public/private/constants/constant/const-of-tree-list-fix-input

(defthm
 parse-public/private/constants/constant/const-of-tree-list-fix-input
 (equal
      (parse-public/private/constants/constant/const
           token (abnf::tree-list-fix input))
      (parse-public/private/constants/constant/const token input)))

Theorem: parse-public/private/constants/constant/const-tree-list-equiv-congruence-on-input

(defthm
 parse-public/private/constants/constant/const-tree-list-equiv-congruence-on-input
 (implies
  (abnf::tree-list-equiv input input-equiv)
  (equal (parse-public/private/constants/constant/const token input)
         (parse-public/private/constants/constant/const
              token input-equiv)))
 :rule-classes :congruence)