		Search-engine friendly clone of the ACL2 documentation.

Mapping-to-language-definition

Ldm-declors/dirdeclors-obj

Map declarators and direct declarators to object declarators and direct declarators in the language definition.

Definitions and Theorems

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))))

Function: ldm-dirdeclor-obj

(defun ldm-dirdeclor-obj (dirdeclor)
 (declare (xargs :guard (dirdeclorp dirdeclor)))
 (declare (xargs :guard (dirdeclor-unambp dirdeclor)))
 (let ((__function__ 'ldm-dirdeclor-obj))
  (declare (ignorable __function__))
  (b*
   (((reterr)
     (c::obj-declor-ident (c::ident "irrelevant")))
    ((when (dirdeclor-case dirdeclor :ident))
     (b* ((ident (dirdeclor-ident->ident dirdeclor))
          ((erp ident1) (ldm-ident ident)))
       (retok (c::obj-declor-ident ident1))))
    ((when (dirdeclor-case dirdeclor :array))
     (b*
      (((dirdeclor-array dirdeclor) dirdeclor)
       ((erp declor1)
        (ldm-dirdeclor-obj dirdeclor.declor))
       ((when dirdeclor.qualspecs)
        (reterr
         (msg
          "Unsupported type qualifiers ~
                              or attribute specifiers ~
                              in direct declarator ~x0 for object."
          (dirdeclor-fix dirdeclor))))
       ((when (not dirdeclor.size?))
        (retok (c::make-obj-declor-array :decl declor1
                                         :size nil)))
       (iconst (check-expr-iconst dirdeclor.size?))
       ((unless iconst)
        (reterr
         (msg
          "Unsupported non-integer-constant size ~
                              in direct declarator ~x0 for object."
          (dirdeclor-fix dirdeclor))))
       (iconst1 (ldm-iconst iconst)))
      (retok (c::make-obj-declor-array :decl declor1
                                       :size iconst1)))))
   (reterr (msg "Unsupported direct declarator ~x0 for object."
                (dirdeclor-fix dirdeclor))))))

Theorem: return-type-of-ldm-declor-obj.declor1

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

Theorem: return-type-of-ldm-dirdeclor-obj.declor1

(defthm return-type-of-ldm-dirdeclor-obj.declor1
  (b* (((mv acl2::?erp ?declor1)
        (ldm-dirdeclor-obj dirdeclor)))
    (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-dirdeclor-obj-ok-when-dirdeclor-obj-formalp

(defthm ldm-dirdeclor-obj-ok-when-dirdeclor-obj-formalp
  (implies (dirdeclor-obj-formalp dirdeclor)
           (b* (((mv acl2::?erp ?declor1)
                 (ldm-dirdeclor-obj dirdeclor)))
             (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-dirdeclor-obj-ok-when-dirdeclor-block-formalp

(defthm ldm-dirdeclor-obj-ok-when-dirdeclor-block-formalp
  (implies (dirdeclor-block-formalp dirdeclor)
           (b* (((mv acl2::?erp ?declor1)
                 (ldm-dirdeclor-obj dirdeclor)))
             (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-dirdeclor-obj-of-dirdeclor-fix-dirdeclor

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

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)

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

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

Subtopics

Ldm-dirdeclor-obj: Map a direct declarator to an object declarator in the language definition.
Ldm-declor-obj: Map a declarator to an object declarator in the language definition.