		Search-engine friendly clone of the ACL2 documentation.

Mapping-to-language-definition

Ldm-param-declon

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

Signature
(ldm-param-declon paramdecl) → (mv erp paramdecl1)
Arguments: paramdecl — Guard (param-declonp 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.

There must be no ending attribute specifiers.

Definitions and Theorems

Function: ldm-param-declon

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

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

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

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

(defthm ldm-param-declon-ok-when-param-declon-formalp
  (implies (param-declon-formalp paramdecl)
           (b* (((mv acl2::?erp ?paramdecl1)
                 (ldm-param-declon paramdecl)))
             (not erp))))

Theorem: ldm-param-declon-of-param-declon-fix-paramdecl

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

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

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