Print expressions, declarations, statements, and related entities.
Function:
(defun print-expr (expr expected-prio pstate) (declare (xargs :guard (and (exprp expr) (expr-priorityp expected-prio) (pristatep pstate)))) (declare (xargs :guard (expr-unambp expr))) (let ((__function__ 'print-expr)) (declare (ignorable __function__)) (b* ((actual-prio (expr->priority expr)) (parenp (not (expr-priority-<= expected-prio actual-prio))) (pstate (if parenp (print-astring "(" pstate) pstate)) (pstate (expr-case expr :ident (print-ident expr.unwrap pstate) :const (print-const expr.unwrap pstate) :string (b* (((unless expr.literals) (raise "Misusage error: ~ empty list of string literals.") (pristate-fix pstate))) (print-stringlit-list expr.literals pstate)) :paren (b* ((pstate (print-astring "(" pstate)) (pstate (print-expr expr.unwrap (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)) ((unless expr.elems) (raise "Misusage error: ~ empty initializer list.") (pristate-fix pstate)) (pstate (print-desiniter-list expr.elems pstate)) (pstate (if expr.final-comma (print-astring ", }" 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 (unop-case expr.op :sizeof) (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)) (expr-priority-unary) (expr-priority-cast))) (pstate (print-expr expr.arg arg-priority 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) :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 (print-expr expr.then (if raise-prio (expr-priority-logor) (expr-priority-expr)) 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)) :stmt (b* ((pstate (print-astring "(" pstate)) (pstate (print-block expr.items 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))) (pstate (if parenp (print-astring ")" pstate) pstate))) pstate)))
Function:
(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)))) (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:
(defun print-const-expr (cexpr pstate) (declare (xargs :guard (and (const-exprp cexpr) (pristatep pstate)))) (declare (xargs :guard (const-expr-unambp cexpr))) (let ((__function__ 'print-const-expr)) (declare (ignorable __function__)) (print-expr (const-expr->unwrap cexpr) (expr-priority-cond) pstate)))
Function:
(defun print-genassoc (genassoc pstate) (declare (xargs :guard (and (genassocp genassoc) (pristatep pstate)))) (declare (xargs :guard (genassoc-unambp genassoc))) (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:
(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)))) (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:
(defun print-member-designor (memdes pstate) (declare (xargs :guard (and (member-designorp memdes) (pristatep pstate)))) (declare (xargs :guard (member-designor-unambp memdes))) (let ((__function__ 'print-member-designor)) (declare (ignorable __function__)) (member-designor-case memdes :ident (print-ident memdes.unwrap 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:
(defun print-type-spec (tyspec pstate) (declare (xargs :guard (and (type-specp tyspec) (pristatep pstate)))) (declare (xargs :guard (type-spec-unambp tyspec))) (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-strunispec tyspec.unwrap pstate))) pstate) :union (b* ((pstate (print-astring "union " pstate)) (pstate (print-strunispec tyspec.unwrap pstate))) pstate) :enum (b* ((pstate (print-astring "enum " pstate)) (pstate (print-enumspec tyspec.unwrap pstate))) pstate) :typedef (print-ident tyspec.name pstate) :int128 (print-astring "__int128" pstate) :float128 (print-astring "_Float128" pstate) :builtin-va-list (print-astring "__builtin_va_list" 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)))))
Function:
(defun print-spec/qual (specqual pstate) (declare (xargs :guard (and (spec/qual-p specqual) (pristatep pstate)))) (declare (xargs :guard (spec/qual-unambp specqual))) (let ((__function__ 'print-spec/qual)) (declare (ignorable __function__)) (spec/qual-case specqual :tyspec (print-type-spec specqual.unwrap pstate) :tyqual (print-type-qual specqual.unwrap pstate) :align (print-align-spec specqual.unwrap pstate) :attrib (print-attrib-spec specqual.unwrap pstate))))
Function:
(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)))) (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:
(defun print-align-spec (alignspec pstate) (declare (xargs :guard (and (align-specp alignspec) (pristatep pstate)))) (declare (xargs :guard (align-spec-unambp alignspec))) (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.arg pstate) :alignas-ambig (prog2$ (impossible) (pristate-fix pstate)))) (pstate (print-astring ")" pstate))) pstate)))
Function:
(defun print-declspec (declspec pstate) (declare (xargs :guard (and (declspecp declspec) (pristatep pstate)))) (declare (xargs :guard (declspec-unambp declspec))) (let ((__function__ 'print-declspec)) (declare (ignorable __function__)) (declspec-case declspec :stocla (print-stor-spec declspec.unwrap pstate) :tyspec (print-type-spec declspec.unwrap pstate) :tyqual (print-type-qual declspec.unwrap pstate) :funspec (print-fun-spec declspec.unwrap pstate) :align (print-align-spec declspec.unwrap pstate) :attrib (print-attrib-spec declspec.unwrap pstate))))
Function:
(defun print-declspec-list (declspecs pstate) (declare (xargs :guard (and (declspec-listp declspecs) (pristatep pstate)))) (declare (xargs :guard (and (consp declspecs) (declspec-list-unambp declspecs)))) (let ((__function__ 'print-declspec-list)) (declare (ignorable __function__)) (b* (((unless (mbt (consp declspecs))) (pristate-fix pstate)) (pstate (print-declspec (car declspecs) pstate)) ((when (endp (cdr declspecs))) pstate) (pstate (print-astring " " pstate))) (print-declspec-list (cdr declspecs) pstate))))
Function:
(defun print-typequal/attribspec (tyqualattrib pstate) (declare (xargs :guard (and (typequal/attribspec-p tyqualattrib) (pristatep pstate)))) (let ((__function__ 'print-typequal/attribspec)) (declare (ignorable __function__)) (typequal/attribspec-case tyqualattrib :tyqual (print-type-qual tyqualattrib.unwrap pstate) :attrib (print-attrib-spec tyqualattrib.unwrap pstate))))
Function:
(defun print-typequal/attribspec-list (tyqualattribs pstate) (declare (xargs :guard (and (typequal/attribspec-listp tyqualattribs) (pristatep pstate)))) (declare (xargs :guard (consp tyqualattribs))) (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:
(defun print-typequal/attribspec-list-list (tyqualattribss pstate) (declare (xargs :guard (and (typequal/attribspec-list-listp tyqualattribss) (pristatep pstate)))) (declare (xargs :guard (consp tyqualattribss))) (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:
(defun print-initer (initer pstate) (declare (xargs :guard (and (initerp initer) (pristatep pstate)))) (declare (xargs :guard (initer-unambp initer))) (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:
(defun print-desiniter (desiniter pstate) (declare (xargs :guard (and (desiniterp desiniter) (pristatep pstate)))) (declare (xargs :guard (desiniter-unambp desiniter))) (let ((__function__ 'print-desiniter)) (declare (ignorable __function__)) (b* (((desiniter desiniter) desiniter) (pstate (if desiniter.design (b* ((pstate (print-designor-list desiniter.design pstate)) (pstate (print-astring " = " pstate))) pstate) pstate)) (pstate (print-initer desiniter.init pstate))) pstate)))
Function:
(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)))) (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:
(defun print-designor (designor pstate) (declare (xargs :guard (and (designorp designor) (pristatep pstate)))) (declare (xargs :guard (designor-unambp designor))) (let ((__function__ 'print-designor)) (declare (ignorable __function__)) (designor-case designor :sub (b* ((pstate (print-astring "[" pstate)) (pstate (print-const-expr designor.index pstate)) (pstate (print-astring "]" pstate))) pstate) :dot (b* ((pstate (print-astring "." pstate)) (pstate (print-ident designor.name pstate))) pstate))))
Function:
(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)))) (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:
(defun print-declor (declor pstate) (declare (xargs :guard (and (declorp declor) (pristatep pstate)))) (declare (xargs :guard (declor-unambp declor))) (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.decl pstate))) pstate)))
Function:
(defun print-dirdeclor (dirdeclor pstate) (declare (xargs :guard (and (dirdeclorp dirdeclor) (pristatep pstate)))) (declare (xargs :guard (dirdeclor-unambp dirdeclor))) (let ((__function__ 'print-dirdeclor)) (declare (ignorable __function__)) (dirdeclor-case dirdeclor :ident (print-ident dirdeclor.unwrap pstate) :paren (b* ((pstate (print-astring "(" pstate)) (pstate (print-declor dirdeclor.unwrap pstate)) (pstate (print-astring ")" pstate))) pstate) :array (b* ((pstate (print-dirdeclor dirdeclor.decl pstate)) (pstate (print-astring "[" pstate)) (pstate (if dirdeclor.tyquals (print-typequal/attribspec-list dirdeclor.tyquals pstate) pstate)) (pstate (if (and dirdeclor.tyquals dirdeclor.expr?) (print-astring " " pstate) pstate)) (pstate (if (expr-option-case dirdeclor.expr? :some) (print-expr (expr-option-some->val dirdeclor.expr?) (expr-priority-asg) pstate) pstate)) (pstate (print-astring "]" pstate))) pstate) :array-static1 (b* ((pstate (print-dirdeclor dirdeclor.decl pstate)) (pstate (print-astring "static " pstate)) (pstate (if dirdeclor.tyquals (b* ((pstate (print-typequal/attribspec-list dirdeclor.tyquals pstate)) (pstate (print-astring " " pstate))) pstate) pstate)) (pstate (print-expr dirdeclor.expr (expr-priority-asg) pstate)) (pstate (print-astring "]" pstate))) pstate) :array-static2 (b* ((pstate (print-dirdeclor dirdeclor.decl pstate)) ((unless dirdeclor.tyquals) (raise "Misusage error: ~ empty list of type qualifiers.") pstate) (pstate (print-typequal/attribspec-list dirdeclor.tyquals pstate)) (pstate (print-astring " static " pstate)) (pstate (print-expr dirdeclor.expr (expr-priority-asg) pstate)) (pstate (print-astring "]" pstate))) pstate) :array-star (b* ((pstate (print-dirdeclor dirdeclor.decl pstate)) (pstate (print-astring "[" pstate)) (pstate (if dirdeclor.tyquals (b* ((pstate (print-typequal/attribspec-list dirdeclor.tyquals pstate)) (pstate (print-astring " " pstate))) pstate) pstate)) (pstate (print-astring "*]" pstate))) pstate) :function-params (b* ((pstate (print-dirdeclor dirdeclor.decl pstate)) (pstate (print-astring "(" pstate)) (pstate (if dirdeclor.params (print-paramdecl-list dirdeclor.params pstate) pstate)) (pstate (if dirdeclor.ellipsis (print-astring ", ...)" pstate) (print-astring ")" pstate)))) pstate) :function-names (b* ((pstate (print-dirdeclor dirdeclor.decl pstate)) (pstate (print-astring "(" pstate)) (pstate (if dirdeclor.names (print-ident-list dirdeclor.names pstate) pstate)) (pstate (print-astring ")" pstate))) pstate))))
Function:
(defun print-absdeclor (absdeclor pstate) (declare (xargs :guard (and (absdeclorp absdeclor) (pristatep pstate)))) (declare (xargs :guard (absdeclor-unambp absdeclor))) (let ((__function__ 'print-absdeclor)) (declare (ignorable __function__)) (b* (((absdeclor absdeclor) absdeclor) ((unless (or absdeclor.pointers absdeclor.decl?)) (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.decl? :some) (print-dirabsdeclor (dirabsdeclor-option-some->val absdeclor.decl?) pstate) pstate))) pstate)))
Function:
(defun print-dirabsdeclor (dirabsdeclor pstate) (declare (xargs :guard (and (dirabsdeclorp dirabsdeclor) (pristatep pstate)))) (declare (xargs :guard (dirabsdeclor-unambp dirabsdeclor))) (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.unwrap pstate)) (pstate (print-astring ")" pstate))) pstate) :array (b* ((pstate (if (dirabsdeclor-option-case dirabsdeclor.decl? :some) (print-dirabsdeclor (dirabsdeclor-option-some->val dirabsdeclor.decl?) pstate) pstate)) (pstate (print-astring "[" pstate)) (pstate (if dirabsdeclor.tyquals (print-typequal/attribspec-list dirabsdeclor.tyquals pstate) pstate)) (pstate (if (and dirabsdeclor.tyquals dirabsdeclor.expr?) (print-astring " " pstate) pstate)) (pstate (if (expr-option-case dirabsdeclor.expr? :some) (print-expr (expr-option-some->val dirabsdeclor.expr?) (expr-priority-asg) pstate) pstate)) (pstate (print-astring "]" pstate))) pstate) :array-static1 (b* ((pstate (if (dirabsdeclor-option-case dirabsdeclor.decl? :some) (print-dirabsdeclor (dirabsdeclor-option-some->val dirabsdeclor.decl?) pstate) pstate)) (pstate (print-astring "static " pstate)) (pstate (if dirabsdeclor.tyquals (b* ((pstate (print-typequal/attribspec-list dirabsdeclor.tyquals pstate)) (pstate (print-astring " " pstate))) pstate) pstate)) (pstate (print-expr dirabsdeclor.expr (expr-priority-asg) pstate)) (pstate (print-astring "]" pstate))) pstate) :array-static2 (b* ((pstate (if (dirabsdeclor-option-case dirabsdeclor.decl? :some) (print-dirabsdeclor (dirabsdeclor-option-some->val dirabsdeclor.decl?) pstate) pstate)) ((unless dirabsdeclor.tyquals) (raise "Misusage error: ~ empty list of type qualifiers.") (pristate-fix pstate)) (pstate (print-typequal/attribspec-list dirabsdeclor.tyquals pstate)) (pstate (print-astring " static " pstate)) (pstate (print-expr dirabsdeclor.expr (expr-priority-asg) pstate)) (pstate (print-astring "]" pstate))) pstate) :array-star (b* ((pstate (if (dirabsdeclor-option-case dirabsdeclor.decl? :some) (print-dirabsdeclor (dirabsdeclor-option-some->val dirabsdeclor.decl?) pstate) pstate)) (pstate (print-astring "[*]" pstate))) pstate) :function (b* ((pstate (if (dirabsdeclor-option-case dirabsdeclor.decl? :some) (print-dirabsdeclor (dirabsdeclor-option-some->val dirabsdeclor.decl?) pstate) pstate)) (pstate (print-astring "(" pstate)) (pstate (if dirabsdeclor.params (b* ((pstate (print-paramdecl-list dirabsdeclor.params pstate)) (pstate (if dirabsdeclor.ellipsis (print-astring ", ..." pstate) pstate))) pstate) pstate)) (pstate (print-astring ")" pstate))) pstate))))
Function:
(defun print-paramdecl (paramdecl pstate) (declare (xargs :guard (and (paramdeclp paramdecl) (pristatep pstate)))) (declare (xargs :guard (paramdecl-unambp paramdecl))) (let ((__function__ 'print-paramdecl)) (declare (ignorable __function__)) (b* (((paramdecl paramdecl) paramdecl) ((unless paramdecl.spec) (raise "Misusage error: no declaration specifiers.") (pristate-fix pstate)) (pstate (print-declspec-list paramdecl.spec pstate)) (pstate (print-paramdeclor paramdecl.decl pstate))) pstate)))
Function:
(defun print-paramdecl-list (paramdecls pstate) (declare (xargs :guard (and (paramdecl-listp paramdecls) (pristatep pstate)))) (declare (xargs :guard (and (consp paramdecls) (paramdecl-list-unambp paramdecls)))) (let ((__function__ 'print-paramdecl-list)) (declare (ignorable __function__)) (b* (((unless (mbt (consp paramdecls))) (pristate-fix pstate)) (pstate (print-paramdecl (car paramdecls) pstate)) ((when (endp (cdr paramdecls))) pstate) (pstate (print-astring ", " pstate))) (print-paramdecl-list (cdr paramdecls) pstate))))
Function:
(defun print-paramdeclor (paramdeclor pstate) (declare (xargs :guard (and (paramdeclorp paramdeclor) (pristatep pstate)))) (declare (xargs :guard (paramdeclor-unambp paramdeclor))) (let ((__function__ 'print-paramdeclor)) (declare (ignorable __function__)) (paramdeclor-case paramdeclor :declor (b* ((pstate (print-astring " " pstate)) (pstate (print-declor paramdeclor.unwrap pstate))) pstate) :absdeclor (b* ((pstate (print-astring " " pstate)) (pstate (print-absdeclor paramdeclor.unwrap pstate))) pstate) :none (pristate-fix pstate) :ambig (prog2$ (impossible) (pristate-fix pstate)))))
Function:
(defun print-tyname (tyname pstate) (declare (xargs :guard (and (tynamep tyname) (pristatep pstate)))) (declare (xargs :guard (tyname-unambp tyname))) (let ((__function__ 'print-tyname)) (declare (ignorable __function__)) (b* (((tyname tyname) tyname) ((unless tyname.specqual) (raise "Misusage error: empty list of specifiers and qualifiers.") (pristate-fix pstate)) (pstate (print-spec/qual-list tyname.specqual pstate)) ((unless (absdeclor-option-case tyname.decl? :some)) pstate) (pstate (print-astring " " pstate)) (pstate (print-absdeclor (absdeclor-option-some->val tyname.decl?) pstate))) pstate)))
Function:
(defun print-strunispec (strunispec pstate) (declare (xargs :guard (and (strunispecp strunispec) (pristatep pstate)))) (declare (xargs :guard (strunispec-unambp strunispec))) (let ((__function__ 'print-strunispec)) (declare (ignorable __function__)) (b* (((strunispec strunispec) strunispec) ((unless (or (ident-option-case strunispec.name :some) strunispec.members)) (raise "Misusage error: empty structure or union specifier.") (pristate-fix pstate)) (pstate (ident-option-case strunispec.name :some (print-ident strunispec.name.val pstate) :none pstate)) (pstate (if (and strunispec.name strunispec.members) (print-astring " " pstate) pstate)) ((when (not strunispec.members)) pstate) (pstate (print-astring "{ " pstate)) (pstate (print-structdecl-list strunispec.members pstate)) (pstate (print-astring " }" pstate))) pstate)))
Function:
(defun print-structdecl (structdecl pstate) (declare (xargs :guard (and (structdeclp structdecl) (pristatep pstate)))) (declare (xargs :guard (structdecl-unambp structdecl))) (let ((__function__ 'print-structdecl)) (declare (ignorable __function__)) (structdecl-case structdecl :member (b* ((pstate (if structdecl.extension (print-astring "__extension__ " pstate) (pristate-fix pstate))) ((unless structdecl.specqual) (raise "Misusage error: empty specifier/qualifier list.") pstate) (pstate (print-spec/qual-list structdecl.specqual pstate)) (pstate (if structdecl.declor (b* ((pstate (print-astring " " pstate)) (pstate (print-structdeclor-list structdecl.declor pstate))) pstate) pstate)) (pstate (if structdecl.attrib (b* ((pstate (print-astring " " pstate)) (pstate (print-attrib-spec-list structdecl.attrib pstate))) pstate) pstate)) (pstate (print-astring ";" pstate))) pstate) :statassert (print-statassert structdecl.unwrap pstate))))
Function:
(defun print-structdecl-list (structdecls pstate) (declare (xargs :guard (and (structdecl-listp structdecls) (pristatep pstate)))) (declare (xargs :guard (and (consp structdecls) (structdecl-list-unambp structdecls)))) (let ((__function__ 'print-structdecl-list)) (declare (ignorable __function__)) (b* (((unless (mbt (consp structdecls))) (pristate-fix pstate)) (pstate (print-structdecl (car structdecls) pstate)) ((when (endp (cdr structdecls))) pstate) (pstate (print-astring " " pstate))) (print-structdecl-list (cdr structdecls) pstate))))
Function:
(defun print-structdeclor (structdeclor pstate) (declare (xargs :guard (and (structdeclorp structdeclor) (pristatep pstate)))) (declare (xargs :guard (structdeclor-unambp structdeclor))) (let ((__function__ 'print-structdeclor)) (declare (ignorable __function__)) (b* (((structdeclor 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:
(defun print-structdeclor-list (structdeclors pstate) (declare (xargs :guard (and (structdeclor-listp structdeclors) (pristatep pstate)))) (declare (xargs :guard (and (consp structdeclors) (structdeclor-list-unambp structdeclors)))) (let ((__function__ 'print-structdeclor-list)) (declare (ignorable __function__)) (b* (((unless (mbt (consp structdeclors))) (pristate-fix pstate)) (pstate (print-structdeclor (car structdeclors) pstate)) ((when (endp (cdr structdeclors))) pstate) (pstate (print-astring ", " pstate))) (print-structdeclor-list (cdr structdeclors) pstate))))
Function:
(defun print-enumspec (enumspec pstate) (declare (xargs :guard (and (enumspecp enumspec) (pristatep pstate)))) (declare (xargs :guard (enumspec-unambp enumspec))) (let ((__function__ 'print-enumspec)) (declare (ignorable __function__)) (b* (((enumspec 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:
(defun print-enumer (enumer pstate) (declare (xargs :guard (and (enumerp enumer) (pristatep pstate)))) (declare (xargs :guard (enumer-unambp enumer))) (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:
(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)))) (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:
(defun print-statassert (statassert pstate) (declare (xargs :guard (and (statassertp statassert) (pristatep pstate)))) (declare (xargs :guard (statassert-unambp statassert))) (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:
(defun print-attrib (attr pstate) (declare (xargs :guard (and (attribp attr) (pristatep pstate)))) (let ((__function__ 'print-attrib)) (declare (ignorable __function__)) (attrib-case attr :name (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:
(defun print-attrib-list (attrs pstate) (declare (xargs :guard (and (attrib-listp attrs) (pristatep pstate)))) (declare (xargs :guard (consp attrs))) (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:
(defun print-attrib-spec (attrspec pstate) (declare (xargs :guard (and (attrib-specp attrspec) (pristatep 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:
(defun print-attrib-spec-list (attrspecs pstate) (declare (xargs :guard (and (attrib-spec-listp attrspecs) (pristatep pstate)))) (declare (xargs :guard (consp attrspecs))) (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:
(defun print-initdeclor (initdeclor pstate) (declare (xargs :guard (and (initdeclorp initdeclor) (pristatep pstate)))) (declare (xargs :guard (initdeclor-unambp initdeclor))) (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)) ((when (initer-option-case initdeclor.init? :none)) pstate) (pstate (print-astring " = " pstate)) (pstate (print-initer (initer-option-some->val initdeclor.init?) pstate))) pstate)))
Function:
(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)))) (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:
(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.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))))
Function:
(defun print-decl (decl pstate) (declare (xargs :guard (and (declp decl) (pristatep pstate)))) (declare (xargs :guard (decl-unambp decl))) (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:
(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)))) (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:
(defun print-label (label pstate) (declare (xargs :guard (and (labelp label) (pristatep pstate)))) (declare (xargs :guard (label-unambp label))) (let ((__function__ 'print-label)) (declare (ignorable __function__)) (label-case label :name (print-ident label.unwrap 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:
(defun print-asm-output (output pstate) (declare (xargs :guard (and (asm-outputp output) (pristatep 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:
(defun print-asm-output-list (outputs pstate) (declare (xargs :guard (and (asm-output-listp outputs) (pristatep pstate)))) (declare (xargs :guard (consp outputs))) (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:
(defun print-asm-input (input pstate) (declare (xargs :guard (and (asm-inputp input) (pristatep 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:
(defun print-asm-input-list (inputs pstate) (declare (xargs :guard (and (asm-input-listp inputs) (pristatep pstate)))) (declare (xargs :guard (consp inputs))) (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:
(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.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-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.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-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-expr.new-pstate (b* ((?new-pstate (print-expr expr expected-prio pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-expr-list.new-pstate (b* ((?new-pstate (print-expr-list exprs pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-const-expr.new-pstate (b* ((?new-pstate (print-const-expr cexpr pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-genassoc.new-pstate (b* ((?new-pstate (print-genassoc genassoc pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-genassoc-list.new-pstate (b* ((?new-pstate (print-genassoc-list genassocs pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-member-designor.new-pstate (b* ((?new-pstate (print-member-designor memdes pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-type-spec.new-pstate (b* ((?new-pstate (print-type-spec tyspec pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-spec/qual.new-pstate (b* ((?new-pstate (print-spec/qual specqual pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(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:
(defthm return-type-of-print-align-spec.new-pstate (b* ((?new-pstate (print-align-spec alignspec pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-declspec.new-pstate (b* ((?new-pstate (print-declspec declspec pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-declspec-list.new-pstate (b* ((?new-pstate (print-declspec-list declspecs pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-typequal/attribspec.new-pstate (b* ((?new-pstate (print-typequal/attribspec tyqualattrib pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(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:
(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:
(defthm return-type-of-print-initer.new-pstate (b* ((?new-pstate (print-initer initer pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-desiniter.new-pstate (b* ((?new-pstate (print-desiniter desiniter pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-desiniter-list.new-pstate (b* ((?new-pstate (print-desiniter-list desiniters pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-designor.new-pstate (b* ((?new-pstate (print-designor designor pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-designor-list.new-pstate (b* ((?new-pstate (print-designor-list designors pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-declor.new-pstate (b* ((?new-pstate (print-declor declor pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-dirdeclor.new-pstate (b* ((?new-pstate (print-dirdeclor dirdeclor pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-absdeclor.new-pstate (b* ((?new-pstate (print-absdeclor absdeclor pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-dirabsdeclor.new-pstate (b* ((?new-pstate (print-dirabsdeclor dirabsdeclor pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-paramdecl.new-pstate (b* ((?new-pstate (print-paramdecl paramdecl pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-paramdecl-list.new-pstate (b* ((?new-pstate (print-paramdecl-list paramdecls pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-paramdeclor.new-pstate (b* ((?new-pstate (print-paramdeclor paramdeclor pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-tyname.new-pstate (b* ((?new-pstate (print-tyname tyname pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-strunispec.new-pstate (b* ((?new-pstate (print-strunispec strunispec pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-structdecl.new-pstate (b* ((?new-pstate (print-structdecl structdecl pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-structdecl-list.new-pstate (b* ((?new-pstate (print-structdecl-list structdecls pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-structdeclor.new-pstate (b* ((?new-pstate (print-structdeclor structdeclor pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-structdeclor-list.new-pstate (b* ((?new-pstate (print-structdeclor-list structdeclors pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-enumspec.new-pstate (b* ((?new-pstate (print-enumspec enumspec pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-enumer.new-pstate (b* ((?new-pstate (print-enumer enumer pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-enumer-list.new-pstate (b* ((?new-pstate (print-enumer-list enumers pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-statassert.new-pstate (b* ((?new-pstate (print-statassert statassert pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-attrib.new-pstate (b* ((?new-pstate (print-attrib attr pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-attrib-list.new-pstate (b* ((?new-pstate (print-attrib-list attrs pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-attrib-spec.new-pstate (b* ((?new-pstate (print-attrib-spec attrspec pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(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:
(defthm return-type-of-print-initdeclor.new-pstate (b* ((?new-pstate (print-initdeclor initdeclor pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-initdeclor-list.new-pstate (b* ((?new-pstate (print-initdeclor-list initdeclors pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-decl-inline.new-pstate (b* ((?new-pstate (print-decl-inline decl pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-decl.new-pstate (b* ((?new-pstate (print-decl decl pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-decl-list.new-pstate (b* ((?new-pstate (print-decl-list decls pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-label.new-pstate (b* ((?new-pstate (print-label label pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-asm-output.new-pstate (b* ((?new-pstate (print-asm-output output pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(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:
(defthm return-type-of-print-asm-input.new-pstate (b* ((?new-pstate (print-asm-input input pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(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:
(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-expr-of-expr-fix-expr (equal (print-expr (expr-fix expr) expected-prio pstate) (print-expr expr expected-prio pstate)))
Theorem:
(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:
(defthm print-expr-of-pristate-fix-pstate (equal (print-expr expr expected-prio (pristate-fix pstate)) (print-expr expr expected-prio pstate)))
Theorem:
(defthm print-expr-list-of-expr-list-fix-exprs (equal (print-expr-list (expr-list-fix exprs) pstate) (print-expr-list exprs pstate)))
Theorem:
(defthm print-expr-list-of-pristate-fix-pstate (equal (print-expr-list exprs (pristate-fix pstate)) (print-expr-list exprs pstate)))
Theorem:
(defthm print-const-expr-of-const-expr-fix-cexpr (equal (print-const-expr (const-expr-fix cexpr) pstate) (print-const-expr cexpr pstate)))
Theorem:
(defthm print-const-expr-of-pristate-fix-pstate (equal (print-const-expr cexpr (pristate-fix pstate)) (print-const-expr cexpr pstate)))
Theorem:
(defthm print-genassoc-of-genassoc-fix-genassoc (equal (print-genassoc (genassoc-fix genassoc) pstate) (print-genassoc genassoc pstate)))
Theorem:
(defthm print-genassoc-of-pristate-fix-pstate (equal (print-genassoc genassoc (pristate-fix pstate)) (print-genassoc genassoc pstate)))
Theorem:
(defthm print-genassoc-list-of-genassoc-list-fix-genassocs (equal (print-genassoc-list (genassoc-list-fix genassocs) pstate) (print-genassoc-list genassocs pstate)))
Theorem:
(defthm print-genassoc-list-of-pristate-fix-pstate (equal (print-genassoc-list genassocs (pristate-fix pstate)) (print-genassoc-list genassocs pstate)))
Theorem:
(defthm print-member-designor-of-member-designor-fix-memdes (equal (print-member-designor (member-designor-fix memdes) pstate) (print-member-designor memdes pstate)))
Theorem:
(defthm print-member-designor-of-pristate-fix-pstate (equal (print-member-designor memdes (pristate-fix pstate)) (print-member-designor memdes pstate)))
Theorem:
(defthm print-type-spec-of-type-spec-fix-tyspec (equal (print-type-spec (type-spec-fix tyspec) pstate) (print-type-spec tyspec pstate)))
Theorem:
(defthm print-type-spec-of-pristate-fix-pstate (equal (print-type-spec tyspec (pristate-fix pstate)) (print-type-spec tyspec pstate)))
Theorem:
(defthm print-spec/qual-of-spec/qual-fix-specqual (equal (print-spec/qual (spec/qual-fix specqual) pstate) (print-spec/qual specqual pstate)))
Theorem:
(defthm print-spec/qual-of-pristate-fix-pstate (equal (print-spec/qual specqual (pristate-fix pstate)) (print-spec/qual specqual pstate)))
Theorem:
(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:
(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:
(defthm print-align-spec-of-align-spec-fix-alignspec (equal (print-align-spec (align-spec-fix alignspec) pstate) (print-align-spec alignspec pstate)))
Theorem:
(defthm print-align-spec-of-pristate-fix-pstate (equal (print-align-spec alignspec (pristate-fix pstate)) (print-align-spec alignspec pstate)))
Theorem:
(defthm print-declspec-of-declspec-fix-declspec (equal (print-declspec (declspec-fix declspec) pstate) (print-declspec declspec pstate)))
Theorem:
(defthm print-declspec-of-pristate-fix-pstate (equal (print-declspec declspec (pristate-fix pstate)) (print-declspec declspec pstate)))
Theorem:
(defthm print-declspec-list-of-declspec-list-fix-declspecs (equal (print-declspec-list (declspec-list-fix declspecs) pstate) (print-declspec-list declspecs pstate)))
Theorem:
(defthm print-declspec-list-of-pristate-fix-pstate (equal (print-declspec-list declspecs (pristate-fix pstate)) (print-declspec-list declspecs pstate)))
Theorem:
(defthm print-typequal/attribspec-of-typequal/attribspec-fix-tyqualattrib (equal (print-typequal/attribspec (typequal/attribspec-fix tyqualattrib) pstate) (print-typequal/attribspec tyqualattrib pstate)))
Theorem:
(defthm print-typequal/attribspec-of-pristate-fix-pstate (equal (print-typequal/attribspec tyqualattrib (pristate-fix pstate)) (print-typequal/attribspec tyqualattrib pstate)))
Theorem:
(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:
(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:
(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:
(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:
(defthm print-initer-of-initer-fix-initer (equal (print-initer (initer-fix initer) pstate) (print-initer initer pstate)))
Theorem:
(defthm print-initer-of-pristate-fix-pstate (equal (print-initer initer (pristate-fix pstate)) (print-initer initer pstate)))
Theorem:
(defthm print-desiniter-of-desiniter-fix-desiniter (equal (print-desiniter (desiniter-fix desiniter) pstate) (print-desiniter desiniter pstate)))
Theorem:
(defthm print-desiniter-of-pristate-fix-pstate (equal (print-desiniter desiniter (pristate-fix pstate)) (print-desiniter desiniter pstate)))
Theorem:
(defthm print-desiniter-list-of-desiniter-list-fix-desiniters (equal (print-desiniter-list (desiniter-list-fix desiniters) pstate) (print-desiniter-list desiniters pstate)))
Theorem:
(defthm print-desiniter-list-of-pristate-fix-pstate (equal (print-desiniter-list desiniters (pristate-fix pstate)) (print-desiniter-list desiniters pstate)))
Theorem:
(defthm print-designor-of-designor-fix-designor (equal (print-designor (designor-fix designor) pstate) (print-designor designor pstate)))
Theorem:
(defthm print-designor-of-pristate-fix-pstate (equal (print-designor designor (pristate-fix pstate)) (print-designor designor pstate)))
Theorem:
(defthm print-designor-list-of-designor-list-fix-designors (equal (print-designor-list (designor-list-fix designors) pstate) (print-designor-list designors pstate)))
Theorem:
(defthm print-designor-list-of-pristate-fix-pstate (equal (print-designor-list designors (pristate-fix pstate)) (print-designor-list designors pstate)))
Theorem:
(defthm print-declor-of-declor-fix-declor (equal (print-declor (declor-fix declor) pstate) (print-declor declor pstate)))
Theorem:
(defthm print-declor-of-pristate-fix-pstate (equal (print-declor declor (pristate-fix pstate)) (print-declor declor pstate)))
Theorem:
(defthm print-dirdeclor-of-dirdeclor-fix-dirdeclor (equal (print-dirdeclor (dirdeclor-fix dirdeclor) pstate) (print-dirdeclor dirdeclor pstate)))
Theorem:
(defthm print-dirdeclor-of-pristate-fix-pstate (equal (print-dirdeclor dirdeclor (pristate-fix pstate)) (print-dirdeclor dirdeclor pstate)))
Theorem:
(defthm print-absdeclor-of-absdeclor-fix-absdeclor (equal (print-absdeclor (absdeclor-fix absdeclor) pstate) (print-absdeclor absdeclor pstate)))
Theorem:
(defthm print-absdeclor-of-pristate-fix-pstate (equal (print-absdeclor absdeclor (pristate-fix pstate)) (print-absdeclor absdeclor pstate)))
Theorem:
(defthm print-dirabsdeclor-of-dirabsdeclor-fix-dirabsdeclor (equal (print-dirabsdeclor (dirabsdeclor-fix dirabsdeclor) pstate) (print-dirabsdeclor dirabsdeclor pstate)))
Theorem:
(defthm print-dirabsdeclor-of-pristate-fix-pstate (equal (print-dirabsdeclor dirabsdeclor (pristate-fix pstate)) (print-dirabsdeclor dirabsdeclor pstate)))
Theorem:
(defthm print-paramdecl-of-paramdecl-fix-paramdecl (equal (print-paramdecl (paramdecl-fix paramdecl) pstate) (print-paramdecl paramdecl pstate)))
Theorem:
(defthm print-paramdecl-of-pristate-fix-pstate (equal (print-paramdecl paramdecl (pristate-fix pstate)) (print-paramdecl paramdecl pstate)))
Theorem:
(defthm print-paramdecl-list-of-paramdecl-list-fix-paramdecls (equal (print-paramdecl-list (paramdecl-list-fix paramdecls) pstate) (print-paramdecl-list paramdecls pstate)))
Theorem:
(defthm print-paramdecl-list-of-pristate-fix-pstate (equal (print-paramdecl-list paramdecls (pristate-fix pstate)) (print-paramdecl-list paramdecls pstate)))
Theorem:
(defthm print-paramdeclor-of-paramdeclor-fix-paramdeclor (equal (print-paramdeclor (paramdeclor-fix paramdeclor) pstate) (print-paramdeclor paramdeclor pstate)))
Theorem:
(defthm print-paramdeclor-of-pristate-fix-pstate (equal (print-paramdeclor paramdeclor (pristate-fix pstate)) (print-paramdeclor paramdeclor pstate)))
Theorem:
(defthm print-tyname-of-tyname-fix-tyname (equal (print-tyname (tyname-fix tyname) pstate) (print-tyname tyname pstate)))
Theorem:
(defthm print-tyname-of-pristate-fix-pstate (equal (print-tyname tyname (pristate-fix pstate)) (print-tyname tyname pstate)))
Theorem:
(defthm print-strunispec-of-strunispec-fix-strunispec (equal (print-strunispec (strunispec-fix strunispec) pstate) (print-strunispec strunispec pstate)))
Theorem:
(defthm print-strunispec-of-pristate-fix-pstate (equal (print-strunispec strunispec (pristate-fix pstate)) (print-strunispec strunispec pstate)))
Theorem:
(defthm print-structdecl-of-structdecl-fix-structdecl (equal (print-structdecl (structdecl-fix structdecl) pstate) (print-structdecl structdecl pstate)))
Theorem:
(defthm print-structdecl-of-pristate-fix-pstate (equal (print-structdecl structdecl (pristate-fix pstate)) (print-structdecl structdecl pstate)))
Theorem:
(defthm print-structdecl-list-of-structdecl-list-fix-structdecls (equal (print-structdecl-list (structdecl-list-fix structdecls) pstate) (print-structdecl-list structdecls pstate)))
Theorem:
(defthm print-structdecl-list-of-pristate-fix-pstate (equal (print-structdecl-list structdecls (pristate-fix pstate)) (print-structdecl-list structdecls pstate)))
Theorem:
(defthm print-structdeclor-of-structdeclor-fix-structdeclor (equal (print-structdeclor (structdeclor-fix structdeclor) pstate) (print-structdeclor structdeclor pstate)))
Theorem:
(defthm print-structdeclor-of-pristate-fix-pstate (equal (print-structdeclor structdeclor (pristate-fix pstate)) (print-structdeclor structdeclor pstate)))
Theorem:
(defthm print-structdeclor-list-of-structdeclor-list-fix-structdeclors (equal (print-structdeclor-list (structdeclor-list-fix structdeclors) pstate) (print-structdeclor-list structdeclors pstate)))
Theorem:
(defthm print-structdeclor-list-of-pristate-fix-pstate (equal (print-structdeclor-list structdeclors (pristate-fix pstate)) (print-structdeclor-list structdeclors pstate)))
Theorem:
(defthm print-enumspec-of-enumspec-fix-enumspec (equal (print-enumspec (enumspec-fix enumspec) pstate) (print-enumspec enumspec pstate)))
Theorem:
(defthm print-enumspec-of-pristate-fix-pstate (equal (print-enumspec enumspec (pristate-fix pstate)) (print-enumspec enumspec pstate)))
Theorem:
(defthm print-enumer-of-enumer-fix-enumer (equal (print-enumer (enumer-fix enumer) pstate) (print-enumer enumer pstate)))
Theorem:
(defthm print-enumer-of-pristate-fix-pstate (equal (print-enumer enumer (pristate-fix pstate)) (print-enumer enumer pstate)))
Theorem:
(defthm print-enumer-list-of-enumer-list-fix-enumers (equal (print-enumer-list (enumer-list-fix enumers) pstate) (print-enumer-list enumers pstate)))
Theorem:
(defthm print-enumer-list-of-pristate-fix-pstate (equal (print-enumer-list enumers (pristate-fix pstate)) (print-enumer-list enumers pstate)))
Theorem:
(defthm print-statassert-of-statassert-fix-statassert (equal (print-statassert (statassert-fix statassert) pstate) (print-statassert statassert pstate)))
Theorem:
(defthm print-statassert-of-pristate-fix-pstate (equal (print-statassert statassert (pristate-fix pstate)) (print-statassert statassert pstate)))
Theorem:
(defthm print-attrib-of-attrib-fix-attr (equal (print-attrib (attrib-fix attr) pstate) (print-attrib attr pstate)))
Theorem:
(defthm print-attrib-of-pristate-fix-pstate (equal (print-attrib attr (pristate-fix pstate)) (print-attrib attr pstate)))
Theorem:
(defthm print-attrib-list-of-attrib-list-fix-attrs (equal (print-attrib-list (attrib-list-fix attrs) pstate) (print-attrib-list attrs pstate)))
Theorem:
(defthm print-attrib-list-of-pristate-fix-pstate (equal (print-attrib-list attrs (pristate-fix pstate)) (print-attrib-list attrs pstate)))
Theorem:
(defthm print-attrib-spec-of-attrib-spec-fix-attrspec (equal (print-attrib-spec (attrib-spec-fix attrspec) pstate) (print-attrib-spec attrspec pstate)))
Theorem:
(defthm print-attrib-spec-of-pristate-fix-pstate (equal (print-attrib-spec attrspec (pristate-fix pstate)) (print-attrib-spec attrspec pstate)))
Theorem:
(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:
(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:
(defthm print-initdeclor-of-initdeclor-fix-initdeclor (equal (print-initdeclor (initdeclor-fix initdeclor) pstate) (print-initdeclor initdeclor pstate)))
Theorem:
(defthm print-initdeclor-of-pristate-fix-pstate (equal (print-initdeclor initdeclor (pristate-fix pstate)) (print-initdeclor initdeclor pstate)))
Theorem:
(defthm print-initdeclor-list-of-initdeclor-list-fix-initdeclors (equal (print-initdeclor-list (initdeclor-list-fix initdeclors) pstate) (print-initdeclor-list initdeclors pstate)))
Theorem:
(defthm print-initdeclor-list-of-pristate-fix-pstate (equal (print-initdeclor-list initdeclors (pristate-fix pstate)) (print-initdeclor-list initdeclors pstate)))
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-of-pristate-fix-pstate (equal (print-decl-inline decl (pristate-fix pstate)) (print-decl-inline decl pstate)))
Theorem:
(defthm print-decl-of-decl-fix-decl (equal (print-decl (decl-fix decl) pstate) (print-decl decl pstate)))
Theorem:
(defthm print-decl-of-pristate-fix-pstate (equal (print-decl decl (pristate-fix pstate)) (print-decl decl pstate)))
Theorem:
(defthm print-decl-list-of-decl-list-fix-decls (equal (print-decl-list (decl-list-fix decls) pstate) (print-decl-list decls pstate)))
Theorem:
(defthm print-decl-list-of-pristate-fix-pstate (equal (print-decl-list decls (pristate-fix pstate)) (print-decl-list decls pstate)))
Theorem:
(defthm print-label-of-label-fix-label (equal (print-label (label-fix label) pstate) (print-label label pstate)))
Theorem:
(defthm print-label-of-pristate-fix-pstate (equal (print-label label (pristate-fix pstate)) (print-label label pstate)))
Theorem:
(defthm print-asm-output-of-asm-output-fix-output (equal (print-asm-output (asm-output-fix output) pstate) (print-asm-output output pstate)))
Theorem:
(defthm print-asm-output-of-pristate-fix-pstate (equal (print-asm-output output (pristate-fix pstate)) (print-asm-output output pstate)))
Theorem:
(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:
(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:
(defthm print-asm-input-of-asm-input-fix-input (equal (print-asm-input (asm-input-fix input) pstate) (print-asm-input input pstate)))
Theorem:
(defthm print-asm-input-of-pristate-fix-pstate (equal (print-asm-input input (pristate-fix pstate)) (print-asm-input input pstate)))
Theorem:
(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:
(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:
(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-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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(defthm print-declspec-declspec-equiv-congruence-on-declspec (implies (declspec-equiv declspec declspec-equiv) (equal (print-declspec declspec pstate) (print-declspec declspec-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-declspec-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-declspec declspec pstate) (print-declspec declspec pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-declspec-list-declspec-list-equiv-congruence-on-declspecs (implies (declspec-list-equiv declspecs declspecs-equiv) (equal (print-declspec-list declspecs pstate) (print-declspec-list declspecs-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-declspec-list-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-declspec-list declspecs pstate) (print-declspec-list declspecs pstate-equiv))) :rule-classes :congruence)
Theorem:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(defthm print-paramdecl-paramdecl-equiv-congruence-on-paramdecl (implies (paramdecl-equiv paramdecl paramdecl-equiv) (equal (print-paramdecl paramdecl pstate) (print-paramdecl paramdecl-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-paramdecl-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-paramdecl paramdecl pstate) (print-paramdecl paramdecl pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-paramdecl-list-paramdecl-list-equiv-congruence-on-paramdecls (implies (paramdecl-list-equiv paramdecls paramdecls-equiv) (equal (print-paramdecl-list paramdecls pstate) (print-paramdecl-list paramdecls-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-paramdecl-list-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-paramdecl-list paramdecls pstate) (print-paramdecl-list paramdecls pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-paramdeclor-paramdeclor-equiv-congruence-on-paramdeclor (implies (paramdeclor-equiv paramdeclor paramdeclor-equiv) (equal (print-paramdeclor paramdeclor pstate) (print-paramdeclor paramdeclor-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-paramdeclor-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-paramdeclor paramdeclor pstate) (print-paramdeclor paramdeclor pstate-equiv))) :rule-classes :congruence)
Theorem:
(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:
(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:
(defthm print-strunispec-strunispec-equiv-congruence-on-strunispec (implies (strunispec-equiv strunispec strunispec-equiv) (equal (print-strunispec strunispec pstate) (print-strunispec strunispec-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-strunispec-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-strunispec strunispec pstate) (print-strunispec strunispec pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-structdecl-structdecl-equiv-congruence-on-structdecl (implies (structdecl-equiv structdecl structdecl-equiv) (equal (print-structdecl structdecl pstate) (print-structdecl structdecl-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-structdecl-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-structdecl structdecl pstate) (print-structdecl structdecl pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-structdecl-list-structdecl-list-equiv-congruence-on-structdecls (implies (structdecl-list-equiv structdecls structdecls-equiv) (equal (print-structdecl-list structdecls pstate) (print-structdecl-list structdecls-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-structdecl-list-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-structdecl-list structdecls pstate) (print-structdecl-list structdecls pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-structdeclor-structdeclor-equiv-congruence-on-structdeclor (implies (structdeclor-equiv structdeclor structdeclor-equiv) (equal (print-structdeclor structdeclor pstate) (print-structdeclor structdeclor-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-structdeclor-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-structdeclor structdeclor pstate) (print-structdeclor structdeclor pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-structdeclor-list-structdeclor-list-equiv-congruence-on-structdeclors (implies (structdeclor-list-equiv structdeclors structdeclors-equiv) (equal (print-structdeclor-list structdeclors pstate) (print-structdeclor-list structdeclors-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-structdeclor-list-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-structdeclor-list structdeclors pstate) (print-structdeclor-list structdeclors pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-enumspec-enumspec-equiv-congruence-on-enumspec (implies (enumspec-equiv enumspec enumspec-equiv) (equal (print-enumspec enumspec pstate) (print-enumspec enumspec-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-enumspec-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-enumspec enumspec pstate) (print-enumspec enumspec pstate-equiv))) :rule-classes :congruence)
Theorem:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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-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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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)