• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
          • Syntax-for-tools
          • Atc
            • Atc-implementation
              • Atc-abstract-syntax
              • Atc-pretty-printer
                • Pprint-expressions
                • Pprint-expr
                • Expr-grade
                  • Expr-grade-fix
                  • Expr-grade-case
                  • Expr-gradep
                  • Expr-grade-equiv
                  • Expr-grade-kind
                  • Expr-grade-xor
                  • Expr-grade-unary
                  • Expr-grade-top
                  • Expr-grade-shift
                  • Expr-grade-relational
                  • Expr-grade-primary
                  • Expr-grade-postfix
                  • Expr-grade-multiplicative
                  • Expr-grade-logical-or
                  • Expr-grade-logical-and
                  • Expr-grade-ior
                  • Expr-grade-equality
                  • Expr-grade-conditional
                  • Expr-grade-cast
                  • Expr-grade-assignment
                  • Expr-grade-and
                  • Expr-grade-additive
                • Pprint-obj-declor
                • Expr-grade-<=
                • Binop-expected-grades
                • Pprint-obj-declon
                • Expr->grade
                • Pprint-tyspecseq
                • Pprint-tag-declon
                • Pprint-struct-declon-list
                • Pprint-fun-declor
                • Pprint-file
                • Pprint-stmt
                • Pprint-struct-declon
                • Pprint-obj-adeclor
                • Pprint-initer
                • Pprint-fun-declon
                • Pprint-indent
                • Pprint-hex-const
                • Pprint-fileset
                • Pprint-dec-const
                • Pprinted-lines-to-file
                • Pprint-tyname
                • Pprint-param-declon-list
                • Pprint-oct-const
                • Pprint-iconst-length
                • Pprint-iconst
                • Pprint-const
                • Expr-grade-index
                • Pprint-param-declon
                • Pprint-label
                • Pprint-ident-list
                • Pprint-binop
                • Pprint-fundef
                • Pprint-file-to-filesystem
                • Pprint-ext-declon-list
                • Pprint-unop
                • Pprint-line
                • Pprint-ident
                • Pprint-ext-declon
                • Pprint-comma-sep
                • Pprint-transunit
                • Pprint-one-line
                • Pprinted-lines-to-channel
                • Pprint-one-line-blank
                • Pprint-line-blank
              • Atc-event-and-code-generation
              • Fty-pseudo-term-utilities
              • Atc-term-recognizers
              • Atc-input-processing
              • Atc-shallow-embedding
              • Atc-process-inputs-and-gen-everything
              • Atc-table
              • Atc-fn
              • Atc-pretty-printing-options
              • Atc-types
              • Atc-macro-definition
            • Atc-tutorial
          • Language
          • Representation
          • Transformation-tools
          • Insertion-sort
          • Pack
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
        • Zcash
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Cryptography
        • Number-theory
        • Lists-light
        • Axe
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Atc-pretty-printer

Expr-grade

Grades of expressions.

This is a tagged union type, introduced by fty::deftagsum.

Member Tags → Types
:top → expr-grade-top
:assignment → expr-grade-assignment
:conditional → expr-grade-conditional
:logical-or → expr-grade-logical-or
:logical-and → expr-grade-logical-and
:ior → expr-grade-ior
:xor → expr-grade-xor
:and → expr-grade-and
:equality → expr-grade-equality
:relational → expr-grade-relational
:shift → expr-grade-shift
:additive → expr-grade-additive
:multiplicative → expr-grade-multiplicative
:cast → expr-grade-cast
:unary → expr-grade-unary
:postfix → expr-grade-postfix
:primary → expr-grade-primary

See pprint-expressions for background.

The grade :top corresponds to the nonterminal expression; the grade :ior corresponds to the nonterminal inclusive-OR-expression; the grade :xor corresponds to the nonterminal exclusive-OR-expression; each of the other grades, :<grade>, corresponds to the nonterminal <grade>-expression.

We stop at primary expressions: we do not need grades for identifier, constant, etc.

Subtopics

Expr-grade-fix
Fixing function for expr-grade structures.
Expr-grade-case
Case macro for the different kinds of expr-grade structures.
Expr-gradep
Recognizer for expr-grade structures.
Expr-grade-equiv
Basic equivalence relation for expr-grade structures.
Expr-grade-kind
Get the kind (tag) of a expr-grade structure.
Expr-grade-xor
Expr-grade-unary
Expr-grade-top
Expr-grade-shift
Expr-grade-relational
Expr-grade-primary
Expr-grade-postfix
Expr-grade-multiplicative
Expr-grade-logical-or
Expr-grade-logical-and
Expr-grade-ior
Expr-grade-equality
Expr-grade-conditional
Expr-grade-cast
Expr-grade-assignment
Expr-grade-and
Expr-grade-additive