		Search-engine friendly clone of the ACL2 documentation.

Atc-pretty-printer

Pprint-tyspecseq

Pretty-print a sequence of type specifiers.

Signature
(pprint-tyspecseq tss) → part
Arguments: tss — Guard (tyspecseqp tss).
Returns: part — Type (msgp part).

As noted in tyspecseq, for now we only capture one sequence for each type, so we need to pick what to print here. We pick the shortest (or only) choice for each type.

Definitions and Theorems

Function: pprint-tyspecseq

(defun pprint-tyspecseq (tss)
  (declare (xargs :guard (tyspecseqp tss)))
  (let ((__function__ 'pprint-tyspecseq))
    (declare (ignorable __function__))
    (tyspecseq-case
         tss
         :void "void"
         :char "char"
         :schar "signed char"
         :uchar "unsigned char"
         :sshort (msg "~s0short~s1"
                      (if tss.signed "signed " "")
                      (if tss.int " int" ""))
         :ushort (msg "unsigned short~s0"
                      (if tss.int " int" ""))
         :sint (cond ((and tss.signed tss.int) "signed int")
                     (tss.signed "signed")
                     (tss.int "int")
                     (t (prog2$ (impossible) "")))
         :uint (msg "unsigned~s0" (if tss.int " int" ""))
         :slong (msg "~s0long~s1"
                     (if tss.signed "signed " "")
                     (if tss.int " int" ""))
         :ulong (msg "unsigned long~s0"
                     (if tss.int " int" ""))
         :sllong (msg "~s0long long~s1"
                      (if tss.signed "signed " "")
                      (if tss.int " int" ""))
         :ullong (msg "unsigned long long~s0"
                      (if tss.int " int" ""))
         :bool "_Bool"
         :float (msg "float~s0"
                     (if tss.complex " _Complex" ""))
         :double (msg "double~s0"
                      (if tss.complex " _Complex" ""))
         :ldouble (msg "long double~s0"
                       (if tss.complex " _Complex" ""))
         :struct (msg "struct ~@0" (pprint-ident tss.tag))
         :union (msg "union ~@0" (pprint-ident tss.tag))
         :enum (msg "union ~@0" (pprint-ident tss.tag))
         :typedef (pprint-ident tss.name))))

Theorem: msgp-of-pprint-tyspecseq

(defthm msgp-of-pprint-tyspecseq
  (b* ((part (pprint-tyspecseq tss)))
    (msgp part))
  :rule-classes :rewrite)

Theorem: pprint-tyspecseq-of-tyspecseq-fix-tss

(defthm pprint-tyspecseq-of-tyspecseq-fix-tss
  (equal (pprint-tyspecseq (tyspecseq-fix tss))
         (pprint-tyspecseq tss)))

Theorem: pprint-tyspecseq-tyspecseq-equiv-congruence-on-tss

(defthm pprint-tyspecseq-tyspecseq-equiv-congruence-on-tss
  (implies (tyspecseq-equiv tss tss-equiv)
           (equal (pprint-tyspecseq tss)
                  (pprint-tyspecseq tss-equiv)))
  :rule-classes :congruence)