Map a direct declarator to a function declarator in the language definition.
(ldm-dirdeclor-fun dirdeclor) → (mv erp fundeclor)
The abstract syntax in the language definition does not have a separate type for direct function declarators, so we return a function declarator here. The input direct declarator must be an identifier followed by a single parenthesized list of parameter declarations.
This function will always result in a c::fun-declor
of the
This function is called when we expect a function declarator, not an object declarator, for which we have a separate function.
Function:
(defun ldm-dirdeclor-fun (dirdeclor) (declare (xargs :guard (dirdeclorp dirdeclor))) (let ((__function__ 'ldm-dirdeclor-fun)) (declare (ignorable __function__)) (b* (((reterr) (c::fun-declor-base (c::ident "irrelevant") nil)) ((unless (dirdeclor-case dirdeclor :function-params)) (reterr (msg "Unsupported direct declarator ~x0 for function." (dirdeclor-fix dirdeclor)))) (inner-dirdeclor (dirdeclor-function-params->decl dirdeclor)) (params (dirdeclor-function-params->params dirdeclor)) ((unless (dirdeclor-case inner-dirdeclor :ident)) (reterr (msg "Unsupported direct declarator ~x0 for function." (dirdeclor-fix dirdeclor)))) (ident (dirdeclor-ident->unwrap inner-dirdeclor)) ((erp ident1) (ldm-ident ident)) ((erp params1) (ldm-paramdecl-list params))) (retok (c::make-fun-declor-base :name ident1 :params params1)))))
Theorem:
(defthm fun-declorp-of-ldm-dirdeclor-fun.fundeclor (b* (((mv acl2::?erp ?fundeclor) (ldm-dirdeclor-fun dirdeclor))) (c::fun-declorp fundeclor)) :rule-classes :rewrite)
Theorem:
(defthm ldm-dirdeclor-fun-of-dirdeclor-fix-dirdeclor (equal (ldm-dirdeclor-fun (dirdeclor-fix dirdeclor)) (ldm-dirdeclor-fun dirdeclor)))
Theorem:
(defthm ldm-dirdeclor-fun-dirdeclor-equiv-congruence-on-dirdeclor (implies (dirdeclor-equiv dirdeclor dirdeclor-equiv) (equal (ldm-dirdeclor-fun dirdeclor) (ldm-dirdeclor-fun dirdeclor-equiv))) :rule-classes :congruence)