		Search-engine friendly clone of the ACL2 documentation.

Parser

Lex-binary-op

Lex a binary-op.

Signature
(lex-binary-op input) → (mv ret-tree ret-input)
Arguments: input — Guard (nat-listp input).
Returns: ret-tree — Type (abnf::tree-resultp ret-tree).; ret-input — Type (nat-listp ret-input).

Definitions and Theorems

Function: lex-binary-op

(defun lex-binary-op (input)
  (declare (xargs :guard (nat-listp input)))
  (let ((__function__ 'lex-binary-op))
    (declare (ignorable __function__))
    (b* (((mv outer-tree outer-input-after-tree)
          (b* (((mv tree input-after-tree)
                (abnf::parse-schars "add.w" input))
               ((unless (reserrp tree))
                (mv tree input-after-tree))
               ((mv tree input-after-tree)
                (abnf::parse-schars "add" input))
               ((unless (reserrp tree))
                (mv tree input-after-tree))
               ((mv tree input-after-tree)
                (abnf::parse-schars "sub.w" input))
               ((unless (reserrp tree))
                (mv tree input-after-tree))
               ((mv tree input-after-tree)
                (abnf::parse-schars "sub" input))
               ((unless (reserrp tree))
                (mv tree input-after-tree))
               ((mv tree input-after-tree)
                (abnf::parse-schars "mul.w" input))
               ((unless (reserrp tree))
                (mv tree input-after-tree))
               ((mv tree input-after-tree)
                (abnf::parse-schars "mul" input))
               ((unless (reserrp tree))
                (mv tree input-after-tree))
               ((mv tree input-after-tree)
                (abnf::parse-schars "div.w" input))
               ((unless (reserrp tree))
                (mv tree input-after-tree))
               ((mv tree input-after-tree)
                (abnf::parse-schars "div" input))
               ((unless (reserrp tree))
                (mv tree input-after-tree))
               ((mv tree input-after-tree)
                (abnf::parse-schars "rem.w" input))
               ((unless (reserrp tree))
                (mv tree input-after-tree))
               ((mv tree input-after-tree)
                (abnf::parse-schars "rem" input))
               ((unless (reserrp tree))
                (mv tree input-after-tree))
               ((mv tree input-after-tree)
                (abnf::parse-schars "mod" input))
               ((unless (reserrp tree))
                (mv tree input-after-tree))
               ((mv tree input-after-tree)
                (abnf::parse-schars "pow.w" input))
               ((unless (reserrp tree))
                (mv tree input-after-tree))
               ((mv tree input-after-tree)
                (abnf::parse-schars "pow" input))
               ((unless (reserrp tree))
                (mv tree input-after-tree))
               ((mv tree input-after-tree)
                (abnf::parse-schars "shl.w" input))
               ((unless (reserrp tree))
                (mv tree input-after-tree))
               ((mv tree input-after-tree)
                (abnf::parse-schars "shl" input))
               ((unless (reserrp tree))
                (mv tree input-after-tree))
               ((mv tree input-after-tree)
                (abnf::parse-schars "shr.w" input))
               ((unless (reserrp tree))
                (mv tree input-after-tree))
               ((mv tree input-after-tree)
                (abnf::parse-schars "shr" input))
               ((unless (reserrp tree))
                (mv tree input-after-tree))
               ((mv tree input-after-tree)
                (abnf::parse-schars "and" input))
               ((unless (reserrp tree))
                (mv tree input-after-tree))
               ((mv tree input-after-tree)
                (abnf::parse-schars "or" input))
               ((unless (reserrp tree))
                (mv tree input-after-tree))
               ((mv tree input-after-tree)
                (abnf::parse-schars "xor" input))
               ((unless (reserrp tree))
                (mv tree input-after-tree))
               ((mv tree input-after-tree)
                (abnf::parse-schars "nand" input))
               ((unless (reserrp tree))
                (mv tree input-after-tree))
               ((mv tree input-after-tree)
                (abnf::parse-schars "nor" input))
               ((unless (reserrp tree))
                (mv tree input-after-tree))
               ((mv tree input-after-tree)
                (abnf::parse-schars "gte" input))
               ((unless (reserrp tree))
                (mv tree input-after-tree))
               ((mv tree input-after-tree)
                (abnf::parse-schars "gt" input))
               ((unless (reserrp tree))
                (mv tree input-after-tree))
               ((mv tree input-after-tree)
                (abnf::parse-schars "lte" input))
               ((unless (reserrp tree))
                (mv tree input-after-tree))
               ((mv tree input-after-tree)
                (abnf::parse-schars "lt" input))
               ((unless (reserrp tree))
                (mv tree input-after-tree)))
            (mv (reserrf-push tree)
                (nat-list-fix input))))
         ((when (reserrp outer-tree))
          (mv outer-tree (nat-list-fix input))))
      (mv (abnf-tree-wrap outer-tree "binary-op")
          outer-input-after-tree))))

Theorem: tree-resultp-of-lex-binary-op.ret-tree

(defthm tree-resultp-of-lex-binary-op.ret-tree
  (b* (((mv ?ret-tree ?ret-input)
        (lex-binary-op input)))
    (abnf::tree-resultp ret-tree))
  :rule-classes :rewrite)

Theorem: nat-listp-of-lex-binary-op.ret-input

(defthm nat-listp-of-lex-binary-op.ret-input
  (b* (((mv ?ret-tree ?ret-input)
        (lex-binary-op input)))
    (nat-listp ret-input))
  :rule-classes :rewrite)

Theorem: len-of-lex-binary-op-<=

(defthm len-of-lex-binary-op-<=
  (b* (((mv ?ret-tree ?ret-input)
        (lex-binary-op input)))
    (<= (len ret-input) (len input)))
  :rule-classes :linear)

Theorem: len-of-lex-binary-op-<

(defthm len-of-lex-binary-op-<
  (b* (((mv ?ret-tree ?ret-input)
        (lex-binary-op input)))
    (implies (not (reserrp ret-tree))
             (< (len ret-input) (len input))))
  :rule-classes :linear)

Theorem: lex-binary-op-of-nat-list-fix-input

(defthm lex-binary-op-of-nat-list-fix-input
  (equal (lex-binary-op (nat-list-fix input))
         (lex-binary-op input)))

Theorem: lex-binary-op-nat-list-equiv-congruence-on-input

(defthm lex-binary-op-nat-list-equiv-congruence-on-input
  (implies (acl2::nat-list-equiv input input-equiv)
           (equal (lex-binary-op input)
                  (lex-binary-op input-equiv)))
  :rule-classes :congruence)