		Search-engine friendly clone of the ACL2 documentation.

Parser

Lex-group-instruction-body

Parse a ( unary / binary / ternary / is / assert / commit / hash / cast / call ).

Signature
(lex-group-instruction-body abnf::input) → (mv abnf::tree abnf::rest-input)
Arguments: abnf::input — Guard (nat-listp abnf::input).
Returns: abnf::tree — Type (abnf::tree-resultp abnf::tree).; abnf::rest-input — Type (nat-listp abnf::rest-input).

Definitions and Theorems

Function: lex-group-instruction-body

(defun lex-group-instruction-body (abnf::input)
 (declare (xargs :guard (nat-listp abnf::input)))
 (let ((__function__ 'lex-group-instruction-body))
  (declare (ignorable __function__))
  (b*
   (((mv abnf::treess abnf::input)
     (b* (((mv abnf::treess1 abnf::input1)
           (b* (((mv abnf::tree abnf::input)
                 (lex-unary abnf::input))
                ((when (reserrp abnf::tree))
                 (mv (reserrf-push abnf::tree)
                     abnf::input))
                (abnf::trees1 (list abnf::tree))
                (abnf::treess (list abnf::trees1)))
             (mv abnf::treess abnf::input)))
          ((when (not (reserrp abnf::treess1)))
           (mv abnf::treess1 abnf::input1))
          ((mv abnf::treess2 abnf::input1)
           (b* (((mv abnf::tree abnf::input)
                 (lex-binary abnf::input))
                ((when (reserrp abnf::tree))
                 (mv (reserrf-push abnf::tree)
                     abnf::input))
                (abnf::trees1 (list abnf::tree))
                (abnf::treess (list abnf::trees1)))
             (mv abnf::treess abnf::input)))
          ((when (not (reserrp abnf::treess2)))
           (mv abnf::treess2 abnf::input1))
          ((mv abnf::treess3 abnf::input1)
           (b* (((mv abnf::tree abnf::input)
                 (lex-ternary abnf::input))
                ((when (reserrp abnf::tree))
                 (mv (reserrf-push abnf::tree)
                     abnf::input))
                (abnf::trees1 (list abnf::tree))
                (abnf::treess (list abnf::trees1)))
             (mv abnf::treess abnf::input)))
          ((when (not (reserrp abnf::treess3)))
           (mv abnf::treess3 abnf::input1))
          ((mv abnf::treess4 abnf::input1)
           (b* (((mv abnf::tree abnf::input)
                 (lex-is abnf::input))
                ((when (reserrp abnf::tree))
                 (mv (reserrf-push abnf::tree)
                     abnf::input))
                (abnf::trees1 (list abnf::tree))
                (abnf::treess (list abnf::trees1)))
             (mv abnf::treess abnf::input)))
          ((when (not (reserrp abnf::treess4)))
           (mv abnf::treess4 abnf::input1))
          ((mv abnf::treess5 abnf::input1)
           (b* (((mv abnf::tree abnf::input)
                 (lex-assert abnf::input))
                ((when (reserrp abnf::tree))
                 (mv (reserrf-push abnf::tree)
                     abnf::input))
                (abnf::trees1 (list abnf::tree))
                (abnf::treess (list abnf::trees1)))
             (mv abnf::treess abnf::input)))
          ((when (not (reserrp abnf::treess5)))
           (mv abnf::treess5 abnf::input1))
          ((mv abnf::treess6 abnf::input1)
           (b* (((mv abnf::tree abnf::input)
                 (lex-commit abnf::input))
                ((when (reserrp abnf::tree))
                 (mv (reserrf-push abnf::tree)
                     abnf::input))
                (abnf::trees1 (list abnf::tree))
                (abnf::treess (list abnf::trees1)))
             (mv abnf::treess abnf::input)))
          ((when (not (reserrp abnf::treess6)))
           (mv abnf::treess6 abnf::input1))
          ((mv abnf::treess7 abnf::input1)
           (b* (((mv abnf::tree abnf::input)
                 (lex-hash abnf::input))
                ((when (reserrp abnf::tree))
                 (mv (reserrf-push abnf::tree)
                     abnf::input))
                (abnf::trees1 (list abnf::tree))
                (abnf::treess (list abnf::trees1)))
             (mv abnf::treess abnf::input)))
          ((when (not (reserrp abnf::treess7)))
           (mv abnf::treess7 abnf::input1))
          ((mv abnf::treess8 abnf::input1)
           (b* (((mv abnf::tree abnf::input)
                 (lex-cast abnf::input))
                ((when (reserrp abnf::tree))
                 (mv (reserrf-push abnf::tree)
                     abnf::input))
                (abnf::trees1 (list abnf::tree))
                (abnf::treess (list abnf::trees1)))
             (mv abnf::treess abnf::input)))
          ((when (not (reserrp abnf::treess8)))
           (mv abnf::treess8 abnf::input1))
          ((mv abnf::treess9 abnf::input1)
           (b* (((mv abnf::tree abnf::input)
                 (lex-call abnf::input))
                ((when (reserrp abnf::tree))
                 (mv (reserrf-push abnf::tree)
                     abnf::input))
                (abnf::trees1 (list abnf::tree))
                (abnf::treess (list abnf::trees1)))
             (mv abnf::treess abnf::input)))
          ((when (not (reserrp abnf::treess9)))
           (mv abnf::treess9 abnf::input1)))
      (mv
       (reserrf
           (list :found (list abnf::treess1
                              abnf::treess2 abnf::treess3
                              abnf::treess4 abnf::treess5
                              abnf::treess6 abnf::treess7
                              abnf::treess8 abnf::treess9)
                 :required
                 '(((:repetition (:repeat 1 (:finite 1))
                                 (:rulename (:rulename "unary"))))
                   ((:repetition (:repeat 1 (:finite 1))
                                 (:rulename (:rulename "binary"))))
                   ((:repetition (:repeat 1 (:finite 1))
                                 (:rulename (:rulename "ternary"))))
                   ((:repetition (:repeat 1 (:finite 1))
                                 (:rulename (:rulename "is"))))
                   ((:repetition (:repeat 1 (:finite 1))
                                 (:rulename (:rulename "assert"))))
                   ((:repetition (:repeat 1 (:finite 1))
                                 (:rulename (:rulename "commit"))))
                   ((:repetition (:repeat 1 (:finite 1))
                                 (:rulename (:rulename "hash"))))
                   ((:repetition (:repeat 1 (:finite 1))
                                 (:rulename (:rulename "cast"))))
                   ((:repetition (:repeat 1 (:finite 1))
                                 (:rulename (:rulename "call")))))))
       abnf::input)))
    ((when (reserrp abnf::treess))
     (mv (reserrf-push abnf::treess)
         (nat-list-fix abnf::input))))
   (mv (abnf::make-tree-nonleaf :rulename? nil
                                :branches abnf::treess)
       abnf::input))))

Theorem: tree-resultp-of-lex-group-instruction-body.tree

(defthm tree-resultp-of-lex-group-instruction-body.tree
  (b* (((mv abnf::?tree abnf::?rest-input)
        (lex-group-instruction-body abnf::input)))
    (abnf::tree-resultp abnf::tree))
  :rule-classes :rewrite)

Theorem: nat-listp-of-lex-group-instruction-body.rest-input

(defthm nat-listp-of-lex-group-instruction-body.rest-input
  (b* (((mv abnf::?tree abnf::?rest-input)
        (lex-group-instruction-body abnf::input)))
    (nat-listp abnf::rest-input))
  :rule-classes :rewrite)

Theorem: len-of-lex-group-instruction-body-<=

(defthm len-of-lex-group-instruction-body-<=
  (b* (((mv abnf::?tree abnf::?rest-input)
        (lex-group-instruction-body abnf::input)))
    (<= (len abnf::rest-input)
        (len abnf::input)))
  :rule-classes :linear)

Theorem: len-of-lex-group-instruction-body-<

(defthm len-of-lex-group-instruction-body-<
  (b* (((mv abnf::?tree abnf::?rest-input)
        (lex-group-instruction-body abnf::input)))
    (implies (not (reserrp abnf::tree))
             (< (len abnf::rest-input)
                (len abnf::input))))
  :rule-classes :linear)

Theorem: lex-group-instruction-body-of-nat-list-fix-input

(defthm lex-group-instruction-body-of-nat-list-fix-input
  (equal (lex-group-instruction-body (nat-list-fix abnf::input))
         (lex-group-instruction-body abnf::input)))

Theorem: lex-group-instruction-body-nat-list-equiv-congruence-on-input

(defthm
      lex-group-instruction-body-nat-list-equiv-congruence-on-input
  (implies (acl2::nat-list-equiv abnf::input input-equiv)
           (equal (lex-group-instruction-body abnf::input)
                  (lex-group-instruction-body input-equiv)))
  :rule-classes :congruence)