• 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
      • Soft
      • Bv
      • Imp-language
      • C
      • Event-macros
      • Java
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
        • Parser-output-to-values
        • Values
        • Syntax
        • Patbind-pattern
        • Operations
          • Object-member-values
          • Object-member-value?
          • Object-member-value
          • Object-has-member-p
      • Syntheto
      • File-io-light
      • Number-theory
      • Cryptography
      • Lists-light
      • Builtins
      • Axe
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Operations

Object-member-values

Retrieve the values associated to a member name in a JSON object.

Signature

(object-member-values name object) → values

Arguments

name — Guard (stringp name).

object — Guard (valuep object).

Returns

values — Type (value-listp values).

As mentioned in values, our model of JSON values does not assume or enforce that JSON objects have members with unique names. Accordingly, given a member name, there may be 0, 1, or more values associated with that name. This function returns the list of such values, in the order in which they occur in the object; member order is captured and significant in our JSON values.

Note that if the JSON object has two duplicate members (meaning not just the same name, but also the same value), the list returned here has correspondingly duplicate values.

Definitions and Theorems

Function: object-member-values-aux

(defun object-member-values-aux (name members)
  (declare (xargs :guard (and (stringp name)
                              (member-listp members))))
  (let ((__function__ 'object-member-values-aux))
    (declare (ignorable __function__))
    (cond ((endp members) nil)
          ((equal name (member->name (car members)))
           (cons (member->value (car members))
                 (object-member-values-aux name (cdr members))))
          (t (object-member-values-aux name (cdr members))))))

Theorem: value-listp-of-object-member-values-aux

(defthm value-listp-of-object-member-values-aux
  (b* ((values (object-member-values-aux name members)))
    (value-listp values))
  :rule-classes :rewrite)

Function: object-member-values

(defun object-member-values (name object)
  (declare (xargs :guard (and (stringp name) (valuep object))))
  (declare (xargs :guard (value-case object :object)))
  (let ((__function__ 'object-member-values))
    (declare (ignorable __function__))
    (object-member-values-aux name (value-object->members object))))

Theorem: value-listp-of-object-member-values

(defthm value-listp-of-object-member-values
  (b* ((values (object-member-values name object)))
    (value-listp values))
  :rule-classes :rewrite)