Atc-fn-info
Fixtype of information associated to
an ACL2 function translated to a C function or loop.
This is a product type introduced by fty::defprod.
Fields
- out-type — type-option
- in-types — type-list
- loop? — stmt-option
- affect — symbol-list
- extobjs — symbol-list
- result-thm — symbolp
- correct-thm — symbolp
- correct-mod-thm — symbolp
- measure-nat-thm — symbolp
- fun-env-thm — symbolp
- limit — pseudo-term
- guard — symbolp
This consists of:
an optional C type that is present,
and represents the function's output type,
when the function is not recursive;
a list of C types representing the function's input types;
an optional (loop) statement that is present,
and is represented by the function,
when the function is recursive;
a list of variables affected by the function;
a list of formals that represent external objects;
the name of the locally generated theorem about the function result(s);
the name of the locally generated theorem that asserts
that the execution of the function is functionally correct,
proved using the monolithic symbolic execution;
the name of the locally generated theorem that asserts
that the execution of the function is functionally correct,
proved using the modular proof generation approach;
the name of the locally generated theorem that asserts
that the measure of the function (when recursive) yields a natural number
(nil if the function is not recursive);
the name of the locally generated theorem that asserts
that looking up the function in the function environment
yields the information for the function
(nil if the function is recursive);
a limit that suffices to execute the code generated from the function,
as explained below;
and the locally generated function for the guard of the function.
The limit is a term that may depend on the function's parameters.
For a non-recursive function,
the term expresses a limit that suffices to execute exec-fun
on the C function generated from the ACL2 function
when the arguments of the C functions have values
symbolically expressed by the ACL2 function's formal parameters.
For a recursive function,
the term expressed a limit that suffices to execute exec-stmt-while
on the C loop generated from the ACL2 function
when the variables read by the C loop have values
symbolically expressed by the ACL2 function's formal parameters.
If none of the target ACL2 functions are recursive,
all the limit terms are quoted constants;
if there are recursive functions,
then those, and all their direct and indirect callers,
have limit terms that in general depend on each function's parameters.
All these limit terms are calculated
when the C code is generated from the ACL2 functions.
Note that exactly one of the first two fields is nil.
This is an invariant.
Subtopics
- Atc-fn-info-fix
- Fixing function for atc-fn-info structures.
- Make-atc-fn-info
- Basic constructor macro for atc-fn-info structures.
- Atc-fn-infop
- Recognizer for atc-fn-info structures.
- Atc-fn-info-equiv
- Basic equivalence relation for atc-fn-info structures.
- Change-atc-fn-info
- Modifying constructor for atc-fn-info structures.
- Atc-fn-info->measure-nat-thm
- Get the measure-nat-thm field from a atc-fn-info.
- Atc-fn-info->correct-mod-thm
- Get the correct-mod-thm field from a atc-fn-info.
- Atc-fn-info->result-thm
- Get the result-thm field from a atc-fn-info.
- Atc-fn-info->out-type
- Get the out-type field from a atc-fn-info.
- Atc-fn-info->in-types
- Get the in-types field from a atc-fn-info.
- Atc-fn-info->fun-env-thm
- Get the fun-env-thm field from a atc-fn-info.
- Atc-fn-info->extobjs
- Get the extobjs field from a atc-fn-info.
- Atc-fn-info->correct-thm
- Get the correct-thm field from a atc-fn-info.
- Atc-fn-info->loop?
- Get the loop? field from a atc-fn-info.
- Atc-fn-info->limit
- Get the limit field from a atc-fn-info.
- Atc-fn-info->guard
- Get the guard field from a atc-fn-info.
- Atc-fn-info->affect
- Get the affect field from a atc-fn-info.
