		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Fun-adeclor-to-params+declor

Decompose an abstract function declarator into a list of parameter declarations and an abstract object declarator.

Signature
(fun-adeclor-to-params+declor declor) → (mv params declor)
Arguments: declor — Guard (fun-adeclorp declor).
Returns: params — Type (param-declon-listp params).; declor — Type (obj-adeclorp declor).

The inverse of this is not well-defined for every abstract object declarator, because the latter may include array declarators, which are not allowed in function declarators. We could define the inverse on object declarators that are restricted not to use array declarators; but we do not need the inverse for now.

Definitions and Theorems

Function: fun-adeclor-to-params+declor

(defun fun-adeclor-to-params+declor (declor)
  (declare (xargs :guard (fun-adeclorp declor)))
  (fun-adeclor-case
       declor :base
       (mv declor.params (obj-adeclor-none))
       :pointer
       (b* (((mv params sub)
             (fun-adeclor-to-params+declor declor.decl)))
         (mv params
             (make-obj-adeclor-pointer :decl sub)))))

Theorem: param-declon-listp-of-fun-adeclor-to-params+declor.params

(defthm param-declon-listp-of-fun-adeclor-to-params+declor.params
  (b* (((mv ?params ?declor)
        (fun-adeclor-to-params+declor declor)))
    (param-declon-listp params))
  :rule-classes :rewrite)

Theorem: obj-adeclorp-of-fun-adeclor-to-params+declor.declor

(defthm obj-adeclorp-of-fun-adeclor-to-params+declor.declor
  (b* (((mv ?params ?declor)
        (fun-adeclor-to-params+declor declor)))
    (obj-adeclorp declor))
  :rule-classes :rewrite)

Theorem: fun-adeclor-to-params+declor-of-fun-adeclor-fix-declor

(defthm fun-adeclor-to-params+declor-of-fun-adeclor-fix-declor
  (equal (fun-adeclor-to-params+declor (fun-adeclor-fix declor))
         (fun-adeclor-to-params+declor declor)))

Theorem: fun-adeclor-to-params+declor-fun-adeclor-equiv-congruence-on-declor

(defthm
 fun-adeclor-to-params+declor-fun-adeclor-equiv-congruence-on-declor
 (implies (fun-adeclor-equiv declor declor-equiv)
          (equal (fun-adeclor-to-params+declor declor)
                 (fun-adeclor-to-params+declor declor-equiv)))
 :rule-classes :congruence)