		Search-engine friendly clone of the ACL2 documentation.

Mapping-to-language-definition

Ldm-paramdecl

Map a parameter declaration to a parameter declaration in the language definition.

Signature
(ldm-paramdecl paramdecl) → (mv erp paramdecl1)
Arguments: paramdecl — Guard (paramdeclp paramdecl).
Returns: paramdecl1 — Type (c::param-declonp paramdecl1).

The declaration specifiers must be all type specifiers, and must form a supported type specifier sequence.

The parameter declarator must map to an object declarator.

Definitions and Theorems

Function: ldm-paramdecl

(defun ldm-paramdecl (paramdecl)
 (declare (xargs :guard (paramdeclp paramdecl)))
 (declare (xargs :guard (paramdecl-unambp paramdecl)))
 (let ((__function__ 'ldm-paramdecl))
  (declare (ignorable __function__))
  (b*
   (((reterr)
     (c::param-declon
          (c::tyspecseq-void)
          (c::obj-declor-ident (c::ident "irrelevant"))))
    (declspecs (paramdecl->spec paramdecl))
    (declor (paramdecl->decl paramdecl))
    ((mv okp tyspecs)
     (check-decl-spec-list-all-typespec declspecs))
    ((unless okp)
     (reterr
      (msg
       "Unsupported declaration specifier list ~
                      in parameter declaration ~x0."
       (paramdecl-fix paramdecl))))
    ((erp tyspecseq)
     (ldm-type-spec-list tyspecs))
    ((erp objdeclor)
     (ldm-paramdeclor declor)))
   (retok (c::make-param-declon :tyspec tyspecseq
                                :declor objdeclor)))))

Theorem: param-declonp-of-ldm-paramdecl.paramdecl1

(defthm param-declonp-of-ldm-paramdecl.paramdecl1
  (b* (((mv acl2::?erp ?paramdecl1)
        (ldm-paramdecl paramdecl)))
    (c::param-declonp paramdecl1))
  :rule-classes :rewrite)

Theorem: ldm-paramdecl-of-paramdecl-fix-paramdecl

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

Theorem: ldm-paramdecl-paramdecl-equiv-congruence-on-paramdecl

(defthm ldm-paramdecl-paramdecl-equiv-congruence-on-paramdecl
  (implies (paramdecl-equiv paramdecl paramdecl-equiv)
           (equal (ldm-paramdecl paramdecl)
                  (ldm-paramdecl paramdecl-equiv)))
  :rule-classes :congruence)