Return the unique value associated to a member name in a JSON object.
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.
(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) (ec-call (value-fix :irrelevant)))) ((= (len values) 1) (car values)) (t (prog2$ (raise "The JSON object ~x0 ~ has multiple members with name ~x1." object name) (ec-call (value-fix :irrelevant))))))))
(defthm valuep-of-object-member-value (b* ((value (object-member-value name object))) (valuep value)) :rule-classes :rewrite)