Print a declaration, inline.
Here `inline' means that we print is as part of the current line, without adding new lines or indentation.
We ensure that there is at least one declaration specifier, as required by the grammar.
Function:
(defun print-decl-inline (decl pstate) (declare (xargs :guard (and (declp decl) (pristatep pstate)))) (declare (xargs :guard (decl-unambp decl))) (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-declspec-list decl.specs pstate)) (pstate (if decl.init (b* ((pstate (print-astring " " pstate)) (pstate (print-initdeclor-list decl.init pstate))) pstate) pstate)) (pstate (if decl.asm? (b* ((pstate (print-astring " " pstate)) (pstate (print-asm-name-spec decl.asm? pstate))) pstate) pstate)) (pstate (if decl.attrib (b* ((pstate (print-astring " " pstate)) (pstate (print-attrib-spec-list decl.attrib pstate))) pstate) pstate)) (pstate (print-astring ";" pstate))) pstate) :statassert (print-statassert decl.unwrap pstate))))
Theorem:
(defthm pristatep-of-print-decl-inline (b* ((new-pstate (print-decl-inline decl pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm print-decl-inline-of-decl-fix-decl (equal (print-decl-inline (decl-fix decl) pstate) (print-decl-inline decl pstate)))
Theorem:
(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:
(defthm print-decl-inline-of-pristate-fix-pstate (equal (print-decl-inline decl (pristate-fix pstate)) (print-decl-inline decl pstate)))
Theorem:
(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)