		Search-engine friendly clone of the ACL2 documentation.

Mapping-to-language-definition

Ldm-extdecl

Map an external declaration to an external declaration in the language definition.

Signature
(ldm-extdecl extdecl) → (mv erp extdecl1)
Arguments: extdecl — Guard (extdeclp extdecl).
Returns: extdecl1 — Type (c::ext-declonp 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.

Definitions and Theorems

Function: ldm-extdecl

(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 :empty))
     (reterr (msg "Unsupported empty external declaration.")))
    ((when (extdecl-case extdecl :asm))
     (reterr
         (msg "Unsupported assembler statement at the top level.")))
    ((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: ext-declonp-of-ldm-extdecl.extdecl1

(defthm ext-declonp-of-ldm-extdecl.extdecl1
  (b* (((mv acl2::?erp ?extdecl1)
        (ldm-extdecl extdecl)))
    (c::ext-declonp extdecl1))
  :rule-classes :rewrite)

Theorem: ldm-extdecl-of-extdecl-fix-extdecl

(defthm ldm-extdecl-of-extdecl-fix-extdecl
  (equal (ldm-extdecl (extdecl-fix extdecl))
         (ldm-extdecl extdecl)))

Theorem: ldm-extdecl-extdecl-equiv-congruence-on-extdecl

(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)