Map statements and blocks to statements and blocks in the language definition.
Function:
(defun ldm-stmt (stmt) (declare (xargs :guard (stmtp stmt))) (declare (xargs :guard (stmt-unambp stmt))) (let ((__function__ 'ldm-stmt)) (declare (ignorable __function__)) (b* (((reterr) (c::stmt-null))) (stmt-case stmt :labeled (b* (((erp label1) (ldm-label stmt.label)) ((erp stmt1) (ldm-stmt stmt.stmt))) (retok (c::make-stmt-labeled :label label1 :body stmt1))) :compound (b* (((erp items1) (ldm-block-item-list stmt.items))) (retok (c::make-stmt-compound :items items1))) :expr (expr-option-case stmt.expr? :some (b* (((erp expr1) (ldm-expr stmt.expr?.val))) (retok (c::stmt-expr expr1))) :none (retok (c::make-stmt-null))) :if (b* (((erp test1) (ldm-expr stmt.test)) ((erp then1) (ldm-stmt stmt.then))) (retok (c::make-stmt-if :test test1 :then then1))) :ifelse (b* (((erp test1) (ldm-expr stmt.test)) ((erp then1) (ldm-stmt stmt.then)) ((erp else1) (ldm-stmt stmt.else))) (retok (c::make-stmt-ifelse :test test1 :then then1 :else else1))) :switch (b* (((erp ctrl1) (ldm-expr stmt.target)) ((erp body1) (ldm-stmt stmt.body))) (retok (c::make-stmt-switch :ctrl ctrl1 :body body1))) :while (b* (((erp test1) (ldm-expr stmt.test)) ((erp body1) (ldm-stmt stmt.body))) (retok (c::make-stmt-while :test test1 :body body1))) :dowhile (b* (((erp body1) (ldm-stmt stmt.body)) ((erp test1) (ldm-expr stmt.test))) (retok (c::make-stmt-dowhile :body body1 :test test1))) :for-expr (b* (((erp init1) (ldm-expr-option stmt.init)) ((erp test1) (ldm-expr-option stmt.test)) ((erp next1) (ldm-expr-option stmt.next)) ((erp body1) (ldm-stmt stmt.body))) (retok (c::make-stmt-for :init init1 :test test1 :next next1 :body body1))) :for-decl (reterr (msg "Unsupported 'for' loop ~x0 ~ with initializing declaration." (stmt-fix stmt))) :for-ambig (prog2$ (impossible) (reterr t)) :goto (b* (((erp ident1) (ldm-ident stmt.label))) (retok (c::make-stmt-goto :target ident1))) :continue (retok (c::stmt-continue)) :break (retok (c::stmt-break)) :return (b* (((erp expr?) (ldm-expr-option stmt.expr?))) (retok (c::make-stmt-return :value expr?))) :asm (reterr (msg "Unsupported assembler statement ~x0." (stmt-fix stmt)))))))
Function:
(defun ldm-block-item (item) (declare (xargs :guard (block-itemp item))) (declare (xargs :guard (block-item-unambp item))) (let ((__function__ 'ldm-block-item)) (declare (ignorable __function__)) (b* (((reterr) (c::block-item-stmt (c::stmt-null)))) (block-item-case item :decl (b* (((erp objdeclon) (ldm-decl-obj item.unwrap))) (retok (c::block-item-declon objdeclon))) :stmt (b* (((erp stmt) (ldm-stmt item.unwrap))) (retok (c::block-item-stmt stmt))) :ambig (prog2$ (impossible) (reterr t))))))
Function:
(defun ldm-block-item-list (items) (declare (xargs :guard (block-item-listp items))) (declare (xargs :guard (block-item-list-unambp items))) (let ((__function__ 'ldm-block-item-list)) (declare (ignorable __function__)) (b* (((reterr) nil) ((when (endp items)) (retok nil)) ((erp item1) (ldm-block-item (car items))) ((erp items1) (ldm-block-item-list (cdr items)))) (retok (cons item1 items1)))))
Theorem:
(defthm return-type-of-ldm-stmt.stmt1 (b* (((mv acl2::?erp ?stmt1) (ldm-stmt stmt))) (c::stmtp stmt1)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-ldm-block-item.item1 (b* (((mv acl2::?erp ?item1) (ldm-block-item item))) (c::block-itemp item1)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-ldm-block-item-list.items1 (b* (((mv acl2::?erp ?items1) (ldm-block-item-list items))) (c::block-item-listp items1)) :rule-classes :rewrite)
Theorem:
(defthm ldm-stmt-of-stmt-fix-stmt (equal (ldm-stmt (stmt-fix stmt)) (ldm-stmt stmt)))
Theorem:
(defthm ldm-block-item-of-block-item-fix-item (equal (ldm-block-item (block-item-fix item)) (ldm-block-item item)))
Theorem:
(defthm ldm-block-item-list-of-block-item-list-fix-items (equal (ldm-block-item-list (block-item-list-fix items)) (ldm-block-item-list items)))
Theorem:
(defthm ldm-stmt-stmt-equiv-congruence-on-stmt (implies (stmt-equiv stmt stmt-equiv) (equal (ldm-stmt stmt) (ldm-stmt stmt-equiv))) :rule-classes :congruence)
Theorem:
(defthm ldm-block-item-block-item-equiv-congruence-on-item (implies (block-item-equiv item item-equiv) (equal (ldm-block-item item) (ldm-block-item item-equiv))) :rule-classes :congruence)
Theorem:
(defthm ldm-block-item-list-block-item-list-equiv-congruence-on-items (implies (block-item-list-equiv items items-equiv) (equal (ldm-block-item-list items) (ldm-block-item-list items-equiv))) :rule-classes :congruence)