Add base case option to isodata :undefined parameter

[gjurgensen]

This adds :base-case and :base-case-then as options to isodata's :undefined parameter. When either of these options are provided, isodata will choose the undefined value by looking for a base case within the newly generated function. A base case of a term may either be the whole term when the term does not include a recursive call, or if the term is an if, then it may be a base case of the then or else branch. A term may have several base cases; the :base-case option is biased toward selecting base cases in else branches, while :base-case-then is biased toward then branches.

The motivation for this feature is that a base-case will likely have a desirable type, and the result may be amenable to combining nested ifs.

[acoglio]

Can these three theorems be made local, so they do not affect the books that they include this tool directly or indirectly?

[acoglio]

I would make the two options more symmetric, i.e. :base-case-then and :base-case-else, also switching them in the two xdoc::lis (i.e. first describing :base-case-then, then :base-case-else briefly).

[acoglio]

It may be cleaner to have an explicit case/check for a quoted constant, between the previous check (for variables) and this check (where the use of ffn-symb suggests that we are in the case of a call term.

[gjurgensen]

Thanks Alessandro, I made some updates. I had meant for the pseudo-termp theorems to be local originally; it was an oversight that they were not.

I also tried to improve the documentation of the find-a-base-case functions. Hopefully it is clearer now.

[acoglio]

Looks good, thanks!