		Search-engine friendly clone of the ACL2 documentation.

Mapping-to-language-definition

Ldm-dirdeclor-fun

Map a direct declarator to a function declarator in the language definition.

Signature
(ldm-dirdeclor-fun dirdeclor) → (mv erp fundeclor)
Arguments: dirdeclor — Guard (dirdeclorp dirdeclor).
Returns: fundeclor — Type (c::fun-declorp fundeclor).

The abstract syntax in the language definition does not have a separate type for direct function declarators, so we return a function declarator here. The input direct declarator must be an identifier followed by a single parenthesized list of parameter declarations, or an empty list of parameter names.

This function will always result in a c::fun-declor of the :base kind; the :pointer kind is generated by ldm-declor-fun.

This function is called when we expect a function declarator, not an object declarator, for which we have a separate function.

Definitions and Theorems

Function: ldm-dirdeclor-fun

(defun ldm-dirdeclor-fun (dirdeclor)
 (declare (xargs :guard (dirdeclorp dirdeclor)))
 (declare (xargs :guard (dirdeclor-unambp dirdeclor)))
 (let ((__function__ 'ldm-dirdeclor-fun))
  (declare (ignorable __function__))
  (b*
   (((reterr)
     (c::fun-declor-base (c::ident "irrelevant")
                         nil))
    ((unless
      (or (dirdeclor-case dirdeclor :function-params)
          (and (dirdeclor-case dirdeclor :function-names)
               (endp (dirdeclor-function-names->names dirdeclor)))))
     (reterr (msg "Unsupported direct declarator ~x0 for function."
                  (dirdeclor-fix dirdeclor))))
    ((mv inner-dirdeclor params)
     (if (dirdeclor-case dirdeclor :function-params)
         (mv (dirdeclor-function-params->declor dirdeclor)
             (dirdeclor-function-params->params dirdeclor))
       (mv (dirdeclor-function-names->declor dirdeclor)
           nil)))
    ((unless (dirdeclor-case inner-dirdeclor :ident))
     (reterr (msg "Unsupported direct declarator ~x0 for function."
                  (dirdeclor-fix dirdeclor))))
    (ident (dirdeclor-ident->ident inner-dirdeclor))
    ((erp ident1) (ldm-ident ident))
    ((erp params1)
     (ldm-param-declon-list params)))
   (retok (c::make-fun-declor-base :name ident1
                                   :params params1)))))

Theorem: fun-declorp-of-ldm-dirdeclor-fun.fundeclor

(defthm fun-declorp-of-ldm-dirdeclor-fun.fundeclor
  (b* (((mv acl2::?erp ?fundeclor)
        (ldm-dirdeclor-fun dirdeclor)))
    (c::fun-declorp fundeclor))
  :rule-classes :rewrite)

Theorem: ldm-dirdeclor-fun-ok-when-dirdeclor-fun-formalp

(defthm ldm-dirdeclor-fun-ok-when-dirdeclor-fun-formalp
  (implies (dirdeclor-fun-formalp dirdeclor)
           (b* (((mv acl2::?erp ?fundeclor)
                 (ldm-dirdeclor-fun dirdeclor)))
             (not erp))))

Theorem: ldm-dirdeclor-fun-of-dirdeclor-fix-dirdeclor

(defthm ldm-dirdeclor-fun-of-dirdeclor-fix-dirdeclor
  (equal (ldm-dirdeclor-fun (dirdeclor-fix dirdeclor))
         (ldm-dirdeclor-fun dirdeclor)))

Theorem: ldm-dirdeclor-fun-dirdeclor-equiv-congruence-on-dirdeclor

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