		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-ident

Print an identifier.

Signature
(print-ident ident pstate) → new-pstate
Arguments: ident — Guard (identp ident).; pstate — Guard (pristatep pstate).
Returns: new-pstate — Type (pristatep new-pstate).

We check that the identifier is a non-empty ACL2 string whose character codes are all valid in our C grammar. This way we can call print-chars.

This is a weaker check than ensuring that the string is in fact a valid C identifier in our concrete syntax. We plan to strengthen this in the future.

Definitions and Theorems

Function: print-ident

(defun print-ident (ident pstate)
 (declare (xargs :guard (and (identp ident)
                             (pristatep pstate))))
 (let ((__function__ 'print-ident))
  (declare (ignorable __function__))
  (b*
   ((string? (ident->unwrap ident))
    ((unless (stringp string?))
     (raise
      "Misusage error: ~
                the identifier contains ~x0 instead of an ACL2 string."
      string?)
     (pristate-fix pstate))
    (chars (acl2::string=>nats string?))
    ((unless chars)
     (raise
       "Misusage error; ~
                the identifier is empty.")
     (pristate-fix pstate))
    ((unless (grammar-character-listp chars))
     (raise
      "Misusage error: ~
                the identifier consists of the character codes ~x0, ~
                not all of which are allowed by the ABNF grammar."
      chars)
     (pristate-fix pstate)))
   (print-chars chars pstate))))

Theorem: pristatep-of-print-ident

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

Theorem: print-ident-of-ident-fix-ident

(defthm print-ident-of-ident-fix-ident
  (equal (print-ident (ident-fix ident) pstate)
         (print-ident ident pstate)))

Theorem: print-ident-ident-equiv-congruence-on-ident

(defthm print-ident-ident-equiv-congruence-on-ident
  (implies (ident-equiv ident ident-equiv)
           (equal (print-ident ident pstate)
                  (print-ident ident-equiv pstate)))
  :rule-classes :congruence)

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

(defthm print-ident-of-pristate-fix-pstate
  (equal (print-ident ident (pristate-fix pstate))
         (print-ident ident pstate)))

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

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