metamath / metamath-knife

Metamath-knife can rapidly verify Metamath proofs, providing strong confidence that the proofs are correct.
Apache License 2.0
26 stars 11 forks source link

refactor outline construction #58

Closed digama0 closed 2 years ago

digama0 commented 2 years ago
digama0 commented 2 years ago

I think a rebuild mechanism would be useful, but it would have a different type signature; I considered making the core of this algorithm more like an iterator, with a OutlineBuilder containing the local variables in this loop. Presumably that is the data structure you would want to have an append method on. Outline in some sense loses information since it closes off the nodes at the end of the file, making them unsuitable for later appends. (I didn't check whether tree nodes are immutable once created, but the code seems to be written as if they are so I went with that. If you allow the tree nodes themselves to be modified, you could append directly to an Outline by pushing to the appropriate node along the right spine of the tree.)