Closed benjub closed 2 years ago
Spec changes should be discussed on the mailing list. For now, following the existing spec more closely sounds like the right move.
It'd be good to eliminate the recomputation, but I don't think it's a showstopper.
Factored out the code for reading p-statements, hence avoiding the above mentioned code repetition. Also, added check for multiply defined labels. @david-a-wheeler: just to be precise: the bugs (or rather, imprecisions compared with the specs) that I fixed in my recent PRs were all already present in the older version of mmverify.py before I worked on it.
@benjub - oh, I see! If the possible-bug is already there, then let's carry on. A future fix might make the tool check the spec more carefully - or alternatively, we can change the spec - but that would be a different matter.
These checks are added in order to follow the specification more closely. Bug was reported in https://groups.google.com/g/metamath/c/PAm7YQb2qkw/m/OcDhSoCFAgAJ
There is a bit of code repetition since the
readstmt
method can now tell if one is reading before $= or after it, but this fact is recomputed later. One could code a general methodread_eapd_stmt
with anend_tokens
argument (typically, either {'$.'} or {'$=', '$.'}), and then methods using it:read_ea_stmt
,read_d_stmt
,read_p_stmt
, with the latter returning a couple (stmt, proof).Requiring that all variables in a $d-statement be typed as well would simplify the specification a bit. Removing $v altogether would simplify the specification further (since then, for a variable, being active and being typed would be one and the same thing). This change would be backward compatible (in that databases complying with the old specification would comply with the new one). Thoughts ? @tirix @digama0 ?