		Search-engine friendly clone of the ACL2 documentation.

Json2ast

J2f-console-statement

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

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

Definitions and Theorems

Function: j2f-console-statement

(defun j2f-console-statement (json-console-statement)
 (declare (xargs :guard (json::memberp json-console-statement)))
 (let ((__function__ 'j2f-console-statement))
   (declare (ignorable __function__))
   (b*
     (((require-json-member-with-name
            json-console-statement
            "Console" *error-console-statement*))
      (jcs-value (json::member->value json-console-statement))
      ((require-json-object-with-single-member
            jcs-value *error-console-statement*))
      (jcs-function (first (json::value-object->members jcs-value)))
      ((require-json-member-with-name
            jcs-function
            "function" *error-console-statement*))
      (jcs-function-value (json::member->value jcs-function))
      ((require-json-object-with-single-member
            jcs-function-value
            *error-console-statement*))
      (jcs-specific-function
           (first (json::value-object->members jcs-function-value)))
      (jcs-specific-function-name
           (json::member->name jcs-specific-function))
      ((mv erp console-function)
       (cond ((equal jcs-specific-function-name "Assert")
              (j2f-console-assert jcs-specific-function))
             ((equal jcs-specific-function-name "Log")
              (j2f-console-log jcs-specific-function))
             ((equal jcs-specific-function-name "Error")
              (j2f-console-error jcs-specific-function))
             (t (mv t *error-outer-console-error*)))))
     (mv erp
         (make-statement-console :get console-function)))))