Print statements, blocks, and related entities.
Since statements and blocks are mutually recursive in our abstract syntax (as in the grammar), their printing functions are mutually recursive. Termination is easily proved, based on the sizes of the fixtypes.
Function:
(defun print-stmt (stmt pstate) (declare (xargs :guard (and (stmtp stmt) (pristatep pstate)))) (declare (xargs :guard (stmt-unambp stmt))) (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-block (stmt-compound->items 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-block stmt.items 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-block (stmt-compound->items 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-block (stmt-compound->items 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 (print-astring "else" pstate)) (pstate (if (stmt-case stmt.else :compound) (b* ((pstate (print-astring " " pstate)) (pstate (print-block (stmt-compound->items 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-block (stmt-compound->items 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-block (stmt-compound->items 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-block (stmt-compound->items 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))) (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 (expr-priority-expr) pstate) :none (print-astring " " pstate))) (pstate (print-astring "; " pstate)) (pstate (expr-option-case stmt.test :some (print-expr stmt.test (expr-priority-expr) pstate) :none pstate)) (pstate (print-astring "; " pstate)) (pstate (expr-option-case stmt.next :some (print-expr stmt.next (expr-priority-expr) pstate) :none pstate)) (pstate (print-astring ")" pstate))) (if (stmt-case stmt.body :compound) (b* ((pstate (print-astring " " pstate)) (pstate (print-block (stmt-compound->items 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 (expr-priority-expr) pstate) :none pstate)) (pstate (print-astring "; " pstate)) (pstate (expr-option-case stmt.next :some (print-expr stmt.next (expr-priority-expr) pstate) :none pstate)) (pstate (print-astring ")" pstate))) (if (stmt-case stmt.body :compound) (b* ((pstate (print-astring " " pstate)) (pstate (print-block (stmt-compound->items 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) :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 (b* ((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." (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:
(defun print-block-item (item pstate) (declare (xargs :guard (and (block-itemp item) (pristatep pstate)))) (declare (xargs :guard (block-item-unambp item))) (let ((__function__ 'print-block-item)) (declare (ignorable __function__)) (block-item-case item :decl (print-decl item.unwrap pstate) :stmt (print-stmt item.unwrap pstate) :ambig (prog2$ (impossible) (pristate-fix pstate)))))
Function:
(defun print-block-item-list (items pstate) (declare (xargs :guard (and (block-item-listp items) (pristatep pstate)))) (declare (xargs :guard (block-item-list-unambp items))) (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))))
Function:
(defun print-block (items pstate) (declare (xargs :guard (and (block-item-listp items) (pristatep pstate)))) (declare (xargs :guard (block-item-list-unambp items))) (let ((__function__ 'print-block)) (declare (ignorable __function__)) (b* ((pstate (print-astring "{" pstate)) (pstate (print-new-line pstate)) (pstate (inc-pristate-indent pstate)) (pstate (print-block-item-list items pstate)) (pstate (dec-pristate-indent pstate)) (pstate (print-indent pstate)) (pstate (print-astring "}" pstate))) pstate)))
Theorem:
(defthm return-type-of-print-stmt.new-pstate (b* ((?new-pstate (print-stmt stmt pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-block-item.new-pstate (b* ((?new-pstate (print-block-item item pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(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:
(defthm return-type-of-print-block.new-pstate (b* ((?new-pstate (print-block items pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm print-stmt-of-stmt-fix-stmt (equal (print-stmt (stmt-fix stmt) pstate) (print-stmt stmt pstate)))
Theorem:
(defthm print-stmt-of-pristate-fix-pstate (equal (print-stmt stmt (pristate-fix pstate)) (print-stmt stmt pstate)))
Theorem:
(defthm print-block-item-of-block-item-fix-item (equal (print-block-item (block-item-fix item) pstate) (print-block-item item pstate)))
Theorem:
(defthm print-block-item-of-pristate-fix-pstate (equal (print-block-item item (pristate-fix pstate)) (print-block-item item pstate)))
Theorem:
(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:
(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:
(defthm print-block-of-block-item-list-fix-items (equal (print-block (block-item-list-fix items) pstate) (print-block items pstate)))
Theorem:
(defthm print-block-of-pristate-fix-pstate (equal (print-block items (pristate-fix pstate)) (print-block items pstate)))
Theorem:
(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:
(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:
(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:
(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:
(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:
(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:
(defthm print-block-block-item-list-equiv-congruence-on-items (implies (block-item-list-equiv items items-equiv) (equal (print-block items pstate) (print-block items-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-block-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-block items pstate) (print-block items pstate-equiv))) :rule-classes :congruence)