		Search-engine friendly clone of the ACL2 documentation.

Parser

Parse-rest-of-struct-component-expression

Parse the rest of a struct-component-expression.

Signature
(parse-rest-of-struct-component-expression token input current) → (mv tree next-token rest-input)
Arguments: token — Guard (abnf::tree-optionp token).; input — Guard (abnf::tree-listp input).; current — Guard (abnf::treep current).
Returns: tree — Type (abnf::tree-resultp tree).; next-token — Type (abnf::tree-optionp next-token).; rest-input — Type (abnf::tree-listp rest-input).

The argument current is the parsed postfix expression that starts the struct component expression.

Definitions and Theorems

Function: parse-rest-of-struct-component-expression

(defun parse-rest-of-struct-component-expression
       (token input current)
 (declare (xargs :guard (and (abnf::tree-optionp token)
                             (abnf::tree-listp input)
                             (abnf::treep current))))
 (let ((__function__ 'parse-rest-of-struct-component-expression))
  (declare (ignorable __function__))
  (b* (((pok tree2)
        (parse-symbol "." token input))
       ((pok tree3)
        (parse-identifier token input)))
   (mv
      (abnf::make-tree-nonleaf
           :rulename? (abnf::rulename "struct-component-expression")
           :branches (list (list current)
                           (list tree2)
                           (list tree3)))
      token input))))

Theorem: tree-resultp-of-parse-rest-of-struct-component-expression.tree

(defthm
     tree-resultp-of-parse-rest-of-struct-component-expression.tree
  (b* (((mv ?tree ?next-token ?rest-input)
        (parse-rest-of-struct-component-expression
             token input current)))
    (abnf::tree-resultp tree))
  :rule-classes :rewrite)

Theorem: tree-optionp-of-parse-rest-of-struct-component-expression.next-token

(defthm
 tree-optionp-of-parse-rest-of-struct-component-expression.next-token
 (b* (((mv ?tree ?next-token ?rest-input)
       (parse-rest-of-struct-component-expression
            token input current)))
   (abnf::tree-optionp next-token))
 :rule-classes :rewrite)

Theorem: tree-listp-of-parse-rest-of-struct-component-expression.rest-input

(defthm
 tree-listp-of-parse-rest-of-struct-component-expression.rest-input
 (b* (((mv ?tree ?next-token ?rest-input)
       (parse-rest-of-struct-component-expression
            token input current)))
   (abnf::tree-listp rest-input))
 :rule-classes :rewrite)

Theorem: parsize-of-parse-rest-of-struct-component-expression-<=

(defthm parsize-of-parse-rest-of-struct-component-expression-<=
  (b* (((mv ?tree ?next-token ?rest-input)
        (parse-rest-of-struct-component-expression
             token input current)))
    (<= (parsize next-token rest-input)
        (parsize token input)))
  :rule-classes :linear)

Theorem: parsize-of-parse-rest-of-struct-component-expression-<

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

Theorem: parse-rest-of-struct-component-expression-of-tree-option-fix-token

(defthm
 parse-rest-of-struct-component-expression-of-tree-option-fix-token
 (equal
   (parse-rest-of-struct-component-expression
        (abnf::tree-option-fix token)
        input current)
   (parse-rest-of-struct-component-expression token input current)))

Theorem: parse-rest-of-struct-component-expression-tree-option-equiv-congruence-on-token

(defthm
 parse-rest-of-struct-component-expression-tree-option-equiv-congruence-on-token
 (implies
  (abnf::tree-option-equiv token token-equiv)
  (equal
     (parse-rest-of-struct-component-expression token input current)
     (parse-rest-of-struct-component-expression
          token-equiv input current)))
 :rule-classes :congruence)

Theorem: parse-rest-of-struct-component-expression-of-tree-list-fix-input

(defthm
   parse-rest-of-struct-component-expression-of-tree-list-fix-input
 (equal
   (parse-rest-of-struct-component-expression
        token (abnf::tree-list-fix input)
        current)
   (parse-rest-of-struct-component-expression token input current)))

Theorem: parse-rest-of-struct-component-expression-tree-list-equiv-congruence-on-input

(defthm
 parse-rest-of-struct-component-expression-tree-list-equiv-congruence-on-input
 (implies
  (abnf::tree-list-equiv input input-equiv)
  (equal
     (parse-rest-of-struct-component-expression token input current)
     (parse-rest-of-struct-component-expression
          token input-equiv current)))
 :rule-classes :congruence)

Theorem: parse-rest-of-struct-component-expression-of-tree-fix-current

(defthm
      parse-rest-of-struct-component-expression-of-tree-fix-current
 (equal
   (parse-rest-of-struct-component-expression
        token input (abnf::tree-fix current))
   (parse-rest-of-struct-component-expression token input current)))

Theorem: parse-rest-of-struct-component-expression-tree-equiv-congruence-on-current

(defthm
 parse-rest-of-struct-component-expression-tree-equiv-congruence-on-current
 (implies
  (abnf::tree-equiv current current-equiv)
  (equal
     (parse-rest-of-struct-component-expression token input current)
     (parse-rest-of-struct-component-expression
          token input current-equiv)))
 :rule-classes :congruence)