		Search-engine friendly clone of the ACL2 documentation.

Mapping-to-language-definition

Ldm-declor-fun

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

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

We map the direct declarator to a function declarator, and then we recursively add pointer layers based on the pointer part of the declarator.

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-declor-fun-loop

(defun ldm-declor-fun-loop (declor1 pointers)
 (declare
     (xargs :guard (and (c::fun-declorp declor1)
                        (typequal/attribspec-list-listp pointers))))
 (let ((__function__ 'ldm-declor-fun-loop))
   (declare (ignorable __function__))
   (b* (((reterr)
         (c::fun-declor-base (c::ident "irrelevant")
                             nil))
        ((when (endp pointers))
         (retok (c::fun-declor-fix declor1)))
        (qualspecs (car pointers))
        ((unless (endp qualspecs))
         (reterr (msg "Unsupported type qualifiers ~x0 in pointer."
                      (typequal/attribspec-list-fix qualspecs))))
        ((erp declor2)
         (ldm-declor-fun-loop declor1 (cdr pointers))))
     (retok (c::fun-declor-pointer declor2)))))

Theorem: fun-declorp-of-ldm-declor-fun-loop.declor2

(defthm fun-declorp-of-ldm-declor-fun-loop.declor2
  (b* (((mv acl2::?erp ?declor2)
        (ldm-declor-fun-loop declor1 pointers)))
    (c::fun-declorp declor2))
  :rule-classes :rewrite)

Theorem: ldm-declor-fun-loop-ok-when-pointers-formalp

(defthm ldm-declor-fun-loop-ok-when-pointers-formalp
  (implies (pointers-formalp pointers)
           (b* (((mv acl2::?erp ?declor2)
                 (ldm-declor-fun-loop declor1 pointers)))
             (not erp))))

Theorem: ldm-declor-fun-loop-of-fun-declor-fix-declor1

(defthm ldm-declor-fun-loop-of-fun-declor-fix-declor1
  (equal (ldm-declor-fun-loop (c::fun-declor-fix declor1)
                              pointers)
         (ldm-declor-fun-loop declor1 pointers)))

Theorem: ldm-declor-fun-loop-fun-declor-equiv-congruence-on-declor1

(defthm ldm-declor-fun-loop-fun-declor-equiv-congruence-on-declor1
  (implies (c::fun-declor-equiv declor1 declor1-equiv)
           (equal (ldm-declor-fun-loop declor1 pointers)
                  (ldm-declor-fun-loop declor1-equiv pointers)))
  :rule-classes :congruence)

Theorem: ldm-declor-fun-loop-of-typequal/attribspec-list-list-fix-pointers

(defthm
  ldm-declor-fun-loop-of-typequal/attribspec-list-list-fix-pointers
 (equal
  (ldm-declor-fun-loop declor1
                       (typequal/attribspec-list-list-fix pointers))
  (ldm-declor-fun-loop declor1 pointers)))

Theorem: ldm-declor-fun-loop-typequal/attribspec-list-list-equiv-congruence-on-pointers

(defthm
 ldm-declor-fun-loop-typequal/attribspec-list-list-equiv-congruence-on-pointers
 (implies
      (typequal/attribspec-list-list-equiv pointers pointers-equiv)
      (equal (ldm-declor-fun-loop declor1 pointers)
             (ldm-declor-fun-loop declor1 pointers-equiv)))
 :rule-classes :congruence)

Function: ldm-declor-fun

(defun ldm-declor-fun (declor)
  (declare (xargs :guard (declorp declor)))
  (declare (xargs :guard (declor-unambp declor)))
  (let ((__function__ 'ldm-declor-fun))
    (declare (ignorable __function__))
    (b* (((reterr)
          (c::fun-declor-base (c::ident "irrelevant")
                              nil))
         ((declor declor) declor)
         ((erp declor1)
          (ldm-dirdeclor-fun declor.direct)))
      (ldm-declor-fun-loop declor1 declor.pointers))))

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

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

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

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

Theorem: ldm-declor-fun-of-declor-fix-declor

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

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

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