		Search-engine friendly clone of the ACL2 documentation.

Mapping-to-language-definition

Ldm-ext-declon

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

Signature
(ldm-ext-declon extdecl) → (mv erp extdecl1)
Arguments: extdecl — Guard (ext-declonp 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-ext-declon

(defun ldm-ext-declon (extdecl)
 (declare (xargs :guard (ext-declonp extdecl)))
 (declare (xargs :guard (ext-declon-unambp extdecl)))
 (let ((__function__ 'ldm-ext-declon))
  (declare (ignorable __function__))
  (b*
   (((reterr)
     (c::ext-declon-fundef
          (c::fundef (c::tyspecseq-void)
                     (c::fun-declor-base (c::ident "irrelevant")
                                         nil)
                     nil)))
    ((when (ext-declon-case extdecl :empty))
     (reterr (msg "Unsupported empty external declaration.")))
    ((when (ext-declon-case extdecl :asm))
     (reterr
         (msg "Unsupported assembler statement at the top level.")))
    ((when (ext-declon-case extdecl :fundef))
     (b* (((erp fundef)
           (ldm-fundef (ext-declon-fundef->fundef extdecl))))
       (retok (c::ext-declon-fundef fundef))))
    (decl (ext-declon-declon->declon extdecl))
    ((mv erp fundeclon)
     (ldm-declon-fun decl))
    ((when (not erp))
     (retok (c::ext-declon-fun-declon fundeclon)))
    ((mv erp objdeclon)
     (ldm-declon-obj decl))
    ((when (not erp))
     (retok (c::ext-declon-obj-declon objdeclon)))
    ((mv erp tagdeclon)
     (ldm-declon-tag decl))
    ((when (not erp))
     (retok (c::ext-declon-tag-declon tagdeclon))))
   (reterr (msg "Unsupported external declaration ~x0."
                (ext-declon-fix extdecl))))))

Theorem: ext-declonp-of-ldm-ext-declon.extdecl1

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

Theorem: ldm-ext-declon-ok-when-ext-declon-formalp

(defthm ldm-ext-declon-ok-when-ext-declon-formalp
  (implies (ext-declon-formalp extdecl)
           (b* (((mv acl2::?erp ?extdecl1)
                 (ldm-ext-declon extdecl)))
             (not erp))))

Theorem: ldm-ext-declon-of-ext-declon-fix-extdecl

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

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

(defthm ldm-ext-declon-ext-declon-equiv-congruence-on-extdecl
  (implies (ext-declon-equiv extdecl extdecl-equiv)
           (equal (ldm-ext-declon extdecl)
                  (ldm-ext-declon extdecl-equiv)))
  :rule-classes :congruence)