• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Zfc
    • Acre
    • Milawa
    • Smtlink
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • C
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • Java
    • Riscv
    • Taspi
    • 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
      • 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-group-coordinate

Parse a group-coordinate.

Signature

(parse-group-coordinate 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-group-coordinate

(defun parse-group-coordinate (token input)
 (declare (xargs :guard (and (abnf::tree-optionp token)
                             (abnf::tree-listp input))))
 (let ((__function__ 'parse-group-coordinate))
  (declare (ignorable __function__))
  (cond
   ((token-stringp "+" token)
    (b* (((pok tree)
          (parse-symbol "+" token input)))
      (mv (abnf-tree-wrap tree "group-coordinate")
          token input)))
   ((token-stringp "-" token)
    (b*
     (((pok< tree)
       (parse-symbol "-" token input))
      ((when (null token))
       (mv (abnf-tree-wrap tree "group-coordinate")
           token input))
      ((mv tree1 next1 input1)
       (parse-numeral token input))
      ((unless (reserrp tree1))
       (mv
        (abnf::make-tree-nonleaf
         :rulename? (abnf::rulename "group-coordinate")
         :branches
         (list
          (list (abnf::make-tree-nonleaf
                     :rulename? nil
                     :branches
                     (list (list (abnf::make-tree-nonleaf
                                      :rulename? nil
                                      :branches (list (list tree))))
                           (list tree1))))))
        next1 input1)))
     (mv (abnf-tree-wrap tree "group-coordinate")
         token input)))
   ((token-stringp "_" token)
    (b* (((pok tree)
          (parse-symbol "_" token input)))
      (mv (abnf-tree-wrap tree "group-coordinate")
          token input)))
   (t
    (b* (((pok tree)
          (parse-numeral token input)))
     (mv
      (abnf::make-tree-nonleaf
       :rulename? (abnf::rulename "group-coordinate")
       :branches
       (list
        (list
         (abnf::make-tree-nonleaf
             :rulename? nil
             :branches
             (list (list (abnf::make-tree-nonleaf :rulename? nil
                                                  :branches (list)))
                   (list tree))))))
      token input))))))

Theorem: tree-resultp-of-parse-group-coordinate.tree

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

Theorem: tree-optionp-of-parse-group-coordinate.next-token

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

Theorem: tree-listp-of-parse-group-coordinate.rest-input

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

Theorem: parsize-of-parse-group-coordinate-<=

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

Theorem: parsize-of-parse-group-coordinate-<

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

Theorem: parse-group-coordinate-of-tree-option-fix-token

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

Theorem: parse-group-coordinate-tree-option-equiv-congruence-on-token

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

Theorem: parse-group-coordinate-of-tree-list-fix-input

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

Theorem: parse-group-coordinate-tree-list-equiv-congruence-on-input

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