Print a list or one or more lists of type qualifiers, corresponding to a `pointer' in the grammar.
(print-type-qual-list-list tyqualss pstate) → new-pstate
Our abstract syntax uses lists of lists of type qualifiers to model what the grammar calls `pointer', which is a sequence of one or more stars, each star followed by zero or more type qualifiers; see declor and absdeclor. Here we print such a `pointer', from its representation as a list of lists of type qualifiers.
The outer list must not be empty, as required in the guard.
We go through each inner list, printing a star for each;
if the inner list under consideration is empty,
the star is all we print;
if the inner list is not empty,
we also print a space,
the type qualifiers (separated by spaces),
and a space.
That is, we provide separation when there are type qualifiers.
But there are no extra separations for stars,
e.g. we print
Function:
(defun print-type-qual-list-list (tyqualss pstate) (declare (xargs :guard (and (type-qual-list-listp tyqualss) (pristatep pstate)))) (declare (xargs :guard (consp tyqualss))) (let ((__function__ 'print-type-qual-list-list)) (declare (ignorable __function__)) (b* (((unless (mbt (consp tyqualss))) (pristate-fix pstate)) (pstate (print-astring "*" pstate)) (tyquals (car tyqualss)) (pstate (if (consp tyquals) (b* ((pstate (print-astring " " pstate)) (pstate (print-type-qual-list tyquals pstate)) (pstate (print-astring " " pstate))) pstate) pstate)) ((when (endp (cdr tyqualss))) pstate)) (print-type-qual-list-list (cdr tyqualss) pstate))))
Theorem:
(defthm pristatep-of-print-type-qual-list-list (b* ((new-pstate (print-type-qual-list-list tyqualss pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm print-type-qual-list-list-of-type-qual-list-list-fix-tyqualss (equal (print-type-qual-list-list (type-qual-list-list-fix tyqualss) pstate) (print-type-qual-list-list tyqualss pstate)))
Theorem:
(defthm print-type-qual-list-list-type-qual-list-list-equiv-congruence-on-tyqualss (implies (type-qual-list-list-equiv tyqualss tyqualss-equiv) (equal (print-type-qual-list-list tyqualss pstate) (print-type-qual-list-list tyqualss-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-type-qual-list-list-of-pristate-fix-pstate (equal (print-type-qual-list-list tyqualss (pristate-fix pstate)) (print-type-qual-list-list tyqualss pstate)))
Theorem:
(defthm print-type-qual-list-list-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-type-qual-list-list tyqualss pstate) (print-type-qual-list-list tyqualss pstate-equiv))) :rule-classes :congruence)