		Search-engine friendly clone of the ACL2 documentation.

Mapping-to-language-definition

Ldm-declor-obj

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

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

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

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

Definitions and Theorems

Function: ldm-declor-obj-loop

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

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

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

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

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

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

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

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

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

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

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

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

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

Function: ldm-declor-obj

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

Theorem: obj-declorp-of-ldm-declor-obj.declor1

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

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

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

Theorem: ldm-declor-obj-ok-when-declor-block-formalp

(defthm ldm-declor-obj-ok-when-declor-block-formalp
  (implies (declor-block-formalp declor)
           (b* (((mv acl2::?erp ?declor1)
                 (ldm-declor-obj declor)))
             (not erp))))

Theorem: ldm-declor-obj-of-declor-fix-declor

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

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

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