Check the well-formedness of identifiers declared in statements, blocks, cases, and function definitions.
Function:
(defun check-identifiers-statement (stmt) (declare (xargs :guard (statementp stmt))) (let ((__function__ 'check-identifiers-statement)) (declare (ignorable __function__)) (statement-case stmt :block (check-identifiers-block stmt.get) :variable-single (check-identifier stmt.name) :variable-multi (check-identifier-list stmt.names) :assign-single nil :assign-multi nil :funcall nil :if (check-identifiers-block stmt.body) :for (b* (((okf &) (check-identifiers-block stmt.init)) ((okf &) (check-identifiers-block stmt.update)) ((okf &) (check-identifiers-block stmt.body))) nil) :switch (b* (((okf &) (check-identifiers-swcase-list stmt.cases)) ((okf &) (check-identifiers-block-option stmt.default))) nil) :leave nil :break nil :continue nil :fundef (check-identifiers-fundef stmt.get))))
Function:
(defun check-identifiers-statement-list (stmts) (declare (xargs :guard (statement-listp stmts))) (let ((__function__ 'check-identifiers-statement-list)) (declare (ignorable __function__)) (b* (((when (endp stmts)) nil) ((okf &) (check-identifiers-statement (car stmts))) ((okf &) (check-identifiers-statement-list (cdr stmts)))) nil)))
Function:
(defun check-identifiers-block (block) (declare (xargs :guard (blockp block))) (let ((__function__ 'check-identifiers-block)) (declare (ignorable __function__)) (check-identifiers-statement-list (block->statements block))))
Function:
(defun check-identifiers-block-option (block?) (declare (xargs :guard (block-optionp block?))) (let ((__function__ 'check-identifiers-block-option)) (declare (ignorable __function__)) (block-option-case block? :none nil :some (check-identifiers-block block?.val))))
Function:
(defun check-identifiers-swcase (case) (declare (xargs :guard (swcasep case))) (let ((__function__ 'check-identifiers-swcase)) (declare (ignorable __function__)) (check-identifiers-block (swcase->body case))))
Function:
(defun check-identifiers-swcase-list (cases) (declare (xargs :guard (swcase-listp cases))) (let ((__function__ 'check-identifiers-swcase-list)) (declare (ignorable __function__)) (b* (((when (endp cases)) nil) ((okf &) (check-identifiers-swcase (car cases))) ((okf &) (check-identifiers-swcase-list (cdr cases)))) nil)))
Function:
(defun check-identifiers-fundef (fundef) (declare (xargs :guard (fundefp fundef))) (let ((__function__ 'check-identifiers-fundef)) (declare (ignorable __function__)) (b* (((okf &) (check-identifier (fundef->name fundef))) ((okf &) (check-identifiers-block (fundef->body fundef)))) nil)))
Theorem:
(defthm return-type-of-check-identifiers-statement._ (b* ((?_ (check-identifiers-statement stmt))) (reserr-optionp _)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-check-identifiers-statement-list._ (b* ((?_ (check-identifiers-statement-list stmts))) (reserr-optionp _)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-check-identifiers-block._ (b* ((?_ (check-identifiers-block block))) (reserr-optionp _)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-check-identifiers-block-option._ (b* ((?_ (check-identifiers-block-option block?))) (reserr-optionp _)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-check-identifiers-swcase._ (b* ((?_ (check-identifiers-swcase case))) (reserr-optionp _)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-check-identifiers-swcase-list._ (b* ((?_ (check-identifiers-swcase-list cases))) (reserr-optionp _)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-check-identifiers-fundef._ (b* ((?_ (check-identifiers-fundef fundef))) (reserr-optionp _)) :rule-classes :rewrite)
Theorem:
(defthm check-identifiers-statement-of-statement-fix-stmt (equal (check-identifiers-statement (statement-fix stmt)) (check-identifiers-statement stmt)))
Theorem:
(defthm check-identifiers-statement-list-of-statement-list-fix-stmts (equal (check-identifiers-statement-list (statement-list-fix stmts)) (check-identifiers-statement-list stmts)))
Theorem:
(defthm check-identifiers-block-of-block-fix-block (equal (check-identifiers-block (block-fix block)) (check-identifiers-block block)))
Theorem:
(defthm check-identifiers-block-option-of-block-option-fix-block? (equal (check-identifiers-block-option (block-option-fix block?)) (check-identifiers-block-option block?)))
Theorem:
(defthm check-identifiers-swcase-of-swcase-fix-case (equal (check-identifiers-swcase (swcase-fix case)) (check-identifiers-swcase case)))
Theorem:
(defthm check-identifiers-swcase-list-of-swcase-list-fix-cases (equal (check-identifiers-swcase-list (swcase-list-fix cases)) (check-identifiers-swcase-list cases)))
Theorem:
(defthm check-identifiers-fundef-of-fundef-fix-fundef (equal (check-identifiers-fundef (fundef-fix fundef)) (check-identifiers-fundef fundef)))
Theorem:
(defthm check-identifiers-statement-statement-equiv-congruence-on-stmt (implies (statement-equiv stmt stmt-equiv) (equal (check-identifiers-statement stmt) (check-identifiers-statement stmt-equiv))) :rule-classes :congruence)
Theorem:
(defthm check-identifiers-statement-list-statement-list-equiv-congruence-on-stmts (implies (statement-list-equiv stmts stmts-equiv) (equal (check-identifiers-statement-list stmts) (check-identifiers-statement-list stmts-equiv))) :rule-classes :congruence)
Theorem:
(defthm check-identifiers-block-block-equiv-congruence-on-block (implies (block-equiv block block-equiv) (equal (check-identifiers-block block) (check-identifiers-block block-equiv))) :rule-classes :congruence)
Theorem:
(defthm check-identifiers-block-option-block-option-equiv-congruence-on-block? (implies (block-option-equiv block? block?-equiv) (equal (check-identifiers-block-option block?) (check-identifiers-block-option block?-equiv))) :rule-classes :congruence)
Theorem:
(defthm check-identifiers-swcase-swcase-equiv-congruence-on-case (implies (swcase-equiv case case-equiv) (equal (check-identifiers-swcase case) (check-identifiers-swcase case-equiv))) :rule-classes :congruence)
Theorem:
(defthm check-identifiers-swcase-list-swcase-list-equiv-congruence-on-cases (implies (swcase-list-equiv cases cases-equiv) (equal (check-identifiers-swcase-list cases) (check-identifiers-swcase-list cases-equiv))) :rule-classes :congruence)
Theorem:
(defthm check-identifiers-fundef-fundef-equiv-congruence-on-fundef (implies (fundef-equiv fundef fundef-equiv) (equal (check-identifiers-fundef fundef) (check-identifiers-fundef fundef-equiv))) :rule-classes :congruence)