• 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
            • Disambiguator
            • Abstract-syntax
              • Expr
              • Exprs/decls/stmts
              • Type-spec
              • Binop
                • Binopp
                • Binop-case
                • Binop-fix
                • Binop-kind
                • Binop-equiv
                • Binop-add
                • Binop-sub
                • Binop-shr
                • Binop-shl
                • Binop-rem
                • Binop-ne
                • Binop-mul
                • Binop-lt
                • Binop-logor
                • Binop-logand
                • Binop-le
                • Binop-gt
                • Binop-ge
                • Binop-eq
                • Binop-div
                • Binop-bitxor
                • Binop-bitior
                • Binop-bitand
                • Binop-asg-xor
                • Binop-asg-sub
                • Binop-asg-shr
                • Binop-asg-shl
                • Binop-asg-rem
                • Binop-asg-mul
                • Binop-asg-ior
                • Binop-asg-div
                • Binop-asg-and
                • Binop-asg-add
                • Binop-asg
              • Stmt
              • Amb-expr/tyname
              • Dirdeclor
              • Unop
              • Asm-stmt
              • Dec/oct/hex-const
              • Simple-escape
              • Attrib
              • Ident
              • Amb-decl/stmt
              • Dirabsdeclor
              • Decl-spec
              • Structdecl
              • Fundef
              • Transunit-ensemble
              • Asm-name-spec
              • Amb-declor/absdeclor
              • Param-declor
              • Declor
              • Type-qual
              • Absdeclor
              • Strunispec
              • Stor-spec
              • Keyword-uscores
              • Align-spec
              • Label
              • Expr-option
              • Spec/qual
              • Lsuffix
              • Hex-frac-const
              • Desiniter
              • Tyname
              • Iconst
              • Dirabsdeclor-option
              • Dec-frac-const
              • Dec-core-fconst
              • Extdecl
              • Amb?-declor/absdeclor
              • Isuffix
              • Initdeclor
              • Hex-core-fconst
              • Const-expr-option
              • Attrib-spec
              • Structdeclor
              • Escape
              • Decl
              • Amb?-expr/tyname
              • Ident-option
              • Bin-expo
              • Absdeclor-option
              • Statassert
              • Param-declon
              • Member-designor
              • Initer-option
              • Initer
              • Fsuffix
              • Enumspec
              • Declor-option
              • Const
              • Hex-quad
              • Eprefix
              • Const-expr
              • Block-item
              • Oct-escape
              • Inc/dec-op
              • Fun-spec
              • Dec-expo
              • Cprefix-option
              • Asm-name-spec-option
              • Amb?-decl/stmt
              • S-char
              • Isuffix-option
              • Genassoc
              • Fundef-option
              • Fsuffix-option
              • Fconst
              • Eprefix-option
              • Dec-expo-option
              • Cprefix
              • C-char
              • Type-spec-option
              • Sign-option
              • Iconst-option
              • Asm-output
              • Asm-input
              • Const-option
              • Usuffix
              • Univ-char-name
              • Transunit
              • Hprefix
              • Enumer
              • Designor
              • Attrib-name
              • Sign
              • Asm-qual
              • Typequal/attribspec
              • Dec-expo-prefix
              • Bin-expo-prefix
              • Stringlit
              • Cconst
              • Expr/tyname
              • Decl/stmt
              • Declor/absdeclor
              • Asm-clobber
              • Typequal/attribspec-list
              • Decl-spec-list
              • Stringlit-list
              • Spec/qual-list
              • Inc/dec-op-list
              • Desiniter-list
              • S-char-list
              • Param-declon-list
              • Decl-list
              • C-char-list
              • Block-item-list
              • Typequal/attribspec-list-list
              • Structdeclor-list
              • Structdecl-list
              • Initdeclor-list
              • Genassoc-list
              • Filepath-transunit-map
              • Extdecl-list
              • Expr-list
              • Enumer-list
              • Attrib-spec-list
              • Type-spec-list
              • Ident-list
              • Asm-qual-list
              • Asm-output-list
              • Asm-input-list
              • Asm-clobber-list
              • Stor-spec-list
              • Ident-set
              • Ident-option-set
              • Eprefix-option-list
              • Designor-list
              • Attrib-list
            • Parser
            • Validator
            • Printer
            • Formalized-subset
            • Mapping-to-language-definition
            • Input-files
            • Defpred
            • Output-files
            • Abstract-syntax-operations
            • Validation-information
            • Implementation-environments
            • Concrete-syntax
            • Unambiguity
            • Ascii-identifiers
            • Preprocessing
            • Abstraction-mapping
          • Atc
          • 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
  • Abstract-syntax

Binop

Fixtype of binary operators [C17:6.5.5-14] [C17:6.5.16] [C17:A.2.1].

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

Member Tags → Types
:mul → binop-mul
:div → binop-div
:rem → binop-rem
:add → binop-add
:sub → binop-sub
:shl → binop-shl
:shr → binop-shr
:lt → binop-lt
:gt → binop-gt
:le → binop-le
:ge → binop-ge
:eq → binop-eq
:ne → binop-ne
:bitand → binop-bitand
:bitxor → binop-bitxor
:bitior → binop-bitior
:logand → binop-logand
:logor → binop-logor
:asg → binop-asg
:asg-mul → binop-asg-mul
:asg-div → binop-asg-div
:asg-rem → binop-asg-rem
:asg-add → binop-asg-add
:asg-sub → binop-asg-sub
:asg-shl → binop-asg-shl
:asg-shr → binop-asg-shr
:asg-and → binop-asg-and
:asg-xor → binop-asg-xor
:asg-ior → binop-asg-ior

The grammar in [C17] does not have a nonterminal for binary operators. Instead, it has nonterminals for various kinds of binary expressions, used to capture certain precedence rules in the grammar itself. In our abstract syntax, for better factoring and orthogonality, it makes sense to introduce a fixtype for binary operators, and use it to define binary expressions as we do in expr. The binary operators are * (binary), /, %, + (binary), - (binary), <<, >>, <, >, <=, >=, ==, !=, & (binary), ^, |, &&, ||, =, *=, /=, %=, +=, -=, <<=, >>=, &=, ^=, and |=.

Subtopics

Binopp
Recognizer for binop structures.
Binop-case
Case macro for the different kinds of binop structures.
Binop-fix
Fixing function for binop structures.
Binop-kind
Get the kind (tag) of a binop structure.
Binop-equiv
Basic equivalence relation for binop structures.
Binop-add
Binop-sub
Binop-shr
Binop-shl
Binop-rem
Binop-ne
Binop-mul
Binop-lt
Binop-logor
Binop-logand
Binop-le
Binop-gt
Binop-ge
Binop-eq
Binop-div
Binop-bitxor
Binop-bitior
Binop-bitand
Binop-asg-xor
Binop-asg-sub
Binop-asg-shr
Binop-asg-shl
Binop-asg-rem
Binop-asg-mul
Binop-asg-ior
Binop-asg-div
Binop-asg-and
Binop-asg-add
Binop-asg