		Search-engine friendly clone of the ACL2 documentation.

Parsing-primitives-seq

Parse-exact-list

Parse zero or more given natural numbers into a tree that matches a direct numeric value notation that consists of that list of numbers.

Signature
(parse-exact-list nats input) → (mv error? tree? rest-input)
Arguments: nats — Guard (nat-listp nats).; input — Guard (nat-listp input).
Returns: error? — Type (maybe-msgp error?).; tree? — Type (and (tree-optionp tree?) (implies (not error?) (treep tree?)) (implies error? (not tree?))) .; rest-input — Type (nat-listp rest-input).

Definitions and Theorems

Function: parse-exact-list-aux

(defun parse-exact-list-aux (nats input)
  (declare (xargs :guard (and (nat-listp nats)
                              (nat-listp input))))
  (let ((__function__ 'parse-exact-list-aux))
    (declare (ignorable __function__))
    (b* (((when (endp nats))
          (mv nil (nat-list-fix input)))
         (nat (lnfix (car nats)))
         ((mv error? input-nat input)
          (parse-any input))
         ((when error?) (mv error? input))
         ((unless (= input-nat nat))
          (mv (msg "Failed to parse ~x0: found ~x1 instead."
                   nat input-nat)
              (cons input-nat input)))
         ((mv error? input)
          (parse-exact-list-aux (cdr nats) input))
         ((when error?) (mv error? input)))
      (mv nil input))))

Theorem: maybe-msgp-of-parse-exact-list-aux.error?

(defthm maybe-msgp-of-parse-exact-list-aux.error?
  (b* (((mv ?error? ?rest-input)
        (parse-exact-list-aux nats input)))
    (maybe-msgp error?))
  :rule-classes :rewrite)

Theorem: nat-listp-of-parse-exact-list-aux.rest-input

(defthm nat-listp-of-parse-exact-list-aux.rest-input
  (b* (((mv ?error? ?rest-input)
        (parse-exact-list-aux nats input)))
    (nat-listp rest-input))
  :rule-classes :rewrite)

Theorem: len-of-parse-exact-list-aux-linear-<=

(defthm len-of-parse-exact-list-aux-linear-<=
  (b* (((mv ?error? ?rest-input)
        (parse-exact-list-aux nats input)))
    (<= (len rest-input) (len input)))
  :rule-classes :linear)

Theorem: len-of-parse-exact-list-aux-linear-<

(defthm len-of-parse-exact-list-aux-linear-<
  (b* (((mv ?error? ?rest-input)
        (parse-exact-list-aux nats input)))
    (implies (and (not error?) (consp nats))
             (< (len rest-input) (len input))))
  :rule-classes :linear)

Theorem: parse-exact-list-aux-of-nat-list-fix-nats

(defthm parse-exact-list-aux-of-nat-list-fix-nats
  (equal (parse-exact-list-aux (nat-list-fix nats)
                               input)
         (parse-exact-list-aux nats input)))

Theorem: parse-exact-list-aux-nat-list-equiv-congruence-on-nats

(defthm parse-exact-list-aux-nat-list-equiv-congruence-on-nats
  (implies (acl2::nat-list-equiv nats nats-equiv)
           (equal (parse-exact-list-aux nats input)
                  (parse-exact-list-aux nats-equiv input)))
  :rule-classes :congruence)

Theorem: parse-exact-list-aux-of-nat-list-fix-input

(defthm parse-exact-list-aux-of-nat-list-fix-input
  (equal (parse-exact-list-aux nats (nat-list-fix input))
         (parse-exact-list-aux nats input)))

Theorem: parse-exact-list-aux-nat-list-equiv-congruence-on-input

(defthm parse-exact-list-aux-nat-list-equiv-congruence-on-input
  (implies (acl2::nat-list-equiv input input-equiv)
           (equal (parse-exact-list-aux nats input)
                  (parse-exact-list-aux nats input-equiv)))
  :rule-classes :congruence)

Function: parse-exact-list

(defun parse-exact-list (nats input)
  (declare (xargs :guard (and (nat-listp nats)
                              (nat-listp input))))
  (let ((__function__ 'parse-exact-list))
    (declare (ignorable __function__))
    (b* (((mv error? input)
          (parse-exact-list-aux nats input))
         ((when error?) (mv error? nil input)))
      (mv nil (tree-leafterm nats) input))))

Theorem: maybe-msgp-of-parse-exact-list.error?

(defthm maybe-msgp-of-parse-exact-list.error?
  (b* (((mv ?error? ?tree? ?rest-input)
        (parse-exact-list nats input)))
    (maybe-msgp error?))
  :rule-classes :rewrite)

Theorem: return-type-of-parse-exact-list.tree?

(defthm return-type-of-parse-exact-list.tree?
  (b* (((mv ?error? ?tree? ?rest-input)
        (parse-exact-list nats input)))
    (and (tree-optionp tree?)
         (implies (not error?) (treep tree?))
         (implies error? (not tree?))))
  :rule-classes :rewrite)

Theorem: nat-listp-of-parse-exact-list.rest-input

(defthm nat-listp-of-parse-exact-list.rest-input
  (b* (((mv ?error? ?tree? ?rest-input)
        (parse-exact-list nats input)))
    (nat-listp rest-input))
  :rule-classes :rewrite)

Theorem: len-of-parse-exact-list-linear-<=

(defthm len-of-parse-exact-list-linear-<=
  (b* (((mv ?error? ?tree? ?rest-input)
        (parse-exact-list nats input)))
    (<= (len rest-input) (len input)))
  :rule-classes :linear)

Theorem: len-of-parse-exact-list-linear-<

(defthm len-of-parse-exact-list-linear-<
  (b* (((mv ?error? ?tree? ?rest-input)
        (parse-exact-list nats input)))
    (implies (and (not error?) (consp nats))
             (< (len rest-input) (len input))))
  :rule-classes :linear)

Theorem: parse-exact-list-of-nat-list-fix-nats

(defthm parse-exact-list-of-nat-list-fix-nats
  (equal (parse-exact-list (nat-list-fix nats)
                           input)
         (parse-exact-list nats input)))

Theorem: parse-exact-list-nat-list-equiv-congruence-on-nats

(defthm parse-exact-list-nat-list-equiv-congruence-on-nats
  (implies (acl2::nat-list-equiv nats nats-equiv)
           (equal (parse-exact-list nats input)
                  (parse-exact-list nats-equiv input)))
  :rule-classes :congruence)

Theorem: parse-exact-list-of-nat-list-fix-input

(defthm parse-exact-list-of-nat-list-fix-input
  (equal (parse-exact-list nats (nat-list-fix input))
         (parse-exact-list nats input)))

Theorem: parse-exact-list-nat-list-equiv-congruence-on-input

(defthm parse-exact-list-nat-list-equiv-congruence-on-input
  (implies (acl2::nat-list-equiv input input-equiv)
           (equal (parse-exact-list nats input)
                  (parse-exact-list nats input-equiv)))
  :rule-classes :congruence)