ISLE: inlining terms

#### Feature

Instead of emitting a function call when a constructor or extractor is used, under some circumstances ISLE should inline the body of the term at the call site. It currently does this for all internal extractors, but not for anything else.

Which terms are useful to inline varies depending on whether the ISLE source is being used for code generation or for formal verification, so we should figure out how best to specify that.

#### Benefit

If inlining is done before building the "trie-again" representation, then overlap checking can be more precise, allowing fewer rules to have priorities. The following step, of serializing the trie-again sea of nodes into a decision tree, also relies on overlap checking for optimization and can generate better code.

For the purposes of formal verification, inlining a term means that term does not need a hand-written spec because it can just be incorporated into a larger verification query.

See also #8599.

#### Implementation

With our current representations, inlining a term preserves semantics as long as the term is declared either `partial` or `multi`, or we can prove that for every possible input there is some rule in the term which will match that input. A reasonable approximation to the latter condition is to check if there is some rule which can match all inputs. If we add the ability to represent cases where terms currently may panic then we can inline all terms, but we can cover a lot of useful cases without doing that.

Our current strategy for building a `trie_again::RuleSet` doesn't give us an easy way to inline terms which are defined by more than one rule. I'd like to see a first implementation of inlining supporting only single-rule terms; let's come back to the multi-rule terms later.

In `sema.rs`, the `Rule::visit` method is almost exactly what we need for inlining a rule. The key difference is that instead of calling `visitor.add_arg` to create a fresh `PatternId` for each argument, we need to provide a `PatternId` from the caller. This method will then return an `Expr` to the caller, which it can use in subsequent bindings. https://github.com/bytecodealliance/wasmtime/blob/7e8abe388e7bd6ae28d4335a3cd89c8692c5c98f/cranelift/isle/isle/src/sema.rs#L870

For multi-rule terms, I think the relatively simplest thing to do is add "push" and "pop" operations to the visitor traits. In `trie_again`'s implementation of those traits, instead of keeping a single current rule, it would keep a collection of rules. `push` would clone all of them and keep a stack of pending partial rules; `pop` would add all the current rules to the rule set and restore the top group from the stack as the new current rules; and all the other visitor methods would apply to all rules in the current rules group.

In the future though, I'd like to explore unifying alternatives within bindings and constraints. I think it's always possible to introduce "union" binding/constraints over a list of alternatives, and have later parts of the rule use only the values introduced by the union binding. That way there's no combinatorial explosion from inlining. It makes overlap checking and serialization more confusing though.

cc: @avanhatt @mmcloughlin