Map an external declaration to an external declaration in the language definition.
(ldm-extdecl extdecl) → (mv erp extdecl1)
Besides supporting function definitions, we support three kinds of declarations: for functions, for objects, and for tags. We try these three mapping functions in turn, but instead of just propagating the errors they may return, we catch them and use them to try the next mapping.
Function:
(defun ldm-extdecl (extdecl) (declare (xargs :guard (extdeclp extdecl))) (declare (xargs :guard (extdecl-unambp extdecl))) (let ((__function__ 'ldm-extdecl)) (declare (ignorable __function__)) (b* (((reterr) (c::ext-declon-fundef (c::fundef (c::tyspecseq-void) (c::fun-declor-base (c::ident "irrelevant") nil) nil))) ((when (extdecl-case extdecl :fundef)) (b* (((erp fundef) (ldm-fundef (extdecl-fundef->unwrap extdecl)))) (retok (c::ext-declon-fundef fundef)))) (decl (extdecl-decl->unwrap extdecl)) ((mv erp fundeclon) (ldm-decl-fun decl)) ((when (not erp)) (retok (c::ext-declon-fun-declon fundeclon))) ((mv erp objdeclon) (ldm-decl-obj decl)) ((when (not erp)) (retok (c::ext-declon-obj-declon objdeclon))) ((mv erp tagdeclon) (ldm-decl-tag decl)) ((when (not erp)) (retok (c::ext-declon-tag-declon tagdeclon)))) (reterr (msg "Unsupported external declaration ~x0." (extdecl-fix extdecl))))))
Theorem:
(defthm ext-declonp-of-ldm-extdecl.extdecl1 (b* (((mv acl2::?erp ?extdecl1) (ldm-extdecl extdecl))) (c::ext-declonp extdecl1)) :rule-classes :rewrite)
Theorem:
(defthm ldm-extdecl-of-extdecl-fix-extdecl (equal (ldm-extdecl (extdecl-fix extdecl)) (ldm-extdecl extdecl)))
Theorem:
(defthm ldm-extdecl-extdecl-equiv-congruence-on-extdecl (implies (extdecl-equiv extdecl extdecl-equiv) (equal (ldm-extdecl extdecl) (ldm-extdecl extdecl-equiv))) :rule-classes :congruence)