		Search-engine friendly clone of the ACL2 documentation.

Operations

Object-member-value

Return the unique value associated to a member name in a JSON object.

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

Sometimes a JSON object is expected to have exactly one member with a given name. In such cases, this operation can be used, instead of the more general object-member-values and object-member-value?. This operation conservatively checks that there is indeed exactly one member in the JSON object with the given name, returning the associated value. If the conservative check fails, 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)
     (prog2$
      (raise
       "The JSON object ~x0 ~
                                         has no member with name ~x1."
       object name)
      (irr-value)))
    ((= (len values) 1) (car values))
    (t
     (prog2$
      (raise
       "The JSON object ~x0 ~
                             has multiple members with name ~x1."
       object name)
      (irr-value)))))))

Theorem: valuep-of-object-member-value

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