API issues

[digama0]

This is a collection of issues I notice while looking at the docs.

• [x] Database has a new method which takes a DbOptions which implements Default, but Database doesn't impl Default.
• [x] Is the default instance for DbOptions actually correct?
• [ ] Database::parse has a complicated input type. The desired flexibility is better accommodated with an impl FileResolver, and it should have a basic API that takes an impl Read or impl BufRead.
• [x] Database::parse_result is a public method that returns a private object.
• [x] Nameset::update shouldn't be public? It can't be called from Database::name_result.
• [ ] The nameset interface is too complicated. You map atoms to tokens, tokens to LookupLabel, then pull out the label and... do something undocumented that depends on SegmentSet to get a statement.
• [ ] Frame is unrecognizable compared to the MM spec. Most of the fields probably shouldn't be public, and it should have an actual API for getting the bits out.
• [ ] Diagnostic doesn't have docstrings for the variants.
• [ ] Database::export should output to an impl Write rather than opening a file itself, and statements should be identified in a uniform way, e.g. by StatementAddress rather than using &str, Token, Atom, StatementAddress and StatementRef depending on the function.
• [x] Database::statement and Database::export shouldn't need to mutate the database.
• [ ] Database::print_grammar, Database::print_formula etc. look like debugging tools, they shouldn't be in the public API. If they are, they should have a return value or write to an impl Write or something.
• [ ] Database::diag_notations is a weird API. types could be a config struct with boolean fields, and the output could be provided by a callback to allow for incremental rendering and doing whatever the user wants to do with the diagnostics.
• [x] Notation could be swapped out for annotate_snippets::snippet::Snippet
• [ ] Executor should not be public. Also, why is there an async implementation in this crate? Use smol or something.
• [x] export::export_mmp should not be public, it should be a function on Database.
• [x] Formula::display should not produce a string, it should be an object implementing Display. That object could be FormulaRef<'_> which bundles together the formula and references into the Database, so that Formula::iter can also be supported.
• [x] Substitutions implements Index<&Label>, which uses an unnecessary indirection since Label is a 4 byte Copy type.
• [x] Formula::build_syntax_proof has an unused A type parameter.
• [x] Grammar::parse_formula takes a &mut dyn Iterator but it could take &mut impl Iterator
• [x] outline says it is not stable, so it should probably not be public at all.
• [ ] There should be a more strongly typed way to inspect StatementRefs. Not all statement kinds have all the data, and the API should be a guide to what has what.
• [ ] parser has lots of public types that should not really be public, or should be public with private members.
• [x] parser::as_str is unsound and should at least be private
• [x] OutlineNode::get_name is unsound because OutlineNode::name is public
• [ ] ProofTree is not stand-alone, it requires ProofTreeArray, so it should probably be exposed as ProofTreeRef retaining a reference to the array
• [x] ProofTreePrinter has too many public fields
• [ ] VerifyExpr should not be public
• [ ] Frame has too many public fields, and in particular optional_dv is public but has a private type
• [x] util should not be public
• [ ] ProofBuilder::build has a complicated type
• [x] Why are filename, fnv and regex being re-exported? I don't see any need to do this

[tirix]

Thanks Mario! As for issues on my contributions:

Database::print_grammar, Database::print_formula etc. look like debugging tools, they shouldn't be in the public API. If they are, they should have a return value or write to an impl Write or something.

Yes, they indeed are debugging tools. Ok with that change for Grammar. For Formula, this could be done on the proposed FormulaRef:

• a Display implementation which would print the formula in a readable format,
• a Debug implementation which would, in addition, print the formula tree in a LISP format like wceq ( cA cB )

Substitutions implements Index<&Label>, which uses an unnecessary indirection since Label is a 4 byte Copy type.

Fix in #34

Grammar::parse_formula takes a &mut dyn Iterator but it could take &mut impl Iterator

Fix in #34

Formula::build_syntax_proof has an unused A type parameter.

Fix in #34

outline says it is not stable, so it should probably not be public at all.

Actually is it just as (un)stable as the rest, and I've also used it in a toy dependent project. I'd say we keep it like that! :-)

For the rest - some of them would be included in an API revamp around Database as proposed in #24 . Snippet looks very interesting!

[tirix]

OutlineNode::get_name is unsound because OutlineNode::name is public

Fix in #56

Database::diag_notations is a weird API. types could be a config struct with boolean fields, and the output could be provided by a callback to allow for incremental rendering and doing whatever the user wants to do with the diagnostics.

The output of Database::diag_notations is now indeed provided through a callback since #49, but the types parameter has not been changed yet.

[tirix]

util should not be public

Fix in #42

Why are filename, fnv and regex being re-exported?

Fix in #42

[tirix]

parser::as_str is unsound and should at least be private

It is used in mm-web-rs, metamath-vspa, rumm, and metamath-web, that's all 4 current dependencies. I think we shall keep it public.

What's your opinion, @digama0 ?

[tirix]

Diagnostic doesn't have docstrings for the variants.

Yes but are the names and the messages in to_snippet not self-explanatory already? In any case, this would be easy to add.

[digama0]

parser::as_str is unsound and should at least be private

It is used in mm-web-rs, metamath-vspa, rumm, and metamath-web, that's all 4 current dependencies. I think we shall keep it public.

What's your opinion, @digama0 ?

Well yes, it is unsound but convenient so I'm not surprised it is used. To avoid breakage, I think it would be fine to replace the existing as_str with one that does from_utf8().unwrap() instead of from_utf8_unchecked(), and those dependents can either make their own private version that does the unsound thing or just use the runtime check. We can also add statement_as_str() type methods on getters that both retrieve a string and convert it to a &str so that they can make use of the invariant to soundly use from_utf8_unchecked. (Be careful that this is actually correct though; the parser doesn't just bail on non-ascii input, so non-ascii can end up in some data structures.)

Diagnostic doesn't have docstrings for the variants.

Yes but are the names and the messages in to_snippet not self-explanatory already? In any case, this would be easy to add.

Not quite; the main purpose of the docs on the variants would be to explain what the arguments to the variants are. Beyond that, copying the first line "short" message from the error report is probably sufficient.

[tirix]

as_str

Actually the definition of as_str is

/// Transmutes this token into a Rust string.
#[must_use]
pub fn as_str(ptr: TokenPtr<'_>) -> &str {
    std::str::from_utf8(ptr).expect("TokenPtr is supposed to be UTF8")
}

So it is not unsafe. It'd rather the other way around: it might be an optimization to use from_utf8_unchecked() internally.

Diagnostic doesn't have docstrings for the variants.

Ok, agreed.

[digama0]

@tirix Oh, if that is as_str then I guess the problem has already been addressed at some point. I will mark it as done.