feat(tactic/solve_by_elim): add accept parameter to prune tree search

[kim-em]

Adds some features to solve_by_elim, to allow pruning of the search tree.

From the doc-string of solve_by_elim.basic_opt:

/--
Configuration options for `solve_by_elim`.

...
* `accept` determines whether the current branch should be explored.
   It takes the current state of original goals as a `list expr` argument,
   and should fail to signal omitting this branch.
   By default `accept := λ _, skip` always succeeds.
* `pre_apply` specifies an additional tactic to run before each round of `apply`.
...
-/

[robertylewis]

It takes the current state of original goals as a list expr argument,

I don't really follow this. (What is a "current state of original goals"?) At least, I have no idea how I'd use this in practice. Could you add an example of when this option is useful and the syntax that would be used to give it?

[kim-em]

@robertylewis, I've updated the documentation in a few places.

The main doc-string for solve_by_elim now says:

- accept: a subsidiary tactic `list expr → tactic unit` that at each step is passed the original goals
    (which may by now be partially solved by previous `apply` steps).
    If the `accept` tactic fails,
    `solve_by_elim` will abort searching the current branch and backtrack.
    This may be used to filter results, either at every step of the search,
    or filtering complete results
    (by testing for the absence of metavariables, and then the filtering condition).

In the doc-string on the configuration structure that contains accept I've written much the same, and included a pointer to the example in the test file, which I've tidied up and improved the explanation for.

Does this make more sense?

(I use this accept parameter in a fundamental way in the equiv_rw PR I've just made.)

[kim-em]

I've also add a module doc.

[robertylewis]

Sorry, this line is still confusing me. I would guess first that it's looking for a list of mvars, and second that it's looking for a list of the types of these mvars. In the code, it looks like you give it neither -- you instantiate the mvars before passing them to accept. Is that optional, or required? What's structure is this list expr argument expected to have?

[kim-em]

Okay, I've tried again.

The idea is that when solve_by_elim is first invoked, we call get_goals, and stash them. Now, at every step in the search tree, we take those "original goals", instantiate metavariables in them (as those original goals have by now been partly solved by previous apply steps), and pass them to the accept tactic. Thus the accept tactic can inspect the history of apply steps that have succeeded up to this point, by looking at how the original metavariables from get_goals have been partially unified.

The main change I made in the docs is to replace phrases like "original goals", explicitly saying that solve_by_elim calls get_goals:

It is passed the original metavariables reported by get_goals when solve_by_elim started, as a list expr argument (these metavariables may by now have been partially solved by previous apply steps), ...

I agree this is non-obvious, and my doc-strings were not adequate, so please tell me if we're still not there yet!

[gebner]

accept is run before the current goals are explored, right? It would be good to clarify that in the docstring.

[kim-em]

Clarified!