		Search-engine friendly clone of the ACL2 documentation.

Pretty-printer

Pprint-console

Pretty-print a console call.

Signature
(pprint-console cnsl level) → line
Arguments: cnsl — Guard (consolep cnsl).; level — Guard (natp level).
Returns: line — Type (msgp line).

Definitions and Theorems

Function: pprint-console

(defun pprint-console (cnsl level)
 (declare (xargs :guard (and (consolep cnsl) (natp level))))
 (let ((__function__ 'pprint-console))
  (declare (ignorable __function__))
  (pprint-line
   (console-case
    cnsl
    :assert (msg "console.assert(~@0);"
                 (pprint-expression cnsl.arg (expr-grade-top)))
    :error
    (msg "console.error(\"~@0\"~s1~@2);"
         (pprint-char-list cnsl.string)
         (if (consp cnsl.exprs) "," "")
         (pprint-comma-separated
              (pprint-expression-list cnsl.exprs (expr-grade-top))))
    :log
    (msg
        "console.log(\"~@0\"~s1~@2);"
        (pprint-char-list cnsl.string)
        (if (consp cnsl.exprs) "," "")
        (pprint-comma-separated
             (pprint-expression-list cnsl.exprs (expr-grade-top)))))
   level)))

Theorem: msgp-of-pprint-console

(defthm msgp-of-pprint-console
  (b* ((line (pprint-console cnsl level)))
    (msgp line))
  :rule-classes :rewrite)

Theorem: pprint-console-of-console-fix-cnsl

(defthm pprint-console-of-console-fix-cnsl
  (equal (pprint-console (console-fix cnsl)
                         level)
         (pprint-console cnsl level)))

Theorem: pprint-console-console-equiv-congruence-on-cnsl

(defthm pprint-console-console-equiv-congruence-on-cnsl
  (implies (console-equiv cnsl cnsl-equiv)
           (equal (pprint-console cnsl level)
                  (pprint-console cnsl-equiv level)))
  :rule-classes :congruence)

Theorem: pprint-console-of-nfix-level

(defthm pprint-console-of-nfix-level
  (equal (pprint-console cnsl (nfix level))
         (pprint-console cnsl level)))

Theorem: pprint-console-nat-equiv-congruence-on-level

(defthm pprint-console-nat-equiv-congruence-on-level
  (implies (acl2::nat-equiv level level-equiv)
           (equal (pprint-console cnsl level)
                  (pprint-console cnsl level-equiv)))
  :rule-classes :congruence)