		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax

Object-member-value?

Return the unique value associated to a member name in a JSON object, if the object has a member with that name.

Signature
(object-member-value? name object) → value?
Arguments: name — Guard (stringp name).; object — Guard (valuep object).
Returns: value? — Type (maybe-valuep value?).

While object-member-values is a general operation that never fails, in some cases a JSON object is expected to have no duplicate member names; indeed, the JSON standards recommend the absence of duplicate member names. In such cases, then, attempting to retrieve the value associated to a member name should result in at most one value. This operation can be used in these cases: it returns an optional value (i.e. a value or no value), but it conservatively checks that there are no other members with the same name; it does so by ensuring that the list returned by object-member-values contains at most one element. If there are duplicate member names, an error occurs.

Definitions and Theorems

Function: object-member-value?

(defun
 object-member-value? (name object)
 (declare (xargs :guard (and (stringp name) (valuep object))))
 (declare (xargs :guard (value-case object :object)))
 (let
  ((__function__ 'object-member-value?))
  (declare (ignorable __function__))
  (b*
   ((values (object-member-values name object)))
   (cond
    ((endp values) nil)
    ((= (len values) 1) (car values))
    (t
     (raise
      "The JSON object ~x0 ~
                     has multiple members with name ~x1."
      object name))))))

Theorem: maybe-valuep-of-object-member-value?

(defthm maybe-valuep-of-object-member-value?
        (b* ((value? (object-member-value? name object)))
            (maybe-valuep value?))
        :rule-classes :rewrite)