		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Dirdeclor-obj-formalp

Check if a direct declarator has formal dynamic semantics, as part of an object declaration (not in a block).

Signature
(dirdeclor-obj-formalp dirdeclor) → yes/no
Arguments: dirdeclor — Guard (dirdeclorp dirdeclor).
Returns: yes/no — Type (booleanp yes/no).

This is for direct declarators not used as part of block items; for those, we have dirdeclor-block-formalp instead.

For all other uses of direct declarators (not as part of block items), we allow identifier declarators and array declarators, the latter without size or with an integer constant as size; also see ldm-dirdeclor-obj.

Definitions and Theorems

Function: dirdeclor-obj-formalp

(defun dirdeclor-obj-formalp (dirdeclor)
  (declare (xargs :guard (dirdeclorp dirdeclor)))
  (declare (xargs :guard (dirdeclor-unambp dirdeclor)))
  (let ((__function__ 'dirdeclor-obj-formalp))
    (declare (ignorable __function__))
    (dirdeclor-case
         dirdeclor
         :ident (ident-formalp dirdeclor.unwrap)
         :paren nil
         :array (and (dirdeclor-obj-formalp dirdeclor.decl)
                     (endp dirdeclor.tyquals)
                     (or (not dirdeclor.expr?)
                         (and (check-expr-iconst dirdeclor.expr?)
                              t)))
         :array-static1 nil
         :array-static2 nil
         :array-star nil
         :function-params nil
         :function-names nil)))

Theorem: booleanp-of-dirdeclor-obj-formalp

(defthm booleanp-of-dirdeclor-obj-formalp
  (b* ((yes/no (dirdeclor-obj-formalp dirdeclor)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: dirdeclor-obj-formalp-of-dirdeclor-fix-dirdeclor

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

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

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