Closed benjub closed 2 years ago
It seems also that Line 67 is superfluous, that is, the bloc
if tok == None: return None
if tok == '$(':
while tok != '$)':
tok = self.read()
else:
return tok
can be replaced by
if tok == '$(':
while tok != '$)':
tok = self.read()
else:
return tok
Also: typos within comments: Incusion --> Inclusion have be length --> have length
I modified the code on my local fork (https://github.com/benjub/mmverify.py/tree/streamline). In particular:
collections
module (deques are not necessary)make_assertion
)optparse
to argparse
and added argument parsing for verbosity, database, and logfile.As a result, performance (speed) improved by 6%--10% on set.mm and iset.mm.
@david-a-wheeler : should I do a PR ?
Definitely do a PR. If it seems likely the variable will be used later, documenting how to get it later in a comment might be appropriate.
@david-a-wheeler : or maybe you want to go directly for the 4 times faster (!!!) version: https://github.com/benjub/mmverify.py/tree/faster ? (which still needs some checking and testing)
Closing since fixed in #7.
Speed is good, but correctness is more important :-).
As noted in #1,
stat_type
is unused. It is initialized to the type of the statement whose proof is being verified, so in (i)set.mm it will always be"|-"
(but it could take multiple values in a given database). The verification of a proof does not involve the typecode of the statement by itself. I think that variable could be removed.As mentioned in #3, the variable
frame
in the functionmake_assertion
is unused. It makes sense since the latest frame (the "present scope") is not particularly relevant to the functionmake_statement
: what is relevant is the "union of the framestack", which is why in that function,self
only appears asin self
. I think that variable could be removed.The function
verify
has an unused argumentstat_label
. The functionverify (stat, proof)
verifies thatproof
is a correct proof ofstat
, and the label of the statement has nothing to do with it. I think that argument could be removed.The use of autopep8 formatting changes indentations slightly. Should this be adopted ?
In the three functions
lookup_c/v/d
, thereversed
seems to be superfluous ? Inlookup_e/f
, it seems correct to havereversed
since this will return the label of the latest active e/f hypothesis with given statement. Similarly correct for both uses inmake_assertion
.(letting @raphlinus and @sctfn know)