search

david-a-wheeler / mmverify.py

Metamath verifier in Python
MIT License
35 stars 10 forks source link

make constants global #11

Closed benjub closed 2 years ago

benjub commented 2 years ago

Constants had local scope, contrary to the specification. This PR makes constant declarations global: wherever they are declared, once they are declared, they stay active forever. As said in the Metamath book, this is necessary, since $a and $p statements stay forever active (they may be used by any later proof), so their statements have to keep the same meaning forever.

BEFORE MERGING, question to anyone, maybe @tirix or @digama0 : to make constants global, I added a field to the class of databases (the set self.constants in class MM). I then had to move add_c, add_v, add_f from being FrameStack methods to being MM methods (since they need to know the set of declared constants). I could have left them as FrameStack methods and added to them an argument constants that is passed when these methods are called in the MM class. I thought the present choice is more natural, but maybe more experienced programmers have an advice concerning these issues ?

tirix commented 2 years ago

Your choice seems a better one to me because it avoids passing around the constants which reside at the top level. In C world, passing less arguments around means a tiny bit less of copying, and smaller stack frames, so a marginally more performant code (but I don't know if this applies to Python) This also means these add_ functions are placed at a level to which they logically belong since they need to access this now-global constants.

So, fine to me.