• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Zfc
    • Acre
    • Milawa
    • Smtlink
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • C
    • Proof-checker-array
    • Soft
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Ethereum
    • Leftist-trees
    • Java
    • Riscv
    • Taspi
    • Bitcoin
    • Zcash
    • Des
    • X86isa
    • Sha-2
    • Yul
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Axe
    • Poseidon
    • Where-do-i-place-my-book
    • Aleo
      • Aleobft
      • Aleovm
      • Leo
        • Grammar
        • Early-version
          • Json2ast
          • Testing
          • Definition
            • Flattening
            • Abstract-syntax
            • Dynamic-semantics
            • Compilation
            • Static-semantics
            • Concrete-syntax
              • Pretty-printer
              • Grammar
              • Lexing-and-parsing
                • Lexer
                • Parser
                  • Parse-symbol-among
                  • Parse-keyword
                  • Parse-named-primitive-type
                  • Parse-rest-of-struct-component-expression
                  • Parse-rest-of-tuple-component-expression
                  • Parse-transition-declaration
                  • Parse-named-type-as-identifier-?-dot-record
                  • Parse-named-type-as-locator-?-dot-record
                  • Parse-assert-not-equal-call
                  • Parse-symbol
                  • Parse-struct-component-declarations
                  • Parse-assert-equal-call
                  • Parse-transition-or-function-declaration
                  • Parse-string-literal
                  • Parse-group-coordinate
                  • Parse-function-declaration
                  • Parse-finalizer
                  • Parse-*-comma-struct-component-declaration
                  • Parse-increment-statement
                  • Parse-function-parameter
                  • Parse-decrement-statement
                  • Parse-struct-component-declaration
                  • Parse-variable-declaration
                  • Parse-mapping-declaration
                  • Parse-function-parameters
                  • Parse-constant-declaration
                  • Parse-assert-call
                  • Parse-*-comma-function-parameter
                  • Parse-program-declaration
                  • Parse-affine-group-literal
                  • Parse-variable-or-free-constant
                  • Parse-struct-declaration
                  • Parse-record-declaration
                  • Parse-finalize-statement
                  • Parse-associated-constant
                  • Parse-numeral
                  • Parse-import-declaration
                  • Parse-identifier
                  • Parse-console-statement
                  • Parse-annotation
                  • Parse-return-statement
                  • Parse-program-item
                  • Parse-assignment-operator
                  • Parse-*-import-declaration
                  • Parse-unit-expression
                  • Parse-named-type
                  • Parse-console-call
                  • Parse-*-comma-natural
                  • Parse-program-id
                  • Parse-atomic-literal
                  • Parse-?-output-type
                  • Parse-unit-type
                  • Parse-*-program-item
                  • Parse-locator
                  • Parse-?-finalizer
                  • Parse-*-annotation
                  • Parse-primary-expression
                  • Parse-literal
                  • Parse-?-comma
                  • Parse-file
                  • Parsize
                  • Check-token-string
                  • Check-token-root
                  • Parse-postfix-expression-rest
                  • Parse-postfix-expression
                  • Parse-token
                  • Token-stringp
                  • Token-rootp
                  • Patbind-pok<
                  • Parse-rest-of-operator-call
                  • Parse-exclusive-disjunctive-expression-rest
                  • Parse-conditional-disjunctive-expression-rest
                  • Parse-conditional-conjunctive-expression-rest
                  • Parse-shift-expression-rest
                  • Parse-multiplicative-expression-rest
                  • Parse-disjunctive-expression-rest
                  • Parse-conjunctive-expression-rest
                  • Parse-additive-expression-rest
                  • Parse-*-statement
                  • Parse-*-comma-type
                  • Parse-*-comma-struct-component-initializer
                  • Parse-*-comma-expression
                  • Parse-unary-expression
                  • Parse-tuple-expression
                  • Parse-struct-expression
                  • Parse-struct-component-initializer
                  • Parse-static-function-call
                  • Parse-shift-expression
                  • Parse-ordering-expression
                  • Parse-multiplicative-expression
                  • Parse-function-arguments
                  • Parse-free-function-call
                  • Parse-exponential-expression
                  • Parse-exclusive-disjunctive-expression
                  • Parse-equality-expression
                  • Parse-disjunctive-expression
                  • Parse-conjunctive-expression
                  • Parse-conditional-ternary-expression
                  • Parse-conditional-statement
                  • Parse-conditional-disjunctive-expression
                  • Parse-conditional-conjunctive-expression
                  • Parse-binary-expression
                  • Parse-additive-expression
                  • Parse-type
                  • Parse-tuple-type
                  • Parse-statement
                  • Parse-loop-statement
                  • Parse-expression
                  • Parse-branch
                  • Parse-block
                  • Patbind-pok
                  • Perr
                • Token-fringe
                • Longest-lexp
                • Parser-interface
                • Grammar-lexp
                • Identifier-lexp
                • Output-file-parsep
                • Input-file-parsep
                • File-lex-parse-p
                • Filter-tokens
                • Lexp
                • File-parsep
                • Input-parser
                • Output-file-lex-parse-p
                • Input-file-lex-parse-p
                • Parser-abstractor-interface
                • Identifier-abnf-stringp
                • Symbol-abnf-stringp
                • Keyword-abnf-stringp
                • Output-parser
                • Tokenizer
              • Input-pretty-printer
              • Output-pretty-printer
              • Unicode-characters
              • Concrete-syntax-trees
              • Symbols
              • Keywords
    • Bigmems
    • Builtins
    • Execloader
    • Solidity
    • Paco
    • Concurrent-programs
    • Bls12-377-curves
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Parser

Parse-?-finalizer

Parse a [ finalizer ].

Signature

(parse-?-finalizer token input) 
  → 
(mv tree next-token rest-input)

Arguments

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).

Definitions and Theorems

Function: parse-?-finalizer

(defun parse-?-finalizer (token input)
  (declare (xargs :guard (and (abnf::tree-optionp token)
                              (abnf::tree-listp input))))
  (let ((__function__ 'parse-?-finalizer))
    (declare (ignorable __function__))
    (b* (((mv tree token1 input1)
          (parse-finalizer token input))
         ((when (not (reserrp tree)))
          (mv (abnf::make-tree-nonleaf :rulename? nil
                                       :branches (list (list tree)))
              token1 input1)))
      (mv (abnf::make-tree-nonleaf :rulename? nil
                                   :branches nil)
          (abnf::tree-option-fix token)
          (abnf::tree-list-fix input)))))

Theorem: tree-resultp-of-parse-?-finalizer.tree

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

Theorem: tree-optionp-of-parse-?-finalizer.next-token

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

Theorem: tree-listp-of-parse-?-finalizer.rest-input

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

Theorem: parsize-of-parse-?-finalizer

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

Theorem: parse-?-finalizer-of-tree-option-fix-token

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

Theorem: parse-?-finalizer-tree-option-equiv-congruence-on-token

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

Theorem: parse-?-finalizer-of-tree-list-fix-input

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

Theorem: parse-?-finalizer-tree-list-equiv-congruence-on-input

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