		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-exprs/decls/stmts

Print expressions, declarations, statements, and related entities.

Definitions and Theorems

Function: print-expr

(defun print-expr (expr expected-prio pstate)
 (declare (xargs :guard (and (exprp expr)
                             (expr-priorityp expected-prio)
                             (pristatep pstate))))
 (declare
    (xargs :guard (and (expr-unambp expr)
                       (expr-aidentp expr (pristate->gcc pstate)))))
 (let ((__function__ 'print-expr))
  (declare (ignorable __function__))
  (b*
   ((actual-prio (expr->priority expr))
    (parenp (expr-priority-< actual-prio expected-prio))
    (pstate (if parenp (print-astring "(" pstate)
              pstate))
    (pstate
     (expr-case
      expr
      :ident (print-ident expr.ident pstate)
      :const (print-const expr.const pstate)
      :string
      (b*
       (((unless expr.strings)
         (raise
          "Misusage error: ~
                         empty list of string literals.")
         (pristate-fix pstate)))
       (print-stringlit-list expr.strings pstate))
      :paren
      (b* ((pstate (print-astring "(" pstate))
           (pstate (print-expr expr.inner (expr-priority-expr)
                               pstate))
           (pstate (print-astring ")" pstate)))
        pstate)
      :gensel
      (b*
       ((pstate (print-astring "_Generic(" pstate))
        (pstate (print-expr expr.control (expr-priority-asg)
                            pstate))
        (pstate (print-astring ", " pstate))
        ((unless expr.assocs)
         (raise
          "Misusage error: ~
                         empty generic association list.")
         pstate)
        (pstate (print-genassoc-list expr.assocs pstate))
        (pstate (print-astring ")" pstate)))
       pstate)
      :arrsub
      (b* ((pstate (print-expr expr.arg1 (expr-priority-postfix)
                               pstate))
           (pstate (print-astring "[" pstate))
           (pstate (print-expr expr.arg2 (expr-priority-expr)
                               pstate))
           (pstate (print-astring "]" pstate)))
        pstate)
      :funcall
      (b* ((pstate (print-expr expr.fun (expr-priority-postfix)
                               pstate))
           (pstate (print-astring "(" pstate))
           (pstate (if expr.args (print-expr-list expr.args pstate)
                     pstate))
           (pstate (print-astring ")" pstate)))
        pstate)
      :member
      (b* ((pstate (print-expr expr.arg (expr-priority-postfix)
                               pstate))
           (pstate (print-astring "." pstate))
           (pstate (print-ident expr.name pstate)))
        pstate)
      :memberp
      (b* ((pstate (print-expr expr.arg (expr-priority-postfix)
                               pstate))
           (pstate (print-astring "->" pstate))
           (pstate (print-ident expr.name pstate)))
        pstate)
      :complit
      (b*
       ((pstate (print-astring "(" pstate))
        (pstate (print-tyname expr.type pstate))
        (pstate (print-astring ") {" pstate))
        (pstate
          (if
           (consp expr.elems)
           (b*
             ((pstate (print-desiniter-list expr.elems pstate))
              (pstate
                   (if expr.final-comma (print-astring ", }" pstate)
                     (print-astring "}" pstate))))
             pstate)
           (print-astring " }" pstate))))
       pstate)
      :unary
      (if (or (unop-case expr.op :postinc)
              (unop-case expr.op :postdec))
          (b* ((pstate (print-expr expr.arg (expr-priority-postfix)
                                   pstate))
               (pstate (print-unop expr.op pstate)))
            pstate)
        (b* ((pstate (print-unop expr.op pstate))
             (spacep (or (and (or (unop-case expr.op :sizeof)
                                  (unop-case expr.op :alignof))
                              (not (expr-case expr.arg :paren)))
                         (and (unop-case expr.op :plus)
                              (expr-case expr.arg :unary)
                              (unop-case (expr-unary->op expr.arg)
                                         :preinc))
                         (and (unop-case expr.op :minus)
                              (expr-case expr.arg :unary)
                              (unop-case (expr-unary->op expr.arg)
                                         :predec))))
             (pstate (if spacep (print-astring " " pstate)
                       pstate))
             (arg-priority (if (or (unop-case expr.op :preinc)
                                   (unop-case expr.op :predec)
                                   (unop-case expr.op :sizeof)
                                   (unop-case expr.op :alignof))
                               (expr-priority-unary)
                             (expr-priority-cast)))
             (pstate (print-expr expr.arg arg-priority pstate)))
          pstate))
      :label-addr
      (b* ((pstate (print-astring "&&" pstate))
           (pstate (print-ident expr.arg pstate)))
        pstate)
      :sizeof
      (b* ((pstate (print-astring "sizeof(" pstate))
           (pstate (print-tyname expr.type pstate))
           (pstate (print-astring ")" pstate)))
        pstate)
      :sizeof-ambig
      (prog2$ (impossible)
              (pristate-fix pstate))
      :alignof
      (b*
        ((pstate (keyword-uscores-case
                      expr.uscores
                      :none (print-astring "_Alignof(" pstate)
                      :start (print-astring "__alignof(" pstate)
                      :both (print-astring "__alignof__(" pstate)))
         (pstate (print-tyname expr.type pstate))
         (pstate (print-astring ")" pstate)))
        pstate)
      :alignof-ambig
      (prog2$ (impossible)
              (pristate-fix pstate))
      :cast
      (b* ((pstate (print-astring "(" pstate))
           (pstate (print-tyname expr.type pstate))
           (pstate (print-astring ") " pstate))
           (pstate (print-expr expr.arg (expr-priority-cast)
                               pstate)))
        pstate)
      :binary
      (b*
        (((mv expected-arg1-prio expected-arg2-prio)
          (binop-expected-priorities expr.op))
         (pstate (print-expr expr.arg1 expected-arg1-prio pstate))
         (pstate (print-astring " " pstate))
         (pstate (print-binop expr.op pstate))
         (pstate (print-astring " " pstate))
         (pstate (print-expr expr.arg2 expected-arg2-prio pstate)))
        pstate)
      :cond
      (b*
       ((raise-prio
            (priopt->paren-nested-conds (pristate->options pstate)))
        (pstate (print-expr expr.test (expr-priority-logor)
                            pstate))
        (pstate (print-astring " ? " pstate))
        (pstate
         (expr-option-case
          expr.then :some
          (b*
           ((pstate (print-expr expr.then.val
                                (if raise-prio (expr-priority-logor)
                                  (expr-priority-expr))
                                pstate))
            (pstate (print-astring " " pstate)))
           pstate)
          :none pstate))
        (pstate (print-astring ": " pstate))
        (pstate (print-expr expr.else
                            (if raise-prio (expr-priority-logor)
                              (expr-priority-cond))
                            pstate)))
       pstate)
      :comma
      (b* ((pstate (print-expr expr.first (expr-priority-expr)
                               pstate))
           (pstate (print-astring ", " pstate))
           (pstate (print-expr expr.next (expr-priority-asg)
                               pstate)))
        pstate)
      :cast/call-ambig
      (prog2$ (impossible)
              (pristate-fix pstate))
      :cast/mul-ambig
      (prog2$ (impossible)
              (pristate-fix pstate))
      :cast/add-ambig
      (prog2$ (impossible)
              (pristate-fix pstate))
      :cast/sub-ambig
      (prog2$ (impossible)
              (pristate-fix pstate))
      :cast/and-ambig
      (prog2$ (impossible)
              (pristate-fix pstate))
      :cast/logand-ambig
      (prog2$ (impossible)
              (pristate-fix pstate))
      :stmt
      (b* ((pstate (print-astring "(" pstate))
           (pstate (print-comp-stmt expr.stmt pstate))
           (pstate (print-astring ")" pstate)))
        pstate)
      :tycompat
      (b*
       ((pstate
             (print-astring "__builtin_types_compatible_p(" pstate))
        (pstate (print-tyname expr.type1 pstate))
        (pstate (print-astring ", " pstate))
        (pstate (print-tyname expr.type2 pstate))
        (pstate (print-astring ")" pstate)))
       pstate)
      :offsetof
      (b* ((pstate (print-astring "__builtin_offsetof(" pstate))
           (pstate (print-tyname expr.type pstate))
           (pstate (print-astring ", " pstate))
           (pstate (print-member-designor expr.member pstate))
           (pstate (print-astring ")" pstate)))
        pstate)
      :va-arg
      (b* ((pstate (print-astring "__builtin_va_arg(" pstate))
           (pstate (print-expr expr.list (expr-priority-asg)
                               pstate))
           (pstate (print-astring ", " pstate))
           (pstate (print-tyname expr.type pstate))
           (pstate (print-astring ")" pstate)))
        pstate)
      :extension
      (b* ((pstate (print-astring "__extension__ " pstate))
           (pstate (print-expr expr.expr (expr-priority-primary)
                               pstate)))
        pstate)))
    (pstate (if parenp (print-astring ")" pstate)
              pstate)))
   pstate)))

Function: print-expr-list

(defun print-expr-list (exprs pstate)
 (declare (xargs :guard (and (expr-listp exprs)
                             (pristatep pstate))))
 (declare
  (xargs
     :guard (and (consp exprs)
                 (expr-list-unambp exprs)
                 (expr-list-aidentp exprs (pristate->gcc pstate)))))
 (let ((__function__ 'print-expr-list))
   (declare (ignorable __function__))
   (b* (((unless (mbt (consp exprs)))
         (pristate-fix pstate))
        (pstate (print-expr (car exprs)
                            (expr-priority-asg)
                            pstate))
        ((when (endp (cdr exprs))) pstate)
        (pstate (print-astring ", " pstate)))
     (print-expr-list (cdr exprs) pstate))))

Function: print-const-expr

(defun print-const-expr (cexpr pstate)
 (declare (xargs :guard (and (const-exprp cexpr)
                             (pristatep pstate))))
 (declare
  (xargs
    :guard (and (const-expr-unambp cexpr)
                (const-expr-aidentp cexpr (pristate->gcc pstate)))))
 (let ((__function__ 'print-const-expr))
   (declare (ignorable __function__))
   (print-expr (const-expr->expr cexpr)
               (expr-priority-cond)
               pstate)))

Function: print-genassoc

(defun print-genassoc (genassoc pstate)
 (declare (xargs :guard (and (genassocp genassoc)
                             (pristatep pstate))))
 (declare
  (xargs
   :guard (and (genassoc-unambp genassoc)
               (genassoc-aidentp genassoc (pristate->gcc pstate)))))
 (let ((__function__ 'print-genassoc))
   (declare (ignorable __function__))
   (genassoc-case
        genassoc :type
        (b* ((pstate (print-tyname genassoc.type pstate))
             (pstate (print-astring ": " pstate))
             (pstate (print-expr genassoc.expr (expr-priority-asg)
                                 pstate)))
          pstate)
        :default
        (b* ((pstate (print-astring "default: " pstate))
             (pstate (print-expr genassoc.expr (expr-priority-asg)
                                 pstate)))
          pstate))))

Function: print-genassoc-list

(defun print-genassoc-list (genassocs pstate)
 (declare (xargs :guard (and (genassoc-listp genassocs)
                             (pristatep pstate))))
 (declare
  (xargs
    :guard
    (and (consp genassocs)
         (genassoc-list-unambp genassocs)
         (genassoc-list-aidentp genassocs (pristate->gcc pstate)))))
 (let ((__function__ 'print-genassoc-list))
   (declare (ignorable __function__))
   (b* (((unless (mbt (consp genassocs)))
         (pristate-fix pstate))
        (pstate (print-genassoc (car genassocs) pstate))
        ((when (endp (cdr genassocs))) pstate)
        (pstate (print-astring ", " pstate)))
     (print-genassoc-list (cdr genassocs)
                          pstate))))

Function: print-member-designor

(defun print-member-designor (memdes pstate)
 (declare (xargs :guard (and (member-designorp memdes)
                             (pristatep pstate))))
 (declare
  (xargs
     :guard
     (and (member-designor-unambp memdes)
          (member-designor-aidentp memdes (pristate->gcc pstate)))))
 (let ((__function__ 'print-member-designor))
   (declare (ignorable __function__))
   (member-designor-case
        memdes
        :ident (print-ident memdes.ident pstate)
        :dot
        (b* ((pstate (print-member-designor memdes.member pstate))
             (pstate (print-astring "." pstate))
             (pstate (print-ident memdes.name pstate)))
          pstate)
        :sub
        (b* ((pstate (print-member-designor memdes.member pstate))
             (pstate (print-astring "[" pstate))
             (pstate (print-expr memdes.index (expr-priority-expr)
                                 pstate)))
          pstate))))

Function: print-type-spec

(defun print-type-spec (tyspec pstate)
 (declare (xargs :guard (and (type-specp tyspec)
                             (pristatep pstate))))
 (declare
  (xargs
    :guard (and (type-spec-unambp tyspec)
                (type-spec-aidentp tyspec (pristate->gcc pstate)))))
 (let ((__function__ 'print-type-spec))
  (declare (ignorable __function__))
  (type-spec-case
   tyspec
   :void (print-astring "void" pstate)
   :char (print-astring "char" pstate)
   :short (print-astring "short" pstate)
   :int (print-astring "int" pstate)
   :long (print-astring "long" pstate)
   :float (print-astring "float" pstate)
   :double (print-astring "double" pstate)
   :signed
   (keyword-uscores-case tyspec.uscores
                         :none (print-astring "signed" pstate)
                         :start (print-astring "__signed" pstate)
                         :both (print-astring "__signed__" pstate))
   :unsigned
   (print-astring "unsigned" pstate)
   :bool (print-astring "_Bool" pstate)
   :complex
   (print-astring "_Complex" pstate)
   :atomic
   (b* ((pstate (print-astring "_Atomic(" pstate))
        (pstate (print-tyname tyspec.type pstate))
        (pstate (print-astring ")" pstate)))
     pstate)
   :struct
   (b* ((pstate (print-astring "struct " pstate))
        (pstate (print-struni-spec tyspec.spec pstate)))
     pstate)
   :union
   (b* ((pstate (print-astring "union " pstate))
        (pstate (print-struni-spec tyspec.spec pstate)))
     pstate)
   :enum
   (b* ((pstate (print-astring "enum " pstate))
        (pstate (print-enum-spec tyspec.spec pstate)))
     pstate)
   :typedef
   (print-ident tyspec.name pstate)
   :int128
   (if tyspec.uscoret (print-astring "__int128_t" pstate)
     (print-astring "__int128" pstate))
   :locase-float80
   (print-astring "__float80" pstate)
   :locase-float128
   (print-astring "__float128" pstate)
   :float16
   (print-astring "_Float16" pstate)
   :float16x
   (print-astring "_Float16x" pstate)
   :float32
   (print-astring "_Float32" pstate)
   :float32x
   (print-astring "_Float32x" pstate)
   :float64
   (print-astring "_Float64" pstate)
   :float64x
   (print-astring "_Float64x" pstate)
   :float128
   (print-astring "_Float128" pstate)
   :float128x
   (print-astring "_Float128x" pstate)
   :builtin-va-list
   (print-astring "__builtin_va_list" pstate)
   :struct-empty
   (b*
    ((pstate (print-astring "struct" pstate))
     (pstate
      (if
       (consp tyspec.attribs)
       (b* ((pstate (print-astring " " pstate))
            (pstate (print-attrib-spec-list tyspec.attribs pstate)))
         pstate)
       pstate))
     (pstate (if tyspec.name?
                 (b* ((pstate (print-astring " " pstate))
                      (pstate (print-ident tyspec.name? pstate)))
                   pstate)
               pstate))
     (pstate (print-astring " { }" pstate)))
    pstate)
   :typeof-expr
   (b* ((pstate (keyword-uscores-case
                     tyspec.uscores
                     :none (print-astring "typeof(" pstate)
                     :start (print-astring "__typeof(" pstate)
                     :both (print-astring "__typeof__(" pstate)))
        (pstate (print-expr tyspec.expr (expr-priority-expr)
                            pstate))
        (pstate (print-astring ")" pstate)))
     pstate)
   :typeof-type
   (b* ((pstate (keyword-uscores-case
                     tyspec.uscores
                     :none (print-astring "typeof(" pstate)
                     :start (print-astring "__typeof(" pstate)
                     :both (print-astring "__typeof__(" pstate)))
        (pstate (print-tyname tyspec.type pstate))
        (pstate (print-astring ")" pstate)))
     pstate)
   :typeof-ambig (prog2$ (impossible)
                         (pristate-fix pstate))
   :auto-type (print-astring "__auto_type" pstate))))

Function: print-spec/qual

(defun print-spec/qual (specqual pstate)
 (declare (xargs :guard (and (spec/qual-p specqual)
                             (pristatep pstate))))
 (declare
  (xargs :guard
         (and (spec/qual-unambp specqual)
              (spec/qual-aidentp specqual (pristate->gcc pstate)))))
 (let ((__function__ 'print-spec/qual))
   (declare (ignorable __function__))
   (spec/qual-case
        specqual
        :typespec (print-type-spec specqual.spec pstate)
        :typequal (print-type-qual specqual.qual pstate)
        :align (print-align-spec specqual.spec pstate)
        :attrib (print-attrib-spec specqual.spec pstate))))

Function: print-spec/qual-list

(defun print-spec/qual-list (specquals pstate)
 (declare (xargs :guard (and (spec/qual-listp specquals)
                             (pristatep pstate))))
 (declare
  (xargs
   :guard
   (and (consp specquals)
        (spec/qual-list-unambp specquals)
        (spec/qual-list-aidentp specquals (pristate->gcc pstate)))))
 (let ((__function__ 'print-spec/qual-list))
   (declare (ignorable __function__))
   (b* (((unless (mbt (consp specquals)))
         (pristate-fix pstate))
        (pstate (print-spec/qual (car specquals)
                                 pstate))
        ((when (endp (cdr specquals))) pstate)
        (pstate (print-astring " " pstate)))
     (print-spec/qual-list (cdr specquals)
                           pstate))))

Function: print-align-spec

(defun print-align-spec (alignspec pstate)
 (declare (xargs :guard (and (align-specp alignspec)
                             (pristatep pstate))))
 (declare
  (xargs
       :guard
       (and (align-spec-unambp alignspec)
            (align-spec-aidentp alignspec (pristate->gcc pstate)))))
 (let ((__function__ 'print-align-spec))
  (declare (ignorable __function__))
  (b*
   ((pstate (print-astring "_Alignas(" pstate))
    (pstate
         (align-spec-case
              alignspec
              :alignas-type (print-tyname alignspec.type pstate)
              :alignas-expr (print-const-expr alignspec.expr pstate)
              :alignas-ambig (prog2$ (impossible)
                                     (pristate-fix pstate))))
    (pstate (print-astring ")" pstate)))
   pstate)))

Function: print-decl-spec

(defun print-decl-spec (declspec pstate)
 (declare (xargs :guard (and (decl-specp declspec)
                             (pristatep pstate))))
 (declare
  (xargs :guard
         (and (decl-spec-unambp declspec)
              (decl-spec-aidentp declspec (pristate->gcc pstate)))))
 (let ((__function__ 'print-decl-spec))
  (declare (ignorable __function__))
  (decl-spec-case declspec :stoclass
                  (print-stor-spec declspec.spec pstate)
                  :typespec
                  (print-type-spec declspec.spec pstate)
                  :typequal
                  (print-type-qual declspec.qual pstate)
                  :function
                  (print-fun-spec declspec.spec pstate)
                  :align
                  (print-align-spec declspec.spec pstate)
                  :attrib
                  (print-attrib-spec declspec.spec pstate)
                  :stdcall
                  (print-astring "__stdcall" pstate)
                  :declspec
                  (b* ((pstate (print-astring "__declspec(" pstate))
                       (pstate (print-ident declspec.arg pstate))
                       (pstate (print-astring ")" pstate)))
                    pstate))))

Function: print-decl-spec-list

(defun print-decl-spec-list (declspecs pstate)
 (declare (xargs :guard (and (decl-spec-listp declspecs)
                             (pristatep pstate))))
 (declare
  (xargs
   :guard
   (and (consp declspecs)
        (decl-spec-list-unambp declspecs)
        (decl-spec-list-aidentp declspecs (pristate->gcc pstate)))))
 (let ((__function__ 'print-decl-spec-list))
   (declare (ignorable __function__))
   (b* (((unless (mbt (consp declspecs)))
         (pristate-fix pstate))
        (pstate (print-decl-spec (car declspecs)
                                 pstate))
        ((when (endp (cdr declspecs))) pstate)
        (pstate (print-astring " " pstate)))
     (print-decl-spec-list (cdr declspecs)
                           pstate))))

Function: print-typequal/attribspec

(defun print-typequal/attribspec (tyqualattrib pstate)
  (declare (xargs :guard (and (typequal/attribspec-p tyqualattrib)
                              (pristatep pstate))))
  (declare (xargs :guard (typequal/attribspec-aidentp
                              tyqualattrib (pristate->gcc pstate))))
  (let ((__function__ 'print-typequal/attribspec))
    (declare (ignorable __function__))
    (typequal/attribspec-case
         tyqualattrib
         :type (print-type-qual tyqualattrib.unwrap pstate)
         :attrib (print-attrib-spec tyqualattrib.unwrap pstate))))

Function: print-typequal/attribspec-list

(defun print-typequal/attribspec-list (tyqualattribs pstate)
 (declare
      (xargs :guard (and (typequal/attribspec-listp tyqualattribs)
                         (pristatep pstate))))
 (declare
    (xargs :guard (and (consp tyqualattribs)
                       (typequal/attribspec-list-aidentp
                            tyqualattribs (pristate->gcc pstate)))))
 (let ((__function__ 'print-typequal/attribspec-list))
   (declare (ignorable __function__))
   (b* (((unless (mbt (consp tyqualattribs)))
         (pristate-fix pstate))
        (pstate (print-typequal/attribspec (car tyqualattribs)
                                           pstate))
        ((when (endp (cdr tyqualattribs)))
         pstate)
        (pstate (print-astring " " pstate)))
     (print-typequal/attribspec-list (cdr tyqualattribs)
                                     pstate))))

Function: print-typequal/attribspec-list-list

(defun print-typequal/attribspec-list-list (tyqualattribss pstate)
 (declare
  (xargs :guard (and (typequal/attribspec-list-listp tyqualattribss)
                     (pristatep pstate))))
 (declare (xargs :guard (and (consp tyqualattribss)
                             (typequal/attribspec-list-list-aidentp
                                  tyqualattribss
                                  (pristate->gcc pstate)))))
 (let ((__function__ 'print-typequal/attribspec-list-list))
  (declare (ignorable __function__))
  (b*
   (((unless (mbt (consp tyqualattribss)))
     (pristate-fix pstate))
    (pstate (print-astring "*" pstate))
    (tyqualattribs (car tyqualattribss))
    (pstate
      (if
       (consp tyqualattribs)
       (b*
        ((pstate (print-astring " " pstate))
         (pstate
              (print-typequal/attribspec-list tyqualattribs pstate))
         (pstate (print-astring " " pstate)))
        pstate)
       pstate))
    ((when (endp (cdr tyqualattribss)))
     pstate))
   (print-typequal/attribspec-list-list (cdr tyqualattribss)
                                        pstate))))

Function: print-initer

(defun print-initer (initer pstate)
 (declare (xargs :guard (and (initerp initer)
                             (pristatep pstate))))
 (declare
  (xargs
       :guard (and (initer-unambp initer)
                   (initer-aidentp initer (pristate->gcc pstate)))))
 (let ((__function__ 'print-initer))
  (declare (ignorable __function__))
  (initer-case
   initer :single
   (print-expr initer.expr (expr-priority-asg)
               pstate)
   :list
   (b*
    ((pstate (print-astring "{" pstate))
     ((unless initer.elems)
      (raise
       "Misusage error: ~
                         empty list of initializers.")
      pstate)
     (pstate (print-desiniter-list initer.elems pstate))
     (pstate (if initer.final-comma (print-astring ", }" pstate)
               (print-astring "}" pstate))))
    pstate))))

Function: print-desiniter

(defun print-desiniter (desiniter pstate)
 (declare (xargs :guard (and (desiniterp desiniter)
                             (pristatep pstate))))
 (declare
   (xargs
        :guard
        (and (desiniter-unambp desiniter)
             (desiniter-aidentp desiniter (pristate->gcc pstate)))))
 (let ((__function__ 'print-desiniter))
  (declare (ignorable __function__))
  (b*
   (((desiniter desiniter) desiniter)
    (pstate
     (if desiniter.designors
      (b* ((pstate (print-designor-list desiniter.designors pstate))
           (pstate (print-astring " = " pstate)))
        pstate)
      pstate))
    (pstate (print-initer desiniter.initer pstate)))
   pstate)))

Function: print-desiniter-list

(defun print-desiniter-list (desiniters pstate)
 (declare (xargs :guard (and (desiniter-listp desiniters)
                             (pristatep pstate))))
 (declare
  (xargs
   :guard
   (and
       (consp desiniters)
       (desiniter-list-unambp desiniters)
       (desiniter-list-aidentp desiniters (pristate->gcc pstate)))))
 (let ((__function__ 'print-desiniter-list))
   (declare (ignorable __function__))
   (b* (((unless (mbt (consp desiniters)))
         (pristate-fix pstate))
        (pstate (print-desiniter (car desiniters)
                                 pstate))
        ((when (endp (cdr desiniters))) pstate)
        (pstate (print-astring ", " pstate)))
     (print-desiniter-list (cdr desiniters)
                           pstate))))

Function: print-designor

(defun print-designor (designor pstate)
 (declare (xargs :guard (and (designorp designor)
                             (pristatep pstate))))
 (declare
  (xargs
   :guard (and (designor-unambp designor)
               (designor-aidentp designor (pristate->gcc pstate)))))
 (let ((__function__ 'print-designor))
  (declare (ignorable __function__))
  (designor-case
   designor :sub
   (b*
    ((pstate (print-astring "[" pstate))
     (pstate (print-const-expr designor.index pstate))
     (pstate
      (const-expr-option-case
        designor.range? :some
        (b* ((pstate (print-astring "..." pstate))
             (pstate (print-const-expr designor.range?.val pstate)))
          pstate)
        :none pstate))
     (pstate (print-astring "]" pstate)))
    pstate)
   :dot
   (b* ((pstate (print-astring "." pstate))
        (pstate (print-ident designor.name pstate)))
     pstate))))

Function: print-designor-list

(defun print-designor-list (designors pstate)
 (declare (xargs :guard (and (designor-listp designors)
                             (pristatep pstate))))
 (declare
  (xargs
    :guard
    (and (consp designors)
         (designor-list-unambp designors)
         (designor-list-aidentp designors (pristate->gcc pstate)))))
 (let ((__function__ 'print-designor-list))
   (declare (ignorable __function__))
   (b* (((unless (mbt (consp designors)))
         (pristate-fix pstate))
        (pstate (print-designor (car designors) pstate))
        ((when (endp (cdr designors))) pstate))
     (print-designor-list (cdr designors)
                          pstate))))

Function: print-declor

(defun print-declor (declor pstate)
 (declare (xargs :guard (and (declorp declor)
                             (pristatep pstate))))
 (declare
  (xargs
       :guard (and (declor-unambp declor)
                   (declor-aidentp declor (pristate->gcc pstate)))))
 (let ((__function__ 'print-declor))
  (declare (ignorable __function__))
  (b*
   (((declor declor) declor)
    (pstate
      (if
        (consp declor.pointers)
        (print-typequal/attribspec-list-list declor.pointers pstate)
        pstate))
    (pstate (print-dirdeclor declor.direct pstate)))
   pstate)))

Function: print-dirdeclor

(defun print-dirdeclor (dirdeclor pstate)
 (declare (xargs :guard (and (dirdeclorp dirdeclor)
                             (pristatep pstate))))
 (declare
   (xargs
        :guard
        (and (dirdeclor-unambp dirdeclor)
             (dirdeclor-aidentp dirdeclor (pristate->gcc pstate)))))
 (let ((__function__ 'print-dirdeclor))
  (declare (ignorable __function__))
  (dirdeclor-case
   dirdeclor :ident
   (print-ident dirdeclor.ident pstate)
   :paren
   (b* ((pstate (print-astring "(" pstate))
        (pstate (print-declor dirdeclor.inner pstate))
        (pstate (print-astring ")" pstate)))
     pstate)
   :array
   (b*
    ((pstate (print-dirdeclor dirdeclor.declor pstate))
     (pstate (print-astring "[" pstate))
     (pstate
       (if dirdeclor.qualspecs
         (print-typequal/attribspec-list dirdeclor.qualspecs pstate)
         pstate))
     (pstate (if (and dirdeclor.qualspecs dirdeclor.size?)
                 (print-astring " " pstate)
               pstate))
     (pstate (if (expr-option-case dirdeclor.size? :some)
                 (print-expr (expr-option-some->val dirdeclor.size?)
                             (expr-priority-asg)
                             pstate)
               pstate))
     (pstate (print-astring "]" pstate)))
    pstate)
   :array-static1
   (b* ((pstate (print-dirdeclor dirdeclor.declor pstate))
        (pstate (print-astring "static " pstate))
        (pstate (if dirdeclor.qualspecs
                    (b* ((pstate (print-typequal/attribspec-list
                                      dirdeclor.qualspecs pstate))
                         (pstate (print-astring " " pstate)))
                      pstate)
                  pstate))
        (pstate (print-expr dirdeclor.size (expr-priority-asg)
                            pstate))
        (pstate (print-astring "]" pstate)))
     pstate)
   :array-static2
   (b*
    ((pstate (print-dirdeclor dirdeclor.declor pstate))
     ((unless dirdeclor.qualspecs)
      (raise
       "Misusage error: ~
                   empty list of type qualifiers.")
      pstate)
     (pstate
        (print-typequal/attribspec-list dirdeclor.qualspecs pstate))
     (pstate (print-astring " static " pstate))
     (pstate (print-expr dirdeclor.size (expr-priority-asg)
                         pstate))
     (pstate (print-astring "]" pstate)))
    pstate)
   :array-star
   (b* ((pstate (print-dirdeclor dirdeclor.declor pstate))
        (pstate (print-astring "[" pstate))
        (pstate (if dirdeclor.qualspecs
                    (b* ((pstate (print-typequal/attribspec-list
                                      dirdeclor.qualspecs pstate))
                         (pstate (print-astring " " pstate)))
                      pstate)
                  pstate))
        (pstate (print-astring "*]" pstate)))
     pstate)
   :function-params
   (b*
    ((pstate (print-dirdeclor dirdeclor.declor pstate))
     (pstate (print-astring "(" pstate))
     (pstate (if dirdeclor.params
                 (print-param-declon-list dirdeclor.params pstate)
               pstate))
     (pstate (if dirdeclor.ellipsis (print-astring ", ...)" pstate)
               (print-astring ")" pstate))))
    pstate)
   :function-names
   (b*
    ((pstate (print-dirdeclor dirdeclor.declor pstate))
     (pstate (print-astring "(" pstate))
     (pstate
       (if dirdeclor.names (print-ident-list dirdeclor.names pstate)
         pstate))
     (pstate (print-astring ")" pstate)))
    pstate))))

Function: print-absdeclor

(defun print-absdeclor (absdeclor pstate)
 (declare (xargs :guard (and (absdeclorp absdeclor)
                             (pristatep pstate))))
 (declare
   (xargs
        :guard
        (and (absdeclor-unambp absdeclor)
             (absdeclor-aidentp absdeclor (pristate->gcc pstate)))))
 (let ((__function__ 'print-absdeclor))
  (declare (ignorable __function__))
  (b*
   (((absdeclor absdeclor) absdeclor)
    ((unless (or absdeclor.pointers absdeclor.direct?))
     (raise
      "Misusage error: ~
                  empty abstract declarator.")
     (pristate-fix pstate))
    (pstate (if absdeclor.pointers (print-typequal/attribspec-list-list
                                        absdeclor.pointers pstate)
              pstate))
    (pstate
         (if (dirabsdeclor-option-case absdeclor.direct? :some)
             (print-dirabsdeclor
                  (dirabsdeclor-option-some->val absdeclor.direct?)
                  pstate)
           pstate)))
   pstate)))

Function: print-dirabsdeclor

(defun print-dirabsdeclor (dirabsdeclor pstate)
 (declare (xargs :guard (and (dirabsdeclorp dirabsdeclor)
                             (pristatep pstate))))
 (declare
  (xargs
   :guard
   (and
       (dirabsdeclor-unambp dirabsdeclor)
       (dirabsdeclor-aidentp dirabsdeclor (pristate->gcc pstate)))))
 (let ((__function__ 'print-dirabsdeclor))
  (declare (ignorable __function__))
  (dirabsdeclor-case
   dirabsdeclor :dummy-base
   (prog2$
    (raise
     "Misusage error: ~
                     dummy base case of direct abstract declarator.")
    (pristate-fix pstate))
   :paren
   (b* ((pstate (print-astring "(" pstate))
        (pstate (print-absdeclor dirabsdeclor.inner pstate))
        (pstate (print-astring ")" pstate)))
     pstate)
   :array
   (b*
    ((pstate
       (if (dirabsdeclor-option-case dirabsdeclor.declor? :some)
           (print-dirabsdeclor
                (dirabsdeclor-option-some->val dirabsdeclor.declor?)
                pstate)
         pstate))
     (pstate (print-astring "[" pstate))
     (pstate
      (if dirabsdeclor.qualspecs (print-typequal/attribspec-list
                                      dirabsdeclor.qualspecs pstate)
        pstate))
     (pstate (if (and dirabsdeclor.qualspecs
                      dirabsdeclor.size?)
                 (print-astring " " pstate)
               pstate))
     (pstate
          (if (expr-option-case dirabsdeclor.size? :some)
              (print-expr (expr-option-some->val dirabsdeclor.size?)
                          (expr-priority-asg)
                          pstate)
            pstate))
     (pstate (print-astring "]" pstate)))
    pstate)
   :array-static1
   (b*
    ((pstate
       (if (dirabsdeclor-option-case dirabsdeclor.declor? :some)
           (print-dirabsdeclor
                (dirabsdeclor-option-some->val dirabsdeclor.declor?)
                pstate)
         pstate))
     (pstate (print-astring "static " pstate))
     (pstate (if dirabsdeclor.qualspecs
                 (b* ((pstate (print-typequal/attribspec-list
                                   dirabsdeclor.qualspecs pstate))
                      (pstate (print-astring " " pstate)))
                   pstate)
               pstate))
     (pstate (print-expr dirabsdeclor.size (expr-priority-asg)
                         pstate))
     (pstate (print-astring "]" pstate)))
    pstate)
   :array-static2
   (b*
    ((pstate
       (if (dirabsdeclor-option-case dirabsdeclor.declor? :some)
           (print-dirabsdeclor
                (dirabsdeclor-option-some->val dirabsdeclor.declor?)
                pstate)
         pstate))
     ((unless dirabsdeclor.qualspecs)
      (raise
       "Misusage error: ~
                   empty list of type qualifiers.")
      (pristate-fix pstate))
     (pstate (print-typequal/attribspec-list
                  dirabsdeclor.qualspecs pstate))
     (pstate (print-astring " static " pstate))
     (pstate (print-expr dirabsdeclor.size (expr-priority-asg)
                         pstate))
     (pstate (print-astring "]" pstate)))
    pstate)
   :array-star
   (b*
    ((pstate
       (if (dirabsdeclor-option-case dirabsdeclor.declor? :some)
           (print-dirabsdeclor
                (dirabsdeclor-option-some->val dirabsdeclor.declor?)
                pstate)
         pstate))
     (pstate (print-astring "[*]" pstate)))
    pstate)
   :function
   (b*
    ((pstate
       (if (dirabsdeclor-option-case dirabsdeclor.declor? :some)
           (print-dirabsdeclor
                (dirabsdeclor-option-some->val dirabsdeclor.declor?)
                pstate)
         pstate))
     (pstate (print-astring "(" pstate))
     (pstate
      (if dirabsdeclor.params
       (b*
        ((pstate
              (print-param-declon-list dirabsdeclor.params pstate))
         (pstate
            (if dirabsdeclor.ellipsis (print-astring ", ..." pstate)
              pstate)))
        pstate)
       pstate))
     (pstate (print-astring ")" pstate)))
    pstate))))

Function: print-param-declon

(defun print-param-declon (param pstate)
 (declare (xargs :guard (and (param-declonp param)
                             (pristatep pstate))))
 (declare
  (xargs :guard
         (and (param-declon-unambp param)
              (param-declon-aidentp param (pristate->gcc pstate)))))
 (let ((__function__ 'print-param-declon))
  (declare (ignorable __function__))
  (b*
   (((param-declon param) param)
    ((unless param.specs)
     (raise "Misusage error: no declaration specifiers.")
     (pristate-fix pstate))
    (pstate (print-decl-spec-list param.specs pstate))
    (pstate (print-param-declor param.declor pstate))
    (pstate
      (if
        (consp param.attribs)
        (b* ((pstate (print-astring " " pstate))
             (pstate (print-attrib-spec-list param.attribs pstate)))
          pstate)
        pstate)))
   pstate)))

Function: print-param-declon-list

(defun print-param-declon-list (params pstate)
 (declare (xargs :guard (and (param-declon-listp params)
                             (pristatep pstate))))
 (declare
  (xargs
   :guard
   (and (consp params)
        (param-declon-list-unambp params)
        (param-declon-list-aidentp params (pristate->gcc pstate)))))
 (let ((__function__ 'print-param-declon-list))
   (declare (ignorable __function__))
   (b* (((unless (mbt (consp params)))
         (pristate-fix pstate))
        (pstate (print-param-declon (car params)
                                    pstate))
        ((when (endp (cdr params))) pstate)
        (pstate (print-astring ", " pstate)))
     (print-param-declon-list (cdr params)
                              pstate))))

Function: print-param-declor

(defun print-param-declor (paramdeclor pstate)
 (declare (xargs :guard (and (param-declorp paramdeclor)
                             (pristatep pstate))))
 (declare
  (xargs
   :guard
   (and (param-declor-unambp paramdeclor)
        (param-declor-aidentp paramdeclor (pristate->gcc pstate)))))
 (let ((__function__ 'print-param-declor))
   (declare (ignorable __function__))
   (param-declor-case
        paramdeclor :nonabstract
        (b* ((pstate (print-astring " " pstate))
             (pstate (print-declor paramdeclor.declor pstate)))
          pstate)
        :abstract
        (b* ((pstate (print-astring " " pstate))
             (pstate (print-absdeclor paramdeclor.declor pstate)))
          pstate)
        :none (pristate-fix pstate)
        :ambig (prog2$ (impossible)
                       (pristate-fix pstate)))))

Function: print-tyname

(defun print-tyname (tyname pstate)
 (declare (xargs :guard (and (tynamep tyname)
                             (pristatep pstate))))
 (declare
  (xargs
       :guard (and (tyname-unambp tyname)
                   (tyname-aidentp tyname (pristate->gcc pstate)))))
 (let ((__function__ 'print-tyname))
  (declare (ignorable __function__))
  (b*
   (((tyname tyname) tyname)
    ((unless tyname.specquals)
     (raise
         "Misusage error: empty list of specifiers and qualifiers.")
     (pristate-fix pstate))
    (pstate (print-spec/qual-list tyname.specquals pstate))
    ((unless (absdeclor-option-case tyname.declor? :some))
     pstate)
    (pstate (print-astring " " pstate))
    (pstate
        (print-absdeclor (absdeclor-option-some->val tyname.declor?)
                         pstate)))
   pstate)))

Function: print-struni-spec

(defun print-struni-spec (struni-spec pstate)
 (declare (xargs :guard (and (struni-specp struni-spec)
                             (pristatep pstate))))
 (declare
  (xargs
    :guard
    (and (struni-spec-unambp struni-spec)
         (struni-spec-aidentp struni-spec (pristate->gcc pstate)))))
 (let ((__function__ 'print-struni-spec))
  (declare (ignorable __function__))
  (b*
   (((struni-spec struni-spec) struni-spec)
    (pstate
      (if
       (consp struni-spec.attribs)
       (b*
         ((pstate (print-astring " " pstate))
          (pstate
               (print-attrib-spec-list struni-spec.attribs pstate)))
         pstate)
       pstate))
    ((unless (or (ident-option-case struni-spec.name? :some)
                 struni-spec.members))
     (raise "Misusage error: empty structure or union specifier.")
     (pristate-fix pstate))
    (pstate (ident-option-case
                 struni-spec.name?
                 :some (print-ident struni-spec.name?.val pstate)
                 :none pstate))
    (pstate (if (and struni-spec.name? struni-spec.members)
                (print-astring " " pstate)
              pstate))
    ((when (not struni-spec.members))
     pstate)
    (pstate (print-astring "{ " pstate))
    (pstate (print-struct-declon-list struni-spec.members pstate))
    (pstate (print-astring " }" pstate)))
   pstate)))

Function: print-struct-declon

(defun print-struct-declon (structdeclon pstate)
 (declare (xargs :guard (and (struct-declonp structdeclon)
                             (pristatep pstate))))
 (declare
  (xargs
   :guard
   (and
      (struct-declon-unambp structdeclon)
      (struct-declon-aidentp structdeclon (pristate->gcc pstate)))))
 (let ((__function__ 'print-struct-declon))
  (declare (ignorable __function__))
  (struct-declon-case
   structdeclon :member
   (b*
    ((pstate (if structdeclon.extension
                 (print-astring "__extension__ " pstate)
               (pristate-fix pstate)))
     ((unless structdeclon.specquals)
      (raise "Misusage error: empty specifier/qualifier list.")
      pstate)
     (pstate (print-spec/qual-list structdeclon.specquals pstate))
     (pstate
      (if structdeclon.declors
       (b*
        ((pstate (print-astring " " pstate))
         (pstate
            (print-struct-declor-list structdeclon.declors pstate)))
        pstate)
       pstate))
     (pstate
      (if structdeclon.attribs
       (b*
        ((pstate (print-astring " " pstate))
         (pstate
              (print-attrib-spec-list structdeclon.attribs pstate)))
        pstate)
       pstate))
     (pstate (print-astring ";" pstate)))
    pstate)
   :statassert (print-statassert structdeclon.unwrap pstate)
   :empty (print-astring ";" pstate))))

Function: print-struct-declon-list

(defun print-struct-declon-list (structdeclons pstate)
 (declare (xargs :guard (and (struct-declon-listp structdeclons)
                             (pristatep pstate))))
 (declare
    (xargs :guard (and (consp structdeclons)
                       (struct-declon-list-unambp structdeclons)
                       (struct-declon-list-aidentp
                            structdeclons (pristate->gcc pstate)))))
 (let ((__function__ 'print-struct-declon-list))
   (declare (ignorable __function__))
   (b* (((unless (mbt (consp structdeclons)))
         (pristate-fix pstate))
        (pstate (print-struct-declon (car structdeclons)
                                     pstate))
        ((when (endp (cdr structdeclons)))
         pstate)
        (pstate (print-astring " " pstate)))
     (print-struct-declon-list (cdr structdeclons)
                               pstate))))

Function: print-struct-declor

(defun print-struct-declor (structdeclor pstate)
 (declare (xargs :guard (and (struct-declorp structdeclor)
                             (pristatep pstate))))
 (declare
  (xargs
   :guard
   (and
      (struct-declor-unambp structdeclor)
      (struct-declor-aidentp structdeclor (pristate->gcc pstate)))))
 (let ((__function__ 'print-struct-declor))
  (declare (ignorable __function__))
  (b*
   (((struct-declor structdeclor)
     structdeclor)
    ((unless (or (declor-option-case structdeclor.declor? :some)
                 (const-expr-option-case structdeclor.expr? :some)))
     (raise "Misusage error: empty structure declarator.")
     (pristate-fix pstate))
    (pstate
         (declor-option-case
              structdeclor.declor?
              :some (print-declor structdeclor.declor?.val pstate)
              :none pstate))
    (pstate
         (if (and (declor-option-case structdeclor.declor? :some)
                  (const-expr-option-case structdeclor.expr? :some))
             (print-astring " " pstate)
           pstate))
    (pstate
     (const-expr-option-case
       structdeclor.expr? :some
       (b*
         ((pstate (print-astring ": " pstate))
          (pstate (print-const-expr structdeclor.expr?.val pstate)))
         pstate)
       :none pstate)))
   pstate)))

Function: print-struct-declor-list

(defun print-struct-declor-list (structdeclors pstate)
 (declare (xargs :guard (and (struct-declor-listp structdeclors)
                             (pristatep pstate))))
 (declare
    (xargs :guard (and (consp structdeclors)
                       (struct-declor-list-unambp structdeclors)
                       (struct-declor-list-aidentp
                            structdeclors (pristate->gcc pstate)))))
 (let ((__function__ 'print-struct-declor-list))
   (declare (ignorable __function__))
   (b* (((unless (mbt (consp structdeclors)))
         (pristate-fix pstate))
        (pstate (print-struct-declor (car structdeclors)
                                     pstate))
        ((when (endp (cdr structdeclors)))
         pstate)
        (pstate (print-astring ", " pstate)))
     (print-struct-declor-list (cdr structdeclors)
                               pstate))))

Function: print-enum-spec

(defun print-enum-spec (enumspec pstate)
 (declare (xargs :guard (and (enum-specp enumspec)
                             (pristatep pstate))))
 (declare
  (xargs :guard
         (and (enum-spec-unambp enumspec)
              (enum-spec-aidentp enumspec (pristate->gcc pstate)))))
 (let ((__function__ 'print-enum-spec))
  (declare (ignorable __function__))
  (b*
   (((enum-spec enumspec) enumspec)
    ((unless (or (ident-option-case enumspec.name :some)
                 enumspec.list))
     (raise "Misusage error: empty enumeration specifiers.")
     (pristate-fix pstate))
    (pstate
     (ident-option-case enumspec.name
                        :some (print-ident enumspec.name.val pstate)
                        :none pstate))
    (pstate (if (and (ident-option-case enumspec.name :some)
                     enumspec.list)
                (print-astring " " pstate)
              pstate))
    ((unless enumspec.list) pstate)
    (pstate (print-astring "{" pstate))
    (pstate (print-enumer-list enumspec.list pstate))
    (pstate (if enumspec.final-comma (print-astring ", }" pstate)
              (print-astring "}" pstate))))
   pstate)))

Function: print-enumer

(defun print-enumer (enumer pstate)
 (declare (xargs :guard (and (enumerp enumer)
                             (pristatep pstate))))
 (declare
  (xargs
       :guard (and (enumer-unambp enumer)
                   (enumer-aidentp enumer (pristate->gcc pstate)))))
 (let ((__function__ 'print-enumer))
  (declare (ignorable __function__))
  (b*
   (((enumer enumer) enumer)
    (pstate (print-ident enumer.name pstate))
    ((unless (const-expr-option-case enumer.value :some))
     pstate)
    (pstate (print-astring " = " pstate))
    (pstate
        (print-const-expr (const-expr-option-some->val enumer.value)
                          pstate)))
   pstate)))

Function: print-enumer-list

(defun print-enumer-list (enumers pstate)
 (declare (xargs :guard (and (enumer-listp enumers)
                             (pristatep pstate))))
 (declare
   (xargs
        :guard
        (and (consp enumers)
             (enumer-list-unambp enumers)
             (enumer-list-aidentp enumers (pristate->gcc pstate)))))
 (let ((__function__ 'print-enumer-list))
   (declare (ignorable __function__))
   (b* (((unless (mbt (consp enumers)))
         (pristate-fix pstate))
        (pstate (print-enumer (car enumers) pstate))
        ((when (endp (cdr enumers))) pstate)
        (pstate (print-astring ", " pstate)))
     (print-enumer-list (cdr enumers)
                        pstate))))

Function: print-statassert

(defun print-statassert (statassert pstate)
 (declare (xargs :guard (and (statassertp statassert)
                             (pristatep pstate))))
 (declare
  (xargs
      :guard
      (and (statassert-unambp statassert)
           (statassert-aidentp statassert (pristate->gcc pstate)))))
 (let ((__function__ 'print-statassert))
  (declare (ignorable __function__))
  (b*
   (((statassert statassert) statassert)
    (pstate (print-astring "_Static_assert(" pstate))
    (pstate (print-const-expr statassert.test pstate))
    (pstate (print-astring ", " pstate))
    ((unless statassert.message)
     (raise
      "Misusage error: ~
                  empty message in static assertion declaration.")
     pstate)
    (pstate (print-stringlit-list statassert.message pstate))
    (pstate (print-astring ");" pstate)))
   pstate)))

Function: print-attrib

(defun print-attrib (attr pstate)
 (declare (xargs :guard (and (attribp attr)
                             (pristatep pstate))))
 (declare
      (xargs :guard (attrib-aidentp attr (pristate->gcc pstate))))
 (let ((__function__ 'print-attrib))
  (declare (ignorable __function__))
  (attrib-case
   attr :name-only
   (print-attrib-name attr.name pstate)
   :name-param
   (b*
    ((pstate (print-attrib-name attr.name pstate))
     (pstate (print-astring "(" pstate))
     ((unless (expr-list-unambp attr.param))
      (raise
           "Internal error: ambiguous expressions in attribute ~x0."
           (attrib-fix attr))
      pstate)
     (pstate (if attr.param (print-expr-list attr.param pstate)
               pstate))
     (pstate (print-astring ")" pstate)))
    pstate))))

Function: print-attrib-list

(defun print-attrib-list (attrs pstate)
 (declare (xargs :guard (and (attrib-listp attrs)
                             (pristatep pstate))))
 (declare
  (xargs
   :guard (and (consp attrs)
               (attrib-list-aidentp attrs (pristate->gcc pstate)))))
 (let ((__function__ 'print-attrib-list))
   (declare (ignorable __function__))
   (b* (((unless (mbt (consp attrs)))
         (pristate-fix pstate))
        (pstate (print-attrib (car attrs) pstate))
        ((when (endp (cdr attrs))) pstate)
        (pstate (print-astring ", " pstate)))
     (print-attrib-list (cdr attrs)
                        pstate))))

Function: print-attrib-spec

(defun print-attrib-spec (attrspec pstate)
 (declare (xargs :guard (and (attrib-specp attrspec)
                             (pristatep pstate))))
 (declare
  (xargs
      :guard (attrib-spec-aidentp attrspec (pristate->gcc pstate))))
 (let ((__function__ 'print-attrib-spec))
  (declare (ignorable __function__))
  (b*
   (((attrib-spec attrspec) attrspec)
    (pstate
      (if attrspec.uscores (print-astring "__attribute__ ((" pstate)
        (print-astring "__attribute ((" pstate)))
    (pstate (if (consp attrspec.attribs)
                (print-attrib-list attrspec.attribs pstate)
              pstate))
    (pstate (print-astring "))" pstate)))
   pstate)))

Function: print-attrib-spec-list

(defun print-attrib-spec-list (attrspecs pstate)
 (declare (xargs :guard (and (attrib-spec-listp attrspecs)
                             (pristatep pstate))))
 (declare
  (xargs
   :guard
   (and
      (consp attrspecs)
      (attrib-spec-list-aidentp attrspecs (pristate->gcc pstate)))))
 (let ((__function__ 'print-attrib-spec-list))
   (declare (ignorable __function__))
   (b* (((unless (mbt (consp attrspecs)))
         (pristate-fix pstate))
        (pstate (print-attrib-spec (car attrspecs)
                                   pstate))
        ((when (endp (cdr attrspecs))) pstate)
        (pstate (print-astring " " pstate)))
     (print-attrib-spec-list (cdr attrspecs)
                             pstate))))

Function: print-initdeclor

(defun print-initdeclor (initdeclor pstate)
 (declare (xargs :guard (and (initdeclorp initdeclor)
                             (pristatep pstate))))
 (declare
  (xargs
      :guard
      (and (initdeclor-unambp initdeclor)
           (initdeclor-aidentp initdeclor (pristate->gcc pstate)))))
 (let ((__function__ 'print-initdeclor))
  (declare (ignorable __function__))
  (b*
   (((initdeclor initdeclor) initdeclor)
    (pstate (print-declor initdeclor.declor pstate))
    (pstate
     (if initdeclor.asm?
         (b* ((pstate (print-astring " " pstate))
              (pstate (print-asm-name-spec initdeclor.asm? pstate)))
           pstate)
       pstate))
    (pstate
     (if
      (consp initdeclor.attribs)
      (b*
       ((pstate (print-astring " " pstate))
        (pstate (print-attrib-spec-list initdeclor.attribs pstate)))
       pstate)
      pstate))
    ((when (initer-option-case initdeclor.init? :none))
     pstate)
    (pstate (print-astring " = " pstate))
    (pstate (print-initer (initer-option-some->val initdeclor.init?)
                          pstate)))
   pstate)))

Function: print-initdeclor-list

(defun print-initdeclor-list (initdeclors pstate)
 (declare (xargs :guard (and (initdeclor-listp initdeclors)
                             (pristatep pstate))))
 (declare
  (xargs
   :guard
   (and
     (consp initdeclors)
     (initdeclor-list-unambp initdeclors)
     (initdeclor-list-aidentp initdeclors (pristate->gcc pstate)))))
 (let ((__function__ 'print-initdeclor-list))
   (declare (ignorable __function__))
   (b* (((unless (mbt (consp initdeclors)))
         (pristate-fix pstate))
        (pstate (print-initdeclor (car initdeclors)
                                  pstate))
        ((when (endp (cdr initdeclors))) pstate)
        (pstate (print-astring ", " pstate)))
     (print-initdeclor-list (cdr initdeclors)
                            pstate))))

Function: print-decl-inline

(defun print-decl-inline (decl pstate)
 (declare (xargs :guard (and (declp decl) (pristatep pstate))))
 (declare
    (xargs :guard (and (decl-unambp decl)
                       (decl-aidentp decl (pristate->gcc pstate)))))
 (let ((__function__ 'print-decl-inline))
  (declare (ignorable __function__))
  (decl-case
   decl :decl
   (b*
    ((pstate
          (if decl.extension (print-astring "__extension__ " pstate)
            (pristate-fix pstate)))
     ((unless decl.specs)
      (raise
       "Misusage error: ~
                 no declaration specifiers in declaration ~x0."
       decl)
      pstate)
     (pstate (print-decl-spec-list decl.specs pstate))
     (pstate
         (if decl.init
             (b* ((pstate (print-astring " " pstate))
                  (pstate (print-initdeclor-list decl.init pstate)))
               pstate)
           pstate))
     (pstate (print-astring ";" pstate)))
    pstate)
   :statassert (print-statassert decl.unwrap pstate))))

Function: print-decl

(defun print-decl (decl pstate)
 (declare (xargs :guard (and (declp decl) (pristatep pstate))))
 (declare
    (xargs :guard (and (decl-unambp decl)
                       (decl-aidentp decl (pristate->gcc pstate)))))
 (let ((__function__ 'print-decl))
   (declare (ignorable __function__))
   (b* ((pstate (print-indent pstate))
        (pstate (print-decl-inline decl pstate))
        (pstate (print-new-line pstate)))
     pstate)))

Function: print-decl-list

(defun print-decl-list (decls pstate)
 (declare (xargs :guard (and (decl-listp decls)
                             (pristatep pstate))))
 (declare
  (xargs
     :guard (and (consp decls)
                 (decl-list-unambp decls)
                 (decl-list-aidentp decls (pristate->gcc pstate)))))
 (let ((__function__ 'print-decl-list))
   (declare (ignorable __function__))
   (b* (((unless (mbt (consp decls)))
         (pristate-fix pstate))
        (pstate (print-decl (car decls) pstate))
        ((when (endp (cdr decls))) pstate))
     (print-decl-list (cdr decls) pstate))))

Function: print-label

(defun print-label (label pstate)
 (declare (xargs :guard (and (labelp label)
                             (pristatep pstate))))
 (declare
  (xargs :guard (and (label-unambp label)
                     (label-aidentp label (pristate->gcc pstate)))))
 (let ((__function__ 'print-label))
  (declare (ignorable __function__))
  (label-case
   label :name
   (b*
    ((pstate (print-ident label.name pstate))
     (pstate
       (if
        (consp label.attribs)
        (b* ((pstate (print-astring " " pstate))
             (pstate (print-attrib-spec-list label.attribs pstate)))
          pstate)
        pstate)))
    pstate)
   :casexpr
   (b* ((pstate (print-astring "case " pstate))
        (pstate (print-const-expr label.expr pstate)))
     (const-expr-option-case
          label.range? :some
          (b* ((pstate (print-astring " ... " pstate))
               (pstate (print-const-expr label.range?.val pstate)))
            pstate)
          :none pstate))
   :default (print-astring "default" pstate))))

Function: print-asm-output

(defun print-asm-output (output pstate)
 (declare (xargs :guard (and (asm-outputp output)
                             (pristatep pstate))))
 (declare
  (xargs :guard (asm-output-aidentp output (pristate->gcc pstate))))
 (let ((__function__ 'print-asm-output))
  (declare (ignorable __function__))
  (b*
   (((asm-output output) output)
    (pstate
      (if output.name (b* ((pstate (print-astring "[" pstate))
                           (pstate (print-ident output.name pstate))
                           (pstate (print-astring "] " pstate)))
                        pstate)
        pstate))
    (pstate
     (if (consp output.constraint)
         (print-stringlit-list output.constraint pstate)
      (prog2$
       (raise
        "Misusage error: ~
                          no constraint in assembler output operand ~x0."
        (asm-output-fix output))
       pstate)))
    (pstate (print-astring " (" pstate))
    ((unless (expr-unambp output.lvalue))
     (raise
      "Internal error: ~
                ambiguous expression ~x0 in assembler output operand."
      output.lvalue)
     pstate)
    (pstate (print-expr output.lvalue (expr-priority-expr)
                        pstate))
    (pstate (print-astring ")" pstate)))
   pstate)))

Function: print-asm-output-list

(defun print-asm-output-list (outputs pstate)
 (declare (xargs :guard (and (asm-output-listp outputs)
                             (pristatep pstate))))
 (declare
  (xargs
    :guard
    (and (consp outputs)
         (asm-output-list-aidentp outputs (pristate->gcc pstate)))))
 (let ((__function__ 'print-asm-output-list))
   (declare (ignorable __function__))
   (b* (((unless (mbt (consp outputs)))
         (pristate-fix pstate))
        (pstate (print-asm-output (car outputs) pstate))
        ((when (endp (cdr outputs))) pstate)
        (pstate (print-astring ", " pstate)))
     (print-asm-output-list (cdr outputs)
                            pstate))))

Function: print-asm-input

(defun print-asm-input (input pstate)
 (declare (xargs :guard (and (asm-inputp input)
                             (pristatep pstate))))
 (declare
    (xargs :guard (asm-input-aidentp input (pristate->gcc pstate))))
 (let ((__function__ 'print-asm-input))
  (declare (ignorable __function__))
  (b*
   (((asm-input input) input)
    (pstate
        (if input.name (b* ((pstate (print-astring "[" pstate))
                            (pstate (print-ident input.name pstate))
                            (pstate (print-astring "] " pstate)))
                         pstate)
          pstate))
    (pstate
     (if (consp input.constraint)
         (print-stringlit-list input.constraint pstate)
      (prog2$
       (raise
        "Misusage error: ~
                          no constraint in assembler input operand ~x0."
        (asm-input-fix input))
       pstate)))
    (pstate (print-astring " (" pstate))
    ((unless (expr-unambp input.rvalue))
     (raise
      "Internal error: ~
                ambiguous expression ~x0 in assembler input operand."
      input.rvalue)
     pstate)
    (pstate (print-expr input.rvalue (expr-priority-expr)
                        pstate))
    (pstate (print-astring ")" pstate)))
   pstate)))

Function: print-asm-input-list

(defun print-asm-input-list (inputs pstate)
 (declare (xargs :guard (and (asm-input-listp inputs)
                             (pristatep pstate))))
 (declare
  (xargs
      :guard
      (and (consp inputs)
           (asm-input-list-aidentp inputs (pristate->gcc pstate)))))
 (let ((__function__ 'print-asm-input-list))
   (declare (ignorable __function__))
   (b* (((unless (mbt (consp inputs)))
         (pristate-fix pstate))
        (pstate (print-asm-input (car inputs) pstate))
        ((when (endp (cdr inputs))) pstate)
        (pstate (print-astring ", " pstate)))
     (print-asm-input-list (cdr inputs)
                           pstate))))

Function: print-asm-stmt

(defun print-asm-stmt (asm pstate)
 (declare (xargs :guard (and (asm-stmtp asm)
                             (pristatep pstate))))
 (declare
      (xargs :guard (asm-stmt-aidentp asm (pristate->gcc pstate))))
 (let ((__function__ 'print-asm-stmt))
  (declare (ignorable __function__))
  (b*
   (((asm-stmt stmt) asm)
    (pstate (print-indent pstate))
    (pstate
      (keyword-uscores-case stmt.uscores
                            :none (print-astring "asm" pstate)
                            :start (print-astring "__asm" pstate)
                            :both (print-astring "__asm__" pstate)))
    (pstate
         (if (consp stmt.quals)
             (b* ((pstate (print-astring " " pstate))
                  (pstate (print-asm-qual-list stmt.quals pstate)))
               pstate)
           pstate))
    (pstate (print-astring " (" pstate))
    ((unless (consp stmt.template))
     (raise
        "Misusage error: no string literals in assembler template.")
     pstate)
    (pstate (print-stringlit-list stmt.template pstate))
    ((unless (case stmt.num-colons
               (0 (and (endp stmt.outputs)
                       (endp stmt.inputs)
                       (endp stmt.clobbers)
                       (endp stmt.labels)))
               (1 (and (endp stmt.inputs)
                       (endp stmt.clobbers)
                       (endp stmt.labels)))
               (2 (and (endp stmt.clobbers)
                       (endp stmt.labels)))
               (3 (endp stmt.labels))
               (4 t)
               (otherwise nil)))
     (raise
      "Misusage error: ~
                  non-empty outputs, inputs, clobbers, or labels ~
                  with insufficient number of colons ~
                  in assembler statement ~x0."
      (asm-stmt-fix stmt))
     pstate)
    (pstate
     (if
      (>= stmt.num-colons 1)
      (b*
       ((pstate (print-astring " :" pstate))
        (pstate
         (if
          (consp stmt.outputs)
          (b* ((pstate (print-astring " " pstate))
               (pstate (print-asm-output-list stmt.outputs pstate)))
            pstate)
          pstate)))
       pstate)
      pstate))
    (pstate
     (if
      (>= stmt.num-colons 2)
      (b*
       ((pstate (print-astring " :" pstate))
        (pstate
          (if
            (consp stmt.inputs)
            (b* ((pstate (print-astring " " pstate))
                 (pstate (print-asm-input-list stmt.inputs pstate)))
              pstate)
            pstate)))
       pstate)
      pstate))
    (pstate
     (if
      (>= stmt.num-colons 3)
      (b*
       ((pstate (print-astring " :" pstate))
        (pstate
          (if
           (consp stmt.clobbers)
           (b*
            ((pstate (print-astring " " pstate))
             (pstate (print-asm-clobber-list stmt.clobbers pstate)))
            pstate)
           pstate)))
       pstate)
      pstate))
    (pstate
     (if
      (>= stmt.num-colons 4)
      (b*
       ((pstate (print-astring " :" pstate))
        (pstate
            (if (consp stmt.labels)
                (b* ((pstate (print-astring " " pstate))
                     (pstate (print-ident-list stmt.labels pstate)))
                  pstate)
              pstate)))
       pstate)
      pstate))
    (pstate (print-astring " );" pstate))
    (pstate (print-new-line pstate)))
   pstate)))

Function: print-stmt

(defun print-stmt (stmt pstate)
 (declare (xargs :guard (and (stmtp stmt) (pristatep pstate))))
 (declare
    (xargs :guard (and (stmt-unambp stmt)
                       (stmt-aidentp stmt (pristate->gcc pstate)))))
 (let ((__function__ 'print-stmt))
  (declare (ignorable __function__))
  (stmt-case
   stmt :labeled
   (b* ((pstate (print-indent pstate))
        (pstate (print-label stmt.label pstate))
        (pstate (print-astring ":" pstate)))
     (if
       (stmt-case stmt.stmt :compound)
       (b* ((pstate (print-astring " " pstate))
            (pstate (print-comp-stmt (stmt-compound->stmt stmt.stmt)
                                     pstate))
            (pstate (print-new-line pstate)))
         pstate)
       (b* ((pstate (print-new-line pstate))
            (pstate (inc-pristate-indent pstate))
            (pstate (print-stmt stmt.stmt pstate))
            (pstate (dec-pristate-indent pstate)))
         pstate)))
   :compound
   (b* ((pstate (print-indent pstate))
        (pstate (print-comp-stmt stmt.stmt pstate))
        (pstate (print-new-line pstate)))
     pstate)
   :expr
   (b*
    ((pstate (print-indent pstate))
     (pstate
          (expr-option-case
               stmt.expr?
               :some (print-expr (expr-option-some->val stmt.expr?)
                                 (expr-priority-expr)
                                 pstate)
               :none pstate))
     (pstate (print-astring ";" pstate))
     (pstate (print-new-line pstate)))
    pstate)
   :if
   (b* ((pstate (print-indent pstate))
        (pstate (print-astring "if (" pstate))
        (pstate (print-expr stmt.test (expr-priority-expr)
                            pstate))
        (pstate (print-astring ")" pstate)))
     (if
       (stmt-case stmt.then :compound)
       (b* ((pstate (print-astring " " pstate))
            (pstate (print-comp-stmt (stmt-compound->stmt stmt.then)
                                     pstate))
            (pstate (print-new-line pstate)))
         pstate)
       (b* ((pstate (print-new-line pstate))
            (pstate (inc-pristate-indent pstate))
            (pstate (print-stmt stmt.then pstate))
            (pstate (dec-pristate-indent pstate)))
         pstate)))
   :ifelse
   (b*
    ((pstate (print-indent pstate))
     (pstate (print-astring "if (" pstate))
     (pstate (print-expr stmt.test (expr-priority-expr)
                         pstate))
     (pstate (print-astring ")" pstate))
     (pstate
      (if
       (stmt-case stmt.then :compound)
       (b* ((pstate (print-astring " " pstate))
            (pstate (print-comp-stmt (stmt-compound->stmt stmt.then)
                                     pstate))
            (pstate (print-astring " " pstate)))
         pstate)
       (b* ((pstate (print-new-line pstate))
            (pstate (inc-pristate-indent pstate))
            (pstate (print-stmt stmt.then pstate))
            (pstate (dec-pristate-indent pstate)))
         pstate)))
     (pstate (if (stmt-case stmt.then :compound)
                 pstate
               (print-indent pstate)))
     (pstate (print-astring "else" pstate))
     (pstate
      (if
       (stmt-case stmt.else :compound)
       (b* ((pstate (print-astring " " pstate))
            (pstate (print-comp-stmt (stmt-compound->stmt stmt.else)
                                     pstate))
            (pstate (print-new-line pstate)))
         pstate)
       (b* ((pstate (print-new-line pstate))
            (pstate (inc-pristate-indent pstate))
            (pstate (print-stmt stmt.else pstate))
            (pstate (dec-pristate-indent pstate)))
         pstate))))
    pstate)
   :switch
   (b* ((pstate (print-indent pstate))
        (pstate (print-astring "switch (" pstate))
        (pstate (print-expr stmt.target (expr-priority-expr)
                            pstate))
        (pstate (print-astring ")" pstate)))
     (if
       (stmt-case stmt.body :compound)
       (b* ((pstate (print-astring " " pstate))
            (pstate (print-comp-stmt (stmt-compound->stmt stmt.body)
                                     pstate))
            (pstate (print-new-line pstate)))
         pstate)
       (b* ((pstate (print-new-line pstate))
            (pstate (inc-pristate-indent pstate))
            (pstate (print-stmt stmt.body pstate))
            (pstate (dec-pristate-indent pstate)))
         pstate)))
   :while
   (b* ((pstate (print-indent pstate))
        (pstate (print-astring "while (" pstate))
        (pstate (print-expr stmt.test (expr-priority-expr)
                            pstate))
        (pstate (print-astring ")" pstate)))
     (if
       (stmt-case stmt.body :compound)
       (b* ((pstate (print-astring " " pstate))
            (pstate (print-comp-stmt (stmt-compound->stmt stmt.body)
                                     pstate))
            (pstate (print-new-line pstate)))
         pstate)
       (b* ((pstate (print-new-line pstate))
            (pstate (inc-pristate-indent pstate))
            (pstate (print-stmt stmt.body pstate))
            (pstate (dec-pristate-indent pstate)))
         pstate)))
   :dowhile
   (b*
    ((pstate (print-indent pstate))
     (pstate (print-astring "do" pstate))
     (pstate
      (if
       (stmt-case stmt.body :compound)
       (b* ((pstate (print-astring " " pstate))
            (pstate (print-comp-stmt (stmt-compound->stmt stmt.body)
                                     pstate))
            (pstate (print-astring " " pstate)))
         pstate)
       (b* ((pstate (print-new-line pstate))
            (pstate (inc-pristate-indent pstate))
            (pstate (print-stmt stmt.body pstate))
            (pstate (dec-pristate-indent pstate))
            (pstate (print-indent pstate)))
         pstate)))
     (pstate (print-astring "while (" pstate))
     (pstate (print-expr stmt.test (expr-priority-expr)
                         pstate))
     (pstate (print-astring ");" pstate))
     (pstate (print-new-line pstate)))
    pstate)
   :for-expr
   (b*
    ((pstate (print-indent pstate))
     (pstate (print-astring "for (" pstate))
     (pstate
          (expr-option-case
               stmt.init
               :some (print-expr stmt.init.val (expr-priority-expr)
                                 pstate)
               :none (print-astring " " pstate)))
     (pstate (print-astring "; " pstate))
     (pstate
          (expr-option-case
               stmt.test
               :some (print-expr stmt.test.val (expr-priority-expr)
                                 pstate)
               :none pstate))
     (pstate (print-astring "; " pstate))
     (pstate
          (expr-option-case
               stmt.next
               :some (print-expr stmt.next.val (expr-priority-expr)
                                 pstate)
               :none pstate))
     (pstate (print-astring ")" pstate)))
    (if
      (stmt-case stmt.body :compound)
      (b* ((pstate (print-astring " " pstate))
           (pstate (print-comp-stmt (stmt-compound->stmt stmt.body)
                                    pstate))
           (pstate (print-new-line pstate)))
        pstate)
      (b* ((pstate (print-new-line pstate))
           (pstate (inc-pristate-indent pstate))
           (pstate (print-stmt stmt.body pstate))
           (pstate (dec-pristate-indent pstate)))
        pstate)))
   :for-decl
   (b*
    ((pstate (print-indent pstate))
     (pstate (print-astring "for (" pstate))
     (pstate (print-decl-inline stmt.init pstate))
     (pstate (print-astring " " pstate))
     (pstate
          (expr-option-case
               stmt.test
               :some (print-expr stmt.test.val (expr-priority-expr)
                                 pstate)
               :none pstate))
     (pstate (print-astring "; " pstate))
     (pstate
          (expr-option-case
               stmt.next
               :some (print-expr stmt.next.val (expr-priority-expr)
                                 pstate)
               :none pstate))
     (pstate (print-astring ")" pstate)))
    (if
      (stmt-case stmt.body :compound)
      (b* ((pstate (print-astring " " pstate))
           (pstate (print-comp-stmt (stmt-compound->stmt stmt.body)
                                    pstate))
           (pstate (print-new-line pstate)))
        pstate)
      (b* ((pstate (print-new-line pstate))
           (pstate (inc-pristate-indent pstate))
           (pstate (print-stmt stmt.body pstate))
           (pstate (dec-pristate-indent pstate)))
        pstate)))
   :for-ambig
   (prog2$ (impossible)
           (pristate-fix pstate))
   :goto
   (b* ((pstate (print-indent pstate))
        (pstate (print-astring "goto " pstate))
        (pstate (print-ident stmt.label pstate))
        (pstate (print-astring ";" pstate))
        (pstate (print-new-line pstate)))
     pstate)
   :gotoe
   (b* ((pstate (print-indent pstate))
        (pstate (print-astring "goto " pstate))
        (pstate (print-expr stmt.label (expr-priority-expr)
                            pstate))
        (pstate (print-astring ";" pstate))
        (pstate (print-new-line pstate)))
     pstate)
   :continue
   (b* ((pstate (print-indent pstate))
        (pstate (print-astring "continue;" pstate))
        (pstate (print-new-line pstate)))
     pstate)
   :break
   (b* ((pstate (print-indent pstate))
        (pstate (print-astring "break;" pstate))
        (pstate (print-new-line pstate)))
     pstate)
   :return
   (b*
    ((pstate (print-indent pstate))
     (pstate (print-astring "return" pstate))
     (pstate
      (expr-option-case
         stmt.expr? :some
         (b* ((pstate (print-astring " " pstate))
              (pstate (print-expr (expr-option-some->val stmt.expr?)
                                  (expr-priority-expr)
                                  pstate)))
           pstate)
         :none pstate))
     (pstate (print-astring ";" pstate))
     (pstate (print-new-line pstate)))
    pstate)
   :asm (print-asm-stmt stmt.unwrap pstate))))

Function: print-comp-stmt

(defun print-comp-stmt (cstmt pstate)
 (declare (xargs :guard (and (comp-stmtp cstmt)
                             (pristatep pstate))))
 (declare
  (xargs
     :guard (and (comp-stmt-unambp cstmt)
                 (comp-stmt-aidentp cstmt (pristate->gcc pstate)))))
 (let ((__function__ 'print-comp-stmt))
   (declare (ignorable __function__))
   (b* (((comp-stmt cstmt) cstmt)
        (pstate (print-astring "{" pstate))
        (pstate (print-new-line pstate))
        (pstate (inc-pristate-indent pstate))
        (pstate (print-label-declaration-list cstmt.labels pstate))
        (pstate (print-block-item-list cstmt.items pstate))
        (pstate (dec-pristate-indent pstate))
        (pstate (print-indent pstate))
        (pstate (print-astring "}" pstate)))
     pstate)))

Function: print-block-item

(defun print-block-item (item pstate)
 (declare (xargs :guard (and (block-itemp item)
                             (pristatep pstate))))
 (declare
  (xargs
     :guard (and (block-item-unambp item)
                 (block-item-aidentp item (pristate->gcc pstate)))))
 (let ((__function__ 'print-block-item))
   (declare (ignorable __function__))
   (block-item-case item
                    :decl (print-decl item.decl pstate)
                    :stmt (print-stmt item.stmt pstate)
                    :ambig (prog2$ (impossible)
                                   (pristate-fix pstate)))))

Function: print-block-item-list

(defun print-block-item-list (items pstate)
 (declare (xargs :guard (and (block-item-listp items)
                             (pristatep pstate))))
 (declare
  (xargs
      :guard
      (and (block-item-list-unambp items)
           (block-item-list-aidentp items (pristate->gcc pstate)))))
 (let ((__function__ 'print-block-item-list))
   (declare (ignorable __function__))
   (b* (((when (endp items))
         (pristate-fix pstate))
        (pstate (print-block-item (car items) pstate)))
     (print-block-item-list (cdr items)
                            pstate))))

Theorem: return-type-of-print-expr.new-pstate

(defthm return-type-of-print-expr.new-pstate
  (b* ((?new-pstate (print-expr expr expected-prio pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-expr-list.new-pstate

(defthm return-type-of-print-expr-list.new-pstate
  (b* ((?new-pstate (print-expr-list exprs pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-const-expr.new-pstate

(defthm return-type-of-print-const-expr.new-pstate
  (b* ((?new-pstate (print-const-expr cexpr pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-genassoc.new-pstate

(defthm return-type-of-print-genassoc.new-pstate
  (b* ((?new-pstate (print-genassoc genassoc pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-genassoc-list.new-pstate

(defthm return-type-of-print-genassoc-list.new-pstate
  (b* ((?new-pstate (print-genassoc-list genassocs pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-member-designor.new-pstate

(defthm return-type-of-print-member-designor.new-pstate
  (b* ((?new-pstate (print-member-designor memdes pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-type-spec.new-pstate

(defthm return-type-of-print-type-spec.new-pstate
  (b* ((?new-pstate (print-type-spec tyspec pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-spec/qual.new-pstate

(defthm return-type-of-print-spec/qual.new-pstate
  (b* ((?new-pstate (print-spec/qual specqual pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-spec/qual-list.new-pstate

(defthm return-type-of-print-spec/qual-list.new-pstate
  (b* ((?new-pstate (print-spec/qual-list specquals pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-align-spec.new-pstate

(defthm return-type-of-print-align-spec.new-pstate
  (b* ((?new-pstate (print-align-spec alignspec pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-decl-spec.new-pstate

(defthm return-type-of-print-decl-spec.new-pstate
  (b* ((?new-pstate (print-decl-spec declspec pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-decl-spec-list.new-pstate

(defthm return-type-of-print-decl-spec-list.new-pstate
  (b* ((?new-pstate (print-decl-spec-list declspecs pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-typequal/attribspec.new-pstate

(defthm return-type-of-print-typequal/attribspec.new-pstate
 (b* ((?new-pstate (print-typequal/attribspec tyqualattrib pstate)))
   (pristatep new-pstate))
 :rule-classes :rewrite)

Theorem: return-type-of-print-typequal/attribspec-list.new-pstate

(defthm return-type-of-print-typequal/attribspec-list.new-pstate
  (b* ((?new-pstate
            (print-typequal/attribspec-list tyqualattribs pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-typequal/attribspec-list-list.new-pstate

(defthm
      return-type-of-print-typequal/attribspec-list-list.new-pstate
 (b*
  ((?new-pstate
       (print-typequal/attribspec-list-list tyqualattribss pstate)))
  (pristatep new-pstate))
 :rule-classes :rewrite)

Theorem: return-type-of-print-initer.new-pstate

(defthm return-type-of-print-initer.new-pstate
  (b* ((?new-pstate (print-initer initer pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-desiniter.new-pstate

(defthm return-type-of-print-desiniter.new-pstate
  (b* ((?new-pstate (print-desiniter desiniter pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-desiniter-list.new-pstate

(defthm return-type-of-print-desiniter-list.new-pstate
  (b* ((?new-pstate (print-desiniter-list desiniters pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-designor.new-pstate

(defthm return-type-of-print-designor.new-pstate
  (b* ((?new-pstate (print-designor designor pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-designor-list.new-pstate

(defthm return-type-of-print-designor-list.new-pstate
  (b* ((?new-pstate (print-designor-list designors pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-declor.new-pstate

(defthm return-type-of-print-declor.new-pstate
  (b* ((?new-pstate (print-declor declor pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-dirdeclor.new-pstate

(defthm return-type-of-print-dirdeclor.new-pstate
  (b* ((?new-pstate (print-dirdeclor dirdeclor pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-absdeclor.new-pstate

(defthm return-type-of-print-absdeclor.new-pstate
  (b* ((?new-pstate (print-absdeclor absdeclor pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-dirabsdeclor.new-pstate

(defthm return-type-of-print-dirabsdeclor.new-pstate
  (b* ((?new-pstate (print-dirabsdeclor dirabsdeclor pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-param-declon.new-pstate

(defthm return-type-of-print-param-declon.new-pstate
  (b* ((?new-pstate (print-param-declon param pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-param-declon-list.new-pstate

(defthm return-type-of-print-param-declon-list.new-pstate
  (b* ((?new-pstate (print-param-declon-list params pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-param-declor.new-pstate

(defthm return-type-of-print-param-declor.new-pstate
  (b* ((?new-pstate (print-param-declor paramdeclor pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-tyname.new-pstate

(defthm return-type-of-print-tyname.new-pstate
  (b* ((?new-pstate (print-tyname tyname pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-struni-spec.new-pstate

(defthm return-type-of-print-struni-spec.new-pstate
  (b* ((?new-pstate (print-struni-spec struni-spec pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-struct-declon.new-pstate

(defthm return-type-of-print-struct-declon.new-pstate
  (b* ((?new-pstate (print-struct-declon structdeclon pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-struct-declon-list.new-pstate

(defthm return-type-of-print-struct-declon-list.new-pstate
 (b* ((?new-pstate (print-struct-declon-list structdeclons pstate)))
   (pristatep new-pstate))
 :rule-classes :rewrite)

Theorem: return-type-of-print-struct-declor.new-pstate

(defthm return-type-of-print-struct-declor.new-pstate
  (b* ((?new-pstate (print-struct-declor structdeclor pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-struct-declor-list.new-pstate

(defthm return-type-of-print-struct-declor-list.new-pstate
 (b* ((?new-pstate (print-struct-declor-list structdeclors pstate)))
   (pristatep new-pstate))
 :rule-classes :rewrite)

Theorem: return-type-of-print-enum-spec.new-pstate

(defthm return-type-of-print-enum-spec.new-pstate
  (b* ((?new-pstate (print-enum-spec enumspec pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-enumer.new-pstate

(defthm return-type-of-print-enumer.new-pstate
  (b* ((?new-pstate (print-enumer enumer pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-enumer-list.new-pstate

(defthm return-type-of-print-enumer-list.new-pstate
  (b* ((?new-pstate (print-enumer-list enumers pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-statassert.new-pstate

(defthm return-type-of-print-statassert.new-pstate
  (b* ((?new-pstate (print-statassert statassert pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-attrib.new-pstate

(defthm return-type-of-print-attrib.new-pstate
  (b* ((?new-pstate (print-attrib attr pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-attrib-list.new-pstate

(defthm return-type-of-print-attrib-list.new-pstate
  (b* ((?new-pstate (print-attrib-list attrs pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-attrib-spec.new-pstate

(defthm return-type-of-print-attrib-spec.new-pstate
  (b* ((?new-pstate (print-attrib-spec attrspec pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-attrib-spec-list.new-pstate

(defthm return-type-of-print-attrib-spec-list.new-pstate
  (b* ((?new-pstate (print-attrib-spec-list attrspecs pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-initdeclor.new-pstate

(defthm return-type-of-print-initdeclor.new-pstate
  (b* ((?new-pstate (print-initdeclor initdeclor pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-initdeclor-list.new-pstate

(defthm return-type-of-print-initdeclor-list.new-pstate
  (b* ((?new-pstate (print-initdeclor-list initdeclors pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-decl-inline.new-pstate

(defthm return-type-of-print-decl-inline.new-pstate
  (b* ((?new-pstate (print-decl-inline decl pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-decl.new-pstate

(defthm return-type-of-print-decl.new-pstate
  (b* ((?new-pstate (print-decl decl pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-decl-list.new-pstate

(defthm return-type-of-print-decl-list.new-pstate
  (b* ((?new-pstate (print-decl-list decls pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-label.new-pstate

(defthm return-type-of-print-label.new-pstate
  (b* ((?new-pstate (print-label label pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-asm-output.new-pstate

(defthm return-type-of-print-asm-output.new-pstate
  (b* ((?new-pstate (print-asm-output output pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-asm-output-list.new-pstate

(defthm return-type-of-print-asm-output-list.new-pstate
  (b* ((?new-pstate (print-asm-output-list outputs pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-asm-input.new-pstate

(defthm return-type-of-print-asm-input.new-pstate
  (b* ((?new-pstate (print-asm-input input pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-asm-input-list.new-pstate

(defthm return-type-of-print-asm-input-list.new-pstate
  (b* ((?new-pstate (print-asm-input-list inputs pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-asm-stmt.new-pstate

(defthm return-type-of-print-asm-stmt.new-pstate
  (b* ((?new-pstate (print-asm-stmt asm pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-stmt.new-pstate

(defthm return-type-of-print-stmt.new-pstate
  (b* ((?new-pstate (print-stmt stmt pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-comp-stmt.new-pstate

(defthm return-type-of-print-comp-stmt.new-pstate
  (b* ((?new-pstate (print-comp-stmt cstmt pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-block-item.new-pstate

(defthm return-type-of-print-block-item.new-pstate
  (b* ((?new-pstate (print-block-item item pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: return-type-of-print-block-item-list.new-pstate

(defthm return-type-of-print-block-item-list.new-pstate
  (b* ((?new-pstate (print-block-item-list items pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: print-expr-of-expr-fix-expr

(defthm print-expr-of-expr-fix-expr
  (equal (print-expr (expr-fix expr)
                     expected-prio pstate)
         (print-expr expr expected-prio pstate)))

Theorem: print-expr-of-expr-priority-fix-expected-prio

(defthm print-expr-of-expr-priority-fix-expected-prio
  (equal (print-expr expr (expr-priority-fix expected-prio)
                     pstate)
         (print-expr expr expected-prio pstate)))

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

(defthm print-expr-of-pristate-fix-pstate
  (equal (print-expr expr
                     expected-prio (pristate-fix pstate))
         (print-expr expr expected-prio pstate)))

Theorem: print-expr-list-of-expr-list-fix-exprs

(defthm print-expr-list-of-expr-list-fix-exprs
  (equal (print-expr-list (expr-list-fix exprs)
                          pstate)
         (print-expr-list exprs pstate)))

Theorem: print-expr-list-of-pristate-fix-pstate

(defthm print-expr-list-of-pristate-fix-pstate
  (equal (print-expr-list exprs (pristate-fix pstate))
         (print-expr-list exprs pstate)))

Theorem: print-const-expr-of-const-expr-fix-cexpr

(defthm print-const-expr-of-const-expr-fix-cexpr
  (equal (print-const-expr (const-expr-fix cexpr)
                           pstate)
         (print-const-expr cexpr pstate)))

Theorem: print-const-expr-of-pristate-fix-pstate

(defthm print-const-expr-of-pristate-fix-pstate
  (equal (print-const-expr cexpr (pristate-fix pstate))
         (print-const-expr cexpr pstate)))

Theorem: print-genassoc-of-genassoc-fix-genassoc

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

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

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

Theorem: print-genassoc-list-of-genassoc-list-fix-genassocs

(defthm print-genassoc-list-of-genassoc-list-fix-genassocs
  (equal (print-genassoc-list (genassoc-list-fix genassocs)
                              pstate)
         (print-genassoc-list genassocs pstate)))

Theorem: print-genassoc-list-of-pristate-fix-pstate

(defthm print-genassoc-list-of-pristate-fix-pstate
  (equal (print-genassoc-list genassocs (pristate-fix pstate))
         (print-genassoc-list genassocs pstate)))

Theorem: print-member-designor-of-member-designor-fix-memdes

(defthm print-member-designor-of-member-designor-fix-memdes
  (equal (print-member-designor (member-designor-fix memdes)
                                pstate)
         (print-member-designor memdes pstate)))

Theorem: print-member-designor-of-pristate-fix-pstate

(defthm print-member-designor-of-pristate-fix-pstate
  (equal (print-member-designor memdes (pristate-fix pstate))
         (print-member-designor memdes pstate)))

Theorem: print-type-spec-of-type-spec-fix-tyspec

(defthm print-type-spec-of-type-spec-fix-tyspec
  (equal (print-type-spec (type-spec-fix tyspec)
                          pstate)
         (print-type-spec tyspec pstate)))

Theorem: print-type-spec-of-pristate-fix-pstate

(defthm print-type-spec-of-pristate-fix-pstate
  (equal (print-type-spec tyspec (pristate-fix pstate))
         (print-type-spec tyspec pstate)))

Theorem: print-spec/qual-of-spec/qual-fix-specqual

(defthm print-spec/qual-of-spec/qual-fix-specqual
  (equal (print-spec/qual (spec/qual-fix specqual)
                          pstate)
         (print-spec/qual specqual pstate)))

Theorem: print-spec/qual-of-pristate-fix-pstate

(defthm print-spec/qual-of-pristate-fix-pstate
  (equal (print-spec/qual specqual (pristate-fix pstate))
         (print-spec/qual specqual pstate)))

Theorem: print-spec/qual-list-of-spec/qual-list-fix-specquals

(defthm print-spec/qual-list-of-spec/qual-list-fix-specquals
  (equal (print-spec/qual-list (spec/qual-list-fix specquals)
                               pstate)
         (print-spec/qual-list specquals pstate)))

Theorem: print-spec/qual-list-of-pristate-fix-pstate

(defthm print-spec/qual-list-of-pristate-fix-pstate
  (equal (print-spec/qual-list specquals (pristate-fix pstate))
         (print-spec/qual-list specquals pstate)))

Theorem: print-align-spec-of-align-spec-fix-alignspec

(defthm print-align-spec-of-align-spec-fix-alignspec
  (equal (print-align-spec (align-spec-fix alignspec)
                           pstate)
         (print-align-spec alignspec pstate)))

Theorem: print-align-spec-of-pristate-fix-pstate

(defthm print-align-spec-of-pristate-fix-pstate
  (equal (print-align-spec alignspec (pristate-fix pstate))
         (print-align-spec alignspec pstate)))

Theorem: print-decl-spec-of-decl-spec-fix-declspec

(defthm print-decl-spec-of-decl-spec-fix-declspec
  (equal (print-decl-spec (decl-spec-fix declspec)
                          pstate)
         (print-decl-spec declspec pstate)))

Theorem: print-decl-spec-of-pristate-fix-pstate

(defthm print-decl-spec-of-pristate-fix-pstate
  (equal (print-decl-spec declspec (pristate-fix pstate))
         (print-decl-spec declspec pstate)))

Theorem: print-decl-spec-list-of-decl-spec-list-fix-declspecs

(defthm print-decl-spec-list-of-decl-spec-list-fix-declspecs
  (equal (print-decl-spec-list (decl-spec-list-fix declspecs)
                               pstate)
         (print-decl-spec-list declspecs pstate)))

Theorem: print-decl-spec-list-of-pristate-fix-pstate

(defthm print-decl-spec-list-of-pristate-fix-pstate
  (equal (print-decl-spec-list declspecs (pristate-fix pstate))
         (print-decl-spec-list declspecs pstate)))

Theorem: print-typequal/attribspec-of-typequal/attribspec-fix-tyqualattrib

(defthm
  print-typequal/attribspec-of-typequal/attribspec-fix-tyqualattrib
 (equal
   (print-typequal/attribspec (typequal/attribspec-fix tyqualattrib)
                              pstate)
   (print-typequal/attribspec tyqualattrib pstate)))

Theorem: print-typequal/attribspec-of-pristate-fix-pstate

(defthm print-typequal/attribspec-of-pristate-fix-pstate
 (equal
      (print-typequal/attribspec tyqualattrib (pristate-fix pstate))
      (print-typequal/attribspec tyqualattrib pstate)))

Theorem: print-typequal/attribspec-list-of-typequal/attribspec-list-fix-tyqualattribs

(defthm
 print-typequal/attribspec-list-of-typequal/attribspec-list-fix-tyqualattribs
 (equal (print-typequal/attribspec-list
             (typequal/attribspec-list-fix tyqualattribs)
             pstate)
        (print-typequal/attribspec-list tyqualattribs pstate)))

Theorem: print-typequal/attribspec-list-of-pristate-fix-pstate

(defthm print-typequal/attribspec-list-of-pristate-fix-pstate
  (equal (print-typequal/attribspec-list
              tyqualattribs (pristate-fix pstate))
         (print-typequal/attribspec-list tyqualattribs pstate)))

Theorem: print-typequal/attribspec-list-list-of-typequal/attribspec-list-list-fix-tyqualattribss

(defthm
 print-typequal/attribspec-list-list-of-typequal/attribspec-list-list-fix-tyqualattribss
 (equal
      (print-typequal/attribspec-list-list
           (typequal/attribspec-list-list-fix tyqualattribss)
           pstate)
      (print-typequal/attribspec-list-list tyqualattribss pstate)))

Theorem: print-typequal/attribspec-list-list-of-pristate-fix-pstate

(defthm print-typequal/attribspec-list-list-of-pristate-fix-pstate
  (equal
       (print-typequal/attribspec-list-list
            tyqualattribss (pristate-fix pstate))
       (print-typequal/attribspec-list-list tyqualattribss pstate)))

Theorem: print-initer-of-initer-fix-initer

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

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

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

Theorem: print-desiniter-of-desiniter-fix-desiniter

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

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

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

Theorem: print-desiniter-list-of-desiniter-list-fix-desiniters

(defthm print-desiniter-list-of-desiniter-list-fix-desiniters
  (equal (print-desiniter-list (desiniter-list-fix desiniters)
                               pstate)
         (print-desiniter-list desiniters pstate)))

Theorem: print-desiniter-list-of-pristate-fix-pstate

(defthm print-desiniter-list-of-pristate-fix-pstate
  (equal (print-desiniter-list desiniters (pristate-fix pstate))
         (print-desiniter-list desiniters pstate)))

Theorem: print-designor-of-designor-fix-designor

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

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

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

Theorem: print-designor-list-of-designor-list-fix-designors

(defthm print-designor-list-of-designor-list-fix-designors
  (equal (print-designor-list (designor-list-fix designors)
                              pstate)
         (print-designor-list designors pstate)))

Theorem: print-designor-list-of-pristate-fix-pstate

(defthm print-designor-list-of-pristate-fix-pstate
  (equal (print-designor-list designors (pristate-fix pstate))
         (print-designor-list designors pstate)))

Theorem: print-declor-of-declor-fix-declor

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

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

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

Theorem: print-dirdeclor-of-dirdeclor-fix-dirdeclor

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

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

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

Theorem: print-absdeclor-of-absdeclor-fix-absdeclor

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

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

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

Theorem: print-dirabsdeclor-of-dirabsdeclor-fix-dirabsdeclor

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

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

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

Theorem: print-param-declon-of-param-declon-fix-param

(defthm print-param-declon-of-param-declon-fix-param
  (equal (print-param-declon (param-declon-fix param)
                             pstate)
         (print-param-declon param pstate)))

Theorem: print-param-declon-of-pristate-fix-pstate

(defthm print-param-declon-of-pristate-fix-pstate
  (equal (print-param-declon param (pristate-fix pstate))
         (print-param-declon param pstate)))

Theorem: print-param-declon-list-of-param-declon-list-fix-params

(defthm print-param-declon-list-of-param-declon-list-fix-params
  (equal (print-param-declon-list (param-declon-list-fix params)
                                  pstate)
         (print-param-declon-list params pstate)))

Theorem: print-param-declon-list-of-pristate-fix-pstate

(defthm print-param-declon-list-of-pristate-fix-pstate
  (equal (print-param-declon-list params (pristate-fix pstate))
         (print-param-declon-list params pstate)))

Theorem: print-param-declor-of-param-declor-fix-paramdeclor

(defthm print-param-declor-of-param-declor-fix-paramdeclor
  (equal (print-param-declor (param-declor-fix paramdeclor)
                             pstate)
         (print-param-declor paramdeclor pstate)))

Theorem: print-param-declor-of-pristate-fix-pstate

(defthm print-param-declor-of-pristate-fix-pstate
  (equal (print-param-declor paramdeclor (pristate-fix pstate))
         (print-param-declor paramdeclor pstate)))

Theorem: print-tyname-of-tyname-fix-tyname

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

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

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

Theorem: print-struni-spec-of-struni-spec-fix-struni-spec

(defthm print-struni-spec-of-struni-spec-fix-struni-spec
  (equal (print-struni-spec (struni-spec-fix struni-spec)
                            pstate)
         (print-struni-spec struni-spec pstate)))

Theorem: print-struni-spec-of-pristate-fix-pstate

(defthm print-struni-spec-of-pristate-fix-pstate
  (equal (print-struni-spec struni-spec (pristate-fix pstate))
         (print-struni-spec struni-spec pstate)))

Theorem: print-struct-declon-of-struct-declon-fix-structdeclon

(defthm print-struct-declon-of-struct-declon-fix-structdeclon
  (equal (print-struct-declon (struct-declon-fix structdeclon)
                              pstate)
         (print-struct-declon structdeclon pstate)))

Theorem: print-struct-declon-of-pristate-fix-pstate

(defthm print-struct-declon-of-pristate-fix-pstate
  (equal (print-struct-declon structdeclon (pristate-fix pstate))
         (print-struct-declon structdeclon pstate)))

Theorem: print-struct-declon-list-of-struct-declon-list-fix-structdeclons

(defthm
   print-struct-declon-list-of-struct-declon-list-fix-structdeclons
 (equal
    (print-struct-declon-list (struct-declon-list-fix structdeclons)
                              pstate)
    (print-struct-declon-list structdeclons pstate)))

Theorem: print-struct-declon-list-of-pristate-fix-pstate

(defthm print-struct-declon-list-of-pristate-fix-pstate
 (equal
      (print-struct-declon-list structdeclons (pristate-fix pstate))
      (print-struct-declon-list structdeclons pstate)))

Theorem: print-struct-declor-of-struct-declor-fix-structdeclor

(defthm print-struct-declor-of-struct-declor-fix-structdeclor
  (equal (print-struct-declor (struct-declor-fix structdeclor)
                              pstate)
         (print-struct-declor structdeclor pstate)))

Theorem: print-struct-declor-of-pristate-fix-pstate

(defthm print-struct-declor-of-pristate-fix-pstate
  (equal (print-struct-declor structdeclor (pristate-fix pstate))
         (print-struct-declor structdeclor pstate)))

Theorem: print-struct-declor-list-of-struct-declor-list-fix-structdeclors

(defthm
   print-struct-declor-list-of-struct-declor-list-fix-structdeclors
 (equal
    (print-struct-declor-list (struct-declor-list-fix structdeclors)
                              pstate)
    (print-struct-declor-list structdeclors pstate)))

Theorem: print-struct-declor-list-of-pristate-fix-pstate

(defthm print-struct-declor-list-of-pristate-fix-pstate
 (equal
      (print-struct-declor-list structdeclors (pristate-fix pstate))
      (print-struct-declor-list structdeclors pstate)))

Theorem: print-enum-spec-of-enum-spec-fix-enumspec

(defthm print-enum-spec-of-enum-spec-fix-enumspec
  (equal (print-enum-spec (enum-spec-fix enumspec)
                          pstate)
         (print-enum-spec enumspec pstate)))

Theorem: print-enum-spec-of-pristate-fix-pstate

(defthm print-enum-spec-of-pristate-fix-pstate
  (equal (print-enum-spec enumspec (pristate-fix pstate))
         (print-enum-spec enumspec pstate)))

Theorem: print-enumer-of-enumer-fix-enumer

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

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

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

Theorem: print-enumer-list-of-enumer-list-fix-enumers

(defthm print-enumer-list-of-enumer-list-fix-enumers
  (equal (print-enumer-list (enumer-list-fix enumers)
                            pstate)
         (print-enumer-list enumers pstate)))

Theorem: print-enumer-list-of-pristate-fix-pstate

(defthm print-enumer-list-of-pristate-fix-pstate
  (equal (print-enumer-list enumers (pristate-fix pstate))
         (print-enumer-list enumers pstate)))

Theorem: print-statassert-of-statassert-fix-statassert

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

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

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

Theorem: print-attrib-of-attrib-fix-attr

(defthm print-attrib-of-attrib-fix-attr
  (equal (print-attrib (attrib-fix attr) pstate)
         (print-attrib attr pstate)))

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

(defthm print-attrib-of-pristate-fix-pstate
  (equal (print-attrib attr (pristate-fix pstate))
         (print-attrib attr pstate)))

Theorem: print-attrib-list-of-attrib-list-fix-attrs

(defthm print-attrib-list-of-attrib-list-fix-attrs
  (equal (print-attrib-list (attrib-list-fix attrs)
                            pstate)
         (print-attrib-list attrs pstate)))

Theorem: print-attrib-list-of-pristate-fix-pstate

(defthm print-attrib-list-of-pristate-fix-pstate
  (equal (print-attrib-list attrs (pristate-fix pstate))
         (print-attrib-list attrs pstate)))

Theorem: print-attrib-spec-of-attrib-spec-fix-attrspec

(defthm print-attrib-spec-of-attrib-spec-fix-attrspec
  (equal (print-attrib-spec (attrib-spec-fix attrspec)
                            pstate)
         (print-attrib-spec attrspec pstate)))

Theorem: print-attrib-spec-of-pristate-fix-pstate

(defthm print-attrib-spec-of-pristate-fix-pstate
  (equal (print-attrib-spec attrspec (pristate-fix pstate))
         (print-attrib-spec attrspec pstate)))

Theorem: print-attrib-spec-list-of-attrib-spec-list-fix-attrspecs

(defthm print-attrib-spec-list-of-attrib-spec-list-fix-attrspecs
  (equal (print-attrib-spec-list (attrib-spec-list-fix attrspecs)
                                 pstate)
         (print-attrib-spec-list attrspecs pstate)))

Theorem: print-attrib-spec-list-of-pristate-fix-pstate

(defthm print-attrib-spec-list-of-pristate-fix-pstate
  (equal (print-attrib-spec-list attrspecs (pristate-fix pstate))
         (print-attrib-spec-list attrspecs pstate)))

Theorem: print-initdeclor-of-initdeclor-fix-initdeclor

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

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

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

Theorem: print-initdeclor-list-of-initdeclor-list-fix-initdeclors

(defthm print-initdeclor-list-of-initdeclor-list-fix-initdeclors
  (equal (print-initdeclor-list (initdeclor-list-fix initdeclors)
                                pstate)
         (print-initdeclor-list initdeclors pstate)))

Theorem: print-initdeclor-list-of-pristate-fix-pstate

(defthm print-initdeclor-list-of-pristate-fix-pstate
  (equal (print-initdeclor-list initdeclors (pristate-fix pstate))
         (print-initdeclor-list initdeclors pstate)))

Theorem: print-decl-inline-of-decl-fix-decl

(defthm print-decl-inline-of-decl-fix-decl
  (equal (print-decl-inline (decl-fix decl)
                            pstate)
         (print-decl-inline decl pstate)))

Theorem: print-decl-inline-of-pristate-fix-pstate

(defthm print-decl-inline-of-pristate-fix-pstate
  (equal (print-decl-inline decl (pristate-fix pstate))
         (print-decl-inline decl pstate)))

Theorem: print-decl-of-decl-fix-decl

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

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

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

Theorem: print-decl-list-of-decl-list-fix-decls

(defthm print-decl-list-of-decl-list-fix-decls
  (equal (print-decl-list (decl-list-fix decls)
                          pstate)
         (print-decl-list decls pstate)))

Theorem: print-decl-list-of-pristate-fix-pstate

(defthm print-decl-list-of-pristate-fix-pstate
  (equal (print-decl-list decls (pristate-fix pstate))
         (print-decl-list decls pstate)))

Theorem: print-label-of-label-fix-label

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

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

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

Theorem: print-asm-output-of-asm-output-fix-output

(defthm print-asm-output-of-asm-output-fix-output
  (equal (print-asm-output (asm-output-fix output)
                           pstate)
         (print-asm-output output pstate)))

Theorem: print-asm-output-of-pristate-fix-pstate

(defthm print-asm-output-of-pristate-fix-pstate
  (equal (print-asm-output output (pristate-fix pstate))
         (print-asm-output output pstate)))

Theorem: print-asm-output-list-of-asm-output-list-fix-outputs

(defthm print-asm-output-list-of-asm-output-list-fix-outputs
  (equal (print-asm-output-list (asm-output-list-fix outputs)
                                pstate)
         (print-asm-output-list outputs pstate)))

Theorem: print-asm-output-list-of-pristate-fix-pstate

(defthm print-asm-output-list-of-pristate-fix-pstate
  (equal (print-asm-output-list outputs (pristate-fix pstate))
         (print-asm-output-list outputs pstate)))

Theorem: print-asm-input-of-asm-input-fix-input

(defthm print-asm-input-of-asm-input-fix-input
  (equal (print-asm-input (asm-input-fix input)
                          pstate)
         (print-asm-input input pstate)))

Theorem: print-asm-input-of-pristate-fix-pstate

(defthm print-asm-input-of-pristate-fix-pstate
  (equal (print-asm-input input (pristate-fix pstate))
         (print-asm-input input pstate)))

Theorem: print-asm-input-list-of-asm-input-list-fix-inputs

(defthm print-asm-input-list-of-asm-input-list-fix-inputs
  (equal (print-asm-input-list (asm-input-list-fix inputs)
                               pstate)
         (print-asm-input-list inputs pstate)))

Theorem: print-asm-input-list-of-pristate-fix-pstate

(defthm print-asm-input-list-of-pristate-fix-pstate
  (equal (print-asm-input-list inputs (pristate-fix pstate))
         (print-asm-input-list inputs pstate)))

Theorem: print-asm-stmt-of-asm-stmt-fix-asm

(defthm print-asm-stmt-of-asm-stmt-fix-asm
  (equal (print-asm-stmt (asm-stmt-fix asm)
                         pstate)
         (print-asm-stmt asm pstate)))

Theorem: print-asm-stmt-of-pristate-fix-pstate

(defthm print-asm-stmt-of-pristate-fix-pstate
  (equal (print-asm-stmt asm (pristate-fix pstate))
         (print-asm-stmt asm pstate)))

Theorem: print-stmt-of-stmt-fix-stmt

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

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

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

Theorem: print-comp-stmt-of-comp-stmt-fix-cstmt

(defthm print-comp-stmt-of-comp-stmt-fix-cstmt
  (equal (print-comp-stmt (comp-stmt-fix cstmt)
                          pstate)
         (print-comp-stmt cstmt pstate)))

Theorem: print-comp-stmt-of-pristate-fix-pstate

(defthm print-comp-stmt-of-pristate-fix-pstate
  (equal (print-comp-stmt cstmt (pristate-fix pstate))
         (print-comp-stmt cstmt pstate)))

Theorem: print-block-item-of-block-item-fix-item

(defthm print-block-item-of-block-item-fix-item
  (equal (print-block-item (block-item-fix item)
                           pstate)
         (print-block-item item pstate)))

Theorem: print-block-item-of-pristate-fix-pstate

(defthm print-block-item-of-pristate-fix-pstate
  (equal (print-block-item item (pristate-fix pstate))
         (print-block-item item pstate)))

Theorem: print-block-item-list-of-block-item-list-fix-items

(defthm print-block-item-list-of-block-item-list-fix-items
  (equal (print-block-item-list (block-item-list-fix items)
                                pstate)
         (print-block-item-list items pstate)))

Theorem: print-block-item-list-of-pristate-fix-pstate

(defthm print-block-item-list-of-pristate-fix-pstate
  (equal (print-block-item-list items (pristate-fix pstate))
         (print-block-item-list items pstate)))

Theorem: print-expr-expr-equiv-congruence-on-expr

(defthm print-expr-expr-equiv-congruence-on-expr
  (implies (expr-equiv expr expr-equiv)
           (equal (print-expr expr expected-prio pstate)
                  (print-expr expr-equiv expected-prio pstate)))
  :rule-classes :congruence)

Theorem: print-expr-expr-priority-equiv-congruence-on-expected-prio

(defthm print-expr-expr-priority-equiv-congruence-on-expected-prio
  (implies (expr-priority-equiv expected-prio expected-prio-equiv)
           (equal (print-expr expr expected-prio pstate)
                  (print-expr expr expected-prio-equiv pstate)))
  :rule-classes :congruence)

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

(defthm print-expr-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-expr expr expected-prio pstate)
                  (print-expr expr expected-prio pstate-equiv)))
  :rule-classes :congruence)

Theorem: print-expr-list-expr-list-equiv-congruence-on-exprs

(defthm print-expr-list-expr-list-equiv-congruence-on-exprs
  (implies (expr-list-equiv exprs exprs-equiv)
           (equal (print-expr-list exprs pstate)
                  (print-expr-list exprs-equiv pstate)))
  :rule-classes :congruence)

Theorem: print-expr-list-pristate-equiv-congruence-on-pstate

(defthm print-expr-list-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-expr-list exprs pstate)
                  (print-expr-list exprs pstate-equiv)))
  :rule-classes :congruence)

Theorem: print-const-expr-const-expr-equiv-congruence-on-cexpr

(defthm print-const-expr-const-expr-equiv-congruence-on-cexpr
  (implies (const-expr-equiv cexpr cexpr-equiv)
           (equal (print-const-expr cexpr pstate)
                  (print-const-expr cexpr-equiv pstate)))
  :rule-classes :congruence)

Theorem: print-const-expr-pristate-equiv-congruence-on-pstate

(defthm print-const-expr-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-const-expr cexpr pstate)
                  (print-const-expr cexpr pstate-equiv)))
  :rule-classes :congruence)

Theorem: print-genassoc-genassoc-equiv-congruence-on-genassoc

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

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

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

Theorem: print-genassoc-list-genassoc-list-equiv-congruence-on-genassocs

(defthm
    print-genassoc-list-genassoc-list-equiv-congruence-on-genassocs
  (implies (genassoc-list-equiv genassocs genassocs-equiv)
           (equal (print-genassoc-list genassocs pstate)
                  (print-genassoc-list genassocs-equiv pstate)))
  :rule-classes :congruence)

Theorem: print-genassoc-list-pristate-equiv-congruence-on-pstate

(defthm print-genassoc-list-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-genassoc-list genassocs pstate)
                  (print-genassoc-list genassocs pstate-equiv)))
  :rule-classes :congruence)

Theorem: print-member-designor-member-designor-equiv-congruence-on-memdes

(defthm
   print-member-designor-member-designor-equiv-congruence-on-memdes
  (implies (member-designor-equiv memdes memdes-equiv)
           (equal (print-member-designor memdes pstate)
                  (print-member-designor memdes-equiv pstate)))
  :rule-classes :congruence)

Theorem: print-member-designor-pristate-equiv-congruence-on-pstate

(defthm print-member-designor-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-member-designor memdes pstate)
                  (print-member-designor memdes pstate-equiv)))
  :rule-classes :congruence)

Theorem: print-type-spec-type-spec-equiv-congruence-on-tyspec

(defthm print-type-spec-type-spec-equiv-congruence-on-tyspec
  (implies (type-spec-equiv tyspec tyspec-equiv)
           (equal (print-type-spec tyspec pstate)
                  (print-type-spec tyspec-equiv pstate)))
  :rule-classes :congruence)

Theorem: print-type-spec-pristate-equiv-congruence-on-pstate

(defthm print-type-spec-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-type-spec tyspec pstate)
                  (print-type-spec tyspec pstate-equiv)))
  :rule-classes :congruence)

Theorem: print-spec/qual-spec/qual-equiv-congruence-on-specqual

(defthm print-spec/qual-spec/qual-equiv-congruence-on-specqual
  (implies (spec/qual-equiv specqual specqual-equiv)
           (equal (print-spec/qual specqual pstate)
                  (print-spec/qual specqual-equiv pstate)))
  :rule-classes :congruence)

Theorem: print-spec/qual-pristate-equiv-congruence-on-pstate

(defthm print-spec/qual-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-spec/qual specqual pstate)
                  (print-spec/qual specqual pstate-equiv)))
  :rule-classes :congruence)

Theorem: print-spec/qual-list-spec/qual-list-equiv-congruence-on-specquals

(defthm
  print-spec/qual-list-spec/qual-list-equiv-congruence-on-specquals
  (implies (spec/qual-list-equiv specquals specquals-equiv)
           (equal (print-spec/qual-list specquals pstate)
                  (print-spec/qual-list specquals-equiv pstate)))
  :rule-classes :congruence)

Theorem: print-spec/qual-list-pristate-equiv-congruence-on-pstate

(defthm print-spec/qual-list-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-spec/qual-list specquals pstate)
                  (print-spec/qual-list specquals pstate-equiv)))
  :rule-classes :congruence)

Theorem: print-align-spec-align-spec-equiv-congruence-on-alignspec

(defthm print-align-spec-align-spec-equiv-congruence-on-alignspec
  (implies (align-spec-equiv alignspec alignspec-equiv)
           (equal (print-align-spec alignspec pstate)
                  (print-align-spec alignspec-equiv pstate)))
  :rule-classes :congruence)

Theorem: print-align-spec-pristate-equiv-congruence-on-pstate

(defthm print-align-spec-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-align-spec alignspec pstate)
                  (print-align-spec alignspec pstate-equiv)))
  :rule-classes :congruence)

Theorem: print-decl-spec-decl-spec-equiv-congruence-on-declspec

(defthm print-decl-spec-decl-spec-equiv-congruence-on-declspec
  (implies (decl-spec-equiv declspec declspec-equiv)
           (equal (print-decl-spec declspec pstate)
                  (print-decl-spec declspec-equiv pstate)))
  :rule-classes :congruence)

Theorem: print-decl-spec-pristate-equiv-congruence-on-pstate

(defthm print-decl-spec-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-decl-spec declspec pstate)
                  (print-decl-spec declspec pstate-equiv)))
  :rule-classes :congruence)

Theorem: print-decl-spec-list-decl-spec-list-equiv-congruence-on-declspecs

(defthm
  print-decl-spec-list-decl-spec-list-equiv-congruence-on-declspecs
  (implies (decl-spec-list-equiv declspecs declspecs-equiv)
           (equal (print-decl-spec-list declspecs pstate)
                  (print-decl-spec-list declspecs-equiv pstate)))
  :rule-classes :congruence)

Theorem: print-decl-spec-list-pristate-equiv-congruence-on-pstate

(defthm print-decl-spec-list-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-decl-spec-list declspecs pstate)
                  (print-decl-spec-list declspecs pstate-equiv)))
  :rule-classes :congruence)

Theorem: print-typequal/attribspec-typequal/attribspec-equiv-congruence-on-tyqualattrib

(defthm
 print-typequal/attribspec-typequal/attribspec-equiv-congruence-on-tyqualattrib
 (implies
      (typequal/attribspec-equiv tyqualattrib tyqualattrib-equiv)
      (equal (print-typequal/attribspec tyqualattrib pstate)
             (print-typequal/attribspec tyqualattrib-equiv pstate)))
 :rule-classes :congruence)

Theorem: print-typequal/attribspec-pristate-equiv-congruence-on-pstate

(defthm
      print-typequal/attribspec-pristate-equiv-congruence-on-pstate
 (implies
      (pristate-equiv pstate pstate-equiv)
      (equal (print-typequal/attribspec tyqualattrib pstate)
             (print-typequal/attribspec tyqualattrib pstate-equiv)))
 :rule-classes :congruence)

Theorem: print-typequal/attribspec-list-typequal/attribspec-list-equiv-congruence-on-tyqualattribs

(defthm
 print-typequal/attribspec-list-typequal/attribspec-list-equiv-congruence-on-tyqualattribs
 (implies
  (typequal/attribspec-list-equiv tyqualattribs tyqualattribs-equiv)
  (equal
       (print-typequal/attribspec-list tyqualattribs pstate)
       (print-typequal/attribspec-list tyqualattribs-equiv pstate)))
 :rule-classes :congruence)

Theorem: print-typequal/attribspec-list-pristate-equiv-congruence-on-pstate

(defthm
 print-typequal/attribspec-list-pristate-equiv-congruence-on-pstate
 (implies
  (pristate-equiv pstate pstate-equiv)
  (equal
       (print-typequal/attribspec-list tyqualattribs pstate)
       (print-typequal/attribspec-list tyqualattribs pstate-equiv)))
 :rule-classes :congruence)

Theorem: print-typequal/attribspec-list-list-typequal/attribspec-list-list-equiv-congruence-on-tyqualattribss

(defthm
 print-typequal/attribspec-list-list-typequal/attribspec-list-list-equiv-congruence-on-tyqualattribss
 (implies
  (typequal/attribspec-list-list-equiv
       tyqualattribss tyqualattribss-equiv)
  (equal (print-typequal/attribspec-list-list tyqualattribss pstate)
         (print-typequal/attribspec-list-list
              tyqualattribss-equiv pstate)))
 :rule-classes :congruence)

Theorem: print-typequal/attribspec-list-list-pristate-equiv-congruence-on-pstate

(defthm
 print-typequal/attribspec-list-list-pristate-equiv-congruence-on-pstate
 (implies
  (pristate-equiv pstate pstate-equiv)
  (equal (print-typequal/attribspec-list-list tyqualattribss pstate)
         (print-typequal/attribspec-list-list
              tyqualattribss pstate-equiv)))
 :rule-classes :congruence)

Theorem: print-initer-initer-equiv-congruence-on-initer

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

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

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

Theorem: print-desiniter-desiniter-equiv-congruence-on-desiniter

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

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

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

Theorem: print-desiniter-list-desiniter-list-equiv-congruence-on-desiniters

(defthm
 print-desiniter-list-desiniter-list-equiv-congruence-on-desiniters
 (implies (desiniter-list-equiv desiniters desiniters-equiv)
          (equal (print-desiniter-list desiniters pstate)
                 (print-desiniter-list desiniters-equiv pstate)))
 :rule-classes :congruence)

Theorem: print-desiniter-list-pristate-equiv-congruence-on-pstate

(defthm print-desiniter-list-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-desiniter-list desiniters pstate)
                  (print-desiniter-list desiniters pstate-equiv)))
  :rule-classes :congruence)

Theorem: print-designor-designor-equiv-congruence-on-designor

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

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

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

Theorem: print-designor-list-designor-list-equiv-congruence-on-designors

(defthm
    print-designor-list-designor-list-equiv-congruence-on-designors
  (implies (designor-list-equiv designors designors-equiv)
           (equal (print-designor-list designors pstate)
                  (print-designor-list designors-equiv pstate)))
  :rule-classes :congruence)

Theorem: print-designor-list-pristate-equiv-congruence-on-pstate

(defthm print-designor-list-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-designor-list designors pstate)
                  (print-designor-list designors pstate-equiv)))
  :rule-classes :congruence)

Theorem: print-declor-declor-equiv-congruence-on-declor

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

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

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

Theorem: print-dirdeclor-dirdeclor-equiv-congruence-on-dirdeclor

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

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

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

Theorem: print-absdeclor-absdeclor-equiv-congruence-on-absdeclor

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

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

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

Theorem: print-dirabsdeclor-dirabsdeclor-equiv-congruence-on-dirabsdeclor

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

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

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

Theorem: print-param-declon-param-declon-equiv-congruence-on-param

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

Theorem: print-param-declon-pristate-equiv-congruence-on-pstate

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

Theorem: print-param-declon-list-param-declon-list-equiv-congruence-on-params

(defthm
 print-param-declon-list-param-declon-list-equiv-congruence-on-params
 (implies (param-declon-list-equiv params params-equiv)
          (equal (print-param-declon-list params pstate)
                 (print-param-declon-list params-equiv pstate)))
 :rule-classes :congruence)

Theorem: print-param-declon-list-pristate-equiv-congruence-on-pstate

(defthm print-param-declon-list-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-param-declon-list params pstate)
                  (print-param-declon-list params pstate-equiv)))
  :rule-classes :congruence)

Theorem: print-param-declor-param-declor-equiv-congruence-on-paramdeclor

(defthm
    print-param-declor-param-declor-equiv-congruence-on-paramdeclor
  (implies (param-declor-equiv paramdeclor paramdeclor-equiv)
           (equal (print-param-declor paramdeclor pstate)
                  (print-param-declor paramdeclor-equiv pstate)))
  :rule-classes :congruence)

Theorem: print-param-declor-pristate-equiv-congruence-on-pstate

(defthm print-param-declor-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-param-declor paramdeclor pstate)
                  (print-param-declor paramdeclor pstate-equiv)))
  :rule-classes :congruence)

Theorem: print-tyname-tyname-equiv-congruence-on-tyname

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

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

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

Theorem: print-struni-spec-struni-spec-equiv-congruence-on-struni-spec

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

Theorem: print-struni-spec-pristate-equiv-congruence-on-pstate

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

Theorem: print-struct-declon-struct-declon-equiv-congruence-on-structdeclon

(defthm
 print-struct-declon-struct-declon-equiv-congruence-on-structdeclon
 (implies (struct-declon-equiv structdeclon structdeclon-equiv)
          (equal (print-struct-declon structdeclon pstate)
                 (print-struct-declon structdeclon-equiv pstate)))
 :rule-classes :congruence)

Theorem: print-struct-declon-pristate-equiv-congruence-on-pstate

(defthm print-struct-declon-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-struct-declon structdeclon pstate)
                  (print-struct-declon structdeclon pstate-equiv)))
  :rule-classes :congruence)

Theorem: print-struct-declon-list-struct-declon-list-equiv-congruence-on-structdeclons

(defthm
 print-struct-declon-list-struct-declon-list-equiv-congruence-on-structdeclons
 (implies
      (struct-declon-list-equiv structdeclons structdeclons-equiv)
      (equal (print-struct-declon-list structdeclons pstate)
             (print-struct-declon-list structdeclons-equiv pstate)))
 :rule-classes :congruence)

Theorem: print-struct-declon-list-pristate-equiv-congruence-on-pstate

(defthm print-struct-declon-list-pristate-equiv-congruence-on-pstate
 (implies
      (pristate-equiv pstate pstate-equiv)
      (equal (print-struct-declon-list structdeclons pstate)
             (print-struct-declon-list structdeclons pstate-equiv)))
 :rule-classes :congruence)

Theorem: print-struct-declor-struct-declor-equiv-congruence-on-structdeclor

(defthm
 print-struct-declor-struct-declor-equiv-congruence-on-structdeclor
 (implies (struct-declor-equiv structdeclor structdeclor-equiv)
          (equal (print-struct-declor structdeclor pstate)
                 (print-struct-declor structdeclor-equiv pstate)))
 :rule-classes :congruence)

Theorem: print-struct-declor-pristate-equiv-congruence-on-pstate

(defthm print-struct-declor-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-struct-declor structdeclor pstate)
                  (print-struct-declor structdeclor pstate-equiv)))
  :rule-classes :congruence)

Theorem: print-struct-declor-list-struct-declor-list-equiv-congruence-on-structdeclors

(defthm
 print-struct-declor-list-struct-declor-list-equiv-congruence-on-structdeclors
 (implies
      (struct-declor-list-equiv structdeclors structdeclors-equiv)
      (equal (print-struct-declor-list structdeclors pstate)
             (print-struct-declor-list structdeclors-equiv pstate)))
 :rule-classes :congruence)

Theorem: print-struct-declor-list-pristate-equiv-congruence-on-pstate

(defthm print-struct-declor-list-pristate-equiv-congruence-on-pstate
 (implies
      (pristate-equiv pstate pstate-equiv)
      (equal (print-struct-declor-list structdeclors pstate)
             (print-struct-declor-list structdeclors pstate-equiv)))
 :rule-classes :congruence)

Theorem: print-enum-spec-enum-spec-equiv-congruence-on-enumspec

(defthm print-enum-spec-enum-spec-equiv-congruence-on-enumspec
  (implies (enum-spec-equiv enumspec enumspec-equiv)
           (equal (print-enum-spec enumspec pstate)
                  (print-enum-spec enumspec-equiv pstate)))
  :rule-classes :congruence)

Theorem: print-enum-spec-pristate-equiv-congruence-on-pstate

(defthm print-enum-spec-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-enum-spec enumspec pstate)
                  (print-enum-spec enumspec pstate-equiv)))
  :rule-classes :congruence)

Theorem: print-enumer-enumer-equiv-congruence-on-enumer

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

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

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

Theorem: print-enumer-list-enumer-list-equiv-congruence-on-enumers

(defthm print-enumer-list-enumer-list-equiv-congruence-on-enumers
  (implies (enumer-list-equiv enumers enumers-equiv)
           (equal (print-enumer-list enumers pstate)
                  (print-enumer-list enumers-equiv pstate)))
  :rule-classes :congruence)

Theorem: print-enumer-list-pristate-equiv-congruence-on-pstate

(defthm print-enumer-list-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-enumer-list enumers pstate)
                  (print-enumer-list enumers pstate-equiv)))
  :rule-classes :congruence)

Theorem: print-statassert-statassert-equiv-congruence-on-statassert

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

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

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

Theorem: print-attrib-attrib-equiv-congruence-on-attr

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

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

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

Theorem: print-attrib-list-attrib-list-equiv-congruence-on-attrs

(defthm print-attrib-list-attrib-list-equiv-congruence-on-attrs
  (implies (attrib-list-equiv attrs attrs-equiv)
           (equal (print-attrib-list attrs pstate)
                  (print-attrib-list attrs-equiv pstate)))
  :rule-classes :congruence)

Theorem: print-attrib-list-pristate-equiv-congruence-on-pstate

(defthm print-attrib-list-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-attrib-list attrs pstate)
                  (print-attrib-list attrs pstate-equiv)))
  :rule-classes :congruence)

Theorem: print-attrib-spec-attrib-spec-equiv-congruence-on-attrspec

(defthm print-attrib-spec-attrib-spec-equiv-congruence-on-attrspec
  (implies (attrib-spec-equiv attrspec attrspec-equiv)
           (equal (print-attrib-spec attrspec pstate)
                  (print-attrib-spec attrspec-equiv pstate)))
  :rule-classes :congruence)

Theorem: print-attrib-spec-pristate-equiv-congruence-on-pstate

(defthm print-attrib-spec-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-attrib-spec attrspec pstate)
                  (print-attrib-spec attrspec pstate-equiv)))
  :rule-classes :congruence)

Theorem: print-attrib-spec-list-attrib-spec-list-equiv-congruence-on-attrspecs

(defthm
 print-attrib-spec-list-attrib-spec-list-equiv-congruence-on-attrspecs
 (implies (attrib-spec-list-equiv attrspecs attrspecs-equiv)
          (equal (print-attrib-spec-list attrspecs pstate)
                 (print-attrib-spec-list attrspecs-equiv pstate)))
 :rule-classes :congruence)

Theorem: print-attrib-spec-list-pristate-equiv-congruence-on-pstate

(defthm print-attrib-spec-list-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-attrib-spec-list attrspecs pstate)
                  (print-attrib-spec-list attrspecs pstate-equiv)))
  :rule-classes :congruence)

Theorem: print-initdeclor-initdeclor-equiv-congruence-on-initdeclor

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

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

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

Theorem: print-initdeclor-list-initdeclor-list-equiv-congruence-on-initdeclors

(defthm
 print-initdeclor-list-initdeclor-list-equiv-congruence-on-initdeclors
 (implies (initdeclor-list-equiv initdeclors initdeclors-equiv)
          (equal (print-initdeclor-list initdeclors pstate)
                 (print-initdeclor-list initdeclors-equiv pstate)))
 :rule-classes :congruence)

Theorem: print-initdeclor-list-pristate-equiv-congruence-on-pstate

(defthm print-initdeclor-list-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-initdeclor-list initdeclors pstate)
                  (print-initdeclor-list initdeclors pstate-equiv)))
  :rule-classes :congruence)

Theorem: print-decl-inline-decl-equiv-congruence-on-decl

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

Theorem: print-decl-inline-pristate-equiv-congruence-on-pstate

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

Theorem: print-decl-decl-equiv-congruence-on-decl

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

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

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

Theorem: print-decl-list-decl-list-equiv-congruence-on-decls

(defthm print-decl-list-decl-list-equiv-congruence-on-decls
  (implies (decl-list-equiv decls decls-equiv)
           (equal (print-decl-list decls pstate)
                  (print-decl-list decls-equiv pstate)))
  :rule-classes :congruence)

Theorem: print-decl-list-pristate-equiv-congruence-on-pstate

(defthm print-decl-list-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-decl-list decls pstate)
                  (print-decl-list decls pstate-equiv)))
  :rule-classes :congruence)

Theorem: print-label-label-equiv-congruence-on-label

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

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

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

Theorem: print-asm-output-asm-output-equiv-congruence-on-output

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

Theorem: print-asm-output-pristate-equiv-congruence-on-pstate

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

Theorem: print-asm-output-list-asm-output-list-equiv-congruence-on-outputs

(defthm
  print-asm-output-list-asm-output-list-equiv-congruence-on-outputs
  (implies (asm-output-list-equiv outputs outputs-equiv)
           (equal (print-asm-output-list outputs pstate)
                  (print-asm-output-list outputs-equiv pstate)))
  :rule-classes :congruence)

Theorem: print-asm-output-list-pristate-equiv-congruence-on-pstate

(defthm print-asm-output-list-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-asm-output-list outputs pstate)
                  (print-asm-output-list outputs pstate-equiv)))
  :rule-classes :congruence)

Theorem: print-asm-input-asm-input-equiv-congruence-on-input

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

Theorem: print-asm-input-pristate-equiv-congruence-on-pstate

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

Theorem: print-asm-input-list-asm-input-list-equiv-congruence-on-inputs

(defthm
     print-asm-input-list-asm-input-list-equiv-congruence-on-inputs
  (implies (asm-input-list-equiv inputs inputs-equiv)
           (equal (print-asm-input-list inputs pstate)
                  (print-asm-input-list inputs-equiv pstate)))
  :rule-classes :congruence)

Theorem: print-asm-input-list-pristate-equiv-congruence-on-pstate

(defthm print-asm-input-list-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-asm-input-list inputs pstate)
                  (print-asm-input-list inputs pstate-equiv)))
  :rule-classes :congruence)

Theorem: print-asm-stmt-asm-stmt-equiv-congruence-on-asm

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

Theorem: print-asm-stmt-pristate-equiv-congruence-on-pstate

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

Theorem: print-stmt-stmt-equiv-congruence-on-stmt

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

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

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

Theorem: print-comp-stmt-comp-stmt-equiv-congruence-on-cstmt

(defthm print-comp-stmt-comp-stmt-equiv-congruence-on-cstmt
  (implies (comp-stmt-equiv cstmt cstmt-equiv)
           (equal (print-comp-stmt cstmt pstate)
                  (print-comp-stmt cstmt-equiv pstate)))
  :rule-classes :congruence)

Theorem: print-comp-stmt-pristate-equiv-congruence-on-pstate

(defthm print-comp-stmt-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-comp-stmt cstmt pstate)
                  (print-comp-stmt cstmt pstate-equiv)))
  :rule-classes :congruence)

Theorem: print-block-item-block-item-equiv-congruence-on-item

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

Theorem: print-block-item-pristate-equiv-congruence-on-pstate

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

Theorem: print-block-item-list-block-item-list-equiv-congruence-on-items

(defthm
    print-block-item-list-block-item-list-equiv-congruence-on-items
  (implies (block-item-list-equiv items items-equiv)
           (equal (print-block-item-list items pstate)
                  (print-block-item-list items-equiv pstate)))
  :rule-classes :congruence)

Theorem: print-block-item-list-pristate-equiv-congruence-on-pstate

(defthm print-block-item-list-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-block-item-list items pstate)
                  (print-block-item-list items pstate-equiv)))
  :rule-classes :congruence)

Theorem: pristate->gcc-of-print-expr

(defthm pristate->gcc-of-print-expr
  (b* ((?new-pstate (print-expr expr expected-prio pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-expr-list

(defthm pristate->gcc-of-print-expr-list
  (b* ((?new-pstate (print-expr-list exprs pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-const-expr

(defthm pristate->gcc-of-print-const-expr
  (b* ((?new-pstate (print-const-expr cexpr pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-genassoc

(defthm pristate->gcc-of-print-genassoc
  (b* ((?new-pstate (print-genassoc genassoc pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-genassoc-list

(defthm pristate->gcc-of-print-genassoc-list
  (b* ((?new-pstate (print-genassoc-list genassocs pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-member-designor

(defthm pristate->gcc-of-print-member-designor
  (b* ((?new-pstate (print-member-designor memdes pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-type-spec

(defthm pristate->gcc-of-print-type-spec
  (b* ((?new-pstate (print-type-spec tyspec pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-spec/qual

(defthm pristate->gcc-of-print-spec/qual
  (b* ((?new-pstate (print-spec/qual specqual pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-spec/qual-list

(defthm pristate->gcc-of-print-spec/qual-list
  (b* ((?new-pstate (print-spec/qual-list specquals pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-align-spec

(defthm pristate->gcc-of-print-align-spec
  (b* ((?new-pstate (print-align-spec alignspec pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-decl-spec

(defthm pristate->gcc-of-print-decl-spec
  (b* ((?new-pstate (print-decl-spec declspec pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-decl-spec-list

(defthm pristate->gcc-of-print-decl-spec-list
  (b* ((?new-pstate (print-decl-spec-list declspecs pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-typequal/attribspec

(defthm pristate->gcc-of-print-typequal/attribspec
 (b* ((?new-pstate (print-typequal/attribspec tyqualattrib pstate)))
   (equal (pristate->gcc new-pstate)
          (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-typequal/attribspec-list

(defthm pristate->gcc-of-print-typequal/attribspec-list
  (b* ((?new-pstate
            (print-typequal/attribspec-list tyqualattribs pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-typequal/attribspec-list-list

(defthm pristate->gcc-of-print-typequal/attribspec-list-list
 (b*
  ((?new-pstate
       (print-typequal/attribspec-list-list tyqualattribss pstate)))
  (equal (pristate->gcc new-pstate)
         (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-initer

(defthm pristate->gcc-of-print-initer
  (b* ((?new-pstate (print-initer initer pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-desiniter

(defthm pristate->gcc-of-print-desiniter
  (b* ((?new-pstate (print-desiniter desiniter pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-desiniter-list

(defthm pristate->gcc-of-print-desiniter-list
  (b* ((?new-pstate (print-desiniter-list desiniters pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-designor

(defthm pristate->gcc-of-print-designor
  (b* ((?new-pstate (print-designor designor pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-designor-list

(defthm pristate->gcc-of-print-designor-list
  (b* ((?new-pstate (print-designor-list designors pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-declor

(defthm pristate->gcc-of-print-declor
  (b* ((?new-pstate (print-declor declor pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-dirdeclor

(defthm pristate->gcc-of-print-dirdeclor
  (b* ((?new-pstate (print-dirdeclor dirdeclor pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-absdeclor

(defthm pristate->gcc-of-print-absdeclor
  (b* ((?new-pstate (print-absdeclor absdeclor pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-dirabsdeclor

(defthm pristate->gcc-of-print-dirabsdeclor
  (b* ((?new-pstate (print-dirabsdeclor dirabsdeclor pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-param-declon

(defthm pristate->gcc-of-print-param-declon
  (b* ((?new-pstate (print-param-declon param pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-param-declon-list

(defthm pristate->gcc-of-print-param-declon-list
  (b* ((?new-pstate (print-param-declon-list params pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-param-declor

(defthm pristate->gcc-of-print-param-declor
  (b* ((?new-pstate (print-param-declor paramdeclor pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-tyname

(defthm pristate->gcc-of-print-tyname
  (b* ((?new-pstate (print-tyname tyname pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-struni-spec

(defthm pristate->gcc-of-print-struni-spec
  (b* ((?new-pstate (print-struni-spec struni-spec pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-struct-declon

(defthm pristate->gcc-of-print-struct-declon
  (b* ((?new-pstate (print-struct-declon structdeclon pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-struct-declon-list

(defthm pristate->gcc-of-print-struct-declon-list
 (b* ((?new-pstate (print-struct-declon-list structdeclons pstate)))
   (equal (pristate->gcc new-pstate)
          (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-struct-declor

(defthm pristate->gcc-of-print-struct-declor
  (b* ((?new-pstate (print-struct-declor structdeclor pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-struct-declor-list

(defthm pristate->gcc-of-print-struct-declor-list
 (b* ((?new-pstate (print-struct-declor-list structdeclors pstate)))
   (equal (pristate->gcc new-pstate)
          (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-enum-spec

(defthm pristate->gcc-of-print-enum-spec
  (b* ((?new-pstate (print-enum-spec enumspec pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-enumer

(defthm pristate->gcc-of-print-enumer
  (b* ((?new-pstate (print-enumer enumer pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-enumer-list

(defthm pristate->gcc-of-print-enumer-list
  (b* ((?new-pstate (print-enumer-list enumers pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-statassert

(defthm pristate->gcc-of-print-statassert
  (b* ((?new-pstate (print-statassert statassert pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-attrib

(defthm pristate->gcc-of-print-attrib
  (b* ((?new-pstate (print-attrib attr pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-attrib-list

(defthm pristate->gcc-of-print-attrib-list
  (b* ((?new-pstate (print-attrib-list attrs pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-attrib-spec

(defthm pristate->gcc-of-print-attrib-spec
  (b* ((?new-pstate (print-attrib-spec attrspec pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-attrib-spec-list

(defthm pristate->gcc-of-print-attrib-spec-list
  (b* ((?new-pstate (print-attrib-spec-list attrspecs pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-initdeclor

(defthm pristate->gcc-of-print-initdeclor
  (b* ((?new-pstate (print-initdeclor initdeclor pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-initdeclor-list

(defthm pristate->gcc-of-print-initdeclor-list
  (b* ((?new-pstate (print-initdeclor-list initdeclors pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-decl-inline

(defthm pristate->gcc-of-print-decl-inline
  (b* ((?new-pstate (print-decl-inline decl pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-decl

(defthm pristate->gcc-of-print-decl
  (b* ((?new-pstate (print-decl decl pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-decl-list

(defthm pristate->gcc-of-print-decl-list
  (b* ((?new-pstate (print-decl-list decls pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-label

(defthm pristate->gcc-of-print-label
  (b* ((?new-pstate (print-label label pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-asm-output

(defthm pristate->gcc-of-print-asm-output
  (b* ((?new-pstate (print-asm-output output pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-asm-output-list

(defthm pristate->gcc-of-print-asm-output-list
  (b* ((?new-pstate (print-asm-output-list outputs pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-asm-input

(defthm pristate->gcc-of-print-asm-input
  (b* ((?new-pstate (print-asm-input input pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-asm-input-list

(defthm pristate->gcc-of-print-asm-input-list
  (b* ((?new-pstate (print-asm-input-list inputs pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-asm-stmt

(defthm pristate->gcc-of-print-asm-stmt
  (b* ((?new-pstate (print-asm-stmt asm pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-stmt

(defthm pristate->gcc-of-print-stmt
  (b* ((?new-pstate (print-stmt stmt pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-comp-stmt

(defthm pristate->gcc-of-print-comp-stmt
  (b* ((?new-pstate (print-comp-stmt cstmt pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-block-item

(defthm pristate->gcc-of-print-block-item
  (b* ((?new-pstate (print-block-item item pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: pristate->gcc-of-print-block-item-list

(defthm pristate->gcc-of-print-block-item-list
  (b* ((?new-pstate (print-block-item-list items pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Subtopics

Print-expr: Print an expression.
Print-typequal/attribspec-list-list: Print a list or one or more lists of type qualifiers and attribute specifiers corresponding to a `pointer' in the grammar.
Print-struni-spec: Print a structure or union specifier.
Print-comp-stmt: Print a compound statement.
Print-expr-list: Print a list of one or more expressions, separated by commas.
Print-struct-declon-list: Print a list of one or more structure declarations, separated by spaces.
Print-stmt: Print a statement, in one or more lines, with proper indentation.
Print-param-declor: Print a parameter declarator.
Print-dirdeclor: Print a direct declarator.
Print-struct-declor: Print a structure declarator.
Print-initer: Print an initializer.
Print-decl-inline: Print a declaration, inline.
Print-struct-declon: Print a structure declaration.
Print-genassoc-list: Print a list of one or more generic associations, separated by commas.
Print-enum-spec: Print an enueration specifier.
Print-absdeclor: Print an abstract declarator.
Print-typequal/attribspec-list: Print a list of one or more type qualifiers and attribute specifiers, separated by spaces.
Print-desiniter-list: Print a list of one or more initializers with optional designations, separated by commas.
Print-const-expr: Print a constant expression.
Print-attrib: Print a GCC attribute.
Print-tyname: Print a type name.
Print-struct-declor-list: Print a list of one or more structure declarators, separated by commas.
Print-spec/qual-list: Print a list of one or more specifiers and qualifiers, separated by spaces.
Print-param-declon-list: Print a list of one or more parameter declarations, separated by commas.
Print-param-declon: Print a parameter declaration.
Print-initdeclor-list: Print a list of one or more initializer declarators, separated by commas.
Print-designor-list: Print a list of one or more designators.
Print-decl-spec-list: Print a list of one or more declaration specifiers, separated by spaces.
Print-decl-list: Print a list of one or more declarations, one per line, all with the same indentation.
Print-attrib-spec-list: Print a list of one or more attribute specifiers, separated by single spaces.
Print-asm-output-list: Print a list of one or more assembler output operands, separated by commas.
Print-asm-input-list: Print a list of one or more assembler input operands, separated by commas.
Print-typequal/attribspec: Print a type qualifier or attribute specifier.
Print-statassert: Print a static assertion declaration.
Print-spec/qual: Print a specifier or qualifier.
Print-member-designor: Print a member designator.
Print-initdeclor: Print an initializer declarator.
Print-enumer-list: Print a list of one or more enumerators, separated by commas.
Print-dirabsdeclor: Print a direct abstract declarator.
Print-desiniter: Print an initializer with optional designations.
Print-decl-spec: Print a declaration specifier.
Print-decl: Print a declaration, in its own indented line.
Print-block-item-list: Print a list of zero or more block items.
Print-attrib-spec: Print an attribute specifier.
Print-attrib-list: Print a list of one or more GCC attributes, comma-separated.
Print-asm-output: Print an assembler output operand.
Print-align-spec: Print an alignment specifier.
Print-type-spec: Print a type specifier.
Print-label: Print a label.
Print-genassoc: Print a generic association.
Print-enumer: Print an enumerator.
Print-designor: Print a designator.
Print-declor: Print a declarator.
Print-block-item: Print a block item.
Print-asm-stmt: Print an assembler statement.
Print-asm-input: Print an assembler input operand.