		Search-engine friendly clone of the ACL2 documentation.

Parser

Lex-program

Parse a program.

Signature
(lex-program 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-program

(defun lex-program (abnf::input)
 (declare (xargs :guard (nat-listp abnf::input)))
 (let ((__function__ 'lex-program))
  (declare (ignorable __function__))
  (b*
   (((mv abnf::treess abnf::input)
     (b*
      (((mv abnf::treess1 abnf::input1)
        (b*
         (((mv abnf::trees1 abnf::input)
           (lex-repetition-*-import abnf::input))
          ((when (reserrp abnf::trees1))
           (mv (reserrf-push abnf::trees1)
               abnf::input))
          ((mv abnf::tree abnf::input)
           (lex-cws abnf::input))
          ((when (reserrp abnf::tree))
           (mv (reserrf-push abnf::tree)
               abnf::input))
          (abnf::trees2 (list abnf::tree))
          ((mv abnf::tree abnf::input)
           (abnf::parse-schars "program" abnf::input))
          ((when (reserrp abnf::tree))
           (mv (reserrf-push abnf::tree)
               abnf::input))
          (abnf::trees3 (list abnf::tree))
          ((mv abnf::tree abnf::input)
           (lex-ws abnf::input))
          ((when (reserrp abnf::tree))
           (mv (reserrf-push abnf::tree)
               abnf::input))
          (abnf::trees4 (list abnf::tree))
          ((mv abnf::tree abnf::input)
           (lex-program-id abnf::input))
          ((when (reserrp abnf::tree))
           (mv (reserrf-push abnf::tree)
               abnf::input))
          (abnf::trees5 (list abnf::tree))
          ((mv abnf::tree abnf::input)
           (lex-ws abnf::input))
          ((when (reserrp abnf::tree))
           (mv (reserrf-push abnf::tree)
               abnf::input))
          (abnf::trees6 (list abnf::tree))
          ((mv abnf::tree abnf::input)
           (abnf::parse-ichars ";" abnf::input))
          ((when (reserrp abnf::tree))
           (mv (reserrf-push abnf::tree)
               abnf::input))
          (abnf::trees7 (list abnf::tree))
          ((mv abnf::trees8 abnf::input)
           (lex-repetition-1*-program-declaration abnf::input))
          ((when (reserrp abnf::trees8))
           (mv (reserrf-push abnf::trees8)
               abnf::input))
          ((mv abnf::tree abnf::input)
           (lex-cws abnf::input))
          ((when (reserrp abnf::tree))
           (mv (reserrf-push abnf::tree)
               abnf::input))
          (abnf::trees9 (list abnf::tree))
          (abnf::treess (list abnf::trees1
                              abnf::trees2 abnf::trees3 abnf::trees4
                              abnf::trees5 abnf::trees6 abnf::trees7
                              abnf::trees8 abnf::trees9)))
         (mv abnf::treess abnf::input)))
       ((when (not (reserrp abnf::treess1)))
        (mv abnf::treess1 abnf::input1)))
      (mv
       (reserrf
        (list
         :found (list abnf::treess1)
         :required
         '(((:repetition (:repeat 0 (:infinity))
                         (:rulename (:rulename "import")))
            (:repetition (:repeat 1 (:finite 1))
                         (:rulename (:rulename "cws")))
            (:repetition (:repeat 1 (:finite 1))
                         (:char-val (:sensitive "program")))
            (:repetition (:repeat 1 (:finite 1))
                         (:rulename (:rulename "ws")))
            (:repetition (:repeat 1 (:finite 1))
                         (:rulename (:rulename "program-id")))
            (:repetition (:repeat 1 (:finite 1))
                         (:rulename (:rulename "ws")))
            (:repetition (:repeat 1 (:finite 1))
                         (:char-val (:insensitive nil ";")))
            (:repetition
             (:repeat 1 (:infinity))
             (:group
                 (((:repetition (:repeat 1 (:finite 1))
                                (:rulename (:rulename "mapping"))))
                  ((:repetition (:repeat 1 (:finite 1))
                                (:rulename (:rulename "struct"))))
                  ((:repetition (:repeat 1 (:finite 1))
                                (:rulename (:rulename "record"))))
                  ((:repetition (:repeat 1 (:finite 1))
                                (:rulename (:rulename "function"))))
                  ((:repetition
                        (:repeat 1 (:finite 1))
                        (:rulename (:rulename "transition")))))))
            (:repetition (:repeat 1 (:finite 1))
                         (:rulename (:rulename "cws")))))))
       abnf::input)))
    ((when (reserrp abnf::treess))
     (mv (reserrf-push abnf::treess)
         (nat-list-fix abnf::input))))
   (mv
      (abnf::make-tree-nonleaf :rulename? (abnf::rulename "program")
                               :branches abnf::treess)
      abnf::input))))

Theorem: tree-resultp-of-lex-program.tree

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

Theorem: nat-listp-of-lex-program.rest-input

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

Theorem: len-of-lex-program-<=

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

Theorem: len-of-lex-program-<

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

Theorem: lex-program-of-nat-list-fix-input

(defthm lex-program-of-nat-list-fix-input
  (equal (lex-program (nat-list-fix abnf::input))
         (lex-program abnf::input)))

Theorem: lex-program-nat-list-equiv-congruence-on-input

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