Simpadd0-dirdeclor
Transform a direct declarator.
- Signature
(simpadd0-dirdeclor dirdeclor fundefp gin)
→
(mv new-dirdeclor new-fundefp gout)
- Arguments
- dirdeclor — Guard (dirdeclorp dirdeclor).
- fundefp — Guard (booleanp fundefp).
- gin — Guard (ginp gin).
- Returns
- new-dirdeclor — Type (dirdeclorp new-dirdeclor).
- new-fundefp — Type (booleanp new-fundefp).
- gout — Type (goutp gout).
The fundefp flag is set iff
the direct declarator is (part of) the one of a function definition
whose parameters have not been transformed yet;
this function is only called by simpadd0-declor
(see how the callers of simpadd0-declor set fundefp),
and recursively by itself.
The fundefp flag is just threaded through most recursively calls.
For the :function-params kind of direct declarator,
if fundefp is t,
then the variable-type map resulting from
transforming the parameter declarations
is return as part of the gout of this ACL2 function,
so that the extended map is available for the function's body.
Additionally, in this case the fundefp result is nil,
because the parameters of the function definition have been
transformed and the variable-type map has been extended for the body.
If instead the input fundefp is nil,
the variable-type map resulting from the parameters
is discarded and not returned as part of the gout.
In the :function-names case,
there is no extension of the variable-type map,
but we set the fundefp output to nil.
