grammar bugfixes

[digama0]

Fixes #135 (or at least, that's the idea). I have a minimal example of the bug currently afflicting set.mm master:

  $c = class wff setvar -> ( ) |- + [ ] $.
  $( $j syntax 'setvar' 'class' 'wff'; syntax '|-' as 'wff'; $)
  $v x A B ph ps $.
  vx $f setvar x $.
  wph $f wff ph $.
  wps $f wff ps $.
  cA $f class A $.
  cB $f class B $.
  cv $a class x $.
  wn $a wff [ A ] $.
  wceq $a wff A = B $.
  wi $a wff ( ph -> ps ) $.
  cdif $a class ( A + B ) $.
  ax1 $a |- [ x ] $.
  ax2 $a |- ( x = x -> ph ) $.

The PR currently fixes the ax1 bug, but the ax2 bug is still not fixed. (Note the cdif axiom, which is not used but seems to muck up the grammar somehow.)

I have to say, I am really considering doing the parser again from first principles. There are way too many hacks in the current implementation and I feel like I'm just piling more on here, but I want to get set.mm green again before considering more complicated refactors.

cc: @tirix

[tirix]

The PR currently fixes the ax1 bug, but the ax2 bug is still not fixed. (Note the cdif axiom, which is not used but seems to muck up the grammar somehow.)

In my opinion, the ax1 is not an issue: the type_conversion was simply missing in the database (see #138 ). What is your fix?

I have to say, I am really considering doing the parser again from first principles. There are way too many hacks in the current implementation and I feel like I'm just piling more on here, but I want to get set.mm green again before considering more complicated refactors.

The parser was one of my very first attempts at Rust and I was both learning Rust and Metamath parsing when I wrote it. On the other hand I'm proud I "somehow" managed and got a solution with no backtracking whatsoever.

[tirix]

There are lots of changes to review. I'll need a bit more time to review and understand what is functionality change and code improvement.

[digama0]

There are lots of changes to review. I'll need a bit more time to review and understand what is functionality change and code improvement.

The changes are summarized as follows:

• moved a comment from FormulaBuilder impl to type, added Debug impl
• added support for parsing syntax FOO BAR BAZ; as equivalent to syntax FOO; syntax BAR; syntax BAZ;
• moved all parsing for syntax to initialize() instead of duplicating it between initialize and handle_commands
• main logical change: previously the self.type_conversions field was completely ignored except at the very end of the formula (via the symbol_enum.peek().is_none() check). Now if other methods fail it tries a random type conversion and loops. That way you can get paths like reduce -> type mismatch -> reduce type conversion -> type match -> shift where previously the type mismatch would cause an overall failure.
• The symbol_enum.peek().is_none() statement becomes superfluous with this change, so it is commented out (pending verification that this is the correct approach).