Add a "statement use" option

[tirix]

As suggested by @GinoGiotto in a comment in #3399, this adds an option to get direct of indirect usage of theorems, given by the list of their labels.

[GinoGiotto]

That's very nice! Definitely I'll apply it for axiom minimizations (this is useful as well for activities like metamath/set.mm#3431, because I needed to list all theorems using df-clel but not ax-8, and --axiom-use doesn't tell definitions, so it wasn't enough for that).

Thank you so much for this work!

[digama0]

Suggested change

	.ok_or("Expected list of Metamaths labels".to_string())
	.ok_or("Expected list of labels".to_string())

I don't think we need to specify this, we don't usually qualify the term elsewhere. We could clarify the grammar in the error message if you think it helps though.

[digama0]

This is also a good place to use glob patterns, if we have them (I think david had an implementation in another PR?) (We can do this in a follow up PR if you prefer)

[tirix]

We did not keep the glob patterns in the final solution. I think eventually the best is to first split the project into library/command line tool, and then only include the glob library of choice into the latter. So yes, let's keep that for later.

[GinoGiotto]

I executed the command cargo run -- set.mm --stmt-use nfmo,nfmod,nfmod2 and it works, but it prints the output directly on the command line. Can the output be printed in a text file like --axiom-use does?

[tirix]

It works, but it prints the output directly on the command line.

Yes, that's not ideal. How about changing the parameters so that --stmt-use would take two parameters, the file name and the list of labels, like this:

OPTIONS:
    -X, --axiom-use <FILE>            Generate `axiom-use` file
        --stmt-use <FILE> <LABELS>    Outputs statements directly or indirectly using the given list of statements

[GinoGiotto]

Sounds good, I like it.

[tirix]

I've committed an update which does that.

I could not use the validator function because it would be applied both on the file path and the label list, so I moved it into our own code.