		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-astring

Print the characters from an ACL2 string.

Signature
(print-astring string pstate) → new-pstate
Arguments: string — Guard (stringp string).; pstate — Guard (pristatep pstate).
Returns: new-pstate — Type (pristatep new-pstate).

This provides the convenience to use use ACL2 strings, instead of using character codes.

Since most of the C syntax is ASCII, this printing function is used to print most of the code.

Note that an ACL2 string can contain characters that, when converted to natural numbers, are larger than 127, and therefore are not ASCII. But we always call this printing function with ASCII strings.

Definitions and Theorems

Function: print-astring

(defun print-astring (string pstate)
 (declare (xargs :guard (and (stringp string)
                             (pristatep pstate))))
 (declare
  (xargs
      :guard (grammar-character-listp (acl2::string=>nats string))))
 (let ((__function__ 'print-astring))
   (declare (ignorable __function__))
   (print-chars (acl2::string=>nats string)
                pstate)))

Theorem: pristatep-of-print-astring

(defthm pristatep-of-print-astring
  (b* ((new-pstate (print-astring string pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: print-astring-of-pristate-fix-pstate

(defthm print-astring-of-pristate-fix-pstate
  (equal (print-astring string (pristate-fix pstate))
         (print-astring string pstate)))

Theorem: print-astring-pristate-equiv-congruence-on-pstate

(defthm print-astring-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-astring string pstate)
                  (print-astring string pstate-equiv)))
  :rule-classes :congruence)