• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Acre
    • Milawa
    • Smtlink
    • Aleobft
    • Abnf
      • Deftreeops
      • Defdefparse
      • Defgrammar
      • Abnf-tree-utilities
      • Notation
      • Grammar-parser
      • Meta-circular-validation
      • Parsing-primitives-defresult
      • Parsing-primitives-seq
        • Parse-exact-list
        • Parse-in-range
        • Parse-exact
        • Parse-any
      • Operations
      • Examples
      • Differences-with-paper
      • Grammar-printer
      • Parsing-tools
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • C
    • Java
    • Taspi
    • Bitcoin
    • Des
    • Ethereum
    • X86isa
    • Sha-2
    • Yul
    • Riscv
    • Zcash
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Poseidon
    • Where-do-i-place-my-book
    • Bigmems
    • Builtins
    • Axe
    • Execloader
    • Solidity
    • Leo
    • Paco
    • Concurrent-programs
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Parsing-primitives-seq

Parse-any

Parse any natural number.

Signature

(parse-any input) → (mv error? nat rest-input)

Arguments

input — Guard (nat-listp input).

Returns

error? — Type (maybe-msgp error?).

nat — Type (natp nat).

rest-input — Type (nat-listp rest-input).

This is the most basic parsing function: it parses any natural number (i.e. ABNF terminal). It is a building block of all the other parsing functions.

The parsed natural number is returned as the second result, so that the caller can examine it (e.g. to see that it is the expected one, or one of the expected ones). The only case in which this may fail is when the input list of natural number is empty; in this case, 0 is returned as second result, but it is irrelevant.

Definitions and Theorems

Function: parse-any

(defun parse-any (input)
  (declare (xargs :guard (nat-listp input)))
  (if (consp input)
      (mv nil (lnfix (car input))
          (nat-list-fix (cdr input)))
    (mv "Failed to parse any natural number: end of input reached."
        0 (nat-list-fix input))))

Theorem: maybe-msgp-of-parse-any.error?

(defthm maybe-msgp-of-parse-any.error?
  (b* (((mv ?error? acl2::?nat ?rest-input)
        (parse-any input)))
    (maybe-msgp error?))
  :rule-classes :rewrite)

Theorem: natp-of-parse-any.nat

(defthm natp-of-parse-any.nat
  (b* (((mv ?error? acl2::?nat ?rest-input)
        (parse-any input)))
    (natp nat))
  :rule-classes (:rewrite :type-prescription))

Theorem: nat-listp-of-parse-any.rest-input

(defthm nat-listp-of-parse-any.rest-input
  (b* (((mv ?error? acl2::?nat ?rest-input)
        (parse-any input)))
    (nat-listp rest-input))
  :rule-classes :rewrite)

Theorem: len-of-parse-any-linear-<=

(defthm len-of-parse-any-linear-<=
  (b* (((mv ?error? acl2::?nat ?rest-input)
        (parse-any input)))
    (<= (len rest-input) (len input)))
  :rule-classes :linear)

Theorem: len-of-parse-any-linear-<

(defthm len-of-parse-any-linear-<
  (b* (((mv ?error? acl2::?nat ?rest-input)
        (parse-any input)))
    (implies (not error?)
             (< (len rest-input) (len input))))
  :rule-classes :linear)

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

(defthm parse-any-of-nat-list-fix-input
  (equal (parse-any (nat-list-fix input))
         (parse-any input)))

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

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