Ex-args
Argument list for function expand
This is a product type introduced by defprod.
Fields
- term-lst — pseudo-term-list
- List of terms to be expanded. The function
finishes when all of them are expanded to given level.
- fn-lst — func-alist
- List of function definitions to use for
function expansion.
- fn-lvls — sym-nat-alist
- Levels to expand each functions to.
- wrld-fn-len — natp
- Number of function definitions in curent world.
- expand-lst — pseudo-term-alist
- An alist of expanded function symbols
associated with their function call
Ex-args stores the list of arguments passed into the
function expand. We design this product type so that we don't have a
long list of arguments to write down every time there's a recursive call.
This document describes what each argument is about and more specifically,
why they exist necessarily. This document comes out because every time when
I read the expand function, I get confused and lost track about why I
designed such a argument in the first place.
Term-lst is easy, it stores the list of terms to be expanded.
Recursively generated new terms are stored in this argument and gets used
in recursive calls. Using a list of terms allows us to use a single
recursive function instead of mutual-recursion, even though every
time we call this function, we really just have one term to expand.
Fn-lst stores a list of function definitions for use of expansion.
This list comes from the smtlink-hint stored in function stub smt-hint. Such a list initially comes from user inputs to Smtlink.
So it can be, for example, some functions that the user wants to get
expanded specially.
Fn-lvls stores a list of maximum number of times each function
needs to be expanded. This list doesn't take into account of functions that
are not specified by the user, which should oftenly be the case. In that
case, those functions will be expanded just once and a pair will be stored
into fn-lvls indicating this function has already been expanded. This
is done by storing a level of 0 for such a function.
Wrld-fn-len is the hardest to explain. But given some thought, I
found it to be necessary to have this argument. wrld-fn-len represents
the length of current ACL2 world, meaning the number of definitions
in total (might be more than that, I'm not completely sure about what the
world is composed of). This argument helps prove termination of
function expand. See expand-measure for a discussion about
the measure function for proving termimation.
Expand-lst stores all functions that are expanded in expand.
This list gets used later for generating the :in-theory hint for
proving that the expanded term implies the original unexpanded term.
Subtopics
- Ex-args-fix
- Fixing function for ex-args structures.
- Make-ex-args
- Basic constructor macro for ex-args structures.
- Ex-args-equiv
- Basic equivalence relation for ex-args structures.
- Ex-args->expand-lst
- Get the expand-lst field from a ex-args.
- Change-ex-args
- Modifying constructor for ex-args structures.
- Ex-args->wrld-fn-len
- Get the wrld-fn-len field from a ex-args.
- Ex-args->term-lst
- Get the term-lst field from a ex-args.
- Ex-args->fn-lvls
- Get the fn-lvls field from a ex-args.
- Ex-args->fn-lst
- Get the fn-lst field from a ex-args.
- Ex-args-p
- Recognizer for ex-args structures.
