		Search-engine friendly clone of the ACL2 documentation.

Mapping-to-language-definition

Ldm-param-declor

Map a parameter declarator to an object declarator in the language definition.

Signature
(ldm-param-declor paramdeclor) → (mv erp objdeclor)
Arguments: paramdeclor — Guard (param-declorp paramdeclor).
Returns: objdeclor — Type (c::obj-declorp objdeclor).

The parameter declarator must be present and not abstract. The declarator must be for an object, which we map to an object declarator.

Definitions and Theorems

Function: ldm-param-declor

(defun ldm-param-declor (paramdeclor)
 (declare (xargs :guard (param-declorp paramdeclor)))
 (declare (xargs :guard (param-declor-unambp paramdeclor)))
 (let ((__function__ 'ldm-param-declor))
  (declare (ignorable __function__))
  (b*
   (((reterr)
     (c::obj-declor-ident (c::ident "irrelevant")))
    ((when (param-declor-case paramdeclor :abstract))
     (reterr
      (msg
       "Unsupported parameter declarator ~x0 ~
                      with abstract declarator."
       (param-declor-fix paramdeclor))))
    ((when (param-declor-case paramdeclor :none))
     (reterr (msg "Unsupported absent parameter declarator ~x0.")))
    ((when (param-declor-case paramdeclor :ambig))
     (prog2$ (impossible) (reterr t)))
    (declor (param-declor-nonabstract->declor paramdeclor)))
   (ldm-declor-obj declor))))

Theorem: obj-declorp-of-ldm-param-declor.objdeclor

(defthm obj-declorp-of-ldm-param-declor.objdeclor
  (b* (((mv acl2::?erp ?objdeclor)
        (ldm-param-declor paramdeclor)))
    (c::obj-declorp objdeclor))
  :rule-classes :rewrite)

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

(defthm ldm-param-declor-ok-when-param-declor-formalp
  (implies (param-declor-formalp paramdeclor)
           (b* (((mv acl2::?erp ?objdeclor)
                 (ldm-param-declor paramdeclor)))
             (not erp))))

Theorem: ldm-param-declor-of-param-declor-fix-paramdeclor

(defthm ldm-param-declor-of-param-declor-fix-paramdeclor
  (equal (ldm-param-declor (param-declor-fix paramdeclor))
         (ldm-param-declor paramdeclor)))

Theorem: ldm-param-declor-param-declor-equiv-congruence-on-paramdeclor

(defthm
      ldm-param-declor-param-declor-equiv-congruence-on-paramdeclor
  (implies (param-declor-equiv paramdeclor paramdeclor-equiv)
           (equal (ldm-param-declor paramdeclor)
                  (ldm-param-declor paramdeclor-equiv)))
  :rule-classes :congruence)