Return the unique value associated to a member name in a JSON object, if the object has a member with that name.
(object-member-value? name object) → 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.
Function:
(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:
(defthm value-optionp-of-object-member-value? (b* ((value? (object-member-value? name object))) (value-optionp value?)) :rule-classes :rewrite)