• 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-postfix-expression

Parse a postfix-expression.

Signature

(parse-postfix-expression 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).

A postfix expression is either a primary expression or something (struct-component-expression or operator-call) that has a postfix expression followed by a dot (.) and an identifier and in the case of operator-call, a parenthesized list of arguments.

We first try to parse a primary expression. If there is no primary expression here, there cannot be a postfix expression, since every postfix expression bottoms out in a primary expression on the left.

After finding a primary expression, we wrap it with a postfix expression layer and pass it to parse-postfix-expression-rest, which looks for dot and indentifier recursively.