• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Zfc
    • Acre
    • Milawa
    • Smtlink
    • Abnf
    • Vwsim
    • Isar
    • Pfcs
      • Proof-support
      • Semantics
      • Lifting
      • R1cs-subset
      • Indexed-names
      • Well-formedness
      • Abstract-syntax
      • Concrete-syntax
        • Lexer
        • Grammar
        • Parser
          • Parse-operator-among
          • Parse-separator
          • Parse-operator
          • Parse-definition
          • Parse-relation-constraint
          • Parse-equality-constraint
          • Parse-*-comma-identifier
          • Parse-*-comma-expression
          • Parse-*-comma-constraint
          • Parse-system
          • Parse-identifier
          • Parse-numeral
          • Parse-constraint
          • Parse-*-definition
          • Parse-*-constraint
          • Parsize
          • Check-token-string
          • Check-token-root
          • Parse-token
          • Token-stringp
          • Token-rootp
          • Patbind-pok<
          • Parse-unary-minus-expression
          • Parse-multiplication-expression-rest
          • Parse-additive-expression-rest
          • Parse-primary-expression
          • Parse-multiplication-expression
          • Parse-additive-expression
          • Parse-expression
          • Patbind-pok
          • Perr
        • Tokenizer
      • R1cs-bridge
      • Parser-interface
    • Wp-gen
    • Dimacs-reader
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • C
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • Java
    • Taspi
    • Riscv
    • Bitcoin
    • Des
    • Ethereum
    • X86isa
    • Sha-2
    • Yul
    • Zcash
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Poseidon
    • Where-do-i-place-my-book
    • Axe
    • Aleo
    • Bigmems
    • Builtins
    • Execloader
    • Solidity
    • Paco
    • Concurrent-programs
    • Bls12-377-curves
  • Debugging
  • Std
  • Community
  • Proof-automation
  • ACL2
  • Macro-libraries
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Parser

Parse-operator-among

Parse an operator among the ones in a specified list.

Signature

(parse-operator-among operators token input) 
  → 
(mv tree next-token rest-input)

Arguments

operators — Guard (string-listp operators).

token — Guard (abnf::tree-optionp token).

input — Guard (abnf::tree-listp input).

Returns

tree — Type (abnf::tree-resultp tree).

next-token — Type (abnf::tree-optionp next-token).

rest-input — Type (abnf::tree-listp rest-input).

This is used to check the presence of an expected operator. We return it as a leaf tree as the first result, because this is how an operator occurs in the CSTs of the syntactic grammar. In other words, the operator rulename does not appear in any CST returned by the parser.

This is consistent with the fact that the rule operator does not appear on the right hand side of any rule other than the rule token.

Definitions and Theorems

Function: parse-operator-among-aux

(defun parse-operator-among-aux (nats strings)
  (declare (xargs :guard (and (nat-listp nats)
                              (string-listp strings))))
  (let ((__function__ 'parse-operator-among-aux))
    (declare (ignorable __function__))
    (and (consp strings)
         (or (equal (string=>nats (str-fix (car strings)))
                    (nat-list-fix nats))
             (parse-operator-among-aux nats (cdr strings))))))

Theorem: booleanp-of-parse-operator-among-aux

(defthm booleanp-of-parse-operator-among-aux
  (b* ((yes/no (parse-operator-among-aux nats strings)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: parse-operator-among-aux-of-nat-list-fix-nats

(defthm parse-operator-among-aux-of-nat-list-fix-nats
  (equal (parse-operator-among-aux (nat-list-fix nats)
                                   strings)
         (parse-operator-among-aux nats strings)))

Theorem: parse-operator-among-aux-nat-list-equiv-congruence-on-nats

(defthm parse-operator-among-aux-nat-list-equiv-congruence-on-nats
  (implies (acl2::nat-list-equiv nats nats-equiv)
           (equal (parse-operator-among-aux nats strings)
                  (parse-operator-among-aux nats-equiv strings)))
  :rule-classes :congruence)

Theorem: parse-operator-among-aux-of-string-list-fix-strings

(defthm parse-operator-among-aux-of-string-list-fix-strings
  (equal (parse-operator-among-aux nats (string-list-fix strings))
         (parse-operator-among-aux nats strings)))

Theorem: parse-operator-among-aux-string-list-equiv-congruence-on-strings

(defthm
   parse-operator-among-aux-string-list-equiv-congruence-on-strings
  (implies (str::string-list-equiv strings strings-equiv)
           (equal (parse-operator-among-aux nats strings)
                  (parse-operator-among-aux nats strings-equiv)))
  :rule-classes :congruence)

Function: parse-operator-among

(defun parse-operator-among (operators token input)
  (declare (xargs :guard (and (string-listp operators)
                              (abnf::tree-optionp token)
                              (abnf::tree-listp input))))
  (declare (xargs :guard (subsetp-equal operators *operators*)))
  (let ((__function__ 'parse-operator-among))
    (declare (ignorable __function__))
    (b* ((tree (check-token-root "operator" token))
         ((when (reserrp tree))
          (perr (reserrf-push tree)))
         (fringe (abnf::tree->string tree))
         ((unless (nat-listp fringe))
          (perr :impossible))
         ((unless (parse-operator-among-aux fringe operators))
          (perr (list :required
                      :one-of (string-list-fix operators)
                      :found tree)))
         (tree (abnf::tree-leafterm fringe))
         ((mv token input) (parse-token input)))
      (mv tree token input))))

Theorem: tree-resultp-of-parse-operator-among.tree

(defthm tree-resultp-of-parse-operator-among.tree
  (b* (((mv ?tree ?next-token ?rest-input)
        (parse-operator-among operators token input)))
    (abnf::tree-resultp tree))
  :rule-classes :rewrite)

Theorem: tree-optionp-of-parse-operator-among.next-token

(defthm tree-optionp-of-parse-operator-among.next-token
  (b* (((mv ?tree ?next-token ?rest-input)
        (parse-operator-among operators token input)))
    (abnf::tree-optionp next-token))
  :rule-classes :rewrite)

Theorem: tree-listp-of-parse-operator-among.rest-input

(defthm tree-listp-of-parse-operator-among.rest-input
  (b* (((mv ?tree ?next-token ?rest-input)
        (parse-operator-among operators token input)))
    (abnf::tree-listp rest-input))
  :rule-classes :rewrite)

Theorem: parsize-of-parse-operator-among-<=

(defthm parsize-of-parse-operator-among-<=
  (b* (((mv ?tree ?next-token ?rest-input)
        (parse-operator-among operators token input)))
    (<= (parsize next-token rest-input)
        (parsize token input)))
  :rule-classes :linear)

Theorem: parsize-of-parse-operator-among-<

(defthm parsize-of-parse-operator-among-<
  (b* (((mv ?tree ?next-token ?rest-input)
        (parse-operator-among operators token input)))
    (implies (not (reserrp tree))
             (< (parsize next-token rest-input)
                (parsize token input))))
  :rule-classes :linear)

Theorem: len-of-parse-operator-among-<=

(defthm len-of-parse-operator-among-<=
  (b* (((mv ?tree ?next-token ?rest-input)
        (parse-operator-among operators token input)))
    (<= (len rest-input) (len input)))
  :rule-classes :linear)

Theorem: len-of-parse-operator-among-<

(defthm len-of-parse-operator-among-<
  (b* (((mv ?tree ?next-token ?rest-input)
        (parse-operator-among operators token input)))
    (implies (and (not (reserrp tree)) next-token)
             (< (len rest-input) (len input))))
  :rule-classes :linear)

Theorem: parse-operator-among-of-string-list-fix-operators

(defthm parse-operator-among-of-string-list-fix-operators
  (equal (parse-operator-among (string-list-fix operators)
                               token input)
         (parse-operator-among operators token input)))

Theorem: parse-operator-among-string-list-equiv-congruence-on-operators

(defthm
     parse-operator-among-string-list-equiv-congruence-on-operators
  (implies
       (str::string-list-equiv operators operators-equiv)
       (equal (parse-operator-among operators token input)
              (parse-operator-among operators-equiv token input)))
  :rule-classes :congruence)

Theorem: parse-operator-among-of-tree-option-fix-token

(defthm parse-operator-among-of-tree-option-fix-token
  (equal
       (parse-operator-among operators (abnf::tree-option-fix token)
                             input)
       (parse-operator-among operators token input)))

Theorem: parse-operator-among-tree-option-equiv-congruence-on-token

(defthm parse-operator-among-tree-option-equiv-congruence-on-token
  (implies
       (abnf::tree-option-equiv token token-equiv)
       (equal (parse-operator-among operators token input)
              (parse-operator-among operators token-equiv input)))
  :rule-classes :congruence)

Theorem: parse-operator-among-of-tree-list-fix-input

(defthm parse-operator-among-of-tree-list-fix-input
  (equal (parse-operator-among operators
                               token (abnf::tree-list-fix input))
         (parse-operator-among operators token input)))

Theorem: parse-operator-among-tree-list-equiv-congruence-on-input

(defthm parse-operator-among-tree-list-equiv-congruence-on-input
  (implies
       (abnf::tree-list-equiv input input-equiv)
       (equal (parse-operator-among operators token input)
              (parse-operator-among operators token input-equiv)))
  :rule-classes :congruence)