• 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-*-import-declaration

Parse a *import-declaration.

Signature

(parse-*-import-declaration token input) 
  → 
(mv trees next-token rest-input)

Arguments

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

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

Returns

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

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

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

Definitions and Theorems

Function: parse-*-import-declaration

(defun parse-*-import-declaration (token input)
  (declare (xargs :guard (and (abnf::tree-optionp token)
                              (abnf::tree-listp input))))
  (let ((__function__ 'parse-*-import-declaration))
    (declare (ignorable __function__))
    (abnf::tree-option-case
         token :none
         (mv nil nil (abnf::tree-list-fix input))
         :some
         (b* (((mv tree1 token1 input1)
               (parse-import-declaration token input))
              ((when (reserrp tree1))
               (mv nil (abnf::tree-option-fix token)
                   (abnf::tree-list-fix input)))
              ((pok trees)
               (parse-*-import-declaration token1 input1)))
           (mv (cons tree1 trees) token input)))))

Theorem: tree-list-resultp-of-parse-*-import-declaration.trees

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

Theorem: tree-optionp-of-parse-*-import-declaration.next-token

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

Theorem: tree-listp-of-parse-*-import-declaration.rest-input

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

Theorem: parsize-of-parse-*-import-declaration-<=

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

Theorem: parse-*-import-declaration-of-tree-option-fix-token

(defthm parse-*-import-declaration-of-tree-option-fix-token
  (equal (parse-*-import-declaration (abnf::tree-option-fix token)
                                     input)
         (parse-*-import-declaration token input)))

Theorem: parse-*-import-declaration-tree-option-equiv-congruence-on-token

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

Theorem: parse-*-import-declaration-of-tree-list-fix-input

(defthm parse-*-import-declaration-of-tree-list-fix-input
 (equal
      (parse-*-import-declaration token (abnf::tree-list-fix input))
      (parse-*-import-declaration token input)))

Theorem: parse-*-import-declaration-tree-list-equiv-congruence-on-input

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