• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Acre
    • Milawa
    • Smtlink
    • Aleobft
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
      • Proof-support
      • Abstract-syntax
      • R1cs-subset
      • Semantics
      • Abstract-syntax-operations
      • Indexed-names
      • Well-formedness
      • Concrete-syntax
        • Lexer
        • Grammar
        • Parser
          • 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-primary-expression
          • Parse-pfcs-integer
          • Parse-constraint
          • Parse-*-definition
          • Parse-*-constraint
          • Parse-expression
          • Parsize
          • Check-token-string
          • Check-token-root
          • Parse-token
          • Token-stringp
          • Token-rootp
          • Patbind-pok<
          • Parse-multiplication-expression-rest
          • Parse-addition-expression-rest
          • Parse-multiplication-expression
          • Parse-addition-expression
          • Patbind-pok
          • Perr
        • Abnf-extensions
        • Tokenizer
      • R1cs-bridge
      • Parser-interface
    • 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

• Parser

Parse-separator

Parse a specified separator.

Signature

(parse-separator separator token input) 
  → 
(mv tree next-token rest-input)

Arguments

separator — Guard (stringp separator).

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 separator. We return it as a leaf tree as the first result, because this is how an separator occurs in the CSTs of the syntactic grammar. In other words, the separator rulename does not appear in any CST returned by the parser.

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

Definitions and Theorems

Function: parse-separator

(defun parse-separator (separator token input)
 (declare (xargs :guard (and (stringp separator)
                             (abnf::tree-optionp token)
                             (abnf::tree-listp input))))
 (declare (xargs :guard (member-equal separator *separators*)))
 (let ((__function__ 'parse-separator))
   (declare (ignorable __function__))
   (b*
    ((tree (check-token-root "separator" token))
     ((when (reserrp tree))
      (perr (reserrf-push tree)))
     ((unless (equal (abnf::tree->string tree)
                     (string=>nats (str-fix separator))))
      (perr (list :required (str-fix separator)
                  :found (abnf::tree-option-fix token))))
     (tree (abnf::tree-leafterm (string=>nats (str-fix separator))))
     ((mv token input) (parse-token input)))
    (mv tree token input))))

Theorem: tree-resultp-of-parse-separator.tree

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

Theorem: tree-optionp-of-parse-separator.next-token

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

Theorem: tree-listp-of-parse-separator.rest-input

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

Theorem: parsize-of-parse-separator-<=

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

Theorem: parsize-of-parse-separator-<

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

Theorem: len-of-parse-separator-<=

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

Theorem: len-of-parse-separator-<

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

Theorem: parse-separator-of-str-fix-separator

(defthm parse-separator-of-str-fix-separator
  (equal (parse-separator (str-fix separator)
                          token input)
         (parse-separator separator token input)))

Theorem: parse-separator-streqv-congruence-on-separator

(defthm parse-separator-streqv-congruence-on-separator
  (implies (acl2::streqv separator separator-equiv)
           (equal (parse-separator separator token input)
                  (parse-separator separator-equiv token input)))
  :rule-classes :congruence)

Theorem: parse-separator-of-tree-option-fix-token

(defthm parse-separator-of-tree-option-fix-token
  (equal (parse-separator separator (abnf::tree-option-fix token)
                          input)
         (parse-separator separator token input)))

Theorem: parse-separator-tree-option-equiv-congruence-on-token

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

Theorem: parse-separator-of-tree-list-fix-input

(defthm parse-separator-of-tree-list-fix-input
  (equal (parse-separator separator
                          token (abnf::tree-list-fix input))
         (parse-separator separator token input)))

Theorem: parse-separator-tree-list-equiv-congruence-on-input

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