selecting spider with Poly phase results in NotImplementedError in proof mode

[dlyongemallo]

Steps to repro:

1. Start a new graph (or edit the demo graph)
2. Add a Z-spider with a phase of, e.g., a (or edit any spider of the demo graph to give it a Poly phase)
3. Click "Start derivation"
4. Select the spider (either by clicking on it, or dragging a selection box that includes it)

Expected: spider is selected

Actual: NotImplementedError is raised with message "denominator not implemented for symbolic Poly".

[RazinShaikh]

When PyZX was built, phases were fractions multiplied by pi. That's why a lot of functions explicitly ask for numerator or denominator of phases. It is not clear to me what should be returned to these functions when they ask for numerator/denominator of symbolic variables. So I left these functions unimplemented. If you have any suggestions on how to tackle this, please let me know.
https://github.com/Quantomatic/pyzx/blob/346346159b53221617c89193158a050280c4e4a9/pyzx/symbolic.py#L311-L317

[dlyongemallo]

I think at this point the right thing to do would be to write a design doc for PyZX and carefully think through of its components and how they should handle phases specified in various ways, and then go through the code to ensure that everything behaves as intended or even rewrite some of the components from scratch where it makes sense. I think any other approach is likely to lead to serious tech debt and difficult-to-reason-about bugs later.

Sorry if that isn't immediately helpful.