• 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
        • Bv
        • Imp-language
        • Event-macros
        • Java
          • Atj
            • Atj-implementation
              • Atj-types
              • Atj-java-primitive-array-model
              • Atj-java-abstract-syntax
              • Atj-input-processing
              • Atj-java-pretty-printer
              • Atj-code-generation
                • Atj-gen-test-method
                • Atj-shallow-code-generation
                • Atj-common-code-generation
                • Atj-shallow-quoted-constant-generation
                  • Atj-qconstants-p
                    • Atj-qconstants
                    • Make-atj-qconstants
                    • Change-atj-qconstants
                    • Honsed-atj-qconstants
                    • Make-honsed-atj-qconstants
                    • Atj-qconstants->symbols
                    • Atj-qconstants->strings
                    • Atj-qconstants->rationals
                    • Atj-qconstants->pairs
                    • Atj-qconstants->numbers
                    • Atj-qconstants->next-index
                    • Atj-qconstants->integers
                    • Atj-qconstants->chars
                  • Atj-gen-shallow-symbol
                  • Atj-gen-shallow-cons-field-name
                  • Atj-gen-shallow-symbol-field-name
                  • Atj-add-qconstant
                  • Atj-add-qconstants-in-term
                  • Atj-gen-shallow-symbol-field
                  • Atj-gen-shallow-rational-id-part
                  • Atj-gen-shallow-number-id-part
                  • Atj-gen-shallow-number-field
                  • Atj-gen-shallow-value
                  • Atj-gen-shallow-cons-fields
                  • Atj-gen-shallow-cons-field
                  • Atj-gen-shallow-string
                  • Atj-gen-shallow-integer-id-part
                  • Atj-gen-shallow-string-field
                  • Atj-gen-shallow-number-field-name
                  • Atj-gen-shallow-char-field
                  • Atj-gen-shallow-char
                  • Atj-gen-shallow-string-field-name
                  • Atj-gen-shallow-cons
                  • Atj-gen-shallow-char-field-name
                  • Atj-gen-shallow-symbol-fields
                  • Atj-gen-shallow-string-fields
                  • Atj-gen-shallow-number-fields
                  • Atj-gen-shallow-number
                  • Atj-gen-shallow-char-fields
                • Atj-pre-translation
                • Atj-gen-everything
                • Atj-name-translation
                • Atj-gen-test-cunit
                • Atj-gen-test-class
                • Atj-gen-main-file
                • Atj-post-translation
                • Atj-deep-code-generation
                • Atj-gen-test-methods
                • Atj-gen-test-file
                • Atj-gen-env-file
                • Atj-gen-output-subdir
              • Atj-java-primitives
              • Atj-java-primitive-arrays
              • Atj-type-macros
              • Atj-java-syntax-operations
              • Atj-fn
              • Atj-library-extensions
              • Atj-java-input-types
              • Atj-test-structures
              • Aij-notions
              • Atj-macro-definition
            • Atj-tutorial
          • Aij
          • Language
        • 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
  • Atj-shallow-quoted-constant-generation

Atj-qconstants-p

Recognize a structured collection of quoted constants.

(atj-qconstants-p x) is a std::defaggregate of the following fields.

  • integers — Invariant (and (integer-listp integers) (no-duplicatesp integers)).
  • rationals — Invariant (and (rational-listp rationals) (no-duplicatesp rationals)).
  • numbers — Invariant (and (acl2-number-listp numbers) (no-duplicatesp numbers)).
  • chars — Invariant (and (character-listp chars) (no-duplicatesp chars)).
  • strings — Invariant (and (string-listp strings) (no-duplicatesp-equal strings)).
  • symbols — Invariant (and (symbol-listp symbols) (no-duplicatesp-eq symbols)).
  • pairs — Invariant (cons-pos-alistp pairs).
  • next-index — Invariant (posp next-index).

Source link: atj-qconstants-p

As we collect quoted constants for the purposes described here, we store their values (without quotes) in a record where they are partitioned into: (i) integers; (ii) other (i.e. non-integer) rationals; (iii) other (i.e. non-rational) numbers; (iv) characters; (v) strings; (vi) symbols; (vii) cons pairs. The first six are duplicate-free lists of appropriate types. The seventh is an alist from the pairs to positive integer indices: the first collected pair gets index 1, the second one gets index 2, and so on; we organize this as an alist instead of a list so that the indices are explicit and so that we can more easily optimize this with a fast alist in the future. The index for the next cons pair is stored in this record. The use of the indices is explained in atj-gen-shallow-cons-field-name. The alist has unique keys, by construction.

Subtopics

Atj-qconstants
Raw constructor for atj-qconstants-p structures.
Make-atj-qconstants
Constructor macro for atj-qconstants-p structures.
Change-atj-qconstants
A copying macro that lets you create new atj-qconstants-p structures, based on existing structures.
Honsed-atj-qconstants
Raw constructor for honsed atj-qconstants-p structures.
Make-honsed-atj-qconstants
Constructor macro for honsed atj-qconstants-p structures.
Atj-qconstants->symbols
Access the symbols field of a atj-qconstants-p structure.
Atj-qconstants->strings
Access the strings field of a atj-qconstants-p structure.
Atj-qconstants->rationals
Access the rationals field of a atj-qconstants-p structure.
Atj-qconstants->pairs
Access the pairs field of a atj-qconstants-p structure.
Atj-qconstants->numbers
Access the numbers field of a atj-qconstants-p structure.
Atj-qconstants->next-index
Access the next-index field of a atj-qconstants-p structure.
Atj-qconstants->integers
Access the integers field of a atj-qconstants-p structure.
Atj-qconstants->chars
Access the chars field of a atj-qconstants-p structure.