|
|
|---|
|
|
|
|---|
FTY utilities for pseudo-terms.
Many system utilities, e.g. built-in and in Std/system, are written using the built-in ACL2 term API. When using these system utilities in code that uses the FTY term API, there may be a slight ``mismatch'', e.g. in the way the two APIs fix non-terms, or in the fact that, for termination, the ACL2 API is based on ACL2-count while the FTY API is based on pseudo-term-count.
The mismatch can be bridged by introducing simple wrappers of those system utilities that fix the term (in the FTY way) and then call the utilities. Here we provide a number of such wrappers, which should be eventually moved to a more central place.
The wrappers are accompanied by theorems leveraged from the wrapped utilities. This way the wrappers can be left disabled in code that uses them.
The ACL2-count vs. pseudo-term-count issue requires a bit more work. Suppose we have a utility that returns results that are ACL2-count-smaller than its arguments (under suitable conditions). In order to prove that the wrapper returns results that are pseudo-term-count-smaller than its arguments, we cannot leverage the theorems about ACL2-count. Instead, we need to enable the utilities to prove the theorems, and we also need to enable some FTY pseudo-term operations, because we need to break the FTY pseudo-term abstraction: we use this approach to prove theorems about the original utilities and pseudo-term-count under pseudo-termp assumptions, from which then the desired theorems about the wrappers readily follow. The theorems about the original utilities and pseudo-term-count are useful to prove the analogous theorems of utilities that call them.