Some unused variables

[benjub]

1. As noted in What does stat_type do? #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.

2. As mentioned in Frame in make_assertion appears to be unused. #3, the variable frame in the function make_assertion is unused. It makes sense since the latest frame (the "present scope") is not particularly relevant to the function make_statement: what is relevant is the "union of the framestack", which is why in that function, self only appears as in self. I think that variable could be removed.

3. The function verify has an unused argument stat_label. The function verify (stat, proof) verifies that proof is a correct proof of stat, and the label of the statement has nothing to do with it. I think that argument could be removed.

4. The use of autopep8 formatting changes indentations slightly. Should this be adopted ?

5. In the three functions lookup_c/v/d, the reversed seems to be superfluous ? In lookup_e/f, it seems correct to have reversed since this will return the label of the latest active e/f hypothesis with given statement. Similarly correct for both uses in make_assertion.

(letting @raphlinus and @sctfn know)

[benjub]

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

[benjub]

I modified the code on my local fork (https://github.com/benjub/mmverify.py/tree/streamline). In particular:

• removed unused variables (or used underscores when in tuples)
• removed need for collections module (deques are not necessary)
• documented code with docstrings for each function and class
• some code cleaning, streamlining, reordering, variable renaming, in order to improve clarity and readibility
• corrected some message typos
• fixed behavior/bug to allow $a-labels as beginning as well as stopping labels
• fixed bug that ignored multiple $v or $c declarations in same scope
• avoid some superfluous reversals and computations (mainly, pass f_hyp and e_hyp as arguments to avoid recalling make_assertion)
• updated code from deprecated 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 ?

[david-a-wheeler]

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.

[benjub]

@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)

[benjub]

Closing since fixed in #7.

[david-a-wheeler]

Speed is good, but correctness is more important :-).