		Search-engine friendly clone of the ACL2 documentation.

Json2ast

J2f-console-log

Converts a json-member console log statement to a leo::statement of kind :console

Signature
(j2f-console-log json-console-log) → (mv erp leo-console-log)
Arguments: json-console-log — Guard (json::memberp json-console-log).
Returns: erp — Type (booleanp erp).; leo-console-log — Type (consolep leo-console-log).

Definitions and Theorems

Function: j2f-console-log

(defun j2f-console-log (json-console-log)
 (declare (xargs :guard (json::memberp json-console-log)))
 (let ((__function__ 'j2f-console-log))
  (declare (ignorable __function__))
  (b*
   (((require-json-member-with-name json-console-log
                                    "Log" *error-console-log*))
    ((json::pattern
        (:object (:member "string" (:string litstring))
                 (:member "parameters"
                          (:array formatting-string-parameters..))))
     (json::member->value json-console-log))
    ((unless (and json::match? (stringp litstring)))
     (mv t *error-console-log*))
    ((mv erp leo-params)
     (j2f-expression-list formatting-string-parameters..))
    ((when erp) (mv t *error-console-log*)))
   (mv nil
       (make-console-log :string (acl2::explode litstring)
                         :exprs leo-params)))))